trueReggeAction_flatEdgeField
plain-language theorem explainer
The true nonlinear 3D Regge action on the periodic Freudenthal torus vanishes at the flat edge-length assignment. Gravity analysts cite this as the kernel-checked flat point of the full (non-conformal) action before TT-symbol work. The proof unfolds the edge sum and multiplies the already-proved zero deficit at each edge by the edge factor.
Claim. For every lattice size $N$, the true Regge action evaluated on the flat edge squared-length field is zero: $S(\ell_{\mathrm{flat}}) = 0$, where $S(\ell) = \sum_e \sqrt{\ell_e}\,(2\pi - \sum_{t \ni e} \theta_t)$ and $\ell_{\mathrm{flat}}$ assigns the Euclidean squared lengths of the canonical triangulation.
background
This module is Stage 1 of the Regge TT continuum-symbol campaign in quantum gravity: it defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field $\ell$, not merely the conformal restriction used in earlier frozen-wave tests.
The action is $S(\ell) = \sum_e \sqrt{\ell_e} \cdot \delta_e$, with deficit $\delta_e = 2\pi - \sum_{\text{incident tets}} \theta$ and dihedral angles from the existing Cayley–Menger machinery (dihedralAngle3Sq). The flat edge field is the Euclidean squared-length assignment on that triangulation; a sibling theorem already shows every deficit vanishes there.
Local setting: preflight for the TT Bloch symbol of the true action. Numerical evidence (not proved here) suggests continuum isotropy with Einstein–Hilbert TT coefficient $-1/4$; the open target is continuum isotropy of that symbol.
proof idea
Term-mode proof by unfolding the action definition, which is a finite sum over edges of $\sqrt{\ell_e}$ times the deficit at $e$. Apply Finset.sum_eq_zero and, at each edge, rewrite the deficit via the sibling lemma that every deficit of the flat edge field is zero, then cancel with mul_zero. No angle or Cayley–Menger computation is redone here; the work is delegated to the flat-deficit lemma.
why it matters
Establishes the flat point of the true (nonlinear, non-conformal) Regge action as a kernel theorem, which the status record flags as flat_action_zero. Downstream, planeWaveActionProfile_zero uses it to show the plane-wave action profile vanishes at amplitude zero, and reggeAction_zeroPotential_eq_zero ties conformal flat normalization to this typed flat point.
In the QG full-theory campaign this is the action-form half of the flat-point certificate (paired with zero deficits). It grounds Stage 1 before the frozen-model identification along conformal fields and before any claim about the TT Bloch symbol. It does not touch continuum isotropy: that remains the open ReggeTTContinuumIsotropyTarget. Framework-wise it sits in discrete gravity on the eight-tick / $D=3$ lattice side, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.