dirichletForm_edgeArea
plain-language theorem explainer
The theorem establishes that the Dirichlet form on the edge-area matrix from weak-field Regge data equals the negation of the Dirichlet form on the bilinear coefficient matrix. Discrete gravity researchers reducing the second-order Regge action to a graph Laplacian on conformal modes would cite this identity. The proof is a one-line wrapper that invokes the general negation property of the Dirichlet form once the definitional equality edgeArea W = - bilinearCoefficient W is noted.
Claim. Let $W$ be weak-field Regge data on $n$ vertices with first-order responses $dArea$ and $dDeficit$, and let $M$ be the bilinear coefficient matrix with entries $M_{ij} = dArea_{ij} dDeficit_{ij}$. Let $A$ be the edge-area matrix defined by $A = -M$. For any log-potential $ε$, the Dirichlet form satisfies $D(A, ε) = -D(M, ε)$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. Under the ansatz $ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2)$, the second-order term in the action becomes a bilinear form on the conformal mode $ε$. WeakFieldReggeData packages the linear responses: its fields $dArea$ and $dDeficit$ record the first-order changes in hinge area and deficit angle. Their entrywise product defines the bilinearCoefficient matrix $M$, while edgeArea is defined as its negation to match the sign convention in the action expansion.
proof idea
The proof is a one-line wrapper. It applies the general lemma dirichletForm_neg to the bilinearCoefficient matrix and the potential $ε$. The accompanying comment records that edgeArea W is definitionally equal to the pointwise negation of bilinearCoefficient W, so the desired equality follows at once.
why it matters
This identity is invoked inside the main theorem weak_field_conformal_reduction to finish the algebraic reduction of the second-order Regge action to half the Dirichlet energy on the edge-area matrix. It supplies the sign-management step in the graph-Laplacian decomposition of §2. Within the Recognition framework it supports the conformal sector of the weak-field limit, consistent with the eight-tick octave once the geometric coefficients satisfying the Schläfli row-sum condition are supplied. The result is fully proved with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.