normalized
plain-language theorem explainer
The normalized sequence ã(n) = a(n) / runningMax(a)(n) is defined for any real-valued sequence a on the naturals. Navier-Stokes regularity analysts cite it when rescaling a hypothetical blowup sequence to produce a bounded ancient solution with sup-norm at most 1. The definition is a direct one-line division by the running maximum supplied by the sibling runningMax.
Claim. Let $a : ℕ → ℝ$. Define the normalized sequence by $ã(n) := a(n) / M̃(n)$, where $M̃(n) = max_{k ≤ n} a(k)$.
background
The running maximum is defined by runningMax a n := Finset.sup' (Finset.range (n+1)) (Finset.nonempty_range_add_one) a, so that M̃(n) ≥ a(n) for every n. The module sets this construction inside the Navier-Stokes regularity argument (NS Paper §3, Step 1): given a sequence of times tₙ → T* with Mₙ = ‖ω(·,tₙ)‖{L^∞} → ∞, the normalized fields ũ = u / M̃(tₙ) are scale-invariant and satisfy ‖ω̃‖{L^∞} ≤ 1 by construction. This is the standard discrete-time preparation for the Caffarelli-Kohn-Nirenberg / Escauriaza-Seregin-Šverák ancient-solution extraction.
proof idea
one-line wrapper that applies runningMax: the body is exactly a n / runningMax a n.
why it matters
The definition supplies the scale-invariant normalization step required to pass from a hypothetical blowup sequence to a bounded ancient solution in the Navier-Stokes regularity proof. It is referenced by canonicalCostAlgebra and CostAlgebraData in the algebra layer, where the same normalization property (cost at identity equals zero) appears as the axiom normalized := J_at_one. The construction therefore bridges the real-analysis preparation in the NS module to the Recognition Composition Law uniqueness results (T5) that characterize J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.