quadraticForm
plain-language theorem explainer
quadraticForm supplies the bilinear quadratic form Q(M, ε) = Σ_{i,j} M_{ij} ε_i ε_j on a finite graph with n vertices. Workers on discrete gravity and Regge calculus cite it when converting the second variation of the action into a graph Laplacian energy. The definition is a direct double summation with no auxiliary lemmas or reductions.
Claim. For an $n$-vertex graph, a real matrix $M : [n]×[n] → ℝ$ and a log-potential assignment $ε : [n] → ℝ$, the quadratic form is $Q(M,ε) = ∑_{i=1}^n ∑_{j=1}^n M_{ij} ε_i ε_j$.
background
The module Weak-Field Conformal Reduction of the Regge Action introduces this bilinear form as the algebraic engine for the second-order expansion. LogPotential n is the type Fin n → ℝ whose values ε_i = ln ψ(σ_i) generate conformal edge lengths via ℓ_{ij} = a · exp((ε_i + ε_j)/2). Upstream results on LedgerFactorization and PhiForcingDerived calibrate the J-cost and log-potential so that ε is the natural perturbation variable around the flat vacuum.
proof idea
The definition is given directly by the double sum over matrix elements weighted by the potential components. No lemmas are invoked; it serves as the primitive expression from which the graph-Laplacian identity is derived in the sibling theorems.
why it matters
quadraticForm is the starting point for dirichlet_eq_neg_quadratic and weak_field_conformal_reduction, which establish that the second-order Regge action equals (1/2) times the Dirichlet form on the conformal mode when the Schläfli row-sum condition holds. It supplies the algebraic core that converts the Regge bilinear form into a positive Dirichlet energy, consistent with the Recognition forcing chain that yields D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.