w04
plain-language theorem explainer
The raw flat-angle Jacobian coefficient at Freudenthal edge indices (0,4) equals exactly -1/8. Anyone expanding the six-tet constant-block contraction over free edge-class coefficients cites this entry. The proof is a one-line rewrite through the full 36-entry rational evaluation table, then kernel rational arithmetic.
Claim. The single-entry radical coefficient $J_{04}/(2\sqrt{a^*_0})$ of the flat-angle Jacobian at Freudenthal edge indices $0$ and $4$ 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 the assembled Regge TT constant block. The stencil-only 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 the TT surface.
The raw coefficient is the flat-angle Jacobian entry divided by twice the square root of the squared Freudenthal edge length. Independently, a literal rational table records every one of the 36 slot-pair weights as bare rationals (phase-independent, never defined via a fiber sum). Upstream, the evaluation theorem identifies each raw coefficient with the corresponding table entry cast to reals; the $(0,4)$ cell of that table is exactly $-1/8$.
proof idea
One-line wrapper. Rewrite by the universal evaluation theorem that equates every raw coefficient to its rational-table entry, specializing to indices $(0,4)$. Then norm_num on the full literal rational stencil table discharges the equality $-1/8 = -1/8$ in $\mathbb{R}$.
why it matters
Feeds the free-coefficient identity for the six-tet raw-table contraction: that sum equals $(c_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$, which vanishes exactly on the alternating-sum hyperplane inhabited by geometric edge-class vectors. The $(0,4)$ weight is one of the thirty-six concrete rationals that make the perfect-square algebra close. Downstream this underwrites the assembled-constant-block zero mode (Gate C-A3 headline) once the hinge cancels the recorded stencil-only residual. It is bookkeeping inside the Regge TT analysis, not a forcing-chain landmark, but without the entrywise rationals the free-coefficient square cannot be stated in the kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.