weightSum
plain-language theorem explainer
weightSum sums the components of a real vector α in dimension n. Calibration theorems for uniform weights and balanced subset-sum verifiers cite this sum when checking total weight equals one or a target. It is implemented as the standard finite sum over Fin n.
Claim. For any natural number $n$ and vector $α : ℝ^n$, weightSum$(α) := ∑_{i ∈ Fin n} α_i$.
background
The module supplies calibration relations for uniform weights in the N-dimensional cost model. Vec n denotes n-component real vectors as maps Fin n → ℝ. This real-valued sum parallels the integer weightSum from BalancedJSubsetSum, which aggregates weights over a witness support.
proof idea
One-line definition that applies the built-in summation operator directly over the finite index set Fin n. No lemmas or tactics are required.
why it matters
This definition feeds uniform_weight_of_sum_one (which concludes uniform weights summing to 1 equal 1/n) and weightSum_uniform (which factors the sum as n times the common value). It also supports fromSubsetSum_isSolution and weightTarget in BalancedJSubsetSum by supplying the matching real sum. It supplies the total-weight primitive for cost calibration in the Ndim layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.