equivOfInitial_map_step
plain-language theorem explainer
The canonical equivalence between two forced Peano arithmetics intertwines successor: applying step then the map equals mapping then step. Anyone proving uniqueness or canonicity of zero/step-preserving maps between Law-of-Logic realizations cites this. The proof is a one-line projection of the initial-lift morphism's step-preservation.
Claim. Let $A$ and $B$ be forced arithmetics over Law-of-Logic realizations $R$ and $S$. Write $e$ for the natural equivalence of their Peano carriers induced by initiality. Then for every carrier element $x$ of $A$, $e(\mathrm{step}_A(x)) = \mathrm{step}_B(e(x))$.
background
An ArithmeticOf package is the Peano object forced by a Law-of-Logic realization, together with a proof that the object is initial among Peano objects. Initiality supplies a unique structure-preserving lift into any other Peano object; composing the two lifts yields a carrier equivalence equivOfInitial between any two forced arithmetics.
The Peano data include a distinguished zero and a step (successor) map on the carrier. The lift morphism is required to preserve both. This lemma isolates the step half of that preservation for the composite equivalence, in full universe generality (arbitrary realizations $R$, $S$).
The companion fact for zero is the sibling equivOfInitial_map_zero. Together they say the forcing equivalence is a Peano homomorphism, not merely a bare bijection of carriers.
proof idea
One-line term proof. The forward map of equivOfInitial A B is defined as (A.initial.lift B.peano).toFun. The initial-lift morphism already carries a map_step field asserting that it intertwines step. Instantiating that field at $x$ is the claim.
why it matters
This is the step half of the structure-preservation package that makes the forcing map canonical. Downstream, forcing_map_iff uses it to characterize every zero/step-preserving function as exactly the forcing equivalence; universal_objective packages existence, zero/step preservation, and uniqueness into the full Universal-Forcing objective across arbitrary realizations.
In the specialized CanonicalIso layer the same fact is re-exported for forced arithmetics of two realizations, and is fed into universalForcingPeanoEquiv, which builds the canonical Peano equivalence (bijection plus map_zero and map_step). That object is the precise content of the universal-forcing program's claim that ArithmeticOf R and ArithmeticOf S are canonically equivalent: not bare existence of some iso, but a unique zero/step-determined morphism.
Within the broader Recognition chain this sits in the foundation layer that forces arithmetic structure from the Law of Logic before the T0–T8 physical forcing (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.