weightSum_uniform
plain-language theorem explainer
Uniform vectors with all components equal to a real a have total weight sum exactly n a. Researchers calibrating costs under uniform weighting in the Ndim module cite this to reduce vector sums to scalar multiples. The proof destructures the uniform hypothesis to extract a, unfolds the summation definition, and simplifies via index-set cardinality.
Claim. Let $n$ be a natural number and let $α$ be an $n$-component real vector whose entries are all equal to some real number $a$. Then the sum of the entries of $α$ equals $n a$.
background
Vec denotes $n$-component real vectors realized as functions from the finite index set Fin $n$ to the reals. UniformWeights asserts that such a vector has every component identical to one fixed real value $a$. weightSum is defined as the ordinary summation of those components over Fin $n$ (imported from the core module). The local setting is the calibration module for uniform weights, whose module header states it supplies calibration relations for uniform weights.
proof idea
The term proof performs case analysis on the UniformWeights hypothesis to obtain the common value $a$ together with the equality proof $ha$. It refines the existential goal with $a$, unfolds weightSum to the explicit sum, and applies simp using $ha$ and the cardinality of the full index set.
why it matters
This supplies a basic reduction for uniform cases inside the cost calibration layer of the Recognition framework. It supports downstream relations such as uniform_sqNorm_one within the same module by converting vector sums to scalar arithmetic. No parent theorem is listed among the used-by edges, but the result closes a calibration step for the uniform-weight hypothesis in Ndim cost calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.