status_signed_deficit_kernel_checked
plain-language theorem explainer
Asserts that the FourTetSignedDeficit module status records the signed-deficit kernel as checked. Anyone auditing the Regge four-tet star pipeline cites this as the boolean gate that the kernel-checked deficit construction is marked complete. Proof is reflexivity against the status record literal.
Claim. The module status flag for kernel-checked signed deficit equals $\mathrm{true}$.
background
The ambient module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tets share an interior hinge AB in a closed 4-cycle link, given as squared-edge data $(l,m,m,m,m,p)$ certified nondegenerate by Cayley-Menger ($\mathrm{cm}_3>0$). It is not a full Triangulation3D embedding.
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 one-parameter family $p(h)=(3/2)(1-h)$ forces $q=h$, so the deficit is $2\pi-4\arccos(h)=4\arcsin(h)$; the sign of the deficit is therefore the sign of the rational $h$, with no arccos evaluation in the kernel.
The module status record packages four booleans: signed-deficit kernel checked, weak-field pair constructed, no-ledger firewall, and N=5 torus extension closed. This declaration exposes only the first flag.
proof idea
One-line reflexivity. The status definition sets signed_deficit_kernel_checked := true by construction; the theorem is rfl against that field projection. No geometric lemmas are invoked.
why it matters
Serves as the audit gate that the first kernel-checked signed Regge deficit on an abstract four-tet star is marked complete in-repo. The underlying geometry (dihedral cosine via Cayley-Menger cofactors, deficit sign from rational $h$, weak-field mesh bounds) is the content that this flag advertises. Downstream consumers of module status can branch on this boolean without reopening the geometric development. No used-by edges are recorded; the flag is a status surface, not a lemma in a forcing chain. It does not itself touch T0-T8, RCL, or the phi-ladder; it sits in the discrete-geometry layer that later gravity and continuum-limit work (e.g. discrete Lichnerowicz status) may consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.