fromNat
plain-language theorem explainer
Defines the embedding of natural numbers into the subgroup of integers generated by a fixed δ by routing through the integer embedding. Workers on the LogicNat recovery isomorphisms cite it when moving statements between Nat and the ledger units. The definition is a direct one-line wrapper around fromZ after the Nat-to-Int cast.
Claim. The map sending each natural number $m$ to the element $m·δ$ inside the subgroup of $ℤ$ consisting of all integer multiples of a fixed $δ$.
background
DeltaSub δ is the subgroup {x : ℤ // ∃ n : ℤ, x = n * δ}. The sibling fromZ δ n constructs the element ⟨n * δ, ⟨n, rfl⟩⟩ inside that subgroup. The module specializes the case δ = 1 to obtain an order isomorphism with ℤ. Upstream, the fromNat and toNat pair in ArithmeticFromLogic supplies the analogous round-trip for LogicNat, and PrimitiveDistinction supplies the underlying distinction axioms.
proof idea
One-line wrapper that applies fromZ after casting the Nat argument via Int.ofNat.
why it matters
This definition supplies the nonnegative generators used by add_left_cancel, embed_injective, eq_iff_toNat_eq, and equivNat in ArithmeticFromLogic. Those theorems recover Nat arithmetic inside LogicNat and close the bridge to the orbit {1, γ, γ², …} in ℝ₊. It therefore supports the transfer principle that lets omega proofs on Nat be lifted back to the ledger units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.