SchlaefliCert
plain-language theorem explainer
SchlaefliCert packages two properties of simplicial hinge collections: the summed area-weighted deficit vanishes whenever every hinge meets the flat-sum condition, and the area-weighted sum of dihedral derivatives vanishes for each edge once Schläfli's identity is assumed. Discrete-gravity and Regge-calculus workers cite it to justify dropping the second term in the variation of the Regge action. The structure is defined by direct bundling of the flat-total-zero and schlaefli-kills-sum fields with no additional derivation steps.
Claim. A structure whose first field asserts that for any finite set of hinges, if each hinge satisfies the flat-sum condition (total dihedral angle equals $2π$), then the total deficit functional vanishes; whose second field asserts that for any hinge collection and any matrix of dihedral-angle derivatives, Schläfli's identity (the weighted sum of areas times derivatives equals zero for every edge) implies the same weighted sum vanishes for every edge.
background
The module formalizes Schläfli's identity for piecewise-flat simplicial complexes as Phase C3 toward discharging the Regge deficit linearization hypothesis. SimplicialHingeData records an abstract hinge by its area and the list of dihedral angles contributed by the top simplices meeting it; the total dihedral at the hinge is their sum and the deficit is $2π$ minus that sum. totalDeficit sums area times deficit over the collection. FlatSumCondition requires that sum of dihedrals equals $2π$ at each hinge. DeficitDerivativeMatrix supplies the entries $dThetadL(h,e)$ intended as partial derivatives of total dihedral with respect to edge length. SchlaefliIdentity is the proposition that for every edge the sum of area times $dThetadL$ vanishes.
proof idea
The declaration is a structure definition whose two fields are stated directly. The first field is satisfied by invoking totalDeficit_flat once the flat-sum condition holds at every hinge. The second field is satisfied by invoking schlaefli_kills_dtheta once SchlaefliIdentity is assumed for the given matrix.
why it matters
schlaefliCert constructs an instance of this certificate, thereby supplying the Phase C3 step that lets the Regge variation reduce to a single term. The construction closes the linearization hypothesis on simplicial complexes and feeds the geometric side of the Recognition forcing chain (T0–T8) that forces three spatial dimensions. The module records the identity as a named hypothesis because Mathlib lacks the ambient geometric calculus needed for a first-principles proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.