equivOfInitial_map_zero
plain-language theorem explainer
The canonical equivalence between two initial Peano objects, each forced by a Law-of-Logic realization, sends zero to zero. Anyone citing the universal-forcing objective or the structure-preserving Peano equivalence needs this fact. The proof is a one-line appeal to zero-preservation of the unique initial lift.
Claim. Let $A$ and $B$ be arithmetic objects forced by Law-of-Logic realizations $R$ and $S$. Write $e$ for the natural equivalence of their Peano carriers induced by initiality. Then $e(0_A) = 0_B$.
background
An ArithmeticOf package is the arithmetic forced by a Law-of-Logic realization: a Peano object together with a proof that it is initial among Peano objects. Initiality supplies a unique structure-preserving morphism out of that object into any other Peano object.
Given two such packages $A$ and $B$, the natural equivalence of carriers is built by lifting each Peano structure along the other's initiality witness: the forward map is the unique morphism $A\to B$, the inverse is the unique morphism $B\to A$. The present lemma records that this forward map preserves zero.
The local setting is CanonicalForcing: general (universe-polymorphic) realizations, not yet specialized to the forced arithmetic of a single realization. The companion step-preservation lemma sits immediately below.
proof idea
One-line term proof. The forward map of equivOfInitial A B is definitionally the unique initial lift of $B$'s Peano object out of $A$. That lift is a Peano morphism, so its map_zero field is exactly the required equality. No further rewriting or case analysis.
why it matters
This is the zero half of the structure-preservation package for the universal forcing equivalence. Downstream, forcing_map_iff uses it to characterize zero/step-preserving maps as exactly the canonical equivalence; universal_objective packages existence, zero/step preservation, and uniqueness into the full universal-forcing claim ("not bare existence of some iso, but a canonical, determined morphism").
In CanonicalIso the same fact is specialized to forced arithmetics and fed into universalForcingPeanoEquiv, the structure-preserving Peano isomorphism between any two realizations. Within the Recognition foundation this is the arithmetic backbone of the forcing chain: once zeros and steps match uniquely across realizations, the Peano skeleton (and everything built on it) is realization-independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.