fourTet_weak_pair
plain-language theorem explainer
For every 0 < h < 1, the four-tet hinge star at deformations +h^2 and -h^2 is an antisymmetric signed-deficit pair: hinge cosines equal +/-h^2, deficits opposite in sign and equal in magnitude, meshes bounded by 3, both cm3 positive, and |deficit| <= 2*pi*h^2. Regge-geometry auditors cite it as the Test B weak-field certificate. Proof assembles prior star lemmas by refine.
Claim. For every real $h$ with $0 < h < 1$, the abstract four-tetrahedron hinge star at squared-edge deformations $+h^2$ and $-h^2$ (about the flat rim $p_0 = 3/2$) satisfies: the common hinge cosine equals $+h^2$ (resp. $-h^2$); the star deficit is strictly positive at $+h^2$ and strictly negative at $-h^2$; $\mathrm{deficit}(-h^2) = -\mathrm{deficit}(+h^2)$; every squared edge of both configurations is at most $3$; both Cayley-Menger determinants $\mathrm{cm}_3$ are positive; and $|\mathrm{deficit}(\pm h^2)| \le 2\pi h^2$.
background
The module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior edge AB in a closed 4-cycle link. Squared edges are locked to the panel $(l,m,m,m,m,p)$ with hinge AB as edge 0. On the kernel-checked slice $l=m=1$, the common dihedral cosine is the rational $q(p)=(3-2p)/3$, flat at $p_0=3/2$ where $q=0$ and each dihedral is $\pi/2$.
Deforming by parameters $\pm h^2$ about that flat value yields hinge cosines $q=\pm h^2$ on the nose, so the star deficit $2\pi-4\arccos(q)$ has sign controlled by the rational $q$ alone (no interval arithmetic). Nondegeneracy is the Cayley-Menger sign $\mathrm{cm}_3>0$ on the six squared edges; a coordinate embedding of the link is not formalized.
Upstream pieces used here include the explicit Cayley-Menger polynomial $\mathrm{cm}_3$, the cofactor cosine formula, the star configuration maps, the deficit-sign lemma, oddness of the deficit in the deformation, mesh bounds, and the absolute-value weak-field estimate.
proof idea
Tactic proof. First record elementary positivity facts: $0<h^2<1$ and $|\pm h^2|\le 1$ (in fact $<1$). Then refine a ten-conjunct goal and discharge each conjunct by a named star lemma:
- hinge cosines via the star cosine identity at $\pm h^2$;
- deficit signs via the four-tet deficit-sign lemma (positive branch at $+h^2$, negative at $-h^2$);
- exact antisymmetry via oddness of the star deficit;
- mesh bound $\le 3$ on all six edges of both configs via the star mesh bound;
- $\mathrm{cm}_3>0$ via the four-tet nondegeneracy lemma on both sides;
- magnitude bounds via the star deficit absolute-value estimate, rewriting absolutes with $h^2>0$.
No new analysis is performed; the certificate is pure assembly of prior star facts under $0<h<1$.
why it matters
This is the module's Test B certificate: the first kernel-checked weak-field pair of opposite-sign Regge deficits on an abstract four-tet star. It shows that signed curvature is not an artifact of orientation conventions or of a single side of the flat point; the family is odd in the deformation and bounded by $2\pi h^2$.
In the Recognition geometry lane it supplies the geometric half of the intended parity obstruction: ledger J-deficits are even in the deformation parameter (seven-gaps / LedgerBridgeNoGo campaign), while this star deficit family is odd. The module deliberately firewalls ledger imports, so the composition "no ledger J-deficit matches the signed star family" is left to the campaign level; the pure algebraic even-function no-go corollary sits immediately below in the same file.
No downstream Lean users are wired yet. Framework contact is geometric rather than T0-T8: it certifies that D=3 hinge stars can carry genuine signed deficit data before any ledger matching is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.