DeltaSub
plain-language theorem explainer
DeltaSub δ is realized as the type ℤ in the UnitMapping module, acting as an abstract stand-in for the subgroup of integers generated by δ. Ledger unit mappings cite it to obtain clean order isomorphisms without carrying subgroup predicates. The definition is a direct one-line type alias.
Claim. Let $Δ_δ$ denote the subgroup of $ℤ$ generated by fixed $δ ∈ ℤ$. In the unit-mapping setting this is identified with the full group $ℤ$.
background
Upstream definitions in LedgerUnits and RecogSpec.Scales realize DeltaSub δ explicitly as the set {x : ℤ // ∃ n : ℤ, x = n * δ}. The UnitMapping module replaces this construction with the plain type ℤ to simplify subsequent maps. The local setting is integer-based ledger units for charge, time, and action, where δ tracks the generator of discrete steps.
proof idea
One-line type alias that sets DeltaSub δ directly to ℤ.
why it matters
The placeholder supplies the target type for equiv_delta, equiv_delta_one, fromZ, and fromNat in LedgerUnits. These equivalences convert between the generated subgroup and ℤ, enabling the integer indexing used in unit mappings. It closes the interface for the eight-tick octave and phi-ladder structures that rely on clean ℤ-isomorphisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.