two_isPosInt
plain-language theorem explainer
The ratio orbit representing 2 is a positive-integer orbit: its rational value equals some natural number n ≥ 1. Anyone building the native-cost structural ledger or character factorization over ratio orbits cites this as the base integer witness. The proof is a one-line existential package: n = 2, with norm_num for positivity and simp on two_toRat for the equality.
Claim. The ratio orbit $2$ is a positive-integer orbit: there exists $n \in \mathbb{N}$ with $n \ge 1$ such that the rational value of the orbit equals $n$. Explicitly, $n = 2$ works.
background
In the Primitive Recognition Calculus native-cost ledger, quantities live on ratio orbits: pairs of signed distinction orbits with nonzero denominator, equipped with a map toRat into $\mathbb{Q}$. The constant orbit two is built from the signed orbit of the natural $2$ over denominator $1$; the simp lemma two_toRat records that its rational value is exactly $2$.
IsPosIntOrbit q means $q$ displays a positive integer: $\exists n:\mathbb{N},, 1\le n \land q.\mathrm{toRat}=n$. The same predicate appears in the real-character factorization pack; here it is restated for the native-cost structural ledger so integer witnesses can be named without leaving the PRC module.
Local setting is the structural ledger for native cost on ratio orbits (siblings include jq, closed-form and nonnegativity facts for the J-cost on orbits). Integer orbits are the discrete anchors against which cost and character identities are specialized.
proof idea
One-line existential constructor. Supply witness $n=2$. Discharge $1\le 2$ by norm_num. Discharge two.toRat = (2:\mathbb{Q}) by simp [two_toRat], which unfolds the definition of two and reduces via the already-proved rational evaluation of the underlying two-orbit.
why it matters
Gives the first concrete positive-integer orbit in the PRC native-cost ledger. Downstream character and cost lemmas that restrict to integer orbits (or that specialize doubled-trace / RCL identities at integer points) need this witness; without it, two is only a bare ratio orbit. In the broader Recognition chain, integer ratio orbits sit under the J-cost and RCL layer (T5 J-uniqueness, Recognition Composition Law): they are the discrete points where the continuous cost character factors through ordinary integers. No used_by edges are recorded yet, so this is presently a leaf certificate rather than a step inside a named parent theorem. It closes the scaffolding gap between the definition of two and any future integer-orbit specialization of jq or native-cost hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.