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 -
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