totalDeficit
plain-language theorem explainer
The total deficit sums area-weighted angular deficits over all hinges in a simplicial complex. Workers on Regge calculus and discrete gravity cite this as the integrated curvature measure. The definition is a direct finite sum of area times deficit for each hinge.
Claim. For a finite collection of hinges indexed by $nH$, each with area $A_h$ and deficit $δ_h = 2π - ∑θ$, the total deficit equals $∑_h A_h δ_h$.
background
The module develops Schläfli's identity for piecewise-flat simplicial complexes as Phase C3 toward discharging the Regge deficit linearization hypothesis. SimplicialHingeData is the structure holding each hinge's area (nonnegative real) and list of dihedral angles from incident top simplices; the total dihedral at the hinge is their sum and the deficit is 2π minus that sum. The upstream deficit definition computes exactly this local quantity as 2π minus the sum of thetas.
proof idea
One-line definition that applies the standard sum over Fin nH of the product of each hinge's area field and its deficit field.
why it matters
It supplies the total curvature functional required by SchlaefliCert (the Phase C3 certificate) and by the theorem totalDeficit_flat that shows vanishing under the flat-sum condition on every hinge. This supports the reduction step in the module doc where Schläfli's identity collapses the Regge variation to a single term set to zero. It touches the open question of proving the full identity without additional geometric-calculus axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.