IndisputableMonolith.Foundation.UniversalForcing.CanonicalForcing

   1/-
   2  UniversalForcing/CanonicalForcing.lean
   3
   4  Closing the representation-claim weakness.
   5
   6  The Universal Forcing thesis must not be demoted to "there exists *some*
   7  isomorphism between the two forced ℕ-towers." Any two countable Peano objects
   8  are abstractly isomorphic, so bare existence carries no content. The actual
   9  content is **canonicity**: the forcing map is the *unique* structure-preserving
  10  function, fully determined by initiality. There is no choice, no representation
  11  ambiguity — the zero/step data pins exactly one map.
  12
  13  This module proves it for strict realizations (the main Universal-Forcing
  14  theorem path), where every forced arithmetic carrier is concretely `LogicNat`:
  15
  16  * `universal_forcing_map_zero` / `universal_forcing_map_step`: the forcing
  17    equivalence is itself a Peano homomorphism (preserves zero and step).
  18  * `universal_forcing_unique`: *any* function preserving zero and step equals
  19    the forcing map. This is the canonicity statement — the map is forced, not
  20    chosen.
  21  * `universal_forcing_iff`: a complete characterization (preservation ↔ being
  22    the forcing map).
  23  * `universal_forcing_equiv_unique`: two equivalences that both preserve zero
  24    and step are equal as functions. Uniqueness up to *nothing*, not merely up to
  25    iso.
  26  * `CanonicalForcingCert` / `canonicalForcingCert_holds`: the certificate.
  27
  28  With this, the program's headline ("two realizations force the same arithmetic")
  29  is a statement about a canonical, determined morphism, not a representation
  30  artifact.
  31
  32  The general (non-strict, cross-universe) case is `ArithmeticOf.universal_objective`:
  33  for any two Law-of-Logic realizations and any forced arithmetics over them
  34  (sharing a carrier universe), the structure-preserving equivalence exists and
  35  is the unique zero/step-preserving map. That theorem is the precise statement
  36  of `universal-forcing-program.mdc`'s "canonical equivalence of `ArithmeticOf R`
  37  and `ArithmeticOf S` across admissible realizations".
  38-/
  39
  40import IndisputableMonolith.Foundation.ArithmeticOf
  41import IndisputableMonolith.Foundation.UniversalForcing.StrictRealization
  42
  43namespace IndisputableMonolith
  44namespace Foundation
  45
  46/-! ## General canonicity (any two realizations, shared carrier universe)
  47
  48The strict, universe-0 statements below are the main-path case. These general
  49lemmas cover *any* two Law-of-Logic realizations whose forced arithmetics share a
  50carrier universe `w` — which is always arrangeable, since the carrier universe is
  51a free parameter of `ArithmeticOf`. The same-universe condition is not a
  52restriction on the mathematics; it is the only setting in which "the unique
  53structure morphism" is even a well-formed comparison (`IsInitial.uniq` quantifies
  54over Peano objects in one universe). `equivOfInitial` itself is cross-universe in
  55its slots, so the pinning `ArithmeticOf.{u,v,w,w,w}` is what makes the uniqueness
  56argument type-check. -/
  57
  58namespace ArithmeticOf
  59
  60open ArithmeticFromLogic
  61
  62universe u v u' v' w
  63
  64variable {R : LogicRealization.{u, v}} {S : LogicRealization.{u', v'}}
  65
  66/-- The forcing equivalence preserves zero (general realizations). -/
  67@[simp] theorem equivOfInitial_map_zero
  68    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S) :
  69    (equivOfInitial A B) A.peano.zero = B.peano.zero :=
  70  (A.initial.lift B.peano).map_zero
  71
  72/-- The forcing equivalence intertwines step (general realizations). -/
  73@[simp] theorem equivOfInitial_map_step
  74    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S)
  75    (x : A.peano.carrier) :
  76    (equivOfInitial A B) (A.peano.step x) = B.peano.step ((equivOfInitial A B) x) :=
  77  (A.initial.lift B.peano).map_step x
  78
  79/-- **General canonicity.** Any function preserving zero and step between two
  80forced arithmetics (sharing a carrier universe) *is* the forcing map. The map is
  81determined by the zero/step data alone — no representational freedom. -/
  82theorem forcing_map_unique
  83    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S)
  84    (f : A.peano.carrier → B.peano.carrier)
  85    (hz : f A.peano.zero = B.peano.zero)
  86    (hs : ∀ x, f (A.peano.step x) = B.peano.step (f x)) :
  87    f = (equivOfInitial A B).toFun := by
  88  have h := A.initial.uniq B.peano
  89      (⟨f, hz, hs⟩ : PeanoObject.Hom A.peano B.peano) (A.initial.lift B.peano)
  90  simpa [equivOfInitial] using h
  91
  92/-- Complete characterization (general realizations). -/
  93theorem forcing_map_iff
  94    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S)
  95    (f : A.peano.carrier → B.peano.carrier) :
  96    (f A.peano.zero = B.peano.zero ∧ ∀ x, f (A.peano.step x) = B.peano.step (f x))
  97      ↔ f = (equivOfInitial A B).toFun := by
  98  constructor
  99  · rintro ⟨hz, hs⟩
 100    exact forcing_map_unique A B f hz hs
 101  · rintro rfl
 102    exact ⟨equivOfInitial_map_zero A B, equivOfInitial_map_step A B⟩
 103
 104/-- **Uniqueness up to nothing** (general realizations): two equivalences that
 105both preserve zero and step are equal as functions. -/
 106theorem forcing_equiv_unique
 107    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S)
 108    (e₁ e₂ : A.peano.carrier ≃ B.peano.carrier)
 109    (hz₁ : e₁ A.peano.zero = B.peano.zero)
 110    (hs₁ : ∀ x, e₁ (A.peano.step x) = B.peano.step (e₁ x))
 111    (hz₂ : e₂ A.peano.zero = B.peano.zero)
 112    (hs₂ : ∀ x, e₂ (A.peano.step x) = B.peano.step (e₂ x)) :
 113    (e₁ : A.peano.carrier → B.peano.carrier) = e₂ := by
 114  have h1 := forcing_map_unique A B (e₁ : A.peano.carrier → B.peano.carrier) hz₁ hs₁
 115  have h2 := forcing_map_unique A B (e₂ : A.peano.carrier → B.peano.carrier) hz₂ hs₂
 116  rw [h1, h2]
 117
 118/-- **The Universal-Forcing objective at full generality.** For *any* two
 119Law-of-Logic realizations `R`, `S` (in arbitrary universes) and any forced
 120arithmetics `A` over `R`, `B` over `S` sharing a carrier universe, there is a
 121structure-preserving equivalence between the carriers that is *the unique*
 122zero/step-preserving map. This is the precise content of
 123`universal-forcing-program.mdc`'s "canonical equivalence of `ArithmeticOf R` and
 124`ArithmeticOf S` across admissible realizations": not bare existence of some
 125iso, but a canonical, determined morphism.
 126
 127Unlike the strict-realization certificate below (where the carrier is concretely
 128`LogicNat` and the map is the identity), here `A.peano.carrier` and
 129`B.peano.carrier` may be genuinely different Peano objects, so the equivalence is
 130a nontrivial iso — yet still the only structure morphism between them. -/
 131theorem universal_objective
 132    (A : ArithmeticOf.{u, v, w, w, w} R) (B : ArithmeticOf.{u', v', w, w, w} S) :
 133    ∃ e : A.peano.carrier ≃ B.peano.carrier,
 134      e A.peano.zero = B.peano.zero
 135      ∧ (∀ x, e (A.peano.step x) = B.peano.step (e x))
 136      ∧ (∀ f : A.peano.carrier → B.peano.carrier,
 137            f A.peano.zero = B.peano.zero →
 138            (∀ x, f (A.peano.step x) = B.peano.step (f x)) →
 139            f = e.toFun) :=
 140  ⟨equivOfInitial A B,
 141   equivOfInitial_map_zero A B,
 142   equivOfInitial_map_step A B,
 143   fun f hz hs => forcing_map_unique A B f hz hs⟩
 144
 145end ArithmeticOf
 146
 147namespace UniversalForcing
 148namespace Strict
 149namespace StrictLogicRealization
 150
 151open ArithmeticFromLogic
 152
 153/-- The strict universal-forcing equivalence preserves zero: it sends `R`'s
 154forced zero to `S`'s forced zero. -/
 155@[simp] theorem universal_forcing_map_zero (R S : StrictLogicRealization.{0,0}) :
 156    (universal_forcing.{0,0,0,0,0,0} R S) (arith.{0,0,0} R).peano.zero
 157      = (arith.{0,0,0} S).peano.zero :=
 158  ((arith.{0,0,0} R).initial.lift (arith.{0,0,0} S).peano).map_zero
 159
 160/-- The strict universal-forcing equivalence intertwines `R`'s step with `S`'s
 161step. -/
 162@[simp] theorem universal_forcing_map_step (R S : StrictLogicRealization.{0,0})
 163    (x : (arith.{0,0,0} R).peano.carrier) :
 164    (universal_forcing.{0,0,0,0,0,0} R S) ((arith.{0,0,0} R).peano.step x)
 165      = (arith.{0,0,0} S).peano.step ((universal_forcing.{0,0,0,0,0,0} R S) x) :=
 166  ((arith.{0,0,0} R).initial.lift (arith.{0,0,0} S).peano).map_step x
 167
 168/-- **Canonicity.** Any function that preserves zero and step *is* the strict
 169universal-forcing map. The structure-preserving map between two forced
 170arithmetics is unique, so the equivalence is determined by the zero/step data
 171alone — there is no representational freedom. -/
 172theorem universal_forcing_unique (R S : StrictLogicRealization.{0,0})
 173    (f : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier)
 174    (hz : f (arith.{0,0,0} R).peano.zero = (arith.{0,0,0} S).peano.zero)
 175    (hs : ∀ x, f ((arith.{0,0,0} R).peano.step x) = (arith.{0,0,0} S).peano.step (f x)) :
 176    f = (universal_forcing.{0,0,0,0,0,0} R S).toFun := by
 177  have h := (arith.{0,0,0} R).initial.uniq (arith.{0,0,0} S).peano
 178      (⟨f, hz, hs⟩ : PeanoObject.Hom (arith.{0,0,0} R).peano (arith.{0,0,0} S).peano)
 179      ((arith.{0,0,0} R).initial.lift (arith.{0,0,0} S).peano)
 180  simpa [universal_forcing, ArithmeticOf.equivOfInitial] using h
 181
 182/-- Complete characterization: a map is the forcing map iff it preserves zero and
 183step. -/
 184theorem universal_forcing_iff (R S : StrictLogicRealization.{0,0})
 185    (f : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier) :
 186    (f (arith.{0,0,0} R).peano.zero = (arith.{0,0,0} S).peano.zero
 187        ∧ ∀ x, f ((arith.{0,0,0} R).peano.step x) = (arith.{0,0,0} S).peano.step (f x))
 188      ↔ f = (universal_forcing.{0,0,0,0,0,0} R S).toFun := by
 189  constructor
 190  · rintro ⟨hz, hs⟩
 191    exact universal_forcing_unique R S f hz hs
 192  · rintro rfl
 193    exact ⟨universal_forcing_map_zero R S, universal_forcing_map_step R S⟩
 194
 195/-- **Uniqueness up to nothing.** Two equivalences that both preserve zero and
 196step are equal as functions. The forcing isomorphism is not "an" iso among many;
 197it is the only structure morphism, hence canonical. -/
 198theorem universal_forcing_equiv_unique (R S : StrictLogicRealization.{0,0})
 199    (e₁ e₂ : (arith.{0,0,0} R).peano.carrier ≃ (arith.{0,0,0} S).peano.carrier)
 200    (hz₁ : e₁ (arith.{0,0,0} R).peano.zero = (arith.{0,0,0} S).peano.zero)
 201    (hs₁ : ∀ x, e₁ ((arith.{0,0,0} R).peano.step x) = (arith.{0,0,0} S).peano.step (e₁ x))
 202    (hz₂ : e₂ (arith.{0,0,0} R).peano.zero = (arith.{0,0,0} S).peano.zero)
 203    (hs₂ : ∀ x, e₂ ((arith.{0,0,0} R).peano.step x) = (arith.{0,0,0} S).peano.step (e₂ x)) :
 204    (e₁ : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier) = e₂ := by
 205  have h1 := universal_forcing_unique R S
 206      (e₁ : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier) hz₁ hs₁
 207  have h2 := universal_forcing_unique R S
 208      (e₂ : (arith.{0,0,0} R).peano.carrier → (arith.{0,0,0} S).peano.carrier) hz₂ hs₂
 209  rw [h1, h2]
 210
 211end StrictLogicRealization
 212end Strict
 213
 214/-- **Certificate: forcing is canonical, not representational.** The forced
 215arithmetic equivalence between any two strict realizations exists, preserves the
 216full Peano structure, and is the unique such map. -/
 217structure CanonicalForcingCert where
 218  /-- The forcing map exists for every pair of strict realizations. -/
 219  exists_map : ∀ (R S : Strict.StrictLogicRealization.{0,0}),
 220      (Strict.StrictLogicRealization.arith.{0,0,0} R).peano.carrier ≃
 221        (Strict.StrictLogicRealization.arith.{0,0,0} S).peano.carrier
 222  /-- It preserves zero. -/
 223  preserves_zero : ∀ (R S : Strict.StrictLogicRealization.{0,0}),
 224      (exists_map R S) (Strict.StrictLogicRealization.arith.{0,0,0} R).peano.zero
 225        = (Strict.StrictLogicRealization.arith.{0,0,0} S).peano.zero
 226  /-- It preserves step. -/
 227  preserves_step : ∀ (R S : Strict.StrictLogicRealization.{0,0})
 228      (x : (Strict.StrictLogicRealization.arith.{0,0,0} R).peano.carrier),
 229      (exists_map R S) ((Strict.StrictLogicRealization.arith.{0,0,0} R).peano.step x)
 230        = (Strict.StrictLogicRealization.arith.{0,0,0} S).peano.step ((exists_map R S) x)
 231  /-- It is the unique zero/step-preserving function. -/
 232  unique : ∀ (R S : Strict.StrictLogicRealization.{0,0})
 233      (f : (Strict.StrictLogicRealization.arith.{0,0,0} R).peano.carrier →
 234            (Strict.StrictLogicRealization.arith.{0,0,0} S).peano.carrier),
 235      f (Strict.StrictLogicRealization.arith.{0,0,0} R).peano.zero
 236          = (Strict.StrictLogicRealization.arith.{0,0,0} S).peano.zero →
 237      (∀ x, f ((Strict.StrictLogicRealization.arith.{0,0,0} R).peano.step x)
 238            = (Strict.StrictLogicRealization.arith.{0,0,0} S).peano.step (f x)) →
 239      f = (exists_map R S).toFun
 240
 241/-- The canonicity certificate holds. -/
 242noncomputable def canonicalForcingCert_holds : CanonicalForcingCert where
 243  exists_map := fun R S => Strict.StrictLogicRealization.universal_forcing.{0,0,0,0,0,0} R S
 244  preserves_zero := fun R S => Strict.StrictLogicRealization.universal_forcing_map_zero R S
 245  preserves_step := fun R S x => Strict.StrictLogicRealization.universal_forcing_map_step R S x
 246  unique := fun R S f hz hs => Strict.StrictLogicRealization.universal_forcing_unique R S f hz hs
 247
 248end UniversalForcing
 249end Foundation
 250end IndisputableMonolith
 251