pith. machine review for the scientific record. sign in
def definition def or abbrev high

RecognitionDeficit

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  40def RecognitionDeficit : Prop := ∀ r : ℝ, 0 < r → r ≠ 1 → 0 < Jcost r

proof body

Definition body.

  41

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.