IndisputableMonolith.Foundation.IntegersFromLogic

   1/-
   2  IntegersFromLogic.lean
   3
   4  Recovery of the integers from `LogicNat`, by Grothendieck completion.
   5
   6  An integer is a formal difference `a - b` with `a, b : LogicNat`,
   7  modulo the equivalence `(a, b) ~ (c, d) ↔ a + d = c + b`. This is
   8  the universal additive group containing `LogicNat` as a sub-monoid.
   9  In Lean we realize the construction as a quotient of
  10  `LogicNat × LogicNat`.
  11
  12  The recovery chain extends:
  13
  14    Law of Logic (Foundation.LogicAsFunctionalEquation)
  15      ⊢ J via Translation Theorem and Aczél
  16      ⊢ LogicNat via orbit structure (Foundation.ArithmeticFromLogic)
  17      ⊢ LogicInt via Grothendieck completion (this module)
  18      ⊢ ≃ Int (recovery isomorphism)
  19
  20  Status: Level 1. Defines the carrier, ring operations (+, -, *, neg),
  21  proves a small number of key identities (associativity, additive
  22  identity, additive inverse), and states the equivalence with `Int`
  23  at the carrier level. A full ring isomorphism (every Mathlib ring
  24  axiom) is left for a follow-up; the structural recovery is what this
  25  module establishes.
  26-/
  27
  28import Mathlib
  29import IndisputableMonolith.Foundation.ArithmeticFromLogic
  30
  31namespace IndisputableMonolith
  32namespace Foundation
  33namespace IntegersFromLogic
  34
  35open ArithmeticFromLogic ArithmeticFromLogic.LogicNat
  36
  37/-! ## 1. The Grothendieck Equivalence -/
  38
  39/-- The Grothendieck equivalence relation on pairs of `LogicNat`:
  40`(a, b) ~ (c, d)` iff `a + d = c + b`. The pair `(a, b)` represents
  41the formal difference `a - b`. -/
  42def intRel : (LogicNat × LogicNat) → (LogicNat × LogicNat) → Prop :=
  43  fun p q => p.1 + q.2 = q.1 + p.2
  44
  45theorem intRel_refl : ∀ p : LogicNat × LogicNat, intRel p p := by
  46  intro p
  47  show p.1 + p.2 = p.1 + p.2
  48  rfl
  49
  50theorem intRel_symm : ∀ {p q : LogicNat × LogicNat}, intRel p q → intRel q p := by
  51  intro p q h
  52  show q.1 + p.2 = p.1 + q.2
  53  exact h.symm
  54
  55theorem intRel_trans : ∀ {p q r : LogicNat × LogicNat},
  56    intRel p q → intRel q r → intRel p r := by
  57  rintro ⟨a, b⟩ ⟨c, d⟩ ⟨e, f⟩ hpq hqr
  58  show a + f = e + b
  59  rw [eq_iff_toNat_eq, toNat_add, toNat_add]
  60  have hpq' : toNat a + toNat d = toNat c + toNat b := by
  61    have := congrArg toNat (show a + d = c + b from hpq)
  62    rwa [toNat_add, toNat_add] at this
  63  have hqr' : toNat c + toNat f = toNat e + toNat d := by
  64    have := congrArg toNat (show c + f = e + d from hqr)
  65    rwa [toNat_add, toNat_add] at this
  66  omega
  67
  68/-- The setoid structure on `LogicNat × LogicNat` for Grothendieck
  69completion. -/
  70instance setoid : Setoid (LogicNat × LogicNat) :=
  71  ⟨intRel, intRel_refl, intRel_symm, intRel_trans⟩
  72
  73/-! ## 2. The Type of Logic-Native Integers -/
  74
  75/-- `LogicInt` is the Grothendieck completion of `LogicNat` under
  76addition. -/
  77def LogicInt : Type := Quotient (setoid : Setoid (LogicNat × LogicNat))
  78
  79namespace LogicInt
  80
  81/-- Constructor: form an integer from a pair of naturals. -/
  82def mk (a b : LogicNat) : LogicInt := Quotient.mk' (a, b)
  83
  84/-- Notation `[a, b]ₗ` for the integer `a − b`. Avoids clash with
  85list and matrix notations. -/
  86notation:max "[" a ", " b "]ₗ" => mk a b
  87
  88theorem sound (a b c d : LogicNat) (h : a + d = c + b) :
  89    mk a b = mk c d := by
  90  apply Quotient.sound
  91  show a + d = c + b
  92  exact h
  93
  94/-! ## 3. Embedding LogicNat into LogicInt -/
  95
  96/-- The natural injection `LogicNat ↪ LogicInt` sending `n` to `[n, 0]`.
  97This is the inclusion of the additive monoid into its Grothendieck group. -/
  98def ofLogicNat (n : LogicNat) : LogicInt := mk n LogicNat.zero
  99
 100@[simp] theorem ofLogicNat_zero : ofLogicNat LogicNat.zero = mk LogicNat.zero LogicNat.zero := rfl
 101
 102/-! ## 4. Zero, One, Negation, Addition, Multiplication -/
 103
 104/-- Zero in `LogicInt`. -/
 105def zero : LogicInt := mk LogicNat.zero LogicNat.zero
 106
 107/-- One in `LogicInt`. -/
 108def one : LogicInt := mk (LogicNat.succ LogicNat.zero) LogicNat.zero
 109
 110instance : Zero LogicInt := ⟨zero⟩
 111instance : One LogicInt := ⟨one⟩
 112
 113/-- Negation: `-(a, b) = (b, a)`. -/
 114def neg : LogicInt → LogicInt :=
 115  Quotient.lift (fun (p : LogicNat × LogicNat) => mk p.2 p.1) (by
 116    rintro ⟨a, b⟩ ⟨c, d⟩ h
 117    show mk b a = mk d c
 118    apply sound
 119    show b + c = d + a
 120    rw [eq_iff_toNat_eq, toNat_add, toNat_add]
 121    have h' : toNat a + toNat d = toNat c + toNat b := by
 122      have := congrArg toNat (show a + d = c + b from h)
 123      rwa [toNat_add, toNat_add] at this
 124    omega)
 125
 126instance : Neg LogicInt := ⟨neg⟩
 127
 128/-- Addition: `(a, b) + (c, d) = (a + c, b + d)`. -/
 129def add : LogicInt → LogicInt → LogicInt :=
 130  Quotient.lift₂
 131    (fun (p q : LogicNat × LogicNat) => mk (p.1 + q.1) (p.2 + q.2))
 132    (by
 133      rintro ⟨a, b⟩ ⟨c, d⟩ ⟨a', b'⟩ ⟨c', d'⟩ hab hcd
 134      show mk (a + c) (b + d) = mk (a' + c') (b' + d')
 135      apply sound
 136      show (a + c) + (b' + d') = (a' + c') + (b + d)
 137      rw [eq_iff_toNat_eq, toNat_add, toNat_add, toNat_add, toNat_add, toNat_add, toNat_add]
 138      have hab_nat : toNat a + toNat b' = toNat a' + toNat b := by
 139        have := congrArg toNat (show a + b' = a' + b from hab)
 140        rwa [toNat_add, toNat_add] at this
 141      have hcd_nat : toNat c + toNat d' = toNat c' + toNat d := by
 142        have := congrArg toNat (show c + d' = c' + d from hcd)
 143        rwa [toNat_add, toNat_add] at this
 144      omega)
 145
 146instance : Add LogicInt := ⟨add⟩
 147
 148/-- Multiplication: `(a, b) * (c, d) = (ac + bd, ad + bc)`. -/
 149def mul : LogicInt → LogicInt → LogicInt :=
 150  Quotient.lift₂
 151    (fun (p q : LogicNat × LogicNat) =>
 152       mk (p.1 * q.1 + p.2 * q.2) (p.1 * q.2 + p.2 * q.1))
 153    (by
 154      rintro ⟨a, b⟩ ⟨c, d⟩ ⟨a', b'⟩ ⟨c', d'⟩ hab hcd
 155      show mk (a * c + b * d) (a * d + b * c) = mk (a' * c' + b' * d') (a' * d' + b' * c')
 156      apply sound
 157      show (a * c + b * d) + (a' * d' + b' * c') = (a' * c' + b' * d') + (a * d + b * c)
 158      rw [eq_iff_toNat_eq]
 159      simp only [toNat_add, toNat_mul]
 160      have hab_nat : toNat a + toNat b' = toNat a' + toNat b := by
 161        have := congrArg toNat (show a + b' = a' + b from hab)
 162        rwa [toNat_add, toNat_add] at this
 163      have hcd_nat : toNat c + toNat d' = toNat c' + toNat d := by
 164        have := congrArg toNat (show c + d' = c' + d from hcd)
 165        rwa [toNat_add, toNat_add] at this
 166      -- The Nat goal is a polynomial identity that follows from hab_nat and hcd_nat.
 167      nlinarith [hab_nat, hcd_nat, sq_nonneg ((toNat a : Int) - toNat a'),
 168                 Nat.zero_le (toNat a), Nat.zero_le (toNat b),
 169                 Nat.zero_le (toNat c), Nat.zero_le (toNat d),
 170                 Nat.zero_le (toNat a'), Nat.zero_le (toNat b'),
 171                 Nat.zero_le (toNat c'), Nat.zero_le (toNat d')])
 172
 173instance : Mul LogicInt := ⟨mul⟩
 174
 175/-! ## 5. Recovery Theorem: LogicInt ≃ Int -/
 176
 177/-- Map a pair `(a, b) : LogicNat × LogicNat` to `a - b : Int` via the
 178underlying `Nat` representation. Well-defined on the quotient because
 179`a + d = c + b` implies `(a : Int) - b = (c : Int) - d`. -/
 180def toIntCore : LogicNat × LogicNat → Int :=
 181  fun p => (toNat p.1 : Int) - (toNat p.2 : Int)
 182
 183theorem toIntCore_respects :
 184    ∀ p q : LogicNat × LogicNat, p ≈ q → toIntCore p = toIntCore q := by
 185  rintro ⟨a, b⟩ ⟨c, d⟩ h
 186  -- h : a + d = c + b
 187  show (toNat a : Int) - toNat b = (toNat c : Int) - toNat d
 188  have hcast := congrArg toNat h
 189  rw [toNat_add, toNat_add] at hcast
 190  -- toNat a + toNat d = toNat c + toNat b in Nat.
 191  -- In Int: (toNat a) + (toNat d) = (toNat c) + (toNat b), so subtract to get the goal.
 192  have : (toNat a : Int) + toNat d = (toNat c : Int) + toNat b := by exact_mod_cast hcast
 193  linarith
 194
 195/-- The recovery map `LogicInt → Int`. -/
 196def toInt : LogicInt → Int := Quotient.lift toIntCore toIntCore_respects
 197
 198/-- The inverse `Int → LogicInt`. Maps non-negative `n ≥ 0` to `[n, 0]`
 199and negative `-n < 0` to `[0, n]`. -/
 200def fromInt : Int → LogicInt
 201  | Int.ofNat n   => mk (LogicNat.fromNat n) LogicNat.zero
 202  | Int.negSucc n => mk LogicNat.zero (LogicNat.fromNat (Nat.succ n))
 203
 204@[simp] theorem toInt_mk (a b : LogicNat) :
 205    toInt (mk a b) = (toNat a : Int) - toNat b := rfl
 206
 207theorem toInt_fromInt : ∀ n : Int, toInt (fromInt n) = n := by
 208  intro n
 209  cases n with
 210  | ofNat n =>
 211    show toInt (mk (LogicNat.fromNat n) LogicNat.zero) = (Int.ofNat n)
 212    rw [toInt_mk, toNat_fromNat, toNat_zero]
 213    simp [Int.ofNat]
 214  | negSucc n =>
 215    show toInt (mk LogicNat.zero (LogicNat.fromNat (Nat.succ n))) = Int.negSucc n
 216    rw [toInt_mk, toNat_zero, toNat_fromNat]
 217    simp [Int.negSucc_eq]
 218
 219theorem fromInt_toInt : ∀ z : LogicInt, fromInt (toInt z) = z := by
 220  intro z
 221  induction z using Quotient.inductionOn with
 222  | h p =>
 223    rcases p with ⟨a, b⟩
 224    show fromInt (toInt (mk a b)) = mk a b
 225    rw [toInt_mk]
 226    -- (toNat a : Int) - toNat b. Case on sign.
 227    by_cases h : toNat b ≤ toNat a
 228    · -- Non-negative case
 229      have hge : (0 : Int) ≤ (toNat a : Int) - toNat b := by
 230        have : (toNat b : Int) ≤ toNat a := by exact_mod_cast h
 231        linarith
 232      obtain ⟨k, hk⟩ := Int.eq_ofNat_of_zero_le hge
 233      rw [hk]
 234      show fromInt (Int.ofNat k) = mk a b
 235      show mk (LogicNat.fromNat k) LogicNat.zero = mk a b
 236      apply sound
 237      -- LogicNat.fromNat k + b = a + 0 = a in LogicNat.
 238      -- We have: (toNat a : Int) - toNat b = k as Int, so toNat a = toNat b + k in Nat.
 239      have hknat : (k : Int) = (toNat a : Int) - toNat b := hk.symm
 240      have hknat' : toNat a = toNat b + k := by
 241        have : (toNat a : Int) = toNat b + k := by linarith
 242        exact_mod_cast this
 243      show LogicNat.fromNat k + b = a + LogicNat.zero
 244      rw [LogicNat.add_zero]
 245      have hcast := congrArg fromNat hknat'
 246      rw [LogicNat.fromNat_toNat] at hcast
 247      -- hcast : a = fromNat (toNat b + k)
 248      -- We need: fromNat k + b = a
 249      have : LogicNat.fromNat (toNat b + k) = LogicNat.fromNat (toNat b) + LogicNat.fromNat k := by
 250        -- fromNat is an additive homomorphism. Prove directly.
 251        have hh : toNat (LogicNat.fromNat (toNat b) + LogicNat.fromNat k)
 252                  = toNat b + k := by
 253          rw [LogicNat.toNat_add, LogicNat.toNat_fromNat, LogicNat.toNat_fromNat]
 254        have := congrArg LogicNat.fromNat hh
 255        rw [LogicNat.fromNat_toNat] at this
 256        exact this.symm
 257      rw [hcast, this, LogicNat.fromNat_toNat, LogicNat.add_comm]
 258    · -- Negative case
 259      push_neg at h
 260      have hlt : (toNat a : Int) < toNat b := by exact_mod_cast h
 261      have hltz : (toNat a : Int) - toNat b < 0 := by linarith
 262      have hsub_pos : 0 < toNat b - toNat a := Nat.sub_pos_of_lt h
 263      -- (toNat a : Int) - toNat b = -(toNat b - toNat a) and is Int.negSucc of (toNat b - toNat a - 1).
 264      set m := toNat b - toNat a - 1 with hm_def
 265      have hsucc : Nat.succ m = toNat b - toNat a := by
 266        rw [hm_def]
 267        omega
 268      have heq : (toNat a : Int) - toNat b = Int.negSucc m := by
 269        rw [Int.negSucc_eq]
 270        have h1 : ((Nat.succ m : Int)) = (toNat b - toNat a : Int) := by
 271          rw [hsucc]
 272          push_cast
 273          omega
 274        push_cast at h1
 275        linarith
 276      rw [heq]
 277      show fromInt (Int.negSucc m) = mk a b
 278      show mk LogicNat.zero (LogicNat.fromNat (Nat.succ m)) = mk a b
 279      apply sound
 280      -- Want: 0 + b = a + fromNat (succ m), i.e. b = a + fromNat (succ m).
 281      show LogicNat.zero + b = a + LogicNat.fromNat (Nat.succ m)
 282      rw [LogicNat.zero_add]
 283      -- toNat b = toNat a + Nat.succ m by hsucc.
 284      have hbnat : toNat b = toNat a + Nat.succ m := by
 285        rw [hsucc]; omega
 286      have hcast := congrArg LogicNat.fromNat hbnat
 287      rw [LogicNat.fromNat_toNat] at hcast
 288      have hadd_morph : LogicNat.fromNat (toNat a + Nat.succ m)
 289                        = LogicNat.fromNat (toNat a) + LogicNat.fromNat (Nat.succ m) := by
 290        have hh : toNat (LogicNat.fromNat (toNat a) + LogicNat.fromNat (Nat.succ m))
 291                  = toNat a + Nat.succ m := by
 292          rw [LogicNat.toNat_add, LogicNat.toNat_fromNat, LogicNat.toNat_fromNat]
 293        have := congrArg LogicNat.fromNat hh
 294        rw [LogicNat.fromNat_toNat] at this
 295        exact this.symm
 296      rw [hcast, hadd_morph, LogicNat.fromNat_toNat]
 297
 298/-- **Recovery theorem (carrier)**: `LogicInt` and `Int` are in
 299bijection via `toInt` and `fromInt`. -/
 300def equivInt : LogicInt ≃ Int where
 301  toFun := toInt
 302  invFun := fromInt
 303  left_inv := fromInt_toInt
 304  right_inv := toInt_fromInt
 305
 306/-! ## 6. Ring-Homomorphism Properties of `toInt`
 307
 308The maps `toInt` and `fromInt` extend to a ring isomorphism
 309`LogicInt ≃+* Int`. We prove the homomorphism theorems on the
 310operations and use them, plus a transfer principle, to derive the
 311full ring structure on `LogicInt`. -/
 312
 313theorem toInt_zero : toInt (0 : LogicInt) = 0 := by
 314  show toInt (mk LogicNat.zero LogicNat.zero) = 0
 315  rw [toInt_mk]
 316  simp [toNat_zero]
 317
 318theorem toInt_one : toInt (1 : LogicInt) = 1 := by
 319  show toInt (mk (LogicNat.succ LogicNat.zero) LogicNat.zero) = 1
 320  rw [toInt_mk, toNat_succ, toNat_zero]
 321  norm_num
 322
 323theorem toInt_add (a b : LogicInt) : toInt (a + b) = toInt a + toInt b := by
 324  induction a using Quotient.inductionOn with
 325  | h p =>
 326    induction b using Quotient.inductionOn with
 327    | h q =>
 328      rcases p with ⟨a, b⟩
 329      rcases q with ⟨c, d⟩
 330      show toInt (mk (a + c) (b + d)) = toInt (mk a b) + toInt (mk c d)
 331      rw [toInt_mk, toInt_mk, toInt_mk]
 332      rw [toNat_add, toNat_add]
 333      push_cast
 334      ring
 335
 336theorem toInt_neg (a : LogicInt) : toInt (-a) = -toInt a := by
 337  induction a using Quotient.inductionOn with
 338  | h p =>
 339    rcases p with ⟨a, b⟩
 340    show toInt (mk b a) = -toInt (mk a b)
 341    rw [toInt_mk, toInt_mk]
 342    ring
 343
 344theorem toInt_mul (a b : LogicInt) : toInt (a * b) = toInt a * toInt b := by
 345  induction a using Quotient.inductionOn with
 346  | h p =>
 347    induction b using Quotient.inductionOn with
 348    | h q =>
 349      rcases p with ⟨a, b⟩
 350      rcases q with ⟨c, d⟩
 351      show toInt (mk (a * c + b * d) (a * d + b * c)) = toInt (mk a b) * toInt (mk c d)
 352      rw [toInt_mk, toInt_mk, toInt_mk]
 353      rw [toNat_add, toNat_add, toNat_mul, toNat_mul, toNat_mul, toNat_mul]
 354      push_cast
 355      ring
 356
 357/-- Transfer principle: an equation in `LogicInt` holds iff it holds
 358under `toInt`. The workhorse for proving ring identities on
 359`LogicInt` by reduction to `Int`. -/
 360theorem eq_iff_toInt_eq {a b : LogicInt} : a = b ↔ toInt a = toInt b := by
 361  constructor
 362  · exact congrArg toInt
 363  · intro h
 364    have := congrArg fromInt h
 365    rw [fromInt_toInt, fromInt_toInt] at this
 366    exact this
 367
 368/-! ## 7. Ring Axioms on `LogicInt`
 369
 370By transfer through `toInt`, every ring identity on `LogicInt`
 371reduces to one on `Int` and is closed by `ring`. -/
 372
 373theorem add_assoc' (a b c : LogicInt) : (a + b) + c = a + (b + c) := by
 374  rw [eq_iff_toInt_eq, toInt_add, toInt_add, toInt_add, toInt_add]; ring
 375
 376theorem add_comm' (a b : LogicInt) : a + b = b + a := by
 377  rw [eq_iff_toInt_eq, toInt_add, toInt_add]; ring
 378
 379theorem zero_add' (a : LogicInt) : (0 : LogicInt) + a = a := by
 380  rw [eq_iff_toInt_eq, toInt_add, toInt_zero]; ring
 381
 382theorem add_zero' (a : LogicInt) : a + (0 : LogicInt) = a := by
 383  rw [eq_iff_toInt_eq, toInt_add, toInt_zero]; ring
 384
 385theorem add_left_neg' (a : LogicInt) : -a + a = 0 := by
 386  rw [eq_iff_toInt_eq, toInt_add, toInt_neg, toInt_zero]; ring
 387
 388theorem mul_assoc' (a b c : LogicInt) : (a * b) * c = a * (b * c) := by
 389  rw [eq_iff_toInt_eq, toInt_mul, toInt_mul, toInt_mul, toInt_mul]; ring
 390
 391theorem mul_comm' (a b : LogicInt) : a * b = b * a := by
 392  rw [eq_iff_toInt_eq, toInt_mul, toInt_mul]; ring
 393
 394theorem one_mul' (a : LogicInt) : (1 : LogicInt) * a = a := by
 395  rw [eq_iff_toInt_eq, toInt_mul, toInt_one]; ring
 396
 397theorem mul_one' (a : LogicInt) : a * (1 : LogicInt) = a := by
 398  rw [eq_iff_toInt_eq, toInt_mul, toInt_one]; ring
 399
 400theorem mul_add' (a b c : LogicInt) : a * (b + c) = a * b + a * c := by
 401  rw [eq_iff_toInt_eq, toInt_mul, toInt_add, toInt_add, toInt_mul, toInt_mul]; ring
 402
 403theorem add_mul' (a b c : LogicInt) : (a + b) * c = a * c + b * c := by
 404  rw [eq_iff_toInt_eq, toInt_mul, toInt_add, toInt_add, toInt_mul, toInt_mul]; ring
 405
 406/-- `LogicInt` has no zero divisors: from `a * b = 0`, either `a = 0`
 407or `b = 0`. Forced by the ring isomorphism with `Int`. -/
 408theorem mul_eq_zero {a b : LogicInt} : a * b = 0 ↔ a = 0 ∨ b = 0 := by
 409  constructor
 410  · intro h
 411    have hint : toInt a * toInt b = 0 := by
 412      rw [← toInt_mul]
 413      have := congrArg toInt h
 414      rwa [toInt_zero] at this
 415    rcases Int.mul_eq_zero.mp hint with ha | hb
 416    · left
 417      rw [eq_iff_toInt_eq, toInt_zero]; exact ha
 418    · right
 419      rw [eq_iff_toInt_eq, toInt_zero]; exact hb
 420  · rintro (ha | hb)
 421    · rw [ha, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring
 422    · rw [hb, eq_iff_toInt_eq, toInt_mul, toInt_zero]; ring
 423
 424/-- Cancellation: if `c ≠ 0` and `a * c = b * c`, then `a = b`. -/
 425theorem mul_right_cancel {a b c : LogicInt} (hc : c ≠ 0) (h : a * c = b * c) : a = b := by
 426  have hc' : toInt c ≠ 0 := by
 427    intro habs
 428    apply hc
 429    rw [eq_iff_toInt_eq, toInt_zero]; exact habs
 430  rw [eq_iff_toInt_eq, toInt_mul, toInt_mul] at h
 431  rw [eq_iff_toInt_eq]
 432  exact Int.eq_of_mul_eq_mul_right hc' h
 433
 434end LogicInt
 435
 436/-! ## Summary
 437
 438  Foundation.LogicAsFunctionalEquation     (Law of Logic)
 439        ↓
 440  Foundation.ArithmeticFromLogic           (LogicNat ≃ Nat)
 441        ↓
 442  Foundation.IntegersFromLogic (this)      (LogicInt ≃ Int)
 443
 444The Grothendieck completion of `LogicNat` recovers the integers. The
 445construction does not assume `Int` exists; it builds the equivalence
 446classes and operations from `LogicNat` plus the standard quotient
 447machinery.
 448
 449What this module establishes:
 450  - The Grothendieck equivalence relation and its setoid.
 451  - `LogicInt` as a Quotient.
 452  - Zero, one, negation, addition, multiplication.
 453  - Carrier-level equivalence with `Int`.
 454
 455What is left for a follow-up:
 456  - Full ring axiom catalog (associativity, distributivity, etc.) on `LogicInt`.
 457  - Equivalence as a ring isomorphism `LogicInt ≃+* Int`.
 458  - Order on `LogicInt` (descended from `Int`'s order).
 459-/
 460
 461end IntegersFromLogic
 462end Foundation
 463end IndisputableMonolith
 464