ZeroDeficitAtFlat
plain-language theorem explainer
Names the discrete vacuum condition for a 3D Regge triangulation: every global edge has vanishing deficit angle at the zero conformal potential. Gravity and discrete-geometry arguments cite it as one side of the criticality ↔ vacuum equivalence. It is a pure Prop abbreviation, not a proved statement.
Claim. For a finite 3D Regge triangulation $K$, the predicate "zero deficit at flat" holds when, for every global edge $e$, the Regge deficit angle of $e$ evaluated at the zero conformal vertex potential equals zero: $\delta_e(0)=0$.
background
This module treats the discrete vacuum Einstein equation for the nonlinear conformal Regge action. In continuum language the vacuum equation is vanishing Ricci curvature; in Regge calculus it is vanishing deficit at every hinge (here, every global edge).
A Triangulation3D packages finite vertex/edge/tetrahedron counts with incidence data and nondegenerate squared-edge lengths on each tetrahedron. The conformal ansatz assigns a real potential to each vertex; the zero potential is the constant-zero assignment. The deficit angle at a global edge is $2\pi$ minus the sum of local dihedral contributions from incident tetrahedra.
The module records the exact equivalence between criticality of the nonlinear action at flat geometry and this zero-deficit predicate as a named input structure, rather than an axiom: the forward direction uses Schläfli cancellation, the reverse needs incidence-rank nondegeneracy.
proof idea
Definition only: the body is the universal quantification that every edge index of $K$ has deficitAngle equal to zero when the potential is zeroPotential. No tactics, no lemmas.
why it matters
This predicate is one half of the Phase-F discrete vacuum Einstein equivalence. The structure DiscreteVacuumEinsteinInput packages the biconditional CriticalAtFlat ↔ ZeroDeficitAtFlat; the theorem reggeAction_critical_iff_zero_deficit simply projects that field. Downstream reverse implications (zero_deficit_of_critical_of_variationFormula_of_separating, and the restricted-incidence variant) conclude this predicate from criticality plus a first-variation formula and a separating/rank hypothesis on the conformal edge-incidence map. The forward fact zero_deficit_of_flat_configuration shows every flat configuration satisfies it. In the Recognition gravity stack this is the discrete stand-in for the vacuum Einstein equation on the nonlinear Regge action, feeding incidence-recovery and restricted-subspace arguments rather than continuum curvature identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.