le_iff_toInt_le_cf
plain-language theorem explainer
Equivalence between the internal signed-orbit order and ordinary integer comparison of the recovered integers. Anyone proving translation invariance or additivity of the ratio-orbit order cites this bridge. The proof rewrites through the choice-free Nat characterization and the pos/neg difference formula for toInt, then finishes both directions by omega.
Claim. For signed orbits $a,b$, one has $a \le b$ if and only if the recovered integers satisfy $a^{\mathrm{toInt}} \le b^{\mathrm{toInt}}$. The left-hand order is the internal nonnegativity of $b-a$; the right-hand comparison is the standard order on $\mathbb{Z}$.
background
Signed orbits are the integer layer of the primitive recognition calculus: each carries a pair of nonnegative ratio-orbit positions (pos, neg). Internal order is defined by nonnegativity of the difference: $a \le b$ means $\mathrm{sub}(b,a)$ is nonnegative. The recovery map $\mathrm{toInt}$ sends a signed orbit to an ordinary integer.
The module develops a choice-free unfold of that recovery: $\mathrm{toInt}(a)$ equals the integer difference of the Nat casts of the pos and neg components. Upstream, le_iff_toNat_cf already characterizes signed-orbit order purely at the Nat level on $\delta$-orbit positions: $a \le b$ iff $b.neg + a.pos \le b.pos + a.neg$ as natural numbers. That theorem is the choice-free replacement for any path that would route through a choice-tainted Int-order lemma.
Local setting is the Grow stack that builds additive monotonicity of the delta-native ratio order from these integer bridges.
proof idea
Rewrite the goal with the choice-free Nat bridge le_iff_toNat_cf and the two instances of toInt_eq, so both sides become comparisons of integer differences of Nat casts. Split the biconditional. Each direction is a pure arithmetic inequality on four natural numbers, discharged by omega. No case splits on signs and no appeal to the choice-tainted Int-order characterization.
why it matters
Feeds directly into leQ_add_right, the translation-invariance theorem for the delta-native ratio order: if $p \le_Q q$ then $p+r \le_Q q+r$. That parent rewrites its hypotheses through this lemma, then simplifies the additive structure on recovered integers. Without a choice-free Int bridge, additive monotonicity of RatioOrbit would inherit classical choice from the older le_iff_toInt_le path. In the Recognition foundation this keeps the integer and rational layers of the forcing chain constructive, so later mass-ladder and octave constructions do not smuggle choice into order facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.