natOrbit_isPosInt
plain-language theorem explainer
For every natural number n at least 1, the ratio orbit built from n is a positive-integer orbit: its rational display equals n. Anyone calibrating characters or monotone multiplicative data on the positive integers cites this. The proof is a one-line existential package of the display identity.
Claim. For every natural number $n \ge 1$, the ratio orbit associated to $n$ is a positive-integer orbit: there exists $m \in \mathbb{N}$ with $m \ge 1$ such that the orbit's rational display equals $m$, and in fact $m = n$.
background
In the primitive recognition calculus, costs act on ratio orbits (equivalence classes of nonzero rationals under reciprocal identification). The display map sends an orbit to a chosen rational representative. The native-cost structural ledger studies costs that factor through a ratio character and obey the Recognition Composition Law on those orbits.
A positive-integer orbit is one whose display is a natural number at least 1. The constructor that embeds a natural number $n$ as an orbit is the orbit of the rational $n$, and a simp lemma records that its display is exactly $n$. This theorem packages that fact into the positive-integer-orbit predicate used throughout the ledger.
proof idea
Term-mode existential introduction. The witness is $n$ itself; the hypothesis $1 \le n$ supplies positivity; the display identity (the simp lemma that the orbit of $n$ has rational display $n$) closes the third conjunct. No further rewriting or case analysis.
why it matters
Positive-integer orbits are the calibration spine for structural native costs. Downstream, the round-5 engine theorem (structural character calibrated on positive integers) uses this to prove that a character attached to a structural cost acts as the identity in display on every such orbit, up to reciprocal orientation the cost cannot see. The monotone-multiplicative extraction theorem likewise needs the predicate to read off arithmetic data a monotone factorized cost leaves on the positive integers. Without a clean membership lemma, both calibration and MonoMult extraction would re-prove the display identity at every call site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.