forcing_map_iff
plain-language theorem explainer
A map between Peano carriers of two arithmetic objects forced by logic realizations preserves zero and successor if and only if it is the canonical initial-object equivalence. Anyone proving uniqueness of arithmetic structure across realizations cites this. The proof is a two-sided constructor: uniqueness one way, the zero/step lemmas the other.
Claim. Let $A$ and $B$ be arithmetic objects forced by logic realizations $R$ and $S$, and let $f$ be any map between their Peano carriers. Then $f$ sends zero to zero and intertwines the successor operations if and only if $f$ equals the underlying function of the natural equivalence between the two initial Peano objects.
background
An ArithmeticOf object packages the Peano structure 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 lift into any other Peano object.
Given two such arithmetic objects $A$ and $B$, equivOfInitial builds the natural equivalence of carriers by lifting each way and verifying the round-trips. Its forward map is the unique zero-and-step morphism from $A$ into $B$.
This module develops canonical forcing for general realizations: maps that preserve the Peano generators are forced, not chosen. The present statement is the complete characterization of those maps.
proof idea
Split the biconditional with constructor.
Forward: from a pair of hypotheses (zero preserved, step intertwining), apply forcing_map_unique, which already shows any such map equals the forward map of equivOfInitial.
Reverse: after rfl identifying $f$ with that forward map, discharge the two generator identities by equivOfInitial_map_zero and equivOfInitial_map_step.
No induction is re-run here; both directions are one-line appeals to the uniqueness and generator lemmas already proved for the initial lift.
why it matters
In the Recognition Science foundation, arithmetic is not postulated: it is forced by any Law-of-Logic realization. This theorem closes the characterization for general realizations: the only zero-and-step map between forced arithmetic objects is the canonical initial equivalence.
It sits beside forcing_map_unique and feeds the parallel uniqueness statements for equivalences (forcing_equiv_unique) and the universal-forcing variants (universal_forcing_iff, universal_forcing_unique). Those siblings package the same idea at the level of full equivalences and of a single universal objective.
No downstream consumers are wired yet in the graph, but the result is the clean iff form a later universal-forcing or cross-realization comparison will quote. It is the map-level half of "uniqueness up to nothing" for Peano structure across realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.