Encyclopedia Foundation Foundation Integers From Logic To Int Core Respects

ARTICLE 3 claims 3 theorems

Foundation Integers From Logic To Int Core Respects

A machine-checked proof that the formal difference of two counting numbers is a genuine integer, no matter how the pair is represented.

Verify this page

The well-defined map

The integers are the numbers we get by allowing subtraction to always work: 3 minus 5 is the integer -2, even though no counting number gives that answer. A standard way to build them is to take pairs of counting numbers and declare two pairs equivalent when their cross-sums match, so (3, 5) and (1, 3) both represent -2 because 3 + 3 = 5 + 1. The declaration toIntCore_respects is the formal guarantee that this identification is coherent: it proves that the map sending a pair (a, b) to the integer a - b gives the same answer for any two equivalent pairs.

This matters because a map defined on pairs must be checked before it can be used on the equivalence classes. The framework's machine-checked library of formal theorems records this check as a theorem, not as an assumption. The proof is short: it uses the defining relation a + d = c + b and the ordinary arithmetic of integers to show a - b = c - d. With this theorem in hand, the library can define the translation from its own integer type to the standard integer type, and then prove that the translation is a bijection, meaning every framework integer corresponds to exactly one ordinary integer and vice versa.

The declaration also underpins the order structure. Once the map is known to be well-defined, the library defines less-than and less-or-equal on its integers by comparing their images in the ordinary integers, and proves that these relations are unique: any relation that agrees with the ordinary order must be exactly the one defined. This gives the framework integers the same ordering properties as the ordinary integers, with the same theorems about reflexivity, transitivity, and the trichotomy law.

What the declaration does not claim is just as important. It does not assert that the framework's integers are the only way to build integers, nor does it say anything about the physical world. It is a piece of pure mathematics: a proof that a particular construction is consistent. The framework's broader claims about physics rest on other theorems, not on this one. This declaration is a load-bearing but local result, one small step in showing that the framework's logical foundations reproduce the standard number systems.

THEOREM toIntCore · IndisputableMonolith/Foundation/IntegersFromLogic.lean
toIntCore · IndisputableMonolith/Foundation/IntegersFromLogic.lean:177 
/-- Map a pair `(a, b) : LogicNat × LogicNat` to `a - b : Int` via the
underlying `Nat` representation. Well-defined on the quotient because
`a + d = c + b` implies `(a : Int) - b = (c : Int) - d`. -/
def toIntCore : LogicNat × LogicNat → Int :=
  fun p => (toNat p.1 : Int) - (toNat p.2 : Int)
