DeltaSub
plain-language theorem explainer
DeltaSub defines the subgroup of integers consisting of all multiples of a fixed integer δ. Ledger unit mappings cite this to construct order isomorphisms between scaled subgroups and the standard integers. The definition is a direct subtype predicate requiring existence of a multiplier n.
Claim. Let δ be an integer. The subgroup generated by δ is the set of all integers x such that there exists an integer n with x = n δ.
background
In the LedgerUnits module, integer subgroups model scaled units for ledger mappings and equivalences. This definition reuses the subgroup construction from RecogSpec.Scales, which introduces it with identical content and notes specialization to δ = 1 for a clean order isomorphism. UnitMapping supplies an abstract placeholder version that reduces the subgroup simply to ℤ for mapping purposes only.
proof idea
The definition is given directly as a subtype of ℤ whose elements satisfy the multiple predicate. No lemmas or tactics are invoked; it serves as a primitive carrier type for downstream constructions such as fromZ and toZ.
why it matters
This definition supplies the carrier for equiv_delta and equiv_delta_one, which establish (non-canonical) equivalences to ℤ via n·δ ↦ n. It implements the doc-comment specialization to δ = 1 for order isomorphisms and supports integer scaling throughout the LedgerUnits module. The construction remains independent of the phi-ladder or forcing chain steps T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.