sqNorm_uniform
plain-language theorem explainer
Uniform vectors in n dimensions have squared Euclidean norm exactly n times the square of their common component. Researchers calibrating n-dimensional cost functions cite this when reducing uniform cases to scalar arithmetic. The proof extracts the common value by case analysis on the uniformity predicate then unfolds the dot product and simplifies the resulting sum.
Claim. Let α : ℝ^n satisfy α_i = a for all i and some real a. Then there exists a real number a such that the squared norm of α equals n a², where the squared norm is the dot product of α with itself.
background
Vec n is the type of maps from Fin n to ℝ. The dot product sums componentwise products over the finite index set. sqNorm α is defined as the dot product of α with itself. UniformWeights α asserts that all components equal some common real value a.
proof idea
Case analysis on the UniformWeights hypothesis yields the common value a together with the pointwise equality. The existential is refined with this a; sqNorm and dot are unfolded and the sum is simplified using the equality, the square law, and the cardinality of the index set.
why it matters
The result supplies the explicit scalar form of the squared norm for uniform weights inside the Cost.Ndim calibration module. It supports reductions used by sibling lemmas such as weightSum_uniform and uniform_sqNorm_one. No downstream theorems are recorded yet, but the lemma closes a basic case in the uniform-weight handling required for n-dimensional cost aggregates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.