le_iff_nonnegFlag_sub_cf
plain-language theorem explainer
Signed-orbit order is equivalent to the structural nonnegative Boolean of the difference being true. Builders of the choice-free ratio ordered-field tower cite this in place of the ℤ-tainted bridge. The proof unfolds the internal order definition and rewrites by the choice-free flag–nonnegativity equivalence.
Claim. For signed orbits $a,b$ (each a pair of distinction-nats meaning $\mathrm{pos}-\mathrm{neg}$), one has $a\le b$ if and only if the structural nonnegative flag of $b-a$ equals $\mathsf{true}$.
background
A signed orbit is a pair of distinction-nats $(\mathrm{pos},\mathrm{neg})$ with intended meaning $\mathrm{pos}-\mathrm{neg}$. Internal order is defined by nonnegativity of the difference: $a\le b$ means $b-a$ is nonnegative. The structural nonnegative flag is the Boolean leq comparison of the two sides, a pure finite-$\mathbb{N}$ check.
The ambient module rebuilds the signed-orbit order without routing through toInt : SignedOrbit → ℤ or Mathlib's integer order, both of which import classical choice. Two already choice-free bridges are used: balanced length as a $\mathbb{N}$-equality, and agreement of the structural Boolean with the $\mathbb{N}$ order. After that, nonnegativity and the flag both collapse to $z.\mathrm{neg}.\mathrm{toNat}\le z.\mathrm{pos}.\mathrm{toNat}$.
Upstream, the choice-free flag–nonnegativity theorem states that the structural flag equals true exactly when internal nonnegativity holds, proved via the $\mathbb{N}$-level leq bridge rather than the integer display.
proof idea
One-line wrapper. Unfold the definition of signed-orbit order, which is nonnegativity of the difference $b-a$. Rewrite by the upstream choice-free equivalence between the structural nonnegative flag and internal nonnegativity. The two sides match immediately; no further arithmetic is required.
why it matters
This is the choice-free replacement for the tainted difference-flag characterization of order. Downstream, the zero-lower-bound form (zero $\le z$ iff the flag of $z$ is true) is obtained by specializing this theorem and simplifying the subtraction against zero. That zero form, together with reflexivity, transitivity, totality, and balanced antisymmetry in the same module, is the base the ratio_* ordered-field tower needs without classical choice.
Forced-floor receipt for the module is that every theorem's axiom footprint is a subset of {propext, Quot.sound}. In the Recognition foundation this keeps the arithmetic-from-logic ladder free of choice before any physics constants or forcing-chain steps are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.