runningMax_pos
plain-language theorem explainer
The running maximum of a real sequence remains positive whenever any term is positive. Navier-Stokes regularity analysts cite it when constructing normalized fields from blow-up sequences to keep the rescaling factor well-defined. The proof is a one-line wrapper applying the monotonicity lemma runningMax_ge via lt_of_lt_of_le.
Claim. Let $a : ℕ → ℝ$ be a sequence and $n ∈ ℕ$. If $a(n) > 0$, then the running maximum of $a$ up to index $n$ satisfies $0 <$ running maximum of $a$ up to $n$.
background
The module implements running-max normalization for the Navier-Stokes regularity argument (NS Paper §3, Step 1). Given a sequence $a : ℕ → ℝ$ with values representing sup-norms that may diverge, the running maximum is the monotone envelope $M̃(n) = sup_{k ≤ n} a(k)$. This ensures the normalized sequence ã(n) = a(n) / M̃(n) satisfies |ã(n)| ≤ 1 by construction, a standard device also appearing in Caffarelli-Kohn-Nirenberg and Escauriaza-Seregin-Šverák arguments. The local setting is pure real analysis on monotone sequences; upstream results supply the Normalization axiom (cost vanishes at unity) and the runningMax definition itself.
proof idea
The proof is a one-line wrapper that applies the lemma runningMax_ge a n (which asserts a n ≤ runningMax a n) to the hypothesis 0 < a n via the transitivity lemma lt_of_lt_of_le.
why it matters
This result directly supports the three downstream theorems in the same module: normalized_le_one, normalized_eq_one_at_max, and rescaleLength_pos. Those close the normalization step that produces bounded ancient solutions from hypothetical blow-ups, feeding the scale-invariant properties required by the Recognition framework's forcing chain (T5 J-uniqueness through T8 D=3). It supplies the positivity half of the unit-maximum claim in the NS paper construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.