Encyclopedia Foundation Foundation Integers From Logic From Int To Int

ARTICLE 3 claims 2 theorems 1 model

Foundation Integers From Logic From Int To Int

A machine-checked proof that the integers built from pairs of natural numbers are exactly the familiar integers, and that the conversion goes both ways without loss.

Verify this page

The round-trip theorem

The integers are the whole numbers ..., -2, -1, 0, 1, 2, ... . One standard way to build them from the natural numbers 0, 1, 2, ... is to take ordered pairs (a, b) and think of the pair as the difference a - b. The pair (5, 2) stands for 3, and the pair (2, 5) stands for -3. Two pairs (a, b) and (c, d) name the same integer when a + d = c + b, a condition called the Grothendieck equivalence. This construction is classical, taught in algebra courses as the formal way to introduce negative numbers.

The Recognition Science framework's machine-checked library of formal theorems implements this construction and proves a round-trip property. The declaration fromInt_toInt states that for every LogicInt z, converting to the ordinary integers and back returns the original z. The framework models LogicInt as the quotient of pairs under the Grothendieck equivalence, and toInt maps each class to its standard integer representative. The theorem says the two views agree perfectly: no information is lost in either direction. This is a THEOREM, verified by the framework's kernel with no additional axioms.

The theorem also shows the ordering and arithmetic behave as expected. The framework proves that the less-than relation on LogicInt matches the usual order on integers, and that addition, multiplication, and negation respect the equivalence. These properties are not assumed; they follow from the definitions. The round-trip theorem is the hinge: it guarantees that the abstract construction and the familiar integers are interchangeable in every formal argument.

What the theorem does not claim is broader. It does not say that the integers are the only number system, nor that this construction is the simplest or most efficient. It does not assert anything about the physical world or about how recognition events relate to arithmetic. The theorem is a statement about a formal construction inside the framework's library, not a claim about external reality. Its value is internal: it certifies that the framework's integer object is faithful to the standard one.

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]
MODEL LogicInt · IndisputableMonolith/Foundation/IntegersFromLogic.lean
LogicInt · IndisputableMonolith/Foundation/IntegersFromLogic.lean:75 
/-- `LogicInt` is the Grothendieck completion of `LogicNat` under
addition. -/
def LogicInt : Type := Quotient (setoid : Setoid (LogicNat × LogicNat))
THEOREM toInt_le · IndisputableMonolith/Foundation/IntegersFromLogic.lean
toInt_le · IndisputableMonolith/Foundation/IntegersFromLogic.lean:383 
/-- The pulled-back non-strict order transports exactly to `Int`. -/
@[simp] theorem toInt_le (a b : LogicInt) :
    a ≤ b ↔ toInt a ≤ toInt b :=
  Iff.rfl

What this page does not claim

The theorem does not claim that integers are the only number system. It does not assert anything about the physical world or recognition events. It does not claim this construction is the simplest or most efficient way to define integers.

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