Foundation Universal Forcing Canonical Iso Universal Forcing Iso Cert

The canonical number system

In mathematics, a bijection between two sets is a pairing that matches each element of one set with exactly one element of the other. A bijection between two number systems, however, is weaker than an isomorphism: it does not, on its face, respect the structure that makes them number systems, such as zero or the successor operation that counts upward. The declaration UniversalForcingIsoCert closes that gap. It establishes that for any two realizations of the framework's logic, the previously known bijection between their forced number systems is actually a structure-preserving isomorphism, and further that this isomorphism is unique.

The framework's ledger, a discrete record of recognition events, forces a particular arithmetic out of any realization that satisfies its basic laws. The existing Universal Forcing spine produced a bare carrier bijection between the forced arithmetics of any two such realizations. The new certificate upgrades this invariant. It proves that the bijection sends the forced zero to the forced zero and commutes with the step map, so it is a homomorphism of Peano algebras, not merely a set bijection. It then packages this structure-preserving isomorphism together with a proof of its uniqueness, quantified over all realizations at the framework's standard universe level.

The uniqueness claim is the heart of the certificate. Any two structure-preserving isomorphisms between the same pair of forced arithmetics have the same underlying function. This is what makes the isomorphism canonical: it is not merely some isomorphism, it is the unique one. The certificate is inhabited by the canonical isomorphism and its uniqueness proof, so the statement is not just a definition but a proved theorem in the framework's machine-checked library of formal theorems.

What the certificate does not claim is as important as what it proves. It establishes isomorphism at the Peano-algebra layer, which carries only zero and step. It does not prove preservation of the ring operations addition and multiplication, nor of the order relation. Those belong to the richer ordered-semiring isomorphism, which remains the next step toward the full Part II crown. The certificate also does not claim anything about the physical interpretation of the forced arithmetic; it is a statement about the internal structure of the framework's number systems.

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

/-- The certificate is inhabited by the canonical iso and its uniqueness. -/
noncomputable def universalForcingIsoCert : UniversalForcingIsoCert where
  iso := fun R S => universalForcingPeanoEquiv R S
  unique := fun R S => peanoEquiv_unique R S

What this page does not claim

The certificate does not claim preservation of the ring operations +, ×, or the order ≤. The certificate does not claim anything about the physical interpretation of the forced arithmetic. The certificate does not claim that the forced arithmetic is the only number system, only that any two are canonically isomorphic.

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: