IsPosIntOrbit
plain-language theorem explainer
A ratio orbit is a positive-integer orbit when its rational display equals some natural number n ≥ 1. Cost monotonicity, trace lower bounds, and structural uniqueness all quantify over this class. The definition is a one-line existential on the verifier map toRat.
Claim. A ratio orbit $q$ is a positive-integer orbit if there exists a natural number $n \geq 1$ such that the rational display of $q$ equals $n$ as a rational.
background
In the primitive recognition calculus, a ratio orbit packages a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). The map toRat is a verifier display sending that package to an ordinary rational via integer division; its internal characterization is cross-multiplication, not a new arithmetic construction.
The structural ledger module builds native-cost uniqueness from RCL-style hypotheses on maps $F$ from ratio orbits to ratio orbits. Many of those hypotheses (monotonicity, calibration anchors, character factorization) are stated only on orbits whose display is a positive integer, so the predicate isolates that discrete ray inside the rational orbit space.
Upstream, the same predicate appears in the real-character factorization pack; here it is restated for the structural ledger so ledger theorems can name the class without importing the cost pack wholesale.
proof idea
Pure definition: unfold to an existential over $\mathbb{N}$. No tactics, no lemmas. Witnesses are supplied later by theorems such as natOrbit_isPosInt, which plugs in the standard natural-number orbit and its toRat identity.
why it matters
This class is the domain restriction for native-cost monotonicity: on positive-integer orbits, cost does not decrease as imbalance grows. It feeds traceDisplay_posInt_ge_two (trace display at least 2 on such orbits under sans-anchor hypotheses), primeDirection_isPosInt, natOrbit_isPosInt, and the gauge-rigidity and structural uniqueness targets that close Round 5 of the ledger ("the structural ledger forces the canonical cost").
In the broader Recognition chain, native cost is the J-cost side of T5 uniqueness and the RCL identity. Restricting monotonicity and uniqueness statements to positive-integer orbits keeps the discrete ladder (phi-rungs, integer imbalance) aligned with the continuous character factorization without claiming the property for every rational orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.