deficitLinearizationCert
plain-language theorem explainer
The theorem populates the DeficitLinearizationCert structure by exhibiting that the first-order term in the Regge action vanishes for any well-shaped simplicial complex and edge perturbation. Researchers on discrete gravity and Regge calculus would cite this as the verified certificate for the linear vanishing under Schläfli's identity. The proof is a one-line term that directly supplies the already-proved linear_regge_vanishes theorem as the witness for the structure field.
Claim. The first-order contribution to the Regge action vanishes: for any well-shaped data $W$ on a simplicial complex with $n_H$ hinges and $n_E$ edges and any edge perturbation field $η$, one has $∑_{h=1}^{n_H} A_h · δ_h^{lin}(η) = 0$, where $A_h$ is the area of hinge $h$ and $δ_h^{lin}$ is the linearized deficit angle obtained from the linearization coefficients of $W$.
background
The module packages the Piran-Williams linearization of the Regge deficit angle around a flat simplicial complex, recording it as Phase C4 toward discharging the general Regge deficit linearization hypothesis. WellShapedData packages a simplicial complex together with its linearization coefficients and hinge areas; EdgePerturbation is a vector of small length changes $η_e$ on the edges; linearizedDeficit applies those coefficients to produce the first-order deficit at each hinge. The upstream linear_regge_vanishes theorem states precisely that the indicated sum is zero under Schläfli's identity.
proof idea
This is a one-line term proof that constructs the DeficitLinearizationCert structure by setting its linear_vanishes field to the function (fun W η => linear_regge_vanishes W η).
why it matters
The declaration supplies the certificate required by Phase C4 of the Piran-Williams program, relying on the Schläfli identity already established in Phase C3. It directly supports the claim that the Regge action becomes quadratic in the conformal perturbation variables once the linear term is removed. No downstream uses are recorded yet; the result closes one step in the broader effort to obtain a quadratic action from the linearized Regge calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.