Foundation Primitive Recognition Calculus Rigidity Base Initiality Base Rigidity

The counting skeleton

The natural numbers are the familiar counting chain: a starting point, zero, and a step that moves from any number to its successor. The declaration base_rigidity is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves that this counting chain is the only possible shape for any structure that satisfies the same basic rules.

The rules define a delta algebra, a general structure with a carrier set, a distinguished starting point, and a distinction step. A delta algebra is a Peano model when its step is injective, its starting point is not a successor, and induction holds: any property true of the start and preserved by the step is true everywhere. These are exactly the conditions that make a structure behave like the natural numbers.

The theorem bundles three results. First, initiality: for every Peano model, there is exactly one structure-preserving map from the counting chain into it. Second, categoricity: every Peano model is isomorphic to the counting chain, meaning there is a bijective structure-preserving map between them. Third, uniqueness of the isomorphism: that map is unique. Together these force any Peano model to be, up to a unique renaming, the natural numbers themselves.

The proof works by defining a recursive map from the counting chain into any Peano model, sending zero to the model's start and each successor to the model's step. Induction shows this map is injective and surjective, so it is a bijection. A separate argument shows any structure-preserving map must equal this one, giving uniqueness. The whole proof is checked by a computer, with no hidden assumptions beyond the standard logical axioms.

What this does not claim is broader. It does not say the natural numbers are the only mathematical structure, nor that every delta algebra is a Peano model. It does not address whether the physical universe is built from such a counting chain. It establishes a rigidity result within a specific algebraic setting: if a structure obeys the Peano rules, it is exactly the counting chain, and that is all.

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

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

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 natural numbers are the only mathematical structure of any kind. Every delta algebra is a Peano model. The physical universe is built from this counting chain.

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: