FlatDeficitAngleSumTarget
plain-language theorem explainer
For a finite 3D Regge triangulation, the flat zero-deficit condition is restated as an angle-sum target: around every global edge the incident local dihedral angles, evaluated at the zero conformal potential, sum exactly to 2π. Gravity and discrete-geometry workers cite it when packaging Dirichlet/Regge flatness inputs without naming deficit angles. It is a pure Prop definition, not a proved statement.
Claim. For a finite 3D Regge triangulation $K$, the property $\mathrm{FlatDeficitAngleSumTarget}(K)$ holds when, for every global edge $e$, the sum over all tetrahedra $\tau$ of the local dihedral-angle incidence contribution of $\tau$ at $e$ (under the zero conformal vertex potential) equals $2\pi$.
background
The ambient module packages exact theorem obligations that instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it only records the geometric targets needed for that instantiation.
A Triangulation3D is a finite abstract 3D Regge complex: vertex/edge/tet counts, edge endpoints, tet vertex maps, and nondegenerate squared-edge data on each tetrahedron. The zero conformal potential assigns the constant $0$ to every vertex. The local incidence contribution of a tetrahedron $\tau$ at a global edge $e$ is the dihedral angle of $\tau$ at the corresponding face under that conformal chart, or $0$ if $e$ does not meet $\tau$.
Classically the hinge deficit is $2\pi$ minus the sum of incident dihedral angles. The present definition is the dual angle-sum form of flatness: that sum equals $2\pi$ at every edge when the metric is undeformed.
proof idea
No proof: this is a definition of a proposition. The body is a universal quantifier over global edges requiring that the sum of localDeficitAngleContribution terms at the zero potential equals $2\pi$. Downstream lemmas unfold the Regge deficit angle identity $\mathrm{deficit}=2\pi-\sum\theta$ to convert this target into zero-deficit form.
why it matters
This Prop is the angle-sum packaging of flat zero deficit used throughout the physical six-tet cubic Dirichlet instance. Downstream, flatDeficitZeroTarget_of_angleSum unfolds the Regge deficit to obtain edgewise zero deficit from the angle sum; globalZeroDeficitAtFlat_of_angleSum lifts that to the global zero-deficit input of the smoothness package; and canonicalPeriodicFlatDeficitAngleSumTarget_of_incidentAngleSum shows the canonical periodic Freudenthal torus meets this target once its incident-angle-sum hypothesis is granted.
In the broader gravity stack this is scaffolding for Regge flatness on the encoded periodic cubic lattice before Hessian/Dirichlet analysis. It sits in the discrete-geometry layer that feeds continuum limit and physical Dirichlet model obligations, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.