deficitAngle_conformal_eq
plain-language theorem explainer
At any edge of the periodic Freudenthal torus, the Regge deficit of a conformal potential equals the true-action deficit of the matching conformal edge-length field. Frozen-model identification proofs cite this edgewise bridge. The argument reindexes the tetrahedron sum by the canonical tet equivalence and matches dihedral contributions slot-by-slot via the edge-slot lookup.
Claim. Let $u$ be a real scalar on the vertices of the $N\times N\times N$ periodic Freudenthal torus, and let $e$ be any edge index of the canonical triangulation. Then the Regge deficit angle of the conformal potential induced by $u$ at $e$ equals the true-action deficit of the typed conformal edge field of $u$ at the corresponding periodic edge.
background
This module is Stage 1 of the Regge TT continuum-symbol program: it defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary squared-length edge field, and prepares the frozen-wave identification of that action with the conformal ansatz already studied elsewhere.
The deficit at an edge is $2\pi$ minus the sum of dihedral angles of incident tetrahedra. Dihedrals are computed by dihedralAngle3Sq (arccos of a Cayley-Menger cofactor ratio) on local squared-edge 6-tuples. Incidence uses the computable slot lookup canonicalEdgeSlot? on the skeleton canonicalPeriodicTriangulation. Finite edge and tet index sets are identified with the typed periodic edges and tets via edgeFinEquiv and tetFinEquiv.
On the frozen side, a vertex potential $u$ induces a conformal edge field (typedConformalEdgeField); the true-action deficit of that field is deficitOfField. The classical side uses deficitAngle on the triangulation with potential toPotential N u.
proof idea
Both sides unfold to a sum of local dihedral contributions over tetrahedra. After congr 1, the tet sums are identified by Fintype.sum_equiv along tetFinEquiv. For each tet, simplify the local contribution definitions and rewrite the edge-in-tet predicate by canonical_edgeInTet_eq. Case on canonicalEdgeSlot? of the transported edge in that tet: if the edge is absent, both contributions are definitionally zero; if present at slot $f$, simplify the conformal dihedral and the field dihedral to dihedralAngle3Sq and finish by conformalTetSqEdges_eq_typedField, which equates the squared-edge 6-tuples.
why it matters
This is the edgewise hinge of the frozen-model identification. Downstream, reggeAction_conformal_eq sums it over edges to prove that the conformal-ansatz Regge action equals the true nonlinear action on conformal edge fields: the kernel equation stating which restriction of the true action the frozen model lives on.
In the QG full-theory campaign this closes a THEOREM-tier step of Stage 1 preflight for the TT Bloch symbol. It does not touch the OPEN continuum target ReggeTTContinuumIsotropyTarget (isotropy of the TT symbol with value $K(0)=-(1/4)I_{TT}$); that remains numerical evidence only. Within Recognition gravity analysis it licenses transferring continuum and symbol statements proved on the frozen conformal sector back to the true Regge action along conformal deformations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.