zero_ratio_not_valid
plain-language theorem explainer
No recognition event exists with ratio zero. This corollary encodes the law of existence in Recognition Science by showing that J-cost diverges as the ratio approaches zero, ruling out nothingness. Researchers deriving physics from information measures cite it as a direct consequence of the ledger structure. The proof proceeds by contradiction, applying linear arithmetic to the positivity axiom on the ratio field.
Claim. There does not exist a recognition event $e$ such that the ratio of $e$ equals zero, where a recognition event is a positive real ratio in the ledger.
background
A RecognitionEvent is a structure consisting of a positive real ratio together with a proof that the ratio exceeds zero; this encodes every physical fact as a ledger entry. The module shows that information cost $J(x)$ is nonnegative for $x>0$, vanishes only at $x=1$, and diverges as $x$ approaches zero from above. Upstream results include the shifted cost $H(x)=J(x)+1$ from CostAlgebra, which converts the Recognition Composition Law into d'Alembert form, and the entropy definition from InitialCondition that ties zero defect to minimum entropy.
proof idea
The term proof assumes an event $e$ with ratio zero. It then invokes linear arithmetic on the positivity hypothesis ratio_pos of that event, which asserts ratio > 0, yielding an immediate contradiction.
why it matters
This corollary completes the IC-001 suite by excluding the zero-ratio case and appears in the ic001_certificate that declares information is the ledger. It realizes the RS forcing step where infinite cost at zero forces existence, consistent with the eight-tick octave and D=3 derived from the phi-ladder. The result closes the gap between abstract information and physical substrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.