normalized_bounded
plain-language theorem explainer
For any positive sequence of real numbers indexed by naturals, the version normalized by its running maximum satisfies an upper bound of one at every step. Analysts studying potential singularities in the Navier-Stokes equations cite this to validate the rescaling that produces ancient solutions with controlled norms. The argument reduces directly to a prior boundedness result on the normalized vorticity field.
Claim. Let $M : ℕ → ℝ$ satisfy $M(n) > 0$ for every natural number $n$. Let $˜M$ denote the sequence obtained by dividing each $M(n)$ by the running maximum of the sequence up to index $n$. Then $˜M(n) ≤ 1$ for all $n$.
background
This module develops the running-max normalization procedure for sequences of sup-norms arising in hypothetical blowups of Navier-Stokes solutions. The running maximum at step n is the supremum of M(k) for k ≤ n, and normalization divides the field by this value to produce a scale-invariant object whose L^∞ norm is at most 1. The local setting is the extraction of ancient solutions as in the Caffarelli-Kohn-Nirenberg approach, relying only on properties of monotone sequences and suprema.
proof idea
The proof is a one-line wrapper that applies the normalized_vorticity_bounded lemma to the input sequence and positivity hypothesis.
why it matters
This boundedness statement is invoked inside the runningMaxCert theorem to establish the full certificate for the running-max construction, including monotonicity and the topological frustration pinch at zero nodes. It completes the normalization step in the Navier-Stokes regularity argument of the Recognition Science framework, ensuring rescaled vorticity remains controlled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.