biased_reasoning_cost
plain-language theorem explainer
The theorem asserts that biased reasoning produces strictly positive J-cost for every ratio r away from 1. Cognitive modelers and information theorists would cite it as the cross-domain instance of universal J-positivity. The proof is a direct one-line application of the core positivity lemma for J-cost.
Claim. For every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$, where this instance is labeled as the cost of biased reasoning.
background
J-cost quantifies deviation from equilibrium through the functional $J(x) = (x + x^{-1})/2 - 1$. The module C16 extends the equilibrium result C7 by showing the same positivity holds off equilibrium in every domain where J applies, including biased reasoning as a cognitive deviation from optimal inference. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 whenever x > 0 and x ≠ 1, proved by rewriting Jcost as a square divided by x and verifying the numerator is positive.
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 theorem feeds the JPositivityUniversalityCert that assembles positivity statements across turbulence, disease, off-target effects, game theory, and arbitrage. It realizes the C16 claim that a single lemma supplies non-equilibrium cost in every RS domain, reinforcing the Recognition Composition Law and the uniform origin of off-equilibrium penalties from J-positivity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.