w50
plain-language theorem explainer
The raw Jacobian coefficient at Freudenthal edge indices (5,0) equals the rational 1/4. Anyone assembling the constant-block stencil contraction for the hinge-aware TT zero mode cites this entry. Proof is a one-line rewrite through the full 36-entry evaluation lemma, then numeric normalization of the literal rational stencil table.
Claim. The radical-normalized flat-angle Jacobian coefficient at edge indices $f=5$, $g=0$ equals $1/4$ as a real: $J_{5,0}/(2\sqrt{a^*_5})=1/4$.
background
Module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1): the hinge-aware assembled constant block of the Regge TT symbol must vanish at the reported TT witness. The assembled O(1) block is built from per-tet raw Jacobian entries contracted against edge-class polarization coefficients, then combined with a hinge diagonal term under a fixed relative-minus convention.
Each raw entry is flatAngleJacobian f g divided by twice the square root of the Freudenthal squared edge length at $f$. Independently, a literal rational table rationalStencilWeight records the radical-free normal form of every $(f,g)$ pair; it is phase-independent and never defined through a fiber sum. The upstream theorem rawJacobianCoefficient_eval asserts that every one of the 36 raw coefficients equals the corresponding table entry cast to $\mathbb{R}$.
Only the row-0 smoke bucket was proved against actual Jacobian data in the earlier audit interface; the full table and its entrywise evaluation live in the bucket-aggregation module that this file imports.
proof idea
One-line wrapper. Rewrite the goal by rawJacobianCoefficient_eval 5 0, which replaces the raw coefficient with the rational stencil weight of bucket $\langle 5,0\rangle$ cast to $\mathbb{R}$. Then norm_num against ReggeTTBucketAggregation.rationalStencilWeight discharges the arithmetic identity that the table entry is $1/4$.
why it matters
Feeds zeroMode_free_coefficients, the algebraic identity that contracts the full 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 square vanishes exactly on the alternating-sum hyperplane inhabited by geometric edge-class coefficient vectors, which is the algebraic content of the assembled constant-block zero mode.
In the module narrative this is one of the concrete table entries needed before the free-coefficient contraction can be expanded by simp over Fin.sum_univ_six. It sits inside the proved (not scaffolding) half of Gate C-A3: once the free contraction is a square and the TT witness lies on the kernel hyperplane, the assembled $k=0$ block is zero, matching the sympy diagnostic that recorded Hhat(0) quadratic = 0 after hinge cancellation of the stencil-only residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.