zero_leQ_iff
plain-language theorem explainer
A ratio orbit is nonnegative under the delta-native rational order exactly when its numerator's signed-orbit integer is nonnegative. Anyone proving ordered-ring laws on ratio orbits cites this bridge. The proof unfolds the order, routes through the signed-orbit integer comparison, collapses the zero representative, and finishes both directions by linear arithmetic.
Claim. For every ratio orbit $r$, $0 \le_{\mathrm{Q}} r$ if and only if $0 \le n(r)$ in $\mathbb{Z}$, where $n(r)$ is the integer read from the numerator's signed orbit via the choice-free $\mathrm{toInt}$ bridge. Equivalently, nonnegativity of $r$ in the rational order is exactly nonnegativity of that numerator integer.
background
Ratio orbits are the delta-native stand-in for rationals in the Primitive Recognition Calculus: each carries a signed-orbit numerator and a positive denominator orbit. The relation $\le_{\mathrm{Q}}$ (written leQ in the development) is the order on those orbits, defined so that comparison reduces to integer comparison of cross-multiplied signed orbits rather than classical rational arithmetic.
The key upstream bridge is the purified equivalence that signed-orbit order is exactly the order of the associated integers under toInt. Zero on the ratio-orbit side is the class with numerator integer $0$ and denominator $1$, so the left-hand comparison against zero collapses to a pure integer nonnegativity statement on the numerator.
The surrounding module builds the ordered-ring fragment of this calculus without classical choice: casts move by axiom-free Int.natCast_mul, and the arithmetic layer sits on the logic-native naturals and integers (toNat, toInt) rather than Mathlib's default classical path.
proof idea
Unfold the definition of the rational order, then rewrite by the signed-orbit bridge SignedOrbit.le_iff_toInt_le. A targeted simp only reduces multiplication and embedding of orbits to integers, using the zero representative together with the simp lemmas for toNat on successor and zero. The goal becomes an ordinary integer inequality; both directions of the biconditional are closed by omega.
why it matters
This lemma is the nonnegativity gate for the ordered-ring law on ratio orbits. Its sole direct consumer is leQ_mul_nonneg_right, which states that right-multiplication by a nonnegative ratio orbit preserves $\le_{\mathrm{Q}}$: after rewriting the nonnegativity hypothesis through this characterization, that proof expands multiplication on representatives, reduces cross-products via the choice-free toInt bridge, and applies Int.mul_le_mul_of_nonneg_right.
In the Recognition foundation stack this is scaffolding for a choice-free rational ordered ring built from logic-native orbits, not an imported classical field. It sits under the Primitive Recognition Calculus grow layer that feeds later forcing and cost constructions; the axiom footprint stays at {propext, Quot.sound}. No T5–T8 landmark is discharged here; the contribution is the arithmetic substrate those landmarks eventually rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.