balanced_is_unique_minimum
plain-language theorem explainer
The theorem shows that among recognition events the balanced state with ratio 1 is the sole minimizer of information cost. Workers deriving ledger-based physics from recognition ratios cite it to confirm that any imbalance encodes strictly positive information. The term-mode proof substitutes the explicit J-cost at unity and invokes the zero-set characterization.
Claim. Let $e$ be a recognition event with positive ratio $x$. If the information cost $J(x)$ equals the cost of the balanced event, then $x=1$.
background
Recognition Science encodes every physical fact as a recognition event: a positive real ratio $x>0$ in the ledger. The information cost of the event is the J-cost $J(x)$, which equals zero precisely when $x=1$ by the upstream lemma Jcost_unit0. The balanced event is defined to be the unit-ratio case, representing the absence of encoded information.
proof idea
One-line wrapper that unfolds infoCost and balancedEvent, rewrites the hypothesis with Jcost_unit0, and applies the lemma info_cost_zero_iff_unit to extract the ratio equality.
why it matters
The result supplies the uniqueness direction inside the IC-001 certificate, completing the claim that information content is exactly the deviation from balance. It anchors the ledger interpretation in the module doc-comment and aligns with the Recognition Composition Law and the eight-tick octave structure. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.