universal_forcing_unique
plain-language theorem explainer
Between any two strict logic realizations, a map of their forced Peano carriers that sends zero to zero and intertwines the step maps must equal the universal forcing map. Anyone proving canonicity of forced arithmetic or uniqueness of structure morphisms cites this. The argument is initiality: package the data as a Peano homomorphism and apply uniqueness of the initial lift.
Claim. Let $R$ and $S$ be strict logic realizations, and let $f$ be a function from the Peano carrier forced by $R$ to that forced by $S$. If $f(0_R)=0_S$ and $f(\mathrm{step}_R(x))=\mathrm{step}_S(f(x))$ for all $x$, then $f$ equals the underlying function of the universal forcing map $R\to S$.
background
A Peano object is a carrier type with a distinguished zero and a unary step map. Homomorphisms are functions preserving zero and step. An arithmetic object forced by a logic realization pairs a Peano object 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 initial arithmetics is built by lifting each Peano object along the other's initiality; its forward map is exactly that unique lift. Strict logic realizations supply forced arithmetics via this construction, so maps between their carriers are constrained by initiality alone.
Local setting: CanonicalForcing packages the universal forcing map between strict realizations and records that it is the unique zero/step-preserving map, with no leftover representational choice.
proof idea
Form the Peano homomorphism whose underlying function is $f$ and whose zero/step laws are the given hypotheses. Initiality of the source arithmetic supplies a uniqueness statement comparing any two homs into the target Peano object. Instantiate that uniqueness on the packaged hom and on the canonical initial lift. Simplify the resulting equality using the definitions of the universal forcing map and of the natural equivalence of initial Peano objects; both reduce to the lift's underlying function, so $f$ equals that function.
why it matters
This is the canonicity half of universal forcing: structure-preserving maps between forced arithmetics are unique, so the equivalence is fixed by zero/step data alone. Downstream, the complete characterization (a map is the forcing map iff it preserves zero and step) uses this as one direction; uniqueness of two zero/step-preserving equivalences as functions is the same fact lifted to isomorphisms; the canonicity certificate records it as the uniqueness field; and uniqueness of the forcing map as a semiring homomorphism on the LogicNat presentation is a direct restatement.
In the Recognition foundation this closes representational freedom at the arithmetic layer that every later forcing step (including the T0–T8 chain) sits on: once logic is realized strictly, the induced natural numbers and their morphisms are forced, not chosen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.