ttSecondDifference_smul
plain-language theorem explainer
Under rescaling a TT polarization matrix by a nonzero constant c, the second-difference quadratic form of the plane-wave Regge action scales by c² with amplitude t replaced by c·t. Gravity analysts auditing the continuum TT Bloch symbol cite this kernel identity. It shows that any unnormalized fixed numerical target (e.g. −1/4) is contradictory, since the same physical family would report both H and c²·H. The proof unfolds the second difference, applies plane-wave action-profile scaling, and clears field denominators.
Claim. Let $c,t\in\mathbb{R}$ be nonzero, $E$ a $3\times 3$ real matrix, and $k\in\mathbb{R}^{3}$. Write $D_{E}(t)$ for the second-difference quadratic form of the plane-wave Regge action profile at amplitude $t$. Then $D_{cE}(t)=c^{2}\,D_{E}(c\cdot t)$.
background
This module is Gate A0 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol in the ReggeTTContinuumSymbol program (QG full-theory, Crux-1(c)). The open target claims a fixed continuum TT Bloch symbol value $-1/4$ on every TT polarization. That fixed number is meaningful only if rescaling cannot manufacture a contradiction.
The plane-wave edge-length family is linear in the polarization matrix $E$ through the edge-class coefficient $c_d(E)=\sum_{ij}E_{ij}D_d^i D_d^j$ (standard quadratic-form convention $D^T E D$). Replacing $E\mapsto c\cdot E$ therefore reparametrizes the same physical family via $t\mapsto c\cdot t$. The second-difference form extracted from the action profile must then scale by $c^{2}$.
Upstream, the plane-wave action profile is already known to scale under $E\mapsto c\cdot E$ (sibling scaling lemmas for polarization coefficients and edge fields). The second-difference operator is the discrete two-jet of that profile about amplitude zero; this theorem records its induced quadratic scaling.
proof idea
Term-mode proof. First record that the lattice size $N$ is nonzero as a real (from NeZero). Unfold the second-difference definition. Simplify with the already-proved plane-wave action-profile scaling identity under $E\mapsto c\cdot E$, together with the elementary rules $c\cdot 0=0$ and $c\cdot(-x)=-(c\cdot x)$. Finish by field_simp, which clears the nonzero denominators $t$ and $c\cdot t$ and produces the factor $c^{2}$ on the right-hand side.
why it matters
Kernel fact (c) in the Gate A0 scaling audit. Downstream it feeds the one-direction Bloch-symbol scaling theorem: if the symbol value at $E$ is $H$, then at $c\cdot E$ it is $c^{2}\cdot H$. Together with the Frobenius pin in the TT-polarization predicate (only $c^{2}=1$ preserves the hypothesis class), this makes a fixed numerical target over normalized polarizations well-posed, while an unnormalized fixed-value claim would force both $H$ and $c^{2}\cdot H$.
The module doc records that the double-counting conventions in the edge coefficient and the Frobenius norm are mutually consistent, matching the C10 numerics probe. Closing this scaling chain is what lets the lane proceed toward the continuum isotropy target rather than stalling on a contradictory specification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.