w53
plain-language theorem explainer
The raw single-entry Jacobian coefficient at edge indices (5,3) is exactly zero. Anyone expanding the six-type free-coefficient contraction of the assembled constant block cites this slot vanishing. Proof is a one-line rewrite to the literal rational stencil table, then kernel arithmetic.
Claim. The raw Jacobian coefficient at slot pair $(5,3)$, namely the flat-angle Jacobian entry divided by twice the square root of the Freudenthal squared edge length on the first index, equals $0$ in $\mathbb{R}$.
background
Module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1, Lane C): the hinge-aware zero mode of the assembled Regge TT constant block. The raw Jacobian coefficient is the single-entry radical form used before full fiber aggregation: flat-angle Jacobian over twice the square root of the Freudenthal squared edge length.
Upstream, every one of the 36 raw coefficients is identified with a phase-independent literal rational table entry (rawJacobianCoefficient_eval). That table is independent of any fiber sum; the $(5,3)$ entry is the rational $0$. The sibling audit module carries an earlier partial table used only for a row-0 smoke check; the aggregation module holds the full 36-entry table verified entrywise.
The free-coefficient contraction over six tetrahedron types is later rewritten as a perfect square in seven displacement-class coefficients. Individual vanishing slots such as this one are the elementary inputs to that algebraic reduction.
proof idea
One-line wrapper. Rewrite the left-hand side by rawJacobianCoefficient_eval at indices $5$ and $3$, which replaces the radical form by the corresponding entry of the full literal rational stencil table cast to $\mathbb{R}$. Then norm_num on that table entry discharges the equality to $0$.
why it matters
Feeds zeroMode_free_coefficients, the algebraic identity that the six-type raw-table contraction in seven free coefficients is exactly $(c_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$. That identity is the exact shape of the assembled constant block: it does not vanish off the constraint surface, and vanishes precisely on the alternating-sum hyperplane inhabited by geometric edge-class coefficient vectors.
In the module narrative this is one of the elementary table facts supporting the zero-mode headline (assembledConstantBlock_eq_zero) and the witness-tie that pins the relative-minus assembly convention between the hinge block and the stencil-only residual. It is pure linear-algebra bookkeeping inside Gate C-A3, not a forcing-chain step (T0–T8), but it is required scaffolding for the Regge TT constant-block cancellation that the sympy diagnostic predicted and the kernel now certifies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.