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
  65end UniversalForcing
  66end Foundation
  67end IndisputableMonolith
  68