zero_deficit_of_flat_configuration
plain-language theorem explainer
A flat analytic configuration of an incidence-consistent 3D Regge triangulation has vanishing deficit angle on every global edge at the zero potential. Discrete-geometry and RS gravity workers cite it when unpacking the discrete vacuum Einstein equation into its flatness half. The proof is a one-line field projection from the flat-configuration witness.
Claim. For any incidence-consistent 3-dimensional triangulation $K$, if $K$ admits a flat analytic configuration (dihedral cosines free of the arccos endpoints $\pm 1$, zero edge deficits, and the smoothness data for the nonlinear action), then the Regge deficit angle vanishes at every global edge of the flat (zero) potential: $\mathrm{deficit}(K,0;e)=0$ for all edges $e$.
background
In Regge calculus the vacuum Einstein equation is zero deficit at every hinge. This module packages that equation for the conformal nonlinear Regge action as a named equivalence rather than an axiom: the forward direction is zero deficit plus global Schläfli cancellation; the reverse needs a rank/nondegeneracy input on the conformal edge-incidence derivative.
A flat analytic configuration on an incidence-consistent triangulation $K$ packages three facts: the arccos endpoint condition at the base point (squared dihedral cosines avoid $\pm 1$), the zero-deficit flatness condition, and the smoothness data needed to invoke Taylor theory for the full nonlinear action. The target predicate asserts that the deficit angle of $K$ at the zero potential vanishes on every global edge. Classically, deficit at a hinge is $2\pi-\sum\theta$.
proof idea
One-line term proof: project the zero-deficit field of the given flat-configuration witness. No auxiliary lemmas fire; the structure already carries flatness as a named component, and the theorem re-exports that component under the module's vacuum-equation vocabulary (ZeroDeficitAtFlat).
why it matters
This is the forward half of the named discrete-vacuum-Einstein input recorded by the module: flat configurations imply zero deficit at the flat potential. The nontrivial reverse implication is the incidence-rank theorem (if all conformal first variations vanish, then each edge deficit is zero). Sibling results such as criticality at the flat potential and the first-variation formula build the variational side of the same package. In the Recognition Science gravity stack the result anchors the discrete vacuum equation on 3D triangulations, consistent with the T8 forcing of $D=3$ spatial dimensions. No downstream consumers are wired yet; the declaration exists to name the flatness half cleanly for later equivalence proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.