BiasedReasoningCost
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 in Recognition Science
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.
scope and limits
- Does not derive the positivity from first principles; relies on Jcost_pos_of_ne_one.
- Does not compute explicit cost values or bounds beyond positivity.
- Does not apply when r = 1, which corresponds to equilibrium with zero cost.
- Does not cover domains outside the seven listed specializations.
Lean usage
example : BiasedReasoningCost := biased_reasoning_costformal statement (Lean)
39def BiasedReasoningCost : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r