Foundation Primitive Recognition Calculus Orbit Arithmetic Add Left Cancel

Left cancellation on the orbit

The declaration add_left_cancel proves a basic property of addition for a structure called the δ-orbit, which is the framework's primitive model of counting. The theorem states that if a + b = a + c, then b = c. In plain language, when two sums share the same left addend and are equal, the right addends must be equal as well. This is the left cancellation law, a property that holds for natural numbers and that the framework derives for its own counting structure rather than assuming it.

The δ-orbit is built from a starting point called zero and a successor operation that moves to the next position. Addition on this orbit is defined as concatenation of repetition: a + b means repeating the act of moving from a, b times. The framework's machine-checked library of formal theorems proves this addition is commutative and associative, and then proves cancellation. The proof of left cancellation works by translating orbit positions to ordinary natural numbers, using the fact that the translation is injective and that natural number addition already satisfies cancellation.

In Recognition Science, this result is part of a larger effort to show that the structure of counting, and eventually more of mathematics, can be derived from a ledger of recognition events, a discrete record of distinctions. The theorem is a small but necessary step: it confirms that the orbit's addition behaves like the addition everyone learns in school, so that later constructions built on it inherit familiar algebraic properties. It is a formal guarantee, checked by the machine, that the primitive counting structure does not introduce unexpected behavior.

The declaration does not claim that the δ-orbit is the only way to model counting, nor does it claim that cancellation holds for any other operation defined on the orbit. It does not assert that the orbit itself is the natural numbers; it only shows that a translation exists that preserves addition. The theorem is specific to the addition operation as defined, and its proof relies on the corresponding property for natural numbers, which is already established in the underlying logic.

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

/-- K4.5. Addition of orbit positions: concatenation of repetition. -/
def add : DistinctionNat → DistinctionNat → DistinctionNat
  | a, zero => a
  | a, succ b => succ (add a b)

/-- 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 δ-orbit is not claimed to be identical to the natural numbers, only that a translation preserving addition exists. The theorem does not claim cancellation holds for any operation other than addition as defined on the orbit. The framework does not claim that the δ-orbit is the only possible primitive model of counting.

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: