BiasedReasoningCost
plain-language theorem explainer
BiasedReasoningCost labels the universal J-cost positivity statement for the domain of biased reasoning in cognitive models. It asserts that any positive real r not equal to 1 produces strictly positive J-cost, modeling deviation from unbiased equilibrium. This definition is invoked in the all_seven_are_one theorem to equate it with analogous costs in turbulence, disease, and market arbitrage. The definition is a direct renaming of the upstream Jcost_pos_of_ne_one result with no additional reasoning.
Claim. $forall r : mathbb{R}, 0 < r to r neq 1 to 0 < J(r)$, where $J$ is the J-cost function satisfying the Recognition Composition Law.
background
The CrossDomain.JPositivityUniversality module specializes the single lemma Jcost_pos_of_ne_one to seven domains, including biased reasoning as a model for cognitive biases. J-cost is the function satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with J(r) > 0 for r ≠ 1. The local setting is the C16 claim that non-equilibrium cost is universal across hydrodynamics, medicine, game theory, finance, and cognition. Upstream, Jcost_pos_of_ne_one establishes the positivity for any such r.
proof idea
One-line definition that instantiates the universal positivity statement Jcost_pos_of_ne_one under the label BiasedReasoningCost.
why it matters
BiasedReasoningCost feeds directly into the theorem all_seven_are_one, which demonstrates that the seven cost propositions are definitionally equal, and into the JPositivityUniversalityCert structure. It realizes the C16 extension of C7 by labeling the off-equilibrium cost for cognitive biases. This supports the framework's claim that the same J-uniqueness generates non-equilibrium costs in every domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.