nonneg_iff_toNat_le
plain-language theorem explainer
Nonnegativity of a signed δ-orbit is exactly the ℕ comparison of its negative and positive orbit lengths. Anyone building the choice-free ordered-field tower on SignedOrbit cites this bridge. The proof is a two-direction constructor argument via the balanced-to-toNat equality, then omega on natural numbers.
Claim. For every signed orbit $z$, $z$ is nonnegative if and only if the natural number read from its negative $\delta$-orbit position is at most the natural number read from its positive $\delta$-orbit position: $\mathrm{nonneg}(z)\iff z_{-}\!.\mathrm{toNat}\le z_{+}\!.\mathrm{toNat}$.
background
This module rebuilds the SignedOrbit order without Mathlib integers. The older characterizations route through a display map into $\mathbb{Z}$ and therefore inherit Classical.choice. Here the order is re-grounded on finite $\delta$-orbit positions: each arm of a signed orbit is a DistinctionNat, and toNat simply counts iteration steps from the identity (zero maps to $0$).
Internal nonnegativity means $z$ is balanced against a pure positive orbit: there exists a $\delta$-orbit $k$ such that $z$ equals the signed orbit with positive arm $k$ and zero negative arm. The already choice-free bridge balanced_iff_toNat_eq converts that balance condition into equality of the two toNat readings. Negation of a signed orbit swaps the two arms, matching the LogicInt pattern $(a,b)\mapsto(b,a)$.
The local goal is a forced-floor base whose #print axioms stays inside {propext, Quot.sound}, so every later ratio-order fact can avoid choice taint.
proof idea
Unfold the definition of nonnegativity and split the biconditional.
Forward: from a witness $k$ with $z$ balanced to the pure positive orbit of $k$, rewrite by balanced_iff_toNat_eq. The positive arm of ofOrbit k is $k$ and the negative arm is zero, so toNat_zero reduces the equality to $0\le k.\mathrm{toNat}$, finished by omega.
Reverse: given $z_{-}!.\mathrm{toNat}\le z_{+}!.\mathrm{toNat}$, take the witness ofNat of the difference of the two naturals. Again rewrite by balanced_iff_toNat_eq; the pure-positive ofOrbit arms and the simp facts toNat_zero, toNat_ofNat turn the goal into an arithmetic inequality on $\mathbb{N}$, closed by omega.
why it matters
This is the first collapse step in the choice-free signed-orbit order foundation. Downstream, nonnegFlag_iff_nonneg_cf rewrites the structural Boolean flag through this lemma plus the choice-free leq_eq_true_iff_cf, and le_iff_toNat_cf characterizes the full order as a pure $\mathbb{N}$ inequality on the four arm lengths after subtraction. Together they replace the choice-tainted nonneg_iff_toInt_nonneg and le_iff_toInt_le.
In the Recognition stack this sits under the Primitive Recognition Calculus grow layer: integers and rationals are built from $\delta$-orbits before the forcing chain (T5 J-uniqueness through T8 dimension) and the ordered-field tower that the ratio lemmas need. Closing the order at the {propext, Quot.sound} floor keeps later mass-ladder and constant extractions free of classical choice they do not require.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.