linearizedDeficit
plain-language theorem explainer
Linearized deficit at hinge h under perturbation η is the first-order Taylor term for the Regge deficit angle change, computed as the negative dot product of the precomputed derivative row with the perturbation vector. Discrete gravity researchers expanding Regge actions around flat simplicial complexes cite this when deriving quadratic effective actions. It is a direct one-line summation definition from the LinearizationCoefficients matrix.
Claim. $δ_h(η) = -∑_e (∂δ_h/∂L_e)|_{flat} ⋅ η_e$, where the partial derivatives are the entries of the linearization coefficients matrix for hinge h and η is the vector of edge-length perturbations.
background
The module packages the Piran-Williams linearization of the Regge deficit angle around a flat simplicial complex. LinearizationCoefficients is the structure holding the matrix of partial derivatives ∂θ_h/∂L_e evaluated at the flat background for each hinge-edge pair. EdgePerturbation packages the vector η of small edge-length changes.
proof idea
One-line definition that negates the sum over edges of the product between the h-th row of the derivative matrix M.dThetadL and the components of η.eta. No lemmas or tactics are applied beyond the built-in summation.
why it matters
This definition supplies the explicit first-order term required by linear_regge_vanishes and DeficitLinearizationCert to certify that the linear contribution to the Regge action sums to zero. It completes the Phase C4 linearization step in the module, feeding the WellShapedData package that Phase C5 uses to obtain a quadratic action in the simplicial ledger. It supports the D=3 geometry extraction in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.