forcedArithmeticIsNat
plain-language theorem explainer
Distinction forces ordinary natural-number arithmetic: the forced carrier is isomorphic to ℕ as a (0,1,+,×)-structure. Cite this as the ForcedSemiring capstone certificate that the arithmetic recovered from logic is Lean's Nat, with no base or arithmetic axioms assumed. The definition packages the existing LogicNat–Nat equivalence with the recovery lemmas for zero, one, addition, and multiplication.
Claim. The forced arithmetic carrier (generated by an identity element and a successor/step) is isomorphic to $\mathbb{N}$ as a semiring: there is an equivalence $e$ with $e(0)=0$, $e(1)=1$, $e(a+b)=e(a)+e(b)$, and $e(a\cdot b)=e(a)\cdot e(b)$ for all elements $a,b$ of the forced carrier.
background
In ArithmeticFromLogic, LogicNat is the type forced by the Law of Logic: a two-constructor inductive type whose identity is the zero-cost (multiplicative identity) element and whose step is one further iteration of the generator. That structure mirrors the positive orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest subset of $\mathbb{R}_+$ closed under multiplication by $\gamma$ and containing 1.
The structure being inhabited here asserts a full $(0,1,+,\times)$-isomorphism from that forced carrier to Lean's Nat. Upstream, the carrier recovery theorem supplies a round-trip equivalence (toNat / fromNat), and separate recovery theorems show that addition and multiplication on the forced carrier agree with ordinary Nat operations under that map. Zero and one are likewise matched.
Locally this sits in UniversalForcing.ForcedSemiring: CanonicalForcing already forces every strict realization onto the same carrier, so packaging the isomorphism completes the claim that distinction forces ordinary natural arithmetic.
proof idea
Field-by-field assembly of the certificate structure, not a new proof. The equivalence field is the existing carrier recovery map LogicNat.equivNat. Zero, addition, and multiplication fields are the corresponding recovery theorems (toNat_zero, toNat_add, toNat_mul). The unit field is the sibling one-preservation fact. No induction or algebraic work happens at this site; it only wires prior lemmas into the capstone record.
why it matters
This is the ForcedSemiring capstone named in the structure doc: "distinction forces ℕ." Every strict realization is already pinned to the same carrier by CanonicalForcing, so the arithmetic distinction forces is, up to canonical semiring isomorphism, exactly the natural numbers Lean already has, with no base, no positional notation, and no arithmetic axioms posited.
It closes the foundation arc that runs from the Law of Logic through orbit arithmetic to a concrete identification with ℕ. That identification is the arithmetic substrate under the broader Universal Forcing / UnifiedForcingChain story (T0–T8), before cost functionals, $\varphi$, eight-tick structure, or dimension forcing are imposed. No downstream consumers are recorded yet; the value is the certificate itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.