DeficitLinearizationCert
plain-language theorem explainer
DeficitLinearizationCert packages the assertion that the first-order Regge action sums to zero for any well-shaped flat simplicial complex and any edge-length perturbation. Lattice-gravity researchers cite it to confirm the linear term drops out before expanding to quadratic order in fluctuations. The structure is directly inhabited by the already-proved linear_regge_vanishes theorem.
Claim. Let $W$ be a well-shaped flat simplicial complex equipped with linearization coefficients satisfying Schläfli's identity, and let $η$ be an arbitrary edge-length perturbation. Then $∑_h A_h · δ_h^{(1)}(η) = 0$, where $A_h$ is the area of hinge $h$ and $δ_h^{(1)}$ denotes the first-order (linearized) deficit angle at that hinge.
background
WellShapedData bundles a FlatSimplicialComplex, its LinearizationCoefficients (the matrix of partial derivatives of deficit angles with respect to edge lengths at the flat point), and a SchlaefliIdentity witness. EdgePerturbation simply supplies a map η : Fin nE → ℝ giving the first-order length shifts. The auxiliary definition linearizedDeficit computes, for each hinge, the contraction of those coefficients against η (with an overall minus sign). The module implements the Piran-Williams (1986) linearization of the Regge action around a flat background, Phase C4 of the program to discharge the linearization hypothesis on general simplicial complexes.
proof idea
The structure itself is a pure packaging definition with no proof body. It is populated by the one-line wrapper deficitLinearizationCert, which supplies the field linear_vanishes by direct appeal to the theorem linear_regge_vanishes. That theorem unfolds the linearized deficit, reorders the double sum, and invokes Schläfli's identity edge-by-edge to obtain exact cancellation.
why it matters
The structure supplies the certificate required by deficitLinearizationCert, which in turn closes the linear-vanishing step needed for Phase C5 (quadratic Regge action). It directly implements the claim in the module documentation that “the linear term vanishes by Schläfli's identity combined with flatness,” thereby justifying the passage from linear to quadratic order in the ε-field. The result sits inside the broader Recognition Science effort to derive the Regge action from the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.