typedConformalEdgeField_zero
plain-language theorem explainer
The zero conformal potential on the periodic Freudenthal lattice produces exactly the flat squared-length edge field. Gravity analysts cite this when normalizing the true nonlinear Regge action at the typed flat point. The proof is a pointwise simplification: function extensionality plus exp(0)=1 and the ring identities add_zero and mul_one.
Claim. For every lattice size $N$, the typed conformal edge-length field built from the identically zero potential equals the flat edge field: $\ell^{\mathrm{conf}}_N(0)=\ell^{\mathrm{flat}}_N$.
background
This module is Stage 1 of the Regge TT continuum-symbol campaign: it defines the true nonlinear 3D Regge action $S(\ell)$ on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field, reuses Cayley–Menger dihedral angles, and prepares the TT Bloch symbol object. Numerical evidence (not proved here) points to an isotropic continuum TT symbol $K(0)=-(1/4)I_{TT}$; the open Lean target is ReggeTTContinuumIsotropyTarget.
Edge geometry is carried by maps from periodic edges to real squared lengths. The flat edge field is the constant (or lattice-normalized) background with vanishing deficit. The typed conformal edge field is the standard exponential conformal deformation of that background by a real potential on edges (or vertices, pushed to edges): schematically $\ell_e(\phi)=\ell^{\mathrm{flat}}_e,e^{\phi_e}$ or an additive log-length form that reduces to the same identities at $\phi=0$.
Sibling lemmas already record that flat fields give vanishing deficit and vanishing true Regge action; this theorem identifies the zero-potential conformal point with that flat field without an extra side-length hypothesis.
proof idea
Term-mode proof by pointwise equality. Apply function extensionality on edges, then unfold the definitions of the typed conformal edge field and the flat edge field. The remaining arithmetic is discharged by simp with Real.exp_zero (so the conformal factor is 1), together with add_zero and mul_one. No geometric lemmas about deficits or dihedral angles are required.
why it matters
Feeds directly into reggeAction_zeroPotential_eq_zero, which states that the conformal Regge action at zero potential is zero, obtained from the typed flat point without a separate side-length hypothesis. That flat normalization is the reference point for the true nonlinear action before second-difference / Bloch-symbol analysis of TT modes.
In the QG full-theory program this anchors Stage 1 preflight: the continuum TT isotropy target and the match to the linearized Einstein–Hilbert coefficient $-1/4$ are measured relative to this flat conformal origin. It does not itself touch the forcing chain (T5–T8) or RCL; it is lattice gravity infrastructure that makes the Regge TT symbol well-defined at the vacuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.