IndisputableMonolith.Geometry.Schlaefli
The Schlaefli module supplies abstract edge-length data for finite simplicial complexes indexed by Fin nE together with the associated Schlaefli identities. Researchers discharging the Regge deficit linearization hypothesis cite it as the bridge between volume and angle computations. The module consists of data structures and algebraic lemmas extending the imported Cayley-Menger and dihedral-angle foundations.
claimAbstract edge-length assignment $ell : Fin n_E to R_{>0}$ for a simplicial complex, together with the Schläfli identity relating variations of hinge areas $A_h$ and dihedral angles $theta_h$.
background
The module follows directly from the Cayley-Menger module, which encodes the volume of an n-simplex via the determinant of its edge lengths, and the DihedralAngle module, which extracts dihedral angles at edges and 2-faces from the same Cayley-Menger data. Both are Phase C1 and C2 of the program to discharge ReggeDeficitLinearizationHypothesis. The local theoretical setting is the preparation of geometric identities needed for deficit linearization in Regge calculus, where edge lengths determine all volumes and angles.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module is Phase C3. It feeds SimplicialDeficitDischarge (Phase C5) for the proof of the paper's Theorem 5.1 (field-curvature identity), DeficitLinearization (Phase C4) for the Piran-Williams linearization of the Regge deficit, and WeakFieldConformalRegge for the algebraic reduction of the Regge action under the conformal edge ansatz. It supplies the identity that eliminates the dtheta term in first-order deficit variations.
scope and limits
- Does not extend to infinite or continuous complexes.
- Does not compute explicit numerical deficit values.
- Does not incorporate matter sources or higher-order curvature.
- Does not address non-simplicial polyhedral complexes.