flatDeficitZeroTarget_iff_globalZeroDeficitAtFlat
plain-language theorem explainer
For any finite 3D Regge triangulation, the flat-deficit zero target is definitionally the same as global zero deficit at the flat potential. Gravity and Regge-smoothness authors cite it when wiring flat-configuration inputs into the physical six-tet cubic Dirichlet model. The proof is pure reflexivity: both sides expand to the same edgewise vanishing of deficit angle under zero potential.
Claim. For every finite 3D Regge triangulation $K$, the flat-deficit zero target on $K$ holds if and only if $K$ has global zero deficit at the flat (zero) potential: for every edge $e$, the deficit angle of $K$ at $e$ under the zero potential vanishes.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not give the physical Dirichlet equality for free; it only assembles the geometric inputs.
A Triangulation3D is a finite 3D Regge complex: vertex/edge/tet counts plus incidence and nondegenerate squared-edge data on each tetrahedron. The deficit at a hinge is $2\pi$ minus the sum of incident dihedral angles. Both the flat-deficit zero target and global zero-deficit-at-flat assert that, under the zero potential, every edge has vanishing deficit angle. Upstream smoothness docs stress that this is an assembled-triangulation condition, not a consequence of local nondegeneracy of individual tets.
The flat-deficit zero target is the exact geometric input that normalizes the flat Regge action to zero; the remaining periodic-Freudenthal task is to prove it from the canonical flat geometry.
proof idea
One-line reflexivity. The two propositions are definitionally identical (both are $\forall e,,\mathrm{deficitAngle},K,(\mathrm{zeroPotential},K),e = 0$), so rfl closes the biconditional with no lemmas or rewriting.
why it matters
This bridge lets the module speak in either vocabulary: the gravity-side flat-deficit target or the smoothness package's global zero-deficit input. Downstream, globalZeroDeficitAtFlat_of_angleSum applies the forward direction after reducing an angle-sum hypothesis to the flat-deficit target, feeding the smoothness layer. CanonicalPeriodicFlatConfigurationInputs then requires global zero deficit at the flat potential (together with a local analytic chart) as the remaining data for a canonical periodic flat configuration; smoothness itself is already built from the local chart.
In the broader RS gravity stack this is bookkeeping on the Regge side of the six-tet cubic Dirichlet instance, not a forcing-chain step (T5–T8). It closes a naming gap so the periodic Freudenthal scaffold can discharge the flat-background normalization without duplicate hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.