Mathematics Distance Shell Multiplicity Erdos132 From Conway Endpoint Disjoint C

The residual pack

The classical problem is Erdős problem 132: how many times can the same distance occur among n points in the plane? The standard answer is that no distance can occur more than n times, and the standard proof is a celebrated result by Szemerédi and Trotter. This declaration is a formal, machine-checked proof that a specific route to that bound is valid.

The route is conditional. The proof establishes that if three separate geometric facts hold, then the Erdős bound follows. The first fact is a bound on the number of certain crossing structures, named after Conway's thrackle conjecture. The second is a uniqueness statement about diameters: two different longest segments in a point set that do not share an endpoint cannot intersect in two distinct points. The third is a screening condition about the layers of distance shells. The declaration packages these three conditions into a single structure and proves that the package implies the Erdős bound.

The proof is a theorem in the framework's machine-checked library of formal theorems. It is not a proof of the three conditions themselves; those are assumed as inputs. The declaration is a bridge: if the conditions are ever proved, the Erdős bound is proved. The library also contains a separate theorem that derives the Erdős bound from the same three conditions, so the pack is a reusable certificate.

What the declaration does not claim is as important as what it proves. It does not prove the Conway thrackle bound, the diameter intersection uniqueness, or the screening condition. It does not prove the Erdős bound outright. It only proves the implication from the three conditions to the bound. The three conditions remain open targets for future proofs.

/-- The live endpoint-disjoint uniqueness residual package proves Erdős #132. -/
theorem erdos132_from_conway_endpoint_disjoint_uniqueness_screening_residual_pack
    (P : Erdos132ConwayEndpointDisjointUniquenessScreeningResidualPack) :
    Erdos132Ordered :=
  erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live
    P.support_conway_thrackle_bound
    P.endpoint_disjoint_diameter_intersection_unique
    P.pointwise_deep_layer_screening

/-- Live residual package after closing the shared-endpoint diameter
representative case. -/
structure Erdos132ConwayEndpointDisjointUniquenessScreeningResidualPack : Prop where
  support_conway_thrackle_bound : ConwayThrackleSupportBoundOnSupport
  endpoint_disjoint_diameter_intersection_unique :
    EndpointDisjointDiameterIntersectionUniqueCertificate
  pointwise_deep_layer_screening : PointwiseDeepLayerScreeningCertificate

What this page does not claim

The declaration does not prove the Conway thrackle support bound, the diameter intersection uniqueness condition, or the pointwise deep layer screening condition. The declaration does not prove the Erdős bound outright; it proves only the implication from those three conditions to the bound.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Mathematics/DistanceShellMultiplicity.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: