totalDeficit_flat
plain-language theorem explainer
When every hinge in a finite collection satisfies the flat-sum condition on its dihedral angles, the total deficit vanishes. Regge calculus and piecewise-flat geometry work cites this to establish the zero baseline before linearizing the action via Schläfli's identity. The proof unfolds the sum definition, applies Finset.sum_eq_zero, invokes the per-hinge zero-deficit lemma from the DihedralAngle module on each term, and finishes with ring.
Claim. Let $H$ be a finite collection of hinges, each with area $A_h$ and dihedral angles $d_h$. If for every $h$ the sum of angles in $d_h$ equals $2π$, then $∑_h A_h (2π - ∑ θ in d_h) = 0$.
background
The Schläfli module formalizes Schläfli's identity for piecewise-flat simplicial complexes as Phase C3 toward discharging the Regge deficit linearization hypothesis. SimplicialHingeData packages each hinge with its area and the list of dihedral angles from incident top simplices; the local deficit is then 2π minus the sum of those angles. totalDeficit is the sum over hinges of area times local deficit. FlatSumCondition is the predicate that this sum of angles equals exactly 2π. The upstream DihedralAngle module supplies both the deficit definition and the theorem deficit_eq_zero_of_flat that converts the flat-sum condition into a zero deficit.
proof idea
Unfold totalDeficit to expose the Finset sum, then apply sum_eq_zero. For each hinge index, unfold the local deficit and apply DihedralAngle.deficit_eq_zero_of_flat to the supplied flat condition on that hinge's dihedrals. Ring closes the resulting zero term.
why it matters
This supplies the flat_total_zero field of the SchlaefliCert record, which certifies the Phase C3 results for the Regge action. It anchors the flat limit case before the full Schläfli identity reduces the variation of the Regge action to a single term. The result sits inside the geometry layer that supports the eight-tick octave and D=3 spatial structure in the broader forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.