TurbulentCost
plain-language theorem explainer
TurbulentCost defines the proposition that J-cost is strictly positive for every positive real r not equal to 1. Researchers in hydrodynamics or non-equilibrium systems cite it as the universal source of off-equilibrium cost under Recognition Science. The declaration is a direct definitional specialisation of the core positivity lemma Jcost_pos_of_ne_one with no additional steps.
Claim. TurbulentCost holds precisely when for every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $J(r) > 0$.
background
The module establishes C16 as the universality of J-cost positivity across domains, extending C7 which covered the equilibrium case J(1) = 0. J-cost is the function obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with the property that J(r) > 0 whenever r ≠ 1. This definition specialises the upstream lemma Jcost_pos_of_ne_one to label the turbulent-flow instance in hydrodynamics.
proof idea
The declaration is a direct definition encoding the universal non-equilibrium cost claim as a Prop. It is instantiated downstream by applying the lemma Jcost_pos_of_ne_one, as seen in the one-line wrapper turbulent_cost.
why it matters
This definition anchors the cross-domain claim C16 by supplying the shared proposition for turbulent flow cost. It feeds the unification theorem all_seven_are_one (which equates the seven domain costs) and the certificate structure JPositivityUniversalityCert. The result extends C7 to the off-equilibrium regime and aligns with T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.