rescaleLength_tendsto_zero
plain-language theorem explainer
If a sequence of reals diverges to infinity then its rescaling factor, defined as the reciprocal square root of the running maximum, tends to zero. Navier-Stokes regularity analysts cite the result when constructing bounded normalized fields from a hypothetical blow-up sequence. The proof is a direct epsilon-N argument that invokes the running-max divergence lemma and compares square roots via field arithmetic.
Claim. Let $a : ℕ → ℝ$ satisfy $a(n) → +∞$ as $n → ∞$. Then the rescaling factor $1 / √{runningMax(a)(n)}$ tends to 0 as $n → ∞$.
background
The module formalizes the running-max normalization step in the Navier-Stokes regularity argument (NS Paper §3, Step 1). A sequence of sup-norms $M_n = ‖ω(·,t_n)‖{L^∞}$ with $M_n → ∞$ yields the running maximum $M̃(n) = sup{k ≤ n} M(k)$ and the normalized fields scaled by $1/M̃(n)$. The rescaling length is the reciprocal square root of this running maximum, guaranteeing scale-invariant bounds. The construction uses only monotone-sequence properties and requires no additional structure beyond the imported Mathlib analysis library.
proof idea
Apply the upstream lemma runningMax_tendsto_atTop to obtain divergence of the running maximum. Unfold Metric.tendsto_nhds and Filter.tendsto_atTop_atTop. For given ε > 0 choose N so the running maximum exceeds (1/ε)^2 + 1. The remainder of the argument compares 1/ε with the square root via sqrt_lt_sqrt and verifies the distance inequality by field_simp and mul_lt_mul_of_pos_left.
why it matters
The theorem completes the first normalization step that produces bounded ancient elements for the Navier-Stokes regularity proof. It directly supports the subsequent claim that the normalized vorticity satisfies ‖ω̃_n‖ ≤ 1. The result aligns with the standard Caffarelli-Kohn-Nirenberg extraction procedure and sits inside the eight-tick octave framework of Recognition Science, though no downstream theorems yet invoke it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.