Foundation Primitive Recognition Calculus Rigidity Base Initiality Base Rec Inje

The uniqueness of counting

The natural numbers are the familiar counting sequence: zero, then one more, then one more again. A recognition ledger, a discrete record of events, has the same shape: a starting point and a step that adds one distinction at a time. The declaration baseRec_injective is a theorem in the framework's machine-checked library of formal theorems. It proves that this counting map, from the abstract ledger into any other system that satisfies the same basic rules, never sends two different ledger positions to the same place. In plain language, distinct counts stay distinct.

The theorem does more than protect one example. It is part of a rigidity result: any carrier that has a starting point, a successor step, and obeys the three Peano-style axioms (successor is injective, zero is not a successor, and induction holds) is uniquely isomorphic to the counting ledger. The proof shows there is exactly one structure-preserving map from the ledger to such a system, and that map is a bijection. This is the categorical notion of initiality: the counting ledger is the universal example, the one every other valid system mirrors. The framework's library proves this in full, with no gaps left to informal argument.

What the theorem does not claim is just as important. It does not say that every possible ledger is the natural numbers. A system with extra structure, or one that fails induction, can differ. It does not assert that the natural numbers are the only model of anything physical. It concerns the abstract algebraic signature of distinction, not which concrete system in the world realizes it. And it does not, by itself, say anything about the cost function or the golden ratio; that is a separate chain of results built on top of this foundation.

The consequence is a clean foundation. Before any talk of cost, scaling, or dimensions, the framework establishes that its most primitive act, making a distinction, has a unique abstract shape. This injectivity result is the first pin: it shows the ledger is not arbitrary, but forced by its own rules. A reader can now see why the framework's later results have a rigid character, they are built on a base that admits no alternatives.

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

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 every possible ledger is the natural numbers. It does not assert that the natural numbers are the only model of anything physical. It does not, by itself, say anything about the cost function or the golden ratio.

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: