DiseaseCost
plain-language theorem explainer
DiseaseCost defines the proposition that J-cost is strictly positive for every positive real r not equal to one. Cross-domain Recognition Science researchers cite it when labeling non-equilibrium costs in medical models of deviation from homeostasis. The definition is a direct label for the universal positivity statement with no internal proof steps.
Claim. The disease cost proposition asserts that for all real numbers $r > 0$ with $r ≠ 1$, the J-cost satisfies $Jcost(r) > 0$.
background
Recognition Science introduces J-cost as the function that vanishes at equilibrium (r = 1) and is positive for any other positive real deviation. Module C16 extends the equilibrium result C7 by showing the same positivity lemma applies uniformly across domains. Jcost is imported from the Cost module and obeys the universal statement Jcost_pos_of_ne_one for r > 0, r ≠ 1.
proof idea
Direct definition of the Prop as the universal quantification over positive reals r ≠ 1. No proof body exists; the companion theorem disease_cost discharges the claim by applying the lemma Jcost_pos_of_ne_one.
why it matters
This definition supplies the medical label for universal J-cost positivity and feeds into the equality theorem all_seven_are_one together with the certification structure JPositivityUniversalityCert. It realises the C16 structural claim that the single lemma Jcost_pos_of_ne_one generates non-equilibrium cost in medicine exactly as in hydrodynamics and game theory. The construction rests on the J-uniqueness property from T5 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.