rescaleLength_pos
plain-language theorem explainer
rescaleLength_pos asserts that the rescaling factor λ_n = 1/sqrt(running maximum of sequence a at n) is positive whenever a_n > 0. Navier-Stokes regularity researchers cite it when building normalized fields from hypothetical blow-up sequences. The proof is a term-mode one-liner that unfolds the definition and chains div_pos with sqrt positivity applied to runningMax_pos.
Claim. Let $a : ℕ → ℝ$ and $n ∈ ℕ$ with $a_n > 0$. Let $M_n$ denote the running supremum of the sequence $a$ up to index $n$. Then the rescaling factor $λ_n := 1/√M_n$ satisfies $λ_n > 0$.
background
The module implements running-max normalization for the Navier-Stokes regularity argument (NS Paper §3 Step 1). Given a sequence of times $t_n → T^*$ with diverging sup-norms $M_n = ‖ω(·,t_n)‖∞, it forms the running maximum $M̃(t) = sup{s≤t} M(s)$, normalizes fields by division by $M̃(t_n)$, and rescales coordinates via $x ↦ x/λ_n$, $t ↦ t/λ_n²$ to obtain scale-invariant bounds ‖ω̃‖_∞ ≤ 1.
proof idea
Unfolds the definition of rescaleLength to expose division by the square root of the running maximum. Applies the lemma that division preserves positivity (with the constant 1) and the square-root positivity map to the conclusion of runningMax_pos.
why it matters
It supplies a basic positivity fact inside the proved normalization toolkit (module status: proved, zero sorry) that supports construction of bounded normalized vorticity fields. The result fills a prerequisite step in NS Paper §3 Step 1 but does not connect to the Recognition Science forcing chain, RCL, or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.