rescaleLength_tendsto_zero
plain-language theorem explainer
If a sequence of reals diverges to positive infinity then its running-max rescaling factor converges to zero in the reals. Navier-Stokes analysts cite the result when constructing normalized ancient solutions from a hypothetical blow-up sequence. The proof is an epsilon-delta argument that invokes the running-max divergence lemma and then applies square-root monotonicity together with the metric definition of neighborhood convergence.
Claim. Let $a : ℕ → ℝ$ satisfy $a_n → +∞$ as $n → ∞$. Define the rescaling length by $ℓ(n) := 1 / √(sup_{k ≤ n} a_k)$. Then $ℓ(n) → 0$ as $n → ∞$.
background
The module implements the first step of the running-max normalization used in the Navier-Stokes regularity argument (NS Paper §3). Given a sequence $a_n$ of sup-norms that diverges, the running maximum is the monotone envelope $M(n) = sup_{k ≤ n} a_k$. The rescaling length is then the reciprocal square root $1/√M(n)$, which normalizes the vorticity so that its $L^∞$ norm is at most 1 on the rescaled coordinates. The local setting is pure real analysis: only monotonicity of the running max and the definition of convergence at infinity are required. The key upstream fact is the sibling lemma that the running max itself tends to infinity whenever the original sequence does.
proof idea
The tactic proof first calls the running-max divergence lemma to obtain that the running max tends to infinity. It then unfolds the metric definition of convergence to the zero neighborhood. For arbitrary ε > 0 it selects N large enough that the running max exceeds (1/ε)² + 1, after which positivity of the square root and the inequality √x > 1/ε together imply that the rescaled length is strictly less than ε for all n ≥ N.
why it matters
The declaration supplies the vanishing of the rescaling factor required to extract a bounded ancient element from any hypothetical blow-up sequence. It therefore feeds the sibling statement that the normalized vorticity remains bounded by 1. In the Recognition Science framework this completes the normalization step that precedes the application of the Caffarelli-Kohn-Nirenberg-type regularity criterion. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.