positive_not_zero
plain-language theorem explainer
A positive ratio orbit has nonzero rational image under the orbit-to-rational map. Field and ordered-structure work on PRC rationals cites this to keep denominators and reciprocals well-defined. The proof is a one-line reduction: positivity implies strictly positive rational value, hence nonzero.
Claim. Let $q$ be a ratio orbit (integer numerator over a nonzero distinction-natural denominator). If $q$ is positive, then the rational number associated to $q$ satisfies $q_{\mathbb{Q}} \neq 0$.
background
In the primitive recognition calculus, a ratio orbit is an integer numerator paired with a nonzero distinction-natural denominator (K4.7). PRC rationals are the quotient of these displays by the cross-multiplication setoid (K4.8), so each orbit class has a well-defined image in $\mathbb{Q}$ via toRat.
Positivity on ratio orbits is the order predicate used before the full field structure is installed. A sibling characterization equates that predicate with strict positivity of the rational image: an orbit is positive if and only if its toRat value is greater than zero.
The local module builds arithmetic (including division from multiplication and reciprocal) on these native rationals, so nonzeroness of positive elements is a standing hygiene lemma for later reciprocal and ordered-field steps.
proof idea
Term-mode one-liner. Apply the sibling equivalence that positive orbits have strictly positive rational image, project the hypothesis through the forward direction, and finish with ne_of_gt: anything strictly greater than zero is unequal to zero.
why it matters
This sits in the foundation layer that turns primitive distinction data into a usable rational field for Recognition Science cost calculus. Downstream siblings define division on PRC rationals from multiplication and reciprocal; nonzeroness of positive elements is the obvious guard that those constructions stay total on the positive cone.
No parent theorems currently list this edge, so it is local infrastructure rather than a named forcing-chain step. It does not touch T5–T8, the RCL, or the mass ladder directly; it only keeps the rational substrate coherent before J-cost and ledger forcing are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.