DeficitDerivativeMatrix
plain-language theorem explainer
A structure that records the matrix of partial derivatives of total dihedral angles at hinges with respect to edge lengths in a simplicial complex. Workers on discrete gravity and Regge calculus cite this when setting up linearization of the action around flat backgrounds. It is introduced as a bare record type with the single field dThetadL mapping hinge-edge index pairs to reals.
Claim. Let $n_H, n_E$ be natural numbers. A DeficitDerivativeMatrix consists of a function $dThetadL : Fin(n_H) → Fin(n_E) → ℝ$ whose entry at hinge $h$ and edge $e$ is the partial derivative of the total dihedral angle at $h$ with respect to the length of edge $e$.
background
The module develops the geometry of piecewise-flat simplicial complexes as Phase C3 toward discharging the Regge deficit linearization hypothesis. A hinge $h$ carries an area $A_h$ and a total dihedral angle obtained by summing the dihedral angles of all top simplices incident on $h$; these angles are expressed via the Cayley-Menger determinant from the edge lengths. Schläfli's identity asserts that the weighted sum over hinges of area times the partial derivative of total angle with respect to each edge length vanishes identically.
proof idea
This is a structure definition that directly packages the field dThetadL with no computation or proof obligations.
why it matters
It supplies the type for the derivative matrix that appears in SchlaefliIdentity and is extended by LinearizationCoefficients. The identity then feeds SchlaefliCert and the theorem schlaefli_kills_dtheta, which removes the second term in the variation of the Regge action. This step recovers the standard Regge equations from the Recognition Science simplicial ledger and continuum bridge, closing the local identity required for the piecewise-flat reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.