ttSecondDifference
plain-language theorem explainer
Defines the normalized centered second difference of the true Regge plane-wave action profile at amplitude t: (2/N³)·(S(t)−2S(0)+S(−t))/t². This is the per-unit-cell TT Bloch quadratic form in the C10 conventions. Anyone proving fixed-N TT symbol existence or continuum isotropy cites it. The body is a pure arithmetic abbreviation of the plane-wave action profile.
Claim. For a polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$, wave vector $k\in\mathbb{R}^3$, and amplitude $t\in\mathbb{R}$, the TT second difference is $$\frac{2}{N^3}\cdot\frac{S_N(E,k;t)-2S_N(E,k;0)+S_N(E,k;-t)}{t^2},$$ where $S_N$ is the true nonlinear Regge action evaluated on the plane-wave edge-length family of amplitude $t$. The factor $2/N^3$ is the per-unit-cell Bloch normalization of the C10 conventions.
background
This module is Stage 1 of the Regge TT continuum-symbol program: it packages the true nonlinear 3D Regge action on the periodic Freudenthal torus, its flat point, and the TT Bloch symbol object. The true action is $S(\ell)=\sum_e\sqrt{\ell_e},(2\pi-\sum\theta)$ with dihedral angles from Cayley–Menger cofactors on local squared-edge tuples.
The plane-wave action profile $S_N(E,k;t)$ evaluates that action on a monochromatic edge-length perturbation of amplitude $t$, polarization $E$, and commensurate momentum $k$. The centered second difference of a $C^2$ scalar $f$ at $0$ is the classical discrete second derivative $(f(t)-2f(0)+f(-t))/t^2$, which converges to $f''(0)$ on the punctured neighborhood of $0$ (local bridge theorem in the existence file).
The prefactor $2/N^3$ converts the global second variation into a per-unit-cell Bloch quadratic form, matching the C10 audit conventions used by the frozen-model and continuum-isotropy targets.
proof idea
Pure definition: no proof obligations. The body multiplies the centered second difference of planeWaveActionProfile N E k by the constant bookkeeping factor $2/N^3$. Downstream existence theorems apply the reusable local bridge (tendsto_centeredSecondDifference_of_contDiffAt) to pass the $t\to 0$ limit inside, identifying the limit with $(2/N^3)\cdot S''(0)$.
why it matters
This is the raw discrete object whose punctured-neighborhood limit is the fixed-$N$ TT Bloch symbol. The value predicate TTBlochSymbolIs is literally "ttSecondDifference tends to $H$". The headline existence theorem planeWave_TTBlochSymbolIs_secondVariation then proves that limit equals $(2/N^3)\cdot(\mathrm{iteratedDeriv},2,S,0)$, with exact bookkeeping and no stray $1/2$.
Evenness and polarization-sign lemmas in this file are stated directly on this form. The 4D exact-action symbol sequence reuses the same $(2/N^3)\cdot S''$ convention as dimension-independent discrete bookkeeping. Numerically, the C10 probe reports continuum isotropy with $K(0)=-(1/4)I_{TT}$ (the linearized Einstein–Hilbert TT coefficient); the open Lean target ReggeTTContinuumIsotropyTarget is the continuum limit of this object, still flagged false.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.