IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.ForcedTrichotomy
The forced structural order on DistinctionNat is total and decidable: any two forced orbit positions compare. The module proves totality, trichotomy, antisymmetry, and decidability by induction on the carrier alone, with an empty axiom footprint. Anyone building the primitive recognition calculus order layer cites these facts before lifting to integers or rationals.
claimOn the forced orbit carrier $\mathrm{DistinctionNat}$, the structural order $\le$ is total: for all $a,b$, either $a\le b$ or $b\le a$. Trichotomy, structural antisymmetry, and decidability of $\le$ hold by induction on the carrier, without $\omega$, $\mathbb{Z}$, or classical choice.
background
Primitive Recognition Calculus builds arithmetic from forced orbit positions rather than from classical $\mathbb{N}$ or $\mathbb{Z}$. The carrier $\mathrm{DistinctionNat}$ indexes those positions; the structural order $\le$ is the order induced by the forcing construction itself, not by an external well-order axiom.
The parent layer IntegerRational supplies the integer and rational scaffolding that sits above this carrier. This module stays strictly below that lift: it only concerns comparisons internal to $\mathrm{DistinctionNat}$.
The doc-comment states the design constraint explicitly: proofs use induction on the carrier, with no omega, no $\mathbb{Z}$, and no classical instance, so #print axioms is empty.
proof idea
Four sibling results form the argument. Totality and trichotomy are proved as Boolean-valued comparisons (leq_total_bool, leq_trichotomy_bool) by induction on the carrier. Decidability of the forced order (forced_order_decidable) packages those Boolean facts into a decision procedure. Structural antisymmetry (leq_antisymm_structural) closes the order axioms. No classical logic or external arithmetic tactics are used.
why it matters in Recognition Science
Without a total, decidable structural order on forced orbit positions, later lifts to integers, rationals, and the recognition cost calculus cannot compare rungs constructively. This module is the order kernel of the Grow layer in Primitive Recognition Calculus: it guarantees that forced positions form a decidable total preorder before any embedding into $\mathbb{Z}$ or $\mathbb{Q}$.
Downstream consumers (none yet wired in the graph) will use these facts wherever the phi-ladder or eight-tick bookkeeping needs a constructive comparison of orbit indices. The empty axiom footprint keeps the foundation aligned with the forcing-chain discipline (T0–T8), which demands that structure be forced rather than postulated.
scope and limits
- Does not construct integers, rationals, or the phi-ladder; only orders DistinctionNat.
- Does not prove well-foundedness or induction principles beyond carrier induction used here.
- Does not connect structural order to the J-cost or Recognition Composition Law.
- Does not assert classical excluded middle; comparisons are Boolean and constructive.
- Does not yet record downstream used-by edges in the dependency graph.