deficit_eq
plain-language theorem explainer
deficit_eq asserts that the Regge deficit at a hinge equals 2π minus the summed dihedral angles around that hinge. Regge calculus workers cite it when relating curvature defects to angle sums in piecewise-flat triangulations. The proof is a one-line reflexivity step that matches the definition of deficit directly to the totalTheta expression.
Claim. For simplicial hinge data $h$, the deficit satisfies $h.deficit = 2π - h.totalTheta$.
background
SimplicialHingeData is a record holding the hinge area (nonnegative real) and a list of dihedral angles contributed by each top simplex sharing the hinge. totalTheta sums those angles; deficit is then defined as 2π minus the sum. This module develops the geometry for Schläfli's identity on piecewise-flat simplicial complexes, the step that reduces the Regge action variation from two terms to one.
proof idea
The proof is a one-line reflexivity that unfolds the definition of deficit inside SimplicialHingeData and matches it exactly to 2π minus totalTheta.
why it matters
The equality supplies the basic relation between deficit and total dihedral angle before Schläfli's identity is stated later in the module. It advances Phase C3 of the program to discharge the Regge deficit linearization hypothesis, allowing the variation of the Regge action to collapse to a single term that vanishes on-shell. The surrounding module imports Cayley-Menger and DihedralAngle to embed the construction inside the Recognition Science ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.