Foundation Universal Forcing Strict Canonical Iso Strict Universal Forcing Iso C

The canonical isomorphism

The declaration StrictUniversalForcingIsoCert is a formal certificate, a packaged proof that a certain kind of bridge between two mathematical structures exists and is unique. The structures in question are Peano algebras, which are the standard formal setting for the natural numbers: a carrier set with a zero element and a successor map. The certificate states that for any two strict realizations of the framework's logic, the bijection between their forced arithmetics is not just any bijection but a structure-preserving isomorphism, meaning it sends zero to zero and commutes with the successor map. It further states that this isomorphism is unique: any two such structure-preserving maps are the same function.

To see what this means, consider two strict realizations as two different ways of supplying the native data of comparison, composition, identity, invariance, and non-triviality. From each such realization, the framework derives an arithmetic, a Peano algebra, rather than taking one as given. The certificate asserts that the derived arithmetics are canonically the same: there is exactly one way to translate between them that respects the structure of zero and successor. This is a uniqueness theorem in the framework's library, a machine-checked collection of formal theorems, and it holds for all pairs of strict realizations.

The certificate does not claim that the two realizations are identical, only that their derived arithmetics are isomorphic in a unique way. It does not claim that the isomorphism is computable, only that it exists and is unique. It does not claim anything about the physical world, about measurements, or about the values of constants. It is a purely structural statement about the framework's own logic, establishing that the derived arithmetic is invariant across strict realizations in the strongest sense: the bridge is forced, not chosen.

/-- **Strict Universal Forcing, structure-preserving form.**

For any two strict Law-of-Logic realizations, the bijection between their forced
arithmetics is a structure-preserving isomorphism of Peano algebras: it sends
zero to zero and commutes with the successor map. -/
noncomputable def strict_universal_forcing_peanoEquiv
    (R S : StrictLogicRealization) :
    PeanoEquiv (StrictLogicRealization.arith R).peano
      (StrictLogicRealization.arith S).peano :=
  universalForcingPeanoEquiv (StrictLogicRealization.toLightweight R)
    (StrictLogicRealization.toLightweight S)

/-- **Strict canonicality.**

Any two structure-preserving isomorphisms between the forced arithmetics of two
strict realizations have the same underlying function.  The strict universal
forcing isomorphism is therefore the unique one. -/
theorem strict_peanoEquiv_unique (R S : StrictLogicRealization)
    (e₁ e₂ : PeanoEquiv (StrictLogicRealization.arith R).peano
      (StrictLogicRealization.arith S).peano) :
    (e₁.toEquiv : (StrictLogicRealization.arith R).peano.carrier
        → (StrictLogicRealization.arith S).peano.carrier)
      = e₂.toEquiv :=
  peanoEquiv_unique (StrictLogicRealization.toLightweight R)
    (StrictLogicRealization.toLightweight S) e₁ e₂

/-- The strict certificate is inhabited by the strict canonical iso and its
uniqueness. -/
noncomputable def strictUniversalForcingIsoCert : StrictUniversalForcingIsoCert where
  iso := fun R S => strict_universal_forcing_peanoEquiv R S
  unique := fun R S => strict_peanoEquiv_unique R S

What this page does not claim

The certificate does not claim that the two realizations are identical, only that their derived arithmetics are uniquely isomorphic. It does not claim that the isomorphism is computable or that it has any physical interpretation. It does not claim anything about measured values or the forcing chain that derives constants.

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