toInt_injective
plain-language theorem explainer
The embedding of logic-forced natural numbers into classical integers, sending each orbit iterate to its iteration count as an integer, is injective. Anyone transferring equalities or ring identities from ℤ back onto the forced carrier cites this. The proof casts the integer equality down to a Nat equality and applies the LogicNat–Nat equivalence.
Claim. The map from logic-forced naturals into the integers, $n \mapsto (\mathrm{count}(n):\mathbb{Z})$ where $\mathrm{count}$ reads the iteration depth of the generator orbit, is injective: equal integer displays imply equal forced naturals.
background
LogicNat is the inductive carrier forced by the Law of Logic: a zero-cost identity constructor and a step constructor that iterates the generator. Its doc-comment states that this two-constructor structure mirrors the orbit ${1,\gamma,\gamma^2,\ldots}$ as the smallest subset of $\mathbb{R}_+$ closed under multiplication by $\gamma$ and containing 1.
The forward map toNat reads off that iteration count. The recovery equivalence equivNat witnesses that LogicNat and Nat have the same underlying set, via round-trip equalities fromNat_toNat and toNat_fromNat.
In ForcedIntegers (UniversalForcing layer, importing ForcedSemiring), toInt is the non-negative display of this carrier inside classical $\mathbb{Z}$, obtained by casting the Nat count. The local setting is recovery of standard arithmetic so later forcing steps can quote classical lemmas after a faithful embedding.
proof idea
Short tactic proof. Introduces $a,b$ and the hypothesis $\mathrm{toInt},a=\mathrm{toInt},b$. That hypothesis is definitionally an equality of two natural counts cast to $\mathbb{Z}$; exact_mod_cast recovers $\mathrm{toNat},a=\mathrm{toNat},b$. The final step applies injectivity of equivNat (whose toFun is toNat), yielding $a=b$. No induction or quotient reasoning is required; the work is entirely the Nat recovery equivalence plus a cast.
why it matters
Injectivity of the integer display is the transfer principle for forced arithmetic: equalities proved in classical $\mathbb{Z}$ pull back to the forced carrier. Downstream ring-law proofs (add_assoc, add_comm, add_zero, add_negate, mul_assoc, mul_comm, mul_one, left_distrib) follow the pattern apply toInt_injective; simp with the corresponding Int lemma.
In the Recognition foundation this sits under UniversalForcing, recovering integers from logic before the forcing chain installs J-uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). Sibling lemmas toInt_add, toInt_mul, toInt_nonneg, and integers_surject, together with ForcedIntegersCert, package the same display as a structure-preserving embedding. Without injectivity, classical identities would not land on the forced carrier, blocking the integer and rational layers that feed later mass and constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.