info_cost_symmetric
plain-language theorem explainer
The declaration proves that information cost is symmetric under inversion of the recognition ratio: J(x) equals J(1/x) for any positive x. Researchers in information-theoretic physics and foundations of quantum mechanics would cite this result as establishing the bidirectional ledger balance in Recognition Science. The proof reduces immediately to the core J-cost symmetry lemma after unfolding the event definition.
Claim. Let $e$ be a recognition event with positive ratio $x > 0$. Then the information cost of $e$ equals the information cost of the inverted event with ratio $x^{-1}$: $J(x) = J(x^{-1})$.
background
Recognition Science treats every physical fact as a recognition event, formalized as a positive real ratio $x > 0$ in the ledger. The structure RecognitionEvent packages such a ratio together with a proof of its positivity. The information cost of an event is defined as the J-cost J(x) of its ratio, where J is the function J(x) = (x + x^{-1})/2 - 1. This theorem sits inside the IC-001 module, which derives that information is identical to the physical ledger. Upstream, the lemma Jcost_symm establishes the algebraic symmetry J(x) = J(x^{-1}) for x > 0 by direct expansion and field simplification.
proof idea
The proof is a one-line wrapper: it unfolds the definition of infoCost on both sides and invokes the Jcost_symm lemma on the positivity witness of the ratio.
why it matters
This fills step 4 of the IC-001 core theorems, confirming the ledger balance principle that recognition is bidirectional. It is referenced by the ic001_certificate which aggregates all eight IC-001 results into a single derived status string. In the broader framework it reinforces the J-uniqueness property by ensuring cost symmetry under inversion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.