deficit_angle
plain-language theorem explainer
The deficit angle at a hinge is defined as twice pi minus the sum of its dihedral angles. Discrete gravity researchers modeling Regge calculus on the RS lattice cite this when building the action or extracting local curvature from simplicial data. It is implemented as a direct one-line subtraction that matches the classical Regge formula.
Claim. Let $h$ be a hinge data structure with positive area and list of dihedral angles $θ_i$. The deficit angle is $2π - ∑ θ_i$.
background
The ReggeCalculus module formalizes exact Regge calculus for the RS discrete gravity programme, replacing the linearized deficit ansatz with the full nonlinear machinery on a Z^3 × Z lattice whose edge lengths come from the J-cost defect field. HingeData packages the hinge area together with the list of dihedral angles from all simplices meeting at that codimension-2 face; the deficit then concentrates curvature at the hinge and enters the Regge action as area times deficit. Upstream geometry supplies the identical formula: DihedralAngle.deficit computes 2π minus the sum of thetas, and Schlaefli.deficit delegates to it for simplicial hinges.
proof idea
This is a one-line definition that subtracts the summed dihedral angles from 2π, directly encoding the standard Regge deficit formula.
why it matters
This definition supplies the deficit angle used to construct HingeContribution and regge_action_from_hinges, to derive curvature_from_deficit, and to state discrete_conservation. It realizes the full nonlinear Regge action in place of Assumption A2, connecting to the RS framework through the phi-ladder edge lengths and the eight-tick octave. It closes scaffolding for the discrete Bianchi identity and the lattice Gauss-Bonnet relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.