forcing_map_unique
plain-language theorem explainer
Any zero-and-step-preserving map between the Peano carriers of two forced arithmetics equals the canonical forcing map given by initiality. Foundation and universal-forcing arguments cite this for canonicity: the map is fixed by zero/step data alone. The proof packages the map as a Peano homomorphism and applies uniqueness of the initial lift, then unfolds the definition of the initial equivalence.
Claim. Let $A$ and $B$ be arithmetics forced by Law-of-Logic realizations $R$ and $S$. If $f$ maps the Peano carrier of $A$ to that of $B$ and satisfies $f(0_A)=0_B$ and $f(S_A x)=S_B(f x)$ for all $x$, then $f$ equals the forward map of the canonical equivalence induced by initiality of the two Peano objects.
background
A Peano object is a carrier type with a distinguished zero and a unary step map. Homomorphisms are functions that send zero to zero and intertwine step. An ArithmeticOf structure packages a Peano object together with a proof that it is initial among Peano objects: there is a unique homomorphism out of it into any other Peano algebra.
The natural equivalence between two such forced arithmetics is built by lifting each Peano object into the other via initiality; its forward map is exactly the unique homomorphism from $A$'s Peano object to $B$'s. The present module develops general canonicity for these maps across arbitrary Law-of-Logic realizations (not only distinction-based ones).
Upstream, initiality supplies both the lift used to define the equivalence and the uniqueness clause that any two homomorphisms out of an initial Peano object coincide.
proof idea
Form the Peano homomorphism whose underlying function is $f$, using the given zero and step preservation hypotheses. Invoke uniqueness of morphisms out of the initial Peano object of $A$ into the Peano object of $B$, comparing that homomorphism to the canonical lift. The resulting equality of underlying functions, rewritten by the definition of the initial equivalence, is the claim. Short term-mode argument: one uniqueness application plus simpa.
why it matters
This is the general canonicity lemma for forced arithmetic: zero/step data alone determine the map, with no representational freedom. It feeds the biconditional characterization of forcing maps, uniqueness of zero/step-preserving equivalences, and the full universal-forcing objective (existence of a structure-preserving equivalence that is the unique zero/step-preserving map between any two forced arithmetics). Downstream, the distinction-specialized canonicity theorem reuses the same idea, and the forced-semiring certificate relies on the resulting unique forcing function. In the Recognition foundation stack this closes the "canonical equivalence of ArithmeticOf across admissible realizations" clause of the universal-forcing program, before specialization to concrete carriers or semiring structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.