typedConformalEdgeField
plain-language theorem explainer
Defines the conformal edge squared-length field on the periodic Freudenthal torus from a vertex potential u: each edge gets its flat displacement squared length times exp(u at both endpoints). Gravity analysts cite it as the exact edge-field family underlying the frozen-wave Regge model. The body is a one-line pointwise product of the displacement class length with that exponential.
Claim. Given a real vertex potential $u$ on the side-$N$ periodic cubic lattice, the induced conformal edge field assigns to each positive-displacement periodic edge $e$ the value $\ell^2_{\mathrm{flat}}(e)\,\exp\bigl(u(e_+)+u(e_-)\bigr)$, where $\ell^2_{\mathrm{flat}}(e)$ depends only on the displacement class of $e$ (values in $\{1,2,3\}$).
background
This module is Stage 1 of the Regge TT continuum-symbol program: it sets up the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus, identifies the frozen conformal model with a restriction of that action, and prepares the TT Bloch symbol object. Numerical evidence (not proved here) suggests continuum TT isotropy with Einstein-Hilbert coefficient $-1/4$; the open target is ReggeTTContinuumIsotropyTarget.
An edge field is a real assignment of squared lengths to positive-displacement periodic edges. The flat background uses only the displacement class via periodicDispSqEdge (classes map to $1,1,1,2,2,2,3$). Vertices are triples in $\mathrm{Fin},N^3$. The conformal family deforms those flat lengths by a multiplicative factor built from a scalar potential at the two endpoints, matching the frozen-wave ansatz used earlier through conformal local squared edges.
proof idea
Pure definition: pointwise, for each edge $e$, multiply the class-dependent flat squared length periodicDispSqEdge e.disp by $\exp(u(e_+)+u(e_-))$. No lemmas or tactics; the type is the edge-field abbreviation (maps from periodic edges to reals).
why it matters
This is the bridge between vertex potentials and the true nonlinear Regge action. Downstream, reggeAction_conformal_eq proves the frozen conformal Regge action equals trueReggeAction on this field (frozen-model identification, part 1). deficitAngle_conformal_eq, hingeMeasure_conformal_eq, and conformalTetSqEdges_eq_typedField transport deficit, hinge measure, and local tet edge tuples onto the same family. frozen_identification and frozen_identification_stencil then decompose the action along this family into the frozen Hessian quadratic (equivalently the anisotropic seven-class Freudenthal stencil energy) plus remainder. That remainder is what later stages must expand to reach the open continuum TT isotropy claim. In short, every conformal identification in the preflight routes through this constructor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.