orderedShellMultiplicity_eq_diameterOrderedEdges_card
plain-language theorem explainer
For a finite planar point set A and real distance Δ, ordered shell multiplicity at Δ equals the number of ordered pairs in A at Euclidean distance exactly Δ. Anyone proving ordered diameter thrackle or Conway-type bounds for Erdős #132 cites this identification. The proof is pure definitional equality (rfl).
Claim. For every finite set $A\subset\mathbb{R}^2$ and every $\Delta\in\mathbb{R}$, the ordered multiplicity of the distance shell at $\Delta$ equals the cardinality of the set of ordered pairs $(p,q)$ with $p,q\in A$, $p\neq q$, and $\|p-q\|=\Delta$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Points live in the Euclidean plane (Point2 is $\mathbb{R}^2$).
Lean works with ordered pairs rather than unordered edges. For any positive distance the ordered multiplicity is exactly twice the classical unordered multiplicity, so classical thresholds of the form $\le n$ become $\le 2n$. The ordered diameter edge set collects pairs with both endpoints in $A$, distinct, and distance exactly $\Delta$; ordered shell multiplicity is that set's cardinality by design.
proof idea
One-line definitional equality: rfl. The left-hand side (ordered shell multiplicity) is defined to be the cardinality of the ordered diameter edge set on the right-hand side, so the two expressions reduce to the same term.
why it matters
This is the bookkeeping bridge that lets diameter-shell bounds speak in either multiplicity language or edge-set language. Downstream it is applied in diameter_conway_bound_from_support_conway (support-level Conway thrackle plus a diameter support hypothesis yields the diameter-specific ordered multiplicity bound) and in diameter_ordered_bound_from_thrackle_components (no-disjoint-diameter-edges plus the ordered thrackle bound recovers the Hopf–Pannwitz ordered multiplicity bound).
In the RS reading, shell occupancy is recognition-energy occupancy on a fixed two-body distance; equating multiplicity to edge cardinality keeps the combinatorial thrackle/Conway arguments aligned with that physical count. It does not itself invoke the forcing chain (T0–T8) or the RCL; it is pure discrete geometry scaffolding for the Erdős #132 physicalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.