IndisputableMonolith.Foundation.UniversalForcingAudit

   1import IndisputableMonolith.Foundation.UniversalForcing
   2import IndisputableMonolith.Foundation.DiscreteLogicRealization
   3import IndisputableMonolith.Foundation.CategoricalLogicRealization
   4import IndisputableMonolith.Foundation.ModularLogicRealization
   5import IndisputableMonolith.Foundation.OrderedLogicRealization
   6import IndisputableMonolith.Foundation.PhysicsLogicRealization
   7
   8/-!
   9  UniversalForcingAudit.lean
  10
  11  Reproducible audit surface for the Universal Forcing program.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Foundation
  16namespace UniversalForcingAudit
  17
  18open UniversalForcing
  19open DiscreteLogicRealization
  20open CategoricalLogicRealization
  21open ModularLogicRealization
  22open OrderedLogicRealization
  23open PhysicsLogicRealization
  24
  25/-! ## Abstract theorem surface -/
  26
  27noncomputable example (R S : LogicRealization.{0, 0}) :
  28    (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier :=
  29  ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
  30-- #print axioms UniversalForcing.arithmetic_invariant
  31--   propext, Quot.sound
  32
  33example (R : LogicRealization) :
  34    ArithmeticOf.PeanoSurface (arithmeticOf R) :=
  35  peano_surface R
  36-- #print axioms UniversalForcing.peano_surface
  37--   propext, Quot.sound
  38
  39/-! ## Continuous positive-ratio realization -/
  40
  41noncomputable example
  42    (C : LogicAsFunctionalEquation.ComparisonOperator)
  43    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C)
  44    (S : LogicRealization.{0, 0}) :
  45    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)).peano.carrier
  46      ≃ (arithmeticOf S).peano.carrier :=
  47  ArithmeticOf.equivOfInitial
  48    (arithmeticOf (LogicRealization.ofPositiveRatioComparison C h)) (arithmeticOf S)
  49-- #print axioms UniversalForcing.continuous_positive_ratio_arithmetic_invariant
  50--   propext, Quot.sound
  51
  52/-! ## Discrete and categorical realizations -/
  53
  54example : boolRealization.hasIdentityStep :=
  55  bool_hasIdentityStep
  56-- #print axioms DiscreteLogicRealization.bool_hasIdentityStep
  57--   propext
  58
  59noncomputable example (R : LogicRealization.{0, 0}) :
  60    (arithmeticOf boolRealization).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
  61  ArithmeticOf.equivOfInitial (arithmeticOf boolRealization) (arithmeticOf R)
  62-- #print axioms DiscreteLogicRealization.bool_arithmetic_invariant
  63--   propext, Quot.sound
  64
  65noncomputable example (R : LogicRealization.{0, 0}) :
  66    (arithmeticOf canonicalCategoricalRealization).peano.carrier
  67      ≃ (arithmeticOf R).peano.carrier :=
  68  ArithmeticOf.equivOfInitial (arithmeticOf canonicalCategoricalRealization) (arithmeticOf R)
  69-- #print axioms CategoricalLogicRealization.categorical_arithmetic_invariant
  70--   propext, Quot.sound
  71
  72/-! ## Modular, ordered, and physics realizations -/
  73
  74noncomputable example (k : ℕ) (R : LogicRealization.{0, 0}) :
  75    (arithmeticOf (modularRealization k)).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
  76  ArithmeticOf.equivOfInitial (arithmeticOf (modularRealization k)) (arithmeticOf R)
  77-- #print axioms ModularLogicRealization.modular_arithmetic_invariant
  78--   propext, Quot.sound
  79
  80example (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
  81    modularInterpret k
  82        (ArithmeticFromLogic.LogicNat.fromNat
  83          (ArithmeticFromLogic.LogicNat.toNat n + modulus k))
  84      = modularInterpret k n :=
  85  modular_interpret_periodic k n
  86-- #print axioms ModularLogicRealization.modular_interpret_periodic
  87--   propext, Quot.sound
  88
  89example :
  90    LogicRealization.FaithfulArithmeticInterpretation natOrderedRealization :=
  91  ordered_faithful
  92-- #print axioms OrderedLogicRealization.ordered_faithful
  93--   propext, Quot.sound
  94
  95noncomputable example (R : LogicRealization.{0, 0}) :
  96    (arithmeticOf natOrderedRealization).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
  97  ArithmeticOf.equivOfInitial (arithmeticOf natOrderedRealization) (arithmeticOf R)
  98-- #print axioms OrderedLogicRealization.ordered_arithmetic_invariant
  99--   propext, Quot.sound
 100
 101example :
 102    LogicRealization.FaithfulArithmeticInterpretation physicsRealization :=
 103  physics_faithful
 104-- #print axioms PhysicsLogicRealization.physics_faithful
 105--   propext, Quot.sound
 106
 107noncomputable example (R : LogicRealization.{0, 0}) :
 108    (arithmeticOf physicsRealization).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
 109  ArithmeticOf.equivOfInitial (arithmeticOf physicsRealization) (arithmeticOf R)
 110-- #print axioms PhysicsLogicRealization.physics_arithmetic_invariant
 111--   propext, Quot.sound
 112
 113end UniversalForcingAudit
 114end Foundation
 115end IndisputableMonolith
 116