trueReggeAction
plain-language theorem explainer
Defines the true nonlinear 3D Regge action on the side-N periodic Freudenthal torus: S(ℓ)=Σ_e √(ℓ_e)·deficit_e for an arbitrary edge squared-length field. Anyone citing the TT Bloch symbol, frozen-model identification, or conformal restriction of Regge gravity on this lattice uses this object. The body is a single finite sum over positive-displacement periodic edges.
Claim. For an edge squared-length field $\ell$ on the side-$N$ periodic Freudenthal torus, the true nonlinear Regge action is $S(\ell)=\sum_e \sqrt{\ell_e}\,\delta_e(\ell)$, where the sum runs over positive-displacement periodic edges and $\delta_e(\ell)$ is the angular deficit at edge $e$ computed from local Cayley–Menger dihedral angles on the squared-edge tuples read from $\ell$.
background
This module is Stage 1 of the Regge TT continuum-symbol program in the QG full-theory campaign. It fixes the true nonlinear 3D Regge action on the canonical periodic Freudenthal triangulation, then builds the flat point, frozen-model identification, and the TT Bloch symbol object around it.
An edge field assigns one real squared length to each positive-displacement periodic edge (base vertex plus one of seven cube displacements). The deficit at an edge is $2\pi$ minus the sum of incident tetrahedron dihedral angles; those angles come from existing Cayley–Menger machinery (dihedralAngle3Sq / cofactor ratios) on the local six-edge squared tuples looked up from the field. The classical continuum target is the Einstein–Hilbert TT coefficient $-1/4$ in the campaign conventions; continuum isotropy of the true action’s TT symbol remains an open named target outside this definition.
proof idea
Pure definition: one finite sum over the Fintype of periodic edges, weighting each edge by $\sqrt{\ell_e}$ times the already-defined per-edge deficit functional. No lemmas, no tactics, no reduction.
why it matters
This is the action whose TT Bloch symbol the C10 probe measured numerically (isotropic continuum limit $K(0)=-(1/4)I_{TT}$ on preregistered directions). Downstream, the plane-wave action profile is literally this functional on plane-wave edge fields; the conformal restriction equals the older concrete Regge action; frozen identification writes $S=(1/2)Q_{\mathrm{frozen}}+\mathrm{remainder}$ along conformal fields; status flags pin flat-action-zero to $S(\ell_{\mathrm{flat}})=0$. It is the nonlinear object the frozen stencil and continuum-isotropy program must eventually expand, not a linearized proxy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.