dirichletForm_diag_irrelevant
plain-language theorem explainer
The Dirichlet form on a finite graph is invariant under arbitrary changes to the diagonal entries of its weight matrix. Workers reducing the Regge action to its weak-field conformal sector cite this when swapping the original edge-area matrix for its Laplacian-Regge version. The proof unfolds the double-sum definition, splits the sum into diagonal and off-diagonal cases via by_cases, cancels the diagonal contribution by ring, and substitutes the off-diagonal equality hypothesis.
Claim. Let $D[ε; M] = (1/2) ∑_{i,j} M_{ij} (ε_i - ε_j)^2$ be the Dirichlet form on a log-potential $ε$. If two matrices $A$ and $B$ agree off the diagonal, then $D[ε; A] = D[ε; B]$.
background
The module WeakFieldConformalRegge develops the algebraic core of the conformal weak-field reduction of the Regge action: the second variation reduces to a Dirichlet form on differences $(ξ_i - ξ_j)^2$ once the edge-length ansatz $ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2)$ is expanded to second order. The key definition is dirichletForm, which takes a symmetric matrix $M$ and a LogPotential $ε : Fin n → ℝ$ (the vertex log-potentials) and returns $(1/2) ∑{i,j} M{ij} (ε_i - ε_j)^2$. Upstream, ContinuumBridge.as identifies this form with the Laplacian action on the simplicial ledger, while EdgeLengthFromPsi.LogPotential records the conformal edge lengths derived from the same potentials.
proof idea
The term proof unfolds dirichletForm, applies two Finset.sum_congr steps to reach the summand, then performs by_cases on whether i equals j. The diagonal branch substitutes and reduces by ring; the off-diagonal branch rewrites the matrix entry via the hypothesis hOff.
why it matters
The result is invoked directly by the sibling theorem dirichletForm_edgeArea_laplacianReggeData, which transfers the Dirichlet form from the original edge-area weights to the Laplacian-Regge matrix. It thereby completes the graph-Laplacian decomposition step in the module, allowing the second-variation Regge action to be expressed purely as a Dirichlet form without reference to diagonal entries. This algebraic closure supports the reduction of the Regge action to the conformal sector in the weak-field limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.