inner_sum_const
plain-language theorem explainer
The lemma shows that for any n, matrix M, vector g, and fixed i, the sum over j of M i j times g i equals the row-sum of M at i multiplied by g i. Workers reducing discrete Regge actions to quadratic forms on conformal fields cite this identity when factoring constants from inner sums. The proof applies the general sum-const-multiplication result in a single step.
Claim. Let $n$ be a natural number, $M$ a real-valued function on Fin $n$ times Fin $n$, $g$ a real-valued function on Fin $n$, and $i$ an element of Fin $n$. Then $$sum_{j in Fin n} M(i,j) cdot g(i) = bigl(sum_{j in Fin n} M(i,j)bigr) cdot g(i).$$
background
In the module on weak-field conformal reduction of the Regge action, this helper lemma supports the algebraic manipulation needed to convert a symmetric zero-row-sum matrix into a Dirichlet form. The module derives the second-order expansion of the Regge action under the conformal edge ansatz ell_{ij} = ell_0 exp((xi_i + xi_j)/2), reducing it to a sum of squared differences (xi_i - xi_j)^2 weighted by area coefficients. The graph-Laplacian decomposition states that for such matrices the quadratic form equals the negative of the Dirichlet form on differences. Upstream results supply the J-cost structure from PhiForcingDerived and the simplicial ledger from EdgeLengthFromPsi, which calibrate the discrete geometry underlying the conformal mode.
proof idea
The proof is a one-line wrapper applying the sum_const_mul_right lemma to the row slice fun j => M i j with constant multiplier g i.
why it matters
This lemma contributes to the graph-Laplacian decomposition that forms the algebraic core of the weak-field reduction, allowing the Regge bilinear form to be rewritten as a Dirichlet form. It advances the finite-dimensional algebra in section 2 of the module documentation, which is required before inserting geometric coefficients from Schlaefli relations. In the broader Recognition Science setting it supports the discrete-to-continuum bridge for gravity, consistent with the eight-tick octave and D=3 spatial dimensions, though the explicit computation of area and deficit responses remains open in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.