Foundation Primitive Recognition Calculus Rigidity Ledger Transport Transport Gr

Transport without residue

In mathematics, a proof is often tied to the particular system where it was written. The declaration transport_graded shows a specific way this tie can be broken. It proves that if a derivation is accepted under a certain graded ledger, a discrete record of recognition events, then the same formula is true in any Peano model, a structure that behaves like the natural numbers with zero, successor, and induction. The result is a theorem in the machine-checked library of formal theorems.

The proof works by transporting meaning along a map from the canonical carrier, the natural numbers, into the target model. The map sends zero to the model's zero and each successor step to the model's successor operation. For a Peano model this map is bijective, meaning every element of the model is reached by exactly one natural number. This bijection lets the framework re-read any formula in the new model, and the transport lemma shows that satisfaction in the new model agrees with satisfaction in the canonical one, formula by formula.

The key property is that the ledger, the record of recognition costs, is invariant under this change of carrier. A derivation accepted with ledger O is true in every Peano model under exactly the gates that the canonical soundness theorem already demanded. Transport adds no new gate. This is what makes the result a zero-cost transport: the validity moves without accumulating additional assumptions.

In Recognition Science, this result matters because it shows that the framework's proofs are not hostage to one particular encoding of the natural numbers. The canonical model is not chosen by convenience; rigidity forces it to be the unique model up to isomorphism. The transport theorem then guarantees that any Peano model carries the same forced truths, with no metatheoretic principle beyond the forced fragment's own basis.

The theorem also covers a specific test case: the commutativity of distinction-composition, a Gödel-test theorem, holds in every Peano model at zero transported cost. This is a concrete instance of the general principle, not an isolated curiosity.

The declaration does not claim that every proof transports, only those accepted under a graded ledger. It does not claim that the transport map itself is constructive in the sense of avoiding choice; the choice-freeness audit is a separate claim about the axiom footprint. And it does not claim anything about models that are not Peano, where the bijection may fail.

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

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

The theorem does not claim that every derivation transports, only those accepted under a graded ledger. The theorem does not claim that the transport map is constructive without choice; the choice-freeness audit is a separate claim. The theorem does not claim anything about models that are not Peano.

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: