def definition def or abbrev

`deficit_angle`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 121noncomputable def deficit_angle (h : HingeData) : ℝ :=

Definition body.

 122  2 * Real.pi - h.dihedral_angles.sum
 123
 124/-- For a flat configuration, all hinges have zero deficit. -/

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

HingeContribution in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
regge_action_from_hinges in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
discrete_conservation in IndisputableMonolith.Gravity.DiscreteBianchi decl_use
curvature_from_deficit in IndisputableMonolith.Gravity.DiscreteCurvature decl_use
deficit_neg_of_angle_excess in IndisputableMonolith.Gravity.ReggeCalculus decl_use
deficit_pos_of_angle_deficit in IndisputableMonolith.Gravity.ReggeCalculus decl_use
flat_deficit_zero in IndisputableMonolith.Gravity.ReggeCalculus decl_use
regge_action in IndisputableMonolith.Gravity.ReggeCalculus decl_use
regge_action_flat in IndisputableMonolith.Gravity.ReggeCalculus decl_use
ReggeCalculusCert in IndisputableMonolith.Gravity.ReggeCalculus decl_use
regge_equations_statement in IndisputableMonolith.Gravity.ReggeCalculus decl_use

Lean names referenced from this declaration's body.