distinction_arithmetic_universal_objective
plain-language theorem explainer
Any two distinctions (pairs of unequal elements, possibly on different carriers) force Peano arithmetics related by a unique zero-and-successor-preserving equivalence of carriers. Researchers citing the Universal Forcing canonicity clause on the distinction side use this statement. The proof is a one-line application of the general ArithmeticOf universal-objective lemma to the two named distinction arithmetics.
Claim. Let $K,L$ be types with decidable equality, $x\neq y$ in $K$ and $a\neq b$ in $L$. Let $A_{xy}$ and $A_{ab}$ be the Peano arithmetic objects forced by these distinctions. Then there is an equivalence $e:A_{xy}.\mathrm{carrier}\simeq A_{ab}.\mathrm{carrier}$ with $e(0_{xy})=0_{ab}$ and $e(S_{xy}p)=S_{ab}(e p)$ for all $p$, and every other zero/step-preserving map $f$ equals $e$.
background
This module is the named bridge on the distinction side of Universal Forcing. A distinction is simply a witness $x\neq y$ in a type with decidable equality. From that witness one builds a Law-of-Logic realization, extracts an ArithmeticOf object (a Peano surface plus an initiality certificate), and identifies the carrier with LogicNat, the two-constructor inductive naturals forced by the Law of Logic (identity as zero-cost unit, step as one generator iterate).
Until this module, the route existed only compositionally: distinction to logic realization, then to ArithmeticOf, then carrier equivalence with LogicNat. Here the named constructor supplies the forced arithmetic of one distinction directly, and the present theorem packages existence plus uniqueness of the structure map between any two such objects.
Upstream, ArithmeticOf is the arithmetic forced by a Law-of-Logic realization; its universal-objective lemma already states that any two such arithmetics are related by a unique zero/step-preserving equivalence. LogicNat is countable by construction, which later pins the $\delta$-native scope: distinction forces countable Peano arithmetic, never the continuum.
proof idea
One-line term wrapper. Instantiate the general lemma ArithmeticOf.universal_objective at the two forced objects arithmeticOfDistinction x y hxy and arithmeticOfDistinction a b hab. That lemma already returns an equivalence of Peano carriers that preserves zero and step and is the unique map with those properties; no further case analysis or induction is performed here.
why it matters
This is the canonicity half of the distinction-to-arithmetic bridge demanded by the Universal Forcing program register ($\delta$-native analysis / unification from distinction, L5). Sibling results already give the named constructor, the Peano surface axioms, carrier equivalence with LogicNat, and countability. The present theorem upgrades bare isomorphism to unique zero/step-preserving map between any two distinctions in the same universe, which is exactly the "canonical equivalence of ArithmeticOf" content of the program note.
It sits beside the honest scope statement that follows in the module: the forced arithmetic is countable LogicNat; the real line is not forced from distinction certificates (cardinality obstruction). In the broader Recognition chain this anchors the arithmetic substrate that later forcing steps (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) build on, without smuggling continuum structure in at the distinction layer. No downstream users are recorded yet; the theorem is a terminal canonicity seal for this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.