leq_trichotomy_bool
plain-language theorem explainer
On the forced finite distinction-orbit carrier, any two positions fall into exactly one of three Boolean regimes: strictly below, balanced (mutual ≤), or strictly above. Order and decidability developments on that carrier cite it as the constructive trichotomy step. The argument is a pure two-level case split on the structural Boolean comparison; the axiom footprint is empty.
Claim. For any two finite distinction-orbit positions $a$ and $b$, either $a \le b$ holds and $b \le a$ fails, or both $a \le b$ and $b \le a$ hold, or else $a \le b$ fails.
background
The carrier is the base-neutral finite orbit of repeated distinction: an inductive type with zero and successor, the discrete positions generated by iterating a single distinction step. Comparison on that carrier is a Boolean predicate defined by structural recursion alone: zero is below every position; a successor is never below zero; and successor-to-successor reduces to the predecessors. No classical choice or real completeness enters the definition.
The local module packages forced order facts for this carrier: totality, trichotomy, decidability without Classical, and structural antisymmetry. Upstream, the Boolean order is exactly the recursive leq on those orbit positions. The point of the package is to obtain a forced analogue of ordered comparison whose decision procedure is finite computation on the orbit, not an omniscience principle.
proof idea
Pure case analysis on the two Boolean values. First split on whether $a \le b$ holds. If it is false, the third disjunct is immediate by reflexivity of Boolean equality. If it is true, split on whether $b \le a$ holds: false yields the strictly-below arm; true yields the balanced arm. Each arm is closed by pairing the two Boolean equalities (or the single false equality). No external lemmas are required beyond the inductive cases of the structural comparison.
why it matters
This is the forced-carrier stand-in for real trichotomy, obtained without the limited principle of omniscience that classical real trichotomy is equivalent to. The doc-comment stresses that deciding the order is a finite computation on the orbit, not an act of omniscience, and that #print axioms is empty. Together with the sibling totality, decidability, and antisymmetry facts, it closes the structural order interface used when the recognition calculus treats the finite distinction orbit as an ordered discrete line. No downstream consumers are wired yet in the graph; the result sits as a leaf that any later forced-order or Grow-layer argument can invoke when it needs exclusive case analysis on below / equal / above.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.