THEOREM fromInt_toInt · IndisputableMonolith/Foundation/IntegersFromLogic.lean
fromInt_toInt · IndisputableMonolith/Foundation/IntegersFromLogic.lean:219 
theorem fromInt_toInt : ∀ z : LogicInt, fromInt (toInt z) = z := by
  intro z
  induction z using Quotient.inductionOn with
  | h p =>
    rcases p with ⟨a, b⟩
    show fromInt (toInt (mk a b)) = mk a b
    rw [toInt_mk]
    -- (toNat a : Int) - toNat b. Case on sign.
    by_cases h : toNat b ≤ toNat a
    · -- Non-negative case
      have hge : (0 : Int) ≤ (toNat a : Int) - toNat b := by
        have : (toNat b : Int) ≤ toNat a := by exact_mod_cast h
        linarith
      obtain ⟨k, hk⟩ := Int.eq_ofNat_of_zero_le hge
      rw [hk]
      show fromInt (Int.ofNat k) = mk a b
      show mk (LogicNat.fromNat k) LogicNat.zero = mk a b
      apply sound
      -- LogicNat.fromNat k + b = a + 0 = a in LogicNat.
      -- We have: (toNat a : Int) - toNat b = k as Int, so toNat a = toNat b + k in Nat.
      have hknat : (k : Int) = (toNat a : Int) - toNat b := hk.symm
      have hknat' : toNat a = toNat b + k := by
        have : (toNat a : Int) = toNat b + k := by linarith
        exact_mod_cast this
      show LogicNat.fromNat k + b = a + LogicNat.zero
      rw [LogicNat.add_zero]
      have hcast := congrArg fromNat hknat'
      rw [LogicNat.fromNat_toNat] at hcast
      -- hcast : a = fromNat (toNat b + k)
      -- We need: fromNat k + b = a
      have : LogicNat.fromNat (toNat b + k) = LogicNat.fromNat (toNat b) + LogicNat.fromNat k := by
        -- fromNat is an additive homomorphism. Prove directly.
        have hh : toNat (LogicNat.fromNat (toNat b) + LogicNat.fromNat k)
                  = toNat b + k := by
          rw [LogicNat.toNat_add, LogicNat.toNat_fromNat, LogicNat.toNat_fromNat]
        have := congrArg LogicNat.fromNat hh
        rw [LogicNat.fromNat_toNat] at this
        exact this.symm
      rw [hcast, this, LogicNat.fromNat_toNat, LogicNat.add_comm]
    · -- Negative case
      push_neg at h
      have hlt : (toNat a : Int) < toNat b := by exact_mod_cast h
      have hltz : (toNat a : Int) - toNat b < 0 := by linarith
      have hsub_pos : 0 < toNat b - toNat a := Nat.sub_pos_of_lt h
      -- (toNat a : Int) - toNat b = -(toNat b - toNat a) and is Int.negSucc of (toNat b - toNat a - 1).
      set m := toNat b - toNat a - 1 with hm_def
      have hsucc : Nat.succ m = toNat b - toNat a := by
        rw [hm_def]
        omega
      have heq : (toNat a : Int) - toNat b = Int.negSucc m := by
        rw [Int.negSucc_eq]
        have h1 : ((Nat.succ m : Int)) = (toNat b - toNat a : Int) := by
          rw [hsucc]
          push_cast
          omega
        push_cast at h1
        linarith
      rw [heq]
      show fromInt (Int.negSucc m) = mk a b
      show mk LogicNat.zero (LogicNat.fromNat (Nat.succ m)) = mk a b
      apply sound
      -- Want: 0 + b = a + fromNat (succ m), i.e. b = a + fromNat (succ m).
      show LogicNat.zero + b = a + LogicNat.fromNat (Nat.succ m)
      rw [LogicNat.zero_add]
      -- toNat b = toNat a + Nat.succ m by hsucc.
      have hbnat : toNat b = toNat a + Nat.succ m := by
        rw [hsucc]; omega
      have hcast := congrArg LogicNat.fromNat hbnat
      rw [LogicNat.fromNat_toNat] at hcast
      have hadd_morph : LogicNat.fromNat (toNat a + Nat.succ m)
                        = LogicNat.fromNat (toNat a) + LogicNat.fromNat (Nat.succ m) := by
        have hh : toNat (LogicNat.fromNat (toNat a) + LogicNat.fromNat (Nat.succ m))
                  = toNat a + Nat.succ m := by
          rw [LogicNat.toNat_add, LogicNat.toNat_fromNat, LogicNat.toNat_fromNat]
        have := congrArg LogicNat.fromNat hh
        rw [LogicNat.fromNat_toNat] at this
        exact this.symm
      rw [hcast, hadd_morph, LogicNat.fromNat_toNat]
THEOREM le_relation_unique · lt_relation_unique · IndisputableMonolith/Foundation/IntegersFromLogic.lean
le_relation_unique · IndisputableMonolith/Foundation/IntegersFromLogic.lean:393 
/-- Any non-strict relation with the required transport law is the canonical
pulled-back relation. -/
theorem le_relation_unique
    (r : LogicInt → LogicInt → Prop)
    (h : ∀ a b, r a b ↔ toInt a ≤ toInt b) :
    r = le := by
  funext a b
  apply propext
  exact h a b
lt_relation_unique · IndisputableMonolith/Foundation/IntegersFromLogic.lean:403 
/-- Any strict relation with the required transport law is the canonical
pulled-back relation. -/
theorem lt_relation_unique
    (r : LogicInt → LogicInt → Prop)
    (h : ∀ a b, r a b ↔ toInt a < toInt b) :
    r = lt := by
  funext a b
  apply propext
  exact h a b

What this page does not claim

The declaration does not prove that the framework's integers are the only possible construction of the integers. The declaration makes no claim about the physical world or about the framework's physics. The declaration does not by itself establish the full arithmetic structure of the framework's integers, such as commutativity or distributivity.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/IntegersFromLogic.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND