reggeAction_zeroPotential_eq_zero
plain-language theorem explainer
On the canonical periodic Freudenthal torus, the concrete Regge action at the zero potential vanishes. Gravity analysts cite this as the flat normalization of the conformal family before expanding about the frozen Hessian. The proof is a short rewrite chain: zero potential is the typed conformal image of the zero vertex field, which is the flat edge field, where the true nonlinear action is already zero.
Claim. Let $T_N$ be the canonical periodic triangulation of the $N\times N\times N$ torus with its standard incidence data. Then the concrete Regge action of $T_N$ evaluated at the zero edge-length potential equals $0$.
background
This module is Stage 1 of the Regge TT continuum-symbol campaign: it defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field, records its flat point, and sets up the frozen-model identification used later for TT Bloch symbols.
The concrete action reggeAction is the existing lattice action on a potential; the true action sums $\sqrt{\ell_e}\cdot(2\pi-\sum\theta)$ with dihedral angles from Cayley–Menger cofactors. Along conformal edge fields the two actions agree (reggeAction_conformal_eq). The zero potential is the flat configuration: all deficits vanish, so the true action at the flat edge field is zero (trueReggeAction_flatEdgeField).
No side-length positivity hypothesis is needed here; the identity is read off the typed flat point of the conformal family.
proof idea
Term-mode rewrite proof. First identify zeroPotential with toPotential N (fun _ => 0) by rfl. Rewrite with that equality, then apply three lemmas in order: reggeAction_conformal_eq (concrete action equals true action on conformal fields), typedConformalEdgeField_zero (zero vertex field maps to the flat edge field), and trueReggeAction_flatEdgeField (true action vanishes on the flat edge field). The composite yields zero.
why it matters
Supplies the flat normalization $S(0)=0$ used by frozen_identification, which writes the true action along the conformal family as $\tfrac12 Q_{\mathrm{frozen}}+\mathrm{remainder}$ with $Q$ the quadratic form of the frozen graph-Laplacian canonicalReggeHessian. That decomposition is definitionally tautological once $S(0)$ is known, but it names the frozen postulate and exposes the remainder that later stages must expand.
In the broader QG program this is bookkeeping for the Regge TT continuum symbol: numerical probes report an isotropic continuum TT symbol matching the linearized Einstein–Hilbert coefficient $-1/4$, but the Lean target ReggeTTContinuumIsotropyTarget remains open. The present lemma is a proved kernel fact, not that continuum claim. It does not invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete-gravity algebra on the Freudenthal lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.