fromZ_one
plain-language theorem explainer
The embedding fromZ_one sends each integer n to the element n in the δ=1 subgroup of ℤ. Scale-mapping code in the Recognition framework cites this when building order isomorphisms between integer rungs and delta subgroups. Construction uses the fact that n equals n times 1, witnessed by the multiplicative identity.
Claim. For any integer $n$, the map $nmapsto(n,exists k.n=kcdot1)$ embeds $mathbb{Z}$ into the subgroup $Delta_1={xinmathbb{Z}midexists kinmathbb{Z}.x=kcdot1}$.
background
DeltaSub δ is the subgroup of ℤ consisting of all integer multiples of a fixed generator δ; the case δ=1 yields the full group ℤ under the subgroup predicate. The module RecogSpec.Scales develops binary scales and φ-exponential wrappers that rely on clean order isomorphisms between integer ladders and these subgroups. Upstream, the subgroup definition appears in LedgerUnits and the multiplicative identity n·1=n is supplied by mul_one in ArithmeticFromLogic.
proof idea
One-line wrapper that packages the integer n with the witness n·1=n, obtained directly from the mul_one lemma in ArithmeticFromLogic via simpa.
why it matters
This definition supplies the forward map for the equivalence equiv_delta_one used in both LedgerUnits and RecogSpec.Scales to identify the δ=1 subgroup with ℤ. It supports the binary scale constructions in the module and feeds into phi-ladder mappings and the eight-tick octave structure of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.