distinction_forcing_map_unique
plain-language theorem explainer
Any zero-and-successor-preserving map between the Peano carriers forced by two distinctions equals the canonical forcing equivalence. Cite this for canonicity of distinction-forced arithmetic: the map is fixed by the distinction data alone. The proof is a one-line application of uniqueness for initial Peano objects to the two distinction-forced arithmetics.
Claim. Let $K$ and $L$ be types with decidable equality, and fix distinctions $x \neq y$ in $K$ and $a \neq b$ in $L$. Write $A_{xy}$ and $A_{ab}$ for the arithmetic objects forced by these distinctions. If $f$ maps the Peano carrier of $A_{xy}$ to that of $A_{ab}$ and preserves zero and the successor step, then $f$ equals the underlying function of the canonical forcing equivalence $A_{xy} \simeq A_{ab}$.
background
This module is the named bridge from a bare distinction to forced arithmetic in the Universal-Forcing program. Given a carrier with two distinguishable points, one first builds a Law-of-Logic realization, then extracts an ArithmeticOf object: a Peano surface together with an initiality witness. The named constructor packages that extraction so a distinction maps directly to its forced arithmetic.
Between any two such objects the canonical forcing equivalence is the unique initial-object isomorphism of their Peano surfaces (zero and step preserved both ways). The present theorem is the uniqueness half: any map that merely preserves zero and step must coincide with that canonical map.
Upstream, the general uniqueness lemma for initial Peano objects supplies the algebraic content; the distinction-side definitions only specialize the carriers and the two forced arithmetics.
proof idea
One-line term wrapper. Instantiate the general uniqueness theorem for forcing maps between initial Peano objects at the two distinction-forced arithmetics, passing the given zero-preservation and step-commutation hypotheses. No extra case analysis or induction is performed here; all work sits in the upstream uniqueness lemma.
why it matters
Canonicity, not bare existence of an isomorphism, is what the Universal-Forcing register demands: the equivalence of forced arithmetics must be the unique zero/step-preserving map, so there is no representational freedom once the distinction data are fixed. Together with the existence of the forcing map, this feeds the universal-objective statement that packages existence-plus-canonicity for any pair of distinctions in one universe.
In the broader foundation chain this pins the countable Peano arithmetic forced by distinction (landing at LogicNat, never at the continuum). The module is explicit that the real line is not forced from countable distinction certificates; uniqueness here concerns only the discrete initial arithmetic. That closes the canonicity clause of the distinction-side half of Universal Forcing without touching later geometric or continuum structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.