Foundation Universal Forcing Canonical Iso Equiv Of Initial Map Step

The step-respecting map

In mathematics, a bijection between two sets is a pairing that matches every element of one set with exactly one element of the other. A structure-preserving isomorphism goes further: it also requires that the pairing respect the operations that give each set its shape. For number systems built from a zero and a successor (the "next number") operation, an isomorphism must send zero to zero and must send the successor of any number to the successor of its paired number. The theorem equivOfInitial_map_step establishes precisely this second property for a specific pairing constructed in the Recognition Science framework.

The framework builds number systems from a starting point it calls a recognition event: a discrete record of a distinction being made, kept in a ledger that tracks every such event. From different choices of how recognition costs are accounted, the framework forces arithmetic structures that are initially only known to have the same size, in the sense of a bare bijection. The theorem in question upgrades that bare pairing: it proves that the pairing sends the successor of any element to the successor of the paired element. Combined with its companion statement that zero maps to zero, the two results together show the pairing is a homomorphism of Peano algebras, not merely a set-level correspondence.

The significance is that the bridge between two forced arithmetics is not arbitrary. A further theorem in the same file, peanoEquiv_unique, proves that any two structure-preserving isomorphisms between the same pair of forced arithmetics have the same underlying function. So the pairing is not just some isomorphism; it is the unique one. This is what the word "canonical" means in the framework's description: the isomorphism is forced by the structure itself, leaving no room for choice.

What the declaration does not claim is equally precise. It concerns only the zero and successor operations. The richer operations of addition, multiplication, and order are not touched by this theorem, because the underlying object it works with carries only zero and step. The framework's own documentation states that preserving those ring operations and the order relation is the next step, not something already proved. The theorem also says nothing about whether the two number systems are identical in content, only that they are uniquely isomorphic at the level of their basic counting structure.

In Recognition Science, this result matters because it shows the arithmetic forced by different realization choices is not merely similar in size but canonically equivalent in structure. A reader can now see that the framework's claim of a unique bridge between forced number systems is a proved statement with a clear scope, and that the scope deliberately stops short of the full algebraic structure.

/-- The universal forcing bijection commutes with the forced step map. -/
theorem equivOfInitial_map_step (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
    (x : (forcedArith R).peano.carrier) :
    (ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S))
        ((forcedArith R).peano.step x)
      = (forcedArith S).peano.step
          ((ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S)) x) :=
  ((forcedArith R).initial.lift (forcedArith S).peano).map_step x

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

/-- The universal forcing bijection commutes with the forced step map. -/
theorem equivOfInitial_map_step (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w})
    (x : (forcedArith R).peano.carrier) :
    (ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S))
        ((forcedArith R).peano.step x)
      = (forcedArith S).peano.step
          ((ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S)) x) :=
  ((forcedArith R).initial.lift (forcedArith S).peano).map_step x

What this page does not claim

The theorem does not preserve addition, multiplication, or order, which are not part of the Peano object it works with. The theorem does not show the two forced arithmetics are identical, only that they are uniquely isomorphic at the level of zero and successor. The theorem does not apply to realizations at different universe levels, since all realizations in the Universal Forcing program are stated at the same universe.

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: