pith. machine review for the scientific record. sign in
def definition def or abbrev high

normalized

show as:
view Lean formalization →

The normalized definition constructs the rescaled sequence ã(n) = a(n) / runningMax(a)(n) for any real-valued sequence a on the naturals. Navier-Stokes analysts would cite it when rescaling a hypothetical blow-up sequence of vorticity sup-norms to produce a bounded ancient solution. The definition is a direct one-line quotient by the running maximum, which itself is the finite supremum over the initial segment.

claimLet $a : ℕ → ℝ$. The normalized sequence is defined by $ã(n) := a(n) / M̃(n)$, where $M̃(n) = max_{k ≤ n} a(k)$.

background

The module formalizes running-max normalization for the Navier-Stokes regularity argument, specifically to extract ancient elements from a blowing-up sequence of times tₙ → T* with Mₙ = ‖ω(·,tₙ)‖{L^∞} → ∞. The running maximum is supplied by the upstream definition runningMax a n := Finset.sup' (Finset.range (n+1)) (Finset.nonempty_range_add_one) a, which returns the maximum of a over the finite initial segment. The local theoretical setting is pure real analysis on monotone sequences and suprema, as stated in the module documentation: it is the standard construction of Caffarelli-Kohn-Nirenberg and Escauriaza-Seregin-Šverák that yields ‖ω̃(·,tₙ)‖{L^∞} ≤ 1 by construction.

proof idea

The definition is a one-line wrapper that applies the upstream runningMax: it simply divides the current term a n by runningMax a n. No tactics or lemmas beyond the definition of runningMax are required.

why it matters in Recognition Science

This supplies the scale-invariant normalization step in NS Paper §3 Step 1. It feeds the downstream CostAlgebraData structure (canonicalCostAlgebra, cost_algebra_unique) where the same normalization pattern appears for the J-cost function satisfying the Recognition Composition Law. The construction directly supports the T5 J-uniqueness claim in the forcing chain by guaranteeing a bounded normalized sequence with |ã| ≤ 1, and it closes the scaffolding for the boundedness claim in the Navier-Stokes regularity argument.

scope and limits

formal statement (Lean)

  70noncomputable def normalized (a : ℕ → ℝ) (n : ℕ) : ℝ :=

proof body

Definition body.

  71  a n / runningMax a n
  72
  73/-- The normalized sequence is bounded by 1 in absolute value. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.