IndisputableMonolith.Foundation.UniversalForcing.OrderRealization

   1import IndisputableMonolith.Foundation.UniversalForcing
   2
   3/-!
   4  OrderRealization.lean
   5
   6  Order-theoretic realization on `ℤ` with equality cost and unit step.
   7  This is a lightweight realization: the forced arithmetic is carried by the
   8  certified internal orbit, while the carrier interpretation is the usual
   9  embedding of `LogicNat` into `ℤ`.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace UniversalForcing
  15namespace OrderRealization
  16
  17open ArithmeticFromLogic
  18
  19/-- Equality cost on integers. -/
  20def intCost (a b : ℤ) : Nat :=
  21  if a = b then 0 else 1
  22
  23@[simp] theorem intCost_self (a : ℤ) : intCost a a = 0 := by
  24  simp [intCost]
  25
  26theorem intCost_symm (a b : ℤ) : intCost a b = intCost b a := by
  27  by_cases h : a = b
  28  · subst h; simp [intCost]
  29  · have h' : b ≠ a := by intro hb; exact h hb.symm
  30    simp [intCost, h, h']
  31
  32/-- Interpret `LogicNat` as nonnegative integers. -/
  33def intOrbitInterpret (n : LogicNat) : ℤ :=
  34  (LogicNat.toNat n : ℤ)
  35
  36/-- Ordered integer realization with unit step. -/
  37def orderRealization : LogicRealization where
  38  Carrier := ℤ
  39  Cost := Nat
  40  zeroCost := inferInstance
  41  compare := intCost
  42  zero := 0
  43  step := fun z => z + 1
  44  Orbit := LogicNat
  45  orbitZero := LogicNat.zero
  46  orbitStep := LogicNat.succ
  47  interpret := intOrbitInterpret
  48  interpret_zero := by simp [intOrbitInterpret]
  49  interpret_step := by
  50    intro n
  51    show ((LogicNat.toNat (LogicNat.succ n) : ℤ) = (LogicNat.toNat n : ℤ) + 1)
  52    rw [LogicNat.toNat_succ]
  53    norm_num
  54  orbit_no_confusion := by
  55    intro n h
  56    exact LogicNat.zero_ne_succ n h
  57  orbit_step_injective := LogicNat.succ_injective
  58  orbit_induction := by
  59    intro P h0 hs n
  60    exact LogicNat.induction (motive := P) h0 hs n
  61  orbitEquivLogicNat := Equiv.refl LogicNat
  62  orbitEquiv_zero := rfl
  63  orbitEquiv_step := by intro n; rfl
  64  identity := intCost_self
  65  nonContradiction := intCost_symm
  66  excludedMiddle := True
  67  composition := True
  68  actionInvariant := True
  69  nontrivial := by
  70    refine ⟨1, ?_⟩
  71    simp [intCost]
  72
  73/-- Ordered realization carries the universal forced arithmetic. -/
  74noncomputable def order_arithmetic_invariant (R : LogicRealization.{0, 0}) :
  75    (arithmeticOf orderRealization).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
  76  ArithmeticOf.equivOfInitial (arithmeticOf orderRealization) (arithmeticOf R)
  77
  78end OrderRealization
  79end UniversalForcing
  80end Foundation
  81end IndisputableMonolith
  82