le_iff_toNat_cf
plain-language theorem explainer
Signed-orbit order a ≤ b is equivalent to a pure ℕ inequality on the four δ-orbit positions: b.neg + a.pos ≤ b.pos + a.neg under toNat. Anyone building the choice-free ratio-orbit ordered field cites this instead of the ℤ-routed le_iff_toInt_le. The proof unfolds le to nonneg of the difference, applies the sibling nonneg_iff_toNat_le bridge, and rewrites the two toNat_add equalities.
Claim. For signed orbits $a,b$, one has $a \le b$ if and only if $\mathrm{toNat}(b_{-}) + \mathrm{toNat}(a_{+}) \le \mathrm{toNat}(b_{+}) + \mathrm{toNat}(a_{-})$, where $a_{\pm}, b_{\pm}$ are the positive and negative $\delta$-orbit components and $\mathrm{toNat}$ reads the finite iteration count.
background
The ambient module rebuilds the signed-orbit order without Mathlib $\mathbb{Z}$. In the older path, $a \le b$ is defined via $\mathrm{toInt}$ and Mathlib's integer order, which pulls in Classical.choice. Every later ratio-orbit rung then inherits that taint. Here the order is re-grounded on $\delta$-orbit positions: each component is a DistinctionNat (equivalently a LogicNat), and toNat is the forward map that reads the iteration count.
A signed orbit is a pair of nonnegative $\delta$-orbits (pos, neg). Subtraction swaps and adds components in the usual way: $(b-a){+} = b{+} + a_{-}$ and $(b-a){-} = b{-} + a_{+}$. The structural predicate $a \le b$ means the difference $b-a$ is nonnegative. The sibling bridge nonneg_iff_toNat_le already collapses nonnegativity of a single signed orbit $z$ to the $\mathbb{N}$ fact $z_{-}.\mathrm{toNat} \le z_{+}.\mathrm{toNat}$. Addition of distinction-nats is recovered by toNat_add, so componentwise sums become ordinary Nat sums.
The module's forced-floor receipt is that every theorem here has #print axioms inside ${\mathrm{propext}, \mathrm{Quot.sound}}$: no choice, no $\mathbb{Z}$ order.
proof idea
Term-mode rewrite chain. Unfold SignedOrbit.le so the goal is nonnegativity of $b-a$. Apply the sibling nonneg_iff_toNat_le to turn that into $(b-a){-}.\mathrm{toNat} \le (b-a){+}.\mathrm{toNat}$. Two definitional equalities identify the difference components: $(b-a){+} = b{+} + a_{-}$ and $(b-a){-} = b{-} + a_{+}$. Rewrite both, then fire DistinctionNat.toNat_add twice to push toNat through the sums, landing exactly on $b_{-}.\mathrm{toNat} + a_{+}.\mathrm{toNat} \le b_{+}.\mathrm{toNat} + a_{-}.\mathrm{toNat}$.
why it matters
This is the choice-free $\mathbb{N}$-level characterization of signed-orbit order that the entire ratio_* ordered-field tower needs. Downstream, ltQ_iff_toNat rewrites ratio strict order through this bridge plus balanced equality; zero_ltQ_iff_num and zero_ltQ_one use it to pin positivity of ratio orbits; the add-mono layer routes its private le_iff_toInt_le_cf through this lemma rather than the tainted le_iff_toInt_le; left/right congruence under balanced equivalence and the mul-right iff for nonnegative flags all rewrite order via this fact.
In the Recognition foundation stack this sits under the primitive recognition calculus that eventually feeds the forcing chain (T0–T8). It does not itself force $\varphi$ or $D=3$; it clears classical choice from the integer/rational order substrate so later rungs stay axiom-light. The doc-comment states it explicitly as the replacement for le_iff_toInt_le.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.