DeficitLinearizationCert
plain-language theorem explainer
The DeficitLinearizationCert structure certifies that the first-order Regge action vanishes for any edge perturbation around a flat simplicial complex. Discrete gravity researchers linearizing the Regge action would cite it to establish that the leading term is quadratic. The structure is populated by a direct application of the already-proved linear_regge_vanishes result.
Claim. Let $W$ be a well-shaped data package (flat simplicial complex, linearization coefficients, and Schläfli identity). Let $η$ be an edge-length perturbation. The certificate asserts that for all such $W$ and $η$, $∑_h A_h · δ_h^{lin}(η) = 0$, where $A_h$ is the area of hinge $h$ and $δ_h^{lin}$ is the first-order deficit angle at $h$.
background
This module packages the Piran-Williams linearization of the Regge deficit around a flat simplicial complex. WellShapedData bundles a FlatSimplicialComplex, the matrix of partial derivatives of deficit angles with respect to edge lengths, and the Schläfli identity enforcing consistency of those derivatives. EdgePerturbation supplies a vector of small changes to the edge lengths. The linearized deficit at a hinge is the negative sum over edges of the derivative coefficient times the perturbation component.
proof idea
The structure is a one-line wrapper that directly invokes the proved linear_regge_vanishes theorem to inhabit the linear_vanishes field.
why it matters
This certificate is used by the deficitLinearizationCert theorem to package the vanishing result. It completes the linearization step in the Piran-Williams approach, ensuring the first-order Regge action vanishes by Schläfli's identity so the leading term is quadratic. This supplies the sum rule needed for Phase C4 of discharging the Regge deficit linearization hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.