status_weak_field_pair_constructed
plain-language theorem explainer
The module status bit recording that a weak-field pair of signed four-tet hinge deficits has been constructed is true. Geometry and discrete-gravity auditors cite it when checking that the signed-deficit construction is marked complete in the claim ledger. The proof is reflexivity on the status record field.
Claim. In the four-tetrahedron signed-deficit status record, the Boolean flag asserting that a weak-field pair of hinge configurations (strictly positive deficit for one deformation sign and strictly negative for the other, with explicit mesh bounds) has been constructed equals $\mathrm{true}$.
background
The ambient module builds signed Regge-convention deficit angles on an abstract four-tetrahedron hinge star: four congruent tetrahedra around a common hinge edge, given as squared-edge data and certified nondegenerate by the Cayley-Menger sign $\mathrm{cm}_3>0$. It is not a full Triangulation3D embedding; only the star-local edge lengths matter.
On the panel-locked slice with hinge and legs squared-length $1$, the common dihedral cosine is $q(p)=(3-2p)/3$. The flat closing value is $p_0=3/2$ ($q=0$). The one-parameter family $p(h)=(3/2)(1-h)$ forces $q=h$, so the star deficit is $2\pi-4\arccos(h)=4\arcsin(h)$. Sign of the deficit is therefore the sign of the rational $h$, with no interval arithmetic.
The module status record packages four Boolean claims: kernel-checked signed deficit, weak-field pair constructed, no ledger imports, and N=5 torus extension closed. This declaration exposes the second flag.
proof idea
One-line reflexivity. The status definition hard-codes weak_field_pair_constructed := true, so projecting that field and comparing to true reduces by rfl. No geometric lemmas are invoked at this site; the geometric work lives in the sibling constructions that justified setting the flag.
why it matters
This is a claim-ledger witness, not a geometric theorem. It records that the module's headline construction (an explicit weak-field pair of four-tet stars with opposite-sign Regge deficits and mesh bounds) is marked complete. Downstream discrete-gravity and continuum-limit work that depends on signed hinge curvature can treat the weak-field sign-reversal sample as available without re-auditing the status record.
In the Recognition geometry stack this sits under discrete curvature bookkeeping that feeds continuum limits (cf. discrete Lichnerowicz status on flat TT modes). It does not itself touch T0-T8, the RCL, or the phi-ladder; it only certifies that the signed four-tet deficit sample used as geometric input is flagged constructed. No used_by edges are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.