Foundation Primitive Recognition Calculus Orbit To Nat Of Nat

The counting bridge

Natural numbers are the everyday counting numbers: zero, one, two, and so on, each built by adding one to the previous. The Recognition Science framework builds its own counting sequence from repeated acts of distinction, where each step marks a new thing as different from all before it. The declaration toNat_ofNat establishes that these two sequences are interchangeable: start with any ordinary natural number, translate it into the framework's distinction sequence, then translate back, and you recover exactly the number you began with. The proof is a simple induction, the same pattern used to show that adding one and subtracting one undo each other.

The declaration is part of a small family of results in the framework's machine-checked library of formal theorems. Its companion ofNat_toNat proves the round trip in the other direction, and together they show the two sequences are equivalent as a verifier display. This matters because the framework wants to talk about counting without depending on a particular notation for numbers; the equivalence lets it borrow the familiar natural numbers whenever a human reader needs to see a count.

What the declaration does not claim is more important than what it does. It does not say that ordinary counting numbers are the same thing as acts of distinction; it only says the two can be translated back and forth without loss. It does not prove that the framework's counting sequence is the only possible one, nor that it matches any physical counting in the world. It is a bridge between two formal systems, not a claim about what counting is.

/-- K4.5. Transport from Lean Nat to the δ-orbit and back is identity. -/
theorem toNat_ofNat (n : Nat) :
    toNat (ofNat n) = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      simp [ofNat, ih]

/-- K4.5. Transport from the δ-orbit to Lean Nat and back is identity. -/
theorem ofNat_toNat (n : DistinctionNat) :
    ofNat (toNat n) = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
      simp [toNat, ih]

/-- K4.5. The δ-orbit is equivalent to Lean Nat as a verifier display. -/
def equivNat : DistinctionNat ≃ Nat where
  toFun := toNat
  invFun := ofNat
  left_inv := ofNat_toNat
  right_inv := toNat_ofNat

What this page does not claim

The declaration does not claim that ordinary counting numbers are identical to acts of distinction. The declaration does not claim that the framework's counting sequence is unique or physically realized. The declaration does not prove any property about addition or multiplication of the distinction sequence.

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/Orbit.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: