positive_ne_zero
plain-language theorem explainer
A positive PRC rational has nonzero verifier display in ℚ. Field and order lemmas on the PRC rational layer cite this to rule out division by zero and collapse of the positive cone. The proof is a one-line term: positivity implies strict positivity of the display, hence inequality with zero.
Claim. Let $q$ be a PRC rational (a ratio-orbit quotient class). If $q$ is positive in the PRC-native sense (nonnegative signed numerator that is not the zero orbit), then its verifier display as a rational satisfies $q_{\mathbb{Q}} \neq 0$.
background
PRC rationals (PRCRat) are nonzero-denominator ratio-orbit quotient classes, identified by cross-multiplication of orbit-level numerator and denominator (K4.8). The map toRat is a verifier display of a ratio orbit as an ordinary rational; internally it is the quotient of the integer display of the numerator by the natural display of the denominator.
PRC-native positivity means the signed numerator is nonnegative and not balanced with the zero orbit. The companion lemma positive_iff_toRat_pos equates that predicate with strict positivity of the verifier display: positive q ↔ 0 < q.toRat. The present module builds the ordered-field layer on these objects after the integer and ratio-orbit constructions.
proof idea
One-line term proof. Apply the forward direction of positive_iff_toRat_pos to the hypothesis positive q, obtaining 0 < q.toRat. Then ne_of_gt yields q.toRat ≠ 0. No case splits or unfolding beyond that bridge lemma.
why it matters
Sits in the Foundation primitive-recognition calculus, on the path from logic-level integers and ratio orbits to a usable rational field. Positivity must exclude zero before division, ordered-field axioms, and cost comparisons can be stated cleanly on PRC rationals. The sibling suite (positive, positive_iff_toRat_pos, positive_not_zero, div, toRat_div) is assembling that layer.
No downstream consumers are wired yet in the graph. In the broader Recognition stack this is scaffolding for later J-cost and forcing-chain work (T5 J-uniqueness and the Recognition Composition Law need a coherent positive multiplicative structure), not a physics endpoint itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.