uniform_sqNorm_one
plain-language theorem explainer
Under uniform weights in n dimensions with squared Euclidean norm equal to one, the common component value a satisfies a squared equals one over n. Researchers calibrating cost models in multi-dimensional Recognition Science settings would cite this normalization step. The proof extracts the common value by case analysis on the uniform hypothesis and rearranges the resulting scalar equation n a squared equals one via division.
Claim. Let $n > 0$ be a natural number and let $α : Fin n → ℝ$ be a vector whose components are all equal to some real number $a$. If the squared Euclidean norm of $α$ equals 1, then $a^2 = 1/n$.
background
The module supplies calibration relations for uniform weights inside the cost framework. Vec n is the type of n-component real vectors, written as functions from Fin n to the reals. UniformWeights α asserts the existence of a real a such that α i equals a for every index i. sqNorm α is defined as the dot product of α with itself, which expands to the sum of squares of the components. The dot product itself is the standard sum over i of α i times t i. This local setting sits inside the Recognition Science cost model, where Cost abbreviates Quantity CostUnit.
proof idea
The proof performs case analysis on the UniformWeights hypothesis to extract the common value a and the equality ha. It first shows that n is nonzero as a real. It then rewrites the squared-norm hypothesis using the definitions of sqNorm and dot to obtain the scalar equation n a squared equals 1. Finally it applies the equivalence eq_div_iff and linear arithmetic to conclude a squared equals 1 over n.
why it matters
This supplies a basic normalization fact for uniform vectors inside n-dimensional cost calibration. It supports the Recognition Science framework's treatment of weight distributions on the phi-ladder and the emergence of D equals 3 spatial dimensions. No downstream theorems are listed yet, but the result closes a calibration step required for uniform-weight cost aggregates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.