le_refl_cf
plain-language theorem explainer
Reflexivity of the internal order on signed orbits, proved without classical choice. Anyone assembling the choice-free ordered-field tower on ratio orbits cites this as the base rung. The proof rewrites the order to a pure ℕ comparison of δ-orbit positions and closes by omega.
Claim. For every signed orbit $a$ (a pair of distinction-nats read as $\mathrm{pos}-\mathrm{neg}$), one has $a \le a$, where $x \le y$ means that the signed difference $y-x$ is nonnegative.
background
A SignedOrbit is a pair of distinction-nats (pos, neg) with intended meaning $\mathrm{pos}-\mathrm{neg}$. Its internal order is defined by nonnegativity of the difference: $a \le b$ iff $b-a$ is nonnegative.
The original characterizations route through toInt : SignedOrbit → ℤ and Mathlib's integer order, which imports Classical.choice. This module re-grounds the order on δ-orbit positions toNat : DistinctionNat → ℕ via two choice-free bridges (balanced length as ℕ equality, and the structural Boolean flag agreeing with the ℕ order). Both nonnegativity and the nonneg flag collapse to the single fact $z.\mathrm{neg}.\mathrm{toNat} \le z.\mathrm{pos}.\mathrm{toNat}$.
The key upstream lemma is the choice-free characterization: $a \le b$ iff $b.\mathrm{neg}.\mathrm{toNat} + a.\mathrm{pos}.\mathrm{toNat} \le b.\mathrm{pos}.\mathrm{toNat} + a.\mathrm{neg}.\mathrm{toNat}$. Forced-floor receipt: axioms stay inside {propext, Quot.sound}.
proof idea
One-line tactic proof. Rewrite the goal with the choice-free characterization le_iff_toNat_cf, which turns $a \le a$ into the ℕ inequality $a.\mathrm{neg}.\mathrm{toNat} + a.\mathrm{pos}.\mathrm{toNat} \le a.\mathrm{pos}.\mathrm{toNat} + a.\mathrm{neg}.\mathrm{toNat}$. That is pure additive commutativity on ℕ, discharged by omega.
why it matters
This is the reflexivity rung of the choice-free signed-orbit order foundation. Downstream, the cross-multiplication order leQ on ratio orbits is defined by comparing two signed-orbit products, and leQ_refl is proved by applying this theorem at the identical cross-product on both sides. Without a choice-free reflexivity here, every later ratio_* ordered-field fact would inherit classical choice through the old toInt path. It sits in the Primitive Recognition Calculus grow layer that builds arithmetic from distinction structure before the forcing chain (T0–T8) and the Recognition Composition Law are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.