le_total_cf
plain-language theorem explainer
Totality of the non-strict order on signed orbits: for any two signed orbits a and b, either a ≤ b or b ≤ a. Builders of the choice-free ordered-field tower on ratio orbits cite this as the integer-level totality step. The proof rewrites both sides through the ℕ-level δ-orbit characterization and closes by omega on natural inequalities.
Claim. For any two signed orbits $a$ and $b$, either $a \le b$ or $b \le a$, where $\le$ is the choice-free non-strict order on signed orbits (equivalently, the order of their $\delta$-orbit natural positions).
background
A signed orbit packages a pair of finite $\delta$-orbit positions (positive and negative legs). The ambient module rebuilds the signed-orbit order without routing through toInt : SignedOrbit → ℤ, because Mathlib's integer order imports classical choice and would taint every later ratio-order rung.
The choice-free bridge is the ℕ characterization: $a \le b$ if and only if $b_{\mathrm{neg}}.\mathrm{toNat} + a_{\mathrm{pos}}.\mathrm{toNat} \le b_{\mathrm{pos}}.\mathrm{toNat} + a_{\mathrm{neg}}.\mathrm{toNat}$. Balanced length is likewise a pure ℕ equality of orbit positions. Once nonnegativity and the order flag collapse to that single natural comparison, reflexivity, transitivity, totality, and antisymmetry-to-balanced become ordinary omega facts over ℕ.
Upstream, the sibling lemma that supplies the rewrite is exactly that ℕ-level iff for the order. The module's forced-floor receipt is that every theorem here has axiom footprint inside {propext, Quot.sound}.
proof idea
Term-style tactic proof in two moves. Rewrite both disjuncts with the choice-free characterization (order iff a four-term inequality of toNat positions). The goal becomes a disjunction of two linear inequalities on natural numbers, which omega discharges by totality of ≤ on ℕ.
why it matters
This is the integer-level totality brick for the choice-free ordered-field tower. Downstream, ratio-orbit totality applies it at the two cross-products: for any two ratio orbits p and q one has leQ p q or leQ q p. The companion reflexivity rung is the same pattern via the reflexivity sibling.
In the Recognition foundation stack this clears classical choice out of the signed-orbit and ratio-orbit orders before any physics constants or forcing-chain steps are attached. The module exists so later ratio_* lemmas inherit only propext and Quot.sound, matching the forced-floor receipt stated in the module doc. It does not itself touch T5–T8, RCL, or the mass ladder; it is pure order infrastructure those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.