positive_iff_toRat_pos
plain-language theorem explainer
Internal positivity of a ratio orbit is equivalent to strict positivity of its verifier rational display. Anyone building the PRC ordered field, Cauchy reals, or J-cost increments cites this bridge. The proof unfolds both sides and routes through the signed-orbit toInt characterizations plus denominator nonzeroness, finishing with positivity and omega.
Claim. For every ratio orbit $q$, the internal positivity predicate on $q$ holds if and only if $0 < \mathrm{toRat}(q)$ in $\mathbb{Q}$, where $\mathrm{toRat}$ is the verifier map sending $q$ to the rational $\mathrm{toInt}(q.\mathrm{num})/\mathrm{toNat}(q.\mathrm{den})$.
background
Primitive Recognition Calculus builds arithmetic from logic orbits rather than assuming $\mathbb{Z}$ and $\mathbb{Q}$. A RatioOrbit is a signed numerator orbit over a positive distinction-nat denominator. The recovery maps toInt and toNat read those orbits as ordinary integers and naturals; toRat is their quotient in the verifier rationals.
Internal positivity is the PRC-native order predicate on ratio orbits (nonnegative numerator that is not balanced with zero). The module sits in the foundation layer that equips these orbits with field operations and order so later J-cost and real constructions can stay choice-light.
Upstream bridges already equate internal balance with integer equality (balanced_iff_toInt_eq: "the balanced characterization agrees with the verifier integer display") and guarantee the denominator is nonzero both as a Nat and after casting to $\mathbb{Q}$. Nonnegativity of signed orbits is likewise tied to toInt nonnegativity.
proof idea
Unfold positive and toRat. First record that the denominator Nat (and its cast to $\mathbb{Q}$) is strictly positive via den_toNat_ne_zero.
Forward direction: from internal positivity, pull toInt nonnegativity of the numerator (nonneg_iff_toInt_nonneg) and exclude the zero case by balanced_iff_toInt_eq against SignedOrbit.zero. Omega upgrades nonneg-and-nonzero to strict positivity of the integer numerator; cast and positivity give $0 < \mathrm{toRat}(q)$.
Converse: from $0 < \mathrm{toRat}(q)$, multiply by the positive denominator cast (mul_pos pattern with field_simp and den_cast_ne_zero) to recover a strictly positive integer numerator. Reassemble internal positivity: nonnegativity via the toInt bridge, and not-balanced-zero by contradiction (balance would force toInt = 0, contradicting omega).
why it matters
This is the order-display bridge for PRC rationals: every later positivity or strict-order fact that wants to compute in $\mathbb{Q}$ and return to the internal predicate routes through it.
Immediate children include positive_normalize (positivity survives ratio normalization), positive_not_zero / positive_ne_zero (positive implies nonzero display), and the rational_field_certificate package that records the ordered-field laws. Downstream real work uses it for PRCBoundednessDelta_positive, Cauchy boundedness targets, and lt_iff_toRat_lt on real Cauchy data. The J-cost distance-increment triangle target also consumes positive PRC rationals built this way.
In the Recognition stack this sits under the foundation forcing path that eventually supports the unique J-cost (T5) and the phi-ladder arithmetic; without a faithful positivity bridge, ordered-field and completeness scaffolding cannot stay aligned with the verifier rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.