peanoEquiv_unique
plain-language theorem explainer
Any two Peano-algebra isomorphisms between the forced arithmetics of two Law-of-Logic realizations agree as carrier maps. Citation target for anyone claiming the Universal Forcing arithmetic extraction is canonical, not merely existent. Proof is a one-line appeal to initiality uniqueness of the source forced Peano object.
Claim. Let $R$ and $S$ be Law-of-Logic realizations, and let $A_R$, $A_S$ be their forced Peano objects. If $e_1, e_2 : A_R \xrightarrow{\sim} A_S$ are structure-preserving isomorphisms (carrier equivalences sending zero to zero and commuting with successor), then the underlying functions of $e_1$ and $e_2$ are identical.
background
Universal Forcing Part II extracts a Peano object (carrier with zero and successor) from each Law-of-Logic realization. A realization supplies a carrier, a comparison cost, an identity element, and a step/generator action; the forced arithmetic is the Peano algebra read off that identity/step data.
A bare carrier bijection between two such Peano objects is weaker than an algebra isomorphism: it need not fix zero or commute with successor. This module upgrades the bare Universal Forcing bijection to a bundled Peano isomorphism (PeanoEquiv: equivalence plus map_zero and map_step).
Initiality of the forced Peano object of $R$ supplies a uniqueness principle for homomorphisms out of it: any two Peano homs $A_R \to B$ agree. That is the lever used here.
proof idea
One-line term proof. Forget each PeanoEquiv to its underlying Peano homomorphism via toHom, then apply the initiality uniqueness field of (forcedArith R).initial at the target Peano object (forcedArith S).peano. Initial uniqueness forces the two homs (hence their carrier maps) to coincide.
why it matters
This is the "canonical" half of canonically equivalent forced arithmetics: existence of a Peano iso is not enough; uniqueness of the underlying map rules out alternative structure-preserving renamings. It is packaged into universalForcingIsoCert (iso plus unique) and mirrored by strict_peanoEquiv_unique in the strict-realization layer.
In the Recognition foundation spine this sits in the arithmetic-extraction layer after the bare Universal Forcing carrier bijection, before ordered-semiring structure. It does not itself invoke T5–T8 or the RCL; it hardens the logical substrate those later forcing steps assume when they treat "the" natural numbers of a realization as unique up to unique Peano iso.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.