dist_sq_unfold
plain-language theorem explainer
Unfolds squared Euclidean distance on the plane as the sum of squared coordinate differences for points in $\mathbb{R}^2$. Diameter-contradiction lemmas in the Hopf–Pannwitz / Erdős #132 shell-multiplicity development cite it to pass from abstract distances to coordinate algebra. Proof applies the Euclidean-space squared-distance identity, reduces the Fin-2 sum, and clears absolute values.
Claim. For any two points $a,b$ in the Euclidean plane $\mathbb{R}^2$ (identified with $\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,2)$), $(d(a,b))^2 = (a_0-b_0)^2 + (a_1-b_1)^2$.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so positive-distance ordered multiplicity is twice the unordered count and the classical threshold $\le n$ becomes $\le 2n$.
Point2 is the plane $\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin},2)$. Distances are the standard Euclidean metric. Downstream diameter arguments place four points in coordinates and need the squared length as an explicit sum of squared coordinate gaps (via Lagrange-type identities relating lens coordinates to cross-distances).
This lemma is the elementary coordinate bridge: it converts the abstract dist on the plane into component arithmetic that orientation and lens-coordinate estimates can consume.
proof idea
Start from the library identity EuclideanSpace.dist_sq_eq a b, which writes squared distance as a sum over the finite index type. Simplify with Fin.sum_univ_two (exactly two coordinates), Real.dist_eq, and pow_two. The remaining absolute values on coordinate differences are removed by linarith using sq_abs on each component, yielding the plain sum of squares.
why it matters
Local plumbing for the Hopf–Pannwitz four-point geometry that underwrites diameter-shell uniqueness in the RS reading of Erdős #132. It is used by properSeparatedDiameterContradiction (properly separated diameter pairs cannot satisfy all four cross-distance bounds; the positive-$\Delta$ orientation-sign core, now an unconditional theorem) and by the sharper sameSideDiameterContradiction (strict same-side orientations of $c,d$ relative to line $ab$ already contradict the diameter bounds).
Those parents place $a,b$ in coordinates, rotate so $(b-a)/|b-a|$ is the first basis vector, and pass to lens coordinates where Lagrange gives $\alpha_c^2+\beta_c^2=(d(a,c))^2$ and analogues. Unfolding squared distance is the first algebraic step of that coordinate reduction. In the broader RS stack this sits in the mathematical substrate for sparse distance shells, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.