dirichlet_form_eq_neg_quadratic
plain-language theorem explainer
The algebraic identity shows that for any symmetric matrix M on a finite vertex set with zero row sums, the Dirichlet form on a log-potential field equals the negative of the associated quadratic form. Workers on the weak-field conformal reduction of the Regge action cite this to obtain a positive expression from the second variation bilinear. The proof is a one-line wrapper that invokes the prior decomposition lemma and applies linear arithmetic.
Claim. Let $M$ be a symmetric real matrix on vertices $Fin n$ with zero row sums and let $ξ$ be a log-potential field. Then the Dirichlet form $D(ξ; M)$ equals the negative of the quadratic form $Q(ξ; M)$.
background
In the weak-field conformal reduction of the Regge action the second-order term arises from the expansion of $S = (1/κ) Σ_h A_h δ_h$ under the ansatz $ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2)$. The module isolates the algebraic step that converts any symmetric zero-row-sum bilinear form into a Dirichlet form on differences $(ξ_i - ξ_j)^2$. The Dirichlet form is the positive expression $½ Σ_{i,j} M_{ij} (ξ_i - ξ_j)^2$ while the quadratic form is the direct sum $Σ_{i,j} M_{ij} ξ_i ξ_j$. Upstream the lemma dirichlet_eq_neg_quadratic supplies the exact relation between these two expressions for any such matrix.
proof idea
The proof is a one-line wrapper that applies the lemma dirichlet_eq_neg_quadratic to the given symmetric matrix M with zero row sums and the log-potential ε, then concludes by linear arithmetic.
why it matters
This identity completes the graph-Laplacian decomposition in §2 of the module, allowing the second-order Regge action to be rewritten as a positive Dirichlet form. It feeds the conformal flat-mode invariance step that reduces the action to $Σ ½ (ξ_i - ξ_j)^2 A_{ij}$. The result sits inside the Recognition Science gravity sector and supports the passage from the J-cost functional through the phi-ladder to the eight-tick octave and D = 3, although the geometric coefficients from Schläfli remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.