module module moderate

`IndisputableMonolith.NavierStokes.RunningMaxNormalization`

The module defines the running maximum of a sequence and associated normalization tools for use in Navier-Stokes formalizations. Researchers handling sequence bounds or vorticity estimates in fluid dynamics would reference these auxiliaries. It supplies the core object M̃(n) = max_{k≤n} a(k) together with monotonicity, positivity, and normalized variants. The module is purely definitional with basic supporting lemmas.

claim$M̃(n) := max_{k≤n} a(k)$, normalized sequence $â(n) := a(n)/M̃(n)$ obeying $â(n) ≤ 1$ with equality at the running-max index, plus rescaling length $L(n)$ with $L(n) → 0$.

background

The module sits inside the Navier-Stokes domain and imports Mathlib for real analysis. It introduces the running-maximum operator on sequences a : ℕ → ℝ, together with its monotonicity, positivity preservation, and limit-to-infinity behavior. Normalization produces a bounded sequence, while rescaleLength supplies a vanishing length scale. These objects prepare boundedness arguments for vorticity or similar quantities.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions supply the normalization infrastructure required by downstream Navier-Stokes results on bounded vorticity. They implement the technical step that converts potentially unbounded sequences into unit-bounded ones while preserving key monotonicity and positivity properties.

scope and limits

Does not treat continuous-time running maxima.
Does not prove convergence of arbitrary input sequences.
Does not invoke Recognition Science constants or the phi-ladder.
Does not address multi-dimensional or vector-valued extensions.

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