arithmeticOfDistinction_peanoSurface
plain-language theorem explainer
Any two distinct points in a decidable carrier force an arithmetic object that satisfies the Peano surface axioms: zero is never a successor, successor is injective, and induction holds. Foundation authors cite this when packaging distinction data into a certified Peano arithmetic. The proof is a one-line term applying the universal-forcing Peano-surface lemma to the logic realization of that distinction.
Claim. Let $K$ be a type with decidable equality, and let $x,y\in K$ with $x\neq y$. The arithmetic object forced by the distinction $(x,y)$ carries the Peano surface: its zero is never a successor, its successor map is injective, and every predicate closed under zero and successor holds for the whole carrier.
background
This module is the named bridge on the distinction side of Universal Forcing. A bare inequality $x\neq y$ on a carrier $K$ is first turned into a LogicRealization, then extracted as an ArithmeticOf object (the structure forced by a Law-of-Logic realization: a Peano object together with an initiality witness). The constructor arithmeticOfDistinction packages that composite into a single named arithmetic.
LogicNat is the inductive naturals forced by the Law of Logic: constructors identity (zero-cost element) and step (one generator iteration), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. The Peano surface of a forced arithmetic is the Prop bundle of three classical Peano axioms on that object's carrier: zero is never a step, step is injective, and the induction schema holds for every predicate on the carrier.
The module's theorem-grade claim is that distinction forces only the countable initial Peano arithmetic, never the continuum; the real line enters only via a completion interface.
proof idea
One-line term proof. Instantiate the distinction $(x,y)$ as a logic realization via logicRealizationOfDistinction, then apply UniversalForcing.peano_surface to that realization. The universal-forcing lemma already proves that every arithmetic extracted from a logic realization carries the Peano surface; no local case analysis is needed.
why it matters
Fills the second theorem-grade bullet of the Distinction-to-Arithmetic bridge: the named distinction arithmetic is not merely an ArithmeticOf shell, it actually satisfies zero-not-step, injective successor, and induction. Downstream, distinctionArithmeticCert packages carrier-equivalence-to-LogicNat and countability into a certificate that every carrier forces initial arithmetic; this lemma is the Peano-surface half of that story (used compositionally with the carrier-iso siblings).
In the Universal Forcing program register this is the distinction-side half of canonicity: a distinction forces the countable initial Peano arithmetic (LogicNat), aligning with the module's honest scope that $\mathbb{R}$ is not forced from countable distinction certificates. It sits upstream of the unique zero/step-preserving forcing map between any two distinctions, which is the content of canonical equivalence of forced arithmetics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.