normalizedRatio
plain-language theorem explainer
The normalized ratio extracts the vorticity scale ratio from any finite-volume profile on an RS lattice. Navier-Stokes regularity researchers cite it when passing lattice cutoffs into conditional completion arguments. It is introduced as the direct quotient of the maximum and RMS vorticity fields packaged in the profile.
Claim. Let $s$ be a finite-volume vorticity profile. The normalized ratio is the quotient of its maximum vorticity to its root-mean-square vorticity.
background
A FiniteVolumeProfile consists of a positive site count, positive omegaMax and omegaRms with omegaRms ≤ omegaMax, and the finite-volume control inequality omegaMax ≤ sqrt(siteCount) * omegaRms. This structure encodes the norm equivalence on a finite RS lattice, where pointwise amplitude is controlled by the RMS scale times the square root of the number of sites.
proof idea
The definition is a direct field projection that returns the quotient of the omegaMax and omegaRms components of the input profile.
why it matters
This definition supplies the input to the finiteVolume_Jcost_bound theorem and to the LatticeFRC and RSLatticeFRC propositions. It closes the logical bridge from the lattice cutoff theorem to the hypothesis used in conditional Navier-Stokes regularity arguments of the form FRC to injection damping to direction constancy to rigid rotation veto to regularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.