runningMaxCert
The runningMaxCert theorem certifies that the running-max normalization on sup-norms satisfies monotonicity, produces rescaled fields bounded by 1, enforces unique zero of the convex J-cost at 1, and excludes nonzero rigid rotations by infinite energy on expanding balls. Navier-Stokes regularity researchers cite it when constructing scale-invariant ancient solutions from hypothetical blowup sequences. The proof is a direct term-mode structure instantiation supplying the four fields from sibling lemmas.
claimThe running-max operator on a sequence of positive sup-norms is monotone; normalization by this running max yields rescaled vorticity bounded by 1 in $L^∞$; any zero of a convex J-cost on $(0,∞)$ with strict positivity away from 1 must occur uniquely at 1; nonzero constant-vorticity fields are rigid rotations with infinite energy on expanding balls.
background
The module formalizes running-max normalization for Navier-Stokes regularity (NS paper §3, Step 1). Given times $t_n → T^*$ with $M_n = ‖ω(·,t_n)‖{L^∞} → ∞$, it builds the running maximum $M̃(t) = sup{s≤t} M(s)$ and normalized fields $ũ(x,t) = u(x,t)/M̃(t_n)$ so that $‖ω̃(·,t_n)‖_{L^∞} ≤ 1$. Key sibling definitions are runningMax (supremum over prior terms) and normalized (rescaling by the running max). The tf_pinch field encodes convex analysis: J strictly convex on $(0,∞)$ with J(1)=0 forces the unique zero at 1. Upstream lemmas include constant_vorticity_implies_rigid_rotation (constant vorticity yields rigid rotation via 2D Biot-Savart) and rigid_rotation_infinite_energy_proved (nonzero rotations diverge in energy).
proof idea
The proof is a term-mode structure instantiation of RunningMaxCert. It directly assigns the monotone field from runningMax_mono, the bounded field from normalized_bounded, the tf_pinch field from tf_pinch_at_zero_node, and the rigid_rotation_energy_diverges field from rigid_rotation_infinite_energy_proved. No further tactics or reductions occur.
why it matters in Recognition Science
This theorem completes the certification of the running-max normalization in the Navier-Stokes module, supplying the four properties required for extracting ancient limits from blowup sequences (NS paper §3 Step 1). It incorporates the TF pinch at zero node and rigid-rotation exclusion, linking to J-cost uniqueness (T5). No downstream uses are recorded, but it closes the normalization scaffolding before limit extraction.
scope and limits
- Does not prove existence of any blowup sequence.
- Does not address full 3D Navier-Stokes regularity.
- Does not treat non-monotone or non-positive sequences.
- Does not extend rigid-rotation exclusion beyond constant vorticity.
formal statement (Lean)
353theorem runningMaxCert : RunningMaxCert where
354 monotone := runningMax_mono
proof body
Term-mode proof.
355 bounded := normalized_bounded
356 tf_pinch := tf_pinch_at_zero_node
357 rigid_rotation := constant_vorticity_implies_rigid_rotation
358 rigid_rotation_energy_diverges := rigid_rotation_infinite_energy_proved
359
360end RunningMaxNormalization
361end NavierStokes
362end IndisputableMonolith