IndisputableMonolith.NavierStokes.RunningMaxNormalization
This module defines the running maximum of a sequence along with normalization and rescaling auxiliaries for Navier-Stokes analysis in Recognition Science. It establishes monotonicity, positivity, and limit properties of the running max and normalized forms. The module functions as a utility library supplying bounded-sequence tools for fluid-dynamics arguments.
claimLet $M̃(n) := max_{k≤n} a(k)$ be the running maximum. The normalized sequence satisfies $â(n) ≤ 1$ with equality at the point of maximum, while the rescaled length $ℓ(n) > 0$ obeys $ℓ(n) → 0$ as $n → ∞$.
background
This module belongs to the NavierStokes domain and supplies sequence-normalization primitives. Its central object is the running maximum, defined pointwise as the maximum value attained by the sequence up to index n. Companion definitions produce a normalized version bounded above by one and a positive rescaling function that vanishes at infinity. The module imports Mathlib to access basic facts about real sequences and maxima.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the running-maximum and normalization primitives that support Navier-Stokes analysis inside the Recognition Science framework. It enables construction of bounded normalized quantities such as vorticity and thereby feeds the broader development of fluid-dynamics results under the Recognition Composition Law.
scope and limits
- Does not prove existence or uniqueness for the Navier-Stokes equations.
- Does not reference the J-function, phi-ladder, or forcing chain T0-T8.
- Does not supply numerical values or physical constants.
declarations in this module (20)
-
def
runningMax -
theorem
runningMax_ge -
theorem
runningMax_mono -
theorem
runningMax_tendsto_atTop -
theorem
runningMax_pos -
def
normalized -
theorem
normalized_le_one -
theorem
normalized_eq_one_at_max -
def
rescaleLength -
theorem
rescaleLength_pos -
theorem
rescaleLength_tendsto_zero -
theorem
normalized_vorticity_bounded -
theorem
normalized_bounded -
theorem
tf_pinch_at_zero_node -
theorem
constant_vorticity_implies_rigid_rotation -
def
rigid_rotation_infinite_energy -
theorem
rigid_rotation_energy_lower_bound -
theorem
rigid_rotation_infinite_energy_proved -
structure
RunningMaxCert -
theorem
runningMaxCert