flatEdgeField
plain-language theorem explainer
Defines the flat background edge-length field on the side-N periodic Freudenthal torus: each positive-displacement edge is assigned the squared length of its displacement class (1,1,1,2,2,2,3). Anyone working the true nonlinear 3D Regge action or TT Bloch symbol cites this as the zero-curvature base point. The body is a one-line pointwise pullback of the canonical displacement-squared table.
Claim. The flat edge field on the side-$N$ periodic Freudenthal torus is the map sending each periodic edge $e$ to the squared length of its positive displacement class, namely the values $(1,1,1,2,2,2,3)$ on the seven classes.
background
This module is Stage 1 of the Regge TT continuum-symbol campaign: it builds the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field, then sets up the TT Bloch symbol object around a flat background.
An edge field is simply a real number (squared length) per positive-displacement periodic edge. The flat choice uses periodicDispSqEdge, which depends only on the displacement class and returns $1$ on the three unit axes, $2$ on the three face diagonals, and $3$ on the space diagonal. That table is exactly the squared edge lengths of the one-cube Freudenthal triangulation of Euclidean space, so the assignment is the discrete flat metric.
Downstream lemmas read local six-tuples of squared edges off this field through the canonical edge-slot tables and feed them into Cayley–Menger dihedral angles and deficit sums.
proof idea
Pure definition: pointwise, apply the displacement-class squared-length table to the edge's displacement. No proof obligations; the type is the edge-field abbreviation (periodic edges to reals).
why it matters
This is the flat point of the true Regge action. Sibling theorems show that at this field every tetrahedron sees the canonical Freudenthal squared-edge tuple, every per-tet angle contribution matches the certified typed-edge angle chain, every deficit vanishes, and the full action is zero. The plane-wave family collapses to this field at amplitude zero, so second-difference and TT Bloch constructions expand about a kernel-checked zero mode.
It grounds the derivative-gate stencil ordering (every tet of the true action sees the stencil's flat tuple) and the status-flag theorem that pins flat_deficit_zero and flat_action_zero to actual kernel facts. In the QG full-theory campaign this is the background against which continuum isotropy of the TT symbol (open target ReggeTTContinuumIsotropyTarget, numerically $K(0)=-(1/4)I_{TT}$) is measured; nothing here claims that continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.