Foundation Primitive Recognition Calculus Rigidity Ledger Transport Nat Algebra

The canonical number model

The natural numbers, 0, 1, 2, and so on, are the counting numbers of ordinary arithmetic. They satisfy the Peano axioms: zero is a natural number, every natural number has a successor, no two numbers share a successor, zero is not a successor, and a property that holds for zero and passes from each number to its successor holds for all numbers. These axioms are the standard foundation for arithmetic, and they are what the declaration natAlgebra_peano establishes for a specific structure inside the Recognition Science framework.

In Recognition Science, a ledger is a discrete record of events, and the framework's primitive calculus is built on a notion of distinction, a single step that separates one thing from another. The framework's kernel has a canonical semantic carrier, the natural numbers themselves, viewed as a δ-algebra: a structure with a zero element and a successor operation. The declaration natAlgebra_peano proves that this carrier, with zero as 0 and successor as the usual +1, is a Peano model of distinction. It verifies injectivity of successor, that zero is not a successor, and the induction principle, all in the framework's machine-checked library of formal theorems.

The significance is rigidity. The framework proves that the base recursor from its δ-base into the natural numbers is bijective, meaning the canonical model is the δ-base up to a unique isomorphism. Reading the natural numbers as "the" model is licensed by this rigidity theorem, not by an arbitrary encoding choice. This is a strong uniqueness result: within the framework, the natural numbers are not one possible implementation among many, but the inevitable one.

The framework then builds a transport map, natRec, that unrolls n distinction steps in any other δ-algebra M. For a Peano model M, this transport map is both injective and surjective, and the framework proves a Transport Lemma: satisfaction of a kernel formula transported into M coincides with satisfaction in the canonical model, formula by formula. The practical payoff is that a derivation the kernel accepts with an empty ledger is true in the transported semantics of every Peano model, with no additional metatheoretic principle. The ledger, the record of recognition events, is invariant under change of carrier.

In Recognition Science, this establishes the natural numbers as the canonical model of the primitive distinction calculus, with all Peano properties holding and a transport mechanism that preserves truth across models. It does not claim that the natural numbers are the only possible carrier for all of mathematics, nor that the Peano axioms themselves are derived from the framework. It does not claim that the transport map works for models that are not Peano, nor that the framework's results hold in classical set theory without the framework's own postulates.

/-- ℕ is a Peano model of distinction. -/
theorem natAlgebra_peano : IsPeanoModel natAlgebra where
  succ_injective := fun _ _ h => Nat.succ.inj h
  zero_not_succ := fun x h => Nat.succ_ne_zero x h
  induction := fun _ h0 hs x => Nat.rec h0 (fun n ih => hs n ih) x

/-- The kernel's canonical model IS the δ-base up to the (unique) iso: the base
recursor into ℕ is bijective. Reading ℕ as "the" model is licensed by rigidity,
not by an encoding choice. -/
theorem base_to_nat_bijective : Function.Bijective (baseRec natAlgebra) :=
  ⟨baseRec_injective natAlgebra natAlgebra_peano,
   baseRec_surjective natAlgebra natAlgebra_peano⟩

/-- The transport map into a Peano model is injective. Choice-free. -/
theorem natRec_injective (M : DeltaAlgebra) (h : IsPeanoModel M) :
    Function.Injective (natRec 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 (natRec M b))
  | succ a ih =>
      intro b he
      cases b with
      | zero => exact absurd he (h.zero_not_succ (natRec M a))
      | succ b => exact congrArg Nat.succ (ih (h.succ_injective he))

/-- The transport map into a Peano model is surjective (the model's own
induction schema). Choice-free. -/
theorem natRec_surjective (M : DeltaAlgebra) (h : IsPeanoModel M) :
    Function.Surjective (natRec M) := by
  intro y
  refine h.induction (fun y => ∃ n, natRec M n = y) ⟨0, rfl⟩ ?_ y
  rintro x ⟨n, rfl⟩
  exact ⟨n + 1, rfl⟩

/-- **The Transport Lemma.** For a Peano model M, satisfaction transported into
M coincides with satisfaction in the canonical model, formula by formula.
Injectivity of the transport map handles the atoms; quantifier witnesses travel
forward. Choice-free. -/
theorem msat_iff_sat (M : DeltaAlgebra) (hM : IsPeanoModel M) :
    ∀ (φ : DFormula) (ρ : Env), msat M ρ φ ↔ DFormula.sat ρ φ := by
  intro φ
  induction φ with
  | eq t s =>
      intro ρ
      simp only [msat, DFormula.sat]
      exact ⟨fun h => natRec_injective M hM h, fun h => congrArg (natRec M) h⟩
  | fls => intro ρ; exact Iff.rfl
  | conj a b iha ihb =>
      intro ρ
      simp only [msat, DFormula.sat]
      exact and_congr (iha ρ) (ihb ρ)
  | disj a b iha ihb =>
      intro ρ
      simp only [msat, DFormula.sat]
      exact or_congr (iha ρ) (ihb ρ)
  | impl a b iha ihb =>
      intro ρ
      simp only [msat, DFormula.sat]
      exact imp_congr (iha ρ) (ihb ρ)
  | all a ih =>
      intro ρ
      simp only [msat, DFormula.sat]
      constructor
      · intro h n
        exact (ih (Env.cons n ρ)).mp (h (natRec M n) n rfl)
      · intro h x n _
        exact (ih (Env.cons n ρ)).mpr (h n)
  | ex a ih =>
      intro ρ
      simp only [msat, DFormula.sat]
      constructor
      · rintro ⟨_, n, _, h⟩
        exact ⟨n, (ih (Env.cons n ρ)).mp h⟩
      · rintro ⟨n, h⟩
        exact ⟨natRec M n, n, rfl, (ih (Env.cons n ρ)).mpr h⟩

/-- **Kill test, FORCED case: PASS.** A derivation the kernel accepts with the
EMPTY ledger is true in the transported semantics of EVERY Peano model, with no
metatheoretic principle beyond the forced fragment. Transport along the unique
iso costs zero posits. -/
theorem transport_forced {d : Deriv} {φ : DFormula} (h : Forced [] d φ)
    (M : DeltaAlgebra) (hM : IsPeanoModel M) (ρ : Env) : msat M ρ φ :=
  (msat_iff_sat M hM φ ρ).mpr (sound_forced h ρ)

What this page does not claim

The natural numbers are the only possible carrier for all of mathematics. The Peano axioms themselves are derived from the framework's primitive distinction calculus. The transport map works for δ-algebras that are not Peano models. The framework's results hold in classical set theory without the framework's own postulates.

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/LedgerTransport.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: