zero_ltQ_iff_num
plain-language theorem explainer
Strict positivity of a ratio orbit against zero is equivalent to its numerator carrying strictly more positive than negative distinction mass under the natural-number reading. Anyone proving that the positive cone of ratio orbits is closed under multiplication will cite this. Both directions reduce the order predicates to Nat inequalities via the cross-equality and balanced characterizations, then finish by omega.
Claim. For every ratio orbit $r$, one has $0 <_{\mathrm{Q}} r$ if and only if $\mathrm{toNat}(r_{\mathrm{num}}^{-}) < \mathrm{toNat}(r_{\mathrm{num}}^{+})$, where the left side is the strict ratio-orbit order against zero and the right side compares the natural readings of the negative and positive parts of the numerator signed orbit.
background
Ratio orbits are the rational-like objects of the primitive recognition calculus: each carries a signed-orbit numerator (and denominator) built from distinction counts. The strict order $\mathrm{ltQ}$ is defined from a non-strict $\mathrm{leQ}$ together with failure of cross-equality; zero is the zero ratio orbit.
Signed orbits split into positive and negative distinction masses. The map $\mathrm{toNat}$ reads a logic/distinction natural as an ordinary $\mathbb{N}$ iteration count; recovery theorems identify addition and multiplication of those carriers with ordinary Nat arithmetic. A signed orbit is balanced precisely when the two $\mathrm{toNat}$ readings agree.
The local module develops positivity and multiplicative closure for this ordered structure, importing the integer/rational carriers, the reflexive-total and trichotomy facts for the ratio order, and the choice-free signed-orbit order.
proof idea
Term-mode bidirectional argument. Unfold $\mathrm{ltQ}$ into the pair $(\mathrm{leQ},,\neg\mathrm{crossEq})$. Forward: rewrite the inequality via the $\mathrm{toNat}$ characterization of $\mathrm{le}$ on the cross form, rewrite non-balance via the balanced-iff-$\mathrm{toNat}$-equality lemma, simplify the zero multiplications and scalings down to Nat arithmetic with the $\mathrm{toNat}$ add/mul/succ/zero recovery facts, then close by omega. Reverse: rebuild the pair; the $\mathrm{le}$ half is the same simplification plus omega, and the non-balance half assumes balance, rewrites to a $\mathrm{toNat}$ equality, simplifies, and contradicts the assumed strict Nat inequality by omega.
why it matters
This is the bridge from the abstract ratio-orbit order to a concrete Nat comparison on numerator masses. The sole recorded consumer is the multiplicative positivity theorem in the same module: if both factors are strictly positive against zero, so is their product. That argument rewrites both hypotheses and the goal through this equivalence, then invokes the corresponding strict-positivity fact for signed-orbit multiplication.
In the broader foundation stack this sits under the primitive recognition calculus that reconstructs arithmetic and ordered ratios from logic before the cost functional and the forcing chain (T5 J-uniqueness through T8 dimension). A clean positive cone under multiplication is prerequisite infrastructure for later comparison and growth arguments on the phi-ladder side, even though this lemma itself does not mention J or phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.