structure definition def or abbrev

`HingeData`

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

formal statement (Lean)

 115structure HingeData where
 116  area : ℝ
 117  dihedral_angles : List ℝ
 118  area_pos : 0 < area
 119
 120/-- The deficit angle at a hinge: 2*pi - sum of dihedral angles. -/

used by (10)

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

discrete_conservation in IndisputableMonolith.Gravity.DiscreteBianchi decl_use
deficit_angle in IndisputableMonolith.Gravity.ReggeCalculus 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
schlafli_identity in IndisputableMonolith.Gravity.ReggeCalculus decl_use

depends on (7)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
deficit in IndisputableMonolith.Geometry.DihedralAngle decl_use
deficit in IndisputableMonolith.Geometry.Schlaefli decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use