inner_sum_const
The lemma shows that for a matrix M indexed by Fin n and a vector g, the sum over j of M i j times g i factors exactly as g i times the row sum of M at fixed i. It is invoked in the algebraic steps that convert the Regge bilinear form into a Dirichlet form on edge differences during the weak-field conformal reduction. The proof is a one-line wrapper that applies the constant-multiplication rule for finite sums.
claimLet $M : {Fin} n → {Fin} n → ℝ$ be any matrix and $g : {Fin} n → ℝ$ any vector. Then for each fixed index $i$, $∑_j M_{ij} g_i = (∑_j M_{ij}) g_i$.
background
The module WeakFieldConformalRegge develops the algebraic core of the weak-field reduction of the Regge action under the conformal edge ansatz ℓ_{ij} = ℓ_0 exp((ξ_i + ξ_j)/2). After expanding to second order, the second variation reduces to a quadratic form Q[ξ; M] on a symmetric matrix M with zero row sums; the target identity is Q[ξ; M] = −D[ξ; M], where D is the Dirichlet form ½ ∑{i,j} M{ij} (ξ_i − ξ_j)². The present lemma supplies the elementary factoring step needed when the inner sum over j carries a factor that depends only on the outer index i.
proof idea
one-line wrapper that applies sum_const_mul_right (fun j => M i j) (g i)
why it matters in Recognition Science
The lemma is an auxiliary step inside the graph-Laplacian decomposition (the fully proved §2 of the module). That decomposition converts the Regge bilinear form Σ M_{ij} ξ_i ξ_j into the Dirichlet form on differences, which is the algebraic content of the weak-field reduction S^(2) = (1/κ) Σ ½ (ξ_i − ξ_j)² A_{ij}. It therefore sits directly beneath the claim that the conformal sector of the second variation is a discrete Laplace operator, as required for the Piran–Williams specialization of the Regge action.
scope and limits
- Does not assume symmetry or zero row sums of M.
- Does not compute the geometric entries of M from Cayley–Menger or dihedral data.
- Applies only to finite sums indexed by Fin n.
- Does not address convergence or continuum limits of the discrete form.
formal statement (Lean)
183private lemma inner_sum_const {n : ℕ} (M : Fin n → Fin n → ℝ) (g : Fin n → ℝ) (i : Fin n) :
184 ∑ j : Fin n, M i j * g i = (∑ j : Fin n, M i j) * g i :=
proof body
Term-mode proof.
185 sum_const_mul_right (fun j => M i j) (g i)
186
187/-- **GRAPH-LAPLACIAN DECOMPOSITION.**
188 For symmetric `M` with zero row sums,
189 `Q[ξ; M] = −D[ξ; M]`.
190
191 This is the algebraic core of the weak-field reduction. -/