forcedIntegersCert_holds
plain-language theorem explainer
Packages the LogicNat-to-integers embedding into a single ForcedIntegersCert: a ring homomorphism that is injective, whose differences exhaust ℤ, and whose negation-fixed locus is exactly the diagonal. Foundation work citing the forced integer layer (the additive mirror of the ratio geometry) points here. The body is a pure structure instance wiring already-proved field lemmas.
Claim. There is a map $e:\mathrm{LogicNat}\to\mathbb{Z}$ with $e(0)=0$, $e(1)=1$, $e(a+b)=e(a)+e(b)$, $e(a\cdot b)=e(a)\cdot e(b)$, $e$ injective, every $z\in\mathbb{Z}$ equal to $e(a)-e(b)$ for some $a,b$, and $e(a)-e(b)=-(e(a)-e(b))$ if and only if $a=b$.
background
This module sits in UniversalForcing after ForcedSemiring. The ambient story is that arithmetic is recovered from the logic layer rather than postulated: LogicNat is the free iterative count type, and integers arise as differences of those counts.
ForcedIntegersCert is the certificate structure that records the integer layer the δ paper names. Its fields demand an embedding of logic naturals into $\mathbb{Z}$ preserving $0,1,+,\times$, injectivity, surjectivity of differences onto all of $\mathbb{Z}$, and the geometric fact that the additive negation involution fixes a difference precisely on the diagonal $a=b$.
The concrete map used is toInt (and its companion lemmas toInt_zero, toInt_one, toInt_add, toInt_mul, toInt_injective, integers_surject, forced_difference_fixed_iff), built upstream in IntegersFromLogic / ArithmeticFromLogic as the recovery map from the logic integer quotient into classical $\mathrm{Int}$.
proof idea
Pure structure construction. Each field of ForcedIntegersCert is filled by the matching already-proved lemma: embed by toInt; zero/one/add/mul preservation by toInt_zero, toInt_one, toInt_add, toInt_mul; injectivity by toInt_injective; difference surjectivity by integers_surject; negation-diagonal characterization by forced_difference_fixed_iff. No new reasoning.
why it matters
Closes the forced-integers certificate in the UniversalForcing chain: the integer layer is forced, canonical, and carries the additive mirror of the ratio layer's comparison geometry (per the structure doc). Downstream consumers of a single packed witness for "logic naturals embed as classical integers with full difference coverage and diagonal negation" can cite this inhabitant rather than reassemble seven lemmas. It sits beside ForcedSemiring as the next arithmetic forcing step after the logic-to-orbit bridge (embed, embed_add, embed_injective in ArithmeticFromLogic). No used_by edges are recorded yet; the declaration is the terminal packaging of this module's integer results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.