SimplicialHingeData
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.