flatDeficitZeroTarget_of_angleSum
plain-language theorem explainer
If the local dihedral angles incident on every edge of a 3D Regge triangulation sum to $2\pi$ at the zero potential, then every Regge deficit angle vanishes. Gravity and discrete-geometry workers cite this when converting an angle-sum flatness certificate into the zero-deficit input required by the flat Regge background. The proof is a one-line algebraic identity: unfold the deficit definition and cancel $2\pi-2\pi$.
Claim. Let $K$ be a finite 3D Regge triangulation. Suppose that for every global edge $e$, the sum of the local dihedral-angle contributions around $e$ at the zero vertex potential equals $2\pi$. Then for every global edge $e$, the Regge deficit angle of $K$ at the zero potential vanishes: $\delta_e=0$.
background
The module packages exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
A Triangulation3D is a finite abstract 3D Regge complex with incidence data and nondegenerate squared-edge lengths on each tetrahedron. The Regge deficit at a global edge under a vertex potential $\xi$ is defined by
$$\delta_e(\xi)=2\pi-\sum_\tau\theta_{e,\tau}(\xi),$$
where $\theta_{e,\tau}$ is the local dihedral contribution of tetrahedron $\tau$ at edge $e$ (the classical hinge deficit $2\pi-\sum\theta$).
Two equivalent flatness targets are used here. The angle-sum target asserts $\sum_\tau\theta_{e,\tau}(0)=2\pi$ for every edge at the zero potential. The zero-deficit target asserts $\delta_e(0)=0$ for every edge. The latter is the geometric input that normalizes the flat Regge action to zero and feeds the smoothness/FlatConfiguration package.
proof idea
Term-mode proof by direct expansion. Fix an arbitrary global edge $e$. Unfold the definition of the Regge deficit angle, which is $2\pi$ minus the sum of local dihedral contributions at the zero potential. Rewrite that sum using the angle-sum hypothesis, which supplies equality to $2\pi$. The remaining identity $2\pi-2\pi=0$ is discharged by ring. No geometric lemmas beyond the definition of deficitAngle are required.
why it matters
Zero deficit on the flat background is the exact geometric normalization needed before the scaled finite-limit and Dirichlet Hessian machinery can run on the six-tet cubic lattice. This bridge converts the more convenient incident-angle-sum certificate into that zero-deficit target.
Downstream, globalZeroDeficitAtFlat_of_angleSum packages the same fact as the global zero-deficit input consumed by the smoothness layer, and canonicalPeriodicFlatDeficitZeroTarget_of_incidentAngleSum specializes it to the canonical encoded periodic Freudenthal torus (the concrete lattice used for the physical Dirichlet instance). Together they close the flat-geometry side of the obligations listed in the module doc: prove the flat-deficit target from canonical flat geometry, then hand it to the physical model.
In the broader RS gravity stack this sits under the Regge cubic-lattice limit and Freudenthal length-chain work, not under the T0–T8 forcing chain itself; it is discrete-geometry infrastructure for the continuum Dirichlet identification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.