laplacianCoefficient_row_sum
plain-language theorem explainer
The Laplacian coefficient matrix built from any real-valued edge weights A on a finite vertex set has identically zero row sums. Gravity researchers reducing the weak-field Regge action to a Dirichlet form cite this identity to replace the geometric Schläfli row-sum hypothesis with a theorem. The proof expands the definition, isolates the diagonal contribution via single-term extraction, and cancels the remainder by ring normalization.
Claim. For any natural number $n$ and any real matrix $A$ on the finite set of $n$ vertices, define the Laplacian coefficient matrix $L$ by $L_{ii} = sum_k A_{ik}$ and $L_{ij} = -A_{ij}$ for $i ≠ j$. Then $sum_j L_{ij} = 0$ for each fixed vertex $i$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action, expressing the second variation as a Dirichlet form on conformal mode differences after the conformal edge-length ansatz. The Laplacian coefficient is the matrix whose diagonal holds the row sum of $A$ and whose off-diagonal entries are the negated weights; this choice automatically satisfies the zero-row-sum condition required for the reduction. SchläfliRowSum is the hypothesis that the bilinear coefficients of the second-order Regge data sum to zero per row, which is needed to convert the quadratic form into minus one-half the sum of squared differences.
proof idea
The proof introduces the row index, unfolds the definition of the Laplacian coefficient, distributes the sum over the difference of the diagonal term and the off-diagonal entry, extracts the full row sum of $A$ on the diagonal by applying sum_eq_single to the indicator, and concludes with the ring tactic.
why it matters
This result discharges the SchläfliRowSum hypothesis for the Laplacian choice of Regge data, as invoked in the downstream theorem schlaefliRowSum_laplacianReggeData. It completes the graph-Laplacian decomposition step in the module, turning the Regge bilinear form into the Dirichlet quadratic form on edge differences and thereby supporting the conformal-sector reduction of the action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.