Encyclopedia Mathematics Mathematics Distance Shell Multiplicity Erdos132 From Support Conway Endpoint Di

ARTICLE 3 claims 3 theorems

Mathematics Distance Shell Multiplicity Erdos132 From Support Conway Endpoint Di

A machine-checked proof shows that if three geometric conditions hold, then a classical bound on repeated distances follows, without proving those conditions themselves.

Verify this page

The Erdős 132 theorem

Erdős problem #132 asks how many times a single distance can occur among n points in the plane. The classical answer, proved by Erdős in 1946, is that the maximum multiplicity of any distance is at most n3/2. The Recognition Science library formalizes this problem in a different setting: it counts ordered pairs of points at a given distance, which doubles the usual count, so the classical threshold ≤ n becomes ≤ 2n in this ordered convention.

The declaration erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live is a theorem in the machine-checked library of formal theorems. It states that if three hypotheses hold, then the ordered Erdős bound follows. The three hypotheses are: a support bound on a Conway thrackle, a uniqueness certificate for diameter intersections, and a pointwise deep-layer screening certificate. Each is a precise geometric condition about how diameter segments in a finite planar set can intersect. The theorem proves the implication: these three conditions together force the Erdős bound.

The theorem does not prove that any of the three hypotheses actually holds. It proves only that they are sufficient. The library also records a residual pack structure that bundles the three hypotheses into a single object, and a second theorem that derives the Erdős bound from that bundle. The first theorem is the live one; the second is a packaging convenience.

What this means in plain terms: the framework has reduced Erdős problem #132 to three separate geometric questions. If those questions have positive answers, the classical bound follows. The reduction is fully checked by the machine; the three questions themselves remain open targets. This is a common pattern in the library: a large theorem that rests on unproved premises, each of which is a named target for future work.

THEOREM erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live · IndisputableMonolith/Mathematics/DistanceShellMultiplicity.lean
erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live · IndisputableMonolith/Mathematics/DistanceShellMultiplicity.lean:6200 
/-- Live corrected Conway-form final assembly: support-level Conway counting,
endpoint-disjoint diameter intersection uniqueness, and pointwise deep-layer
screening imply Erdős #132.  The shared-endpoint diameter representative case is
already proved by `shared_endpoint_diameter_representatives_meet_simply`; the
endpoint-disjoint existence part is supplied by `fourPointDiameterCrossing_thm`.
-/
theorem erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live
    (hSupport : ConwayThrackleSupportBoundOnSupport)
    (hUnique : EndpointDisjointDiameterIntersectionUniqueCertificate)
    (hScreen : PointwiseDeepLayerScreeningCertificate) :
    Erdos132Ordered :=
  erdos132_from_diameter_sparsity_and_no_deep_layer
    (diameter_shell_sparse_from_diameter_conway_bound
      (diameter_conway_bound_from_support_conway hSupport
        (diameter_support_forms_conway_from_simple_representatives
          (diameter_support_simple_representatives_from_ordered_representatives
            (distinct_diameter_representatives_meet_simply_from_cases
              shared_endpoint_diameter_representatives_meet_simply
              (endpoint_disjoint_diameter_representatives_meet_simply_from_unique_live hUnique))))))
    (no_deep_layer_from_pointwise_screening_certificate hScreen)
THEOREM Erdos132ConwayEndpointDisjointUniquenessScreeningResidualPack · IndisputableMonolith/Mathematics/DistanceShellMultiplicity.lean
Erdos132ConwayEndpointDisjointUniquenessScreeningResidualPack · IndisputableMonolith/Mathematics/DistanceShellMultiplicity.lean:6221 
/-- 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
THEOREM erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live · IndisputableMonolith/Mathematics/DistanceShellMultiplicity.lean
erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live · IndisputableMonolith/Mathematics/DistanceShellMultiplicity.lean:6200 
/-- Live corrected Conway-form final assembly: support-level Conway counting,
endpoint-disjoint diameter intersection uniqueness, and pointwise deep-layer
screening imply Erdős #132.  The shared-endpoint diameter representative case is
already proved by `shared_endpoint_diameter_representatives_meet_simply`; the
endpoint-disjoint existence part is supplied by `fourPointDiameterCrossing_thm`.
-/
theorem erdos132_from_support_conway_endpoint_disjoint_uniqueness_and_deep_screening_live
    (hSupport : ConwayThrackleSupportBoundOnSupport)
    (hUnique : EndpointDisjointDiameterIntersectionUniqueCertificate)
    (hScreen : PointwiseDeepLayerScreeningCertificate) :
    Erdos132Ordered :=
  erdos132_from_diameter_sparsity_and_no_deep_layer
    (diameter_shell_sparse_from_diameter_conway_bound
      (diameter_conway_bound_from_support_conway hSupport
        (diameter_support_forms_conway_from_simple_representatives
          (diameter_support_simple_representatives_from_ordered_representatives
            (distinct_diameter_representatives_meet_simply_from_cases
              shared_endpoint_diameter_representatives_meet_simply
              (endpoint_disjoint_diameter_representatives_meet_simply_from_unique_live hUnique))))))
    (no_deep_layer_from_pointwise_screening_certificate hScreen)

What this page does not claim

The theorem does not prove Erdős problem #132 itself, since its three hypotheses remain unproved. The theorem does not establish any physical or recognition-theoretic interpretation of the distance shell multiplicity. The theorem does not give a constructive method for finding the bound; it only proves a conditional implication.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND