Mathematics Distance Shell Multiplicity

Distance shells and their occupancy

In a finite set of points in the plane, a distance shell is the collection of all pairs whose separation equals one particular value. The multiplicity of that shell is the number of pairs in it, its occupancy. For example, in a square of side length one, the four sides form a shell of multiplicity four at distance one, and the two diagonals form a shell of multiplicity two at distance the square root of two. This notion is entirely classical: it is the raw material of a famous problem posed by Paul Erdős in 1946, which asks whether the number of distinct distances determined by n points can be as small as n divided by the square root of the logarithm of n.

The subject here, DistanceShellMultiplicity, formalizes this idea in a machine-checked library of formal theorems. It works with ordered pairs of points, which doubles the count for any positive distance: an unordered pair {a, b} appears as both (a, b) and (b, a). The classical threshold of n distinct distances therefore becomes a threshold of 2n ordered pairs. The subject proves basic structural facts about these shells, such as the uniqueness of the diameter shell: any finite set has exactly one largest distance value, and that value is shared by all pairs at maximum separation.

The deeper content of the subject is a chain of implications aimed at Erdős's problem. It introduces a certificate called EndpointDisjointDiameterIntersectionUnique, which asserts that two distinct diameter segments that do not share an endpoint can intersect in at most one point. From this, together with a bound on a combinatorial structure called a Conway thrackle and a screening condition on point layers, the subject derives a statement called Erdos132Ordered. This is a formal version of a bound on the number of distinct distances, though the full resolution of Erdős's problem remains open; the subject reduces it to three named hypotheses that are not yet proved.

In Recognition Science, the subject reinterprets a distance shell physically. A distance value is not only a geometric separation but a two-body recognition-energy shell: the energy cost for two points to be recognized as being at that separation. The multiplicity is then the occupancy of that energy shell, the number of pairs sharing that cost. This is a definitional choice, a model, not a derived theorem. The framework's broader claim, that recognition cost is forced by a small set of axioms, is separate from this subject, which operates on the classical geometry side and supplies the combinatorial scaffolding that a physical derivation would later need.

What the subject establishes in plain language is a precise, machine-checked dictionary between a classical counting problem and a physical energy picture, plus a conditional route toward the Erdős bound. A reader can now see that the number of distinct distances in a point set is the number of occupied energy shells, and that bounding that number is equivalent to controlling how many pairs can share the same recognition cost. The three unproved hypotheses are the remaining obstacles; the subject does not claim to have removed them.

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

/-- Forget orientation of an ordered edge. -/
def unorderedEdgeOfOrdered (e : Point2 × Point2) : Sym2 Point2 :=
  Sym2.mk e

/-- The diameter value is uniquely determined by the set: it is the maximum of
the ordered distance spectrum, and two maxima of the same set are equal. -/
theorem isDiameterShell_unique
    {A : Finset Point2} {Δ₁ Δ₂ : ℝ}
    (h₁ : IsDiameterShell A Δ₁) (h₂ : IsDiameterShell A Δ₂) :
    Δ₁ = Δ₂ :=
  le_antisymm (h₂.2 _ h₁.1) (h₁.2 _ h₂.1)

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

/-- The component package specified by the proof plan.  Each field is a
standalone classical bridge target; together they close the shell-flux bridge.
-/
structure ShellFluxComponentPack : Prop where
  pair_budget_pressure :
    ∀ᶠ n in atTop,
      ∀ A : Finset Point2,
        A.card = n →
          ∀ Δ : ℝ, IsDiameterShell A Δ → PairBudgetPressure A Δ
  low_shell_structure :
    ∀ᶠ n in atTop,
      ∀ A : Finset Point2,
        A.card = n →
          ∀ Δ : ℝ,
            IsDiameterShell A Δ →
              PairBudgetPressure A Δ → LowShellStructure A Δ
  layer_flux_alternative :
    ∀ᶠ n in atTop,
      ∀ A : Finset Point2,
        A.card = n →
          ∀ Δ : ℝ,
            IsDiameterShell A Δ →
              LowShellStructure A Δ → LayerFluxAlternative A Δ
  deep_layer_screening :
    ∀ᶠ n in atTop,
      ∀ A : Finset Point2,
        A.card = n →
          ∀ Δ : ℝ,
            IsDiameterShell A Δ →
              LowShellStructure A Δ → DeepLayerScreening A Δ

What this page does not claim

The subject does not prove the full Erdős distinct distances problem; it derives a conditional bound from three unproved hypotheses. The physical interpretation of a distance shell as a recognition-energy shell is a definitional model, not a derived theorem. The subject does not establish the framework's central cost function or the forcing chain; it operates on the classical geometry side.

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: