Foundation Primitive Recognition Calculus Rigidity Ledger Transport Nat Rec Inje

The transport map

The natural numbers are the standard model of counting: zero, then one, then two, and so on. Mathematicians often ask whether some other structure, built from different primitives, behaves exactly like the natural numbers. The declaration natRec_injective is part of an answer to that question inside the Recognition Science framework. It states that a certain translation map, which carries the natural numbers into any other model of counting, never sends two different numbers to the same place. In plain terms, the map is injective: distinct inputs yield distinct outputs.

The framework builds its own model of counting, called the δ-base, from a primitive notion of distinction: a zero element and a successor operation. The natural numbers themselves form one such model. The framework's library, a machine-checked collection of formal theorems, proves that the natural numbers are a Peano model of this δ-base: successor is injective, zero is not a successor, and induction holds. The transport map natRec unrolls a natural number into a sequence of distinction steps inside any other model. The theorem natRec_injective proves that this unrolling is faithful: no two natural numbers collapse to the same element in the target model, provided the target model is itself Peano.

This injectivity is not a curiosity. It is the load-bearing wall for a larger result called the Transport Lemma. The lemma says that a formula true in the canonical model remains true when re-read in any Peano model, formula by formula. Injectivity handles the atomic equalities: if two terms evaluate to the same element in the target model, the transport map being injective forces them to have been equal in the source. Without injectivity, the translation could conflate distinct objects and the whole transfer would fail. The library proves the lemma, and from it derives that any derivation the kernel accepts with the empty ledger is true in every Peano model, at zero additional cost.

The theorem is deliberately narrow. It does not claim that every model of counting is isomorphic to the natural numbers; that stronger claim, base_to_nat_bijective, is a separate theorem in the library. It does not claim that the transport map is surjective, that every element of the target model is reached; that is a separate theorem, natRec_surjective, which requires the target model's own induction schema. And it does not claim anything about the fine-structure constant, the Riemann Hypothesis, or any other empirical or number-theoretic result. The theorem is a structural fact about translation between models of counting, nothing more.

What the theorem changes is the epistemic status of the framework's claims. Because the transport map is injective, the framework can move results from its canonical model into any Peano model without loss of information. This is what the library calls zero-cost transport: the ledger of recognition events, the record of what the kernel has accepted, is invariant under change of carrier. A reader who worries that the framework's results depend on a particular encoding of the natural numbers can see, from this theorem, that the encoding is rigid: any Peano model will do, and the results carry over unchanged.

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

/-- ℕ 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 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 theorem does not claim that every model of counting is isomorphic to the natural numbers. The theorem does not claim that the transport map is surjective without the target model being Peano. The theorem does not claim anything about empirical constants or number-theoretic results like the Riemann Hypothesis.

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: