Foundation Primitive Recognition Calculus Rigidity Ledger Transport

Transport without a toll

The natural numbers, 0, 1, 2, and so on, are the counting numbers of ordinary arithmetic. Their defining properties are the Peano axioms: zero is not the successor of any number, the successor function never repeats itself, and a proof by induction works. Any structure obeying these axioms is a Peano model, a carrier set with a zero and a successor step that behave exactly like the natural numbers. The natural numbers themselves are the canonical model, the one every other model is compared against.

A standard fact, known for over a century, is that all Peano models are isomorphic: they are the same shape, just wearing different clothes. The module under discussion makes this precise and puts it to work. It defines a transport map that carries a natural number n into any Peano model by applying that model's successor step n times, starting from its zero. The map is bijective, meaning every element of the model is reached exactly once, and it is choice-free, meaning the proof never invokes the axiom of choice.

The decisive step is a transport lemma. A formula of the kernel language, such as the commutativity of addition, can be read in two ways: in the canonical model of the natural numbers, or in any Peano model M, where equalities and quantifiers are re-interpreted through the transport map. The lemma proves these two readings agree, formula by formula. Injectivity of the transport map handles the atomic equalities, and quantifier witnesses travel forward along the map. The proof is choice-free throughout.

In Recognition Science, this is called ledger transport: the ledger is a discrete record of recognition events, and the kernel is the fixed starting point of the framework's reasoning. The module shows that a derivation the kernel accepts with an empty ledger is true in every Peano model, with no metatheoretic principle beyond the forced fragment. A derivation accepted with a non-empty ledger is true in every Peano model under exactly the gates the canonical soundness theorem already demanded. Transport adds no new gate; the ledger is invariant under change of carrier.

The practical consequence is a zero-cost transfer of results. A theorem proved once in the canonical model, such as the commutativity of distinction-composition, holds in every Peano model at no additional cost. The machine-checked library of formal theorems, the framework's library, verifies this by a kill test: the axiom footprint of transport is contained in the forced fragment's own basis, with no classical choice. What the framework proves about the natural numbers is not an accident of one encoding; it is true of any structure that counts like the natural numbers do.

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

/-- **Kill test, graded case: PASS.** An accepted derivation with ledger `O` is
true in every Peano model under EXACTLY the gates `Gated O` the canonical
soundness theorem already demanded. Transport adds no gate: the ledger is
invariant under change of carrier. -/
theorem transport_graded {Γ : Ctx} {d : Deriv} {φ : DFormula} {O : Ledger}
    (h : check Γ d = some (φ, O)) (hG : Gated O)
    (M : DeltaAlgebra) (hM : IsPeanoModel M) (ρ : Env) (hΓ : CtxSat ρ Γ) :
    msat M ρ φ :=
  (msat_iff_sat M hM φ ρ).mpr (sound_cond d Γ φ O h hG ρ hΓ)

What this page does not claim

This module does not prove the Peano axioms; it assumes them as the definition of a Peano model. This module does not show that every mathematical structure is a Peano model, only that results transport between those that are. This module does not derive the cost function J or any of the later forcing-chain results; it concerns only the transport of kernel derivations.

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: