Foundation Integers From Logic Int Rel Trans

The transitivity of integer equivalence

An integer can be built from a pair of natural numbers (a, b), thought of as the formal difference a - b. The pair (3, 1) and the pair (4, 2) both represent the integer 2, because 3 + 2 = 4 + 1. This is the Grothendieck equivalence relation: (a, b) ~ (c, d) iff a + d = c + b. The declaration intRel_trans is the formal proof that this relation is transitive: if (a, b) ~ (c, d) and (c, d) ~ (e, f), then (a, b) ~ (e, f).

The transitivity property is one of three requirements for an equivalence relation, along with reflexivity (a pair is equivalent to itself) and symmetry (if one pair is equivalent to another, the reverse holds). Together, these three properties ensure that the relation partitions all pairs into disjoint classes, each class representing a single integer. The declaration intRel_trans is the machine-checked proof that the third property holds for the specific relation defined by a + d = c + b.

The proof itself is short: it uses the associativity and commutativity of addition on natural numbers. From a + d = c + b and c + f = e + d, one derives a + f = e + b. This is not a new mathematical discovery; it is a formal verification that a familiar property holds for this particular construction. The declaration belongs to the framework's machine-checked library of formal theorems, which builds integers from logic in a way that can be audited step by step.

In Recognition Science, the construction of integers from pairs of natural numbers is part of a larger program: deriving the structures of mathematics and physics from a single logical starting point. The declaration intRel_trans does not, by itself, establish anything about the physical world, nor does it prove that integers exist in any metaphysical sense. It is a precise, formal statement about a mathematical construction, verified by a computer, that provides a foundation for further developments within the framework.

theorem intRel_refl : ∀ p : LogicNat × LogicNat, intRel p p := by
  intro p
  show p.1 + p.2 = p.1 + p.2
  rfl

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

What this page does not claim

The declaration does not prove that integers exist independently of the construction. The declaration does not establish any physical fact about the world. The declaration does not introduce new mathematics; it verifies a standard property of an equivalence relation.

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: