rms
The root-mean-square amplitude of a real scalar field sampled on a finite lattice of N sites is defined as the square root of the average of the squared field values. Researchers modeling discrete vorticity or fluid flows inside the Recognition Science J-cost monotonicity program cite this when they normalize local amplitudes against the global scale of the field. The definition is obtained by a direct one-line application of the real square root to the mean-square quantity already present in the same module.
claimLet $f$ be a real-valued function on a finite set of $N$ sites. The RMS amplitude is $sqrt( (1/N) sum_i f(i)^2 )$.
background
The Discrete Vorticity module packages exact bookkeeping objects for finite vorticity fields on a lattice window. These objects comprise total, RMS, and normalized amplitudes together with transport, viscous, and stretching contribution fields, all in service of an exact decomposition of the J-cost derivative. The hard PDE inequalities are kept separate so they can be added lemma by lemma. This RMS definition is built directly on the mean-square quantity that averages the squared field values over the sites. Upstream material includes the phi-powered scale function from large-scale structure and the bounded normalized sequence from running-max normalization.
proof idea
The definition is a one-line wrapper that applies the real square root function to the output of the mean-square definition.
why it matters in Recognition Science
This supplies the RMS scale used by the normalized-amplitude definition, which in turn supports the total J-cost computation relative to that scale. It therefore participates in the discrete bookkeeping layer that precedes J-cost monotonicity statements for Navier-Stokes vorticity. The surrounding Recognition Science framework invokes the Recognition Composition Law and the eight-tick octave to constrain the underlying phi-ladder, yet this algebraic definition remains independent of those constants.
scope and limits
- Does not extend to continuous fields or take limits as site count grows.
- Does not embed the phi-ladder cutoff or running normalization from sibling modules.
- Does not compute any J-cost or monotonicity statement.
- Does not distinguish vorticity from a general scalar field.
Lean usage
def normalizedAmplitude {N : ℕ} (f : Fin N → ℝ) (i : Fin N) : ℝ := |f i| / rms fformal statement (Lean)
40def rms {siteCount : ℕ} (f : Fin siteCount → ℝ) : ℝ :=
proof body
Definition body.
41 Real.sqrt (rmsSq f)
42
43/-- Pointwise normalized amplitude relative to the RMS scale. -/