deficit
plain-language theorem explainer
Deficit at a hinge is 2π minus the sum of its dihedral angles. Discrete gravity and Regge calculus workers cite it when reducing the action variation via Schläfli's identity to a single curvature term. The definition is a one-line wrapper delegating to the dihedral-angle deficit on the angle list stored inside the hinge data structure.
Claim. For simplicial hinge data consisting of a nonnegative area and a list of dihedral angles θ_i, the deficit equals 2π − ∑ θ_i.
background
The module records Schläfli's identity for piecewise-flat simplicial complexes in Phase C3 of the program to discharge the Regge deficit linearization hypothesis. SimplicialHingeData abstracts each hinge by its area (a nonnegative real) and the list of dihedral angles from the top simplices that meet at the hinge; the total dihedral angle is their sum and the deficit is 2π minus that sum. The upstream DihedralAngle.deficit is defined as 2 * Real.pi - sumThetas ds, which matches the hinge-level curvature term exactly.
proof idea
The definition is a one-line wrapper that applies DihedralAngle.deficit to the dihedrals field of the input hinge data.
why it matters
This supplies the angular deficit term used in downstream derivations of the fine-structure constant and the lambda recurrence. It is invoked by faces_per_vertex, angular_deficit_per_vertex, passive_edges_at_D3, and lambda_rec_is_forced, as well as by JPositivityUniversalityCert. It supplies the hinge curvature that lets Schläfli's identity collapse the Regge variation δS/δL_e to a single sum over areas times deficits, consistent with the D=3 forcing chain and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.