Foundation Primitive Recognition Calculus Rigidity Base Initiality Base Categori

The categorical pin

The natural numbers 0, 1, 2, 3, ... are not just a familiar list. They are the unique structure, up to relabeling, that has a starting point and a distinct next step for every element, with no loops and no dead ends. This uniqueness is what mathematicians call categoricity: any two structures satisfying those same plain conditions are the same in every way that matters, connected by exactly one structure-preserving map. The theorem base_categorical in the Recognition Science library's rigidity section proves this categoricity for its foundational delta-algebra, a raw signature of distinction: a carrier with a distinguished zero and a successor function.

The proof works by showing that the natural numbers are the initial object in the category of such structures. From any candidate structure M that satisfies the Peano-style conditions (injective successor, zero not a successor, and induction), the theorem constructs a unique map from the natural numbers into M. This map is the recursive definition: send zero to M's zero, and send each successor to M's successor. The theorem then proves this map is injective and surjective, so it is a bijection, and the uniqueness of the map makes the structures isomorphic in exactly one way. The same file also proves the stronger base_unique_iso, which packages the uniqueness of the isomorphism itself.

In Recognition Science, this result is the base tier of a larger forcing chain. The framework models reality as a ledger, a discrete record of recognition events, and the delta-algebra is the raw act of distinction that the ledger builds on. The categoricity theorem pins down that this act of distinction, with a starting point and a next step, is necessarily the natural numbers and nothing else. This is a structural claim about the foundation, not a claim about physics: it says that any model of this primitive distinction is the same as the natural numbers, so the framework's foundational arithmetic is rigid, not arbitrary.

What the theorem does not claim is just as important. It does not claim that the natural numbers are the only model of the Peano axioms in the usual sense; that is a separate, classical result. It does not claim that the framework's delta-algebra is the same as the natural numbers as a set; it is a structure with a carrier, zero, and successor, and the theorem shows it is isomorphic to the natural numbers. It does not claim that this categoricity forces any physical law or constant; that work happens in later parts of the forcing chain, not in this base theorem. The theorem is a pin in the foundation: it establishes the rigidity of the primitive distinction, and nothing more.

theorem base_categorical : target_categorical :=
  fun M h => ⟨baseHom M, baseRec_injective M h, baseRec_surjective M h⟩

theorem base_initial : target_initial :=
  fun M => ⟨baseInitial M⟩

/-- The initial map into a Peano model is injective (δ-orbit induction, using the
model's `succ_injective` and `zero_not_succ`). Choice-free. -/
theorem baseRec_injective (M : DeltaAlgebra) (h : IsPeanoModel M) :
    Function.Injective (baseRec M) := by
  intro a
  induction a with
  | zero =>
      intro b he
      cases b with
      | zero => rfl
      | succ b => exact absurd he.symm (h.zero_not_succ (baseRec M b))
  | succ a ih =>
      intro b he
      cases b with
      | zero => exact absurd he (h.zero_not_succ (baseRec M a))
      | succ b => exact congrArg DistinctionNat.succ (ih (h.succ_injective he))

/-- The initial map into a Peano model is surjective (the model's own induction
schema: every element is reached from `M.zero` by steps). Choice-free. -/
theorem baseRec_surjective (M : DeltaAlgebra) (h : IsPeanoModel M) :
    Function.Surjective (baseRec M) := by
  intro y
  refine h.induction (fun y => ∃ n, baseRec M n = y) ⟨DistinctionNat.zero, rfl⟩ ?_ y
  rintro x ⟨n, rfl⟩
  exact ⟨DistinctionNat.succ n, rfl⟩

theorem base_unique_iso : target_unique_iso := by
  intro M h
  refine ⟨{ default := ⟨baseHom M, baseRec_injective M h, baseRec_surjective M h⟩,
            uniq := ?_ }⟩
  intro f
  apply Subtype.ext
  exact (baseInitial M).uniq f.1

What this page does not claim

The theorem does not claim that the natural numbers are the only model of the Peano axioms in the usual sense. The theorem does not claim that the delta-algebra is the same as the natural numbers as a set. The theorem does not claim that this categoricity forces any physical law or constant.

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/Rigidity/BaseInitiality.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: