uniform_weight_of_sum_one
plain-language theorem explainer
When weights in an n-component vector are constant and sum to one with n positive, each equals 1/n. Researchers calibrating cost functions or normalized distributions in Recognition Science cite this to anchor the uniform case before invoking entropy or forcing relations. The proof cases on the uniformity hypothesis, rewrites the sum as n times the common value, and solves the resulting equation with division and linear arithmetic.
Claim. If a vector of weights $α$ in $ℝ^n$ is uniform and sums to one, with $n>0$, then there exists a real number $a$ such that $α_i = a$ for all $i$ and $a = 1/n$.
background
The module supplies calibration identities for uniform weights in the cost model. UniformWeights asserts that a vector $α : Vec n$ (i.e., a function $Fin n → ℝ$) is constant: there exists $a ∈ ℝ$ such that $α_i = a$ for every index $i$. weightSum simply adds the components: $∑_{i:Fin n} α_i$. The local setting is therefore the set of algebraic relations that hold once weights have been forced uniform and normalized to total mass one. Upstream, the uniform distribution in ShannonEntropy is defined by the same constant $1/n$ (for $n>0$), and the weightSum definition is reused from the BalancedJSubsetSum context, confirming that the same summation operator appears across cryptographic and information-theoretic layers.
proof idea
Tactic proof. It cases on the UniformWeights hypothesis to obtain the common value $a$, rewrites the sum hypothesis as $n·a = 1$ via the definition of weightSum and Finset.card_univ, then applies eq_div_iff followed by linarith to conclude $a = 1/n$. The only non-trivial lemma invoked is the field division rule; the rest is arithmetic simplification.
why it matters
The result closes the normalization step inside the cost-calibration layer, ensuring that any uniform weight vector used downstream (for example in entropy calculations or N-dimensional cost aggregates) is exactly the standard $1/n$ distribution. It therefore supports the uniform case of the Recognition Composition Law and the phi-ladder mass formulas that presuppose normalized weights. No downstream theorems are recorded yet, but the declaration sits directly beneath the uniform distribution definition imported from ShannonEntropy and is a prerequisite for any later claim that uniform weights achieve unit squared norm or minimal J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.