integers_surject
plain-language theorem explainer
Every integer arises as a difference of two forced naturals under the canonical embedding into ℤ. Anyone assembling the forced-integers certificate or the additive group layer of Universal Forcing cites this surjectivity. The proof picks the pair of LogicNat orbits of z.toNat and (−z).toNat, then closes by simplification and omega.
Claim. For every $z \in \mathbb{Z}$ there exist forced naturals $a,b$ (elements of the Logic-forced orbit $\{1,\gamma,\gamma^2,\ldots\}$) such that $z = \iota(a) - \iota(b)$, where $\iota$ is the canonical embedding of forced naturals into $\mathbb{Z}$.
background
LogicNat is the inductive type forced by the Law of Logic: identity is the zero-cost multiplicative unit, and step iterates the generator once. It is the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest subset of $\mathbb{R}_+$ closed under multiplication by $\gamma$ and containing 1. The maps toNat/fromNat identify LogicNat with ordinary $\mathbb{N}$, with toNat_fromNat the left inverse.
The sibling embedding toInt sends each forced natural into $\mathbb{Z}$. The present module sits in Universal Forcing after ForcedSemiring: once nonnegatives are forced, one asks whether their differences fill all of $\mathbb{Z}$ or only a proper subcollection. The doc-comment states the claim directly: "The forced difference layer is all of $\mathbb{Z}$, so distinction forces the full additive group of integers."
proof idea
Term-mode construction, not a wrapper. For arbitrary $z:\mathbb{Z}$, take witnesses
$a = \mathrm{fromNat}(z.\mathrm{toNat})$ and $b = \mathrm{fromNat}((-z).\mathrm{toNat})$.
Unfold toInt and apply LogicNat.toNat_fromNat so both sides become ordinary integer arithmetic on $z.\mathrm{toNat}$ and $(-z).\mathrm{toNat}$. The goal reduces to an identity that omega discharges (covering the three sign cases of $z$ uniformly).
why it matters
Closes the surjectivity half of the forced-integers story: every integer is a forced difference, so the additive group forced by distinction is exactly $\mathbb{Z}$, not a thin submonoid of differences. Downstream, forcedIntegersCert_holds packages the certificate (embed := toInt together with zero/one/add/mul laws); this theorem is the missing surjectivity ingredient that certificate consumers rely on when they treat the forced difference layer as all of $\mathbb{Z}$.
In the broader Recognition chain this sits under Universal Forcing of arithmetic structure from the cost/J-automorphism data (upstream CostAlgebra multiplicativity and the golden cost projector), before ratios and the continuum are forced. It is the additive counterpart of the multiplicative unit-locus story for ForcedRatios mentioned in the module's next section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.