Foundation Primitive Recognition Calculus Grow Forced Trichotomy

Forced trichotomy

Trichotomy is the classical principle that for any two numbers, exactly one of less than, equal to, or greater than holds. For real numbers, that principle is surprisingly heavy: proving it constructively requires a logical choice principle called the limited principle of omniscience, because comparing two arbitrary reals can demand infinite information. The framework's ledger, a discrete record of recognition events, sidesteps the whole issue. Its positions are built by finite steps, so comparing them is a finite computation.

The module ForcedTrichotomy proves that on the ledger's forced carrier, trichotomy holds without any choice principle. The proof is a case split on two decidable Booleans, and the machine-checked library of formal theorems records no axioms beyond the ambient type theory's standard three. The order relation itself is the decision procedure: deciding whether one position is below another is just running a structural recursion, not an act of omniscience.

Concretely, the theorem states that for any two forced positions a and b, exactly one of three cases holds: a is strictly below b, a is balanced with b, or a is strictly above b. The proof is by induction on the carrier, and the antisymmetry witness stays on the forced carrier, deliberately avoiding a bridge to natural numbers that would reintroduce choice. This is the forced analogue of real trichotomy, but it needs none of the omniscience that the real version demands.

What this changes: the framework can order its own structure without importing classical assumptions. The order is total, decidable, and antisymmetric, all proved by pure structural recursion. That means the ledger's internal comparisons are computationally real, not logically ideal. For a reader, the takeaway is that the framework's foundational order is not a borrowed classical convenience but a forced consequence of the discrete structure itself.

/-- The forced structural order on `DistinctionNat` is total: for any two forced
orbit positions, one is structurally below the other. Proved by induction on the
carrier; no `omega`, no `ℤ`, no classical instance. `#print axioms` is empty. -/
theorem leq_total_bool (a b : DistinctionNat) :
    leq a b = true ∨ leq b a = true := by
  induction a generalizing b with
  | zero => exact Or.inl rfl
  | succ a ih =>
      cases b with
      | zero => exact Or.inr rfl
      | succ b =>
          have := ih b
          unfold leq
          simpa using this

/-- Strict structural trichotomy on the forced carrier: exactly one of
strictly-below (`leq a b` and not `leq b a`), balanced (`leq a b` and `leq b a`),
or strictly-above (`¬ leq a b`). Pure case split on two decidable Booleans;
`#print axioms` is empty. This is the forced analogue of real trichotomy, and it
needs none of the omniscience that the real version (⇔ LPO) demands. -/
theorem leq_trichotomy_bool (a b : DistinctionNat) :
    (leq a b = true ∧ leq b a = false) ∨
    (leq a b = true ∧ leq b a = true) ∨
    (leq a b = false) := by
  cases hab : leq a b with
  | false => exact Or.inr (Or.inr rfl)
  | true =>
      cases hba : leq b a with
      | false => exact Or.inl ⟨rfl, rfl⟩
      | true => exact Or.inr (Or.inl ⟨rfl, rfl⟩)

/-- The forced order relation is decidable WITHOUT `Classical`: the structural
`Bool` recursion `leq` is itself the decision procedure. Deciding `<` on the
forced carrier is a finite computation, not an act of omniscience. -/
def forced_order_decidable (a b : DistinctionNat) : Decidable (leq a b = true) :=
  inferInstance

What this page does not claim

This module does not prove trichotomy for real numbers; that remains tied to the limited principle of omniscience. The order is on the forced carrier only, not on any arbitrary extension of the ledger.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/Grow/ForcedTrichotomy.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: