normalized_bounded
Normalized vorticity remains bounded by 1 for every index when the input sequence M is strictly positive. Researchers on Navier-Stokes regularity cite the bound to control rescaled fields during extraction of ancient solutions from blowup sequences. The argument is a direct one-line application of the sibling lemma normalized_vorticity_bounded.
claimLet $M : ℕ → ℝ$ satisfy $M(n) > 0$ for all $n$. Let $˜M(n)$ denote the sequence normalized by its running maximum, i.e., $˜M(n) = M(n) / sup_{k ≤ n} M(k)$. Then $˜M(n) ≤ 1$ for all $n$.
background
The module constructs the running-max normalization for Navier-Stokes regularity analysis. Given a sequence of sup-norms $M_n = ‖ω(·, t_n)‖_{L^∞}$ that diverges, the running maximum is the pointwise supremum up to each time, and the normalized vorticity is obtained by dividing the original field by this supremum on rescaled coordinates. The construction yields scale-invariant fields whose $L^∞$ norm is at most 1 by design, relying only on monotonicity of the supremum and positivity of the sequence.
proof idea
The proof is a one-line wrapper that applies normalized_vorticity_bounded to the inputs M and the positivity hypothesis hpos.
why it matters in Recognition Science
The theorem supplies the boundedness component of runningMaxCert, which certifies the full set of properties (monotonicity, boundedness, TF pinch, rigid rotation) needed for the running-max construction. It completes the scale-invariant bound step in the Navier-Stokes regularity argument that extracts ancient elements from hypothetical blowup sequences. In the Recognition Science setting this supports the topological-frustration analysis of vorticity within the forcing-chain framework.
scope and limits
- Does not establish global existence of smooth solutions.
- Does not decide whether blowup occurs for arbitrary initial data.
- Does not supply convergence rates for the normalized sequence.
- Does not extend the bound to compressible or magnetohydrodynamic flows.
formal statement (Lean)
136theorem normalized_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) :
137 ∀ n, normalized M n ≤ 1 :=
proof body
Term-mode proof.
138 fun n => normalized_vorticity_bounded M hpos n
139
140/-! ## TF Pinch at Zero Node (Thm 5.5) -/
141
142/-- **TF Pinch at a zero node**: if the J-cost function J(x) has a zero at
143 x₀ in the interior of the domain, then the vorticity direction is constant
144 in a neighborhood of x₀.
145
146 This is pure convex analysis: J is strictly convex (J'' > 0), so
147 J(x₀) = 0 implies x₀ = 1 (the unique minimum). At x = 1, the vorticity
148 direction is determined by the leading-order quadratic expansion J ≈ ε²/2.
149
150 In RS: the TF (topological frustration) prevents simultaneous vanishing of
151 both the vorticity magnitude and direction — one of them must persist. -/