normalizedRatio_le_sqrt_siteCount
plain-language theorem explainer
The theorem bounds the normalized vorticity ratio on any finite RS lattice by the square root of the site count. Workers on the conditional Navier-Stokes regularity route cite it to obtain a finite recognition-cost input from the lattice cutoff. The proof is a direct algebraic reduction that rewrites the ratio as a division and invokes the finiteVolumeControl field.
Claim. Let $s$ be a finite-volume vorticity profile on an RS lattice with site count $N$, maximum vorticity $ω_ max$, and RMS vorticity $ω_ rms$. Then the normalized ratio satisfies $ω_ max / ω_ rms ≤ √N$.
background
FiniteVolumeProfile is a structure that packages a vorticity profile on a finite RS lattice. Its fields include siteCount (a positive natural), omegaMax and omegaRms (positive reals with omegaRms ≤ omegaMax), and the key finiteVolumeControl hypothesis omegaMax ≤ √siteCount · omegaRms. The normalizedRatio is the quotient omegaMax / omegaRms that appears in the lattice FRC bridge. Module doc states that this bridge supplies the finite recognition-cost bound needed for the conditional-completion route FRC → injection_damping → direction_constancy → rigid_rotation_veto → regularity. Upstream results supply the cost and identity definitions used in the surrounding J-cost estimates.
proof idea
The term proof unfolds normalizedRatio to expose the division omegaMax / omegaRms. It rewrites the target inequality via div_le_iff₀ using omegaRms_pos, then applies simpa with the finiteVolumeControl field of s, using commutativity and associativity of multiplication to match the form.
why it matters
This bound is the direct premise of finiteVolume_Jcost_bound, which produces the explicit J-cost estimate Jcost(normalizedRatio s) ≤ √siteCount. That estimate feeds the FRC hypothesis in the Navier-Stokes regularity paper and closes the logical loop from the lattice φ-ladder cutoff to the conditional-completion chain. It supplies the finite-volume control step required by the Recognition Science lattice construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.