leq_total_bool
plain-language theorem explainer
For any two forced orbit positions, the structural order places at least one below or equal to the other. Foundation authors cite this when they need totality of the forced order on the distinction carrier without classical arithmetic. The argument is induction on the first argument with a case split on the second; no omega, no integers, empty axiom list.
Claim. For all forced orbit positions $a,b$ on the distinction carrier, either the structural order reports $a \leq b$ or it reports $b \leq a$ (as Boolean equalities to true).
background
The Primitive Recognition Calculus builds a natural-number-like carrier from forced distinctions rather than Peano postulates. DistinctionNat is that carrier: forced orbit positions generated by zero and successor. The structural order leq is the Boolean comparison defined recursively on the carrier (imported from the IntegerRational layer).
Totality here means: for any pair of positions, at least one direction of leq evaluates to true. This is the order-theoretic half of a constructive trichotomy package. Upstream, IntegerOrder already records trichotomy for signed orbits by reduction to integer comparison; the present lemma stays on the unsigned forced carrier and never leaves the inductive structure.
Local setting (module ForcedTrichotomy): obtain the forced analogue of real trichotomy by pure case splits on decidable Booleans, with no classical omniscience principle.
proof idea
Tactic proof by induction on $a$, generalizing $b$.
- Zero case:
leq zero bholds definitionally, so the left disjunct isrfl. - Successor case: case-split on $b$. If $b$ is zero, the right disjunct holds definitionally. If $b$ is also a successor, unfold
leq(which recurses on both successors) and discharge by the inductive hypothesis on the predecessors, withsimpa.
No external lemmas beyond the inductive structure of the carrier and the recursive equation for leq. Empty #print axioms.
why it matters
Totality is the first brick in the forced-order package on the distinction carrier. Sibling results (leq_trichotomy_bool, forced_order_decidable, leq_antisymm_structural) assemble full structural trichotomy: exactly one of strictly-below, balanced, or strictly-above, by case split on two decidable Booleans.
That package is the forced analogue of real trichotomy, and it needs none of the omniscience (LPO) that the real version demands. In the Recognition foundation this matters because arithmetic and order are derived from the recognition calculus rather than assumed classically: successor is one more generator application (ArithmeticFromLogic), and order properties must close constructively on the forced carrier.
No downstream consumers are wired yet (used_by empty); the lemma exists to underwrite the trichotomy siblings and any later ledger or mass-ladder comparisons that need a total structural order without classical instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.