SchlaefliIdentity
plain-language theorem explainer
SchlaefliIdentity encodes the piecewise-flat Schläfli relation by requiring that the sum over hinges of area times the dihedral-angle derivative with respect to each edge length vanishes identically. Regge-calculus and discrete-gravity researchers cite it to reduce the first variation of the Regge action to a single term. The declaration is realized as an explicit definition of the corresponding Prop that asserts the vanishing sum for every edge.
Claim. For a finite collection of hinges indexed by $h=1,…,n_H$ with areas $A_h$ and a matrix whose entries are the partial derivatives $∂θ_h/∂L_e$ of total dihedral angles with respect to edge lengths, the identity asserts that for every edge $e$, $∑_h A_h · (∂θ_h / ∂L_e) = 0$.
background
In the Geometry.Schlaefli module the identity is formalized for piecewise-flat simplicial complexes as Phase C3 of the program to discharge the Regge deficit linearization hypothesis. SimplicialHingeData packages each hinge with a nonnegative area and a list of dihedral angles; the total dihedral at the hinge is the sum of those angles and the deficit is $2π$ minus that sum. DeficitDerivativeMatrix supplies the matrix whose $(h,e)$ entry stands for the partial of the total dihedral at hinge $h$ with respect to the length of edge $e$.
proof idea
The declaration is a direct definition that packages the classical identity as the Prop asserting the vanishing sum for every edge index $e$. No lemmas are applied; the body simply unfolds the forall-quantified equality.
why it matters
This definition supplies the hypothesis structure required by WellShapedData in DeficitLinearization and by the SchlaefliCert certificate. It fills the Phase C3 slot that reduces the Regge variation to a single term, as stated in the module documentation: the second term $Σ A · dθ/dL$ vanishes, leaving only the $∂A/∂L · δ$ piece that yields the Regge equations of motion. The identity is the piecewise-flat counterpart of the classical Schläfli relation (Schläfli 1858; Regge 1961, eq. 2.8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.