IndisputableMonolith.Geometry.DeficitLinearization
Linearizes the Regge curvature deficit about a flat simplicial background. Defines flat complexes, edge perturbations, and the first-order deficit form, then proves that linear term vanishes on well-shaped data. Downstream simplicial-ledger discharge of the field-curvature identity imports this module as Phase C4. The argument assembles Cayley-Menger volumes, dihedral angles, and Schläfli's identity into a first-order identity.
claimOn a flat simplicial complex with finitely many hinges and edges, each hinge obeying the flat-sum condition, the first-order change of the Regge deficit under an edge-length perturbation is a linear form in the induced dihedral variations. That linear form vanishes identically on well-shaped background data.
background
Regge calculus encodes curvature on a piecewise-flat simplicial complex by deficit angles at hinges (codimension-2 faces): the deficit is $2\pi$ minus the sum of dihedral angles meeting there. On a flat background every hinge deficit is zero. The Recognition program needs the first-order response of those deficits when edge lengths are perturbed, so that the continuum curvature identity can be recovered from a discrete ledger.
Upstream modules supply the geometric ingredients. Cayley-Menger determinants convert edge lengths into simplex volumes (Phase C1). Dihedral angles at edges and 2-faces are then extracted from that CM data (Phase C2). Schläfli's identity relates volume variations to edge lengths and dihedral angles on a piecewise-flat complex (Phase C3).
This module packages those pieces into the linearization layer: a flat complex structure, an edge-perturbation type, coefficient data for the linear form, a well-shapedness predicate, and the vanishing statement for the linearized deficit.
proof idea
Definition-heavy module with one core vanishing theorem and a bundled certificate. FlatSimplicialComplex records finite hinge and edge index types together with the flat-sum condition at each hinge. EdgePerturbation and LinearizationCoefficients supply the first-order data; linearizedDeficit evaluates the resulting linear form. WellShapedData packages the geometric hypotheses needed for the expansion to be valid. The theorem linear_regge_vanishes then shows the linearized deficit is identically zero on that data, by feeding Schläfli and the flat-sum condition into the first-order expansion. DeficitLinearizationCert / deficitLinearizationCert wrap the result for downstream discharge.
why it matters in Recognition Science
Phase C4 of the program that discharges ReggeDeficitLinearizationHypothesis on general simplicial complexes. The sole downstream consumer is SimplicialDeficitDischarge (Phase C5), which composes C1-C4 to prove the paper's Theorem 5.1 (field-curvature identity) as a Lean theorem. Without a clean linearization-and-vanishing step, the discrete ledger cannot pass from combinatorial deficit bookkeeping to the continuum curvature term required by Recognition Science. The module therefore sits on the critical path from elementary simplex geometry to the forcing-chain geometry that underwrites $D=3$ and the eight-tick structure.
scope and limits
- Does not treat curved (non-flat) backgrounds or second-order deficit terms.
- Does not derive continuum Einstein equations; only the discrete linear identity.
- Does not fix a concrete mesh or dimension beyond the abstract finite-index setup.
- Does not discharge ReggeDeficitLinearizationHypothesis alone; needs Phase C5 composition.
- Does not address non-well-shaped or degenerate simplices.