arithmeticOfDistinction
plain-language theorem explainer
From any carrier with two distinct points, extract the forced arithmetic object of the distinction-native Law-of-Logic realization. Citation target for the Universal-Forcing distinction bridge (program register L5) and for every canonicity or Peano-surface lemma that follows. One-line wrapper: apply the universal forcing arithmetic extractor to the distinction realization.
Claim. Given a type $K$ with decidable equality and points $x,y\in K$ with $x\neq y$, let $R$ be the Law-of-Logic realization native to that distinction. Then there is a forced arithmetic object $\mathrm{ArithmeticOf}(R)$: an initial Peano object attached to $R$.
background
The module closes the Universal-Forcing distinction side. Previously the path from a bare distinction to arithmetic existed only as a composition: a distinction yields a $K$-native logic realization, the universal extractor turns that realization into an arithmetic object, and a separate identification shows the carrier is LogicNat. This definition supplies the missing named constructor.
An ArithmeticOf structure packages a Peano object together with a proof that it is initial among Peano objects for the given realization. The upstream extractor UniversalForcing.arithmeticOf builds that package from any Law-of-Logic realization. The distinction-side input is the realization produced by two unequal points on a decidable carrier.
Local scope is deliberately narrow: a distinction forces the countable initial Peano arithmetic (LogicNat), not the continuum. The real line enters only via a later completion or display interface.
proof idea
One-line wrapper. Feed the distinction-native logic realization into the already-proved universal extractor UniversalForcing.arithmeticOf. No new algebra; the definition merely names the composite so downstream lemmas can cite a single ArithmeticOf-valued map from distinction data.
why it matters
This is the named object the program register asks for: a Lean map from distinction data to ArithmeticOf. Every theorem in the module hangs off it. Downstream, the Peano-surface lemma records zero-not-a-step, injectivity of step, and induction; the carrier equivalence identifies the underlying set with LogicNat; countability follows at once. The forcing-map pair and the universal-objective theorem then prove that between any two distinctions the zero/step-preserving map exists and is unique (canonicity, not bare isomorphism). The certificate structure packages the whole package for any carrier that admits a distinction. Framework landmark: this is the distinction half of Universal Forcing, landing at the countable initial Peano object rather than at the reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.