ofOrbit_toInt
plain-language theorem explainer
Embedding a finite distinction orbit as a nonnegative signed orbit recovers its natural-number count as an integer. Anyone routing ratio-orbit order through the choice-free integer bridge cites this simp lemma constantly. The proof reduces to the integer identity n − 0 = n and closes by ring.
Claim. For every finite distinction orbit $n$, the integer display of the nonnegative signed orbit with positive part $n$ and zero negative part equals the natural-number iteration count of $n$: if $z = \langle n, 0\rangle$, then $\mathrm{toInt}(z) = \mathrm{toNat}(n)$ in $\mathbb{Z}$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Its verifier map toNat reads off the iteration count as a Lean natural.
Signed orbits package a pair of such positions (positive and negative parts). The display map sends a signed orbit $z$ to the integer $(\mathrm{toNat}(z.\mathrm{pos}):\mathbb{Z}) - (\mathrm{toNat}(z.\mathrm{neg}):\mathbb{Z})$. The constructor ofOrbit builds the nonnegative case: positive part $n$, negative part zero.
This module sits under the foundation layer that grows integers and rationals from recognition orbits without classical choice, feeding the later ratio-orbit order and arithmetic.
proof idea
One-line definitional reduction. Expanding ofOrbit n gives the pair $\langle n, 0\rangle$; expanding the signed-orbit integer display gives $(\mathrm{toNat}(n):\mathbb{Z}) - (\mathrm{toNat}(0):\mathbb{Z})$. The goal is rewritten as $n - 0 = n$ in $\mathbb{Z}$ and closed by ring. No induction and no external lemmas beyond the definitions of ofOrbit and toInt.
why it matters
This simp lemma is the standard bridge from nonnegative orbit positions into integer arithmetic. Downstream ratio-orbit order theorems (leQ_trans, leQ_antisymm, leQ_add_right, leQ_mul_nonneg_right, zero_leQ_iff, leQ_neg_neg_iff) all reduce cross-multiplication inequalities to integer comparisons and fire this lemma to collapse denominator and numerator displays built from ofOrbit.
It is pure foundation scaffolding for the choice-free ordered-ring structure on ratio orbits, not a physics forcing step (T0–T8). Without it, every simp chain that moves between signed-orbit products and Int inequalities would have to unfold by hand. It also feeds absolute-value and betweenness facts in the integer-order layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.