hopf_pannwitz_strict_lens_coord
plain-language theorem explainer
Two points in the closed vesica piscis of radius Δ, both strictly above the baseline, have squared Euclidean distance strictly less than Δ². Discrete-geometry and RS shell-multiplicity arguments cite this as the coordinate core of the four-point Hopf–Pannwitz lemma. The proof is a short nlinarith Positivstellensatz certificate fed by positivity of the two orientation determinants and the four disk inequalities.
Claim. Let $\Delta>0$. If $(c_x,c_y)$ and $(d_x,d_y)$ both lie in the closed lens $D((0,0),\Delta)\cap D((\Delta,0),\Delta)$ and $c_y>0$, $d_y>0$, then $(c_x-d_x)^2+(c_y-d_y)^2<\Delta^2$.
background
The module physicalizes Erdős problem #132: a distance value is a shell in the pairwise Euclidean spectrum, read in RS as a two-body recognition-energy shell whose multiplicity is the shell occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances ordered multiplicity is twice the unordered count, so classical thresholds double.
The geometric object here is the vesica piscis (lens) formed by two closed disks of radius $\Delta$ centered at $(0,0)$ and $(\Delta,0)$. A point $(x,y)$ is in the closed lens when $x^2+y^2\le\Delta^2$ and $(x-\Delta)^2+y^2\le\Delta^2$. The theorem treats the open upper half-lens $y>0$.
Classically this is the coordinate form of the Hopf–Pannwitz diameter fact for the lens: the diameter of the vesica is $\Delta$, attained only on the baseline endpoints, with strict inequality off the axis. Downstream, placing two diameter segments in coordinates reduces proper same-side configurations to this inequality via Lagrange’s identity relating squared distances to lens coordinates $(\alpha,\beta)$.
proof idea
Tactic proof by nlinarith with an explicit polynomial certificate. First derive $c_x>0$, $d_x>0$, $c_x<\Delta$, and $d_x<\Delta$ from the disk inequalities and $c_y,d_y>0$ (each a one-line nlinarith). Then feed nlinarith the four disk inequalities, the sign hypotheses, those four bounds, and nonnegativity of two squared orientation-type forms
$\bigl(c_y(\Delta-d_x)-d_y(\Delta-c_x)\bigr)^2$ and $(c_y d_x-d_y c_x)^2$,
plus several strict product positivities (mul_pos of $\Delta$, half-lens heights, and complementary baseline gaps). The solver closes the strict squared-distance bound; no external named lemmas beyond arithmetic positivity are required.
why it matters
This is the central classical input for the four-point Hopf–Pannwitz lemma in the proper-separation case inside Distance Shell Multiplicity. It discharges the positive-$\Delta$ orientation-sign core of ProperSeparatedDiameterContradiction, which states that two diameter segments cannot have both endpoints of the second segment strictly on the same side of the first while keeping all cross-distances $\le\Delta$.
Direct consumers: the lower-half reflection hopf_pannwitz_strict_lens_coord_neg; the theorem properSeparatedDiameterContradiction (and its Prop bridge ProperSeparatedDiameterContradiction); and the sharper sameSideDiameterContradiction, which needs only the single orientation-product condition. Together these block same-side diameter pairs and feed the sparse-shell / ordered-multiplicity analysis of Erdős #132 in RS units. No T0–T8 forcing step is invoked here; the result is pure plane geometry supporting the shell-occupancy bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.