equivOfInitial_map_step
plain-language theorem explainer
The universal forcing bijection between forced Peano carriers of any two Law-of-Logic realizations intertwines the successor maps. Anyone citing the upgrade from bare carrier equivalence to Peano-algebra homomorphism needs this. The proof is a one-line appeal to the map_step field of the unique initial lift.
Claim. For any two Law-of-Logic realizations $R$ and $S$, and any element $x$ of the forced Peano carrier of $R$, the canonical initiality equivalence $e$ satisfies $e(\mathrm{step}_R(x)) = \mathrm{step}_S(e(x))$.
background
Universal Forcing extracts, from each Law-of-Logic realization, an arithmetic object ArithmeticOf: a Peano carrier with zero and step, together with a proof of initiality among Peano objects. Initiality supplies a unique homomorphism out of that object into any other Peano object; composing the two lifts yields a bare carrier bijection equivOfInitial between any two forced arithmetics.
A bare bijection need not respect zero or successor. This module (CanonicalIso) sits in the arithmetic-extraction layer of Universal Forcing Part II and upgrades that bijection to a Peano-algebra isomorphism. The companion statement for zero is already available; the present result is the successor half.
Upstream, equivOfInitial is defined by sending $x$ along the unique lift of the target Peano object out of the source's initial structure. That lift is a Peano homomorphism by construction, so it already carries a map_step field; the theorem simply specializes that field to the forced arithmetics of $R$ and $S$.
proof idea
One-line term proof. Unfold equivOfInitial on the forced arithmetics: its forward map is exactly the unique initial lift of $S$'s Peano object out of $R$'s initial structure. Apply that lift's built-in map_step at $x$. No further rewriting is required.
why it matters
Without successor-commutation the universal forcing map is only a set bijection, not a number-system isomorphism. This lemma is half of the structure package: it is the map_step field of universalForcingPeanoEquiv, the bundled Peano equivalence between forced arithmetics of any two realizations.
Downstream it feeds the general-realization versions in CanonicalForcing (forcing_map_iff, universal_objective), which characterize the forcing map as the unique zero-and-step-preserving function and state the full Universal-Forcing objective: canonical, not merely existential, equivalence of forced arithmetics across admissible realizations.
In the broader RS forcing chain this is arithmetic infrastructure rather than a T0–T8 landmark: it makes the extracted Peano content realization-independent at the algebra level. Ring operations and order are explicitly out of scope here; the module doc flags the ordered-semiring iso as remaining Part II work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.