Encyclopedia Foundation Foundation Integers From Logic To Int From Int

ARTICLE 4 claims 4 theorems

Foundation Integers From Logic To Int From Int

The theorem toInt_fromInt proves that converting a logic-built integer to a standard one and back again changes nothing.

Verify this page

The round-trip guarantee

Integers are the whole numbers ..., -2, -1, 0, 1, 2, ... . The Recognition Science framework builds them from a discrete record of events, then proves that its construction agrees with the familiar integers. The declaration toInt_fromInt is the round-trip guarantee: it proves that converting a framework integer to a standard integer and then back again returns the original framework integer. In symbols, for every framework integer z, fromInt (toInt z) = z.

The framework constructs its integers as formal differences of counting numbers. A pair (a, b) represents a - b, and two pairs are equivalent when a + d = c + b. This is the Grothendieck construction, a standard method for inventing subtraction where it did not exist. The framework's toInt function maps each such pair to the ordinary integer a - b. The theorem toInt_fromInt proves this map is a bijection onto the standard integers: no two distinct framework integers collapse to the same standard integer, and every standard integer is reached.

In Recognition Science, a ledger is a discrete record of events, and cost is the forced price of recognition. The framework models integers as a ledger of paired counts, and toInt_fromInt proves that this ledger is exactly the integers, not a shadow of them. The theorem also proves that the order relation, addition, and multiplication on framework integers match the standard ones: a < b exactly when toInt a < toInt b, and similarly for addition and multiplication.

The declaration does not claim that the framework invented integers, nor that it explains why integers exist. It claims only that the framework's construction is faithful to the standard integers. The theorem is a bridge, not a discovery: it shows the framework's ledger-based integers are the familiar integers in a new costume. What the framework adds is a proof that this costume is exact, so later results about recognition can use integers without fear of mismatch.

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 toInt_mk · IndisputableMonolith/Foundation/IntegersFromLogic.lean
toInt_mk · IndisputableMonolith/Foundation/IntegersFromLogic.lean:204 
@[simp] theorem toInt_mk (a b : LogicNat) :
    toInt (mk a b) = (toNat a : Int) - toNat b := rfl
THEOREM toInt_lt · IndisputableMonolith/Foundation/IntegersFromLogic.lean
toInt_lt · IndisputableMonolith/Foundation/IntegersFromLogic.lean:388 
/-- The pulled-back strict order transports exactly to `Int`. -/
@[simp] theorem toInt_lt (a b : LogicInt) :
    a < b ↔ toInt a < toInt b :=
  Iff.rfl
THEOREM add · mul · IndisputableMonolith/Foundation/IntegersFromLogic.lean
add · IndisputableMonolith/Foundation/IntegersFromLogic.lean:128 
/-- Addition: `(a, b) + (c, d) = (a + c, b + d)`. -/
def add : LogicInt → LogicInt → LogicInt :=
  Quotient.lift₂
    (fun (p q : LogicNat × LogicNat) => mk (p.1 + q.1) (p.2 + q.2))
    (by
      rintro ⟨a, b⟩ ⟨c, d⟩ ⟨a', b'⟩ ⟨c', d'⟩ hab hcd
      show mk (a + c) (b + d) = mk (a' + c') (b' + d')
      apply sound
      show (a + c) + (b' + d') = (a' + c') + (b + d)
      rw [eq_iff_toNat_eq, toNat_add, toNat_add, toNat_add, toNat_add, toNat_add, toNat_add]
      have hab_nat : toNat a + toNat b' = toNat a' + toNat b := by
        have := congrArg toNat (show a + b' = a' + b from hab)
        rwa [toNat_add, toNat_add] at this
      have hcd_nat : toNat c + toNat d' = toNat c' + toNat d := by
        have := congrArg toNat (show c + d' = c' + d from hcd)
        rwa [toNat_add, toNat_add] at this
      omega)
mul · IndisputableMonolith/Foundation/IntegersFromLogic.lean:148 
/-- Multiplication: `(a, b) * (c, d) = (ac + bd, ad + bc)`. -/
def mul : LogicInt → LogicInt → LogicInt :=
  Quotient.lift₂
    (fun (p q : LogicNat × LogicNat) =>
       mk (p.1 * q.1 + p.2 * q.2) (p.1 * q.2 + p.2 * q.1))
    (by
      rintro ⟨a, b⟩ ⟨c, d⟩ ⟨a', b'⟩ ⟨c', d'⟩ hab hcd
      show mk (a * c + b * d) (a * d + b * c) = mk (a' * c' + b' * d') (a' * d' + b' * c')
      apply sound
      show (a * c + b * d) + (a' * d' + b' * c') = (a' * c' + b' * d') + (a * d + b * c)
      rw [eq_iff_toNat_eq]
      simp only [toNat_add, toNat_mul]
      have hab_nat : toNat a + toNat b' = toNat a' + toNat b := by
        have := congrArg toNat (show a + b' = a' + b from hab)
        rwa [toNat_add, toNat_add] at this
      have hcd_nat : toNat c + toNat d' = toNat c' + toNat d := by
        have := congrArg toNat (show c + d' = c' + d from hcd)
        rwa [toNat_add, toNat_add] at this
      -- The Nat goal is a polynomial identity that follows from hab_nat and hcd_nat.
      nlinarith [hab_nat, hcd_nat, sq_nonneg ((toNat a : Int) - toNat a'),
                 Nat.zero_le (toNat a), Nat.zero_le (toNat b),
                 Nat.zero_le (toNat c), Nat.zero_le (toNat d),
                 Nat.zero_le (toNat a'), Nat.zero_le (toNat b'),
                 Nat.zero_le (toNat c'), Nat.zero_le (toNat d')])

What this page does not claim

The theorem does not claim that the framework invented the integers or that they arise from recognition physics. It does not claim that the framework's construction is the only way to build integers. It does not claim that the framework's integers are physically real; it claims only a formal equivalence.

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