RecognitionDeficit
plain-language theorem explainer
The universal non-equilibrium cost statement asserts that J-cost is strictly positive for every positive real ratio r not equal to one. Cross-domain researchers in hydrodynamics, medicine, game theory, and cognitive science cite this as the common source of deviation cost. The declaration introduces it as a definition with no internal proof structure.
Claim. The recognition deficit is the assertion that $J(r) > 0$ whenever $r > 0$ and $r ≠ 1$, where $J$ denotes the J-cost function: $∀ r ∈ ℝ, 0 < r → r ≠ 1 → 0 < J(r)$.
background
This module presents the J-cost positivity universality claim, labeled C16, as the off-equilibrium counterpart to the equilibrium result C7. J-cost quantifies the cost of deviation from the fixed point at ratio one, where the J function satisfies J(1) = 0. The definition RecognitionDeficit captures this positivity in a form that is definitionally identical across seven domains: turbulent flow cost, disease cost from homeostasis deviation, off-target cost in CRISPR, off-equilibrium game cost, market arbitrage gap, biased reasoning cost, and recognition deficit in neurodevelopment.
proof idea
This declaration is a definition that directly states the quantified positivity condition as a Prop. It contains no proof body and applies no lemmas internally.
why it matters
The definition supplies the common proposition underlying the equality theorem all_seven_are_one, which shows that the seven domain costs are identical. It realizes the structural claim in the module documentation that a single lemma generates non-equilibrium cost in every Recognition Science domain. This step connects the core J function properties to applications in physics, biology, and cognition without additional assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.