w31
plain-language theorem explainer
The radical-normalized flat-angle Jacobian entry at tetrahedron edge-slot pair (3,1) equals the exact rational -1/4. Anyone expanding the assembled O(1) constant block of the Regge TT symbol cites this table entry. The proof is a one-line rewrite through the 36-entry evaluation lemma, then kernel rational arithmetic on the literal stencil weight table.
Claim. For edge-slot indices $f=3$ and $g=1$ in the six-edge tetrahedron indexing, the raw Jacobian coefficient $\mathrm{flatAngleJacobian}(3,1)/(2\sqrt{a^*_3})$ equals $-1/4$ as a real number.
background
This module sits in the QG full-theory campaign (Paper C / Pillar 1, Lane C) and closes Gate C-A3: the hinge-aware zero mode of the assembled Regge TT constant block. The raw Jacobian coefficient is the single-entry radical form $\mathrm{flatAngleJacobian}(f,g)/(2\sqrt{a^*_f})$, not a fiber sum. Upstream, a full 36-entry literal rational table records the radical-free normal form of every such coefficient; that table is phase-independent and never defined through the coefficient itself.
The evaluation lemma states that every raw coefficient equals the corresponding rational table entry cast to $\mathbb{R}$. Only the row-0 smoke bucket was checked against live Jacobian data in an earlier audit; the full table is kernel-verified entry by entry against the closed forms of the flat-angle Jacobian and Freudenthal squared edge lengths. The present entry is one cell of that table, needed when the six-type contraction is expanded by hand.
proof idea
One-line wrapper. Rewrite the left-hand side by the universal evaluation lemma rawJacobianCoefficient_eval at arguments $(3,1)$, which replaces the radical form by the rational stencil weight of bucket $\langle 3,1\rangle$ cast to $\mathbb{R}$. Then norm_num on that literal match arm yields $-1/4$.
why it matters
Feeds the free-coefficient identity zeroMode_free_coefficients, which expands the six-tetrahedron raw-table contraction into the perfect square $(c_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$. That identity is the exact algebraic shape of the assembled constant block: it vanishes precisely on the alternating-sum hyperplane inhabited by geometric edge-class coefficient vectors, and is the algebraic engine behind the zero-mode headline of Gate C-A3.
In the broader campaign the stencil-only residual at the reported TT witness is nonzero; the hinge term cancels it under the pinned relative-minus assembly convention. Pinning every rational table cell (including this one) keeps the free-coefficient expansion free of silent numerical substitutions and closes the constant-block side of the hinge-aware zero mode.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.