info_cost_zero_iff_unit
plain-language theorem explainer
The theorem establishes that the information cost attached to a recognition event is zero precisely when the event ratio equals one. Workers on the IC-001 ledger chain cite it to fix the unique zero-defect state. The proof unfolds the cost definition, substitutes the squared-ratio identity for J, reduces the zero equation to an algebraic square vanishing, and invokes the unit lemma for the converse.
Claim. For a recognition event $e$ with positive ratio $x$, the information cost satisfies $J(x)=0$ if and only if $x=1$.
background
RecognitionEvent is the structure that encodes each physical fact as a positive real ratio $x>0$ together with its positivity witness. The information cost of the event is the J-cost function applied to that ratio. The module frames information as identical to the physical ledger, so that $J(x)=0$ marks the sole balanced state carrying no encoded content.
proof idea
The proof unfolds infoCost and splits the biconditional via constructor. Forward direction rewrites via Jcost_eq_sq, clears the positive denominator, and applies nlinarith to obtain $(x-1)^2=0$. Reverse direction substitutes the hypothesis $x=1$ and applies Jcost_unit0.
why it matters
It supplies the zero-cost characterization used by balanced_is_unique_minimum to conclude that equal costs force the balanced event, and it appears inside the IC-001 certificate and the positive-cost theorem for non-unit ratios. The result realizes the second core theorem of the information-is-ledger claim, confirming uniqueness of the balanced state and anchoring the zero point of the J-cost function in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.