ltQ_mul_pos
plain-language theorem explainer
The product of two strictly positive rational orbits is again strictly positive under the strict orbit order. Anyone assembling the ordered multiplicative structure on rational orbits, or proving positivity of products, cites this. The argument rewrites positivity to a numerator comparison and applies the corresponding signed-orbit fact.
Claim. Let $p$ and $q$ be rational orbits. If $0 < p$ and $0 < q$ in the strict orbit order, then $0 < p\cdot q$.
background
In Primitive Recognition Calculus, a signed orbit is an integer-like difference of two distinction naturals (positive part minus negative part; K4.6). A rational orbit packages a signed numerator over a nonzero distinction-natural denominator, giving a rational display (K4.7).
The strict order on rational orbits is the non-strict order together with failure of cross-equality. Positivity relative to zero has a pure numerator characterization: zero is strictly below a rational orbit exactly when the numerator's negative part is strictly smaller (under toNat) than its positive part.
This module sits in the Grow layer that builds arithmetic and order on rational orbits from signed orbits, importing trichotomy and order infrastructure.
proof idea
Rewrite both positivity hypotheses and the goal via the numerator characterization of strict positivity relative to zero. Observe that the numerator of a rational-orbit product is definitionally the signed-orbit product of the numerators. Apply the signed-orbit lemma that the product of two strictly positive signed orbits remains strictly positive (negative part of the product strictly below the positive part under toNat).
why it matters
This is a basic positive-cone fact for the rational-orbit layer of Primitive Recognition Calculus: multiplication preserves strict positivity. It belongs to the Grow development that equips rational orbits with ordered arithmetic built from signed orbits and distinction naturals.
No downstream uses are recorded in the dependency graph yet; the lemma is local infrastructure for multiplicative structure on rational orbits. It does not itself enter the forcing chain (T0–T8), J-uniqueness, or the Recognition Composition Law, but it supports the discrete ordered-arithmetic substrate those later results rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.