bounded_Jcost_bounded_max
plain-language theorem explainer
Bounded J-cost of the scale ratio implies the maximum value is linearly bounded by the reference value. Fluid dynamicists working on the Recognition Science discretization of Navier-Stokes would cite this to control pointwise vorticity growth in the phi-ladder cutoff. The proof is a direct application of the Jcost ratio bound lemma followed by multiplication by the reference value and cancellation.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. If $M, R, B > 0$ and $J(M/R) ≤ B$, then $M ≤ (2B + 2) R$.
background
The module formalizes the algebraic and combinatorial core of the argument that the φ-ladder provides an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. The J-cost is defined as J(x) = ½(x + x⁻¹) - 1 for x > 0, with J(1) = 0 by normalization. Upstream results include the theorem Jcost_ratio_bound, which states that if Jcost r ≤ B for r > 0 then r ≤ 2B + 2.
proof idea
The proof first notes that the ratio max_val / ref_val is positive by division of positives. It applies the Jcost_ratio_bound lemma to obtain the ratio bound ≤ 2B + 2. It then multiplies both sides by ref_val using mul_le_mul_of_nonneg_right and cancels via div_mul_cancel₀.
why it matters
This algebraic bound is assembled into the main certificate phiLadderCutoff, which packages all results with zero sorry. It fills the scale-control step in the Navier-Stokes regularity argument of papers/tex/NS_Regularity_Phi_Ladder_Cutoff.tex, supporting finite cascade depth and decay to zero. It connects to the J-uniqueness property and the phi-ladder structure in the broader Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.