info_cost_pos_of_ne_one
plain-language theorem explainer
Any recognition ratio other than unity carries strictly positive information cost under the J-function. Researchers deriving physical content from ledger imbalances in foundational physics would cite this as IC-001.3. The proof is a short term-mode argument that negates the zero-cost characterization, invokes non-negativity, and applies the order property that a nonnegative real unequal to zero is positive.
Claim. Let $x > 0$ be the ratio of a recognition event. If $x ≠ 1$, then the information cost $J(x) > 0$.
background
A recognition event encodes a physical fact as a positive real ratio in the ledger. Its information cost is the value of the J-function, which is nonnegative for all positive arguments and vanishes precisely when the ratio equals one. Upstream results from the ObserverForcing and MultiplicativeRecognizerL4 modules supply the nonnegativity lemma and the zero-cost characterization used here.
proof idea
The argument first applies the zero-cost characterization to the assumption that the ratio differs from one, obtaining that the cost is nonzero. It then combines this with the nonnegativity of the cost via the lemma that a nonnegative real unequal to zero is strictly positive.
why it matters
The theorem supplies the strict-positivity clause required by the IC-001 certificate that information is the ledger. It feeds directly into the downstream ic001_certificate definition and reinforces the framework claim that any ledger imbalance carries positive cost, consistent with the bidirectional symmetry of J and the interpretation that the ledger constitutes physical reality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.