runningMaxCert
plain-language theorem explainer
runningMaxCert certifies that the running-max normalization for hypothetical Navier-Stokes blowup sequences satisfies monotonicity, unit boundedness after rescaling, the TF pinch property for the J-cost, and exclusion of rigid rotations by infinite energy. Navier-Stokes regularity researchers cite it when building scale-invariant ancient profiles from diverging sup-norms. The proof is a direct term-mode record that assembles four upstream lemmas.
Claim. Let $M_n$ be a sequence of $L^∞$ vorticity norms diverging to infinity. The running maximum is monotone non-decreasing. Normalization by this running maximum yields rescaled vorticity with supremum norm at most 1. A convex J-cost vanishing at 1 and positive elsewhere on $(0,∞)$ has unique zero at 1. Nonzero constant vorticity produces a rigid rotation whose kinetic energy diverges on expanding balls.
background
The module formalizes running-max normalization for the Navier-Stokes regularity argument (NS Paper §3, Step 1). Given times $t_n → T^*$ and $M_n = ‖ω(·,t_n)‖∞ with $M_n → ∞$, one defines the running maximum $M̃(t) = sup{s≤t} M(s)$ and rescaled fields $ũ(x,t) = u(x,t)/M̃(t_n)$. The structure RunningMaxCert packages the four properties needed to extract an ancient limit element: monotonicity of the running max, boundedness of the normalized sequence, the TF pinch at zero nodes, and infinite energy of rigid rotations.
proof idea
The proof is a term-mode structure instantiation. It supplies the monotone field by runningMax_mono, the bounded field by normalized_bounded, the tf_pinch field by tf_pinch_at_zero_node, the rigid_rotation field by constant_vorticity_implies_rigid_rotation, and the rigid_rotation_energy_diverges field by rigid_rotation_infinite_energy_proved.
why it matters
This theorem completes the certification of the running-max normalization step in the Navier-Stokes regularity proof. It directly supports extraction of scale-invariant blowup profiles and relies on the TF pinch (unique zero of J at 1) together with the rigid-rotation energy divergence. The construction sits inside the broader Recognition Science program that derives D=3 and the alpha band from the J-uniqueness and phi-ladder axioms, though the present module remains within classical real analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.