IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.ForcedTrichotomy
The forced structural order on DistinctionNat is total: any two forced orbit positions are comparable. The module proves totality, trichotomy, decidability, and structural antisymmetry by induction on the carrier, with no omega, integers, or classical axioms. Foundation authors cite it when building the ordered growth calculus for primitive recognition. Proofs stay constructive and axiom-free.
claimOn the carrier of forced orbit positions $\mathrm{DistinctionNat}$, the structural order $\le$ is total: for all $a,b$, either $a\le b$ or $b\le a$. The module also records Boolean trichotomy, decidability of the order, and structural antisymmetry, all proved by induction without classical choice or integer arithmetic.
background
Primitive recognition calculus builds discrete structure from forced distinctions rather than from $\mathbb{Z}$ or classical order. DistinctionNat is the carrier of forced orbit positions under that growth process. The structural order compares two such positions by how they sit in the forced construction, not by an external numeric embedding.
The parent layer IntegerRational supplies the integer and rational scaffolding used elsewhere in the calculus, but this module deliberately avoids omega, $\mathbb{Z}$, and classical instances. The goal is a total, decidable order whose only axioms are those of the constructive core (empty #print axioms).
Sibling results in the module package totality as a Boolean predicate, upgrade it to trichotomy, prove the order is decidable, and record structural antisymmetry. Together they make the forced order a usable total order on orbit positions.
proof idea
The argument is inductive on the DistinctionNat carrier. Totality of the structural order is obtained by induction, then packaged as a Boolean comparison (leq_total_bool) and as trichotomy (leq_trichotomy_bool). Decidability of the forced order follows from the Boolean form. Structural antisymmetry is proved in the same inductive style. No omega tactics, no integer embedding, and no classical decidability instances are used; the development stays inside constructive Lean.
why it matters in Recognition Science
A total, decidable structural order on forced orbit positions is prerequisite infrastructure for the Grow layer of primitive recognition calculus. Without it, later comparisons of distinctions, rung placement, and growth steps cannot be stated constructively. The module sits under Foundation and feeds any downstream development that needs ordered DistinctionNat (growth rules, orbit ranking, and related forcing lemmas).
In the broader Recognition Science chain, discrete ordered carriers support the path from the Recognition Composition Law and J-cost uniqueness toward the eight-tick octave and dimension forcing. This file closes the constructive totality gap for the forced order itself: empty axiom footprint, induction-only proofs, and Boolean interfaces ready for later automation.
scope and limits
- Does not define DistinctionNat or the structural order itself; those come from upstream modules.
- Does not embed the order into integers or rationals; IntegerRational is imported but not used as a numeric model here.
- Does not claim classical totality via excluded middle; proofs are constructive and axiom-free.
- Does not by itself force physical constants, phi, or dimension; it only orders orbit positions.
- Does not list downstream consumers in-repo; used_by is currently empty.