IndisputableMonolith.Foundation.UniversalForcing.CanonicalSemiringIso

   1import IndisputableMonolith.Foundation.UniversalForcing.CanonicalIso
   2
   3/-!
   4  CanonicalSemiringIso.lean
   5
   6  Universal Forcing, Part II — the ordered-semiring layer.
   7
   8  `CanonicalIso.lean` upgraded the universal forcing invariant from a bare
   9  carrier bijection to a *unique structure-preserving isomorphism of Peano
  10  algebras* (respecting zero and successor).  This module takes the next step:
  11  it shows the canonical isomorphism also respects the *arithmetic* the Peano
  12  structure determines — addition, multiplication, the order, and the
  13  constants `0` and `1`.
  14
  15  The construction is faithful to "the operations the initiality fold
  16  determines".  Every forced carrier folds canonically onto the reference
  17  initial object `LogicNat` via `R.orbitEquivLogicNat`, and `LogicNat` already
  18  carries the recovered arithmetic (`ArithmeticFromLogic`: `Add`, `Mul`,
  19  `LinearOrder`, with the Peano laws as theorems).  We transport `0, 1, +, ×, ≤`
  20  along that fold, then prove the universal forcing isomorphism commutes with
  21  all of them.
  22
  23  The single load-bearing lemma is `fold_iso_compat`: the universal forcing
  24  isomorphism composed with `S`'s fold to `LogicNat` equals `R`'s fold.  This is
  25  pure initiality — both are Peano homomorphisms from the (initial) forced
  26  arithmetic of `R` into `LogicNat`, hence identical.  Everything else follows
  27  by `Equiv` algebra.
  28
  29  Scope.  This proves the canonical map is a homomorphism for `+` and `×`, sends
  30  `0 ↦ 0` and `1 ↦ 1`, and is an order isomorphism for `≤`: the full
  31  ordered-commutative-semiring isomorphism content at the element level.  It does
  32  not bundle `LogicNat` (or the carriers) as a Mathlib `OrderedCommSemiring`
  33  typeclass *instance*; that is a separate, purely `LogicNat`-side enrichment and
  34  is not needed for the forcing statement.
  35
  36  Universes.  Realization carriers are pinned to `Type 0` (so the forced Peano
  37  carriers match `LogicNat : Type 0` and the initiality `uniq` into `logicNatPeano`
  38  typechecks), with independent cost universes `v, w`.  This is exactly the
  39  Universal Forcing program's situation.
  40-/
  41
  42namespace IndisputableMonolith
  43namespace Foundation
  44namespace UniversalForcing
  45
  46open ArithmeticFromLogic
  47open ArithmeticOf (logicNatPeano)
  48
  49universe v w
  50
  51/-! ## The canonical fold onto the reference initial object -/
  52
  53/-- The canonical fold of a realization's forced arithmetic onto the reference
  54`LogicNat`, packaged as a Peano homomorphism. -/
  55def foldHom (R : LogicRealization.{0, v}) :
  56    PeanoObject.Hom (forcedArith R).peano logicNatPeano where
  57  toFun := fun x => R.orbitEquivLogicNat x
  58  map_zero := R.orbitEquiv_zero
  59  map_step := R.orbitEquiv_step
  60
  61@[simp] theorem foldHom_toFun (R : LogicRealization.{0, v})
  62    (x : (forcedArith R).peano.carrier) :
  63    (foldHom R).toFun x = R.orbitEquivLogicNat x := rfl
  64
  65/-- **Fold compatibility (pure initiality).**  The universal forcing isomorphism
  66`R ⥲ S`, followed by `S`'s fold onto `LogicNat`, equals `R`'s fold onto
  67`LogicNat`.  Both are Peano homomorphisms out of the initial forced arithmetic of
  68`R`, so initiality forces them equal. -/
  69theorem fold_iso_compat (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w})
  70    (x : (forcedArith R).peano.carrier) :
  71    S.orbitEquivLogicNat ((universalForcingPeanoEquiv R S).toEquiv x)
  72      = R.orbitEquivLogicNat x := by
  73  have h := (forcedArith R).initial.uniq logicNatPeano
  74    (PeanoObject.Hom.comp (foldHom S) (universalForcingPeanoEquiv R S).toHom)
  75    (foldHom R)
  76  exact congrFun h x
  77
  78/-! ## Transported arithmetic on the forced carrier
  79
  80The operations are the `LogicNat` operations carried back along the canonical
  81fold `R.orbitEquivLogicNat`. -/
  82
  83/-- The forced zero of a realization (transported `0 : LogicNat`). -/
  84noncomputable def forcedZero (R : LogicRealization.{0, v}) :
  85    (forcedArith R).peano.carrier :=
  86  R.orbitEquivLogicNat.symm 0
  87
  88/-- The forced one of a realization (transported `1 : LogicNat`). -/
  89noncomputable def forcedOne (R : LogicRealization.{0, v}) :
  90    (forcedArith R).peano.carrier :=
  91  R.orbitEquivLogicNat.symm 1
  92
  93/-- Forced addition (transported `+` on `LogicNat`). -/
  94noncomputable def forcedAdd (R : LogicRealization.{0, v})
  95    (a b : (forcedArith R).peano.carrier) : (forcedArith R).peano.carrier :=
  96  R.orbitEquivLogicNat.symm (R.orbitEquivLogicNat a + R.orbitEquivLogicNat b)
  97
  98/-- Forced multiplication (transported `×` on `LogicNat`). -/
  99noncomputable def forcedMul (R : LogicRealization.{0, v})
 100    (a b : (forcedArith R).peano.carrier) : (forcedArith R).peano.carrier :=
 101  R.orbitEquivLogicNat.symm (R.orbitEquivLogicNat a * R.orbitEquivLogicNat b)
 102
 103/-- Forced order (transported `≤` on `LogicNat`). -/
 104def forcedLe (R : LogicRealization.{0, v})
 105    (a b : (forcedArith R).peano.carrier) : Prop :=
 106  R.orbitEquivLogicNat a ≤ R.orbitEquivLogicNat b
 107
 108/-! ## The universal forcing isomorphism is an ordered-semiring isomorphism -/
 109
 110/-- The canonical isomorphism sends the forced zero to the forced zero. -/
 111theorem iso_map_forcedZero (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w}) :
 112    (universalForcingPeanoEquiv R S).toEquiv (forcedZero R) = forcedZero S := by
 113  apply S.orbitEquivLogicNat.injective
 114  simp only [forcedZero, fold_iso_compat, Equiv.apply_symm_apply]
 115
 116/-- The canonical isomorphism sends the forced one to the forced one. -/
 117theorem iso_map_forcedOne (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w}) :
 118    (universalForcingPeanoEquiv R S).toEquiv (forcedOne R) = forcedOne S := by
 119  apply S.orbitEquivLogicNat.injective
 120  simp only [forcedOne, fold_iso_compat, Equiv.apply_symm_apply]
 121
 122/-- **Additivity.**  The canonical isomorphism is a homomorphism for forced
 123addition. -/
 124theorem iso_map_forcedAdd (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w})
 125    (a b : (forcedArith R).peano.carrier) :
 126    (universalForcingPeanoEquiv R S).toEquiv (forcedAdd R a b)
 127      = forcedAdd S ((universalForcingPeanoEquiv R S).toEquiv a)
 128          ((universalForcingPeanoEquiv R S).toEquiv b) := by
 129  apply S.orbitEquivLogicNat.injective
 130  simp only [forcedAdd, fold_iso_compat, Equiv.apply_symm_apply]
 131
 132/-- **Multiplicativity.**  The canonical isomorphism is a homomorphism for forced
 133multiplication. -/
 134theorem iso_map_forcedMul (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w})
 135    (a b : (forcedArith R).peano.carrier) :
 136    (universalForcingPeanoEquiv R S).toEquiv (forcedMul R a b)
 137      = forcedMul S ((universalForcingPeanoEquiv R S).toEquiv a)
 138          ((universalForcingPeanoEquiv R S).toEquiv b) := by
 139  apply S.orbitEquivLogicNat.injective
 140  simp only [forcedMul, fold_iso_compat, Equiv.apply_symm_apply]
 141
 142/-- **Order isomorphism.**  The canonical isomorphism preserves and reflects the
 143forced order. -/
 144theorem iso_map_forcedLe (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w})
 145    (a b : (forcedArith R).peano.carrier) :
 146    forcedLe R a b
 147      ↔ forcedLe S ((universalForcingPeanoEquiv R S).toEquiv a)
 148          ((universalForcingPeanoEquiv R S).toEquiv b) := by
 149  simp only [forcedLe, fold_iso_compat]
 150
 151/-! ## Certificate -/
 152
 153/-- **Universal Forcing ordered-semiring isomorphism certificate.**
 154
 155For any two Law-of-Logic realizations, the canonical isomorphism between their
 156forced arithmetics preserves `0`, `1`, addition, multiplication, and the order.
 157Together with `UniversalForcingIsoCert` (zero/successor preservation and
 158uniqueness) this says the forced arithmetics are isomorphic as ordered
 159commutative semirings, canonically, across all realizations. -/
 160structure ForcedOrderedSemiringIsoCert where
 161  preserves_zero : ∀ (R S : LogicRealization.{0, 0}),
 162    (universalForcingPeanoEquiv R S).toEquiv (forcedZero R) = forcedZero S
 163  preserves_one : ∀ (R S : LogicRealization.{0, 0}),
 164    (universalForcingPeanoEquiv R S).toEquiv (forcedOne R) = forcedOne S
 165  preserves_add : ∀ (R S : LogicRealization.{0, 0}) (a b : (forcedArith R).peano.carrier),
 166    (universalForcingPeanoEquiv R S).toEquiv (forcedAdd R a b)
 167      = forcedAdd S ((universalForcingPeanoEquiv R S).toEquiv a)
 168          ((universalForcingPeanoEquiv R S).toEquiv b)
 169  preserves_mul : ∀ (R S : LogicRealization.{0, 0}) (a b : (forcedArith R).peano.carrier),
 170    (universalForcingPeanoEquiv R S).toEquiv (forcedMul R a b)
 171      = forcedMul S ((universalForcingPeanoEquiv R S).toEquiv a)
 172          ((universalForcingPeanoEquiv R S).toEquiv b)
 173  preserves_le : ∀ (R S : LogicRealization.{0, 0}) (a b : (forcedArith R).peano.carrier),
 174    forcedLe R a b
 175      ↔ forcedLe S ((universalForcingPeanoEquiv R S).toEquiv a)
 176          ((universalForcingPeanoEquiv R S).toEquiv b)
 177
 178/-- The ordered-semiring isomorphism certificate is inhabited. -/
 179noncomputable def forcedOrderedSemiringIsoCert : ForcedOrderedSemiringIsoCert where
 180  preserves_zero := fun R S => iso_map_forcedZero R S
 181  preserves_one := fun R S => iso_map_forcedOne R S
 182  preserves_add := fun R S => iso_map_forcedAdd R S
 183  preserves_mul := fun R S => iso_map_forcedMul R S
 184  preserves_le := fun R S => iso_map_forcedLe R S
 185
 186end UniversalForcing
 187end Foundation
 188end IndisputableMonolith
 189