zero_lt_of_positive
plain-language theorem explainer
A positive primitive-recognition rational is strictly greater than zero in the PRC order. Anyone assembling Cauchy ledgers or null-equivalence on those rationals cites this bridge. The proof is a two-step transfer: rewrite the order via the ordinary-rational embedding, then apply the positivity characterization on that image.
Claim. Let $q$ be a primitive recognition calculus rational. If $q$ is positive, then $0 < q$ in the PRC strict order.
background
The module builds a Cauchy completion of primitive recognition calculus (PRC) rationals, the rational layer of the Recognition calculus before J-cost distances and real quotients appear. PRC rationals carry a positivity predicate and a strict order lt, both designed to match ordinary rational arithmetic after an embedding toRat.
Two comparison lemmas sit immediately upstream of this fact: the order on PRC rationals is equivalent to the ordinary order on their toRat images, and positivity of a PRC rational is equivalent to positivity of that same image. The local goal is only the zero-comparison special case needed when Cauchy epsilons and constant ledgers are introduced.
Downstream material defines a J-cost-derived distance on these rationals (via a squared additive gap, avoiding a rational absolute value on the first pass) and then Cauchy sequences valued in PRC rationals.
proof idea
Tactic proof in two moves. Rewrite the goal lt 0 q along the order-embedding lemma that equates PRC lt with ordinary < on toRat images. The rewritten goal is then the ordinary statement 0 < toRat q, which follows by modus ponens from the positivity-embedding lemma applied to the hypothesis that q is positive, cleaned up with simpa.
why it matters
This is a small order-bridge lemma inside the real-construction layer of Primitive Recognition Calculus. It is used when showing that every constant rational ledger is a Cauchy sequence: the Cauchy witness needs a strictly positive epsilon, and the zero-comparison must sit in the PRC order, not only in ordinary rationals. It is also used in the intended null-distance relation on Cauchy ledgers, whose quantifiers run over positive PRC epsilons and compare J-cost distances by lt.
In the broader Recognition stack this sits below the J-cost surface and the eventual real quotient; it does not itself invoke the Recognition Composition Law, T5 J-uniqueness, or the phi ladder. It simply keeps the rational order coherent so those later constructions can quantify over positive gaps without leaving the PRC type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.