deficitOfField_flatEdgeField
plain-language theorem explainer
At the flat squared-length assignment on the periodic Freudenthal torus, the Regge deficit angle vanishes on every edge. Gravity analysts cite this as the kernel-checked flat point of the true nonlinear 3D Regge action. The proof rewrites the angle sum via the flat-field contribution lemma and invokes the certified periodic typed angle-sum identity, then cancels 2π − 2π.
Claim. For every positive-displacement periodic edge $e$ on the side-$N$ Freudenthal torus, the Regge deficit of the constant flat edge-squared-length field at $e$ is zero: $\delta(\ell_{\mathrm{flat}}, e) = 0$, where $\delta = 2\pi - \sum_{t}\theta_{t}$ is $2\pi$ minus the sum of incident dihedral angles.
background
This module is Stage 1 of the Regge TT continuum-symbol campaign: it defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus as a function of an arbitrary edge squared-length field, and records its flat point before any continuum or TT analysis.
A PeriodicEdge is a base vertex plus one of seven positive cube displacements. A PeriodicTet is one of the six Freudenthal tetrahedra in each cubic cell. The deficit at an edge under a field $\ell$ is $2\pi$ minus the sum, over all periodic tets, of the per-tet angle contribution (dihedral angle when the edge occupies a slot of that tet, else zero).
The flat field is the constant Euclidean squared-length assignment. Upstream, edgeAngleContributionOfField_flat identifies each flat contribution with the certified typed-edge angle contribution, and canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds states that those typed contributions sum to exactly $2\pi$ around every edge.
proof idea
Unfold the deficit definition to $2\pi$ minus the sum of angle contributions. The main step is a calc block: replace each summand by the certified typed contribution via edgeAngleContributionOfField_flat (congruence under Finset.sum_congr), then apply canonicalPeriodicDirectTypedEdgeAngleSumTarget_holds to obtain sum $= 2\pi$. Rewrite the deficit with that identity and finish by ring ($2\pi - 2\pi = 0$). No geometry is re-derived; the periodic angle-sum chain is reused as a black box.
why it matters
This is the deficit form of the flat-point theorem for the true Regge action. Downstream, trueReggeAction_flatEdgeField multiplies each edge term by this vanishing deficit to prove the full action is zero at flat. The second-variation module re-exports it as deficit_planeWave_zero: plane-wave edge fields at amplitude zero reduce to the flat field, so deficits vanish along that family at $t=0$.
It grounds the status flag flat_deficit_zero in ReggeTTSymbolPreflightStatus and appears in status_flags_grounded. In the QG campaign this certifies that the nonlinear action has a genuine Euclidean critical point before TT Bloch-symbol and continuum-isotropy work. The continuum isotropy target (ReggeTTContinuumIsotropyTarget, $K(0)=-(1/4)I_{TT}$) remains open; this lemma only locks the discrete flat point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.