universal_objective
plain-language theorem explainer
Any two forced arithmetics over Law-of-Logic realizations (sharing a carrier universe) admit a unique zero-and-successor-preserving equivalence of Peano carriers. This is the full-generality universal-forcing objective: not bare existence of an iso, but a canonical determined morphism. Cite it for the program's claim that ArithmeticOf is unique across admissible realizations. The proof is a four-component term packaging the initial-object lift with uniqueness of structure maps.
Claim. Let $R$ and $S$ be Law-of-Logic realizations, and let $A$ and $B$ be arithmetics forced by $R$ and $S$ respectively (with Peano carriers in a common universe). Then there exists an equivalence $e$ of the Peano carriers such that $e(0_A)=0_B$, $e(S_A x)=S_B(e x)$ for every $x$, and every map $f$ that preserves zero and successor equals $e$.
background
An ArithmeticOf R is the arithmetic object forced by a Law-of-Logic realization $R$: a Peano object together with a proof that it is initial among Peano objects. Initiality supplies a unique structure morphism out of that Peano object into any other, so two initial Peano objects are canonically equivalent.
The natural equivalence equivOfInitial is built by lifting each initial object into the other and taking the resulting pair of maps as inverse functors. Sibling lemmas record that this equivalence sends zero to zero and commutes with successor, and that any other zero/step-preserving function coincides with it.
The local setting is CanonicalForcing inside UniversalForcing: the goal is the program claim that forced arithmetics over arbitrary realizations are related by a unique structure morphism, not merely that some isomorphism exists.
proof idea
Pure term proof assembling four already-proved pieces into an existential witness. The equivalence is equivOfInitial A B (the initial-object lift). Zero preservation is equivOfInitial_map_zero; successor commutation is equivOfInitial_map_step. Uniqueness of any competing zero/step map is discharged by forcing_map_unique. No further tactics or case analysis.
why it matters
This is the precise content of the universal-forcing program's "canonical equivalence of ArithmeticOf R and ArithmeticOf S across admissible realizations": existence plus canonicity in one statement, at full universe generality. Downstream, distinction_arithmetic_universal_objective specializes it to arithmetics forced by bare distinctions, so the same unique zero/step equivalence holds whenever two unequal pairs generate Peano structure. Unlike the strict-realization certificate (where carriers are concretely LogicNat and the map is identity), carriers here may be genuinely different Peano objects; the iso is nontrivial yet still the only structure morphism. It sits in the Foundation layer that turns Law-of-Logic realizations into unique arithmetic, feeding the path from distinction primitives toward the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.