distinction_forces_arithmeticOf
plain-language theorem explainer
Any inhabited type with two unequal points forces an initial Peano arithmetic whose carrier is canonically equivalent to LogicNat. Foundation workers cite this as the existential bridge from bare distinction data to the named ArithmeticOf object. The proof unpacks the existential hypothesis and applies the carrier-equivalence lemma for arithmeticOfDistinction.
Claim. Let $K$ be a type with decidable equality. If there exist $x,y\in K$ with $x\neq y$, then there exist such a pair together with a nonempty type equivalence between the Peano carrier of the arithmetic forced by that named distinction and $\mathrm{LogicNat}$ (the two-constructor naturals: identity and step).
background
This module is the named bridge on the distinction side of Universal Forcing. Compositionally one already had: a distinction yields a logic realization, that realization yields an ArithmeticOf, and the carrier identifies with LogicNat. The module packages the first two steps as a single constructor and states canonicity of the forcing map between distinctions.
LogicNat is the inductive type forced by the Law of Logic: identity (zero-cost multiplicative unit) and step (one generator iteration), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. The canonical arithmetic object on any logic realization is the initial Peano structure on LogicNat. The local claim is narrower and sharper: a distinction forces only the countable initial Peano arithmetic; the continuum is not forced from countable distinction certificates alone.
Upstream, arithmeticOfDistinction builds the named ArithmeticOf from a concrete pair $x\neq y$, and arithmeticOfDistinction_carrier_equiv_logicNat supplies the carrier equivalence used here.
proof idea
Term-mode existential packaging. Unpack the hypothesis $h$ to a concrete pair $x,y$ with $x\neq y$. Return that same pair together with a witness of Nonempty of the carrier equivalence, obtained by wrapping the already-proved lemma arithmeticOfDistinction_carrier_equiv_logicNat at those points. No new arithmetic content is derived; the theorem only lifts the pointwise carrier iso to an existential statement over bare distinction data.
why it matters
Closes the L5 register item (δ-native analysis / unification from distinction): from the bare proposition that $K$ has two distinct points, a named distinction forces initial Peano arithmetic with carrier LogicNat. It is the existential face of the named bridge; siblings supply the constructor, the Peano surface, countability, and uniqueness of the zero/step-preserving forcing map between two distinctions in one universe.
In the Recognition forcing chain this sits at the logic-to-arithmetic handoff before T5–T8 (J-uniqueness, φ, eight-tick octave, $D=3$). The module is explicit that the forced arithmetic lands at LogicNat, never at $\mathbb{R}$; reals enter only via a completion/display interface. No downstream consumers are recorded yet; the theorem is the public existential API for that bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.