arithmeticOfDistinction_carrier_equiv_logicNat
plain-language theorem explainer
Given any carrier with two distinct points, the Peano carrier of the arithmetic forced by that distinction is canonically equivalent to LogicNat (the Law-of-Logic naturals). Anyone proving the δ-native lower bound that distinction forces only countable initial Peano arithmetic cites this identification. The definition is a one-line re-export of the upstream distinction-to-LogicNat equivalence.
Claim. For any type $K$ with decidable equality and any $x,y\in K$ with $x\neq y$, the Peano carrier of the arithmetic object forced by that distinction is equivalent to $\mathrm{LogicNat}$: $(\mathrm{ArithmeticOf}(\mathrm{distinction}))_{\mathrm{Peano}}.\mathrm{carrier}\simeq\mathrm{LogicNat}$.
background
This module is the named bridge on the distinction side of Universal Forcing. Separately proved pieces (instantiation of a Law-of-Logic realization from two unequal points, extraction of an ArithmeticOf, and carrier identification) are welded into a single constructor from distinction data to forced arithmetic, plus canonicity of the forcing map.
LogicNat is the inductive type 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 sibling arithmeticOfDistinction builds the forced ArithmeticOf by extracting Universal Forcing arithmetic from the $K$-native logic realization of $x\neq y$.
The module states the δ-native scope honestly: a distinction forces the countable initial Peano object and nothing more; the continuum is not forced from countable distinction certificates.
proof idea
One-line wrapper. It applies the upstream identification distinction_arithmetic_equiv_logicNat at the same universe levels, specialized to the given distinction data $x,y,hxy$. No extra algebraic work: the equivalence is inherited from the compositional route (logic realization of distinction → Universal Forcing arithmetic → carrier ≃ LogicNat).
why it matters
This is one of the THEOREM-grade named pieces the module advertises: the carrier of distinction-forced arithmetic is LogicNat. Downstream, arithmeticOfDistinction_carrier_countable transports countability along the inverse equivalence (LogicNat ≃ ℕ), stating the δ-native lower fact that distinction forces exactly the countable initial Peano object. distinction_forces_arithmeticOf packages existence of such a named distinction with nonempty carrier equivalence to LogicNat from bare $\exists x,y,,x\neq y$. The certificate distinctionArithmeticCert records both the equivalence and countability for every carrier.
In the Universal Forcing program this closes the identification half of the distinction→ArithmeticOf bridge. It does not touch T5–T8 (J-cost, φ, eight-tick, D=3); those sit later. The companion non-claim is that ℝ is not forced from distinction alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.