normalized_bounded
plain-language theorem explainer
The theorem shows that any positive sequence M from naturals to reals yields a normalized version bounded above by 1. Navier-Stokes regularity researchers cite it to guarantee scale-invariant sup-norms when extracting limits from hypothetical blowup sequences. The proof is a one-line wrapper applying the sibling vorticity boundedness result.
Claim. Let $M:ℕ→ℝ$ satisfy $M(n)>0$ for every $n$. Then the normalized sequence satisfies $N(n)≤1$ for all $n$, where $N$ is obtained by dividing each term by the running maximum up to that index.
background
The module constructs running-max normalization to produce scale-invariant fields from a hypothetical blowup sequence $M_n=‖ω(·,t_n)‖{L^∞}$ with $M_n→∞$. The running maximum is defined as the monotone envelope $M̃(t)=sup{s≤t}M(s)$, after which the normalized fields satisfy $‖ω̃‖_{L^∞}≤1$ by construction. This step uses only monotone sequence properties and is independent of Recognition Science constants such as the J-cost or phi-ladder.
proof idea
The proof is a one-line wrapper that applies normalized_vorticity_bounded to the positive sequence M and the positivity hypothesis.
why it matters
The result supplies the boundedness clause inside runningMaxCert, which collects the four properties (monotonicity, boundedness, TF pinch, rigid rotation) required for the Navier-Stokes regularity argument in NS Paper §3 Step 1. It closes the normalization construction before the TF pinch at zero node is invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.