Foundation Primitive Recognition Calculus Orbit Arithmetic

Orbit arithmetic

Orbit arithmetic is the arithmetic of counting repetitions in a discrete ledger. A ledger, a discrete record of events, has positions: zero, one more, one more again. The framework Recognition Science builds its counting from this idea, and the resulting arithmetic is ordinary arithmetic. Addition is concatenation of repetition: three repetitions followed by two repetitions is five repetitions. Multiplication is nested repetition: two repetitions of three repetitions is six repetitions. These are the familiar operations, rebuilt from the primitive act of distinguishing one thing from another.

The classical facts come first. The natural numbers, 0, 1, 2, 3, ..., are the counting numbers. Addition and multiplication on them satisfy the standard laws: a + b = b + a, (a + b) + c = a + (b + c), a * b = b * a, and so on. These laws are the algebraic backbone of arithmetic. The framework's orbit positions, written DistinctionNat, are a formal copy of the natural numbers. The copy obeys the same laws: addition is commutative and associative, multiplication is commutative, and zero and one behave as identities. The proofs are machine-checked, meaning a computer program has verified every step.

The key result is that the orbit positions are not just similar to the natural numbers; they are the same structure. A translation from orbit positions to natural numbers preserves addition and multiplication. This means the verifier display of orbit arithmetic matches ordinary arithmetic exactly. The translation is also injective: if two orbit positions display the same natural number, they are the same position. So the framework's primitive counting does not introduce a new arithmetic; it recovers the arithmetic we already know.

In Recognition Science, this work is a foundation stone. The framework aims to derive physical structure from a ledger of recognition events. Before it can talk about scales, cycles, or dimensions, it must show that its primitive counting behaves correctly. This establishes that the most basic operation, counting repetitions, is sound. The consequence is that everything built on this counting can use ordinary arithmetic without fear of a hidden inconsistency. The framework's ledger does not reinvent arithmetic; it inherits it.

One notable property is cancellation. If a + b = a + c, then b = c; if a * b is nonzero and a is nonzero, then b is nonzero. These are standard facts about natural numbers, and the orbit positions also have them. They matter because they ensure that the ledger's arithmetic is well-behaved: no two different positions collapse into the same sum, and no nonzero product vanishes. This is the kind of solid ground a larger theory needs.

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

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

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]

theorem mul_comm (a b : DistinctionNat) :
    a * b = b * a := by
  induction a with
  | zero =>
      rw [zero_mul_eq, mul_zero_eq]
  | succ n ih =>
      rw [succ_mul_eq, mul_succ_eq, ih]

/-- The verifier display is injective: equal Nat displays come from equal
orbit positions. -/
theorem toNat_inj {a b : DistinctionNat} (h : a.toNat = b.toNat) :
    a = b := by
  have := congrArg DistinctionNat.ofNat h
  rwa [ofNat_toNat, ofNat_toNat] at this

What this page does not claim

This module does not define subtraction or division on orbit positions. This module does not connect orbit arithmetic to any physical constant or dimension. The framework's full derivation of natural numbers from recognition is not established in this module alone.

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: