toInt_zero
plain-language theorem explainer
The integer embedding of the forced natural zero is ordinary zero: toInt maps LogicNat.zero to 0. Anyone proving ring identities for LogicInt via the recovery map cites this as a simp fact. The proof is a one-line unfolding of the embedding definition.
Claim. If $N$ is the forced natural carrier and $\iota : N \to \mathbb{Z}$ sends each element to its iteration count, then $\iota(0_N) = 0$.
background
LogicNat is the natural-number carrier forced by the Law of Logic: two constructors, identity (zero-cost multiplicative unit of the orbit) and step (one generator iteration). It mirrors the orbit ${1, \gamma, \gamma^2, \ldots}$ as the smallest subset of $\mathbb{R}_+$ closed under multiplication by $\gamma$ and containing 1.
In ForcedIntegers, the map toInt embeds a LogicNat into $\mathbb{Z}$ by casting its iteration count: $\iota(n) = (\mathrm{toNat}, n : \mathbb{Z})$. The same name appears upstream for LogicInt and SignedOrbit recovery maps; here the domain is only LogicNat.
The module sits in UniversalForcing and builds the integer layer from ForcedSemiring, so zero-preservation is the first coherence check before add/mul lemmas.
proof idea
One-line wrapper: simp [toInt] unfolds the embedding to the cast of LogicNat.toNat on zero, which reduces to $0$ by the natural-number zero lemma already available to simp.
why it matters
Zero-preservation is the base simp fact for transporting LogicInt arithmetic through the recovery map. Downstream, IntegersFromLogic uses it in zero_add', add_zero', and add_left_neg' (rewrite equality to integer equality, apply toInt_add/toInt_neg, then ring). It also appears in mul_eq_zero and mul_right_cancel when identifying the zero element, and in RationalsFromLogic when building fromRat.
In the Recognition forcing chain this is scaffolding for the integer carrier before rationals and the J-cost calculus: without $\iota(0)=0$, the ring isomorphism equivInt and the no-zero-divisors claim do not close. It is not itself a T0–T8 landmark, but it is a necessary coherence step on the path from LogicNat to the forced integers used later in the mass ladder and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.