dirichletForm_edgeArea_laplacianReggeData
plain-language theorem explainer
The theorem shows that the Dirichlet form on log-potentials induced by edge-area weights extracted from Laplacian Regge data equals the Dirichlet form induced by the original symmetric matrix A. Workers reducing the weak-field Regge action to a quadratic form on conformal modes cite this identity to justify the flat-sector simplification. The proof is a one-line wrapper that applies the diagonal-irrelevance lemma after substituting the explicit bilinear coefficients.
Claim. Let $A$ be a symmetric real matrix on vertices indexed by Fin $n$ and let $ε$ be a log-potential. The Dirichlet form $D[ε;M] = ½ ∑_{i,j} M_{ij} (ε_i - ε_j)^2$ evaluated on the edge-area matrix $M$ derived from the Laplacian Regge data of $A$ equals the same form evaluated on $A$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action, expressing the second-order term as a Dirichlet form on vertex log-potentials. The Dirichlet form generated by a symmetric matrix $M$ is $D[ε;M] = ½ ∑{i,j} M{ij} (ε_i - ε_j)^2$. Edge-area weights are defined by $A_{ij} = -M_{ij}$ where $M$ comes from the bilinear coefficients of WeakFieldReggeData. LogPotential is the type Fin $n$ → ℝ recording vertex values $ε_i = ln ψ(σ_i)$. Upstream, dirichletForm_diag_irrelevant proves the form ignores diagonal entries, while bilinearCoefficient_laplacianReggeData identifies the off-diagonal entries of the Laplacian data with those of $A$.
proof idea
The proof is a one-line wrapper that invokes dirichletForm_diag_irrelevant. It introduces the off-diagonal hypothesis, unfolds edgeArea, rewrites the bilinear coefficient via bilinearCoefficient_laplacianReggeData, unfolds laplacianCoefficient, and simplifies with the symmetry assumption on $A$.
why it matters
This identity supplies the algebraic step that converts the graph-Laplacian second-variation matrix into the standard Dirichlet form on differences. It is invoked by the parent theorem weak_field_conformal_reduction_laplacianData, which states the unconditional flat-sector reduction of the second-order Regge action to ½ dirichletForm A ε. The result belongs to the graph-Laplacian decomposition layer and supplies the finite-dimensional algebra that turns a symmetric zero-row-sum matrix into the quadratic form required by the conformal reduction in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.