IndisputableMonolith.Foundation.ArithmeticOf

   1import IndisputableMonolith.Foundation.LogicRealization
   2import IndisputableMonolith.Foundation.ArithmeticFromLogic
   3
   4/-!
   5  ArithmeticOf.lean
   6
   7  Arithmetic extracted from an abstract Law-of-Logic realization.
   8
   9  The key point is initiality: once a realization supplies identity/step
  10  data, the forced arithmetic object is the initial Peano algebra generated
  11  by that data. Initial objects are unique up to unique isomorphism; this is
  12  the mechanism behind Universal Forcing.
  13-/
  14
  15namespace IndisputableMonolith
  16namespace Foundation
  17
  18open ArithmeticFromLogic
  19
  20universe u
  21
  22/-- A Peano algebra: a type with a zero element and a step map. -/
  23structure PeanoObject where
  24  carrier : Type u
  25  zero : carrier
  26  step : carrier → carrier
  27
  28namespace PeanoObject
  29
  30/-- Homomorphisms of Peano algebras. -/
  31structure Hom (A B : PeanoObject) where
  32  toFun : A.carrier → B.carrier
  33  map_zero : toFun A.zero = B.zero
  34  map_step : ∀ x : A.carrier, toFun (A.step x) = B.step (toFun x)
  35
  36namespace Hom
  37
  38instance (A B : PeanoObject) : CoeFun (Hom A B) (fun _ => A.carrier → B.carrier) where
  39  coe f := f.toFun
  40
  41/-- Identity homomorphism. -/
  42def id (A : PeanoObject) : Hom A A where
  43  toFun := fun x => x
  44  map_zero := rfl
  45  map_step := fun _ => rfl
  46
  47/-- Composition of homomorphisms. -/
  48def comp {A B C : PeanoObject} (g : Hom B C) (f : Hom A B) : Hom A C where
  49  toFun := g.toFun ∘ f.toFun
  50  map_zero := by rw [Function.comp_apply, f.map_zero, g.map_zero]
  51  map_step := by
  52    intro x
  53    rw [Function.comp_apply, f.map_step, g.map_step, Function.comp_apply]
  54
  55end Hom
  56
  57/-- Initiality of a Peano algebra. This is data, so it lives in `Type`. -/
  58structure IsInitial (A : PeanoObject) where
  59  lift : ∀ B : PeanoObject, Hom A B
  60  uniq : ∀ (B : PeanoObject) (f g : Hom A B), f.toFun = g.toFun
  61
  62end PeanoObject
  63
  64/-- The arithmetic object forced by a Law-of-Logic realization. -/
  65structure ArithmeticOf (R : LogicRealization) where
  66  peano : PeanoObject
  67  initial : PeanoObject.IsInitial peano
  68
  69namespace ArithmeticOf
  70
  71/-- Peano surface of a forced arithmetic object. -/
  72structure PeanoSurface {R : LogicRealization} (A : ArithmeticOf R) : Prop where
  73  zero_ne_step : ∀ x : A.peano.carrier, A.peano.zero ≠ A.peano.step x
  74  step_injective : Function.Injective A.peano.step
  75  induction :
  76    ∀ P : A.peano.carrier → Prop,
  77      P A.peano.zero →
  78      (∀ n, P n → P (A.peano.step n)) →
  79      ∀ n, P n
  80
  81/-! ## LogicNat as the canonical initial Peano object -/
  82
  83/-- The Peano object carried by `LogicNat`. -/
  84def logicNatPeano : PeanoObject where
  85  carrier := LogicNat
  86  zero := LogicNat.zero
  87  step := LogicNat.succ
  88
  89/-- Fold from `LogicNat` into an arbitrary Peano object. -/
  90def logicNatFold (B : PeanoObject) : LogicNat → B.carrier
  91  | LogicNat.identity => B.zero
  92  | LogicNat.step n => B.step (logicNatFold B n)
  93
  94/-- Lift from `LogicNat` to any Peano object by primitive recursion. -/
  95def logicNatLift (B : PeanoObject) : PeanoObject.Hom logicNatPeano B where
  96  toFun := logicNatFold B
  97  map_zero := rfl
  98  map_step := by
  99    intro x
 100    rfl
 101
 102private theorem logicNatLift_unique_fun (B : PeanoObject)
 103    (f : PeanoObject.Hom logicNatPeano B) :
 104    f.toFun = (logicNatLift B).toFun := by
 105  funext n
 106  induction n with
 107  | identity =>
 108      exact f.map_zero
 109  | step n ih =>
 110      calc
 111        f.toFun (LogicNat.step n) = B.step (f.toFun n) := f.map_step n
 112        _ = B.step ((logicNatLift B).toFun n) := by rw [ih]
 113        _ = (logicNatLift B).toFun (LogicNat.step n) := rfl
 114
 115/-- `LogicNat` is initial among Peano objects. -/
 116def logicNat_initial : PeanoObject.IsInitial logicNatPeano where
 117  lift := logicNatLift
 118  uniq := by
 119    intro B f g
 120    rw [logicNatLift_unique_fun B f, logicNatLift_unique_fun B g]
 121
 122/-- The Peano object extracted from a realization's own orbit. -/
 123def realizationPeano (R : LogicRealization) : PeanoObject where
 124  carrier := R.Orbit
 125  zero := R.orbitZero
 126  step := R.orbitStep
 127
 128/-- Fold from a realization orbit into any Peano object, through the
 129realization's certified equivalence with `LogicNat`. -/
 130def realizationFold (R : LogicRealization) (B : PeanoObject) : R.Orbit → B.carrier :=
 131  fun n => (logicNatLift B).toFun (R.orbitEquivLogicNat n)
 132
 133/-- Homomorphism from the extracted realization orbit into any Peano object. -/
 134def realizationLift (R : LogicRealization) (B : PeanoObject) :
 135    PeanoObject.Hom (realizationPeano R) B where
 136  toFun := realizationFold R B
 137  map_zero := by
 138    unfold realizationFold
 139    change (logicNatLift B).toFun (R.orbitEquivLogicNat R.orbitZero) = B.zero
 140    rw [R.orbitEquiv_zero]
 141    rfl
 142  map_step := by
 143    intro x
 144    unfold realizationFold
 145    change (logicNatLift B).toFun (R.orbitEquivLogicNat (R.orbitStep x)) =
 146      B.step ((logicNatLift B).toFun (R.orbitEquivLogicNat x))
 147    rw [R.orbitEquiv_step]
 148    rfl
 149
 150private theorem realizationLift_unique_fun (R : LogicRealization) (B : PeanoObject)
 151    (f : PeanoObject.Hom (realizationPeano R) B) :
 152    f.toFun = (realizationLift R B).toFun := by
 153  funext n
 154  have hlogic :
 155      (f.toFun ∘ R.orbitEquivLogicNat.symm) =
 156        (logicNatLift B).toFun := by
 157    exact logicNatLift_unique_fun B
 158      { toFun := f.toFun ∘ R.orbitEquivLogicNat.symm
 159        map_zero := by
 160          simp [Function.comp_def]
 161          have hz := f.map_zero
 162          have hsymm0 : R.orbitEquivLogicNat.symm LogicNat.zero = R.orbitZero := by
 163            apply R.orbitEquivLogicNat.injective
 164            simp [R.orbitEquiv_zero]
 165          change f.toFun (R.orbitEquivLogicNat.symm LogicNat.zero) = B.zero
 166          rw [hsymm0]
 167          exact hz
 168        map_step := by
 169          intro k
 170          simp [Function.comp_def]
 171          change f.toFun (R.orbitEquivLogicNat.symm (LogicNat.succ k)) =
 172            B.step (f.toFun (R.orbitEquivLogicNat.symm k))
 173          have hstep_symm :
 174              R.orbitEquivLogicNat.symm (LogicNat.succ k) =
 175                R.orbitStep (R.orbitEquivLogicNat.symm k) := by
 176            apply R.orbitEquivLogicNat.injective
 177            rw [R.orbitEquiv_step]
 178            simp
 179          rw [hstep_symm]
 180          simpa [realizationPeano] using f.map_step (R.orbitEquivLogicNat.symm k) }
 181  have hn : R.orbitEquivLogicNat.symm (R.orbitEquivLogicNat n) = n := by simp
 182  calc
 183    f.toFun n = (f.toFun ∘ R.orbitEquivLogicNat.symm) (R.orbitEquivLogicNat n) := by
 184      simp [Function.comp_def, hn]
 185    _ = (logicNatLift B).toFun (R.orbitEquivLogicNat n) := by rw [hlogic]
 186    _ = (realizationLift R B).toFun n := rfl
 187
 188/-- The extracted realization orbit is initial. -/
 189def realization_initial (R : LogicRealization) :
 190    PeanoObject.IsInitial (realizationPeano R) where
 191  lift := realizationLift R
 192  uniq := by
 193    intro B f g
 194    rw [realizationLift_unique_fun R B f, realizationLift_unique_fun R B g]
 195
 196/-- Arithmetic extracted from the realization's own identity-step orbit. -/
 197def extracted (R : LogicRealization) : ArithmeticOf R where
 198  peano := realizationPeano R
 199  initial := realization_initial R
 200
 201/-- Peano surface for the extracted arithmetic of any realization. -/
 202theorem extracted_peanoSurface (R : LogicRealization) :
 203    PeanoSurface (extracted R) where
 204  zero_ne_step := R.orbit_no_confusion
 205  step_injective := R.orbit_step_injective
 206  induction := R.orbit_induction
 207
 208/-- The natural equivalence between two initial Peano objects. -/
 209noncomputable def equivOfInitial {R S : LogicRealization}
 210    (A : ArithmeticOf R) (B : ArithmeticOf S) : A.peano.carrier ≃ B.peano.carrier where
 211  toFun := (A.initial.lift B.peano).toFun
 212  invFun := (B.initial.lift A.peano).toFun
 213  left_inv := by
 214    intro x
 215    have hcomp :
 216        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano)).toFun =
 217          (PeanoObject.Hom.id A.peano).toFun :=
 218      A.initial.uniq A.peano
 219        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano))
 220        (PeanoObject.Hom.id A.peano)
 221    exact congrFun hcomp x
 222  right_inv := by
 223    intro y
 224    have hcomp :
 225        (PeanoObject.Hom.comp (A.initial.lift B.peano) (B.initial.lift A.peano)).toFun =
 226          (PeanoObject.Hom.id B.peano).toFun :=
 227      B.initial.uniq B.peano
 228        (PeanoObject.Hom.comp (A.initial.lift B.peano) (B.initial.lift A.peano))
 229        (PeanoObject.Hom.id B.peano)
 230    exact congrFun hcomp y
 231
 232/-- Canonical arithmetic object for any realization: the initial Peano object.
 233
 234This definition is intentionally realization-independent at this stage. The
 235realization supplies the interpretation; initiality supplies the invariant
 236arithmetic content. -/
 237def canonical (R : LogicRealization) : ArithmeticOf R where
 238  peano := logicNatPeano
 239  initial := logicNat_initial
 240
 241/-- The Peano surface for the canonical arithmetic object. -/
 242theorem canonical_peanoSurface (R : LogicRealization) :
 243    PeanoSurface (canonical R) where
 244  zero_ne_step := by
 245    intro x h
 246    cases h
 247  step_injective := by
 248    intro a b h
 249    exact LogicNat.succ_injective h
 250  induction := by
 251    intro P h0 hstep n
 252    exact LogicNat.induction (motive := P) h0 hstep n
 253
 254end ArithmeticOf
 255
 256end Foundation
 257end IndisputableMonolith
 258