distinction_forcing_map
plain-language theorem explainer
Canonical equivalence of Peano carriers forced by any two distinctions (in one universe). Anyone citing Universal Forcing canonicity on the distinction side uses this map as the named bridge. Proof is a one-line wrapper: the natural initial-object equivalence between the two forced ArithmeticOf objects.
Claim. Let $K$ and $L$ be types with decidable equality, and let $x \neq y$ in $K$ and $a \neq b$ in $L$ be distinctions. Write $A_{x,y}$ and $A_{a,b}$ for the arithmetics forced by those distinctions. Then there is a canonical equivalence $A_{x,y}.\mathrm{peano}.\mathrm{carrier} \simeq A_{a,b}.\mathrm{peano}.\mathrm{carrier}$ between their Peano carriers.
background
This module is the named bridge on the distinction side of Universal Forcing: it turns a bare distinction (two unequal points in a carrier) into a forced ArithmeticOf object and proves that object is canonical across distinctions.
arithmeticOfDistinction extracts, from $x \neq y$ on $K$, the Law-of-Logic realization native to that distinction and then the forced arithmetic of that realization. The resulting structure carries a Peano surface (zero, step, induction) whose carrier is identified with the countable initial Peano arithmetic (LogicNat), not with the continuum.
ArithmeticOf packages a Peano object together with an initiality witness. Between any two such initial Peano objects there is a natural equivalence equivOfInitial, built by mutual initial lifts. That is the only upstream ingredient this definition needs.
proof idea
One-line wrapper. Apply ArithmeticOf.equivOfInitial to the two forced arithmetics arithmeticOfDistinction x y hxy and arithmeticOfDistinction a b hab. The resulting map is the mutual initial lift of the two Peano objects, hence an equivalence of carriers. No extra algebraic work.
why it matters
This is the named forcing map the module exists to supply: the single object that sends distinction data to a structure-preserving carrier equivalence, with no representational choice left open. Downstream, distinction_forcing_map_unique cites it as the unique zero/step-preserving map between any two distinction-forced arithmetics (canonicity, not bare iso). Together with the sibling uniqueness and universal-objective theorems, it closes the Universal Forcing register item that any two distinctions force the same countable initial Peano arithmetic up to a unique structure map. It does not touch the continuum: the module separately records that $\mathbb{R}$ is not forced from countable distinction certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.