dirichletForm_neg
plain-language theorem explainer
The theorem shows that the Dirichlet form on a negated coefficient matrix equals the negative of the form on the original matrix, for any finite index set and any log-potential. Workers reducing the second variation of the Regge action to a graph Laplacian would cite this identity when edge areas are defined as the negation of bilinear coefficients. The proof is a direct algebraic reduction that unfolds the sum definition, negates each summand by ring arithmetic, and distributes the outer negation via sum distributivity.
Claim. Let $M$ be any real $n$ by $n$ matrix and let $ε$ be a log-potential on the $n$ indices. The Dirichlet form $D(-M,ε)$ equals $-D(M,ε)$, where $D(M,ε)$ denotes the sum over all indices $i$ of the inner sum over $j$ of $M_{ij}(ε_i-ε_j)^2$.
background
In the weak-field conformal reduction of the Regge action the second-order term is rewritten as a Dirichlet form on edge differences. The Dirichlet form for coefficient matrix $M$ and potential $ε$ is the double sum $∑_i ∑j M{ij}(ε_i-ε_j)^2$. LogPotential $n$ is the type of functions from the finite set of $n$ vertices to the reals that encode the conformal factor $ξ$. The module isolates this algebraic identity before introducing the geometric hypothesis package that supplies the area and deficit coefficients from Schläfli identities.
proof idea
Unfold the definition of the Dirichlet form. For each summand apply the ring tactic to obtain the pointwise negation. Distribute the negation over each inner sum by sum_neg_distrib together with sum_congr. Replace the outer function by its negated counterpart via funext, then apply sum_neg_distrib once more to the outer sum and finish with ring.
why it matters
The result is invoked directly by dirichletForm_edgeArea, which equates the Dirichlet form on edgeArea to the negative of the form on bilinearCoefficient. It supplies the sign flip required by the definition edgeArea = − bilinearCoefficient inside the graph-Laplacian decomposition step of the module. That step converts the Regge bilinear form into the Dirichlet form on conformal differences, completing one of the three algebraic claims needed for the weak-field reduction of the Regge action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.