laplacianCoefficient
plain-language theorem explainer
Defines the graph Laplacian matrix entries from a symmetric edge-area weight matrix A on Fin n, placing the row sum on the diagonal so rows total zero and subtracting A_ij off-diagonal. Cited by symmetry, row-sum, and Dirichlet-form theorems that reduce the weak-field Regge action to a quadratic form on differences. The definition is a direct case split on index equality.
Claim. For symmetric edge-area weights $A : {Fin n} {to} {Fin n} {to} {mathbb R}$, the Laplacian coefficient matrix $L$ satisfies $L_{ij} = delta_{ij} sum_k A_{ik} - A_{ij}$.
background
The module reduces the second variation of the Regge action under a conformal edge-length ansatz to a Dirichlet form on field differences. For any symmetric matrix M with zero row sums the identity sum_{i,j} M_{ij} xi_i xi_j = -1/2 sum_{i,j} M_{ij} (xi_i - xi_j)^2 holds, converting the bilinear Regge term into the desired energy on gradients.
proof idea
One-line definition that implements the standard graph Laplacian: diagonal receives the full row sum of A while off-diagonal entries receive -A_ij.
why it matters
Supplies the concrete matrix that turns Regge bilinear coefficients into the Dirichlet form of the second-order weak-field action. It is invoked directly by laplacianReggeData and by the symmetry and row-sum lemmas that discharge the SchläfliRowSum hypothesis in the flat conformal sector. This closes the algebraic step that converts S = (1/kappa) sum A_h delta_h into the conformal Dirichlet energy after weak-field expansion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.