sqNorm
plain-language theorem explainer
sqNorm defines the squared Euclidean norm of an n-component real vector as its self-dot product. Calibration theorems for uniform weights in the Recognition Science cost model cite this when deriving scaling relations under the UniformWeights predicate. The definition is a direct one-line alias to the dot product from the Core module.
Claim. For a vector $α : ℝ^n$ given as a function on Fin n, the squared norm is defined by $‖α‖^2 := α · α$, where the dot product is the standard sum $∑_{i=0}^{n-1} α_i · α_i$.
background
The Cost.Ndim.Calibration module establishes calibration relations for uniform weights. Vec n is the type of n-component real vectors, realized as functions Fin n → ℝ. The dot product is the weighted inner product $∑_{i:Fin n} α_i t_i$ used by the logarithmic aggregate in the Recognition framework.
proof idea
One-line definition that applies the dot product from Core to the input vector with itself.
why it matters
sqNorm feeds the two uniform-weight theorems in the same module: sqNorm_uniform (which factors the norm as n a²) and uniform_sqNorm_one (which recovers the uniform component a = 1/√n for unit norm). It supplies the basic quadratic form needed for cost calibration steps that connect to the phi-ladder and D = 3 spatial dimensions in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.