hom_eq_universalForcing
plain-language theorem explainer
Any Peano-algebra homomorphism between the forced arithmetics of two Law-of-Logic realizations equals the universal forcing map on carriers. Cite this for uniqueness of arithmetic extraction: there is exactly one such homomorphism, and it is the canonical isomorphism. The proof is a one-line appeal to initiality uniqueness of the source forced Peano object.
Claim. For Law-of-Logic realizations $R$ and $S$, and any Peano-algebra homomorphism $f$ from the forced arithmetic of $R$ to that of $S$, the underlying map of $f$ equals the underlying map of the universal forcing Peano equivalence between those forced arithmetics.
background
Universal Forcing Part II extracts arithmetic from Law-of-Logic realizations. A PeanoObject is a carrier with zero and a step map; a homomorphism preserves both. The forced arithmetic of a realization is the initial Peano object in that realization's interpretation, so there is a unique homomorphism out of it into any other Peano object.
The parent spine already supplies a bare carrier bijection between forced arithmetics of any two realizations. This module upgrades that bijection to a structure-preserving Peano isomorphism and proves uniqueness of the underlying function. The universal forcing Peano equivalence is that unique isomorphism, built from the initial lift.
Honest scope from the module: only zero and step are in the Peano surface here. Ring operations and order are deferred.
proof idea
Term-mode proof. Apply the uniqueness field of the initiality witness on the forced arithmetic of $R$: any two Peano homs from that initial object into the forced Peano object of $S$ agree on carriers. Instantiate with the given homomorphism $f$ and with the canonical initial lift (the map underlying the universal forcing Peano equivalence). Equality of underlying functions follows immediately.
why it matters
This is the uniqueness half of the canonical-isomorphism package for forced arithmetics. Together with the zero/step preservation lemmas and the bundled Peano equivalence, it justifies calling the universal forcing map the unique structure-preserving isomorphism at the Peano-algebra layer, not merely some bijection.
It feeds the quantified certificate that packages existence-plus-uniqueness over all realizations. In the Recognition foundation this locks the arithmetic invariant extracted from any Law-of-Logic realization: different realizations cannot produce non-isomorphic Peano structure, and cannot produce two distinct isomorphisms either.
Open remainder stated in the module: preservation of $+$, $\times$, and $\le$ is not proved here, because the Peano surface carries only zero and step. That richer ordered-semiring iso is the next crown step for Part II.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.