normalizedRatio_ge_one
plain-language theorem explainer
The normalized vorticity ratio on any finite-volume RS lattice profile is bounded below by one. Workers on the lattice bridge to Navier-Stokes regularity cite the result to anchor the subsequent J-cost estimate from below. The argument is a direct term-mode application of the division inequality to the profile fields omegaRms positivity and omegaRms ≤ omegaMax.
Claim. For every finite-volume vorticity profile $s$, $1 ≤ ω_max(s) / ω_rms(s)$.
background
A FiniteVolumeProfile is a structure on an RS lattice that records a positive site count, positive RMS vorticity ω_rms, maximum vorticity ω_max satisfying ω_rms ≤ ω_max, and the finite-volume control ω_max ≤ √(siteCount) · ω_rms. The auxiliary definition normalizedRatio forms the quotient ω_max / ω_rms. Module documentation states that this construction closes the logical loop between the lattice φ-ladder cutoff result and the conditional-completion route from the Navier-Stokes regularity paper. On a finite RS lattice the normalized vorticity ratio is automatically finite-volume controlled, supplying a finite recognition-cost bound that enters the abstract chain FRC to regularity. The upstream FiniteVolumeProfile encodes the scale information and norm-equivalence input required for the bridge.
proof idea
The proof unfolds the definition of normalizedRatio to obtain the quotient ω_max / ω_rms. It then applies the right-hand side of the one_le_div lemma (if 0 < a and a ≤ b then 1 ≤ b/a) directly to the fields omegaRms_pos and omegaRms_le_max of the input profile. The entire argument is therefore a one-line term-mode invocation of real division monotonicity.
why it matters
The theorem is invoked inside finiteVolume_Jcost_bound to obtain the hypothesis 1 ≤ normalizedRatio s before applying the J-cost self-bound and the √(siteCount) control. It supplies the missing lower bound in the lattice FRC bridge, which the module documentation describes as the exact logical link from the φ-ladder cutoff to the hypothesis of the conditional-completion route. In the Recognition Science setting this step secures the finite recognition-cost estimate on the lattice before feeding into the Navier-Stokes regularity argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.