IndisputableMonolith.Foundation.RecoveredTowerAxiomAudit

   1import IndisputableMonolith.Foundation.ArithmeticFromLogic
   2import IndisputableMonolith.Foundation.IntegersFromLogic
   3import IndisputableMonolith.Foundation.RationalsFromLogic
   4import IndisputableMonolith.Foundation.RealsFromLogic
   5import IndisputableMonolith.Foundation.ComplexFromLogic
   6
   7/-!
   8  RecoveredTowerAxiomAudit.lean
   9
  10  Audit surface for the Law-of-Logic recovered number tower:
  11
  12    LogicNat → LogicInt → LogicRat → LogicReal → LogicComplex.
  13
  14  The point of this file is not to rebuild arithmetic. It pins the named
  15  recovery/equality/transport theorems in one import target so `#print axioms`
  16  can be run consistently as the tower is strengthened.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Foundation
  21namespace RecoveredTowerAxiomAudit
  22
  23/-! ## Natural numbers -/
  24
  25example : ArithmeticFromLogic.LogicNat ≃ Nat :=
  26  ArithmeticFromLogic.LogicNat.equivNat
  27-- #print axioms ArithmeticFromLogic.LogicNat.equivNat
  28--   no axioms
  29
  30example (a b : ArithmeticFromLogic.LogicNat) :
  31    ArithmeticFromLogic.LogicNat.toNat (a + b)
  32      = ArithmeticFromLogic.LogicNat.toNat a + ArithmeticFromLogic.LogicNat.toNat b :=
  33  ArithmeticFromLogic.LogicNat.toNat_add a b
  34-- #print axioms ArithmeticFromLogic.LogicNat.toNat_add
  35--   no axioms
  36
  37example (a b : ArithmeticFromLogic.LogicNat) :
  38    ArithmeticFromLogic.LogicNat.toNat (a * b)
  39      = ArithmeticFromLogic.LogicNat.toNat a * ArithmeticFromLogic.LogicNat.toNat b :=
  40  ArithmeticFromLogic.LogicNat.toNat_mul a b
  41-- #print axioms ArithmeticFromLogic.LogicNat.toNat_mul
  42--   no axioms
  43
  44/-! ## Integers -/
  45
  46example : IntegersFromLogic.LogicInt ≃ Int :=
  47  IntegersFromLogic.LogicInt.equivInt
  48-- #print axioms IntegersFromLogic.LogicInt.equivInt
  49--   propext, Quot.sound
  50
  51example (a b : IntegersFromLogic.LogicInt) :
  52    IntegersFromLogic.LogicInt.toInt (a + b)
  53      = IntegersFromLogic.LogicInt.toInt a + IntegersFromLogic.LogicInt.toInt b :=
  54  IntegersFromLogic.LogicInt.toInt_add a b
  55-- #print axioms IntegersFromLogic.LogicInt.toInt_add
  56--   propext, Quot.sound
  57
  58example (a b : IntegersFromLogic.LogicInt) :
  59    IntegersFromLogic.LogicInt.toInt (a * b)
  60      = IntegersFromLogic.LogicInt.toInt a * IntegersFromLogic.LogicInt.toInt b :=
  61  IntegersFromLogic.LogicInt.toInt_mul a b
  62-- #print axioms IntegersFromLogic.LogicInt.toInt_mul
  63--   propext, Quot.sound
  64
  65/-! ## Rationals -/
  66
  67noncomputable example : RationalsFromLogic.LogicRat ≃ ℚ :=
  68  RationalsFromLogic.LogicRat.equivRat
  69-- #print axioms RationalsFromLogic.LogicRat.equivRat
  70--   propext, Classical.choice, Quot.sound
  71
  72example (a b : RationalsFromLogic.LogicRat) :
  73    RationalsFromLogic.LogicRat.toRat (a + b)
  74      = RationalsFromLogic.LogicRat.toRat a + RationalsFromLogic.LogicRat.toRat b :=
  75  RationalsFromLogic.LogicRat.toRat_add a b
  76-- #print axioms RationalsFromLogic.LogicRat.toRat_add
  77--   propext, Classical.choice, Quot.sound
  78
  79example (a b : RationalsFromLogic.LogicRat) :
  80    RationalsFromLogic.LogicRat.toRat (a * b)
  81      = RationalsFromLogic.LogicRat.toRat a * RationalsFromLogic.LogicRat.toRat b :=
  82  RationalsFromLogic.LogicRat.toRat_mul a b
  83-- #print axioms RationalsFromLogic.LogicRat.toRat_mul
  84--   propext, Classical.choice, Quot.sound
  85
  86/-! ## Reals -/
  87
  88noncomputable example : RealsFromLogic.LogicReal ≃ ℝ :=
  89  RealsFromLogic.LogicReal.equivReal
  90-- #print axioms RealsFromLogic.LogicReal.equivReal
  91--   propext, Classical.choice, Quot.sound
  92
  93example (x y : RealsFromLogic.LogicReal) :
  94    RealsFromLogic.LogicReal.toReal (x + y)
  95      = RealsFromLogic.LogicReal.toReal x + RealsFromLogic.LogicReal.toReal y :=
  96  RealsFromLogic.LogicReal.toReal_add x y
  97-- #print axioms RealsFromLogic.LogicReal.toReal_add
  98--   propext, Classical.choice, Quot.sound
  99
 100example (x y : RealsFromLogic.LogicReal) :
 101    RealsFromLogic.LogicReal.toReal (x * y)
 102      = RealsFromLogic.LogicReal.toReal x * RealsFromLogic.LogicReal.toReal y :=
 103  RealsFromLogic.LogicReal.toReal_mul x y
 104-- #print axioms RealsFromLogic.LogicReal.toReal_mul
 105--   propext, Classical.choice, Quot.sound
 106
 107/-! ## Complex numbers -/
 108
 109noncomputable example : ComplexFromLogic.LogicComplex ≃ ℂ :=
 110  ComplexFromLogic.LogicComplex.equivComplex
 111-- #print axioms ComplexFromLogic.LogicComplex.equivComplex
 112--   propext, Classical.choice, Quot.sound
 113
 114example (z w : ComplexFromLogic.LogicComplex) :
 115    ComplexFromLogic.LogicComplex.toComplex (z + w)
 116      = ComplexFromLogic.LogicComplex.toComplex z + ComplexFromLogic.LogicComplex.toComplex w :=
 117  ComplexFromLogic.LogicComplex.toComplex_add z w
 118-- #print axioms ComplexFromLogic.LogicComplex.toComplex_add
 119--   propext, Classical.choice, Quot.sound
 120
 121example (z w : ComplexFromLogic.LogicComplex) :
 122    ComplexFromLogic.LogicComplex.toComplex (z * w)
 123      = ComplexFromLogic.LogicComplex.toComplex z * ComplexFromLogic.LogicComplex.toComplex w :=
 124  ComplexFromLogic.LogicComplex.toComplex_mul z w
 125-- #print axioms ComplexFromLogic.LogicComplex.toComplex_mul
 126--   propext, Classical.choice, Quot.sound
 127
 128end RecoveredTowerAxiomAudit
 129end Foundation
 130end IndisputableMonolith
 131