w25
plain-language theorem explainer
The raw single-entry Jacobian coefficient at edge-pair indices (2,5) is exactly zero. Anyone expanding the free-coefficient contraction of the assembled constant block cites this entry. The proof is a one-line rewrite through the evaluated rational stencil table, then numeric normalization.
Claim. The raw Jacobian coefficient at slot pair $(2,5)$ vanishes: $J_{2,5}/(2\sqrt{a^*_2})=0$ in $\mathbb{R}$, where $J_{fg}$ is the flat-angle Jacobian and $a^*_f$ is the squared Freudenthal edge length.
background
Module setting 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 relative-minus assembly convention.
rawJacobianCoefficient f g is the single-entry radical coefficient $J_{fg}/(2\sqrt{a^*_f})$, used by early bucket checks and by the free-coefficient contraction. Upstream, rawJacobianCoefficient_eval identifies every such entry with the corresponding literal rational from the independent 36-entry rationalStencilWeight table (phase-independent match, never defined through a fiber sum). That table is kernel-verified entrywise against the closed forms of the flat-angle Jacobian and Freudenthal edge lengths.
proof idea
One-line wrapper. Rewrite by rawJacobianCoefficient_eval 2 5, which replaces the radical form by the rational stencil weight of bucket $\langle 2,5\rangle$ cast to $\mathbb{R}$. Then norm_num on ReggeTTBucketAggregation.rationalStencilWeight evaluates that table entry to $0$.
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_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$. That identity is the exact shape of the assembled constant block: it does not vanish for free coefficients, and vanishes exactly on the alternating-sum hyperplane where geometric edge-class coefficient vectors live.
Together with the sibling entry lemmas, this closes the coefficient table needed for the zero-mode headline (assembledConstantBlock_eq_zero) in the hinge-aware Gate C-A3 chain. Landmark context is the Regge TT Bloch/stencil analysis supporting the Recognition gravity side of the QG campaign, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.