info_cost_nonneg
plain-language theorem explainer
Recognition events carry non-negative information cost J(x) for any positive ratio x. Researchers treating information as the physical ledger would cite this as the base non-negativity result in the IC-001 series. The proof is a direct one-line application of the J-cost non-negativity lemma to the event's ratio positivity.
Claim. For every recognition event $e$ with ratio $x > 0$, the information cost satisfies $J(x) ≥ 0$.
background
In the InformationIsLedger module a RecognitionEvent is a structure that encodes a physical fact as a positive ratio $x$ in the ledger, with the ratio_pos field ensuring the J-cost is well-defined. The information cost of the event is the defect functional J(x) drawn from the LawOfExistence module. The local setting is the claim that information is the physical ledger: every recognition ratio carries a definite J-cost, with J(x) = 0 precisely when the ledger is balanced at x = 1.
proof idea
The proof is a one-line wrapper that applies the Jcost_nonneg lemma from the Cost module (and its JcostCore sibling) to the ratio_pos field of the RecognitionEvent.
why it matters
This is theorem IC-001.1 and the first entry in the ic001_certificate. It is used by foldl_add_nonneg, info_cost_pos_of_ne_one, and the certificate itself. The result supplies the non-negativity foundation for the Recognition Science interpretation that information content equals physical ledger content, consistent with the J-uniqueness property and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.