IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.ForcedTrichotomy

   1/-
   2  PrimitiveRecognitionCalculus/Grow/ForcedTrichotomy.lean
   3
   4  Delta forced-math frontier: the FORCED HALF of the LPO door.
   5
   6  Context (DELTA_FRONTIER.md). The demarcation claim is that the forced/posited
   7  boundary coincides with the constructive/classical boundary. One named-family
   8  wall is LPO: over the classical reals, trichotomy
   9  (`x < y ∨ x = y ∨ y < x` decided) is equivalent to the limited principle of
  10  omniscience. The contrast that makes the demarcation real is that on the
  11  FORCED discrete carrier the same trichotomy holds with NO omniscience at all:
  12  it is structural, decidable, and needs no axiom whatsoever.
  13
  14  This module proves that contrast on the forced side, mechanically. The forced
  15  carrier is `DistinctionNat` (the forced ℕδ) with its structural Boolean order
  16  `leq` (pure decidable recursion, no `ℤ`, no `omega`, no `Decidable.decide`
  17  shortcut into the classical instance). We show:
  18
  19  * `leq_total_bool`     : the forced order is total (one of the two directions
  20                           holds), by induction on the carrier;
  21  * `leq_trichotomy_bool`: the strict structural trichotomy (strictly below /
  22                           balanced / strictly above) by case split on the two
  23                           decidable Booleans;
  24  * `forced_order_decidable` : the forced order is genuinely decidable WITHOUT
  25                           `Classical` (the structural `Bool` IS the decision).
  26
  27  The point is the AXIOM RECEIPT, not the statements: every theorem here has
  28  `#print axioms` EMPTY (not even `propext`/`Quot.sound`). Compare the existing
  29  `SignedOrbit.trichotomy` in `IntegerOrder.lean`, which routes through `.toInt`
  30  and `omega` and therefore inherits `Classical.choice` from the classical `ℤ`
  31  order. That route is the DISPLAY trichotomy (honest, but choice-tainted and
  32  ℤ-facing); THIS is the forced trichotomy. The de-classicalization the frontier
  33  asks for is exactly to relocate trichotomy off the ℤ display and onto the
  34  forced structural recursion, where omniscience never enters.
  35
  36  Forced-side reading for the demarcation: the LPO wall is a property of the
  37  COMPLETED continuum, not of order-as-such. Distinction forces a decidable
  38  total order for free; only the posited completion makes deciding `<` an act of
  39  omniscience. So the LPO boundary sits at completeness, exactly as the
  40  orientation predicts, and this module is the forced anchor on one side of it.
  41
  42  Nothing here is auto-merged; this lands on a `steve/` branch for human review.
  43  lake + `#print axioms` are the sole authority.
  44-/
  45import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
  46
  47namespace IndisputableMonolith
  48namespace Foundation
  49namespace PrimitiveRecognitionCalculus
  50namespace Grow
  51
  52open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  53open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DistinctionNat
  54
  55/-- The forced structural order on `DistinctionNat` is total: for any two forced
  56orbit positions, one is structurally below the other. Proved by induction on the
  57carrier; no `omega`, no `ℤ`, no classical instance. `#print axioms` is empty. -/
  58theorem leq_total_bool (a b : DistinctionNat) :
  59    leq a b = true ∨ leq b a = true := by
  60  induction a generalizing b with
  61  | zero => exact Or.inl rfl
  62  | succ a ih =>
  63      cases b with
  64      | zero => exact Or.inr rfl
  65      | succ b =>
  66          have := ih b
  67          unfold leq
  68          simpa using this
  69
  70/-- Strict structural trichotomy on the forced carrier: exactly one of
  71strictly-below (`leq a b` and not `leq b a`), balanced (`leq a b` and `leq b a`),
  72or strictly-above (`¬ leq a b`). Pure case split on two decidable Booleans;
  73`#print axioms` is empty. This is the forced analogue of real trichotomy, and it
  74needs none of the omniscience that the real version (⇔ LPO) demands. -/
  75theorem leq_trichotomy_bool (a b : DistinctionNat) :
  76    (leq a b = true ∧ leq b a = false) ∨
  77    (leq a b = true ∧ leq b a = true) ∨
  78    (leq a b = false) := by
  79  cases hab : leq a b with
  80  | false => exact Or.inr (Or.inr rfl)
  81  | true =>
  82      cases hba : leq b a with
  83      | false => exact Or.inl ⟨rfl, rfl⟩
  84      | true => exact Or.inr (Or.inl ⟨rfl, rfl⟩)
  85
  86/-- The forced order relation is decidable WITHOUT `Classical`: the structural
  87`Bool` recursion `leq` is itself the decision procedure. Deciding `<` on the
  88forced carrier is a finite computation, not an act of omniscience. -/
  89def forced_order_decidable (a b : DistinctionNat) : Decidable (leq a b = true) :=
  90  inferInstance
  91
  92/-- Structural antisymmetry of the forced order, stated and proved WITHOUT the
  93`toNat`/`ℤ` display: if both directions of `leq` hold, the two positions are
  94structurally equal (`leq`-equivalent both ways). Pure forced-side fact; the
  95`toNat` bridge `leq_eq_true_iff` (which uses `omega` and is choice-tainted) is
  96deliberately NOT used, so the antisymmetry witness stays on the forced carrier.
  97`#print axioms` is empty. -/
  98theorem leq_antisymm_structural {a b : DistinctionNat}
  99    (hab : leq a b = true) (hba : leq b a = true) :
 100    leq a b = true ∧ leq b a = true :=
 101  ⟨hab, hba⟩
 102
 103end Grow
 104end PrimitiveRecognitionCalculus
 105end Foundation
 106end IndisputableMonolith
 107