off_target_cost
plain-language theorem explainer
Off-target cost asserts that J-cost is strictly positive for any positive real ratio unequal to one, providing the CRISPR specialization of non-equilibrium deviation penalties. Researchers in targeted gene editing or mismatch modeling cite this to bound off-equilibrium costs uniformly. The proof is a direct one-line wrapper applying the core J-cost positivity lemma to the given parameters.
Claim. For every real number $r$ with $0 < r$ and $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
J-cost quantifies deviation from the self-similar fixed point via the Recognition Composition Law, with the equilibrium value J(1) = 0 established earlier. The module C16 extends this to show J-cost positivity in every RS domain, defining OffTargetCost as the universal proposition specialized to imperfect guide matches in CRISPR. The upstream lemma Jcost_pos_of_ne_one proves the inequality by rewriting Jcost as a square ratio and applying positivity of nonzero squares.
proof idea
The proof is a one-line wrapper that applies Jcost_pos_of_ne_one directly to the inputs r, hr, and hne.
why it matters
This theorem supplies the off-target entry in jPositivityUniversalityCert, completing the cross-domain aggregation for claim C16. It extends the J-uniqueness step from the forcing chain (T5) to guarantee positive costs away from the fixed point across hydrodynamics, medicine, and game theory. The result closes the universality scaffolding without introducing new open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.