SimplicialHingeData
SimplicialHingeData records the area of a hinge together with the list of dihedral angles from adjacent top simplices. Workers on Regge calculus and discrete gravity cite this record when assembling piecewise-flat complexes for deficit calculations. The declaration is a pure structure definition with a non-negativity constraint on area and no proof obligations.
claimA hinge is specified by a non-negative real area $A$ and a finite list of dihedral angle data, where each entry is a cosine value in $[-1,1]$.
background
In the Schläfli module a hinge is an $(n-2)$-dimensional face shared by several $n$-simplices. SimplicialHingeData collects the hinge area $A_h$ and the list of dihedral angles at that hinge. DihedralAngleData supplies the basic record holding a cosine in $[-1,1]$, from which the angle is recovered by arccos; the same record appears in both the local DihedralAngle and the ReggeCalculus modules. The surrounding module formalizes Schläfli's identity for piecewise-flat simplicial complexes, the identity that reduces the Regge variation to a single deficit term.
proof idea
The declaration is a pure structure definition introducing the three fields area, area_nonneg and dihedrals. No lemmas are invoked and no tactics are used; the structure simply packages data for downstream definitions such as deficit and totalTheta.
why it matters in Recognition Science
This structure is the basic data carrier for Phase C3 of the Regge deficit linearization program. It is used directly by FlatSimplicialComplex to index hinges and by SchlaefliCert to certify that the total deficit vanishes under the flat-sum condition. It also supplies the hinge data required by the SchlaefliIdentity definition and the schlaefli_kills_dtheta theorem that eliminates the $A_h dθ/dL$ term in the Regge equations.
scope and limits
- Does not derive dihedral angles from edge lengths via Cayley-Menger determinants.
- Does not impose the flat-sum condition on the list of dihedrals.
- Does not compute the deficit or total dihedral angle; those are separate definitions.
- Does not address curved or non-simplicial complexes.
formal statement (Lean)
84structure SimplicialHingeData where
85 area : ℝ
86 area_nonneg : 0 ≤ area
87 dihedrals : List DihedralAngleData
88
89namespace SimplicialHingeData
90
91/-- Sum of the dihedral angles at the hinge. -/