IsPosIntOrbit
plain-language theorem explainer
A ratio orbit is a positive-integer orbit when its rational display equals some natural number n ≥ 1. Cost uniqueness and monotonicity arguments cite this predicate to restrict the native cost map to the positive-integer ray. The body is a one-line existential definition, not a proved statement.
Claim. A ratio orbit $q$ is a positive-integer orbit when there exists a natural number $n \ge 1$ such that the rational display of $q$ equals $n$ as an element of $\mathbb{Q}$.
background
In the primitive recognition calculus, a ratio orbit packages a signed integer numerator over a nonzero distinction-nat denominator. The map toRat is the verifier display of that package as an ordinary rational (spec tag A5: transport by cross-multiplication).
The Cost.RealCharacterFactorization module studies native cost maps on ratio orbits under the Recognition Composition Law and related structural hypotheses. Restricting attention to orbits whose display is a positive integer is the discrete ray on which monotonicity, calibration, and uniqueness statements are stated.
The same predicate appears in the structural ledger under the gloss "an orbit displaying a positive integer," and is the domain filter for native-cost monotonicity: cost does not decrease as imbalance grows on that ray.
proof idea
Definitional unpacking only. The predicate is the Prop ∃ n : ℕ, 1 ≤ n ∧ q.toRat = (n : ℚ). No tactics, no lemmas: witnesses are pairs (n, hn, heq) with n ≥ 1 and equality of rational displays.
why it matters
This is the discrete filter used throughout native-cost uniqueness. Downstream, native-cost monotonicity is quantified only over positive-integer orbits; traceDisplay_posInt_ge_two uses it to force the doubled-trace display at least 2 on that class; natOrbit_isPosInt and primeDirection_isPosInt populate the class; and the Round-5 terminal PRCStructuralNativeCostUniquenessTarget_proved routes through the same ledger.
In the Recognition framework the native cost is the unique map compatible with the RCL (the functional equation behind T5 J-uniqueness). Pinning cost behaviour on positive-integer orbits is the discrete half of that rigidity before continuous character factorization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.