schlaefli_kills_dtheta
plain-language theorem explainer
Schläfli's identity forces the area-weighted sum of dihedral-angle derivatives with respect to each edge length to vanish identically. Workers in Regge calculus cite this result to drop the second term in the variation of the Regge action. The proof is a direct application of the defining universal quantifier in SchlaefliIdentity at the chosen edge.
Claim. Let $n_H$ and $n_E$ be natural numbers. Let $A_h$ be the area of hinge $h$ and let $M$ be the matrix of partial derivatives $M_{h e} = partial theta_h / partial L_e$ of the total dihedral angles. If Schläfli's identity holds, then for every edge index $e$, $sum_h A_h * (partial theta_h / partial L_e) = 0$.
background
SimplicialHingeData packages a nonnegative area together with the list of dihedral angles meeting at the hinge; totalTheta sums those angles and deficit subtracts the sum from 2 pi. DeficitDerivativeMatrix records the function dThetadL whose values are intended to be the partial derivatives of total dihedral angle with respect to edge length. SchlaefliIdentity is the proposition asserting that the area-weighted sum of these derivatives vanishes for every edge.
proof idea
The proof is a one-line wrapper that applies the hypothesis hS at the edge e. Because SchlaefliIdentity is defined as the universal quantification over edges of the vanishing sum, specializing the quantifier to e immediately yields the equality.
why it matters
The declaration is invoked inside schlaefliCert to witness that Schläfli's identity eliminates the dtheta contribution. It thereby completes the reduction step described in the module documentation: the Regge variation collapses to a single term under this hypothesis. This is Phase C3 of the program to discharge the Regge deficit linearization hypothesis on general simplicial complexes. The identity itself remains an open assumption whose first-principles proof would close the scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.