leq_eq_true_iff
plain-language theorem explainer
The structural Boolean order on finite δ-orbit positions returns true exactly when the underlying generator counts satisfy ordinary ℕ inequality. Order and absolute-value lemmas on signed orbits cite this as the choice-free bridge to the verifier. The proof is double structural induction, reducing the successor case to Nat.succ_le_succ_iff.
Claim. For finite $\delta$-orbit positions $a$ and $b$, the recursively defined Boolean comparison evaluates to true if and only if the iteration count of $a$ is at most that of $b$: the Boolean predicate holds $\iff$ $\mathrm{count}(a)\le\mathrm{count}(b)$ in $\mathbb{N}$.
background
In the primitive recognition calculus, finite $\delta$-orbit positions (DistinctionNat) are the inductive carrier built by iterating a generator from a zero. The map that reads off the iteration count sends each such position to an ordinary natural number; it is the same forward map used for logic-nats in ArithmeticFromLogic.
The internal Boolean order is defined by structural recursion alone: zero is $\le$ everything, a successor is never $\le$ zero, and successors compare by comparing their predecessors. No classical decision procedure is invoked; the recursion is the decision procedure.
This module sits under IntegerRational and feeds IntegerOrder. Upstream, Peano facts such as reflexivity and zero-least are already theorems of the inductive structure rather than axioms. The present statement equates the Boolean recursion with the verifier order on counts.
proof idea
Term-mode proof by induction on the first argument, generalizing the second, with a case split on the second at each step.
Zero against zero: both sides hold by reflexivity of $\le$ on $0$ and rfl on the Boolean. Zero against a successor: left is definitionally true, right is Nat.zero_le.
Successor against zero: left is definitionally false, so the forward direction is Bool.noConfusion; the reverse is Nat.not_succ_le_zero.
Successor against successor: rewrite by the inductive hypothesis, then apply Nat.succ_le_succ_iff. No classical axioms beyond propext appear.
why it matters
This is the choice-free bridge that lets every later order fact on signed orbits discharge Boolean comparisons by rewriting to ordinary ℕ inequalities. Downstream, forced trichotomy uses it so that decidability of the forced order is just the structural Boolean recursion (no Classical). Nonnegativity of a signed orbit collapses to a pure count inequality via the same bridge.
IntegerOrder leans on it heavily: triangle inequalities for absolute value (abs_add_le_add_abs, abs_sub_le_add_abs), the betweenness characterization of absolute bounds, transitivity of absolute comparisons, and the integer-order certificate all open with a rewrite along this equivalence. Without it, the internal Boolean order would be an opaque recursion rather than a verified display of ℕ order.
In the Recognition forcing chain this sits in the arithmetic foundation beneath T5–T8: order on orbits must be forced and decidable before mass ladders and dimensional constraints can be stated choice-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.