normalizedAmplitude
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.