ofOrbit
plain-language theorem explainer
Embeds a δ-orbit natural n as the nonnegative signed orbit difference (n, 0). Anyone building integer or rational order from orbit arithmetic cites this cast: denominators and absolute bounds enter SignedOrbit via ofOrbit. The body is the structure constructor with zero negative part.
Claim. Given a distinction-orbit natural $n$, form the signed orbit difference $\mathrm{ofOrbit}(n) := (n,\,0)$, i.e. the nonnegative pair with positive part $n$ and negative part the zero orbit.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, playing the role of ℕ without choosing a numeral base. A SignedOrbit is a pair of such orbits (pos, neg) whose intended meaning is the difference pos − neg (K4.6).
The IntegerRational module builds integers and rationals from these orbit objects rather than from Mathlib ℤ/ℚ, so every positive quantity that must enter signed arithmetic needs an explicit embedding. ofOrbit is that embedding: it sends a pure δ-orbit position to a signed difference with vanishing negative part.
Upstream, the structure SignedOrbit and the inductive DistinctionNat are the only dependencies; no arithmetic lemmas are required to state the cast.
proof idea
Pure definition: the structure constructor ⟨n, DistinctionNat.zero⟩. No tactics, no lemmas. The nonnegative reading follows immediately from the intended meaning pos − neg once the negative component is zero.
why it matters
This cast is the bridge from unsigned δ-orbits into signed orbit arithmetic, and it is used heavily (dozens of downstream sites). Cross-multiplication order on ratio orbits defines leQ p q by comparing p.num * ofOrbit(q.den) with q.num * ofOrbit(p.den), so every rational comparison funnels through ofOrbit. Integer-order facts such as abs_le_iff_between express |z| ≤ n as the two-sided inequality −ofOrbit(n) ≤ z ≤ ofOrbit(n). Choice-free nonnegativity and multiplication lemmas (e.g. nonnegFlag_mul_ofOrbit_right_of_ne_zero_cf) likewise fix the right factor via ofOrbit.
In the Recognition foundation this keeps integer and rational structure internal to the distinction calculus before any external number system is assumed, supporting later forcing-chain and ladder constructions that need ordered arithmetic on orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.