normalizedRatio_pos
plain-language theorem explainer
The theorem shows that for any finite-volume vorticity profile on an RS lattice the normalized ratio of maximum to RMS vorticity is strictly positive. Lattice FRC bridge users cite it to guarantee the ratio is positive before feeding it into recognition-cost bounds for Navier-Stokes regularity arguments. The proof is a direct term-mode application of division positivity after unfolding the definition and using the profile's RMS positivity together with the ordering omega_rms ≤ omega_max.
Claim. Let $s$ be a finite-volume vorticity profile on an RS lattice with fields satisfying $0 < s.omegaRms$ and $s.omegaRms ≤ s.omegaMax$. Then $0 < s.omegaMax / s.omegaRms$.
background
A FiniteVolumeProfile is a structure on an RS lattice that records siteCount (positive natural), omegaMax, omegaRms (positive real), the ordering omegaRms ≤ omegaMax, and the finite-volume control omegaMax ≤ sqrt(siteCount) * omegaRms. The normalizedRatio is the definition omegaMax / omegaRms. The module supplies the lattice bridge that converts the phi-ladder cutoff into a finite recognition-cost bound usable by any conditional-completion route of the form FRC to regularity.
proof idea
The proof is a one-line term-mode wrapper. It unfolds normalizedRatio to obtain the quotient omegaMax / omegaRms, then applies div_pos to the pair (lt_of_lt_of_le omegaRms_pos omegaRms_le_max, omegaRms_pos).
why it matters
This result guarantees the normalized ratio is positive so that it can enter the finite recognition-cost bound inside the lattice FRC bridge. The bridge in turn feeds the conditional-completion chain FRC to injection_damping to direction_constancy to rigid_rotation_veto to regularity. The module closes the logical loop between the lattice phi-ladder cutoff and the hypothesis used by the Navier-Stokes regularity paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.