le_trans_cf
plain-language theorem explainer
Transitivity of the internal order on signed orbits, proved without classical choice. Anyone assembling a choice-free ordered-field tower on signed orbits (the ratio_* layer) cites this. The proof rewrites both hypotheses and the goal through the ℕ-level δ-orbit characterization, then closes by omega on natural-number inequalities.
Claim. Let $a,b,c$ be signed orbits (pairs of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$). If $a\le b$ and $b\le c$ in the internal order ($x\le y$ means $y-x$ is nonnegative), then $a\le c$.
background
A signed orbit is a pair $(\mathrm{pos},\mathrm{neg})$ of distinction-nats, intended as the difference $\mathrm{pos}-\mathrm{neg}$. Its internal order is defined by $a\le b$ iff the difference $b-a$ is nonnegative.
The ambient IntegerRational development characterizes that order via toInt into Mathlib $\mathbb{Z}$, which imports classical choice. This module rebuilds the order entirely on finite $\mathbb{N}$ positions of the $\delta$-orbit: nonnegativity collapses to a single comparison of natural numbers on the positive and negative legs.
The key upstream bridge is the choice-free characterization: $a\le b$ if and only if $b.neg.toNat + a.pos.toNat \le b.pos.toNat + a.neg.toNat$. With that bridge in hand, order axioms become pure arithmetic on $\mathbb{N}$.
proof idea
One short tactic proof. Rewrite both hypotheses and the goal with the choice-free characterization le_iff_toNat_cf, turning $a\le b$, $b\le c$, and $a\le c$ into three inequalities of natural numbers built from the four toNat legs. Then omega discharges the resulting $\mathbb{N}$ transitivity obligation. No appeal to toInt, $\mathbb{Z}$, or classical choice.
why it matters
This is one of the four elementary order axioms (refl, trans, total, antisymm-to-balanced) re-proved on the choice-free base. The module doc states the forced-floor receipt: every theorem here has #print axioms inside {propext, Quot.sound}. That base is exactly what the downstream ratio_* ordered-field tower needs so that ordered comparisons on rational-like objects do not inherit classical choice from Mathlib $\mathbb{Z}$.
No direct used_by edges are recorded yet; the declaration sits among its siblings (le_refl_cf, le_total_cf, le_antisymm_balanced_cf) as infrastructure for that tower. In the broader Recognition forcing chain it is foundation plumbing rather than a T0–T8 landmark, but without a choice-free order the later arithmetic-from-logic development cannot stay constructive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.