Foundation Universal Forcing Canonical Iso Hom Eq Universal Forcing

The canonical number system

A number system is more than a collection of symbols. It is a starting point, usually called zero, together with a way to step from one number to the next, the successor operation. Two number systems are structurally the same when a bijection, a perfect matching between their elements, also sends the starting point of one to the starting point of the other and commutes with the stepping operation. Such a matching is called an isomorphism of Peano algebras, named after Giuseppe Peano who axiomatized the natural numbers in 1889.

The Recognition Science framework builds a number system from each of its realizations, which are concrete instances of the framework's rules. Earlier work had already produced a bijection between the number systems of any two realizations, but a bare bijection does not by itself respect zero or successor. The declaration hom_eq_universalForcing closes that gap: it proves that any structure-preserving map between two such forced number systems is exactly the universal forcing bijection. In plain terms, the framework's construction does not merely match up the elements of two number systems; it matches up their zeros and their stepping operations as well.

The theorem goes further and establishes uniqueness. The statement says that any homomorphism, a structure-preserving map, from one forced number system to another must equal the universal forcing map. Consequently, there is exactly one way to translate between the number systems of any two realizations while preserving their structure. This is what mathematicians mean by a canonical isomorphism: not just some isomorphism, but the unique one. The framework's library of machine-checked theorems records this as a certificate, quantified over all realizations, so the result holds for every pair at once.

In Recognition Science, this result matters because it shows that the framework's arithmetic is coherent across its different realizations. The number systems are not merely equivalent in size; they are identical in structure, and the identification between them is forced, not chosen. This strengthens the sense in which the framework's arithmetic is a single, well-defined object rather than a collection of loosely related ones. The uniqueness result is what makes the word canonical meaningful here.

The theorem does not claim that the isomorphism preserves addition, multiplication, or order. The Peano objects in this layer carry only zero and successor, so the proof covers only those operations. Preserving the richer ring operations and the order relation is the next step in the program, and it remains open. The theorem also does not claim that the framework's number systems are the ordinary natural numbers; it claims only that the systems built from different realizations are canonically isomorphic to each other.

/-- Any Peano homomorphism into the target forced arithmetic equals the
universal forcing map: there is exactly one Peano homomorphism, and it is an
isomorphism. -/
theorem hom_eq_universalForcing (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
    (f : PeanoObject.Hom (forcedArith R).peano (forcedArith S).peano) :
    f.toFun = (universalForcingPeanoEquiv R S).toEquiv :=
  (forcedArith R).initial.uniq (forcedArith S).peano f
    ((forcedArith R).initial.lift (forcedArith S).peano)

/-- **Canonicality.**  Any two structure-preserving isomorphisms between the
forced arithmetics of two realizations have the same underlying function.  The
isomorphism furnished by Universal Forcing is therefore the unique one. -/
theorem peanoEquiv_unique (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
    (e₁ e₂ : PeanoEquiv (forcedArith R).peano (forcedArith S).peano) :
    (e₁.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier)
      = (e₂.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier) :=
  (forcedArith R).initial.uniq (forcedArith S).peano e₁.toHom e₂.toHom

/-- **Universal Forcing isomorphism certificate.**

For any two Law-of-Logic realizations, there is a canonical structure-preserving
isomorphism between their forced arithmetics, and that isomorphism is unique. -/
structure UniversalForcingIsoCert where
  /-- The canonical Peano-algebra isomorphism between any two forced arithmetics. -/
  iso : ∀ R S : LogicRealization.{0, 0},
    PeanoEquiv (forcedArith R).peano (forcedArith S).peano
  /-- That isomorphism is unique as a structure-preserving map. -/
  unique : ∀ (R S : LogicRealization.{0, 0})
      (e₁ e₂ : PeanoEquiv (forcedArith R).peano (forcedArith S).peano),
      (e₁.toEquiv : (forcedArith R).peano.carrier → (forcedArith S).peano.carrier)
        = e₂.toEquiv

What this page does not claim

The isomorphism preserves the ring operations of addition and multiplication or the order relation. The forced number systems are identical to the ordinary natural numbers. The uniqueness result applies to any map that does not preserve zero and successor.

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/UniversalForcing/CanonicalIso.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: