zero_ltQ_one
plain-language theorem explainer
The zero ratio orbit is strictly below the unit under cross-multiplication strict order on rational orbits. Anyone assembling ordered arithmetic on the PRC ratio display cites this base inequality. The proof unfolds the strict-order definition, discharges the weak half by reducing signed-orbit comparison to a decidable natural inequality, and rules out cross-balance by direct computation.
Claim. On ratio orbits (signed-orbit numerator over a nonzero distinction-orbit denominator), the zero orbit is strictly less than the unit orbit. Strict order means the weak cross-multiplication order holds and the two orbits are not cross-balanced: $0 < 1$.
background
A ratio orbit packages a signed-orbit numerator with a nonzero distinction-orbit denominator. Weak order compares two displays by cross-multiplication: the signed product of the first numerator with the second denominator is at most the reverse product, using the choice-free signed-orbit order. Strict order is that weak relation together with failure of cross-equivalence, the internal PRC relation that two ratios balance under scaled signed products (K4.10).
Signed-orbit order itself reduces to a natural-number comparison on $\delta$-orbit positions: $a \le b$ iff the summed toNat data on positive and negative parts satisfy a linear inequality. That characterization is the choice-free replacement for an integer-level comparison. This module lives in the Primitive Recognition Calculus grow layer, building ordered arithmetic on ratio orbits from integer and distinction primitives.
proof idea
Unfold strict order into weak order plus non-equivalence. For the weak half, unfold cross-multiplication order, rewrite via the choice-free signed-orbit characterization that compares toNat positions, and close by decide on the resulting natural inequality for zero versus one. For the second half, assume cross-balance of zero and one and contradict it by a decidable proof that those two orbits are not cross-balanced.
why it matters
This pins the elementary fact $0 < 1$ inside the PRC ratio-orbit order, a prerequisite for positivity and ordered-field development on the recognition calculus rationals. It rests on the choice-free signed-orbit order and the cross-multiplication definitions (K4.7 structure, K4.10 balance). The mirror graph currently lists no downstream dependents, so the lemma acts as a leaf-level order fact for later grow results on ratio orbits. In the broader Recognition Science foundation it supports the arithmetic substrate beneath the forcing chain, without yet invoking J-uniqueness, $\varphi$, or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.