status
plain-language theorem explainer
Module-level status certificate for signed Regge deficit angles on an abstract four-tetrahedron hinge star. It records four boolean completion flags: kernel-checked signed deficit, constructed weak-field pair, ledger-import firewall, and closed N=5 Freudenthal torus extension. Downstream certificate lanes and zero-parameter claims cite it as a contact gate. The body is a pure structure literal with no proof obligations.
Claim. The four-tet signed-deficit module status is the record with signed-deficit kernel checked $=\mathrm{true}$, weak-field pair constructed $=\mathrm{true}$, no-ledger-import firewall $=\mathrm{true}$, and $N=5$ torus extension open $=\mathrm{false}$ (i.e. the extension is closed).
background
The ambient module builds the first kernel-checked signed Regge-convention deficit angles on an abstract four-tet star: squared-edge data for four congruent tetrahedra around a common hinge AB, certified nondegenerate by Cayley–Menger sign $\mathrm{cm}_3>0$. Configuration is panel-locked: squared edges $(l,m,m,m,m,p)$ with hinge edge $0$; common dihedral cosine $q$ from the cofactor formula. On the slice $l=m=1$ one has $q(p)=(3-2p)/3$, flat value $p_0=3/2$, and deformation $p(h)=(3/2)(1-h)$ giving deficit $4\arcsin(h)$ so the sign of the deficit equals the sign of the rational $q=h$.
FourTetSignedDeficitStatus is the four-field Bool record for this certificate lane. Sibling geometry (star minors, cofactors, nondegeneracy) supplies the kernel content those flags summarize. Parallel status defs elsewhere (RS-native units, discrete Lichnerowicz) follow the same pattern: scoped claim flags, not geometric theorems.
proof idea
Definitional structure literal, not a tactic or term proof. Each field of FourTetSignedDeficitStatus is assigned a Boolean constant: three completion flags true, and n5_torus_extension_open := false. The doc-comment states the N=5 periodic Freudenthal torus extension is closed by the Analysis lift equating the N=5 face-diagonal hinge deficit to the face-diagonal star deficit; the field name is retained while the value is flipped to closed. No lemmas are applied.
why it matters
This status is the contact certificate for the THEOREM-tier four-tet signed-deficit lane: first kernel-checked signed Regge deficits with explicit weak-field mesh bounds and sign control without arccos or interval arithmetic. It is heavily referenced (dozens of use sites) by astrophysics observability certificates, chemistry bond predicates, RS-native unit and $\lambda_{\mathrm{rec}}$ derivations, baryon asymmetry and inflation falsifiers, and other module gates that require geometry firewall and kernel-checked deficit infrastructure.
In the Recognition framework it anchors discrete curvature (Regge hinge deficits) that feed continuum limits and gravity contact, complementary to T8 ($D=3$) and discrete operator work. Closing the N=5 torus extension removes a former open flag and tightens the path from abstract star deficits toward periodic Freudenthal meshes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.