Foundation Universal Forcing Canonical Iso

The canonical isomorphism

In Recognition Science, a realization is a concrete model of the framework's axioms, such as one based on positive ratios or on discrete Boolean values. Each realization gives rise to a forced arithmetic, a Peano-style number system built from a zero element and a successor (step) function. The universal forcing construction previously produced a bijection, a one-to-one pairing, between the carriers of any two such forced arithmetics. A bijection alone, however, does not guarantee that the structure of the number systems is respected: it might not send zero to zero or commute with the successor function.

This result closes that gap. It proves that the universal forcing bijection does send the forced zero to the forced zero and does commute with the forced step map. This upgrades the bijection to a homomorphism, a map that preserves the algebraic structure. The result then bundles this data into a PeanoEquiv, a structure-preserving isomorphism between Peano objects. The central result, peanoEquiv_unique, establishes that any two such structure-preserving isomorphisms between the same pair of forced arithmetics have the same underlying function. This uniqueness is what makes the isomorphism canonical: it is not merely some isomorphism, but the unique one.

In Recognition Science, this canonical isomorphism is a certificate that the number systems arising from different realizations are not just equinumerous but structurally identical in their most basic recursive architecture. The result is quantified over all realizations in the certificate structure UniversalForcingIsoCert, which packages the existence of the iso and its uniqueness. This means that the Peano-algebra layer of arithmetic is forced, not chosen, by the framework's axioms.

The honest scope of this result is precise. It establishes the unique Peano-algebra isomorphism, meaning it respects zero and successor. It does not yet prove preservation of the ring operations of addition and multiplication, nor of the order relation. The PeanoObject in the framework's ArithmeticOf.lean carries only zero and step, so the richer ordered-semiring isomorphism remains the next step toward the full arithmetic-extraction layer.

/-- The universal forcing bijection sends the forced zero to the forced zero. -/
theorem equivOfInitial_map_zero (R : LogicRealization.{u, v}) (S : LogicRealization.{u, w}) :
    (ArithmeticOf.equivOfInitial (forcedArith R) (forcedArith S))
        (forcedArith R).peano.zero
      = (forcedArith S).peano.zero :=
  ((forcedArith R).initial.lift (forcedArith S).peano).map_zero

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

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

This result does not prove preservation of the ring operations + and × or the order relation ≤. This result does not establish the canonical isomorphism for realizations at different universe levels. This result does not claim that the forced arithmetic is the only possible number system, only that it is canonically unique up to isomorphism.

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: