Foundation Primitive Recognition Calculus Rigidity Ledger Transport Nat Rec Surj

The transport map's reach

The natural numbers are the familiar counting sequence 0, 1, 2, 3, and so on. A Peano model is any structure that satisfies the same defining properties: a starting point, a successor operation that never repeats itself, and an induction principle saying that what holds for the start and passes from each number to its successor holds for all numbers. The classical natural numbers are one such model, but so are other structures that merely behave like them.

In the Recognition Science framework, the kernel's canonical semantic carrier is the natural numbers, treated as a ledger, a discrete record of events. The declaration natRec_surjective proves a property of the transport map, the function that unrolls a natural number into the corresponding element of any other Peano model by applying that model's successor operation that many times. The theorem states that this transport map is surjective: for every element of the target model, there exists a natural number that maps to it. In plain language, counting steps in the target model reaches everything in it; no element is left unreachable.

The proof uses the target model's own induction schema. It starts with the model's zero element, which is reached by the natural number 0, and shows that if some element is reached by a natural number n, then its successor is reached by n + 1. By induction, every element is reached. The proof is choice-free, meaning it does not rely on the axiom of choice; it constructs witnesses explicitly at every step.

This surjectivity matters for the framework's transport lemma, which states that satisfaction of a formula in the canonical model coincides with satisfaction in any Peano model. The surjectivity ensures that a universal quantifier ranging over the target model genuinely constrains all of its elements, not just a subset. Without it, a statement true in the canonical model might fail to hold somewhere in the target model that the quantifier never reaches.

In Recognition Science, this result supports the claim that the kernel's canonical model is the δ-base up to a unique isomorphism, licensed by rigidity rather than by an arbitrary encoding choice. The transport map is bijective into any Peano model, and this bijectivity is what lets the framework move derivations and their ledgers between models without adding new assumptions.

The theorem does not claim that every structure is a Peano model. It applies only to those that satisfy the defining properties, and the surjectivity proof depends on the induction principle. It also does not claim that the transport map is computable in any practical sense, nor that it preserves any structure beyond the successor operation. It is a statement about reachability within a class of structures, not about the efficiency or uniqueness of the path taken.

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

/-- Non-vacuity of the transported universal: in a Peano model, EVERY element of
the carrier is reached by a witness, so `msat`'s guarded ∀ genuinely constrains
all of M. (Surjectivity is exactly what a Peano model adds here.) -/
theorem msat_all_covers (M : DeltaAlgebra) (hM : IsPeanoModel M)
    {a : DFormula} {ρ : Env} (h : msat M ρ (.all a)) (x : M.carrier) :
    ∃ n, natRec M n = x ∧ msat M (Env.cons n ρ) a := by
  obtain ⟨n, rfl⟩ := natRec_surjective M hM x
  exact ⟨n, rfl, h (natRec M n) n rfl⟩

What this page does not claim

Every structure is a Peano model. The transport map is computable in practice. The transport map preserves structure beyond the successor operation.

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: