w05
plain-language theorem explainer
The raw Jacobian coefficient at edge-pair slots (0,5) equals the rational 1/4. Gravity analysts cite it when expanding the six-by-six stencil table that feeds the assembled constant block. The proof is a one-line rewrite through the full evaluation lemma, then kernel arithmetic on the literal rational table.
Claim. The single-entry radical coefficient of the flat-angle Jacobian at tetrahedron edge indices $f=0$, $g=5$, normalized by twice the square root of the Freudenthal squared edge length at $f$, equals $1/4$ 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 the Regge TT symbol. The assembled constant block combines a hinge contribution with a stencil-only residual; the stencil side is built from raw Jacobian coefficients on the six edge slots of a Freudenthal tetrahedron.
The coefficient rawJacobianCoefficient f g is the flat-angle Jacobian entry divided by $2\sqrt{a^*_f}$. Independently, rationalStencilWeight is a bare match table of rationals for all 36 slot pairs, never defined through a fiber sum. The evaluation theorem states that every raw coefficient equals the corresponding table entry cast to $\mathbb{R}$; the $(0,5)$ cell of that table is the literal $1/4$.
Only the radical-trivial smoke entries are needed pointwise here; the full table is already kernel-verified entry by entry upstream.
proof idea
One-line wrapper. Rewrite the goal by the universal evaluation lemma rawJacobianCoefficient_eval at arguments $(0,5)$, which replaces the radical form by the rational table entry cast to $\mathbb{R}$. Then norm_num on rationalStencilWeight discharges the match arm $|,0,5,\Rightarrow 1/4$.
why it matters
Feeds zeroMode_free_coefficients, which contracts the full six-by-six raw table over six tetrahedron types in seven free edge-class 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 algebraic shape of the assembled constant block: it vanishes exactly on the alternating-sum hyperplane occupied by geometric edge-class vectors, and is the algebraic engine behind the zero-mode headline that the Schlaefli-reduced assembled block is zero at the TT witness.
In the Gate C-A3 story, the stencil residual and hinge term cancel under the pinned relative-minus assembly convention. Pinning individual table entries such as $(0,5)=1/4$ keeps the free-coefficient expansion fully explicit and referee-checkable, with no silent dependence on offline numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.