IndisputableMonolith.Geometry.Schlaefli
This module supplies abstract edge-length data for finite simplicial complexes indexed by Fin nE together with the Schlaefli identity. Researchers linearizing Regge deficits or reducing the Regge action in discrete gravity would cite it as Phase C3 infrastructure. The module consists of data definitions and identities assembled from the imported Cayley-Menger and DihedralAngle modules.
claimAbstract edge-length assignment $\ell : \mathrm{Fin}\, n_E \to \mathbb{R}_{>0}$ for a simplicial complex, together with the Schläfli identity relating edge variations to dihedral-angle differentials.
background
The module imports CayleyMenger, which encodes the volume of an n-simplex from its C(n+1,2) edge lengths via the Cayley-Menger determinant, and DihedralAngle, which extracts dihedral angles at edges and 2-faces from that data. Both are described as phases C1 and C2 toward discharging the ReggeDeficitLinearizationHypothesis.
It introduces SimplicialEdgeData and related structures (totalTheta, deficit, SchlaefliIdentity) that treat edge lengths as an abstract finite-indexed map. The local setting is the geometry layer preparing simplicial deficit linearization for the Recognition Science program.
proof idea
This is a definition module, no proofs. It collects edge-data structures, states the Schlaefli identity, and records auxiliary facts such as schlaefli_kills_dtheta and totalDeficit_flat that follow directly from the imported volume and angle constructions.
why it matters in Recognition Science
The module feeds SimplicialDeficitDischarge (Phase C5, proving the paper's Theorem 5.1 as a field-curvature identity), DeficitLinearization (Phase C4, packaging the Piran-Williams linearization), and WeakFieldConformalRegge (algebraic core of the Regge-action reduction under conformal edge ansatz). It supplies the missing geometric identity between C2 and C4.
scope and limits
- Does not treat infinite or non-finite edge sets.
- Does not compute explicit volumes or angles for concrete complexes.
- Does not incorporate curvature sources or matter terms.
- Does not extend the identity to non-simplicial complexes.