w40
plain-language theorem explainer
The raw flat-angle Jacobian coefficient at edge indices (4,0) equals exactly -1/8 as a real. Anyone expanding the six-tet assembled constant-block contraction into free edge-class coefficients cites this entry. The proof is a one-line rewrite through the full 36-entry rational evaluation table, finished by norm_num on the literal stencil weight.
Claim. The single-entry radical coefficient $J_{40}/(2\sqrt{a^*_4})$ of the flat-angle Jacobian equals $-1/8$ in $\mathbb{R}$.
background
This module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1): the hinge-aware zero mode of the assembled Regge TT 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, so the assembled $k=0$ block is zero on TT.
rawJacobianCoefficient f g is the radical-normalized single entry flatAngleJacobian f g / (2 sqrt(freudenthalTetSqEdges f)). Independently, rationalStencilWeight is the full 36-slot literal rational table (phase-independent, never defined through a fiber sum). Upstream rawJacobianCoefficient_eval asserts every raw coefficient equals the corresponding table entry cast to $\mathbb{R}$; the table records the $(4,0)$ slot as $-1/8$.
proof idea
One-line wrapper. Rewrite the goal by rawJacobianCoefficient_eval 4 0, which replaces the radical form by the rational stencil weight at bucket $\langle 4,0\rangle$ cast to $\mathbb{R}$. Then norm_num on ReggeTTBucketAggregation.rationalStencilWeight discharges the literal match clause to $-1/8$.
why it matters
Feeds zeroMode_free_coefficients, which contracts the raw table over the six tetrahedron types in seven free coefficients 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 does not vanish for free coefficients, and vanishes exactly on the alternating-sum hyperplane where every geometric edge-class coefficient vector lives.
In the Gate C-A3 chain this entry is one of the 36 rational bricks needed before the free-coefficient expansion can be simplified by simp on slotDispClass. It sits under the zero-mode headline assembledConstantBlock_eq_zero and the witness-tie that pins assembled = hinge - stencilOnlyConstantWitnessResidual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.