equiv_delta
plain-language theorem explainer
For any nonzero integer δ the cyclic subgroup of all multiples of δ inside the integers is equivalent to the full integers by the rule that sends each multiple nδ to the coefficient n. Researchers handling discrete scalings or lattice subgroups in algebraic number theory would cite the construction when reducing generated subgroups to standard form. The definition directly assembles the coefficient extractor, the multiplier map, and the two inversion lemmas that certify they are mutual inverses.
Claim. For any nonzero integer $δ$, the subgroup of integers consisting of all multiples of $δ$ is equivalent to $ℤ$ itself via the correspondence that sends the element $n·δ$ to the integer $n$.
background
The subgroup generated by a fixed nonzero integer δ is the set of all integers x such that x equals n times δ for some integer n. The module treats these subgroups in general and specializes to the generator δ equals 1 to obtain a canonical order isomorphism between the subgroup and the integers. Upstream definitions supply the explicit maps that extract the coefficient from a subgroup element and that embed an arbitrary integer by multiplying it by δ; the accompanying inversion lemmas establish that the two maps are mutual inverses.
proof idea
The definition constructs the equivalence by supplying the forward map as the coefficient extractor, the inverse map as the multiplier, and the two inversion lemmas to witness the left and right inverse properties.
why it matters
The equivalence supplies the algebraic identification needed to treat scaled discrete steps uniformly inside the ledger unit system. It supports the integer coefficients that appear in the phi-ladder mass formulas and in the eight-tick octave structure of the Recognition Science forcing chain. No downstream theorems are recorded, indicating that the construction remains an internal tool for handling nonzero generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.