w30
plain-language theorem explainer
The raw single-entry Jacobian coefficient at tetrahedron edge-pair indices (3,0) is exactly zero as a real. Gravity analysts cite it when expanding the six-type stencil contraction that becomes the assembled constant block. The proof is a one-line wrapper: evaluate via the full rational table, then close by numeric normalization.
Claim. The raw Jacobian coefficient at edge indices $f=3$, $g=0$ equals $0$ in $\mathbb{R}$. Equivalently, after radical-free normalization against the Freudenthal squared edge lengths, that entry of the flat-angle Jacobian table is the rational $0$.
background
Module context is Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1, Lane C): hinge-aware zero mode for the Regge TT assembled constant block. The stencil-only constant residual at the reported TT witness does not vanish; the hinge term cancels it under the pinned assembly convention assembled = hinge − Σ_Gcc.
rawJacobianCoefficient f g is the single-entry radical coefficient J_fg / (2 √a*_f) used in early bucket checks. The full independent rational table rationalStencilWeight lists all 36 slot pairs as bare rationals (phase-independent, not defined through any fiber sum). Upstream rawJacobianCoefficient_eval asserts every raw entry equals the corresponding table rational cast to ℝ.
Indices run over Fin 6 edge slots of the Freudenthal tetrahedron. Entry (3,0) is one of the many zeros in that table; the free-coefficient identity later contracts all thirty-six against seven displacement-class coordinates.
proof idea
One-line wrapper. Rewrite the goal by rawJacobianCoefficient_eval 3 0, which replaces the radical form by the rational table entry at bucket ⟨3,0,…⟩ cast to ℝ. Then norm_num on ReggeTTBucketAggregation.rationalStencilWeight evaluates that match arm to 0 and closes.
why it matters
Feeds zeroMode_free_coefficients, the algebraic identity that the six-tetrahedron raw-table contraction in seven free coefficients is the perfect square (c₀+c₁+c₂−c₃−c₄−c₅+c₆)²/2. That identity is the exact shape of the assembled constant block: it vanishes precisely on the alternating-sum hyperplane inhabited by geometric edge-class coefficient vectors, which is the zero-mode headline of this module.
In the finishing charter this is scaffolding for Gate C-A3 (hinge-aware zero mode), not a T0–T8 forcing step. It is pure table arithmetic inside the Regge TT Bloch/stencil pipeline that ultimately supports assembledConstantBlock_eq_zero at the TT witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.