GlobalZeroDeficitAtFlat
plain-language theorem explainer
Global zero-deficit at the flat potential means every edge of a finite 3D Regge triangulation has vanishing deficit angle when all conformal vertex potentials are zero. It is an assembled-mesh condition, not a local tetrahedron fact. First-variation and flat-configuration packages cite it as the global geometric input that makes the nonlinear Regge action critical at flat space. The declaration is a pure Prop abbreviation of that edgewise vanishing statement.
Claim. For a finite 3D Regge triangulation $K$, the property $\mathrm{GlobalZeroDeficitAtFlat}(K)$ holds if and only if, at the zero conformal vertex potential $\xi\equiv 0$, the Regge deficit angle on every global edge $e$ vanishes: $\delta_K(0,e)=0$.
background
The module packages analytic hypotheses needed for the full nonlinear Regge action: the conformal edge chart must stay in the nondegenerate tetrahedral cone, arccos arguments must avoid $\pm 1$, and the finite action must be smooth at the flat potential. Those requirements are named configurations rather than hidden axioms.
A Triangulation3D is finite incidence data (vertices, edges, tets) plus a nondegenerate squared-edge tuple on every tetrahedron. The zero conformal potential assigns value $0$ to every vertex. The deficit angle on a global edge is $2\pi$ minus the sum of local dihedral contributions from incident tets under the conformal ansatz.
The doc-comment stresses the global character: zero deficit on the assembled mesh does not follow from local nondegeneracy of each tetrahedron alone. Local Euclidean realizations supply chart data; this Prop records the complementary global angle-sum condition.
proof idea
There is no proof body: the declaration is a definitional Prop. It expands to the universal quantification that deficitAngle K (zeroPotential K) e = 0 for every edge index e : Fin K.nE. Downstream lemmas treat the name as a hypothesis rather than deriving it from local data.
why it matters
First-variation theorems use this hypothesis to conclude directional and full criticality of the Regge action at the zero potential once the first-variation formula is available (directionalCritical_of_firstVariationFormula_of_zeroDeficit, reggeActionCriticalAtZero_of_firstVariationFormula_of_zeroDeficit).
The smoothness module itself packages it with a local analytic flat chart into FlatConfiguration via flatConfiguration_of_localChart_zeroDeficit. On the gravity side, the physical six-tet cubic Dirichlet instance treats it as the remaining global input after a realized Freudenthal tetrahedron supplies the local chart (CanonicalPeriodicFlatConfigurationInputs, and the ..._of_realizedFreudenthalTet_zeroDeficit constructors), feeding continuum Dirichlet limits for the periodic full Regge action.
In the Recognition geometry stack this is the discrete flat-space matching condition in $D=3$ Regge calculus: curvature (deficit) vanishes identically on the flat conformal background before second-order and continuum analysis proceed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.