normalizedAmplitude
This definition supplies the pointwise normalized amplitude of a discrete vorticity field on a finite lattice, obtained by dividing the absolute value at each site by the field's root-mean-square scale. Researchers constructing the J-cost monotonicity argument for discrete Navier-Stokes would cite it when normalizing local contributions before summation. It is realized directly as the quotient of the site absolute value by the global RMS of the field.
claimLet $f$ be a real-valued function on a finite set of $N$ sites. The normalized amplitude at site $i$ is $|f(i)|$ divided by the root-mean-square value of $f$.
background
The Discrete Vorticity module packages exact bookkeeping for finite vorticity fields on a lattice window. It introduces total, RMS, and normalized amplitudes along with transport, viscous, and stretching contribution fields to support an exact decomposition of the J-cost derivative. The module deliberately isolates these discrete objects from the continuous PDE inequalities so that lemmas can be added incrementally.
proof idea
The definition is a one-line wrapper that applies the absolute value at the selected site and divides by the RMS of the full field.
why it matters in Recognition Science
This definition is invoked by totalJcost to obtain the total J-cost of a discrete vorticity field relative to its RMS scale. It completes the bookkeeping layer required for the J-cost monotonicity program in the Navier-Stokes module. Within Recognition Science it preserves the exact cost structure derived from the multiplicative recognizer while preparing the discrete approximation to vorticity evolution.
scope and limits
- Does not prove any inequality or monotonicity property of the J-cost.
- Does not address the continuous limit or the full Navier-Stokes PDE.
- Does not incorporate phi-ladder cutoffs or spectral emergence.
- Does not compute time derivatives or evolution identities.
Lean usage
total (fun i => Jcost (normalizedAmplitude f i))formal statement (Lean)
44def normalizedAmplitude {siteCount : ℕ} (f : Fin siteCount → ℝ) (i : Fin siteCount) : ℝ :=
proof body
Definition body.
45 |f i| / rms f
46
47/-- The total J-cost of a discrete vorticity field relative to its RMS scale. -/