cost_nonneg
plain-language theorem explainer
Any recognition event has non-negative J-cost. Applications in acoustics, aesthetics, and agronomy cite this to certify that derived costs remain non-negative. The proof is a one-line wrapper applying the Jcost non-negativity lemma to the positive state component of the event.
Claim. Let $e$ be a recognition event with positive real state $x > 0$. Then $0 ≤ J(x)$, where $J$ denotes the J-cost function.
background
RecognitionEvent is the structure consisting of a positive real state $x$ together with the proof that $x > 0$. The cost of an event is defined to be the J-cost of its state. The module ObserverForcing shows that any non-trivial coherent recognition structure forces an observer by establishing non-negative costs, zero-cost persistent reference frames, and cooper pairing. Upstream, Jcost_nonneg asserts $J(x) ≥ 0$ for $x > 0$ via the AM-GM inequality (or equivalently via the squared representation $J(x) = (x-1)^2/(2x)$).
proof idea
One-line wrapper that applies the Jcost_nonneg lemma directly to the positive-state field of the recognition event.
why it matters
This result supplies the non-negativity clause required by the PitchJNDCert, SpeechIntelligibilityCert, CulturalAestheticCert, and YieldGapCert structures. It realizes the first step of the seven-step observer-forcing argument in the module: every recognition event carries non-negative J-cost. The fact sits inside the T5 J-uniqueness and T6 phi-fixed-point segment of the forcing chain and is presupposed by all downstream cost-based certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.