universalForcingPeanoEquiv
plain-language theorem explainer
Canonical Peano-algebra isomorphism between the forced arithmetics of any two Law-of-Logic realizations. It packages the universal forcing carrier bijection with zero and successor preservation. Cite it when arguing that forced number systems are uniquely isomorphic across realizations, not merely bijective as sets. The body is a structure instance: underlying map from initiality, fields filled by the two preservation lemmas.
Claim. For any two Law-of-Logic realizations $R$ and $S$, there is a structure-preserving isomorphism of Peano objects between the forced arithmetic of $R$ and that of $S$: an equivalence of carriers sending zero to zero and intertwining the successor maps.
background
A Law-of-Logic realization supplies a carrier, a comparison cost, an identity, and a step/generator action. From that data one extracts an arithmetic object: a Peano algebra (carrier, zero, successor) together with a proof that it is initial among Peano objects. Initiality yields a unique homomorphism into any other Peano object, and therefore a natural carrier equivalence between the forced arithmetics of any two realizations.
That bare equivalence is only a set bijection. The module upgrades it at the Peano-algebra layer: the forcing map must send zero to zero and commute with successor, so it is a homomorphism of Peano objects, not merely a bijection of carriers. The bundled form of such a map is a structure-preserving Peano isomorphism: an equivalence of carriers plus the two preservation identities.
Upstream, the natural equivalence between initial Peano objects is built by lifting each initial object into the other; the zero and step preservation facts are the corresponding fields of those lifts (already proved for general realizations in the CanonicalForcing layer).
proof idea
One-line structure instance. The underlying carrier equivalence is the natural map between initial Peano objects applied to the forced arithmetics of $R$ and $S$. Zero preservation is the specialized zero lemma for those forced arithmetics; successor intertwining is the specialized step lemma. No further tactic work: the three fields of the Peano-isomorphism bundle are filled directly by those three upstream constructions.
why it matters
This is the arithmetic-extraction upgrade in Universal Forcing Part II: the invariant moves from a bare carrier bijection to a unique Peano-algebra isomorphism. Downstream, the uniqueness theorem for Peano homomorphisms into a forced arithmetic identifies every such homomorphism with this map; the iso certificate packages the family of these isomorphisms with uniqueness over all realizations.
The ordered-semiring layer builds on it directly: fold compatibility, additivity, multiplicativity, and order preservation are all stated in terms of this canonical map, and the forced ordered-semiring certificate records that the same map preserves $0$, $1$, $+$, $\times$, and $\le$. Honest scope from the module: Peano objects carry only zero and step, so ring and order structure is the remaining crown of Part II, not proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.