rescaleLength_pos
The positivity of the rescaling length factor follows from the positivity of the running maximum via square-root and division rules. Analysts constructing normalized ancient solutions from hypothetical Navier-Stokes blow-up sequences cite this lemma to guarantee a well-defined positive scale factor. The proof is a one-line term-mode reduction that unfolds the definition and applies standard positivity facts for division and square roots.
claimLet $a : ℕ → ℝ$, $n ∈ ℕ$, and suppose $a_n > 0$. Then $0 < λ_n$ where $λ_n = 1 / √(sup_{k ≤ n} a_k)$.
background
The module implements the running-max normalization step in the Navier-Stokes regularity argument. The running maximum of sequence a up to index n is the least upper bound of the values a_0 through a_n. The rescaling length is defined as the reciprocal of the square root of this running maximum and is used to rescale space by λ_n and time by λ_n² so that the normalized vorticity satisfies a uniform L^∞ bound of 1.
proof idea
The term proof unfolds the definition of rescaleLength to expose the division 1 / √(runningMax a n), applies the lemma div_pos with the constant 1 shown positive, and closes by invoking Real.sqrt_pos.mpr on the runningMax_pos theorem applied to the hypothesis 0 < a n.
why it matters in Recognition Science
The lemma supplies the positivity needed for the rescaling construction in the Navier-Stokes blow-up analysis. It directly supports the extraction of ancient elements with bounded normalized vorticity as described in the module documentation. No downstream uses are recorded yet; the result closes a basic positivity obligation in the normalization pipeline.
scope and limits
- Does not prove existence of any blow-up sequence.
- Does not verify that the rescaled fields satisfy the Navier-Stokes equations.
- Does not provide an upper bound on the rescaling length.
formal statement (Lean)
95theorem rescaleLength_pos (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
96 0 < rescaleLength a n := by
proof body
Term-mode proof.
97 unfold rescaleLength
98 apply div_pos one_pos
99 exact Real.sqrt_pos.mpr (runningMax_pos a n h)
100
101/-- The rescaling factor tends to 0 as the running max diverges. -/