toInt_add
plain-language theorem explainer
Addition on logic-forced naturals is preserved by the integer recovery map: the image of a sum is the sum of the images in ℤ. Anyone embedding LogicNat into the forced integers, or transferring semiring laws along that embedding, cites this. The proof unfolds the recovery map, rewrites by the Nat-level addition recovery, then finishes by casting and ring.
Claim. For all logic-forced natural numbers $a$ and $b$, the integer recovery map satisfies $\mathrm{rec}(a+b)=\mathrm{rec}(a)+\mathrm{rec}(b)$ in $\mathbb{Z}$.
background
LogicNat is the inductive type forced by the Law of Logic: identity is the zero-cost (multiplicative) unit of the orbit, and step is one further generator iterate, mirroring ${1,\gamma,\gamma^2,\ldots}$ as the smallest subset of $\mathbb{R}_+$ closed under multiplication by $\gamma$ and containing 1.
The recovery map toNat sends LogicNat to ordinary Nat and is already known to preserve addition (ArithmeticFromLogic recovery theorem). In this module the integer recovery map on LogicNat is the composite embedding into $\mathbb{Z}$ (nonnegative part of the signed-orbit display used elsewhere as $(\mathrm{pos.toNat}:\mathbb{Z})-(\mathrm{neg.toNat}:\mathbb{Z})$). The local setting is UniversalForcing.ForcedIntegers: integers as forced structure once the logic naturals and their arithmetic are in place, imported from ForcedSemiring.
proof idea
Short tactic proof. Unfold the local integer recovery map with simp only [toInt], exposing the cast of toNat. Rewrite by LogicNat.toNat_add so the Nat-level sum appears. push_cast moves the sum into $\mathbb{Z}$, and ring closes the integer identity. No induction is needed here; the inductive work already lives in the Nat recovery lemma.
why it matters
This is the additive half of the LogicNat→ℤ embedding used throughout ForcedIntegers (siblings cover zero, one, mul, injectivity, nonnegativity, and surjectivity onto nonnegative integers). Downstream, IntegersFromLogic builds the full ring laws on LogicInt by the transfer principle: an equation holds in LogicInt iff it holds under the integer recovery map. Concrete consumers include add_assoc', add_comm', add_zero', zero_add', add_left_neg', mul_add', and add_mul', each reducing via recovery of addition (and often multiplication) then finishing with ring on ℤ.
In the Recognition forcing chain this sits under arithmetic-from-logic: once naturals are forced, their additive structure must embed cleanly into the forced integers before difference constructions and ring axioms can be discharged. It is proved scaffolding for that transfer, not an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.