dirichletForm_flat
plain-language theorem explainer
The Dirichlet form associated to any real matrix M on a finite index set vanishes identically when evaluated on the zero function. Workers on the weak-field conformal reduction of the Regge action cite this identity as the zero-mode verification inside the second-variation expansion. The proof unfolds the sum definition, applies ring arithmetic to each summand, and concludes by summation to zero.
Claim. For any natural number $n$ and any real matrix $M$ indexed by $Fin n$, the Dirichlet form $D(M,0)=0$, where $0$ is the zero function on $Fin n$.
background
In the weak-field conformal Regge module the Dirichlet form is the quadratic expression arising from the graph-Laplacian identity: for symmetric zero-row-sum matrices $M$, the bilinear form equals the negative of half the sum of $M_{ij}(f_i-f_j)^2$. The module documentation states that this identity converts the second-order Regge action under the conformal edge ansatz into a Dirichlet energy on edge differences. The present result records the elementary evaluation on the constant mode.
proof idea
The proof unfolds dirichletForm, introduces the auxiliary statement that every summand $M_{ij}((0-0)^2)$ equals zero by the ring tactic, and finishes with simp using sum_const_zero together with mul_zero. It is a direct algebraic verification after unfolding.
why it matters
This supplies the zero-mode base case inside the graph-Laplacian decomposition that feeds weakFieldConformalReggeCert. The certificate packages the full algebraic reduction of the Regge second variation to the Dirichlet form on differences, consistent with the conformal sector of the T8 eight-tick structure. It closes the trivial flat sector of the reduction without invoking geometric Schläfli data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.