LinearizationCoefficients
plain-language theorem explainer
LinearizationCoefficients packages the matrix of first partial derivatives of deficit angles with respect to edge lengths, evaluated on a flat simplicial background. Discrete gravity researchers cite it when expanding the Regge action to quadratic order under edge perturbations. The declaration is a direct structural extension of DeficitDerivativeMatrix with no added fields or proof obligations.
Claim. A linearization-coefficient structure for $n_H$ hinges and $n_E$ edges is a matrix $M$ whose entry $M_{h,e}$ equals the partial derivative of the deficit angle at hinge $h$ with respect to the length of edge $e$, evaluated at the flat configuration.
background
The Piran-Williams linearization expands the Regge deficit around a flat simplicial complex where all deficits vanish. A perturbation of edge lengths by a vector η produces a first-order deficit change δ̂_h = −∑_e (∂θ_h/∂L_e) η_e, with the minus sign arising because deficit equals 2π minus total dihedral sum. The module imports deficit definitions from DihedralAngle and Schlaefli, together with the DeficitDerivativeMatrix structure whose dThetadL field stores exactly these partials.
proof idea
The declaration is a one-line structural extension of DeficitDerivativeMatrix nH nE, inheriting the dThetadL matrix field without introducing new components or axioms.
why it matters
The structure supplies the coefficient matrix required by linearizedDeficit and by the WellShapedData bundle that also carries the flat complex and the Schläfli identity. It completes Phase C4 of the Regge linearization program, preparing the quadratic action result of Phase C5 in which the linear term vanishes by Schläfli’s identity. The construction sits inside the Recognition Science geometry layer that precedes the conformal ansatz linking edge perturbations to the log-potential field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.