recognition_deficit
plain-language theorem explainer
Recognition deficit asserts that J-cost is strictly positive for every positive real r unequal to one. Cross-domain researchers in Recognition Science cite it to unify non-equilibrium costs uniformly across hydrodynamics, medicine, game theory, and neurodevelopment. The proof is a one-line term that directly invokes the core J-cost positivity lemma from the Cost module.
Claim. $forall r : mathbb{R}, 0 < r to r neq 1 to 0 < Jcost(r)$
background
The module establishes J-cost positivity universality as the off-equilibrium analogue of C7. RecognitionDeficit is the proposition forall r : R, 0 < r -> r != 1 -> 0 < Jcost r. The local setting treats this as the single source of non-equilibrium cost in every RS domain where J-cost applies, with specializations to turbulent flow, disease, off-target CRISPR, arbitrage, and biased reasoning. It rests on the upstream lemma Jcost_pos_of_ne_one whose doc-comment states J(x) > 0 for x != 1 and x > 0, proved by rewriting Jcost as a square and applying positivity of squares.
proof idea
The proof is a term-mode one-liner that constructs the required function by applying Jcost_pos_of_ne_one directly to the parameters r, hr, and hne. No additional tactics or reductions are used.
why it matters
This theorem supplies the recognition-deficit component of jPositivityUniversalityCert, which collects the seven domain specializations. It realizes the module's structural claim extending C7 to off-equilibrium cases and supports the universal J-cost property that underpins the Recognition Composition Law and the forcing chain from T0 to T8. No open scaffolding remains for this positivity statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.