schlaefliRowSum_laplacianReggeData
plain-language theorem explainer
The theorem shows that Laplacian second-variation data for any symmetric edge weights satisfies the Schläfli row-sum vanishing condition required for the conformal reduction. Workers on discrete gravity and Regge calculus cite it when specializing to flat backgrounds. The proof is a direct substitution that invokes the zero row-sum property of the Laplacian coefficients and matches it to the bilinear form via the definition of laplacianReggeData.
Claim. For any $n$ and symmetric $A : [n]×[n]→ℝ$, let $W$ be the weak-field Regge data with $dArea_{ij}=1$ and $dDeficit_{ij}$ equal to the graph-Laplacian coefficients of $A$. Then $W$ obeys the Schläfli row-sum condition: for every vertex $i$, $∑_j$ bilinearCoefficient$(W,i,j)=0$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. The second-order term arises from the conformal edge ansatz $ℓ_{ij}=ℓ_0 exp((ξ_i+ξ_j)/2)$ expanded to quadratic order in the conformal modes ξ. This produces a bilinear form on ξ whose coefficients are packaged in WeakFieldReggeData; the SchläfliRowSum property then guarantees that the form reduces to the Dirichlet quadratic form on differences $(ξ_i−ξ_j)^2$.
proof idea
The proof is a one-line wrapper. It introduces the row index i, applies the upstream theorem laplacianCoefficient_row_sum A i to obtain the vanishing sum of Laplacian coefficients, and substitutes via bilinearCoefficient_laplacianReggeData to match the required sum of bilinear coefficients for laplacianReggeData.
why it matters
This discharges the Schläfli row-sum hypothesis for Laplacian data, enabling the unconditional reduction weak_field_conformal_reduction_laplacianData. That result feeds the certification weakFieldConformalReggeCert, which packages the full algebraic core of the conformal Regge reduction. It closes the gap between the graph-Laplacian decomposition lemma and the geometric input from flat Regge calculus, aligning with the framework's use of the Dirichlet form as the quadratic action in the conformal sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.