IndisputableMonolith.Foundation.RealsFromLogic

   1import Mathlib.Topology.UniformSpace.CompareReals
   2import IndisputableMonolith.Foundation.RationalsFromLogic
   3
   4/-!
   5  RealsFromLogic.lean
   6
   7  Recovery of the real numbers from the Law-of-Logic rational layer.
   8
   9  The construction uses Mathlib's Bourbaki completion of `ℚ` as the
  10  completion engine, while the input rationals are the recovered rationals
  11  `LogicRat` from `Foundation.RationalsFromLogic`.  In other words:
  12
  13    Law of Logic
  14      ⊢ LogicNat
  15      ⊢ LogicInt
  16      ⊢ LogicRat ≃ ℚ
  17      ⊢ Completion ℚ ≃ ℝ
  18
  19  The type `LogicReal` is a wrapper around `CompareReals.Bourbakiℝ`,
  20  Mathlib's uniform-space completion of the rational uniform space.  The
  21  map `toReal` is the canonical comparison equivalence with Mathlib's
  22  Cauchy real numbers.
  23
  24  This file intentionally exposes a transport-first API.  Algebra and
  25  order on `LogicReal` are defined by pulling back the corresponding
  26  structures along `toReal`, so every downstream theorem can reduce to
  27  the existing real theorem and then be read back as a recovered-real
  28  theorem.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Foundation
  33namespace RealsFromLogic
  34
  35open Filter UniformSpace
  36open RationalsFromLogic RationalsFromLogic.LogicRat
  37
  38noncomputable section
  39
  40/-! ## 1. Logic-rational Cauchy sequences -/
  41
  42/-- A recovered-rational Cauchy sequence. The Cauchy predicate is measured
  43after transport to Mathlib's `ℚ`, using the standard uniform structure on
  44`ℚ`. This is the exact point where the recovered rational layer enters the
  45Cauchy completion. -/
  46structure CauchySeqLogicRat where
  47  seq : ℕ → LogicRat
  48  cauchy_toRat : CauchySeq (fun n => toRat (seq n))
  49
  50/-- The underlying Mathlib-rational sequence of a recovered-rational Cauchy
  51sequence. -/
  52def CauchySeqLogicRat.toRatSeq (s : CauchySeqLogicRat) : ℕ → ℚ :=
  53  fun n => toRat (s.seq n)
  54
  55theorem CauchySeqLogicRat.toRatSeq_cauchy (s : CauchySeqLogicRat) :
  56    CauchySeq s.toRatSeq :=
  57  s.cauchy_toRat
  58
  59/-! ## 2. The recovered real type -/
  60
  61/-- `LogicReal` is the Cauchy completion of the recovered rationals, realized
  62through the canonical completion of `ℚ` and the equivalence `LogicRat ≃ ℚ`.
  63
  64The wrapper prevents global instance pollution on `Completion ℚ` while still
  65letting us reuse Mathlib's completed real line. -/
  66structure LogicReal where
  67  val : CompareReals.Bourbakiℝ
  68
  69namespace LogicReal
  70
  71/-- Transport a recovered real to Mathlib's real line. -/
  72noncomputable def toReal (x : LogicReal) : ℝ :=
  73  CompareReals.compareEquiv x.val
  74
  75/-- Transport a Mathlib real into the recovered real line. -/
  76noncomputable def fromReal (x : ℝ) : LogicReal :=
  77  ⟨CompareReals.compareEquiv.symm x⟩
  78
  79theorem toReal_fromReal (x : ℝ) : toReal (fromReal x) = x := by
  80  simp [toReal, fromReal]
  81
  82theorem fromReal_toReal (x : LogicReal) : fromReal (toReal x) = x := by
  83  cases x
  84  simp [toReal, fromReal]
  85
  86/-- Carrier equivalence between recovered reals and Mathlib reals. -/
  87noncomputable def equivReal : LogicReal ≃ ℝ where
  88  toFun := toReal
  89  invFun := fromReal
  90  left_inv := fromReal_toReal
  91  right_inv := toReal_fromReal
  92
  93/-- Equality transfer: recovered real equality is exactly equality after
  94transport to Mathlib's real line. -/
  95theorem eq_iff_toReal_eq {x y : LogicReal} : x = y ↔ toReal x = toReal y := by
  96  constructor
  97  · exact congrArg toReal
  98  · intro h
  99    have := congrArg fromReal h
 100    rw [fromReal_toReal, fromReal_toReal] at this
 101    exact this
 102
 103/-! ## 3. Embedding of recovered rationals -/
 104
 105/-- Coerce a Mathlib rational into the Bourbaki completion. -/
 106noncomputable def ofRatCore (q : ℚ) : LogicReal :=
 107  ⟨Completion.coe' (show CompareReals.Q from q)⟩
 108
 109/-- Embed a recovered rational into `LogicReal`. -/
 110noncomputable def ofLogicRat (q : LogicRat) : LogicReal :=
 111  ofRatCore (toRat q)
 112
 113theorem toReal_ofRatCore (q : ℚ) : toReal (ofRatCore q) = (q : ℝ) := by
 114  -- `CompareReals.compareEquiv` is the unique completion comparison map;
 115  -- on dense rational points it agrees with the usual rational coercion.
 116  simpa [toReal, ofRatCore, CompareReals.compareEquiv] using
 117    (CompareReals.bourbakiPkg.compare_coe rationalCauSeqPkg
 118      (show CompareReals.Q from q))
 119
 120theorem toReal_ofLogicRat (q : LogicRat) : toReal (ofLogicRat q) = (toRat q : ℝ) := by
 121  rw [ofLogicRat, toReal_ofRatCore]
 122
 123/-! ## 4. Algebra and order by transport through `toReal` -/
 124
 125instance : Zero LogicReal := ⟨fromReal 0⟩
 126instance : One LogicReal := ⟨fromReal 1⟩
 127instance : Add LogicReal := ⟨fun x y => fromReal (toReal x + toReal y)⟩
 128instance : Neg LogicReal := ⟨fun x => fromReal (-toReal x)⟩
 129instance : Sub LogicReal := ⟨fun x y => fromReal (toReal x - toReal y)⟩
 130instance : Mul LogicReal := ⟨fun x y => fromReal (toReal x * toReal y)⟩
 131instance : Inv LogicReal := ⟨fun x => fromReal (toReal x)⁻¹⟩
 132instance : Div LogicReal := ⟨fun x y => fromReal (toReal x / toReal y)⟩
 133instance : LE LogicReal := ⟨fun x y => toReal x ≤ toReal y⟩
 134instance : LT LogicReal := ⟨fun x y => toReal x < toReal y⟩
 135
 136@[simp] theorem toReal_zero : toReal (0 : LogicReal) = 0 := toReal_fromReal 0
 137@[simp] theorem toReal_one : toReal (1 : LogicReal) = 1 := toReal_fromReal 1
 138@[simp] theorem toReal_add (x y : LogicReal) : toReal (x + y) = toReal x + toReal y :=
 139  toReal_fromReal _
 140@[simp] theorem toReal_neg (x : LogicReal) : toReal (-x) = -toReal x :=
 141  toReal_fromReal _
 142@[simp] theorem toReal_sub (x y : LogicReal) : toReal (x - y) = toReal x - toReal y :=
 143  toReal_fromReal _
 144@[simp] theorem toReal_mul (x y : LogicReal) : toReal (x * y) = toReal x * toReal y :=
 145  toReal_fromReal _
 146@[simp] theorem toReal_inv (x : LogicReal) : toReal x⁻¹ = (toReal x)⁻¹ :=
 147  toReal_fromReal _
 148@[simp] theorem toReal_div (x y : LogicReal) : toReal (x / y) = toReal x / toReal y :=
 149  toReal_fromReal _
 150
 151theorem le_iff_toReal_le {x y : LogicReal} : x ≤ y ↔ toReal x ≤ toReal y := Iff.rfl
 152theorem lt_iff_toReal_lt {x y : LogicReal} : x < y ↔ toReal x < toReal y := Iff.rfl
 153
 154theorem add_assoc' (x y z : LogicReal) : (x + y) + z = x + (y + z) := by
 155  rw [eq_iff_toReal_eq]
 156  simp
 157  ring
 158
 159theorem add_comm' (x y : LogicReal) : x + y = y + x := by
 160  rw [eq_iff_toReal_eq]
 161  simp
 162  ring
 163
 164theorem zero_add' (x : LogicReal) : (0 : LogicReal) + x = x := by
 165  rw [eq_iff_toReal_eq]
 166  simp
 167
 168theorem add_zero' (x : LogicReal) : x + (0 : LogicReal) = x := by
 169  rw [eq_iff_toReal_eq]
 170  simp
 171
 172theorem add_left_neg' (x : LogicReal) : -x + x = 0 := by
 173  rw [eq_iff_toReal_eq]
 174  simp
 175
 176theorem mul_assoc' (x y z : LogicReal) : (x * y) * z = x * (y * z) := by
 177  rw [eq_iff_toReal_eq]
 178  simp
 179  ring
 180
 181theorem mul_comm' (x y : LogicReal) : x * y = y * x := by
 182  rw [eq_iff_toReal_eq]
 183  simp
 184  ring
 185
 186theorem one_mul' (x : LogicReal) : (1 : LogicReal) * x = x := by
 187  rw [eq_iff_toReal_eq]
 188  simp
 189
 190theorem mul_one' (x : LogicReal) : x * (1 : LogicReal) = x := by
 191  rw [eq_iff_toReal_eq]
 192  simp
 193
 194theorem mul_add' (x y z : LogicReal) : x * (y + z) = x * y + x * z := by
 195  rw [eq_iff_toReal_eq]
 196  simp
 197  ring
 198
 199theorem add_mul' (x y z : LogicReal) : (x + y) * z = x * z + y * z := by
 200  rw [eq_iff_toReal_eq]
 201  simp
 202  ring
 203
 204/-! ## 5. Completeness certificate -/
 205
 206/-- The underlying Bourbaki completion is complete. This is the formal
 207completion theorem for the recovered real layer. -/
 208theorem bourbaki_complete : CompleteSpace CompareReals.Bourbakiℝ := by
 209  change CompleteSpace (Completion CompareReals.Q)
 210  infer_instance
 211
 212/-- Every recovered real is represented by a Mathlib real and vice versa. -/
 213theorem logicReal_recovered_from_completion :
 214    (∀ x : LogicReal, fromReal (toReal x) = x) ∧
 215    (∀ x : ℝ, toReal (fromReal x) = x) :=
 216  ⟨fromReal_toReal, toReal_fromReal⟩
 217
 218end LogicReal
 219
 220end
 221
 222end RealsFromLogic
 223end Foundation
 224end IndisputableMonolith
 225