dirichlet_eq_neg_quadratic
plain-language theorem explainer
The identity equates the quadratic form on a symmetric zero-row-sum matrix M to the negative of its Dirichlet form on any potential ε. It is cited in the weak-field conformal reduction of the Regge action within Recognition Science gravity derivations. The proof expands each squared difference, distributes the double sums, cancels the pure-square contributions via the row-sum hypothesis, and finishes by ring arithmetic.
Claim. Let $M$ be a symmetric real matrix on $n$ indices with all row sums zero. For any real-valued assignment $ε$ on those indices, the associated quadratic form satisfies $Q(M,ε) = -D(M,ε)$, where $Q(M,ε) = ∑_{i,j} M_{ij} ε_i ε_j$ and $D(M,ε) = ½ ∑_{i,j} M_{ij} (ε_i - ε_j)^2$.
background
The module isolates the algebraic core of the weak-field conformal reduction of the Regge action. Section 2 states the graph-Laplacian decomposition: for symmetric $M$ with zero row sums, the bilinear quadratic form on a potential equals the negative of the Dirichlet energy form. This identity converts the second-variation matrix of the Regge action into a sum of squared differences on edges. The row-sum hypothesis on $M$ is supplied by the geometric input package and is the discrete counterpart of the flat-mode condition in Regge calculus linearization.
proof idea
Unfold quadraticForm and dirichletForm. Expand each $(ε_i - ε_j)^2$ term by ring. Distribute the double sums and apply sum_const_mul_right together with the row-sum hypothesis to show the $ε_i^2$ and $ε_j^2$ blocks vanish. The remaining cross term supplies the factor of $-2$ that produces the sign change; ring closes the equality.
why it matters
This supplies the graph-Laplacian decomposition required for the weak-field conformal reduction. It is applied directly in weak_field_conformal_reduction to equate the second-order Regge action to half the Dirichlet form on edgeArea, and it appears in the certification theorem weakFieldConformalReggeCert. The result completes the finite-dimensional algebraic step that lets the Recognition Science forcing chain produce the Einstein-Hilbert action in the weak-field limit under the conformal ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.