arithmeticOfDistinction_carrier_countable
plain-language theorem explainer
Any two distinct points in a decidable type force an arithmetic object whose Peano carrier is countable. Citation is for the δ-native scope claim that distinction yields only the initial countable Peano structure, never a continuum. The proof transfers countability along the carrier equivalence with LogicNat, itself equivalent to ℕ.
Claim. Let $K$ be a type with decidable equality, and let $x,y\in K$ with $x\neq y$. Write $A$ for the arithmetic object forced by that distinction. Then the Peano carrier of $A$ is a countable type.
background
This module is the named bridge from a bare distinction (two unequal points of a carrier $K$) to a forced ArithmeticOf object. Compositionally the route already existed: distinction data yields a logic realization, which extracts an arithmetic, which is identified with LogicNat. Here those steps are packaged as a single constructor arithmeticOfDistinction.
LogicNat is the inductive Peano carrier forced by the Law of Logic: constructors identity (zero-cost unit) and step (one generator iterate), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. The recovery equivalence equivNat identifies LogicNat with ordinary $\mathbb{N}$ by round-trip maps toNat/fromNat.
The sibling result arithmeticOfDistinction_carrier_equiv_logicNat states that the Peano carrier of the distinction-forced arithmetic is canonically equivalent to LogicNat. Countability is the immediate corollary recorded here. The module's honest scope line is that distinction forces only this countable initial object; the continuum is not forced from countable distinction certificates.
proof idea
Term-mode transfer of countability along equivalences. First obtain Countable LogicNat from Countable Nat via Countable.of_equiv applied to the symmetric recovery equivalence LogicNat.equivNat. Then apply Countable.of_equiv again along the symmetric carrier equivalence arithmeticOfDistinction_carrier_equiv_logicNat, landing countability on the Peano carrier of arithmeticOfDistinction. No induction or Peano axioms are reopened; the argument is pure transport.
why it matters
Feeds the certificate distinctionArithmeticCert, which packages two facts for every carrier: the forced arithmetic is initial (carrier $\simeq$ LogicNat) and the forced arithmetic is countable. The latter field is exactly this theorem.
In the Universal Forcing program this is the δ-native lower bound: a named distinction forces precisely the countable initial Peano object and nothing larger. The module pairs it with real_not_forced_from_distinction, so the real line enters only through a completion or display interface, not from distinction alone. That separation keeps the forcing chain honest before later steps (T5–T8, RCL, continuum display) are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.