EdgeField
plain-language theorem explainer
An edge squared-length field assigns one real number (a squared length) to each positive-displacement periodic edge on the side-N Freudenthal torus. Anyone writing the true nonlinear 3D Regge action, deficits, or TT Bloch symbols on this lattice cites this type. It is a one-line type abbreviation, not a proved statement.
Claim. An edge field on the side-$N$ periodic Freudenthal torus is a map $\ell$ from the set of positive-displacement periodic edges to $\mathbb{R}$, sending each edge to a squared length.
background
This module is Stage 1 of the Regge TT continuum-symbol program: it packages the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus, its flat background, and the TT Bloch symbol object used in the continuum-isotropy campaign.
A PeriodicEdge is a positive-displacement edge on the $N\times N\times N$ torus, given by a base vertex and one of seven cube displacements. The seven displacement classes carry flat squared lengths $1,1,1,2,2,2,3$. An edge field is simply an arbitrary real assignment to those edges; the flat field and plane-wave perturbations are special cases.
Downstream, local six-tuples of squared edges are read off the field via the canonical edge-slot tables, then fed to Cayley–Menger dihedral angles. Deficits are $2\pi$ minus the incident angle sum, and the true Regge action is $\sum_e \sqrt{\ell_e}\cdot\mathrm{deficit}(e)$.
proof idea
No proof: this is a type abbreviation. It names the function space PeriodicEdge N N N → ℝ so every later definition (flat field, plane-wave family, local squared-edge readout, dihedral angles, deficits, true Regge action) can take a single parameter of that type.
why it matters
This is the configuration space for the true nonlinear Regge action in the QG full-theory campaign. Every object in the preflight stack is parameterized by it: flatEdgeField, planeWaveEdgeField, typedConformalEdgeField, tetSqEdgesOfField, tetDihedralAngleOfField, edgeAngleContributionOfField, deficitOfField, and trueReggeAction.
The module’s open target is continuum TT isotropy of that action’s Bloch symbol (numerical evidence only so far: $K(0)=-(1/4)I_{TT}$). Without a uniform edge-field type, the nonlinear action, its linearization, and the frozen-model comparison cannot be stated on the same domain. In the Recognition gravity stack this is the lattice-side input to the Regge TT continuum-symbol program, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.