finiteVolume_Jcost_bound
The theorem proves that the J-cost of the normalized vorticity ratio on any finite-volume profile s satisfies J(normalizedRatio s) ≤ sqrt(siteCount s). Workers closing the lattice bridge to Navier-Stokes regularity in Recognition Science cite this bound to obtain finite recognition cost from the φ-ladder cutoff. The term proof chains three prior lemmas via le_trans: the ratio is at least one, J-cost is monotone above one, and the ratio itself is bounded by sqrt(siteCount).
claimLet $s$ be a finite-volume vorticity profile on the RS lattice with $N$ sites. Then the recognition cost satisfies $J(ω_{max}/ω_{rms}) ≤ √N$.
background
The module supplies the logical bridge between the lattice φ-ladder cutoff and the conditional-completion route used in the Navier-Stokes regularity argument. A FiniteVolumeProfile packages siteCount, omegaMax, omegaRms together with the finite-volume control axiom omegaMax ≤ √siteCount · omegaRms; normalizedRatio extracts the scale ratio omegaMax/omegaRms. Jcost is the recognition cost induced by the multiplicative recognizer comparator (or equivalently the J-cost of an observer forcing event). The upstream le_trans lemma from ArithmeticFromLogic composes the two inequalities that appear in the proof.
proof idea
Term-mode proof. Obtain 1 ≤ normalizedRatio s from the sibling normalizedRatio_ge_one. Apply the sibling Jcost_le_self_of_one_le to replace Jcost by the ratio itself. Compose the resulting inequality with normalizedRatio_le_sqrt_siteCount via the upstream le_trans.
why it matters in Recognition Science
The bound is applied verbatim by the downstream theorem frc_holds_on_RS_lattice to establish RSLatticeFRC on any finite RS lattice. This step realizes the finite-volume control required by the conditional-completion route (FRC → injection damping → regularity) and closes the lattice-to-PDE link described in the module doc-comment. It sits inside the T5–T8 segment of the forcing chain where J-uniqueness and the eight-tick octave already fix the cost function and spatial dimension.
scope and limits
- Does not prove regularity of the continuous Navier-Stokes equations.
- Does not extend the bound to infinite or continuous lattices.
- Does not supply numerical values or explicit constants beyond the sqrt(siteCount) form.
- Does not address the full conditional-completion sequence past the cost bound itself.
Lean usage
theorem frc_holds_on_RS_lattice (s : FiniteVolumeProfile) : RSLatticeFRC s := finiteVolume_Jcost_bound sformal statement (Lean)
79theorem finiteVolume_Jcost_bound (s : FiniteVolumeProfile) :
80 Jcost (normalizedRatio s) ≤ Real.sqrt s.siteCount := by
proof body
Term-mode proof.
81 have h₁ : 1 ≤ normalizedRatio s := normalizedRatio_ge_one s
82 have h₂ : Jcost (normalizedRatio s) ≤ normalizedRatio s :=
83 Jcost_le_self_of_one_le h₁
84 exact le_trans h₂ (normalizedRatio_le_sqrt_siteCount s)
85
86/-- Strong lattice FRC: the cost is bounded by the explicit finite-volume constant
87`sqrt(siteCount)`. -/