IndisputableMonolith.Foundation.UniversalForcing.CanonicalIso

   1import IndisputableMonolith.Foundation.UniversalForcing
   2
   3/-!
   4  CanonicalIso.lean
   5
   6  Universal Forcing, Part II (arithmetic-extraction layer).
   7
   8  The existing Universal Forcing spine (`UniversalForcing.universal_forcing`,
   9  `ArithmeticOf.equivOfInitial`) produces a *bare carrier bijection*
  10  `(arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier` between the
  11  forced arithmetics of any two Law-of-Logic realizations.  A bijection between
  12  two number systems is weaker than an isomorphism of number systems: it does
  13  not, on its face, respect zero or successor.
  14
  15  This module closes that gap at the Peano-algebra layer:
  16
  17  1. `equivOfInitial_map_zero` / `equivOfInitial_map_step`: the universal
  18     forcing bijection *does* send zero to zero and commute with the step map,
  19     so it is a homomorphism of Peano algebras, not merely a set bijection.
  20  2. `PeanoEquiv`: a bundled structure-preserving isomorphism of Peano objects.
  21  3. `peanoEquiv_unique`: any two structure-preserving isomorphisms between the
  22     same pair of forced arithmetics have the *same* underlying function.  This
  23     is the "canonical" in "canonically equivalent": the isomorphism is not
  24     merely some isomorphism, it is the unique one.
  25  4. `universalForcingIsoCert`: the package, quantified over all realizations.
  26
  27  Everything is stated at the `{0, 0}` realization universe used throughout the
  28  rest of the Universal Forcing program (positive-ratio, discrete-Boolean,
  29  modular, categorical, etc. realizations are all `LogicRealization.{0, 0}`), so
  30  the Peano carriers all live in `Type 0` and the file is universe-monomorphic.
  31
  32  Honest scope.  This upgrades the invariant from `≃` to *unique Peano-algebra
  33  isomorphism*.  Preservation of the *ring* operations `+`, `×` and the order
  34  `≤` is the next step and is not proved here, because `PeanoObject` in
  35  `ArithmeticOf.lean` carries only `zero` and `step`.  The richer
  36  ordered-semiring iso is the remaining work toward the full Part II crown.
  37-/
  38
  39namespace IndisputableMonolith
  40namespace Foundation
  41namespace UniversalForcing
  42
  43open ArithmeticFromLogic
  44
  45universe u v w
  46
  47/-! ## Universe-pinned forced arithmetic
  48
  49`ArithmeticOf` carries five universe parameters: two for the realization carrier
  50and cost, one for the forced Peano carrier, and two for the `IsInitial` lift and
  51uniqueness target universes.  The bare `arithmeticOf R` leaves the last two free,
  52so each textual occurrence spawns fresh unpinned universe metavariables.  This
  53abbreviation pins every `ArithmeticOf` universe to the single realization
  54universe `u`, which is exactly the situation in the Universal Forcing program
  55(orbits live in `Type u`).  Using it throughout keeps the file
  56universe-monomorphic in spirit while staying polymorphic in `u, v`. -/
  57
  58/-- The forced arithmetic of a realization, with all `ArithmeticOf` universes
  59pinned to the realization's own carrier universe. -/
  60abbrev forcedArith (R : LogicRealization.{u, v}) :
  61    ArithmeticOf.{u, v, u, u, u} R :=
  62  arithmeticOf R
  63
  64/-! ## Bundled structure-preserving isomorphism of Peano objects -/
  65
  66/-- A structure-preserving isomorphism of Peano objects: an equivalence of
  67carriers that respects zero and step. -/
  68structure PeanoEquiv (A B : PeanoObject.{u}) where
  69  toEquiv : A.carrier ≃ B.carrier
  70  map_zero : toEquiv A.zero = B.zero
  71  map_step : ∀ x, toEquiv (A.step x) = B.step (toEquiv x)
  72
  73namespace PeanoEquiv
  74
  75/-- The underlying Peano homomorphism of a structure-preserving isomorphism. -/
  76def toHom {A B : PeanoObject.{u}} (e : PeanoEquiv A B) : PeanoObject.Hom A B where
  77  toFun := e.toEquiv
  78  map_zero := e.map_zero
  79  map_step := e.map_step
  80
  81end PeanoEquiv
  82
  83/-! ## The universal forcing bijection is a Peano homomorphism
  84
  85`R` and `S` share the carrier universe `u` (their cost universes `v, w` are
  86independent), so both forced Peano carriers live in `Type u` and the
  87canonicality argument's `uniq` call typechecks.  All `ArithmeticOf` universes
  88are pinned through `forcedArith`. -/
  89
  90/-- The universal forcing bijection sends the forced zero to the forced zero. -/
  91theorem equivOfInitial_map_zero (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w}) :
  92    (ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S))
  93        (forcedArith R).peano.zero
  94      = (forcedArith S).peano.zero :=
  95  ((forcedArith R).initial.lift (forcedArith S).peano).map_zero
  96
  97/-- The universal forcing bijection commutes with the forced step map. -/
  98theorem equivOfInitial_map_step (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
  99    (x : (forcedArith R).peano.carrier) :
 100    (ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S))
 101        ((forcedArith R).peano.step x)
 102      = (forcedArith S).peano.step
 103          ((ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S)) x) :=
 104  ((forcedArith R).initial.lift (forcedArith S).peano).map_step x
 105
 106/-- The canonical structure-preserving isomorphism between the forced
 107arithmetics of two realizations. This packages the universal forcing bijection
 108together with proofs that it respects zero and step. -/
 109noncomputable def universalForcingPeanoEquiv
 110    (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w}) :
 111    PeanoEquiv (forcedArith R).peano (forcedArith S).peano where
 112  toEquiv := ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S)
 113  map_zero := equivOfInitial_map_zero R S
 114  map_step := equivOfInitial_map_step R S
 115
 116@[simp] theorem universalForcingPeanoEquiv_toEquiv
 117    (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w}) :
 118    (universalForcingPeanoEquiv R S).toEquiv
 119      = ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S) :=
 120  rfl
 121
 122/-! ## Canonicality: the structure-preserving isomorphism is unique -/
 123
 124/-- **Canonicality.**  Any two structure-preserving isomorphisms between the
 125forced arithmetics of two realizations have the same underlying function.  The
 126isomorphism furnished by Universal Forcing is therefore the unique one. -/
 127theorem peanoEquiv_unique (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
 128    (e₁ e₂ : PeanoEquiv (forcedArith R).peano (forcedArith S).peano) :
 129    (e₁.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier)
 130      = (e₂.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier) :=
 131  (forcedArith R).initial.uniq (forcedArith S).peano e₁.toHom e₂.toHom
 132
 133/-- Any Peano homomorphism into the target forced arithmetic equals the
 134universal forcing map: there is exactly one Peano homomorphism, and it is an
 135isomorphism. -/
 136theorem hom_eq_universalForcing (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
 137    (f : PeanoObject.Hom (forcedArith R).peano (forcedArith S).peano) :
 138    f.toFun = (universalForcingPeanoEquiv R S).toEquiv :=
 139  (forcedArith R).initial.uniq (forcedArith S).peano f
 140    ((forcedArith R).initial.lift (forcedArith S).peano)
 141
 142/-! ## Certificate, quantified over all realizations -/
 143
 144/-- **Universal Forcing isomorphism certificate.**
 145
 146For any two Law-of-Logic realizations, there is a canonical structure-preserving
 147isomorphism between their forced arithmetics, and that isomorphism is unique. -/
 148structure UniversalForcingIsoCert where
 149  /-- The canonical Peano-algebra isomorphism between any two forced arithmetics. -/
 150  iso : ∀ R S : LogicRealization.{0, 0},
 151    PeanoEquiv (forcedArith R).peano (forcedArith S).peano
 152  /-- That isomorphism is unique as a structure-preserving map. -/
 153  unique : ∀ (R S : LogicRealization.{0, 0})
 154      (e₁ e₂ : PeanoEquiv (forcedArith R).peano (forcedArith S).peano),
 155      (e₁.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier)
 156        = e₂.toEquiv
 157
 158/-- The certificate is inhabited by the canonical iso and its uniqueness. -/
 159noncomputable def universalForcingIsoCert : UniversalForcingIsoCert where
 160  iso := fun R S => universalForcingPeanoEquiv R S
 161  unique := fun R S => peanoEquiv_unique R S
 162
 163end UniversalForcing
 164end Foundation
 165end IndisputableMonolith
 166