leQ_refl
plain-language theorem explainer
Every ratio orbit is less than or equal to itself under the cross-multiplication order. Anyone assembling a preorder or total order on native rationals in the Primitive Recognition Calculus cites this. The proof unfolds the cross-product definition and applies choice-free reflexivity of the signed-orbit order, since both sides are the same product.
Claim. For every ratio orbit $p$ (signed-orbit numerator over a nonzero distinction-nat denominator), $p \le_Q p$, where $p \le_Q q$ means the signed orbit $p_{\mathrm{num}}\cdot q_{\mathrm{den}}$ is $\le$ the signed orbit $q_{\mathrm{num}}\cdot p_{\mathrm{den}}$.
background
A ratio orbit is the native rational display in this calculus: a signed orbit as numerator and a nonzero distinction-nat as denominator. The module equips these with a cross-multiplication order: $p \le_Q q$ holds exactly when the signed product of $p$'s numerator with $q$'s denominator (cast via SignedOrbit.ofOrbit) is $\le$ the swapped product.
That comparison lives on signed orbits, not on classical integers. The upstream choice-free order on signed orbits already supplies reflexivity: every signed orbit is $\le$ itself, proved by reducing to a natural-number comparison and a trivial omega step. The present lemma lifts that fact to ratio orbits.
Local setting is the Grow layer of Primitive Recognition Calculus: build order structure on rationals without classical choice, so later cost and ladder constructions stay constructive.
proof idea
One-step reduction. Unfold the cross-multiplication definition of the ratio order; both sides become the same signed-orbit product $p_{\mathrm{num}}\cdot p_{\mathrm{den}}$. Apply the upstream choice-free reflexivity lemma on signed orbits to that common product. No case split and no arithmetic beyond what that lemma already closed.
why it matters
Reflexivity is the first preorder axiom for the native rational order. Together with the sibling totality statement (any two ratio orbits are comparable by the same cross-product test), it starts the total-preorder package on ratio orbits that later cost uniqueness and ladder comparisons need.
Downstream use sites are not yet wired in this graph snapshot, but the lemma sits in the Foundation / Primitive Recognition Calculus path that underwrites constructive comparison before J-cost and phi-ladder material. It inherits the choice-free discipline of the signed-orbit order, so the rational layer does not reintroduce classical choice.
No forcing-chain landmark (T5--T8) is discharged here; this is infrastructure for ordered rationals inside the recognition calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.