normalized
plain-language theorem explainer
The definition supplies the normalized sequence ã(n) = a(n) / runningMax(a)(n) for rescaling blowup sequences. Navier-Stokes regularity researchers cite it when constructing bounded ancient solutions from hypothetical singularities. The implementation is a direct one-line division by the running-maximum definition.
Claim. For a sequence $a : ℕ → ℝ$, the normalized value at index $n$ is defined by $ã(n) := a(n) / M̃(n)$, where $M̃(n) = max_{k ≤ n} a(k)$.
background
The module implements running-max normalization for the Navier-Stokes regularity argument (NS Paper §3, Step 1). It extracts ancient elements from a sequence of times $t_n → T^*$ with sup-norms $M_n → ∞$ by rescaling fields to satisfy $‖ω̃(·,t_n)‖{L^∞} ≤ 1$. The running maximum is the sibling definition $M̃(n) = max{k ≤ n} a(k)$ supplied by runningMax.
proof idea
One-line wrapper that applies the runningMax definition and performs the division.
why it matters
The definition fills the first normalization step in the Navier-Stokes regularity construction. It is referenced by canonicalCostAlgebra, CostAlgebraData, and cost_algebra_unique in the CostAlgebra module, where the same pattern supplies the normalized cost at the identity. The construction is standard real-analysis scaffolding and aligns with the scale-invariant properties required by the eight-tick octave and J-uniqueness (T5) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.