IndisputableMonolith.Geometry.DeficitLinearization
This module defines the flat-background simplicial complex that serves as the setting for linearizing Regge deficits on hinges and edges. Workers on simplicial gravity and the Regge calculus cite it when assembling the linearization hypothesis for discharge. It collects the Cayley-Menger, dihedral-angle, and Schläfli machinery into one interface without performing the linearization itself.
claimA flat-background simplicial complex consists of finitely many hinges indexed by $Fin n_H$ and edges indexed by $Fin n_E$, with each hinge obeying the flat-sum condition on its dihedral angles.
background
The module sits inside the Phase C program that discharges the Regge deficit linearization hypothesis on general simplicial complexes. It imports the Cayley-Menger determinant (volume from edge lengths), the dihedral-angle construction from those lengths, and Schläfli's identity for piecewise-flat complexes. The central object is the flat-background simplicial complex whose hinges satisfy the flat-sum condition, providing the reference geometry against which perturbations are measured.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
It supplies the core definitions required by SimplicialDeficitDischarge (Phase C5), which composes Phases C1–C4 to obtain a general simplicial discharge of the ReggeDeficitLinearizationHypothesis and thereby a Lean statement of the paper's Theorem 5.1 (field-curvature identity).
scope and limits
- Does not treat curved or non-flat background geometries.
- Does not derive explicit linearization coefficients or perform the deficit expansion.
- Does not prove the full discharge of the linearization hypothesis.
- Does not address higher-dimensional or non-simplicial complexes.