w12
plain-language theorem explainer
The raw Jacobian coefficient at edge-slot pair (1,2) equals the exact rational −1/8. Anyone assembling the Schläfli-reduced constant block or the free-coefficient zero-mode identity cites this entry. The proof is a one-line rewrite through the full 36-entry evaluation lemma, followed by rational arithmetic on the literal stencil table.
Claim. The single-entry radical coefficient of the flat-angle Jacobian at Freudenthal tetrahedron edge indices $f=1$, $g=2$, normalized by twice the square root of the squared edge length, equals $-1/8$ in $\mathbb{R}$.
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 analysis. The assembled constant block of the per-tet Hessian is built from raw Jacobian coefficients: each entry is the flat-angle Jacobian divided by twice the square root of the corresponding Freudenthal squared edge length.
Upstream, rawJacobianCoefficient_eval proves that every one of the 36 slot pairs evaluates to an exact rational drawn from an independent literal table rationalStencilWeight. That table is phase-independent and never defined through a fiber sum; the (1,2) cell is recorded as $-(1/8)$. The present lemma simply names that cell.
These rationals feed the free-coefficient contraction that becomes the perfect-square identity for the assembled $k=0$ block, and they also appear in the hinge/edge-diagonal assembly that cancels the stencil-only residual at the TT witness.
proof idea
One-line wrapper. Rewrite by the universal evaluation theorem rawJacobianCoefficient_eval at arguments $1$ and $2$, which replaces the radical form by the cast of rationalStencilWeight on the bucket $\langle 1,2\rangle$. Then norm_num discharges the match clause of the full literal rational table, yielding $-1/8$ in $\mathbb{R}$.
why it matters
Named coefficient lemmas such as this one are the atomic inputs to zeroMode_free_coefficients, which shows that the six-tetrahedron raw-table contraction equals $(c_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$ and therefore vanishes exactly on the alternating-sum hyperplane occupied by geometric edge-class vectors. That identity is the algebraic spine of the assembled-constant zero mode (Gate C-A3 headline).
The same rationals are consumed by the 4D star-kernel homothety stationarity theorems (fullStar_homothety_stationary in the 1-2 and 2-2 hinge kernels), which need every stencil weight explicit. In the broader Recognition gravity stack this is bookkeeping inside the Regge TT Bloch interface, not a forcing-chain landmark, but without the exact $-1/8$ the free-coefficient square and the hinge-cancellation witness split cannot close in the kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.