physiological_ros
plain-language theorem explainer
The declaration establishes that the J-cost vanishes at the unit ratio, providing the equilibrium baseline for physiological reactive oxygen species in the Recognition Science chemistry model. Researchers modeling aging and oxidative stress would reference this result to separate controlled signaling from damage cascades. The proof reduces directly to the unit lemma for J-cost via term application.
Claim. $J(1) = 0$, where the J-cost function is given by $J(x) = (x-1)^2/(2x)$ for a ratio $x$.
background
The Reactive Oxygen Species module quantifies ROS via the J-cost applied to the ratio of radical to normal oxygen species. Physiological levels correspond to equilibrium with J-cost zero, while oxidative stress requires J-cost exceeding the phi threshold. The upstream Jcost_unit0 lemma states that J(x) is expressed as a squared ratio J(x) = (x-1)^2/(2x) and establishes the unit case by simplification.
proof idea
The proof is a one-line term wrapper that applies the Jcost_unit0 lemma from the Cost module, which itself simplifies the definition of Jcost at argument 1.
why it matters
This result supplies the physiological component to the ROSCert definition, which aggregates the five ROS types, the equilibrium condition, and the positive stress condition. It anchors the B2 aging depth analysis in the Recognition Science framework, where J-cost zero marks controlled signaling before damage cascades begin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.