globalZeroDeficitAtFlat_of_angleSum
plain-language theorem explainer
If every edge of a 3D triangulation has incident local dihedral-angle contributions summing to 2π at the zero potential, the triangulation has global zero deficit in the flat configuration. Gravity and Regge-calculus workers cite this when feeding the smoothness package an angle-sum hypothesis instead of a deficit hypothesis. The proof is a two-step term: angle-sum implies flat-deficit-zero, then the known iff yields global zero deficit.
Claim. Let $K$ be a 3-dimensional triangulation. Suppose that for every global edge $e$, the sum over tetrahedra $\tau$ of the local dihedral-angle contribution of $e$ in $\tau$, evaluated at the zero potential, equals $2\pi$. Then $K$ satisfies the global zero-deficit-at-flat condition.
background
This module packages the 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; it connects the encoded periodic Freudenthal scaffold to the model target.
The hypothesis is the angle-sum form of flat zero deficit: around each global edge, the incident local dihedral-angle contributions (at the zero potential) sum to $2\pi$. That is the classical Regge picture of a flat link: deficit angle vanishes precisely when the solid angle around the edge is a full turn.
Global zero deficit at flat is the smoothness-package input that says the triangulation carries no curvature defect when all edge lengths sit at the flat reference. The angle-sum target is the equivalent, more geometric packaging of that same condition.
proof idea
Term-mode composition of two prior facts. First apply the lemma that the angle-sum target implies the flat-deficit-zero target (by unfolding the Regge deficit angle definition). Then apply the forward direction of the equivalence between flat-deficit-zero and global zero deficit at flat. No new calculation; pure transport along already-proved implications.
why it matters
Feeds the canonical periodic specialization canonicalPeriodicGlobalZeroDeficitAtFlat_of_incidentAngleSum, which reduces the global zero-deficit input for the encoded periodic Freudenthal torus to an exact incident Freudenthal dihedral-angle sum. That is the geometric gate the smoothness package needs before the physical six-tet cubic Dirichlet model can be instantiated on the torus.
In the broader gravity stack this sits between the Regge cubic-lattice limit and the Freudenthal length-chain endpoint certificates: flatness of the link (angle sum $2\pi$) is the discrete stand-in for vanishing curvature, which the continuum Dirichlet story then inherits. It is a proved bridge lemma, not scaffolding; the open work lives in discharging the angle-sum hypothesis on concrete periodic instances, not in this transport step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.