FlatDeficitZeroTarget
plain-language theorem explainer
For a 3D triangulation, the flat-deficit zero target asserts that every edge has vanishing deficit angle at the zero potential. Anyone normalizing the Regge action on a flat background, or packaging a FlatConfiguration for the periodic Freudenthal torus, cites this predicate. It is a Prop definition, not a proved statement: the body is the universal quantification over edges of deficitAngle = 0.
Claim. Given a 3-dimensional triangulation $K$, the flat-deficit zero target is the proposition that for every edge $e$ of $K$, the deficit angle of $e$ evaluated at the zero potential configuration equals zero: $\delta_e(0)=0$.
background
In Regge calculus the curvature of a piecewise-flat 3-complex is concentrated on edges as deficit angles: the amount by which the sum of incident dihedral angles fails to equal $2\pi$. The zero potential is the reference assignment of edge lengths (or metric data) corresponding to the undeformed flat background.
This module packages theorem obligations that connect an encoded periodic Freudenthal torus to the physical six-tet cubic Dirichlet model. It does not assert the physical Dirichlet equality for free; it isolates the exact geometric inputs required. The flat-deficit zero target is one such input: the condition that the background is metrically flat at every edge.
An equivalent angle-sum form (recorded in a sibling comment) rewrites the same condition as: incident local dihedral-angle contributions around each global edge sum to $2\pi$. Downstream constructions reduce the target to that sum when convenient.
proof idea
Definitional, not a proof. The body is the single Prop $\forall e,;\mathrm{deficitAngle}(K,,0,,e)=0$, i.e. vanishing deficit at the zero potential on every edge index. No tactics or lemmas are applied; consumers discharge or assume this Prop as a hypothesis.
why it matters
This predicate is the exact geometric input needed to normalize the flat Regge action to zero on the canonical periodic Freudenthal background. Downstream, canonicalPeriodicFlatDeficitZeroTarget and its angle-sum reduction prove the target for the encoded torus; CanonicalPeriodicFlatConfigurationInputs packages it with a local analytic chart as the remaining data for a FlatConfiguration.
From there it feeds action-normalization theorems (canonicalPeriodicReggeAction_zeroPotential_eq_zero_of_flatDeficit / _of_flatConfiguration) and the full nonlinear Regge-to-Dirichlet continuum limits under variable-weighted finite probes. In the Recognition gravity stack this closes the flat-background side of the six-tet cubic Dirichlet instance: without zero deficits at the reference potential, the Regge action cannot be gauged to vanish and the Dirichlet-energy identification fails to start from a clean zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.