toInt

In the Arithmetic-from-Logic layer, forced naturals are the inductive type with constructors identity (the zero-cost multiplicative unit of the orbit) and step (one more multiplication by the generator γ). That type mirrors the smallest subset of ℝ₊ containing 1 and closed under multiplication by γ.

The forward map from a forced natural to Lean Nat simply counts how many steps were applied: identity maps to 0, and each step increments. The present definition lifts that count one step further into the classical integers by the standard non-negative cast.

The surrounding module develops forced integers as differences of forced naturals and certifies that the resulting carrier recovers ordinary ℤ. This embedding is the non-negative leg of that recovery.

Pure definition: apply the iteration-count map from forced naturals to Nat, then coerce the result to ℤ. No lemmas or tactics are involved.

This is the non-negative bridge from forced arithmetic into classical Int. Downstream, the Integers-from-Logic recovery map, the carrier equivalence LogicInt ≃ Int, the transfer principle (equations hold in LogicInt iff they hold after embedding), and the no-zero-divisors / cancellation lemmas all route through integer embeddings of this shape. In the Universal Forcing chain it supplies the concrete integer values against which forced differences and ring identities are checked, so the later claim that the integers themselves are forced has a usable comparison map. Sibling lemmas (zero/one preservation, add/mul homomorphism, injectivity, non-negativity) sit on top of this cast.