normalizedRatio_le_sqrt_siteCount
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove Navier-Stokes regularity.
- Does not apply outside finite RS lattices.
- Does not replace the external PDE steps in the conditional route.
- Does not give sharper constants than the sqrt bound.
Lean usage
have h := normalizedRatio_le_sqrt_siteCount sformal statement (Lean)
60theorem normalizedRatio_le_sqrt_siteCount (s : FiniteVolumeProfile) :
61 normalizedRatio s ≤ Real.sqrt s.siteCount := by
proof body
Term-mode proof.
62 unfold normalizedRatio
63 rw [div_le_iff₀ s.omegaRms_pos]
64 simpa [mul_comm, mul_left_comm, mul_assoc] using s.finiteVolumeControl
65
66/-! ## Bounding J-cost on the lattice -/
67
68/-- On the half-line `[1, ∞)`, the canonical cost is bounded by the identity.
69
70This is the simple estimate needed for the finite-volume FRC bound:
71`J(x) = (x + x⁻¹)/2 - 1 ≤ x` whenever `x ≥ 1`. -/