Foundation Primitive Recognition Calculus Orbit

The distinction orbit

The foundation primitive recognition calculus orbit is the simplest possible sequence: a starting point and a rule for taking one more step. In plain terms, it is a way to count by making distinctions. You begin with a first state, call it zero, and from any state you can move to a new one, its successor. This is the same structure a child uses to count on fingers, and it is the same structure the natural numbers use: 0, 1, 2, 3, and so on.

The classical definition of the natural numbers was formalized by Giuseppe Peano in 1889. His axioms state that zero is a natural number, every natural number has a successor, zero is not the successor of any number, and if two numbers have the same successor they are equal. These axioms, with the principle of mathematical induction, give the natural numbers their full power: they allow proofs about all numbers at once, not just the ones you can write down. The orbit here mirrors that exact structure, but it builds it from a different starting point: the act of distinction itself.

The orbit establishes three structural facts. First, zero is not the successor of any state, so the sequence has a genuine beginning. Second, the successor rule is injective: two different states never lead to the same next state, so the sequence never folds back on itself. Third, the principle of induction holds over the whole orbit, which means any property true of zero and preserved by the successor step is true of every state. These three facts are what make the orbit a counting structure rather than a mere list.

The orbit also proves that this structure is exactly the natural numbers in disguise. It defines a translation from each orbit state to a natural number and back again, and proves that translating round trip returns you to where you started. This equivalence is stated as a formal bijection. In Recognition Science, this is the base-neutral finite orbit of repeated distinction: the framework's ledger, a discrete record of events, begins with this minimal counting spine. The orbit is the raw material on which the framework's later results, such as the forced cost function and the golden ratio, are built.

What this means in practice is that the framework does not assume numbers as a given. It derives a counting structure from the primitive act of making a distinction, and then proves that this derived structure is indistinguishable from the familiar natural numbers. The consequence is that the framework's foundational vocabulary is not borrowed from elsewhere; it is generated from its own first principle. A reader who understands counting already understands the orbit, and the theorems simply confirm that the two are the same thing.

/-- R8. Successor is injective. -/
theorem succ_injective :
    Function.Injective succ := by
  intro a b h
  cases h
  rfl

/-- R8. Induction over the δ-orbit. -/
theorem induction {P : DistinctionNat → Prop}
    (hzero : P zero)
    (hsucc : ∀ n : DistinctionNat, P n → P (succ n)) :
    ∀ n : DistinctionNat, P n := by
  intro n
  induction n with
  | zero => exact hzero
  | succ n ih => exact hsucc n 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

This module does not derive the cost function or any physical constant. The orbit is not claimed to be a model of time or space. The equivalence to natural numbers does not imply the framework's axioms are the same as Peano's.

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: