DeltaSub
plain-language theorem explainer
DeltaSub δ supplies an abstract integer type as a stand-in for the subgroup generated by δ inside unit-mapping code. Ledger-unit equivalence constructions cite this placeholder to treat all δ-mappings uniformly through ℤ. The definition is a direct one-line alias to the integer type.
Claim. For any integer δ, let ΔSub(δ) stand for the type ℤ, serving as an abstract placeholder for the subgroup of ℤ generated by δ.
background
The UnitMapping module supplies integer-based mappings between ledger units and recognition scales. Upstream definitions in LedgerUnits and RecogSpec.Scales both give DeltaSub δ explicitly as the set {x : ℤ // ∃ n : ℤ, x = n * δ}, the subgroup generated by δ, and note that the case δ = 1 yields a clean order isomorphism to ℤ. The present declaration replaces that set with the bare type ℤ to simplify mapping code while preserving the intended integer arithmetic.
proof idea
The definition is a one-line alias that directly sets DeltaSub δ to ℤ.
why it matters
DeltaSub feeds the equivalence maps equiv_delta, equiv_delta_one, fromZ and fromNat in LedgerUnits, which realize the non-canonical isomorphism n·δ ↦ n. It therefore supplies the integer interface required by the unit-mapping layer that sits between LedgerUnits and the Recognition scales. No open question is closed by this alias itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.