IndisputableMonolith.Foundation.ComplexFromLogic

   1import Mathlib
   2import IndisputableMonolith.Foundation.RealsFromLogic
   3
   4/-!
   5  ComplexFromLogic.lean
   6
   7  Complex numbers over the recovered real line.
   8
   9  We do not redevelop complex analysis in this file.  We construct the carrier
  10  `LogicComplex` as pairs of recovered reals and prove the carrier-level
  11  equivalence with Mathlib's `ℂ`.  Later analytic modules can state explicitly
  12  when holomorphy/contour integration are being performed in Mathlib `ℂ` via
  13  this equivalence.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Foundation
  18namespace ComplexFromLogic
  19
  20open RealsFromLogic
  21open RealsFromLogic.LogicReal
  22open RationalsFromLogic
  23
  24noncomputable section
  25
  26/-- Complex numbers built over recovered reals. -/
  27structure LogicComplex where
  28  re : LogicReal
  29  im : LogicReal
  30
  31namespace LogicComplex
  32
  33/-- Transport a recovered complex number to Mathlib's complex line. -/
  34def toComplex (z : LogicComplex) : ℂ :=
  35  ⟨toReal z.re, toReal z.im⟩
  36
  37/-- Transport a Mathlib complex number to the recovered complex line. -/
  38def fromComplex (z : ℂ) : LogicComplex where
  39  re := fromReal z.re
  40  im := fromReal z.im
  41
  42@[simp] theorem toComplex_re (z : LogicComplex) :
  43    (toComplex z).re = toReal z.re := rfl
  44
  45@[simp] theorem toComplex_im (z : LogicComplex) :
  46    (toComplex z).im = toReal z.im := rfl
  47
  48@[simp] theorem toComplex_fromComplex (z : ℂ) :
  49    toComplex (fromComplex z) = z := by
  50  apply Complex.ext <;> simp [toComplex, fromComplex, toReal_fromReal]
  51
  52@[simp] theorem fromComplex_toComplex (z : LogicComplex) :
  53    fromComplex (toComplex z) = z := by
  54  cases z with
  55  | mk re im =>
  56    simp [toComplex, fromComplex, fromReal_toReal]
  57
  58/-- Carrier equivalence between recovered complex numbers and Mathlib `ℂ`. -/
  59def equivComplex : LogicComplex ≃ ℂ where
  60  toFun := toComplex
  61  invFun := fromComplex
  62  left_inv := fromComplex_toComplex
  63  right_inv := toComplex_fromComplex
  64
  65/-- Equality transfer for recovered complex numbers. -/
  66theorem eq_iff_toComplex_eq {z w : LogicComplex} :
  67    z = w ↔ toComplex z = toComplex w := by
  68  constructor
  69  · exact congrArg toComplex
  70  · intro h
  71    have := congrArg fromComplex h
  72    rw [fromComplex_toComplex, fromComplex_toComplex] at this
  73    exact this
  74
  75/-! ## Algebra and coordinate transport -/
  76
  77instance : Zero LogicComplex := ⟨fromComplex 0⟩
  78instance : One LogicComplex := ⟨fromComplex 1⟩
  79instance : Add LogicComplex := ⟨fun z w => fromComplex (toComplex z + toComplex w)⟩
  80instance : Neg LogicComplex := ⟨fun z => fromComplex (-toComplex z)⟩
  81instance : Sub LogicComplex := ⟨fun z w => fromComplex (toComplex z - toComplex w)⟩
  82instance : Mul LogicComplex := ⟨fun z w => fromComplex (toComplex z * toComplex w)⟩
  83instance : Inv LogicComplex := ⟨fun z => fromComplex (toComplex z)⁻¹⟩
  84instance : Div LogicComplex := ⟨fun z w => fromComplex (toComplex z / toComplex w)⟩
  85
  86@[simp] theorem toComplex_zero : toComplex (0 : LogicComplex) = 0 := by
  87  exact toComplex_fromComplex 0
  88
  89@[simp] theorem toComplex_one : toComplex (1 : LogicComplex) = 1 := by
  90  exact toComplex_fromComplex 1
  91
  92@[simp] theorem toComplex_add (z w : LogicComplex) :
  93    toComplex (z + w) = toComplex z + toComplex w := by
  94  simp [HAdd.hAdd, Add.add]
  95
  96@[simp] theorem toComplex_neg (z : LogicComplex) :
  97    toComplex (-z) = -toComplex z := by
  98  simp [Neg.neg]
  99
 100@[simp] theorem toComplex_sub (z w : LogicComplex) :
 101    toComplex (z - w) = toComplex z - toComplex w := by
 102  simp [HSub.hSub, Sub.sub]
 103
 104@[simp] theorem toComplex_mul (z w : LogicComplex) :
 105    toComplex (z * w) = toComplex z * toComplex w := by
 106  simp [HMul.hMul, Mul.mul]
 107
 108@[simp] theorem toComplex_inv (z : LogicComplex) :
 109    toComplex z⁻¹ = (toComplex z)⁻¹ := by
 110  simp [Inv.inv]
 111
 112@[simp] theorem toComplex_div (z w : LogicComplex) :
 113    toComplex (z / w) = toComplex z / toComplex w := by
 114  simp [HDiv.hDiv, Div.div]
 115
 116/-- Embed recovered reals into recovered complex numbers. -/
 117def ofLogicReal (x : LogicReal) : LogicComplex where
 118  re := x
 119  im := 0
 120
 121@[simp] theorem toComplex_ofLogicReal (x : LogicReal) :
 122    toComplex (ofLogicReal x) = (toReal x : ℂ) := by
 123  apply Complex.ext <;> simp [ofLogicReal, toComplex]
 124
 125/-- Embed recovered rationals into recovered complex numbers through recovered
 126reals. -/
 127def ofLogicRat (q : RationalsFromLogic.LogicRat) : LogicComplex :=
 128  ofLogicReal (RealsFromLogic.LogicReal.ofLogicRat q)
 129
 130@[simp] theorem toComplex_ofLogicRat (q : RationalsFromLogic.LogicRat) :
 131    toComplex (ofLogicRat q) = ((RationalsFromLogic.LogicRat.toRat q : ℚ) : ℂ) := by
 132  rw [ofLogicRat, toComplex_ofLogicReal, toReal_ofLogicRat]
 133  norm_num
 134
 135/-- The recovered complex carrier is exactly Mathlib `ℂ`, by transport. -/
 136theorem logicComplex_recovered_from_mathlib :
 137    (∀ z : LogicComplex, fromComplex (toComplex z) = z) ∧
 138    (∀ z : ℂ, toComplex (fromComplex z) = z) :=
 139  ⟨fromComplex_toComplex, toComplex_fromComplex⟩
 140
 141end LogicComplex
 142
 143end
 144
 145end ComplexFromLogic
 146end Foundation
 147end IndisputableMonolith
 148