IndisputableMonolith.Foundation.UniversalForcing.CanonicalIso
Canonical isomorphisms of forced arithmetic between any two Law-of-Logic realizations, upgraded from bare carrier bijections to unique Peano-algebra maps that preserve zero and successor. Anyone citing universal forcing uniqueness or the ordered-semiring lift will land here. The argument is initiality of Peano algebras plus uniqueness of the induced homomorphisms.
claimFor Law-of-Logic realizations $R$ and $S$, the forced arithmetic objects $\mathrm{Arith}(R)$ and $\mathrm{Arith}(S)$ (with all arithmetic universes pinned to each realization's carrier) are uniquely isomorphic as Peano algebras: there is a unique structure-preserving equivalence sending zero to zero and successor to successor.
background
Universal Forcing asserts that any two Law-of-Logic realizations have canonically equivalent forced arithmetic, because those objects are initial Peano algebras. The parent module states the bare carrier-level form of that theorem.
This module tightens the invariant. Forced arithmetic of a realization is the Peano structure extracted from the realization, with every ArithmeticOf universe fixed to the realization's own carrier universe so that universe polymorphism cannot hide inequivalent copies. A Peano equivalence is a bijection of carriers that intertwines zero and the successor operation.
The local setting is the Foundation layer of Recognition Science: arithmetic is not postulated independently but forced by the Law of Logic, so uniqueness of the forced Peano object is part of the forcing chain that later pins constants and dimension.
proof idea
The module builds forced arithmetic for each realization, then constructs the unique Peano homomorphism out of an initial algebra (zero and step maps of the initiality equivalence). Uniqueness of that homomorphism yields a unique Peano equivalence between any two realizations' forced arithmetics, together with a certificate packaging the iso and the uniqueness statement. Downstream modules import this package rather than re-deriving initiality.
why it matters in Recognition Science
This is Universal Forcing Part I at the structure-preserving level: the bare bijection becomes a unique zero-and-successor isomorphism of Peano algebras. CanonicalSemiringIso imports it to lift the same map through the ordered-semiring operations the Peano structure induces. Strict.CanonicalIso imports the same pattern for the strict "no escape hatch" realizations, upgrading the strict universal-forcing bijection to a structure-preserving iso.
In the broader framework the result anchors the claim that forced arithmetic is unique up to unique iso, so later steps (mass ladder, constants, eight-tick structure) do not depend on a choice of realization. It does not yet touch the J-cost or T5–T8 forcing steps; those sit further downstream once arithmetic is fixed.
scope and limits
- Does not prove the ordered-semiring or ring layer; that is CanonicalSemiringIso.
- Does not treat strict realizations; see Strict.CanonicalIso.
- Does not derive physical constants, phi, or dimension from the Peano iso alone.
- Does not claim uniqueness of the Law-of-Logic realization itself, only of forced arithmetic.
- Does not address non-Peano models or alternative arithmetic foundations.
used by (2)
depends on (1)
declarations in this module (11)
-
abbrev
forcedArith -
structure
PeanoEquiv -
def
toHom -
theorem
equivOfInitial_map_zero -
theorem
equivOfInitial_map_step -
def
universalForcingPeanoEquiv -
theorem
universalForcingPeanoEquiv_toEquiv -
theorem
peanoEquiv_unique -
theorem
hom_eq_universalForcing -
structure
UniversalForcingIsoCert -
def
universalForcingIsoCert