disease_cost
plain-language theorem explainer
The theorem establishes that disease cost holds by direct instantiation of the core J-cost positivity result for any positive real deviation from unity. Systems biologists modeling homeostasis deviations would cite this as the Recognition Science account of disease as off-equilibrium cost. The proof is a one-line wrapper applying Jcost_pos_of_ne_one.
Claim. For every real number $r$ satisfying $0 < r$ and $r ≠ 1$, the J-cost satisfies $0 < Jcost(r)$, where this instance is the disease cost specialization of the universal positivity claim.
background
The module frames J-cost positivity as C16, the cross-domain extension of C7. DiseaseCost is the proposition that Jcost r is positive for all positive reals r unequal to 1. This is one of several domain labels (turbulent flow, market arbitrage, biased reasoning) that share the identical mathematical content. The upstream lemma Jcost_pos_of_ne_one from the Cost module states that J(x) > 0 for x > 0 and x ≠ 1.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one to the parameters r, hr, and hne.
why it matters
This declaration supplies the disease entry in the jPositivityUniversalityCert record that certifies the full cross-domain claim. It fills the disease specialization inside the C16 statement that the same positivity lemma governs every RS domain where J-cost applies. The relevant framework landmark is the universal off-equilibrium result that J(r) > 0 whenever r ≠ 1, the direct analogue of the equilibrium case J(1) = 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.