ltQ_irrefl
plain-language theorem explainer
Strict order on rational orbits is irreflexive: no orbit is strictly below itself. Anyone assembling trichotomy or a strict total order on ratio orbits cites this. The argument is immediate from the definition of strict order as weak order plus non-equality, together with reflexivity of cross-equality.
Claim. For every rational orbit $p$ (integer numerator over a nonzero orbit denominator), $\neg(p < p)$, where $p < q$ means $p \le q$ and $p$ is not cross-equal to $q$.
background
A rational orbit is a display of an integer numerator over a nonzero orbit denominator (K4.7). Cross-equality is the natural equality relation on these displays; it is reflexive by a short unfolding to balanced signed orbits.
The strict order on rational orbits is defined pointwise as the conjunction of the weak order with failure of cross-equality. The surrounding module packages the order facts needed for a trichotomy statement on these orbits, importing the integer-rational and integer-order layers of the primitive recognition calculus.
Upstream, reflexivity of cross-equality is already proved, so the only remaining step for irreflexivity of the strict relation is to feed that fact into the second conjunct of the definition.
proof idea
Assume the strict relation holds of $p$ with itself. By definition that yields both the weak inequality and the negation of cross-equality. Reflexivity of cross-equality on rational orbits immediately contradicts the second conjunct, so the assumption is false. The proof is a two-line intro-and-exact against that reflexivity lemma.
why it matters
Irreflexivity is the first structural property required before a strict order can support trichotomy. The sibling trichotomy declaration in the same module needs it so that the three cases (less, equal, greater) are pairwise exclusive. In the primitive recognition calculus this order compares ratio-orbit displays that later feed cost and growth comparisons; without irreflexivity those comparisons would admit self-loops. The declaration sits in the Foundation layer that underwrites the forcing chain, though it does not itself invoke J-uniqueness, $\varphi$, or the eight-tick octave. Downstream use count is presently empty, so its immediate consumer is the local trichotomy package rather than a named paper proposition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.