universal_forcing_equiv_unique
plain-language theorem explainer
Any two Peano equivalences between the arithmetic carriers of strict logic realizations that preserve zero and successor are identical as functions. Cited whenever one needs the forced arithmetic isomorphism to be unique, not merely existent. Proof applies the unique-forcing-map lemma to each equivalence and rewrites.
Claim. Let $R$ and $S$ be strict logic realizations, and let $e_1,e_2$ be equivalences between their Peano carriers. If both send zero to zero and commute with successor, then $e_1=e_2$ as functions on the underlying carriers.
background
In the Universal Forcing / Canonical Forcing development, each strict logic realization $R$ carries an arithmetic object arith R whose Peano surface supplies a carrier, zero, and successor. The canonical arithmetic object is realization-independent at the type level: "the realization supplies the interpretation; initiality supplies the invariant arithmetic content" (ArithmeticOf.canonical).
A structure morphism of Peano carriers is a map sending zero to zero and commuting with step. Equivalences with those two preservation laws are the candidate isomorphisms between the forced arithmetics of two realizations. The sibling lemma universal_forcing_unique already says there is at most one such map of carriers (not necessarily bijective). The present statement lifts that uniqueness to the level of equivalences: two Peano-preserving equivalences cannot differ even as bare functions.
Local setting is the StrictLogicRealization namespace, where forcing is meant to be canonical rather than representational.
proof idea
Short tactic proof. Coerce each equivalence $e_1,e_2$ to an ordinary carrier map, then apply universal_forcing_unique R S to each, using the given zero- and step-preservation hypotheses. That lemma returns that both maps equal the unique forcing map from $R$ to $S$. Rewrite along those two equalities to conclude $e_1=e_2$ as functions. No separate bijectivity or inverse argument is needed; uniqueness of the underlying map already forces the equivalences to coincide.
why it matters
Closes the uniqueness half of the module certificate: "forcing is canonical, not representational. The forced arithmetic equivalence between any two strict realizations exists, preserves the full Peano structure, and is the unique such map." Doc-comment frames it as uniqueness up to nothing: the forcing isomorphism is not one iso among many, but the only structure morphism.
Together with the existence and preservation siblings (universal_forcing_map_zero, universal_forcing_map_step, universal_forcing_unique, universal_forcing_iff), it pins the arithmetic content shared by all strict realizations to a single Peano isomorphism class. That is the foundation-level claim that arithmetic is forced rather than chosen. No downstream uses are recorded yet; the declaration sits at the end of the StrictLogicRealization uniqueness cluster. It does not itself invoke T5–T8 or the RCL, but it underwrites the claim that whatever physics is later read off forced arithmetic is independent of which strict realization one started from.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.