Foundation Primitive Recognition Calculus Orbit Zero Ne Succ

The first distinction

The natural numbers begin with a simple rule: zero is not the next number after anything. The declaration zero_ne_succ states this rule for the framework's own counting structure, a type called DistinctionNat. This type has two ways to build a value: zero, the starting point, and succ, which takes one value and produces the next one. The theorem proves that for any value n, zero is not equal to succ n. In plain terms, the first position in the sequence is not a repetition of some earlier position; the sequence has a genuine beginning.

The proof itself is short and mechanical. It assumes the opposite, that zero equals succ n, and then shows this assumption leads to an impossible case. The same file also proves that the successor function is injective, meaning different inputs always give different outputs, and that the structure supports induction, the principle that a property holding for zero and preserved by successor holds for every value. These three results together give the counting structure the standard behavior of the natural numbers: a first element, no cycles, and a way to reason about all elements at once.

In Recognition Science, this structure represents the base-neutral finite orbit of repeated distinction, the minimal record of making one distinction after another. The framework uses this orbit as the foundation for building more complex structures, and the machine-checked library of formal theorems records these proofs. The declaration zero_ne_succ is one of the first steps in that foundation, establishing that the process of making distinctions has a definite starting point that is not itself a repetition.

The theorem does not claim that the natural numbers are invented by the framework, nor that zero is a physical object. It establishes a structural property of a formal counting type, not a statement about the physical universe. The proof also does not show that the framework's counting structure is the only way to model counting, nor does it derive any of the deeper results of the framework, such as the cost function or the golden ratio. It is a modest but necessary lemma: the first step is not a loop.

/-- R8. Zero is not a successor. -/
theorem zero_ne_succ (n : DistinctionNat) :
    zero ≠ succ n := by
  intro h
  cases h

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

What this page does not claim

The theorem does not claim that zero is a physical object or that the natural numbers are discovered by the framework. No claim is made that this counting structure is the only possible way to model repeated distinction. The proof does not derive the cost function, the golden ratio, or any other result beyond the basic properties of the orbit.

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: