w00
plain-language theorem explainer
The (0,0) entry of the raw per-slot Jacobian coefficient table is exactly zero as a real. Downstream zero-mode algebra cites this as one of the 36 literal table facts when contracting free edge-class coefficients. Proof is a one-line rewrite through the closed-form evaluation lemma, then rational arithmetic on the stencil weight table.
Claim. The raw Jacobian coefficient at tetrahedron slot pair $(0,0)$ equals $0$ in $\mathbb{R}$. Equivalently, after reducing by the flat-angle Jacobian over twice the square-root edge factor, that entry matches the literal rational stencil weight $0$.
background
Module setting is Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1): the hinge-aware assembled constant block of the Regge TT symbol, and whether it vanishes at $k=0$ on TT polarizations. The sympy diagnostic showed the stencil-only constant residual is nonzero at the reported TT witness, while the assembled block (hinge minus that residual) cancels; this file pins that cancellation in the kernel.
The raw Jacobian coefficient at a pair of face slots $(f,g)$ is the flat-angle Jacobian entry divided by twice the square root of the Freudenthal squared edge length on slot $f$. Independently, rationalStencilWeight is a bare 36-entry rational match table (phase-independent, not defined via any fiber sum). The evaluation theorem states every raw coefficient equals the corresponding table entry cast to $\mathbb{R}$.
Section 3 of the module isolates each of the 36 evaluations as a private rewrite lemma so that each norm_num stays small enough for the local build memory guard.
proof idea
One-line wrapper. Rewrite the goal by the universal evaluation theorem at $(0,0)$, which replaces the radical form by the rational stencil weight of bucket $\langle 0,0\rangle$ cast to $\mathbb{R}$. Then norm_num on that table definition discharges $0=0$.
why it matters
This is one cell of the literal $6\times 6$ coefficient table that the free-coefficient contraction expands. The parent theorem zeroMode_free_coefficients sums rawJacobianCoefficient f g * c(slotDispClass t f) * c(slotDispClass t g) over six tetrahedron types and all slot pairs, and obtains 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 on the alternating-sum hyperplane where geometric edge-class coefficient vectors live, and not for free $c$.
In the broader Gate C-A3 story, the assembled $O(1)$ block (hinge minus stencil residual) is the zero-mode headline once reduced at $k=0$. Pinning every table entry, including this zero diagonal, keeps the contraction fully kernel-checked rather than trusted from offline CAS output. Framework role is discrete gravity / Regge calculus on the TT sector, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.