zeroMode_free_coefficients
plain-language theorem explainer
The six-tetrahedron raw Jacobian contraction in seven free edge-class coefficients equals the perfect square (c0+c1+c2-c3-c4-c5+c6)^2/2. Anyone tracking the hinge-aware Regge TT zero mode cites this for the algebraic shape of the assembled constant block. The proof expands the finite sums, substitutes the thirty-six tabulated weights, and finishes by ring.
Claim. For any real coefficients $c_0,\ldots,c_6$, the triple sum over the six tetrahedron types $t$ and face pairs $(f,g)$ of $\mathrm{rawJacobian}_{f g}\, c_{\mathrm{slot}(t,f)}\, c_{\mathrm{slot}(t,g)}$ equals $(c_0+c_1+c_2-c_3-c_4-c_5+c_6)^2/2$.
background
This module closes 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 constant block does not vanish under TT; a sympy diagnostic recorded residual $-\pi(\sqrt{2}+4)/8$ at the witness $E=\mathrm{diag}(1,-1,0)/\sqrt{2}$, $k=e_z$. The assembled object cancels once the hinge contribution is included with relative minus sign.
The seven free coefficients index geometric edge-displacement classes on the cubic lattice (three axis, three face-diagonal, one body-diagonal). The map slotDispClass assigns, for each tetrahedron type and each of six faces, which of those seven classes the face edge belongs to. The raw Jacobian table supplies the per-face-pair weights of the Schlaefli-reduced cell stencil at zero wave vector.
The identity is purely algebraic in free $c$: it does not yet impose that $c$ arise as edge-class coefficients of a polarization matrix. That geometric constraint (the alternating-sum hyperplane) is applied only downstream.
proof idea
Expand the three finite sums over Fin 6 via Fin.sum_univ_six, then unfold slotDispClass so every index becomes a concrete class in Fin 7. Rewrite each of the thirty-six raw Jacobian entries by the named weight lemmas w00 through w55. The resulting multivariate polynomial identity is discharged by ring, yielding the perfect square on the right-hand side.
why it matters
This is the algebraic engine under the Gate C-A3 headline assembledConstantBlock_eq_zero: instantiate free coefficients by the geometric edge-class map polEdgeCoeff E, then invoke the alternating-sum vanishing polEdgeCoeff_alternatingSum to kill the square. The same identity feeds the zero-momentum symbol corollary zeroMomentum_symbol_is_zero, which states that the fixed-$N$ TT Bloch symbol of the true nonlinear Regge action at $k=0$ is identically zero for every polarization.
In the broader finishing charter this closes the hinge-aware zero-mode gate: stencil-only residual is nonzero, hinge cancels it, and the free-coefficient square explains why cancellation is forced exactly on the geometric hyperplane and nowhere else. It is lattice gravity bookkeeping rather than a T0-T8 forcing step, but it is required before the continuum TT graviton mode can be read off the discrete second variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.