is
plain-language theorem explainer
Records that the four-tet signed Regge-deficit construction sits on a different primitive from LedgerBridgeNoGo, hence is RS-independent of that no-go. Geometers working the abstract hinge-star family would cite it when separating local deficit sign from ledger-bridge constraints. The content is the CoupledAxis independence predicate (distinct primitives), with no separate proof body exposed here.
Claim. The four-tetrahedron hinge-star signed-deficit development is consistent with, but independent of, the LedgerBridgeNoGo result: the two rest on distinct Recognition-Science primitives in the coupled-axis sense ($A.\mathrm{primitive}\neq B.\mathrm{primitive}$).
background
The ambient module builds the first kernel-checked signed Regge-convention deficit angles on an abstract four-tet star: four congruent tetrahedra around a common hinge AB, given as squared-edge data $(l,m,m,m,m,p)$ and certified nondegenerate by Cayley-Menger ($\mathrm{cm}_3>0$). It is not a Triangulation3D instance; no coordinate embedding of the closed 4-cycle link is formalized.
On the slice $l=m=1$, the common dihedral cosine is $q(p)=(3-2p)/3$, flat at $p_0=3/2$. The deformation $p(h)=(3/2)(1-h)$ yields $q=h$ and deficit $2\pi-4\arccos(h)=4\arcsin(h)$, so the sign of the deficit is the sign of the rational $h$ with no arccos numerics.
Upstream, RS-independence means two coupled axes are carried by different primitives. That is the only named dependency: the lemma invokes that predicate rather than a geometric identity.
proof idea
No tactic or term proof body is attached in the extracted declaration (zero body lines). The sole dependency is the Foundation definition of independence on coupled axes: two axes are independent when their primitives differ. The lemma is therefore a classification or interface fact wiring the four-tet deficit development to that predicate relative to LedgerBridgeNoGo, not a Cayley-Menger or dihedral computation.
why it matters
Inside the Geometry tier for signed Regge deficits, this separates the abstract four-tet hinge-star sign theorem from ledger-bridge no-go constraints. Downstream uses are empty in the graph, so it currently documents a non-coupling rather than feeding a parent existence or curvature theorem.
Framework role is organizational: the module's kernel-checked deficit sign (positive vs negative under the one-parameter family, weak-field mesh bounds) should not be read as contingent on LedgerBridgeNoGo. It does not itself advance T5-T8 forcing, RCL, or the phi-ladder mass formula; it only keeps the Regge-star geometry on its own primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.