w03
plain-language theorem explainer
The raw single-entry Jacobian coefficient at edge-pair indices (0,3) is exactly zero as a real. Anyone expanding the six-type stencil contraction for the assembled constant block cites this entry. The proof is a one-line wrapper: rewrite by the full rational evaluation lemma, then close by numeric reduction on the literal stencil table.
Claim. The raw Jacobian coefficient at slot pair $(0,3)$ equals $0$ in $\mathbb{R}$: if $J_{fg}$ denotes the flat-angle Jacobian entry and $a^*_f$ the Freudenthal squared edge length, then $J_{0,3}/(2\sqrt{a^*_0})=0$.
background
This module sits in the QG full-theory campaign (Paper C / Pillar 1, Lane C) and closes the hinge-aware zero-mode gate for Regge TT. The assembled constant block combines a hinge contribution with the stencil-only Hessian contraction; the stencil side is built from raw single-entry radical coefficients
$$\mathrm{raw}(f,g)=J_{fg}/(2\sqrt{a^*_f}),$$
one for each ordered pair of the six tetrahedron edge slots.
Upstream, rawJacobianCoefficient_eval identifies every such entry with a phase-independent literal rational table rationalStencilWeight on the 36 bucket pairs. That table is not a fiber sum: it is a bare match of rationals, offline-derived from the closed forms of the flat-angle Jacobian and Freudenthal lengths, then kernel-checked entrywise. For the pair $(0,3)$ the table records the rational $0$.
proof idea
One-line wrapper. Rewrite the goal by rawJacobianCoefficient_eval 0 3, which replaces the radical coefficient by the real cast of rationalStencilWeight on bucket $\langle 0,3\rangle$. Then norm_num on that table entry discharges $0=0$.
why it matters
Feeds zeroMode_free_coefficients, the algebraic identity that the six-type raw-table contraction in seven free edge-class 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 vanishes precisely on the alternating-sum hyperplane inhabited by geometric edge-class vectors, which is the zero-mode content of Gate C-A3.
Each concrete table entry such as this $(0,3)$ zero is a necessary brick in the simp/Fin.sum expansion of that contraction. The module doc ties the broader story to the sympy diagnostic residual and the hinge-minus-stencil assembly convention; this lemma is purely the stencil-table side of that ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.