forced_order_decidable
plain-language theorem explainer
On the forced carrier DistinctionNat, the structural order is decidable without classical logic: the Bool-valued recursion that defines the comparison is itself the decision procedure. Foundation work that stays on the forced side (trichotomy, antisymmetry, growth) cites this when a computational yes/no is required rather than excluded middle. The body is a one-line inferInstance, since Bool equality is already decidable.
Claim. For any two positions $a,b$ of the forced carrier, the proposition "$a \le b$ holds" (i.e. the structural Boolean comparison returns true) is decidable by a finite computation, with no classical choice.
background
In the Primitive Recognition Calculus, positions live on a forced carrier (DistinctionNat) built before any bridge to ordinary $\mathbb{N}$ or $\mathbb{Z}$. The order relation is not postulated classically: it is a structural recursion leq returning Bool, defined in the IntegerRational layer and reused here as the forced comparison.
The local module ForcedTrichotomy packages the order facts that stay purely on that carrier: totality and trichotomy as Boolean identities, decidability of the true-branch, and structural antisymmetry. The point of the package is to keep comparison computational so later growth and display arguments do not smuggle in Classical or omega-tainted bridges.
Upstream, toNat reads iteration count off a logic-nat orbit, but this declaration deliberately does not need that display: decidability is native to the Bool recursion itself.
proof idea
One-line definition: inferInstance. Lean already has a Decidable instance for equality on Bool, and leq a b is definitionally a Bool, so Decidable (leq a b = true) is synthesized with no custom cases, no classical axioms, and no appeal to toNat.
why it matters
Recognition Science forces structure from a single functional equation and a discrete carrier; order on that carrier must be a finite computation, not an act of omniscience. This instance records that fact for the forced order, so proofs of trichotomy, antisymmetry, and growth can branch on leq without Classical.
It sits beside the Boolean totality/trichotomy lemmas and the structural antisymmetry result in the same module (the latter explicitly avoids the choice-tainted toNat bridge). No downstream consumers are wired yet in the graph; the declaration is infrastructure for forced-side order reasoning in the foundation layer, aligned with keeping the forcing chain free of classical residue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.