rmsSq
plain-language theorem explainer
The definition computes the average of squared amplitudes for a scalar field on a finite lattice. Discrete fluid dynamics work in Recognition Science cites it when bounding J-cost changes under vorticity evolution. It is realized as a direct normalization of the total sum of squares by site count.
Claim. For a scalar field $f$ on $N$ sites, the mean squared amplitude is given by $rmsSq(f) = N^{-1} sum_{i=1}^N f(i)^2$.
background
The module supplies exact bookkeeping objects for finite vorticity fields on a lattice window, including totals, RMS measures, and decompositions of J-cost derivatives into transport, viscous, and stretching contributions. The local theoretical setting deliberately isolates this discrete surface from the hard PDE inequalities so lemmas can be added incrementally. The upstream total definition supplies the summation operator over Fin siteCount.
proof idea
One-line wrapper that applies total to the pointwise squared field and divides by siteCount.
why it matters
This supplies the squared RMS component that feeds the rms amplitude definition in the same module. It supports the J-cost monotonicity program by furnishing exact amplitude measures for discrete Navier-Stokes bookkeeping, consistent with convex J-cost minimization and local 8-tick dynamics from upstream PhiForcingDerived and PhysicsComplexityStructure structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.