deficitLinearizationCert
The declaration populates the DeficitLinearizationCert structure by exhibiting the vanishing of the summed first-order Regge action term. Researchers linearizing Regge calculus on simplicial complexes cite it to confirm cancellation around flat backgrounds under the conformal perturbation ansatz. The proof is a direct one-line term that applies the already-proved linear_regge_vanishes result to arbitrary well-shaped data and edge perturbations.
claimThe certificate asserts that for all natural numbers $n_H$ and $n_E$, every well-shaped data structure $W$ on a complex with $n_H$ hinges and $n_E$ edges, and every edge-length perturbation field $η$, the sum over hinges $h$ of (hinge area times linearized deficit) vanishes: $∑_h A_h · δ_h^{lin}(η) = 0$.
background
The module packages the Piran-Williams linearization of the Regge deficit angle around a flat simplicial complex. Around a background with all edge lengths $a$ (hence all deficits zero), a small perturbation $η_e$ induces the first-order deficit $δ_h({a + η_e}) = ∑e (∂δ_h/∂L_e)|{flat} · η_e + O(η²)$, with coefficients fixed by the complex combinatorics and vertex-angle measure. WellShapedData packages the complex, its linearization coefficients, and the sum-rule requirement that follows from Schläfli's identity combined with flatness.
proof idea
The proof is a one-line term that constructs the certificate by applying the linear_regge_vanishes theorem to the supplied well-shaped data $W$ and perturbation $η$.
why it matters in Recognition Science
This declaration supplies the certificate required for Phase C4 of the program to discharge the Regge deficit linearization hypothesis on general simplicial complexes. It records the vanishing of the linear term in the Regge action $S_{Regge} = ∑_h A_h δ_h$, which is needed so that the action becomes quadratic in the ε-field under the conformal ansatz $η_e = a · (ε_i + ε_j)/2$. The module documentation states that this cancellation follows from Schläfli's identity together with flatness and is a prerequisite for the quadratic action in Phase C5.
scope and limits
- Does not prove existence of the linearization coefficients for arbitrary complexes.
- Does not compute explicit coefficient values beyond the cubic-lattice case already treated elsewhere.
- Does not address quadratic or higher-order terms in the deficit expansion.
- Does not apply when the background simplicial complex is not flat.
formal statement (Lean)
188theorem deficitLinearizationCert : DeficitLinearizationCert where
189 linear_vanishes := fun W η => linear_regge_vanishes W η
proof body
Term-mode proof.
190
191end
192
193end DeficitLinearization
194end Geometry
195end IndisputableMonolith