IndisputableMonolith.Foundation.UniversalForcing.ForcedSemiring

   1/-
   2  UniversalForcing/ForcedSemiring.lean
   3
   4  From "the successor tower is forced" to "the arithmetic is forced."
   5
   6  Canonicity (CanonicalForcing) shows the Universal-Forcing map is the unique
   7  zero/step-preserving map between two forced arithmetics. But zero and step are
   8  only the *Peano* surface. The program's thesis is that distinction forces the
   9  same arithmetic *structure*, and arithmetic is the semiring: addition and
  10  multiplication, not just succession.
  11
  12  This module closes that gap. Addition and multiplication on the forced carrier
  13  (`LogicNat`) are the standard primitive-recursive operations
  14  (ArithmeticFromLogic). The key fact is that they are *determined by zero and
  15  step*: any function preserving zero and step automatically preserves `+` and
  16  `*`, because those operations are defined by recursion on step with base zero.
  17  Therefore the canonical forcing map — already the unique zero/step morphism — is
  18  automatically a semiring homomorphism, and being a bijection, a semiring
  19  isomorphism.
  20
  21  The upshot: distinction forces not merely *a successor tower* but *the
  22  arithmetic*, `(ℕ, 0, 1, +, ×)`, canonically, in every strict realization, with
  23  the connecting map a determined semiring isomorphism.
  24-/
  25
  26import IndisputableMonolith.Foundation.UniversalForcing.CanonicalForcing
  27
  28namespace IndisputableMonolith
  29namespace Foundation
  30namespace UniversalForcing
  31namespace ForcedSemiring
  32
  33open ArithmeticFromLogic
  34open ArithmeticFromLogic.LogicNat
  35
  36/-! ## Any zero/step-preserving self-map of `LogicNat` preserves `+` and `×`. -/
  37
  38/-- A map fixing zero and commuting with `succ` preserves addition. Addition
  39recurses on its second argument, so the proof is a single induction. -/
  40theorem map_preserves_add (h : LogicNat → LogicNat)
  41    (h0 : h LogicNat.zero = LogicNat.zero)
  42    (hs : ∀ n, h (LogicNat.succ n) = LogicNat.succ (h n)) :
  43    ∀ a b : LogicNat, h (a + b) = h a + h b := by
  44  intro a b
  45  induction b with
  46  | identity =>
  47      show h (a + LogicNat.zero) = h a + h LogicNat.zero
  48      rw [add_zero, h0, add_zero]
  49  | step b ih =>
  50      show h (a + LogicNat.succ b) = h a + h (LogicNat.succ b)
  51      rw [add_succ, hs, ih, hs, add_succ]
  52
  53/-- A map fixing zero and commuting with `succ` (hence, by the previous lemma,
  54preserving `+`) preserves multiplication. Multiplication recurses on its second
  55argument via addition. -/
  56theorem map_preserves_mul (h : LogicNat → LogicNat)
  57    (h0 : h LogicNat.zero = LogicNat.zero)
  58    (hs : ∀ n, h (LogicNat.succ n) = LogicNat.succ (h n)) :
  59    ∀ a b : LogicNat, h (a * b) = h a * h b := by
  60  have hadd := map_preserves_add h h0 hs
  61  intro a b
  62  induction b with
  63  | identity =>
  64      show h (a * LogicNat.zero) = h a * h LogicNat.zero
  65      rw [mul_zero, h0, mul_zero]
  66  | step b ih =>
  67      show h (a * LogicNat.succ b) = h a * h (LogicNat.succ b)
  68      rw [mul_succ, hadd, ih, hs, mul_succ]
  69
  70/-- A zero/step-preserving map fixes `1 = succ 0`. -/
  71theorem map_preserves_one (h : LogicNat → LogicNat)
  72    (h0 : h LogicNat.zero = LogicNat.zero)
  73    (hs : ∀ n, h (LogicNat.succ n) = LogicNat.succ (h n)) :
  74    h 1 = 1 := by
  75  show h (LogicNat.succ LogicNat.zero) = LogicNat.succ LogicNat.zero
  76  rw [hs, h0]
  77
  78/-! ## The canonical forcing map as a semiring isomorphism. -/
  79
  80/-- The universal-forcing map between two strict realizations, presented as a
  81self-map of `LogicNat` (the forced carriers are definitionally `LogicNat`). -/
  82noncomputable def forcingFn (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) :
  83    LogicNat → LogicNat :=
  84  fun n => (UniversalForcing.Strict.StrictLogicRealization.universal_forcing.{0,0,0,0,0,0} R S) n
  85
  86theorem forcingFn_zero (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) :
  87    forcingFn R S LogicNat.zero = LogicNat.zero :=
  88  UniversalForcing.Strict.StrictLogicRealization.universal_forcing_map_zero R S
  89
  90theorem forcingFn_succ (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) (n : LogicNat) :
  91    forcingFn R S (LogicNat.succ n) = LogicNat.succ (forcingFn R S n) :=
  92  UniversalForcing.Strict.StrictLogicRealization.universal_forcing_map_step R S n
  93
  94/-- **The forcing map preserves addition.** -/
  95theorem forcingFn_add (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0})
  96    (a b : LogicNat) :
  97    forcingFn R S (a + b) = forcingFn R S a + forcingFn R S b :=
  98  map_preserves_add (forcingFn R S) (forcingFn_zero R S) (forcingFn_succ R S) a b
  99
 100/-- **The forcing map preserves multiplication.** -/
 101theorem forcingFn_mul (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0})
 102    (a b : LogicNat) :
 103    forcingFn R S (a * b) = forcingFn R S a * forcingFn R S b :=
 104  map_preserves_mul (forcingFn R S) (forcingFn_zero R S) (forcingFn_succ R S) a b
 105
 106/-- **The forcing map preserves one.** -/
 107theorem forcingFn_one (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) :
 108    forcingFn R S 1 = 1 :=
 109  map_preserves_one (forcingFn R S) (forcingFn_zero R S) (forcingFn_succ R S)
 110
 111/-- The forcing map is a bijection: it is the underlying function of the
 112universal-forcing equivalence. -/
 113theorem forcingFn_bijective (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) :
 114    Function.Bijective (forcingFn R S) :=
 115  (UniversalForcing.Strict.StrictLogicRealization.universal_forcing.{0,0,0,0,0,0} R S).bijective
 116
 117/-- **Uniqueness as a semiring map.** Any function preserving zero and step
 118equals the forcing map, so in particular the forcing map is the unique semiring
 119homomorphism — it is determined, not chosen. (Restated from canonicity for the
 120`LogicNat` presentation.) -/
 121theorem forcingFn_unique (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0})
 122    (f : LogicNat → LogicNat)
 123    (h0 : f LogicNat.zero = LogicNat.zero)
 124    (hs : ∀ n, f (LogicNat.succ n) = LogicNat.succ (f n)) :
 125    f = forcingFn R S :=
 126  UniversalForcing.Strict.StrictLogicRealization.universal_forcing_unique R S f h0 hs
 127
 128/-- **Certificate: distinction forces the arithmetic, not just the tower.** For
 129any two strict realizations the canonical forcing map is a bijection that
 130preserves `0`, `1`, `+`, and `×`, and it is the unique zero/step-preserving map.
 131The forced object is the semiring `(ℕ, 0, 1, +, ×)`, canonically. -/
 132structure ForcedSemiringCert where
 133  map : ∀ (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}), LogicNat → LogicNat
 134  bij : ∀ R S, Function.Bijective (map R S)
 135  zero : ∀ R S, map R S LogicNat.zero = LogicNat.zero
 136  one : ∀ R S, map R S 1 = 1
 137  add : ∀ R S a b, map R S (a + b) = map R S a + map R S b
 138  mul : ∀ R S a b, map R S (a * b) = map R S a * map R S b
 139  unique : ∀ R S (f : LogicNat → LogicNat),
 140      f LogicNat.zero = LogicNat.zero →
 141      (∀ n, f (LogicNat.succ n) = LogicNat.succ (f n)) →
 142      f = map R S
 143
 144/-- The forced-semiring certificate holds. -/
 145noncomputable def forcedSemiringCert_holds : ForcedSemiringCert where
 146  map := forcingFn
 147  bij := forcingFn_bijective
 148  zero := forcingFn_zero
 149  one := forcingFn_one
 150  add := forcingFn_add
 151  mul := forcingFn_mul
 152  unique := forcingFn_unique
 153
 154/-! ## Honest note: on the strict path the forcing map is the identity.
 155
 156`StrictLogicRealization` uses a uniform free orbit (`LogicNat`) for every
 157realization, so the two forced arithmetics are literally the same carrier and the
 158canonical map between them is the identity. This does not trivialize the theory:
 159the non-trivial content is (a) the general preservation lemmas above, which apply
 160to *any* zero/step map, and (b) the cross-carrier canonicity in
 161`CanonicalForcing.ArithmeticOf.forcing_map_unique`. It is simply honest about the
 162strict presentation. -/
 163theorem forcingFn_eq_id (R S : UniversalForcing.Strict.StrictLogicRealization.{0,0}) :
 164    forcingFn R S = id :=
 165  (forcingFn_unique R S id rfl (fun _ => rfl)).symm
 166
 167/-! ## The forced arithmetic is Lean's `ℕ`, as a semiring. -/
 168
 169theorem toNat_one : LogicNat.toNat 1 = 1 := rfl
 170
 171/-- **Capstone: distinction forces `ℕ`.** The forced carrier `LogicNat` is
 172isomorphic to Lean's `Nat` as a `(0, 1, +, ×)`-structure. Every strict realization
 173forces this same carrier (CanonicalForcing), so the arithmetic that distinction
 174forces is, up to canonical semiring isomorphism, exactly the natural numbers Lean
 175already has — with no base, no positional notation, and no arithmetic axioms
 176posited. -/
 177structure ForcedArithmeticIsNat where
 178  toEquiv : LogicNat ≃ Nat
 179  map_zero : toEquiv LogicNat.zero = 0
 180  map_one : toEquiv 1 = 1
 181  map_add : ∀ a b, toEquiv (a + b) = toEquiv a + toEquiv b
 182  map_mul : ∀ a b, toEquiv (a * b) = toEquiv a * toEquiv b
 183
 184/-- The forced arithmetic is `ℕ`. -/
 185noncomputable def forcedArithmeticIsNat : ForcedArithmeticIsNat where
 186  toEquiv := LogicNat.equivNat
 187  map_zero := LogicNat.toNat_zero
 188  map_one := toNat_one
 189  map_add := LogicNat.toNat_add
 190  map_mul := LogicNat.toNat_mul
 191
 192end ForcedSemiring
 193end UniversalForcing
 194end Foundation
 195end IndisputableMonolith
 196