Jcost_ratio_bound
plain-language theorem explainer
Bounded J-cost B on a positive ratio r forces r itself to be at most 2B + 2. Navier-Stokes regularity arguments on the phi-ladder cite the result to convert energy-cascade cost bounds into explicit scale cutoffs. The proof is a one-line algebraic reduction: unfold the definition of J-cost and apply linear arithmetic after noting the inverse is positive.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. If $0 < r$ and $J(r) ≤ B$, then $r ≤ 2B + 2$.
background
J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, the canonical recognition cost of a multiplicative event with ratio x. It is nonnegative and vanishes only at x = 1, serving as the derived cost of any multiplicative recognizer comparator and equivalently the cost of a recognition event state.
proof idea
The proof unfolds the definition of J-cost inside the bound hypothesis, records that the inverse of r is positive, and invokes linarith to obtain the linear inequality on r.
why it matters
The result is invoked directly by bounded_Jcost_bounded_max to turn a J-cost bound into a bound on maximum vorticity. It supplies the algebraic step that lets the phi-ladder cutoff terminate the Navier-Stokes energy cascade on the discrete lattice, consistent with the J-uniqueness and eight-tick octave landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.