IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Grow.SignedOrbitOrderChoiceFree

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.IntegerRational
   2
   3/-!
   4# Choice-free signed-orbit order foundation
   5
   6The `SignedOrbit` order in `IntegerRational.lean` is characterized only through the
   7verifier integer display (`le_iff_toInt_le`, `nonneg_iff_toInt_nonneg`,
   8`nonnegFlag_eq_true_iff_nonneg`). Those route through `SignedOrbit.toInt : SignedOrbit → ℤ`
   9and Mathlib's `ℤ` order, which carries `Classical.choice`. So every downstream order rung
  10(`ratio_le_refl`, ...) inherits choice taint it does not need.
  11
  12This module re-grounds the order entirely on the δ-orbit `DistinctionNat.toNat` (a finite ℕ
  13position) via the two already-choice-free bridges:
  14  * `balanced_iff_toNat_eq` : balanced length is a ℕ-level equality, no `ℤ`;
  15  * `leq_eq_true_iff` : the structural Boolean flag agrees with the ℕ order.
  16Both `nonneg z` and `nonnegFlag z = true` collapse to the single ℕ fact
  17`z.neg.toNat ≤ z.pos.toNat`, after which reflexivity / transitivity / totality /
  18antisymmetry-to-balanced are pure `omega` over ℕ. No `SignedOrbit.toInt`, no `ℤ`, no choice.
  19
  20Forced-floor receipt: `#print axioms` of every theorem here is a subset of
  21`{propext, Quot.sound}`. This is the choice-free base the `ratio_*` ordered-field tower needs.
  22-/
  23
  24namespace IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
  25
  26open IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus
  27
  28/-- Internal nonnegativity collapses to a pure ℕ inequality on δ-orbit positions,
  29through the choice-free `balanced_iff_toNat_eq` bridge (NOT `nonneg_iff_toInt_nonneg`). -/
  30theorem nonneg_iff_toNat_le (z : SignedOrbit) :
  31    SignedOrbit.nonneg z ↔ z.neg.toNat ≤ z.pos.toNat := by
  32  unfold SignedOrbit.nonneg
  33  constructor
  34  · rintro ⟨k, hk⟩
  35    rw [SignedOrbit.balanced_iff_toNat_eq] at hk
  36    have hp : (SignedOrbit.ofOrbit k).pos = k := rfl
  37    have hn : (SignedOrbit.ofOrbit k).neg = DistinctionNat.zero := rfl
  38    rw [hp, hn, DistinctionNat.toNat_zero] at hk
  39    omega
  40  · intro h
  41    refine ⟨DistinctionNat.ofNat (z.pos.toNat - z.neg.toNat), ?_⟩
  42    rw [SignedOrbit.balanced_iff_toNat_eq]
  43    have hp : (SignedOrbit.ofOrbit (DistinctionNat.ofNat (z.pos.toNat - z.neg.toNat))).pos
  44        = DistinctionNat.ofNat (z.pos.toNat - z.neg.toNat) := rfl
  45    have hn : (SignedOrbit.ofOrbit (DistinctionNat.ofNat (z.pos.toNat - z.neg.toNat))).neg
  46        = DistinctionNat.zero := rfl
  47    rw [hp, hn, DistinctionNat.toNat_zero, DistinctionNat.toNat_ofNat]
  48    omega
  49
  50/-- Choice-free restatement of the structural Boolean order's agreement with the ℕ order.
  51The original `DistinctionNat.leq_eq_true_iff` is choice-TAINTED (its `simp [leq]` proof pulls
  52`Classical.choice` through a classical `Bool`/`Decidable` simp lemma). Here the same fact is
  53reproved by bare structural induction on the δ-orbit positions: every step is a constructor
  54match plus `omega` over ℕ, so the closure stays inside `{propext, Quot.sound}`. -/
  55theorem leq_eq_true_iff_cf (a b : DistinctionNat) :
  56    DistinctionNat.leq a b = true ↔ a.toNat ≤ b.toNat := by
  57  induction a generalizing b with
  58  | zero =>
  59      cases b with
  60      | zero => exact ⟨fun _ => Nat.le_refl _, fun _ => rfl⟩
  61      | succ b => exact ⟨fun _ => Nat.zero_le _, fun _ => rfl⟩
  62  | succ a ih =>
  63      cases b with
  64      | zero =>
  65          constructor
  66          · intro h
  67            exact absurd h Bool.false_ne_true
  68          · intro h
  69            rw [DistinctionNat.toNat_succ, DistinctionNat.toNat_zero] at h
  70            exact absurd h (Nat.not_succ_le_zero _)
  71      | succ b =>
  72          have hstep : DistinctionNat.leq (DistinctionNat.succ a) (DistinctionNat.succ b)
  73              = DistinctionNat.leq a b := rfl
  74          rw [hstep, ih, DistinctionNat.toNat_succ, DistinctionNat.toNat_succ]
  75          exact Nat.succ_le_succ_iff.symm
  76
  77/-- The structural nonnegative flag agrees with internal nonnegativity, proved
  78choice-free via `leq_eq_true_iff_cf` (NOT `nonnegFlag_eq_true_iff_nonneg`, which goes through `ℤ`). -/
  79theorem nonnegFlag_iff_nonneg_cf (z : SignedOrbit) :
  80    z.nonnegFlag = true ↔ SignedOrbit.nonneg z := by
  81  rw [nonneg_iff_toNat_le]
  82  unfold SignedOrbit.nonnegFlag
  83  rw [leq_eq_true_iff_cf]
  84
  85/-- The signed-orbit order, characterized purely at the ℕ-level on δ-orbit positions.
  86This is the choice-free replacement for `le_iff_toInt_le`. -/
  87theorem le_iff_toNat_cf (a b : SignedOrbit) :
  88    SignedOrbit.le a b ↔ b.neg.toNat + a.pos.toNat ≤ b.pos.toNat + a.neg.toNat := by
  89  unfold SignedOrbit.le
  90  rw [nonneg_iff_toNat_le]
  91  have hp : (SignedOrbit.sub b a).pos = b.pos + a.neg := rfl
  92  have hn : (SignedOrbit.sub b a).neg = b.neg + a.pos := rfl
  93  rw [hp, hn, DistinctionNat.toNat_add, DistinctionNat.toNat_add]
  94
  95/-- The order via the structural nonnegative flag of the difference: the choice-free
  96foundation the `ratio_*` rungs need (replaces the tainted `le_iff_nonnegFlag_sub`). -/
  97theorem le_iff_nonnegFlag_sub_cf (a b : SignedOrbit) :
  98    SignedOrbit.le a b ↔ (SignedOrbit.sub b a).nonnegFlag = true := by
  99  unfold SignedOrbit.le
 100  rw [nonnegFlag_iff_nonneg_cf]
 101
 102/-- Reflexivity of the signed-orbit order, choice-free. -/
 103theorem le_refl_cf (a : SignedOrbit) : SignedOrbit.le a a := by
 104  rw [le_iff_toNat_cf]; omega
 105
 106/-- Transitivity, choice-free. -/
 107theorem le_trans_cf (a b c : SignedOrbit)
 108    (hab : SignedOrbit.le a b) (hbc : SignedOrbit.le b c) : SignedOrbit.le a c := by
 109  rw [le_iff_toNat_cf] at hab hbc ⊢; omega
 110
 111/-- Totality, choice-free. -/
 112theorem le_total_cf (a b : SignedOrbit) :
 113    SignedOrbit.le a b ∨ SignedOrbit.le b a := by
 114  rw [le_iff_toNat_cf, le_iff_toNat_cf]; omega
 115
 116/-- Antisymmetry up to balanced-length equivalence, choice-free. -/
 117theorem le_antisymm_balanced_cf (a b : SignedOrbit)
 118    (hab : SignedOrbit.le a b) (hba : SignedOrbit.le b a) : SignedOrbit.balanced a b := by
 119  rw [le_iff_toNat_cf] at hab hba
 120  rw [SignedOrbit.balanced_iff_toNat_eq]
 121  omega
 122
 123end IndisputableMonolith.PRCGrow.SignedOrbitOrderChoiceFree
 124