ttSecondDifference_even
plain-language theorem explainer
The per-cell second-difference quadratic form of the true Regge action along a plane-wave family is even in the amplitude: evaluating at −t equals evaluating at t. Anyone building or citing the TT Bloch symbol object needs this symmetry. The proof is a short algebraic identity after unfolding the definition: double negation and (−t)² = t² make the numerator and denominator match.
Claim. For any polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$, wavevector $k\in\mathbb{R}^3$, and amplitude $t\in\mathbb{R}$, the normalized second-difference form of the plane-wave action profile satisfies $Q_E(k,-t)=Q_E(k,t)$, where $Q_E(k,t)=(2/N^3)\,(S(t)-2S(0)+S(-t))/t^2$ and $S$ is the true Regge action along the plane-wave edge field of amplitude $t$.
background
This module is Stage 1 of the Regge TT continuum-symbol campaign: it defines the true nonlinear 3D Regge action on the periodic Freudenthal torus as a function of an arbitrary edge squared-length field, identifies the flat point, and sets up the TT Bloch symbol object. Numerical C10 probes suggest continuum isotropy with Einstein–Hilbert coefficient $-1/4$, but that continuum claim remains an OPEN target; the file only certifies definitions and algebraic preflight lemmas.
The second-difference form is the per-unit-cell Bloch quadratic form in C10 conventions: $(2/N^3)\cdot(S(t)-2S(0)+S(-t))/t^2$, with $S$ the plane-wave action profile at polarization $E$ and momentum $k$. Evenness in the amplitude $t$ is the elementary symmetry needed before one treats the object as a well-formed quadratic symbol rather than a directed finite-difference probe.
proof idea
Term-mode algebraic identity. Unfold the definition of the second-difference form. Rewrite with neg_neg (so $S(-(-t))=S(t)$) and neg_sq (so $(-t)^2=t^2$). The numerator $S(-t)-2S(0)+S(t)$ is then identical to $S(t)-2S(0)+S(-t)$, and the common positive factor $(2/N^3)/t^2$ matches; ring closes the equality. No property of the action profile beyond its appearance in the formula is used.
why it matters
Evenness is one of the well-formedness/symmetry lemmas for the TT Bloch symbol object that the preflight status record certifies. Downstream, ReggeTTSymbolPreflightStatus and status_flags_grounded pin those flags to kernel theorems (instantiated at $N=3$ for the campaign torus) rather than bare Booleans. Without evenness, the second-difference form would depend on the sign of the probe amplitude and could not serve as a quadratic symbol candidate.
In the broader QG full-theory program this sits under gravity analysis on the Freudenthal lattice, preparing the continuum TT symbol whose isotropy and value $K(0)=-(1/4)I_{TT}$ remain OPEN (ReggeTTContinuumIsotropyTarget). The lemma is pure preflight algebra, not a continuum or Einstein–Hilbert identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.