Foundation Primitive Recognition Calculus Orbit Arithmetic Add Right Cancel

Cancellation on the orbit

In ordinary arithmetic, if you have a true equation and add the same number to both sides, the equation stays true. The reverse also holds: if a + c = b + c, then you can cancel the common c and conclude a = b. This property, called right cancellation, is what makes addition a sensible, reversible operation rather than a one-way process that loses information. The Recognition Science declaration add_right_cancel proves exactly this law for its own primitive counting positions, the distinction naturals, which are the framework's basic discrete record of repeated recognition events.

The framework builds these positions from two rules: a starting position called zero, and a successor operation that moves to the next position. Addition is defined as concatenation of repetition: adding b to a means repeating the successor step b times starting from a. On this structure, the theorem states that for any positions a, b, and c, if a + c = b + c, then a = b. The proof is short and mechanical: it translates the equality into the familiar natural numbers, uses the standard cancellation law there, and translates back. The same library also proves the mirror-image left cancellation law, commutativity, associativity, and that the display of these positions matches ordinary counting numbers exactly.

What the declaration does not claim is broader than what it proves. It says nothing about subtraction, division, or any operation beyond addition. It does not assert that the distinction naturals are the only structure with cancellation, nor that they form a complete arithmetic system. It only establishes that the primitive counting positions behave like the natural numbers with respect to adding and removing a common term. That single fact is what lets the framework treat its ledger of recognition events as a reliable arithmetic object: equal totals cannot conceal unequal parts.

/-- K4.5. Right cancellation for orbit addition. -/
theorem add_right_cancel {a b c : DistinctionNat}
    (h : a + c = b + c) : a = b := by
  apply add_left_cancel (a := c)
  rw [add_comm c a, add_comm c b]
  exact h

/-- K4.5. Left cancellation for orbit addition. -/
theorem add_left_cancel {a b c : DistinctionNat}
    (h : a + b = a + c) : b = c := by
  apply toNat_inj
  have h' : (a + b).toNat = (a + c).toNat := by rw [h]
  rw [toNat_add, toNat_add] at h'
  exact Nat.add_left_cancel h'

theorem add_comm (a b : DistinctionNat) :
    a + b = b + a := by
  induction a with
  | zero =>
      rw [zero_add_eq, add_zero_eq]
  | succ n ih =>
      rw [succ_add_eq, add_succ_eq, ih]

theorem add_assoc (a b c : DistinctionNat) :
    (a + b) + c = a + (b + c) := by
  induction c with
  | zero => rfl
  | succ n ih =>
      show (a + b) + succ n = a + (b + succ n)
      rw [add_succ_eq, add_succ_eq, add_succ_eq, ih]

/-- K4.5. The verifier display of orbit addition matches Lean Nat addition. -/
theorem toNat_add (a b : DistinctionNat) :
    (a + b).toNat = a.toNat + b.toNat := by
  induction b with
  | zero =>
      rw [add_zero_eq, toNat_zero, Nat.add_zero]
  | succ n ih =>
      show (succ (a + n)).toNat = a.toNat + (succ n).toNat
      rw [toNat_succ, toNat_succ, ih]
      omega

What this page does not claim

The declaration does not prove subtraction, division, or any operation beyond addition. The declaration does not claim the distinction naturals are the only structure with cancellation. The declaration does not assert that the distinction naturals form a complete ordered arithmetic system.

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/PrimitiveRecognitionCalculus/OrbitArithmetic.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: