module module high

`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 L33
theorem runningMax_ge L38
theorem runningMax_mono L45
theorem runningMax_tendsto_atTop L53
theorem runningMax_pos L62
def normalized L70
theorem normalized_le_one L74
theorem normalized_eq_one_at_max L80
def rescaleLength L91
theorem rescaleLength_pos L95
theorem rescaleLength_tendsto_zero L102
theorem normalized_vorticity_bounded L130
theorem normalized_bounded L136
theorem tf_pinch_at_zero_node L152
theorem constant_vorticity_implies_rigid_rotation L169
def rigid_rotation_infinite_energy L186
theorem rigid_rotation_energy_lower_bound L190
theorem rigid_rotation_infinite_energy_proved L287
structure RunningMaxCert L335
theorem runningMaxCert L353