IndisputableMonolith.Geometry.DeficitLinearization
Phase C4 of the Regge linearization program: on a flat-background simplicial complex, first-order edge-length perturbations produce a linearized deficit that vanishes identically. Anyone discharging the Regge deficit linearization hypothesis cites the certificate and the vanishing lemma. The argument assembles Cayley–Menger volumes, dihedral angles, and Schläfli into a first-order identity on well-shaped data.
claimOn a flat simplicial complex (finitely many hinges and edges, each hinge summing to a flat angle), an edge-length perturbation has linearized deficit $\delta\varepsilon = \sum_h c_h\,\delta\ell$ with coefficients from the first variation of dihedral angles. For well-shaped data the linearized Regge deficit vanishes: $\delta\varepsilon \equiv 0$ to first order.
background
Regge calculus assigns curvature to a piecewise-flat complex via angle deficits at hinges (codimension-2 faces). The paper's field-curvature identity needs a linearization hypothesis: on a flat background, the first variation of total deficit under edge-length changes is zero. This module packages that statement for general finite complexes.
Upstream geometry is already in place. Cayley–Menger (Phase C1) recovers simplex volumes from edge lengths. Dihedral angles (Phase C2) are read off that metric data. Schläfli's identity (Phase C3) relates volume variation to dihedral variations: $\sum_e \ell_e,d\theta_e = c_n,dV$ in each simplex. The flat-background complex here is finite: hinges indexed by $\mathrm{Fin},n_H$, edges by $\mathrm{Fin},n_E$, each hinge obeying the flat-sum condition (total angle $2\pi$ or $\pi$ as appropriate).
proof idea
The module is definitional scaffolding plus one vanishing theorem, not a long tactic development. It introduces the flat complex carrier, edge perturbations, and linearization coefficients (first derivatives of hinge angles w.r.t. edge lengths). The linearized deficit is the corresponding contraction. Well-shaped data packages nondegeneracy so the derivatives exist. The key lemma linear_regge_vanishes then applies Schläfli simplex-by-simplex and cancels against the flat-sum condition at each hinge, yielding first-order vanishing. A certificate bundle packages the hypotheses for downstream discharge.
why it matters in Recognition Science
This is Phase C4 in the chain that proves the paper's Theorem 5.1 (field-curvature identity) inside Lean. Downstream, SimplicialDeficitDischarge (Phase C5) "composes Phases C1–C4 into a general simplicial discharge of ReggeDeficitLinearizationHypothesis." Without a clean linearization-on-flat statement, the ledger cannot equate curvature flux to recognition cost at linear order. In the broader Recognition framework the result sits in the geometry layer that feeds simplicial ledger identities, not in the T0–T8 forcing chain itself; it is infrastructure for matching discrete curvature to the continuum side of the ledger.
scope and limits
- Does not treat curved backgrounds; only flat-sum hinges.
- Does not prove higher-order (quadratic) deficit expansions.
- Does not fix continuum dimension or force D = 3; pure simplicial combinatorics.
- Does not discharge ReggeDeficitLinearizationHypothesis alone; Phase C5 composes the certificate.
- Does not address infinite or non-well-shaped complexes.