OffTargetCost
plain-language theorem explainer
OffTargetCost defines the proposition that J-cost is strictly positive for every positive real r not equal to 1. Researchers working on CRISPR off-target effects or market arbitrage cite it as the common non-equilibrium cost source across Recognition Science domains. The definition is a direct specialization of the core positivity result Jcost_pos_of_ne_one with no additional structure.
Claim. OffTargetCost asserts that for all real numbers $r$, if $0 < r$ and $r ≠ 1$ then $Jcost(r) > 0$, where $Jcost$ is the J-cost function satisfying $Jcost(1) = 0$.
background
The module C16 on J-Cost Positivity Universality extends the equilibrium result C7 by labeling the same positivity statement in seven domains. Jcost is imported from the Cost module as the function obeying the Recognition Composition Law with zero at unity and strict positivity elsewhere. The definition isolates the off-target CRISPR instance of the universal claim that holds identically for turbulent flow, disease, game theory, arbitrage, biased reasoning, and recognition deficit.
proof idea
This is a definition that directly encodes the quantified positivity statement. It is instantiated without further reduction in the downstream off_target_cost theorem by direct application of Jcost_pos_of_ne_one.
why it matters
OffTargetCost supplies the off-target label inside the all_seven_are_one theorem that equates the seven domain costs and inside the JPositivityUniversalityCert structure. It fills the C16 slot by extending the equilibrium zero of C7 to non-equilibrium positivity, consistent with deviations from the T6 phi fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.