dirichletForm
plain-language theorem explainer
The declaration defines the Dirichlet form D[ε; M] as half the double sum over vertices of M_ij times the squared difference (ε_i - ε_j)^2, where ε is a log-potential on a finite set of n vertices. Researchers performing the weak-field conformal reduction of the Regge action cite this expression to convert bilinear coefficients into graph-Laplacian energy. It is introduced by direct summation without auxiliary lemmas.
Claim. Let $M$ be a real matrix indexed by pairs from a finite set of $n$ vertices and let $ε$ be a log-potential assignment $ε : Fin n → ℝ$. The Dirichlet form is $D[ε; M] := ½ ∑_{i,j} M_{ij} (ε_i - ε_j)^2$.
background
The module WeakFieldConformalRegge develops the algebraic core of the weak-field reduction of the Regge action. It begins from the conformal edge ansatz ℓ_ij = ℓ_0 exp((ξ_i + ξ_j)/2) and expands to second order, yielding a quadratic form on the conformal factor ξ. The log-potential ε is the upstream object LogPotential n, defined as the type Fin n → ℝ with ε_i = ln ψ(σ_i) and used to generate edge lengths via the exponential ansatz; the same type appears in ContinuumBridge.laplacian_action.
proof idea
This is a direct definition that expands to the summation (1/2) * ∑_i ∑_j M i j * (ε i - ε j)^2. No lemmas or tactics are invoked; the expression is the primitive from which all later identities are derived by unfolding.
why it matters
The definition supplies the positive quadratic expression that appears in the reduced second-order Regge action. It is invoked by the graph-Laplacian decomposition theorem dirichlet_eq_neg_quadratic, which proves quadraticForm M ε = - dirichletForm M ε for symmetric M with zero row sums, and by dirichletForm_edgeArea which relates it to the geometric edge-area matrix. In the Recognition framework this completes the algebraic step that converts Regge bilinear coefficients into Dirichlet energy on the graph, consistent with the T7 eight-tick octave and the D = 3 spatial dimensions of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.