zero_ratio_not_valid
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.
claimThere 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 in Recognition Science
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.
scope and limits
- Does not compute the explicit divergence rate of J(x) as x approaches zero.
- Does not extend the result to negative ratios or complex values.
- Does not address compositions of multiple recognition events.
- Does not derive the Landauer bound or thermodynamic limits.
formal statement (Lean)
137theorem zero_ratio_not_valid :
138 ¬ ∃ e : RecognitionEvent, e.ratio = 0 := by
proof body
Term-mode proof.
139 rintro ⟨e, he⟩
140 linarith [e.ratio_pos]
141
142/-! ## §IV. Information and Shannon Entropy -/
143
144/-- **THEOREM IC-001.9**: Shannon entropy equals expected J-cost.
145 H(X) = Σ p_i · J(p_i) = expected information cost.
146 This proves our information measure is consistent with Shannon's. -/