turbulent_cost
plain-language theorem explainer
The declaration certifies that turbulent flow carries strictly positive J-cost for any deviation parameter r > 0 with r ≠ 1. Hydrodynamic modelers and cross-domain RS analysts cite it to confirm dissipation away from equilibrium in flow regimes. The proof is a direct one-line wrapper that invokes the core positivity lemma Jcost_pos_of_ne_one.
Claim. For all real numbers $r$ with $0 < r$ and $r ≠ 1$, the J-cost satisfies $0 < Jcost(r)$.
background
Jcost is the Recognition Science cost function whose positivity for non-unit arguments supplies the universal non-equilibrium penalty. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 whenever x > 0 and x ≠ 1; its proof rewrites Jcost via Jcost_eq_sq and applies positivity of squares and division. The module C16 frames this as the cross-domain extension of C7, asserting that the identical positivity result labels turbulent cost in hydrodynamics, disease cost, off-target CRISPR cost, and other domains.
proof idea
This is a one-line wrapper that applies Jcost_pos_of_ne_one r hr hne, where hr and hne are the supplied hypotheses 0 < r and r ≠ 1.
why it matters
It supplies the turbulent field inside jPositivityUniversalityCert and the turbulent_positive field inside hydrodynamicsCert. The result therefore completes the structural claim of C16 that a single lemma Jcost_pos_of_ne_one generates non-equilibrium cost across every RS domain; it directly instantiates the off-equilibrium analogue of C7 and anchors the hydrodynamics certification that turbulent regimes incur positive J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.