quadraticForm
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute the entries of M from Cayley-Menger or dihedral formulas.
- Does not impose symmetry or zero row-sum conditions on M.
- Does not incorporate remainder terms from the conformal length expansion.
- Does not evaluate the full nonlinear Regge action.
formal statement (Lean)
173def quadraticForm {n : ℕ} (M : Fin n → Fin n → ℝ) (ε : LogPotential n) : ℝ :=
proof body
Definition body.
174 ∑ i : Fin n, ∑ j : Fin n, M i j * ε i * ε j
175
176/-- Helper: pulling a constant out of a sum (right-multiplication form). -/