distinctionArithmeticCert
plain-language theorem explainer
For every carrier type with decidable equality, every bare distinction forces an initial Peano arithmetic whose carrier is LogicNat (hence countable) and which carries the full Peano surface. Citation target for the Universal Forcing δ-native bridge from inequality data to ArithmeticOf. Term-mode assembly of three already-proved component lemmas into the certificate structure.
Claim. For every type $K$ with decidable equality, and every pair $x,y\in K$ with $x\neq y$, the distinction-forced arithmetic object has carrier equivalent to $\mathrm{LogicNat}$, that carrier is countable, and the object carries the Peano surface (zero is never a successor, successor is injective, and induction holds).
background
This module is the named bridge on the distinction side of Universal Forcing. Separately proved pieces already ran
$$(\exists x,y:K,,x\neq y)\to\mathrm{LogicRealization}\to\mathrm{ArithmeticOf}\to\mathrm{carrier}\simeq\mathrm{LogicNat},$$
but there was no single certificate packaging the forced arithmetic as initial Peano with countable LogicNat carrier.
arithmeticOfDistinction is the named ArithmeticOf of one distinction. Upstream, arithmeticOfDistinction_peanoSurface records that its zero is never a step, step is injective, and induction holds (via UniversalForcing.peano_surface on the logic realization). arithmeticOfDistinction_carrier_equiv_logicNat identifies the carrier with LogicNat; countability then follows by transfer from $\mathbb{N}$. The certificate structure bundles exactly these three facts for every distinction on $K$.
proof idea
Term-mode construction of the three certificate fields. forces_initial_arithmetic wraps the carrier equivalence as a Nonempty witness via arithmeticOfDistinction_carrier_equiv_logicNat. forced_arithmetic_countable is a direct application of arithmeticOfDistinction_carrier_countable. peano_surface applies arithmeticOfDistinction_peanoSurface. No new algebra: pure packaging of prior theorems.
why it matters
Closes the L5 register item (δ-native analysis / unification from distinction) by supplying a single Prop-valued certificate that every distinction forces initial countable Peano arithmetic. Sits at the end of the DistinctionToArithmetic weld: named ArithmeticOf constructor, Peano surface, LogicNat identification, countability, and (nearby) canonicity of the forcing map between distinctions. Honest scope is built in: a distinction forces LogicNat, never $\mathbb{R}$; the continuum enters only through a completion/display interface (real_not_forced_from_distinction). No downstream users yet in the graph; this is the export surface for the bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.