IndisputableMonolith.Foundation.UniversalForcing

   1import IndisputableMonolith.Foundation.ArithmeticOf
   2
   3/-!
   4  UniversalForcing.lean
   5
   6  First formal statement of the Universal Forcing theorem:
   7
   8  any two Law-of-Logic realizations have canonically equivalent forced
   9  arithmetic objects, because those objects are initial Peano algebras.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace UniversalForcing
  15
  16/-- The forced arithmetic object of a realization. -/
  17def arithmeticOf (R : LogicRealization) : ArithmeticOf R :=
  18  ArithmeticOf.extracted R
  19
  20/-- **Universal Forcing, first theorem form.**
  21
  22For any two Law-of-Logic realizations, the arithmetic objects extracted from
  23them are canonically equivalent. In this first formal spine the equivalence is
  24the unique equivalence between initial Peano algebras. Later realization
  25modules enrich the interpretation map from each carrier into this invariant
  26arithmetic object. This definition now uses the realization's own internal
  27orbit, not the reference `LogicNat` object. -/
  28noncomputable def arithmetic_invariant
  29    (R S : LogicRealization) :
  30    (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
  31  ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
  32
  33/-- The forced arithmetic of every realization is canonically equivalent to
  34the reference `LogicNat` Peano object. This is the simplest form of the
  35Universal Forcing theorem. -/
  36noncomputable def arith_universal_initial (R : LogicRealization) :
  37    (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  38  R.orbitEquivLogicNat
  39
  40/-- **Universal Forcing Meta-Theorem, abstract spine.**
  41
  42Any two Law-of-Logic realizations have canonically equivalent forced
  43arithmetic objects. -/
  44noncomputable def universal_forcing (R S : LogicRealization) :
  45    (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
  46  ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
  47
  48/-- The continuous positive-ratio realization has the same forced arithmetic
  49as every other realization. -/
  50noncomputable def continuous_positive_ratio_arithmetic_invariant
  51    (C : LogicAsFunctionalEquation.ComparisonOperator)
  52    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C)
  53    (S : LogicRealization.{0, 0}) :
  54    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier
  55      ≃ (arithmeticOf S).peano.carrier :=
  56  ArithmeticOf.equivOfInitial
  57    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)) (arithmeticOf S)
  58
  59/-- The Peano surface is available for the forced arithmetic of every
  60realization. -/
  61theorem peano_surface (R : LogicRealization) :
  62    ArithmeticOf.PeanoSurface (arithmeticOf R) :=
  63  ArithmeticOf.extracted_peanoSurface R
  64
  65/-! ## Paper-Upgrade Certificate
  66
  67This package is the Lean-facing headline for the arithmetic paper's stronger
  68version: the positive-ratio construction is not a special arithmetic choice.
  69Every Law-of-Logic realization extracts an initial Peano object, every such
  70object is equivalent to the reference `LogicNat`, and any two extracted
  71arithmetic objects are canonically equivalent.
  72-/
  73
  74/-- **Universal Forcing certificate.**
  75
  76The arithmetic extracted from any admissible Law-of-Logic realization is
  77initial, has the Peano surface, is equivalent to `LogicNat`, and is invariant
  78up to canonical equivalence across realizations. -/
  79structure UniversalForcingCert where
  80  invariant :
  81    ∀ R S : LogicRealization.{0, 0},
  82      (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier
  83  to_reference :
  84    ∀ R : LogicRealization.{0, 0},
  85      (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat
  86  peano :
  87    ∀ R : LogicRealization.{0, 0},
  88      ArithmeticOf.PeanoSurface (arithmeticOf R)
  89  continuous_positive_ratio_invariant :
  90    ∀ (C : LogicAsFunctionalEquation.ComparisonOperator)
  91      (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C)
  92      (S : LogicRealization.{0, 0}),
  93      (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier
  94        ≃ (arithmeticOf S).peano.carrier
  95
  96/-- The Universal Forcing certificate is inhabited by the existing initiality
  97theorems. -/
  98noncomputable def universalForcingCert : UniversalForcingCert where
  99  invariant := fun R S => by
 100    change R.Orbit ≃ S.Orbit
 101    exact R.orbitEquivLogicNat.trans S.orbitEquivLogicNat.symm
 102  to_reference := fun R => by
 103    change R.Orbit ≃ ArithmeticFromLogic.LogicNat
 104    exact R.orbitEquivLogicNat
 105  peano := fun R => peano_surface R
 106  continuous_positive_ratio_invariant := fun C h S =>
 107    by
 108      change ArithmeticFromLogic.LogicNat ≃ S.Orbit
 109      exact S.orbitEquivLogicNat.symm
 110
 111/-- Any two Law-of-Logic realizations force the same arithmetic surface. -/
 112theorem forced_arithmetic_surfaces_equivalent (R S : LogicRealization.{0, 0}) :
 113    Nonempty ((arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier) :=
 114  ⟨by
 115    change R.Orbit ≃ S.Orbit
 116    exact R.orbitEquivLogicNat.trans S.orbitEquivLogicNat.symm⟩
 117
 118end UniversalForcing
 119end Foundation
 120end IndisputableMonolith
 121