IndisputableMonolith.Foundation.UniversalForcing.AxiomAudit

   1import IndisputableMonolith.Foundation.UniversalForcing.MetaphysicalRealization
   2import IndisputableMonolith.Foundation.UniversalForcing.Invariance.TwoCases
   3import IndisputableMonolith.Foundation.UniversalForcing.ModularRealization
   4import IndisputableMonolith.Foundation.UniversalForcing.OrderRealization
   5import IndisputableMonolith.Foundation.UniversalForcing.CategoricalRealization
   6
   7/-!
   8  AxiomAudit.lean
   9
  10  Reproducible theorem surface for the Universal Forcing Lean program.
  11-/
  12
  13namespace IndisputableMonolith
  14namespace Foundation
  15namespace UniversalForcing
  16namespace AxiomAudit
  17
  18open Invariance.Universal
  19
  20/-! ## Abstract universal forcing -/
  21
  22noncomputable example (R S : LogicRealization) :
  23    (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
  24  ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
  25-- #print axioms Invariance.Universal.universal_forcing
  26--   propext, Quot.sound
  27
  28example (R : LogicRealization) :
  29    ArithmeticOf.PeanoSurface (arithmeticOf R) :=
  30  universal_peano_surface R
  31-- #print axioms Invariance.Universal.universal_peano_surface
  32--   propext, Quot.sound
  33
  34/-! ## First two realizations -/
  35
  36open ContinuousRealization DiscreteRealization
  37
  38noncomputable example
  39    (C : LogicAsFunctionalEquation.ComparisonOperator)
  40    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C) :
  41    (arithmeticOf (continuousRealization C h)).peano.carrier
  42      ≃ (arithmeticOf discreteRealization).peano.carrier :=
  43  ArithmeticOf.equivOfInitial (arithmeticOf (continuousRealization C h))
  44    (arithmeticOf discreteRealization)
  45-- #print axioms Invariance.TwoCases.arith_continuous_equiv_arith_discrete
  46--   propext, Quot.sound
  47
  48/-! ## Mathematical realizations -/
  49
  50open ModularRealization OrderRealization CategoricalRealization
  51
  52noncomputable example (R : LogicRealization.{0, 0}) :
  53    (arithmeticOf orderRealization).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
  54  ArithmeticOf.equivOfInitial (arithmeticOf orderRealization) (arithmeticOf R)
  55-- #print axioms OrderRealization.order_arithmetic_invariant
  56--   propext, Quot.sound
  57
  58noncomputable example (R : LogicRealization.{0, 0}) :
  59    (arithmeticOf categoricalRealization).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
  60  ArithmeticOf.equivOfInitial (arithmeticOf categoricalRealization) (arithmeticOf R)
  61-- #print axioms CategoricalRealization.categorical_arith_equiv_logicNat
  62--   propext
  63
  64/-! ## Extra-mathematical realizations -/
  65
  66open MusicRealization NarrativeRealization EthicsRealization BiologyRealization
  67
  68noncomputable example :
  69    (arithmeticOf musicRealization).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  70  musicRealization.orbitEquivLogicNat
  71
  72noncomputable example :
  73    (arithmeticOf narrativeRealization).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  74  narrativeRealization.orbitEquivLogicNat
  75
  76noncomputable example :
  77    (arithmeticOf ethicsRealization).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  78  ethicsRealization.orbitEquivLogicNat
  79
  80noncomputable example :
  81    (arithmeticOf biologyRealization).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  82  biologyRealization.orbitEquivLogicNat
  83
  84/-! ## Metaphysical structural identification -/
  85
  86open MetaphysicalRealization
  87
  88noncomputable example (R : LogicRealization) :
  89    (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  90  R.orbitEquivLogicNat
  91
  92end AxiomAudit
  93end UniversalForcing
  94end Foundation
  95end IndisputableMonolith
  96