equiv_delta
plain-language theorem explainer
The definition supplies a non-canonical isomorphism between the subgroup of integers generated by any nonzero δ and the full integers via the coefficient map n·δ ↦ n. Discrete symmetry or lattice analysts in Recognition Science cite it when normalizing scaled integer counts back to unit steps. The construction directly assembles the equivalence from the explicit embedding and projection maps together with their mutual inverse lemmas.
Claim. For any nonzero integer $δ$, the subgroup of integers generated by $δ$, defined as the set of all integer multiples of $δ$, is equivalent to the integers themselves via the map sending each multiple $n·δ$ to the coefficient $n$.
background
The LedgerUnits module introduces DeltaSub δ as the subgroup of ℤ consisting of all integer multiples of δ, with the special case δ = 1 yielding a canonical order isomorphism. The general nonzero case requires a non-canonical equivalence that extracts coefficients. Upstream results supply the embedding map sending n to n·δ, the projection extracting the coefficient via choice, and the two lemmas verifying that these maps are mutual inverses.
proof idea
This is a one-line wrapper that constructs the equivalence structure by supplying toZ δ as the forward map, fromZ δ as the inverse map, fromZ_toZ δ as the left inverse, and toZ_fromZ δ hδ as the right inverse.
why it matters
The declaration completes the general nonzero δ case for integer subgroup equivalences in LedgerUnits, enabling reductions of scaled counts in unit mappings. It supports downstream handling of discrete structures in the Recognition framework, such as phi-ladder rung assignments and integer steps in forcing chains. No open questions or scaffolding are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.