leq
plain-language theorem explainer
Boolean less-or-equal on finite δ-orbit positions, defined by pure structural recursion on the distinction carrier. Anyone building forced order, trichotomy, or choice-free comparison on the orbit cites it. The body is the three-clause Peano recursion: zero is below everything, successor is never below zero, and successors compare by peeling.
Claim. Define a Boolean predicate $\mathrm{le}(a,b)$ on finite $\delta$-orbit positions by structural recursion: $\mathrm{le}(0,\_)=\mathsf{true}$; $\mathrm{le}(S\_,0)=\mathsf{false}$; $\mathrm{le}(Sa,Sb)=\mathrm{le}(a,b)$.
background
The carrier is DistinctionNat, the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with constructors zero and succ, exactly the Peano skeleton without presupposing $\mathbb{N}$. Successor here is one more application of the distinction generator, matching the arithmetic-from-logic reading of step.
This module sits in Primitive Recognition Calculus and builds integer/rational structure from orbit arithmetic. The Boolean order is the forced-side comparison: it never consults a display map to $\mathbb{N}$ or $\mathbb{Z}$ in its definition, so later totality and trichotomy can stay axiom-light.
Upstream, the inductive shape of the orbit and the successor constructor are the only ingredients. No cost functional or ratio orbit enters the definition itself.
proof idea
Definition by pattern match, not a proved theorem. Three exhaustive clauses on the inductive constructors: the zero-left case returns true; the successor-vs-zero case returns false; the double-successor case recurses on the predecessors. No tactics, no lemmas, no classical decidability instance is invoked at definition time.
why it matters
This is the decision procedure that makes forced order computable without Classical. Downstream, forced_order_decidable treats the Boolean recursion itself as the Decidable instance; leq_total_bool and leq_trichotomy_bool prove totality and strict trichotomy by induction and case split on the two Booleans, with empty axiom footprint. Structural antisymmetry (leq_antisymm_structural) stays on the forced carrier and deliberately avoids the choice-tainted toNat bridge.
Choice-free agreement with the $\mathbb{N}$ order (leq_eq_true_iff_cf) and nonnegativity flags on signed orbits also consume it. In the Recognition stack this is foundation plumbing: the discrete order on distinction orbits that later supports integer display, signed orbit arithmetic, and grow-side order facts, all before continuum or LPO-style omniscience appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.