finiteVolume_Jcost_bound
plain-language theorem explainer
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).
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.