deficitLinearizationCert
plain-language theorem explainer
The declaration certifies that the first-order term in the Regge action vanishes for edge perturbations around a flat simplicial complex once Schläfli's identity is imposed. Workers on discretized gravity or Regge calculus would cite it when confirming that the linear contribution to the action is identically zero. The proof is a one-line wrapper that supplies the already-established linear_regge_vanishes theorem to the DeficitLinearizationCert structure.
Claim. The first-order variation of the Regge action vanishes: for well-shaped data $W$ on a flat simplicial complex with $n_H$ hinges and $n_E$ edges together with an edge-length perturbation field $η$, one has $∑_h A_h · δ̃_h(η) = 0$, where $A_h$ is the area of hinge $h$ and $δ̃_h$ is the linearized deficit angle at that hinge.
background
The module packages the Piran-Williams linearization of the Regge deficit angle around a flat simplicial complex (Phase C4). Around a flat background with edge lengths $a$, a small perturbation $η_e$ produces a first-order deficit $δ_h({a + η_e}) = ∑_e (∂δ_h/∂L_e)|_flat · η_e + O(η²)$. The structure DeficitLinearizationCert records that the linear piece of the total action $S_Regge = ∑_h A_h · δ_h$ is identically zero when Schläfli's identity holds. WellShapedData supplies the complex, its hinges, areas, and the linearization coefficients; EdgePerturbation supplies the field $η$; linearizedDeficit assembles the first-order contribution at each hinge.
proof idea
One-line wrapper that applies linear_regge_vanishes to populate the linear_vanishes field of DeficitLinearizationCert.
why it matters
The certificate records the vanishing of the linear term required before the quadratic action can be extracted in Phase C5. It rests on the already-proved linear_regge_vanishes theorem, which itself uses Schläfli's identity (Phase C3) together with flatness. In the Recognition framework this step closes the linearization hypothesis for general simplicial complexes before the geometry module is used by mass and topology constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.