deficit
plain-language theorem explainer
The deficit at a hinge is defined as 2π minus the summed dihedral angles extracted from a list of DihedralAngleData. Researchers deriving the fine-structure constant or lambda recurrence from discrete curvature cite it when closing the Regge linearization step on simplicial complexes. It is a direct one-line definition that applies sumThetas and subtracts the result from 2π.
Claim. The angular deficit for a list of dihedral angle data $ds$ is $2π - ∑ θ_i$, where each $θ_i = arccos(c_i)$ and $c_i ∈ [-1,1]$ is the cosine carried by the $i$-th entry.
background
The module constructs dihedral angles at edges of simplices from Cayley-Menger minors, as Phase C2 toward discharging the Regge deficit linearization hypothesis on general simplicial complexes. DihedralAngleData is the structure holding a cosine in [-1,1] together with the derived angle θ = arccos(cosine), which is guaranteed to lie in [0,π]. sumThetas maps a list of such data to the sum of their θ values. The upstream Schlaefli.deficit re-exports the same construction on SimplicialHingeData, confirming the hinge-level curvature measure used in Regge calculus.
proof idea
One-line definition that subtracts the output of sumThetas from 2π.
why it matters
This supplies the explicit Regge deficit expression required by angular_deficit_per_vertex and faces_per_vertex in AlphaDerivation and by lambda_rec_is_forced in LambdaRecDerivation. It completes the Phase C2 setup referenced in the module doc for the simplicial discharge program, directly supporting the D=3 discrete curvature count that enters the eight-tick octave and the alpha band derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.