leq_eq_true_iff_cf
plain-language theorem explainer
The structural Boolean order flag on δ-orbit positions equals true exactly when the underlying natural counts satisfy the usual ≤. Anyone building the choice-free signed-orbit order cites this bridge instead of the classical Bool/Decidable version. The proof is bare double induction on the two orbit constructors, reducing each successor step to Nat.succ_le_succ_iff.
Claim. For δ-orbit positions $a,b$, the structural Boolean comparison flag $\mathrm{leq}(a,b)$ equals $\mathsf{true}$ if and only if the iteration counts satisfy $a^{\mathbb{N}} \le b^{\mathbb{N}}$.
background
The module rebuilds the signed-orbit order without routing through SignedOrbit.toInt or Mathlib's $\mathbb{Z}$ order, both of which drag in Classical.choice. Order facts are re-grounded on the finite $\mathbb{N}$ position of the $\delta$-orbit via already choice-free bridges: balanced length as a $\mathbb{N}$ equality, and this Boolean-flag agreement with the $\mathbb{N}$ order.
DistinctionNat is the inductive $\delta$-orbit (zero and succ), with toNat reading off the iteration count exactly as LogicNat.toNat does in ArithmeticFromLogic: identity maps to $0$, step maps to successor. The structural flag leq is defined by recursion on those constructors. Upstream Peano facts used here are toNat_zero, toNat_succ, Nat.le_refl, Nat.zero_le, and Nat.succ_le_succ_iff.
The original leq_eq_true_iff is choice-tainted because simp [leq] pulls classical Bool/Decidable lemmas. This restatement stays inside {propext, Quot.sound}.
proof idea
Structural induction on $a$, generalizing over $b$, then case-split on $b$.
Zero/zero and zero/succ: both directions are immediate from Nat.le_refl / Nat.zero_le and definitional rfl on the flag.
Succ/zero: the flag is definitionally false, so the forward direction is Bool.false_ne_true; the reverse rewrites toNat via toNat_succ and toNat_zero and applies Nat.not_succ_le_zero.
Succ/succ: the flag on successors equals the flag on the predecessors by rfl. Rewrite by the IH and the two toNat_succ identities, then finish with Nat.succ_le_succ_iff.symm. No classical simp, no Decidable, no $\mathbb{Z}$.
why it matters
This is the second of the two choice-free bridges named in the module doc (with balanced_iff_toNat_eq). Downstream, nonnegFlag_iff_nonneg_cf rewrites the structural nonnegative flag through this lemma rather than the $\mathbb{Z}$-tainted nonnegFlag_eq_true_iff_nonneg. The same bridge feeds zero_le_iff_nonnegFlag_cf, the right-multiplication order cancellation le_mul_right_iff_of_nonnegFlag_of_not_balanced_zero_cf, and nonnegFlag_mul_ofOrbit_right_of_ne_zero_cf.
Those rungs are the base the ratio_* ordered-field tower needs without inheriting choice. In the Recognition foundation this keeps the primitive recognition calculus (signed orbits as pre-rational distinctions) inside the forced-floor axiom set {propext, Quot.sound}, so later forcing-chain and ordered-field developments do not silently depend on classical choice at the order layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.