schlaefliCert
SchlaefliCert packages the two consequences of Schläfli's identity on piecewise-flat simplicial complexes: the total deficit vanishes on flat hinges, and the area-weighted sum of dihedral-angle derivatives with respect to each edge length is identically zero. Regge-calculus workers would cite it to justify collapsing the variation of the Regge action to a single term. The proof is a direct term-mode construction that supplies the two fields of the certificate structure from the lemmas totalDeficit_flat and schlaefli_kills_dtheta.
claimLet $K$ be a simplicial $n$-complex with hinges $h$ carrying areas $A_h$ and dihedral angles whose sum satisfies the flat condition. The Schläfli certificate asserts that the total deficit vanishes whenever every hinge meets the flat-sum condition, and that under the Schläfli identity the sum over hinges of $A_h$ times the partial derivative of the total dihedral angle at $h$ with respect to edge length $L_e$ equals zero for every edge $e$.
background
The module formalizes Schläfli's identity for piecewise-flat simplicial complexes as Phase C3 of the program to discharge the Regge deficit linearization hypothesis. SimplicialHingeData packages the edge lengths, areas, and dihedral angles for each hinge; totalDeficit sums the angular deficits over all hinges; DeficitDerivativeMatrix stores the partial derivatives of dihedral angles with respect to edge lengths; and SchlaefliIdentity encodes the classical relation that the weighted sum of those derivatives vanishes. The upstream lemma totalDeficit_flat states that if every hinge satisfies the flat-sum condition then totalDeficit hinges equals zero, while schlaefli_kills_dtheta states that under SchlaefliIdentity the sum of area times dThetadL vanishes for each edge.
proof idea
The proof is a term-mode instantiation of the SchlaefliCert structure. It supplies the flat_total_zero field by applying totalDeficit_flat to the given hinges and flatness hypothesis, and supplies the schlaefli_kills_sum field by applying schlaefli_kills_dtheta to the hinges, derivative matrix, Schläfli identity, and edge index.
why it matters in Recognition Science
This declaration completes the Phase C3 certificate in the Schläfli module, which is required to reduce the Regge action variation to a single term as described in the module documentation: the second sum in δS_Regge / δL_e vanishes by Schläfli, leaving only the first term. In the Recognition Science framework it supplies the geometric identity needed to close the forcing chain from T0 to T8, particularly the emergence of D = 3 spatial dimensions through simplicial complexes and the eight-tick octave. No downstream uses are recorded yet, so the certificate remains an interface awaiting integration into the Regge-to-Einstein-Hilbert convergence argument.
scope and limits
- Does not derive Schläfli's identity from first principles or from the Cayley-Menger determinant.
- Does not apply to curved or non-piecewise-flat complexes.
- Does not compute explicit numerical values for the derivatives or deficits.
- Does not address non-simplicial or higher-codimension hinges.
formal statement (Lean)
184theorem schlaefliCert : SchlaefliCert where
185 flat_total_zero := fun hinges hFlat => totalDeficit_flat hinges hFlat
proof body
Term-mode proof.
186 schlaefli_kills_sum := fun hinges M hS e => schlaefli_kills_dtheta hinges M hS e
187
188end
189
190end Schlaefli
191end Geometry
192end IndisputableMonolith