Foundation Primitive Recognition Calculus Rigidity Base Initiality Base Rec Surj

The counting theorem

The natural numbers are the counting numbers: zero, one, two, and so on, with no gaps and no repetitions. The declaration baseRec_surjective proves half of that description in a precise setting. It says that if you have any collection of objects with a distinguished starting point and a "next" step, and that collection obeys the three laws of counting (the next step never repeats, the starting point is not a next step, and the principle of induction holds), then every object in the collection can be reached by starting at zero and applying the next step some finite number of times. In plain words: there are no hidden objects, no unreachable corners, no extra elements beyond what the counting process generates.

The other half, proved separately, says the process never repeats: different numbers of steps always land on different objects. Together the two halves form a complete structural description. Any such collection is not merely similar to the natural numbers; it is, in the technical sense, the same structure. A map exists that sends each counting number to its counterpart in the collection, and this map is a bijection, meaning it pairs every element of the collection with exactly one counting number. This is the kind of result mathematicians call a categoricity theorem: the laws pin down the structure completely, leaving no room for alternative models.

The proof is short and direct. To show every object is reachable, the argument uses the induction law itself. It defines a property: "this object can be reached by some number of steps." The starting point has the property, since zero steps reach it. If an object has the property, then applying the next step reaches the next object, so that has the property too. By induction, every object has the property. The formal proof in the machine-checked library of formal theorems is a handful of lines, and the machine verifies each step.

In Recognition Science, this result anchors the framework's basic vocabulary. The framework models recognition events as discrete steps in a ledger, a structured record of what has been distinguished. The theorem guarantees that this ledger, when it obeys the counting laws, has no extra structure beyond the steps themselves. It does not claim that the natural numbers are the only possible carrier of a distinction process, nor that any arbitrary step function forms a valid counting structure. It claims only that once the three laws hold, the structure is forced to be the counting numbers, a fact the framework relies on when it builds its later results about cost and scaling.

/-- 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_categorical : target_categorical :=
  fun M h => ⟨baseHom M, baseRec_injective M h, baseRec_surjective M h⟩

What this page does not claim

The theorem does not claim that the natural numbers are the only possible carrier of a distinction process. It does not claim that any arbitrary step function forms a valid counting structure. It does not derive the cost function or any later framework result.

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: