toInt_nonneg
plain-language theorem explainer
Every logic-natural embeds into ℤ as a nonnegative integer under the canonical recovery map. Foundation work on the forced-integer layer cites this when building differences and the additive group. The proof unfolds the embedding and applies the standard nonnegativity of nat-cast.
Claim. For every logic-natural $n$ (the inductive type with constructors identity and step), the canonical recovery map into the integers satisfies $0 \le \iota(n)$, where $\iota$ is the embedding of logic-naturals into $\mathbb{Z}$.
background
LogicNat is the natural-number type forced by the Law of Logic: identity is the zero-cost multiplicative unit in the orbit, and step is one further generator iterate. Its two-constructor shape mirrors the smallest subset ${1,\gamma,\gamma^2,\ldots}\subset\mathbb{R}_+$ closed under multiplication by $\gamma$ and containing 1.
This module sits in UniversalForcing after ForcedSemiring. It builds the integer layer from forced arithmetic so that distinction yields a full additive group, not a proper subcollection. The local recovery map sends a LogicNat into $\mathbb{Z}$ by the usual nat-cast path (compare the signed-orbit display $\mathrm{toInt}(z)=z_{\mathrm{pos}}-z_{\mathrm{neg}}$ elsewhere in the primitive calculus).
Upstream scaffolding includes the cost-functional and projector-forced structures that pin the arithmetic carrier; the present lemma only needs the nonnegativity of the integer image of a natural.
proof idea
Term-style tactic proof in two steps. First unfold the local recovery map on LogicNat (simp only [toInt]), exposing a nat-cast into $\mathbb{Z}$. Then apply Int.natCast_nonneg, which states that every natural number, viewed as an integer, is $\ge 0$. No induction on LogicNat is required once the definition reduces to nat-cast.
why it matters
Places the forced naturals inside the nonnegative cone of $\mathbb{Z}$, which is the first half of identifying forced differences with all of the integers. The module header that follows states the target: every integer is a difference of two forced numbers, so distinction forces the full additive group, not a proper subcollection.
Sibling lemmas (additivity, multiplicativity, injectivity of the embedding, surjectivity of differences, and the ForcedIntegers certificate) complete that identification. In the broader Recognition forcing chain this is foundation arithmetic: LogicNat from the Law of Logic, then integers as differences, before cost uniqueness (T5), $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8). No downstream users are recorded yet; the lemma is infrastructure for the difference-layer theorems in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.