FourTetSignedDeficitStatus
plain-language theorem explainer
A four-field Boolean status record for the signed-deficit contact certificate lane on an abstract four-tetrahedron hinge star. Geometry and Regge-calculus auditors cite it to read off which certificate steps are closed in-kernel versus still open. It is a plain structure definition; the companion value fills the flags from the module's proved results.
Claim. A status record consisting of four Boolean flags: whether the signed Regge deficit kernel has been checked; whether a weak-field opposite-sign pair has been constructed; whether the module firewall excludes ledger imports; and whether the $N=5$ periodic Freudenthal torus extension remains open.
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 the Cayley-Menger sign $\mathrm{cm}_3 > 0$. It is not an encoded triangulation and no coordinate embedding of the closed 4-cycle link is formalized here.
Each tet carries squared edges $(l,m,m,m,m,p)$ with hinge edge $0$. On the kernel-checked slice $l=m=1$ the common dihedral cosine is $q(p)=(3-2p)/3$. The flat value is $p_0=3/2$ ($q=0$, $\theta=\pi/2$). The deformation $p(h)=(3/2)(1-h)$ yields $q=h$ and deficit $4\arcsin(h)$, so the sign of the deficit is the sign of the rational $q=h$ with no arccos evaluation.
This structure is the typed checklist for that certificate lane. The companion status value sets the $N=5$ torus flag closed by the Analysis lift equating the $N=5$ face-diagonal hinge deficit to the face-diagonal star deficit.
proof idea
No proof body: a structure declaration with four Bool fields. Downstream code constructs an inhabitant by assigning concrete booleans from the module's theorems (kernel-checked signed deficit, weak-field pair, firewall, and the closed $N=5$ torus lift).
why it matters
Gives a single typed surface for the signed-deficit contact certificate lane so auditors can see which geometry steps are closed without reading the whole module. The only direct consumer is the module status value, which sets kernel-checked, weak-field pair, and firewall to true and flips the $N=5$ torus flag to closed via the Analysis lift equating the $N=5$ face-diagonal hinge deficit to the face-diagonal star deficit.
In the broader Recognition geometry stack this sits under signed Regge deficits on hinge stars (the discrete curvature that feeds continuum limits and gravity contact). It does not itself invoke the forcing chain T0–T8, RCL, or the $\phi$-ladder; it only certifies local geometric sign control needed before those layers consume deficit data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.