sum_const_mul_right
plain-language theorem explainer
The lemma states that for any finite index set of size n, real-valued f, and constant c, the sum over j of f(j) times c equals the total sum of f(j) multiplied by c. Algebraic helpers of this form are cited in proofs establishing graph-Laplacian identities for discrete gravity reductions. The proof is a one-line wrapper applying the standard Finset sum-multiplication rule.
Claim. For any natural number $n$, function $f : [n] → ℝ$, and real $c$, $∑_{j ∈ [n]} f(j) · c = (∑_{j ∈ [n]} f(j)) · c$.
background
The WeakFieldConformalRegge module develops the algebraic core of the weak-field reduction of the Regge action to a Dirichlet form on conformal modes. It proves three independent claims: conformal expansion of edge lengths to second order, graph-Laplacian decomposition of quadratic forms, and packaging of geometric input under the Schläfli row-sum hypothesis. The decomposition step rewrites a symmetric zero-row-sum bilinear form Σ M_{ij} ξ_i ξ_j as −½ Σ M_{ij} (ξ_i − ξ_j)², which requires several finite-sum identities over Fin n.
proof idea
The proof is a one-line wrapper that applies the Finset.sum_mul lemma by rewriting the left-hand side.
why it matters
This helper is invoked by inner_sum_const, which supports the dirichlet_eq_neg_quadratic theorem establishing the graph-Laplacian decomposition Q[ξ; M] = −D[ξ; M]. That identity is the algebraic core of the weak-field conformal reduction, allowing the second-order Regge action to equal ½ times the Dirichlet form on the conformal mode ε with edge weights given by area-deficit products. It fills the graph-Laplacian step inside the module's §2 claim and feeds the main weak_field_conformal_reduction theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.