Mathematics Distance Shell Multiplicity Erdos132 From Conway Endpoint Disjoint U

The residual pack

Erdős problem #132 asks how many times a single distance can occur among n points in the plane. Classically, each distinct distance value defines a shell: the set of point pairs at that separation. The framework's library records a physical reading of these shells as two-body recognition-energy shells, where the multiplicity of a distance is the number of pairs occupying that shell. For a positive distance, the framework counts ordered pairs, so the classical threshold of n occurrences becomes 2n.

The declaration erdos132_from_conway_endpoint_disjoint_uniqueness_screening_residual_pack is a theorem in the machine-checked library. It proves that if three separate conditions hold, then the ordered version of Erdős problem #132 follows. The three conditions are: a bound on the support of a Conway thrackle, a uniqueness certificate for diameter intersections, and a pointwise deep-layer screening certificate. The theorem packages these three assumptions into a single structure and derives the Erdős result from them.

The three conditions are not proved in the library. The declaration establishes a conditional result: it shows the logical bridge from the assumptions to the conclusion. The first condition concerns Conway thrackles, a classical object in graph theory. The second concerns diameter shells: for a finite set of points, all diameter edges that do not share an endpoint must meet at a single point. The third concerns a screening process on layers of the distance spectrum. Each is a named certificate, a formal statement that the library treats as an input.

In Recognition Science, this conditional theorem is part of a larger program that reads combinatorial geometry through the lens of recognition costs. The framework models distance values as energy shells and seeks to derive classical results from its own principles. This declaration does not itself establish the Erdős bound; it establishes that the bound follows from the three certificates. The certificates remain open targets for the framework to prove.

What the declaration does not claim is equally precise. It does not prove any of the three certificates. It does not prove the classical unordered version of Erdős problem #132 directly, only the ordered version under the assumptions. And it does not claim that the physical reading of distance shells as recognition-energy shells is established; that reading is a modeling choice, not a theorem.

/-- 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

/-- Number of occupied shells in the ordered distance spectrum. -/
noncomputable def occupiedShellCount (A : Finset Point2) : ℕ :=
  (orderedDistanceSpectrum A).card

What this page does not claim

The declaration does not prove any of the three certificates it assumes. The declaration does not establish the classical unordered version of Erdős problem #132. The physical reading of distance shells as recognition-energy shells is a modeling choice, not a theorem.

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: