w45
plain-language theorem explainer
The raw flat-angle Jacobian coefficient at tetrahedron edge-slot pair (4,5) is exactly zero. Anyone expanding the six-type stencil contraction into free displacement-class coefficients cites this entry. The proof is a one-line rewrite to the literal rational stencil table, then kernel numeric evaluation.
Claim. The single-entry radical coefficient $J_{45}/(2\sqrt{a^*_4})$ of the flat-angle Jacobian at edge-slot indices $4$ and $5$ equals $0$ in $\mathbb{R}$.
background
Module context is 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 residual at the reported TT witness does not vanish; the hinge term cancels it under the relative-minus assembly convention.
rawJacobianCoefficient f g is the single-entry radical form flatAngleJacobian f g / (2 sqrt(freudenthalTetSqEdges f)). It is not a fiber sum. The full 36-entry literal rational table rationalStencilWeight is phase-independent and defined by bare match, never through the radical form. Upstream rawJacobianCoefficient_eval equates every raw coefficient to the corresponding table entry cast to real.
proof idea
One-line wrapper. Rewrite the goal by rawJacobianCoefficient_eval 4 5, which replaces the radical coefficient with the rational table entry at bucket (4,5). Then norm_num on ReggeTTBucketAggregation.rationalStencilWeight evaluates that literal match to 0 in ℝ.
why it matters
Feeds zeroMode_free_coefficients, the algebraic identity that the six-tetrahedron raw-table contraction in seven free coefficients is the perfect square (c0+c1+c2-c3-c4-c5+c6)^2/2. That identity is the exact shape of the assembled constant block: it vanishes on the alternating-sum hyperplane where geometric edge-class coefficient vectors live, and nowhere else off that surface.
Closing this single table entry is mechanical bookkeeping inside the zero-mode headline chain (assembledConstantBlock_eq_zero and the hinge-cancellation witness split). It does not itself touch T0–T8 or the RCL; it is gravity-side stencil arithmetic supporting the TT zero mode.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.