balanced_has_minimum_cost
plain-language theorem explainer
The balanced recognition event carries the lowest possible information cost among all events with positive ratio. A physicist modeling information as ledger imbalance would cite this to show that only deviations from unity encode content. The proof proceeds by term reduction: unfolding the cost, substituting the zero value at balance, and invoking non-negativity of J-cost on the given ratio.
Claim. For every recognition event with positive ratio $x$, the J-cost of the balanced state satisfies $J(1) = 0 ≤ J(x)$.
background
RecognitionEvent encodes each physical fact as a positive real ratio together with a proof of positivity. The associated information cost is the J-cost of that ratio, which is zero exactly at the balanced point x = 1. The module develops the thesis that information coincides with the ledger: every recognition event carries J-cost as its information content, and the balanced state encodes nothing. Upstream, Jcost_nonneg asserts 'J(x) ≥ 0 for positive x (AM-GM inequality)' while Jcost_unit0 shows Jcost 1 = 0.
proof idea
Term-mode proof that unfolds the definitions of information cost and the balanced event, rewrites the balanced cost to zero using Jcost_unit0, then applies Jcost_nonneg to the ratio positivity witness.
why it matters
This result supplies IC-001.5, the minimum-cost property of the balanced state, within the InformationIsLedger module. It is invoked by the ic001_certificate that assembles the full derivation of information as ledger. The placement anchors the Recognition Science claim that physical content arises only from imbalance, aligning with the J-uniqueness in the forcing chain and the zero-entropy deterministic state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.