Encyclopedia Foundation Foundation Integers From Logic Le Relation Unique

ARTICLE 3 claims 2 theorems 1 model

Foundation Integers From Logic Le Relation Unique

The integers can be built from pairs of counting numbers; a machine-checked proof shows their ordering is the only one possible.

Verify this page

One ordering, no alternatives

The integers, the familiar line of whole numbers that extends forever in both directions, can be constructed from the natural numbers alone. The classical trick is to take ordered pairs of natural numbers, such as (5, 2), and declare two pairs equivalent when their cross-sums match: (5, 2) and (7, 4) both represent the difference 5 − 2 = 7 − 4 = 3. The negative numbers appear as pairs like (2, 5), which stands for 2 − 5 = −3. This construction, named for the mathematician Alexander Grothendieck, turns subtraction into a defined operation instead of a partial one.

The Recognition Science framework carries this construction into its own formal language. Its ledger, a discrete record of events with no gaps, provides the natural numbers; the Grothendieck construction then yields the integers, called LogicInt. The framework's machine-checked library of formal theorems proves that this construction is faithful: every LogicInt corresponds to exactly one ordinary integer, and the usual operations of addition, multiplication, and negation behave as expected.

Among these theorems is le_relation_unique. It states that the ordering on LogicInt is unique: if any relation r on pairs of LogicInt agrees with the standard ordering, meaning r a b holds exactly when a is less than or equal to b, then r must be that standard ordering. In symbols, if for all a and b, r a b is equivalent to toInt a ≤ toInt b, then r equals le. The proof is short and direct: it uses the fact that two relations are equal when they agree on every pair, and that two logical statements are equal when they imply each other.

The theorem does not claim that the integers are the only way to extend the natural numbers, nor that the ordering is the only relation one could define. It says only that within this particular construction, once the standard ordering is specified, no other relation can agree with it everywhere and differ somewhere. The uniqueness is a property of the construction, not a statement about all possible number systems.

What this means in practice is that the framework's integers are not ambiguous. When a later theorem uses the ordering on LogicInt, it refers to a unique, well-defined relation. This is a small but necessary step in building a foundation where every concept has a single, fixed meaning.

THEOREM le_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
MODEL intRel · IndisputableMonolith/Foundation/IntegersFromLogic.lean
intRel · IndisputableMonolith/Foundation/IntegersFromLogic.lean:39 
/-- The Grothendieck equivalence relation on pairs of `LogicNat`:
`(a, b) ~ (c, d)` iff `a + d = c + b`. The pair `(a, b)` represents
the formal difference `a - b`. -/
def intRel : (LogicNat × LogicNat) → (LogicNat × LogicNat) → Prop :=
  fun p q => p.1 + q.2 = q.1 + p.2
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]

What this page does not claim

The theorem does not claim that the integers are the only extension of the natural numbers. It does not claim that the ordering is the only relation one could define on LogicInt. It does not claim that the Grothendieck construction is the only way to build integers from natural numbers.

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