erdos132_from_final_components
plain-language theorem explainer
Final assembly of the ordered Erdős #132 statement from three classical geometry inputs: diameter-shell existence, Hopf–Pannwitz diameter sparsity, and no residual deep-layer case in the low-shell regime. Cite this when packaging the RS formalization of Erdős #132 after the bookkeeping reductions. The proof is a one-line term composition: convert the component pack to ordered Hopf–Pannwitz form, then apply the no-deep-layer bridge.
Claim. Assume a Hopf–Pannwitz component pack (eventual existence of a diameter shell, and a sparsity bound on that diameter shell) and that, for all sufficiently large finite planar sets, whenever $\Delta$ is a diameter shell with low-shell structure, the residual deep-layer case does not occur. Then the ordered Erdős #132 claim holds: for every sufficiently large finite $A\subset\mathbb{R}^2$ there exist distinct distances $r\neq s$ that are both sparse shells of $A$.
background
This module is the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. The development uses ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
The target Erdős #132 in ordered normalization asserts that every large enough finite planar set has two distinct sparse distance shells. The Hopf–Pannwitz component pack splits the classical sparsity surface into two props: eventual diameter-shell existence, and a diameter-shell sparsity bound. The remaining geometric obstruction after finite accounting is the low-shell no-deep-layer statement: in the low-shell regime, a diameter shell cannot realize the residual deep-layer case.
Cost-algebra $H(x)=J(x)+1$ and related functional-equation reparametrizations appear in the dependency graph as ambient RS infrastructure; they are not the geometric content of this assembly step.
proof idea
Pure term-mode one-liner. First apply the conversion lemma that turns a Hopf–Pannwitz component pack into the ordered Hopf–Pannwitz surface (diameter existence plus diameter sparsity in the ordered-pair normalization). Feed that surface, together with the low-shell no-deep-layer hypothesis, into the already-proved bridge erdos132_from_hopf_pannwitz_and_no_deep_layer, which discharges the ordered Erdős #132 goal. No new geometric argument is introduced here; the declaration only wires the final bookkeeping interface.
why it matters
This is the fully reduced final assembly theorem after the proof-plan bookkeeping: the remaining classical geometry inputs are exactly diameter-shell existence, Hopf–Pannwitz diameter sparsity, and no residual deep-layer case in the low-shell regime. Downstream, the module’s live endpoint residual is the current open surface left once this packaging is in place; the diameter-sparsity assembly comment records that diameter existence and finite bookkeeping are already proved, so the conditional packages the older Hopf–Pannwitz sparsity surface with the low-shell no-deep theorem.
In the RS reading, sparse distance shells are sparse two-body recognition-energy shells. Establishing two distinct sparse shells for large planar sets is the ordered form of Erdős #132 that the module physicalizes. No further used-by parents are recorded yet; the declaration sits at the tip of the assembly chain rather than feeding a named parent theorem in the graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.