ForcedArithmeticIsNat
plain-language theorem explainer
Packages the claim that the logic-forced carrier is canonically isomorphic to ordinary natural numbers as a (0,1,+,×)-structure. Anyone citing the Universal Forcing capstone (distinction forces ℕ) uses this certificate type. It is a pure structure definition: four preservation fields plus a type equivalence, filled later by the concrete instance.
Claim. A certificate that the logic-forced naturals are isomorphic to $\mathbb{N}$ as a $(0,1,+,\times)$-structure: 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)$.
background
In ArithmeticFromLogic, LogicNat is the inductive carrier forced by the Law of Logic: constructors identity (zero-cost multiplicative unit in the orbit) and step (one generator iteration). Its two-constructor shape mirrors the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest subset of $\mathbb{R}_+$ containing 1 and closed under multiplication by $\gamma$.
This module sits in UniversalForcing: CanonicalForcing already shows every strict realization forces that same carrier. The present structure records what it means for that forced arithmetic to be ordinary $\mathbb{N}$ up to semiring isomorphism, without positing base, place-value, or Peano axioms by hand.
Upstream cost-projector and one-primitive recognition calculus supply the forcing context in which the carrier and operations are uniquely determined before the comparison to Lean's Nat.
proof idea
No proof body: this is a structure (certificate type). It bundles (i) a type equivalence from the logic-forced naturals to Nat, (ii) preservation of zero and one, and (iii) homomorphism laws for addition and multiplication. The downstream definition forcedArithmeticIsNat fills the fields with LogicNat.equivNat and the corresponding toNat_* lemmas.
why it matters
Capstone packaging for the Universal Forcing story: distinction forces a unique arithmetic carrier, and that carrier is, up to canonical semiring isomorphism, exactly Lean's naturals. The doc-comment states the point directly: no base, no positional notation, no arithmetic axioms posited.
The sole immediate consumer is forcedArithmeticIsNat, which inhabits the structure and thereby closes the "forced arithmetic is ℕ" claim inside ForcedSemiring. Downstream work that needs a named witness that forced $(0,1,+,\times)$ matches standard $\mathbb{N}$ cites this type (or its instance) rather than re-proving the four preservation laws.
In the broader Recognition chain this anchors the arithmetic layer beneath later forcing (T5–T8, RCL, phi-ladder): once the carrier is identified with $\mathbb{N}$, counting, octaves, and rung indices sit on familiar ground.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.