biased_agent
plain-language theorem explainer
The biased_agent theorem establishes that the J-cost is strictly positive for any positive real r distinct from 1. Economists applying Recognition Science to behavioral models would cite this to certify the presence of systematic bias in agents. The argument is a direct one-line wrapper that invokes the general J-cost positivity lemma.
Claim. Let $r$ be a real number satisfying $r > 0$ and $r ≠ 1$. Then the J-cost of $r$ is positive: $Jcost(r) > 0$.
background
The module derives five canonical behavioral economics findings from the configuration dimension equaling 5. Within this setting rational agents satisfy J = 0, corresponding to perfect value recognition, while behavioral bias corresponds to J > 0, indicating systematic recognition error. The J-cost function therefore serves as the quantitative measure of that error.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module (also present in JcostCore and LocalCache). That lemma rewrites Jcost via its square form and invokes positivity of squares for nonzero arguments together with positivity of the remaining denominator.
why it matters
This result supplies the biased field inside the behavioralEconomicsCert definition that certifies the five findings. It directly encodes the module's distinction between rational agents (J = 0) and biased agents (J > 0). The declaration therefore bridges the core cost positivity results to the economic interpretation of bias inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.