forcing_equiv_unique
plain-language theorem explainer
Any two zero-and-step-preserving equivalences between the Peano carriers of forced arithmetics A and B are identical as functions. Cite this for uniqueness of the structure morphism between ArithmeticOf objects across Law-of-Logic realizations. The proof applies the unique-map lemma to each equivalence and equates the two characterizations.
Claim. Let $A$ and $B$ be arithmetic objects forced by Law-of-Logic realizations $R$ and $S$. If $e_1,e_2$ are equivalences of their Peano carriers that both send zero to zero and commute with successor, then $e_1=e_2$ as functions $A.\mathrm{carrier}\to B.\mathrm{carrier}$.
background
An ArithmeticOf object packages a Peano structure forced by a Law-of-Logic realization: a carrier with zero and step, together with an initiality witness. The canonical choice uses LogicNat (identity as zero-cost unit, step as one generator iterate), but here the carriers of $A$ and $B$ may be genuinely different Peano objects in different universes.
The local setting is CanonicalForcing under UniversalForcing: structure morphisms between forced arithmetics, not bare existence of some iso. The companion uniqueness result for plain maps (not necessarily equivalences) states that any two zero/step-preserving functions $A.\mathrm{carrier}\to B.\mathrm{carrier}$ coincide; that is the lemma this theorem reduces to.
Initiality of the Peano object is what makes the zero/step data determine a unique morphism out of $A$, so two equivalences that both preserve that data cannot differ as functions.
proof idea
One short reduction. Cast each equivalence to an ordinary function and apply forcing_map_unique to both: that lemma says any zero-and-step-preserving map $A.\mathrm{carrier}\to B.\mathrm{carrier}$ equals the unique such map. The two applications therefore yield the same characterization of $e_1$ and of $e_2$, and a rewrite finishes the equality of functions. No separate induction or initiality argument is replayed here.
why it matters
This is the uniqueness half of the universal-forcing claim for general realizations: not merely that some iso exists between forced arithmetics, but that any two zero/step-preserving equivalences are the same map. The module comment frames the full objective as a canonical, determined morphism between ArithmeticOf R and ArithmeticOf S across admissible realizations, contrasting the strict-realization case (where the carrier is concretely LogicNat and the map is the identity).
Sibling results (forcing_map_unique, universal_forcing_equiv_unique, universal_forcing_iff) assemble existence-plus-uniqueness into the full canonical equivalence. In the Recognition foundation chain this pins the arithmetic content forced by the Law of Logic as realization-independent: different realizations may present different Peano carriers, yet the structure morphism between them is unique. No downstream uses are recorded yet; the declaration closes the uniqueness side of the general-realization story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.