hopf_pannwitz_strict_lens_coord_neg
plain-language theorem explainer
In the closed vesica piscis of two disks of radius Δ centered at (0,0) and (Δ,0), any two points with strictly negative y-coordinates have squared Euclidean separation strictly less than Δ². This is the lower-half twin of the Hopf–Pannwitz strict lens inequality. Diameter-contradiction arguments for Erdős #132 cite it when both points lie below the diameter segment. The proof reflects y ↦ −y and invokes the upper-half coordinate form.
Claim. Let $\Delta>0$. Suppose $(c_x,c_y)$ and $(d_x,d_y)$ both lie in the closed lens $D((0,0),\Delta)\cap D((\Delta,0),\Delta)$, i.e. $c_x^2+c_y^2\le\Delta^2$, $(c_x-\Delta)^2+c_y^2\le\Delta^2$ and likewise for $(d_x,d_y)$, and suppose $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: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count (threshold $\le n$ becomes $\le 2n$).
The geometric engine is the vesica piscis (lens) $D((0,0),\Delta)\cap D((\Delta,0),\Delta)$. Hopf–Pannwitz asserts that this lens has diameter $\Delta$, with strict inequality off the two centers. The sibling theorem hopf_pannwitz_strict_lens_coord states the strict bound when both points have positive $y$-coordinate (open upper half-lens).
The present result is the matching lower-half statement. Downstream diameter contradictions place a diameter segment on the $x$-axis and reduce same-side pairs to lens coordinates via rotation and Lagrange's identity $\alpha^2+\beta^2=\mathrm{dist}^2$; orientation signs then select the upper or lower half.
proof idea
Reflect both $y$-coordinates: set $c_y'=-c_y$ and $d_y'=-d_y$. From $c_y<0$ and $d_y<0$ one gets $c_y'>0$ and $d_y'>0$. Squaring is even, so the four disk inequalities for $(c_x,c_y')$ and $(d_x,d_y')$ follow from the originals by nlinarith. Apply the upper-half theorem hopf_pannwitz_strict_lens_coord to $(\Delta,c_x,c_y',d_x,d_y')$, obtaining $(c_x-d_x)^2+(c_y'-d_y')^2<\Delta^2$. Since $(c_y'-d_y')^2=(c_y-d_y)^2$, a final nlinarith closes the claim. Pure reflection reduction; no new geometric content.
why it matters
Feeds the two diameter-contradiction engines of the module: properSeparatedDiameterContradiction (properly separated diameter segments cannot place both endpoints of the second segment on the same strict side of the first) and the sharper sameSideDiameterContradiction (same-side orientation product alone already contradicts the diameter bounds).
Those contradictions are the geometric spine of the RS treatment of Erdős #132: sparse shells and diameter uniqueness force multiplicity bounds on recognition-energy distance shells. Without the lower-half lens inequality, orientation signs $\beta<0$ would leave a gap in the case split. The result is pure Euclidean plane geometry; it does not itself invoke $\varphi$, the eight-tick octave, or the forcing chain T0–T8, but it underwrites the combinatorial shell-occupancy claims that the module exports upward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.