DistinctionArithmeticCert
plain-language theorem explainer
Packages three properties that any distinction on a carrier forces: an initial Peano arithmetic whose carrier is equivalent to the logic-forced naturals, countability of that carrier, and the full Peano surface. Downstream, the universal certificate theorem instantiates this structure for every carrier. As a Prop-valued structure it is a definitional certificate interface, not a proved statement.
Claim. For a type $K$ with decidable equality, a distinction-to-arithmetic certificate is the conjunction of: (i) every pair of distinct elements $x,y\in K$ forces an arithmetic object whose Peano carrier is equivalent to the logic-forced naturals; (ii) that carrier is countable; (iii) the forced arithmetic satisfies the Peano surface (zero $\neq$ successor, successor injective, induction).
background
This module is the named bridge on the distinction side of Universal Forcing. Separately proved pieces (logic realization of a distinction, extraction of an ArithmeticOf, identification of the carrier with the logic-forced naturals) are welded into a single constructor from distinction data, plus canonicity of the forcing map between distinctions.
The logic-forced naturals are the two-constructor inductive type with identity (zero-cost element) and step (one generator iteration), mirroring the orbit ${1,\gamma,\gamma^2,\ldots}$. An arithmetic object forced by a Law-of-Logic realization pairs a Peano object with an initiality witness. Its Peano surface is the Prop that zero is never a successor, successor is injective, and induction holds.
The module states the $\delta$-native scope honestly: a distinction forces only the countable initial Peano arithmetic, never the continuum; the real line enters only via completion or display, not from distinction alone.
proof idea
No proof body: this is a Prop-valued structure definition. It names three fields that any certificate instance must supply: nonempty equivalence of the forced Peano carrier to the logic-forced naturals; countability of that carrier; and the Peano-surface Prop on the forced arithmetic object. Instantiation is deferred to the downstream theorem that fills the fields from the already-proved carrier-equivalence, countability, and Peano-surface lemmas for the named distinction-to-arithmetic constructor.
why it matters
This is the certificate interface the Universal Forcing program register asks for on the distinction side (L5: $\delta$-native analysis / unification from distinction). It packages the theorem-grade facts already established in-module: the named arithmetic object of one distinction, its Peano surface, carrier equivalence to the logic-forced naturals, and countability.
The sole direct consumer is the theorem that the certificate holds for every carrier: it fills the three fields by applying the carrier-equivalence, countability, and Peano-surface results for the distinction constructor. Together with the forcing-map uniqueness results in the same module, this closes the canonicity half of "canonical equivalence of arithmetic objects" without claiming that distinction forces the continuum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.