Foundation Integers From Logic Mul Right Cancel

The cancellation law

The integers are the familiar whole numbers: ..., -2, -1, 0, 1, 2, .... The Recognition Science framework builds its own version of them, called LogicInt, from a discrete record of counting events, and it proves that this version obeys the same cancellation law as ordinary arithmetic. The law says that if a times b equals a times c, then b equals c, as long as a is not zero. In symbols: if a * b = a * c and a ≠ 0, then b = c.

The framework constructs LogicInt as pairs of natural numbers (a, b) that represent a - b, with two pairs equivalent when their cross-sums agree: (a, b) ~ (c, d) iff a + d = c + b. This is the classical Grothendieck construction, the standard way to build the integers from the natural numbers. The machine-checked library proves the cancellation law for this construction, along with the other ring laws: commutativity of addition and multiplication, the identity laws, and the distributive law. Each proof is checked by the framework's formal library, a machine-checked collection of formal theorems, so the result is not a matter of hand-waving.

The cancellation law is a test of whether the construction is sound. If the framework's LogicInt did not satisfy it, the construction would be broken, because cancellation is essential to solving equations like a * x = a * y. The proof that it holds means the construction behaves like the integers should: it is a genuine ring, not a defective imitation. This is one of the foundational steps that lets the framework claim its integers are the real thing.

What the declaration does not claim is equally important. It does not claim that the cancellation law is true for all numbers in every context; it is a theorem about LogicInt specifically, proved from the framework's definitions. It does not claim that the framework's construction is the only way to build the integers, or that it is simpler than the standard one. It does not claim that the integers themselves are somehow created by the framework; they are a mathematical object that the framework models, not invents. The declaration is a precise, local result: for this construction, cancellation holds.

The practical consequence is that the framework's integers can be used with confidence in further proofs. When a later theorem needs to cancel a common factor, it can cite this law instead of re-proving it. The cancellation law is a small but necessary brick in the foundation; without it, the whole edifice would be unstable.

/-- 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')])

/-- `LogicInt` is the Grothendieck completion of `LogicNat` under
addition. -/
def LogicInt : Type := Quotient (setoid : Setoid (LogicNat × LogicNat))

/-- 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

/-- 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

This answer does not claim that the cancellation law holds for all numbers in every context. This answer does not claim that the framework's construction of the integers is the only possible one. This answer does not claim that the integers are created by the framework rather than modeled by it.

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: