weightSum
plain-language theorem explainer
The weightSum definition computes the total of an n-dimensional real vector's components by direct summation. Calibration researchers in the N-dimensional cost model and subset-sum cryptographers would reference this aggregate. The definition is a straightforward summation over the Fin n index set with no additional lemmas required.
Claim. For a real vector $α$ with $n$ components where $α : Fin n → ℝ$, the weight sum is defined as $∑_{i : Fin n} α_i$.
background
The module Cost.Ndim.Calibration develops relations for uniform weights in the Recognition Science cost framework. Vectors are defined via the abbrev Vec (n : ℕ) := Fin n → ℝ, providing n-component real vectors as coordinate functions. This summation serves as the basic aggregation operator for these vectors.
proof idea
This declaration is a direct definition that unfolds to the standard summation ∑ i : Fin n, α i. No tactics or lemmas are invoked; it is the primitive sum constructor applied to the vector components.
why it matters
This sum feeds directly into the uniform weight theorems within the module, including weightSum_uniform which relates the sum to n times the uniform value a, and uniform_weight_of_sum_one which derives that each component equals 1/n when the sum is 1 and weights are uniform. It is also referenced in the BalancedJSubsetSum module for establishing solutions from subset sums. In the broader framework, it supplies the aggregation step for cost calculations in N dimensions, supporting the transition from vector representations to scalar costs before engaging higher structures such as the J-cost or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.