weak_field_conformal_reduction_laplacianData
plain-language theorem explainer
Any symmetric edge-weight matrix A on a finite vertex set induces Laplacian Regge data whose second-order action on a log-potential ε equals half the Dirichlet form of A. Gravity modelers working in the weak-field conformal sector cite this to replace the full Regge quadratic form with a standard Dirichlet energy on differences. The term proof is a two-rewrite application of the general conformal reduction followed by the edge-area equivalence for the Laplacian data.
Claim. For any natural number $n$, any symmetric real matrix $A$ on vertices indexed by Fin $n$, and any log-potential assignment $ε$, the second-order Regge action evaluated on the Laplacian-derived Regge data equals $(1/2)$ times the Dirichlet form generated by the weights $A$ on $ε$.
background
The module proves the algebraic core of the weak-field conformal reduction of the Regge action. A log-potential $ε$ records vertex values $ε_i = ln ψ(σ_i)$ so that edge lengths follow the conformal ansatz proportional to $exp((ε_i + ε_j)/2)$. The Dirichlet form is the quadratic energy $D[ε; A] = (1/2) ∑{i,j} A{ij} (ε_i - ε_j)^2$ for symmetric $A$ (quoted from the sibling definition).
proof idea
Two-rewrite term proof. First invoke the general weak-field conformal reduction on the Laplacian Regge data, using the already-proved Schläfli row-sum property for that data. Second replace the Dirichlet form on the induced edge-area matrix by the original weights $A$ via the diagonal-irrelevance lemma.
why it matters
Supplies the concrete reduction step required by the kappa-scaled variant and by the top-level certification theorem that packages conformal expansion, graph-Laplacian decomposition, and reduction. It closes the graph-Laplacian decomposition section of the module, converting any symmetric zero-row-sum bilinear form into the Dirichlet energy on differences. This algebraic identity is the prerequisite before geometric Regge coefficients from Cayley-Menger data can be inserted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.