module module high

`IndisputableMonolith.NavierStokes.RunningMaxNormalization`

This module defines the running maximum operator on sequences together with normalization and rescaling auxiliaries for Navier-Stokes analysis. Researchers bounding vorticity or solution norms in fluid models would reference these constructions. The module supplies the core object M̃(n) = max_{k≤n} a(k) plus monotonicity, positivity, and convergence lemmas that follow directly from the definition.

claimLet $M̃(n) := max_{k ≤ n} a(k)$ be the running maximum of a real sequence $a$. The module also introduces the normalized sequence $a(n)/M̃(n)$ (equal to 1 at maxima) and a positive rescaling length function that tends to zero at infinity.

background

The module sits inside the NavierStokes domain of the Recognition Science development. It works with discrete sequences that represent quantities such as vorticity magnitude or energy norms. The central definition is the running maximum, written M̃(n), which records the largest value attained up to index n. Companion definitions include a normalized version that maps the sequence into [0,1] and a length-rescaling map whose limit is zero. All constructions rely only on the ordered field structure of the reals supplied by Mathlib.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The constructions supply the normalization layer required for boundedness statements in the Navier-Stokes regularity program. They feed the sibling result normalized_vorticity_bounded and any later global existence or blow-up criteria that rely on controlled suprema. Within the larger Recognition framework the module therefore supplies the concrete sequence tools that sit beneath claims about spatial dimension D=3 and the eight-tick octave.

scope and limits

Does not prove existence or uniqueness of Navier-Stokes solutions.
Does not invoke the J-cost function or Recognition Composition Law.
Does not derive physical constants such as alpha or G.
Applies only to discrete sequences, not to continuous-time flows.

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