IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject

   1import IndisputableMonolith.Foundation.UniversalForcing
   2import IndisputableMonolith.Foundation.UniversalForcing.Strict.DiscreteBoolean
   3
   4/-!
   5  NaturalNumberObject.lean
   6
   7  Lawvere natural-number object characterization of the forced arithmetic.
   8
   9  This module makes precise the categorical sense in which the Law of Logic
  10  forces the natural numbers. The Lawvere characterization is:
  11  a triple `(N, z, s)` is a *natural-number object* if for every triple
  12  `(X, x, f)` with `x : X` and `f : X → X` there exists a unique map
  13  `h : N → X` satisfying `h z = x` and `h ∘ s = f ∘ h`.
  14
  15  This is the statement "ℕ is the initial pointed endomap algebra" and it is
  16  what "ℕ" means in any categorical foundation that does not presuppose ℕ.
  17
  18  We prove:
  19
  20  * `LogicNat` with `identity`/`step` is a natural-number object.
  21  * Every realization's forced arithmetic is a natural-number object.
  22  * Any two natural-number objects are canonically isomorphic.
  23  * The strict Boolean realization carrier collapses to the parity image
  24    `Nat.bodd ∘ toNat`, but the iteration object is unchanged.
  25
  26  The last point is the formal answer to the critic's worry: "you did not
  27  derive ℕ; you smuggled in iteration-counting." The iteration object is
  28  the natural-number object in the Lawvere sense, and it is the same in
  29  every realization, including the discrete Boolean one whose carrier
  30  contains only two elements.
  31-/
  32
  33namespace IndisputableMonolith
  34namespace Foundation
  35namespace UniversalForcing
  36
  37open ArithmeticFromLogic
  38
  39universe u
  40
  41/-! ## Lawvere natural-number object property -/
  42
  43/-- A triple `(N, z, s)` is a Lawvere natural-number object: for every
  44target pointed endomap `(X, x, f)`, primitive recursion exists and is unique.
  45
  46This characterization makes no reference to `Nat`. It is the universal
  47property that any Peano structure must satisfy. The field name `recursor`
  48avoids the reserved `rec` symbol used for auto-generated structure recursors. -/
  49structure IsNaturalNumberObject {N : Type u} (z : N) (s : N → N) where
  50  recursor : ∀ {X : Type u}, X → (X → X) → N → X
  51  recursor_zero : ∀ {X : Type u} (x : X) (f : X → X), recursor x f z = x
  52  recursor_step : ∀ {X : Type u} (x : X) (f : X → X) (n : N),
  53    recursor x f (s n) = f (recursor x f n)
  54  recursor_unique : ∀ {X : Type u} (x : X) (f : X → X) (h : N → X),
  55    h z = x → (∀ n, h (s n) = f (h n)) → ∀ n, h n = recursor x f n
  56
  57namespace IsNaturalNumberObject
  58
  59variable {N : Type u} {z : N} {s : N → N}
  60
  61/-- The Peano object carried by a natural-number object. -/
  62def toPeano (_h : IsNaturalNumberObject z s) : PeanoObject where
  63  carrier := N
  64  zero := z
  65  step := s
  66
  67/-- Initiality of an NNO in the category of pointed endomap algebras. -/
  68def isInitial (h : IsNaturalNumberObject z s) :
  69    PeanoObject.IsInitial (toPeano h) where
  70  lift := fun B =>
  71    { toFun := h.recursor B.zero B.step
  72      map_zero := h.recursor_zero B.zero B.step
  73      map_step := fun n => h.recursor_step B.zero B.step n }
  74  uniq := by
  75    intro B f g
  76    funext n
  77    have hf := h.recursor_unique B.zero B.step f.toFun f.map_zero f.map_step n
  78    have hg := h.recursor_unique B.zero B.step g.toFun g.map_zero g.map_step n
  79    rw [hf, hg]
  80
  81end IsNaturalNumberObject
  82
  83/-! ## `LogicNat` is a natural-number object -/
  84
  85/-- `LogicNat` with `identity` and `step` is a Lawvere natural-number object. -/
  86def logicNat_isNNO :
  87    IsNaturalNumberObject (N := LogicNat) LogicNat.identity LogicNat.step where
  88  recursor := fun {X} x f => ArithmeticOf.logicNatFold ⟨X, x, f⟩
  89  recursor_zero := fun _ _ => rfl
  90  recursor_step := fun _ _ _ => rfl
  91  recursor_unique := by
  92    intro X x f h hz hs n
  93    induction n with
  94    | identity => exact hz
  95    | step n ih =>
  96        calc
  97          h (LogicNat.step n) = f (h n) := hs n
  98          _ = f (ArithmeticOf.logicNatFold ⟨X, x, f⟩ n) := by rw [ih]
  99          _ = ArithmeticOf.logicNatFold ⟨X, x, f⟩ (LogicNat.step n) := rfl
 100
 101/-! ## Forced arithmetic of every realization is a natural-number object -/
 102
 103/-- The natural-number object structure on a realization's iteration orbit.
 104Provided by transport from `LogicNat` through the realization's certified
 105orbit equivalence. The universe of the NNO is the carrier universe of the
 106realization. -/
 107noncomputable def realizationOrbit_isNNO.{u₁, v₁} (R : LogicRealization.{u₁, v₁}) :
 108    IsNaturalNumberObject (N := R.Orbit) R.orbitZero R.orbitStep where
 109  recursor := fun {X} x f n =>
 110    @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (R.orbitEquivLogicNat n)
 111  recursor_zero := fun {X} x f => by
 112    show @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (R.orbitEquivLogicNat R.orbitZero) = x
 113    rw [R.orbitEquiv_zero]
 114    rfl
 115  recursor_step := fun {X} x f n => by
 116    show @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (R.orbitEquivLogicNat (R.orbitStep n)) =
 117      f (@ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (R.orbitEquivLogicNat n))
 118    rw [R.orbitEquiv_step]
 119    rfl
 120  recursor_unique := by
 121    intro X x f h hz hs n
 122    have hlogic_zero :
 123        (h ∘ R.orbitEquivLogicNat.symm) LogicNat.zero = x := by
 124      simp only [Function.comp_apply]
 125      have hsymm0 : R.orbitEquivLogicNat.symm LogicNat.zero = R.orbitZero := by
 126        apply R.orbitEquivLogicNat.injective
 127        simp [R.orbitEquiv_zero]
 128      rw [hsymm0]
 129      exact hz
 130    have hlogic_step : ∀ k,
 131        (h ∘ R.orbitEquivLogicNat.symm) (LogicNat.step k) =
 132          f ((h ∘ R.orbitEquivLogicNat.symm) k) := by
 133      intro k
 134      simp only [Function.comp_apply]
 135      have hsymm_step :
 136          R.orbitEquivLogicNat.symm (LogicNat.step k) =
 137            R.orbitStep (R.orbitEquivLogicNat.symm k) := by
 138        apply R.orbitEquivLogicNat.injective
 139        rw [R.orbitEquiv_step]
 140        simp
 141      rw [hsymm_step]
 142      exact hs (R.orbitEquivLogicNat.symm k)
 143    have huniq :
 144        ∀ k, (h ∘ R.orbitEquivLogicNat.symm) k =
 145          @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ k := by
 146      intro k
 147      induction k with
 148      | identity => exact hlogic_zero
 149      | step k ih =>
 150          calc
 151            (h ∘ R.orbitEquivLogicNat.symm) (LogicNat.step k)
 152                = f ((h ∘ R.orbitEquivLogicNat.symm) k) := hlogic_step k
 153            _ = f (@ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ k) := by rw [ih]
 154            _ = @ArithmeticOf.logicNatFold.{u₁} ⟨X, x, f⟩ (LogicNat.step k) := rfl
 155    have hh : h n = (h ∘ R.orbitEquivLogicNat.symm) (R.orbitEquivLogicNat n) := by
 156      simp [Function.comp_apply]
 157    rw [hh, huniq]
 158
 159/-- Convenience alias: the forced arithmetic of every realization is a Lawvere
 160natural-number object. The forced arithmetic is by definition the realization
 161orbit, so this is the same statement as `realizationOrbit_isNNO`. -/
 162noncomputable def forcedArithmetic_isNNO.{u₁, v₁} (R : LogicRealization.{u₁, v₁}) :
 163    IsNaturalNumberObject
 164      (N := (arithmeticOf R).peano.carrier)
 165      (arithmeticOf R).peano.zero
 166      (arithmeticOf R).peano.step :=
 167  realizationOrbit_isNNO R
 168
 169/-! ## Uniqueness up to canonical isomorphism -/
 170
 171/-- Any two natural-number objects are canonically equivalent. This is the
 172Lawvere statement that the natural-number object is unique up to unique
 173isomorphism. -/
 174def IsNaturalNumberObject.equiv
 175    {N₁ N₂ : Type u} {z₁ : N₁} {s₁ : N₁ → N₁} {z₂ : N₂} {s₂ : N₂ → N₂}
 176    (h₁ : IsNaturalNumberObject z₁ s₁) (h₂ : IsNaturalNumberObject z₂ s₂) :
 177    N₁ ≃ N₂ where
 178  toFun := h₁.recursor z₂ s₂
 179  invFun := h₂.recursor z₁ s₁
 180  left_inv := by
 181    intro n
 182    have hcomp_zero : (h₂.recursor z₁ s₁) ((h₁.recursor z₂ s₂) z₁) = z₁ := by
 183      rw [h₁.recursor_zero, h₂.recursor_zero]
 184    have hcomp_step : ∀ k,
 185        (h₂.recursor z₁ s₁) ((h₁.recursor z₂ s₂) (s₁ k)) =
 186          s₁ ((h₂.recursor z₁ s₁) ((h₁.recursor z₂ s₂) k)) := by
 187      intro k
 188      rw [h₁.recursor_step, h₂.recursor_step]
 189    have hid_zero : (id : N₁ → N₁) z₁ = z₁ := rfl
 190    have hid_step : ∀ k, (id : N₁ → N₁) (s₁ k) = s₁ ((id : N₁ → N₁) k) := by
 191      intro k; rfl
 192    have huniq_id := h₁.recursor_unique z₁ s₁ id hid_zero hid_step n
 193    have huniq_comp := h₁.recursor_unique z₁ s₁
 194      (fun k => (h₂.recursor z₁ s₁) ((h₁.recursor z₂ s₂) k))
 195      hcomp_zero hcomp_step n
 196    rw [huniq_comp]
 197    exact huniq_id.symm
 198  right_inv := by
 199    intro n
 200    have hcomp_zero : (h₁.recursor z₂ s₂) ((h₂.recursor z₁ s₁) z₂) = z₂ := by
 201      rw [h₂.recursor_zero, h₁.recursor_zero]
 202    have hcomp_step : ∀ k,
 203        (h₁.recursor z₂ s₂) ((h₂.recursor z₁ s₁) (s₂ k)) =
 204          s₂ ((h₁.recursor z₂ s₂) ((h₂.recursor z₁ s₁) k)) := by
 205      intro k
 206      rw [h₂.recursor_step, h₁.recursor_step]
 207    have hid_zero : (id : N₂ → N₂) z₂ = z₂ := rfl
 208    have hid_step : ∀ k, (id : N₂ → N₂) (s₂ k) = s₂ ((id : N₂ → N₂) k) := by
 209      intro k; rfl
 210    have huniq_id := h₂.recursor_unique z₂ s₂ id hid_zero hid_step n
 211    have huniq_comp := h₂.recursor_unique z₂ s₂
 212      (fun k => (h₁.recursor z₂ s₂) ((h₂.recursor z₁ s₁) k))
 213      hcomp_zero hcomp_step n
 214    rw [huniq_comp]
 215    exact huniq_id.symm
 216
 217/-- The forced arithmetic of every realization is canonically equivalent to
 218`LogicNat`. This is the Universal Forcing statement at the natural-number
 219object level: every Law-of-Logic realization carries the same NNO. -/
 220noncomputable def realizationOrbit_equiv_logicNat (R : LogicRealization.{0, 0}) :
 221    R.Orbit ≃ LogicNat :=
 222  IsNaturalNumberObject.equiv (realizationOrbit_isNNO R) logicNat_isNNO
 223
 224/-- The Lawvere universality statement: any two realizations have iteration
 225orbits that satisfy the natural-number-object property, hence are
 226canonically equivalent. -/
 227noncomputable def universal_forcing_via_NNO
 228    (R S : LogicRealization.{0, 0}) : R.Orbit ≃ S.Orbit :=
 229  IsNaturalNumberObject.equiv (realizationOrbit_isNNO R) (realizationOrbit_isNNO S)
 230
 231/-! ## The Boolean parity-collapse theorem
 232
 233The discrete Boolean realization is the sharpest test of the iteration-object
 234versus orbit-as-set distinction. The carrier `Bool` has only two elements,
 235and the strict realization's `interpret : LogicNat → Bool` collapses
 236infinitely many iteration steps onto two values. The iteration object
 237itself never collapses; it is `LogicNat`, the natural-number object.
 238
 239The theorem below makes the collapse explicit: the Boolean interpretation
 240is exactly the parity map `Nat.bodd ∘ toNat`. -/
 241
 242namespace Strict.DiscreteBoolean
 243
 244open IndisputableMonolith.Foundation.UniversalForcing.Strict
 245
 246/-- One step of the Boolean strict realization is `xor true _`, which is
 247boolean negation. -/
 248private theorem xorBool_true (b : Bool) : xorBool true b = !b := by
 249  cases b <;> rfl
 250
 251/-- The Boolean strict-realization interpretation is the parity map.
 252
 253This is the formal statement that the iteration count survives even when
 254the orbit-as-set collapses to `{false, true}`. -/
 255theorem interpret_eq_parity (n : LogicNat) :
 256    StrictLogicRealization.interpret strictBooleanRealization n =
 257      Nat.bodd (LogicNat.toNat n) := by
 258  induction n with
 259  | identity => rfl
 260  | step n ih =>
 261      show xorBool true (StrictLogicRealization.interpret strictBooleanRealization n) =
 262        Nat.bodd (Nat.succ (LogicNat.toNat n))
 263      rw [xorBool_true, ih, Nat.bodd_succ]
 264
 265/-- Even though the carrier image collapses, the iteration object is the
 266full `LogicNat`. Concretely: the interpretation map is not injective. -/
 267theorem interpret_collapses :
 268    ¬ Function.Injective
 269      (StrictLogicRealization.interpret strictBooleanRealization) := by
 270  intro hinj
 271  have h0 :
 272      StrictLogicRealization.interpret strictBooleanRealization LogicNat.identity =
 273        Nat.bodd 0 := interpret_eq_parity _
 274  have h2 :
 275      StrictLogicRealization.interpret strictBooleanRealization
 276        (LogicNat.step (LogicNat.step LogicNat.identity)) =
 277          Nat.bodd 2 := interpret_eq_parity _
 278  have hbodd : (Nat.bodd 0 : Bool) = Nat.bodd 2 := by decide
 279  have hboth :
 280      StrictLogicRealization.interpret strictBooleanRealization LogicNat.identity =
 281        StrictLogicRealization.interpret strictBooleanRealization
 282          (LogicNat.step (LogicNat.step LogicNat.identity)) := by
 283    rw [h0, h2, hbodd]
 284  have hne : LogicNat.identity ≠ LogicNat.step (LogicNat.step LogicNat.identity) :=
 285    LogicNat.zero_ne_succ _
 286  exact hne (hinj hboth)
 287
 288/-- Despite the carrier collapse, the iteration object is itself a
 289natural-number object — the same one as in the continuous positive-ratio
 290realization. -/
 291def boolean_freeOrbit_isNNO :
 292    IsNaturalNumberObject
 293      (N := StrictLogicRealization.FreeOrbit strictBooleanRealization)
 294      LogicNat.identity LogicNat.step :=
 295  logicNat_isNNO
 296
 297end Strict.DiscreteBoolean
 298
 299end UniversalForcing
 300end Foundation
 301end IndisputableMonolith
 302