pith. sign in
module module high

IndisputableMonolith.Geometry.DeficitLinearization

show as:
view Lean formalization →

The module defines structures for flat-background simplicial complexes with finite hinges and edges obeying the flat-sum condition on dihedral angles. Researchers discharging the Regge deficit linearization hypothesis in the Recognition Science program cite it as the Phase C4 assembly of geometric primitives. It supplies the perturbation and certification objects that close the linearization step before downstream composition.

claimA flat-background simplicial complex consists of finitely many hinges indexed by $n_H$ and edges indexed by $n_E$, each hinge obeying the flat-sum condition on its dihedral angles derived from edge lengths.

background

The module sits inside the program to formalize Regge calculus for piecewise-flat complexes. It imports the Cayley-Menger determinant that encodes simplex volumes from edge lengths, the dihedral-angle construction from those lengths, and Schläfli's identity relating angle and volume variations. The supplied doc-comment states the central object: a flat-background simplicial complex with finitely many hinges and edges satisfying the flat-sum condition.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the linearization definitions that the SimplicialDeficitDischarge module composes to prove the paper's Theorem 5.1 on the field-curvature identity. It completes Phase C4 of the discharge sequence for the ReggeDeficitLinearizationHypothesis on general simplicial complexes.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (8)