pith. machine review for the scientific record. sign in
def definition def or abbrev high

deficit

show as:
view Lean formalization →

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π.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 134def deficit (ds : List DihedralAngleData) : ℝ :=

proof body

Definition body.

 135  2 * Real.pi - sumThetas ds
 136
 137/-- At a flat hinge, the deficit is zero. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (8)

Lean names referenced from this declaration's body.