Pith. sign in
theorem

polEdgeCoeff_alternatingSum

proved
show as:
module
IndisputableMonolith.Gravity.Analysis.ReggeTTHingeAwareZeroMode
domain
Gravity
line
342 · github
papers citing
none yet

plain-language theorem explainer

For every real 3×3 matrix E, the alternating sum of its seven edge-class polarization coefficients vanishes: three face-diagonal classes exactly double-count the three axis classes plus the body diagonal. Anyone proving the Gate C-A3 assembled constant-block zero mode cites this identity. The proof unfolds the coefficient definition and finishes by ring.

Claim. For every real $3\times 3$ matrix $E$, writing $c_d(E)$ for the edge-class coefficient of $E$ in displacement class $d\in\{0,\ldots,6\}$, one has $c_0(E)+c_1(E)+c_2(E)-c_3(E)-c_4(E)-c_5(E)+c_6(E)=0$. Equivalently, at the level of quadratic-form values, $c_{x+y}+c_{x+z}+c_{y+z}=2\,\mathrm{tr}+\mathrm{off}=(c_x+c_y+c_z)+c_{x+y+z}$.

background

This module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1): the hinge-aware zero mode of the Regge TT Bloch symbol. The sympy diagnostic found that the stencil-only constant block does not vanish under TT (kernel residual $-\pi(\sqrt{2}+4)/8$), while the assembled $k=0$ cell stencil does vanish once hinge and Hessian blocks are combined with a relative minus sign.

Edge-class coefficients $c_d(E)$ extract, for each of the seven Freudenthal displacement classes on the cubic lattice (three axis, three face-diagonal, one body-diagonal), the quadratic-form pairing of a polarization matrix $E$ with the corresponding real displacement vector. They are the building blocks of both the hinge/edge-diagonal $O(1)$ block and the assembled constant block.

The identity proved here is purely algebraic in those seven scalars: the three face-diagonal classes double-count exactly what the three axis classes and the body-diagonal class contribute. No TT or wave-vector hypothesis is required.

proof idea

Term-mode proof by definition chase and ring. Unfold the edge-class coefficient definition together with the real displacement map of the Freudenthal stencil preflight, expand the three-term finite sums over Fin 3, and close with ring. No external lemmas beyond the coefficient definition and the displacement encoding are needed; the cancellation is an identity of quadratic forms on $3\times 3$ matrices.

why it matters

This is the free-coefficient identity that makes the Gate C-A3 headline go through. The parent theorem assembledConstantBlock_eq_zero reduces the assembled constant block (Schlaefli-reduced $k=0$ raw cell stencil) to a linear combination of the seven edge-class coefficients, then rewrites that combination via the free-coefficient zero-mode lemma and this alternating-sum identity, obtaining zero for every polarization matrix $E$.

Downstream, the zero-momentum symbol corollary uses the same vanishing to conclude that the fixed-$N$ TT Bloch symbol of the true nonlinear Regge action at zero wave vector exists and equals zero. In the finishing charter this closes the hinge-aware half of the lattice flat zero mode: stencil-only residual is cancelled by the hinge block, and the algebraic skeleton of that cancellation is the present sum.

No Recognition forcing-chain landmark (T5–T8, RCL, phi) is directly invoked; the result is local to the Regge discrete-gravity analysis lane.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.