laplacianCoefficient_symm
plain-language theorem explainer
The Laplacian coefficient matrix inherits symmetry from its input matrix A. Researchers reducing the Regge action to a Dirichlet form in the weak-field conformal sector cite the result to justify index interchange in the second-variation bilinear form. The proof is a direct case split on index equality: the diagonal case is immediate by reflexivity while the off-diagonal case simplifies to an application of the symmetry hypothesis after unfolding.
Claim. If $A$ is a symmetric real matrix indexed by $n$ points, then the associated Laplacian coefficient matrix $L$ satisfies $L_{ij}=L_{ji}$ for all indices $i,j$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action, converting the second variation into a Dirichlet form on differences $(ξ_i - ξ_j)^2$. The Laplacian coefficient matrix is the graph-Laplacian object appearing in the decomposition lemma that equates the quadratic form $Σ M_{ij} ξ_i ξ_j$ to $-½ Σ M_{ij} (ξ_i - ξ_j)^2$ whenever $M$ is symmetric with zero row sums. This theorem supplies the symmetry of that coefficient matrix, which is packaged into WeakFieldReggeData together with the normalization dArea = 1.
proof idea
The tactic proof introduces the indices, unfolds the definition of the Laplacian coefficient, and splits on whether i equals j. The equal case reduces by substitution and reflexivity. The unequal case introduces the swapped inequality, simplifies the conditional expression via simp on the false branches and zero subtraction, then rewrites using the symmetry hypothesis on A.
why it matters
The result discharges the symmetry requirement inside the definition of laplacianReggeData, which supplies the weak-field Regge data whose deficit coefficients are exactly the Laplacian matrix. It thereby completes the algebraic step that turns the Regge bilinear form into the Dirichlet form on edge differences, as outlined in the module's graph-Laplacian decomposition section. Within the Recognition framework this supports the finite-dimensional reduction of the Regge action before geometric input from Schläfli or Cayley-Menger formulas is supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.