equivOfInitial_map_zero
plain-language theorem explainer
Between any two Law-of-Logic realizations, the universal forcing carrier bijection of their forced Peano arithmetics sends zero to zero. Anyone packaging that bijection as a Peano-algebra homomorphism cites this fact. The proof is a one-line projection of the initial-object lift's built-in zero preservation.
Claim. For any two Law-of-Logic realizations $R$ and $S$, if $A_R$ and $A_S$ are their forced arithmetic objects, then the natural equivalence of initial Peano objects satisfies $e(0_{A_R}) = 0_{A_S}$.
background
A Law-of-Logic realization supplies a carrier, a comparison cost, an identity element, and a step/generator action. From that data one extracts an arithmetic object: a Peano algebra (carrier with zero and successor) together with a proof that it is initial among Peano objects.
Initiality yields a unique Peano homomorphism out of the forced arithmetic into any other Peano object. The natural equivalence between two forced arithmetics is defined by composing those unique lifts in both directions; its underlying function is therefore the unique zero-and-step-preserving map from one carrier to the other.
This module sits in the arithmetic-extraction layer of Universal Forcing. The bare spine already gives a carrier bijection between forced arithmetics of any two realizations. That bijection is a priori only a set equivalence; the present lemma is the first half of upgrading it to a Peano-algebra homomorphism.
proof idea
One-line term proof. The universal forcing equivalence is defined as the unique lift of the target Peano object out of the source's initiality witness. That lift is already a Peano homomorphism, so its map_zero field is exactly the required identity. No extra algebraic work is needed beyond projecting that field.
why it matters
This is the zero half of the Peano-homomorphism upgrade that CanonicalIso exists to deliver. Downstream, universalForcingPeanoEquiv packages the bare equivalence together with this lemma and its step twin into a bundled structure-preserving isomorphism. The same fact is re-exported at full universe generality in CanonicalForcing, and it feeds forcing_map_iff (the complete characterization of the forcing map) and universal_objective (the unique zero/step-preserving equivalence between any two forced arithmetics).
In the Recognition framework this is the arithmetic-layer content of canonical equivalence across admissible realizations: not bare existence of some bijection, but a determined morphism fixed by zero and successor. Ring operations and order are still out of scope; PeanoObject carries only zero and step, so the ordered-semiring iso remains the open Part II crown.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.