DeficitLinearizationCert
DeficitLinearizationCert records the statement that the first-order Regge action vanishes identically for any well-shaped flat simplicial complex and edge perturbation. Discrete-gravity researchers cite it to justify expanding the action to quadratic order in length changes. The structure is a direct definition that records the algebraic identity obtained by reordering the double sum and applying Schläfli's identity edgewise.
claimA certificate structure asserting that for all natural numbers $n_H$, $n_E$, any well-shaped data package $W$ (flat simplicial complex equipped with linearization coefficients and Schläfli identity) and any edge perturbation map $η$, the sum $∑_h A_h · δ_h^{lin}(η) = 0$, where $A_h$ is the area of hinge $h$ and $δ_h^{lin}(η)$ is the first-order deficit angle induced at that hinge.
background
The module develops the Piran-Williams linearization of the Regge deficit angle around a flat background. Well-shaped data packages a flat simplicial complex, the matrix of partial derivatives of deficit angles with respect to edge lengths, and the Schläfli identity satisfied by those derivatives. An edge perturbation supplies a real increment to each edge length. The upstream vanishing result establishes that the area-weighted sum of linearized deficits is zero; the certificate records this identity for downstream use. The module states that the linear part of the Regge action vanishes under Schläfli's identity, so the action becomes quadratic in the perturbation to leading order.
proof idea
The declaration is a structure definition with empty body. It is a one-line wrapper that records the proved vanishing identity as its sole field, with the identity itself obtained by moving the minus sign, swapping summation order, and invoking Schläfli's identity on each edge.
why it matters in Recognition Science
The certificate supplies the vanishing identity required by the certificate construction that immediately follows it in the module. It completes the linearization step of the Piran-Williams program, confirming that the first-order Regge action is identically zero and thereby justifying the quadratic approximation needed for the subsequent phase. The result rests on the flat-background assumption together with Schläfli's identity.
scope and limits
- Does not derive the linearization coefficients for an arbitrary complex.
- Does not address non-flat backgrounds or higher-order terms.
- Does not supply explicit coefficients for concrete lattices.
- Does not treat the full nonlinear Regge action.
formal statement (Lean)
181structure DeficitLinearizationCert where
182 linear_vanishes : ∀ {nH nE : ℕ}
183 (W : WellShapedData nH nE) (η : EdgePerturbation nE),
184 (∑ h : Fin nH, (W.complex.hinges h).area *
185 linearizedDeficit W.coeffs η h) = 0
186
187/-- The certificate is inhabited by the proved `linear_regge_vanishes`. -/