RunningMaxCert
plain-language theorem explainer
RunningMaxCert bundles the five analytic properties required to normalize a hypothetical Navier-Stokes blow-up sequence by its running maximum and extract an ancient solution with unit-bounded vorticity. A researcher working on the Recognition Science derivation of the regularity criterion cites this certificate when rescaling the vorticity field and passing to the limit. The definition is assembled directly from five sibling lemmas already established in the module.
Claim. A structure asserting: (i) the running-maximum function on any real sequence is monotone; (ii) normalization of a positive sequence by its running maximum yields a rescaled sequence bounded above by 1; (iii) any convex cost function $J$ on $(0,∞)$ that vanishes at 1 and is strictly positive elsewhere has its only zero at 1; (iv) every constant-vorticity field is realized by a rigid rotation; (v) every nonzero rigid rotation produces quartically divergent energy on expanding balls.
background
The module formalizes the running-max normalization used in the Navier-Stokes regularity proof to extract ancient elements from a blowing-up sequence. Given times $t_n→T^*$ with sup-norms $M_n=‖ω(·,t_n)‖{L^∞}$ tending to infinity, one defines the running maximum $M̃(t)=sup{s≤t}M(s)$ and the normalized fields $ũ(x,t)=u(x,t)/M̃(t_n)$ on rescaled coordinates so that $‖ω̃(·,t_n)‖_{L^∞}≤1$ by construction. This is standard monotone-sequence analysis and requires only sup properties together with the Normalization axiom from CostAxioms, which encodes that the cost functional vanishes at unity.
proof idea
The structure is a direct bundling of five sibling lemmas: runningMax_mono supplies monotonicity, normalized_bounded supplies the unit bound, tf_pinch_at_zero_node supplies the J-cost uniqueness statement, constant_vorticity_implies_rigid_rotation supplies the rigid-rotation representation, and rigid_rotation_infinite_energy_proved supplies the energy-divergence claim via an integral lower bound on the unit ball followed by quartic scaling.
why it matters
This certificate is the direct input to the theorem runningMaxCert that constructs the normalized ancient solution. It fills the first step of the Navier-Stokes regularity argument in the Recognition Science framework, ensuring that any hypothetical blow-up can be rescaled to a limit satisfying the ancient-solution equation with bounded vorticity. The rigid-rotation energy divergence closes the contradiction for constant profiles, consistent with the three-dimensional spatial structure forced by the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.