linear_regge_vanishes
plain-language theorem explainer
The sum over hinges of area times linearized deficit vanishes identically for any edge perturbation on a flat simplicial complex equipped with Schläfli's identity. Regge-calculus workers would cite the result to confirm that the first-order variation of the discrete Einstein-Hilbert action is zero before quadratic curvature terms appear. The proof unfolds the linearized-deficit definition, interchanges summation order, and applies the per-edge Schläfli identity supplied inside WellShapedData to obtain zero termwise.
Claim. Let $W$ be a well-shaped data package consisting of a flat simplicial complex with $n_H$ hinges and $n_E$ edges, its matrix of first partial derivatives of deficit angles, and the Schläfli identity on those derivatives. For any edge-length perturbation map $η$, one has $∑_{h} A_h ⋅ δ_h^{lin}(η) = 0$, where $A_h$ denotes the area of hinge $h$ and $δ_h^{lin}(η) = -∑_e (∂δ_h/∂L_e) η_e$ is the first-order deficit at $h$.
background
The module implements the Piran-Williams linearization of the Regge action around a flat simplicial background. WellShapedData packages a FlatSimplicialComplex, the LinearizationCoefficients matrix of partials dThetadL, and the SchlaefliIdentity that supplies the necessary sum rules. EdgePerturbation is simply a map Fin nE → ℝ recording the length increments η_e. linearizedDeficit is defined as the negative of the contraction of that matrix against η at each hinge.
proof idea
Unfold linearizedDeficit to expose the double sum carrying a minus sign. Rewrite by distributing sums and invoking Finset.sum_comm to interchange the hinge and edge indices, producing a sum over edges of η_e times an inner sum over hinges. For each edge the inner sum is precisely the left-hand side of the Schlaefli identity stored in W.schlaefli; multiplication by η_e followed by summation therefore yields zero via mul_zero and Finset.sum_eq_zero.
why it matters
The theorem populates the linear_vanishes field of DeficitLinearizationCert, which is invoked by simplicialFieldCurvatureCert inside SimplicialDeficitDischarge to discharge the ReggeDeficitLinearizationHypothesis. It thereby establishes that the leading non-trivial term in the expanded Regge action is quadratic in the perturbations, exactly as required for the quadratic curvature action in the simplicial ledger. The result closes Phase C4 of the program that discharges the linearization hypothesis on general simplicial complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.