DeltaSub
DeltaSub defines the subgroup of integers generated by a fixed δ as the subtype of all integer multiples n·δ. Ledger unit mappings in Recognition Science cite it to build order isomorphisms between scaled subgroups and ℤ. The definition is a direct subtype construction requiring no lemmas or reduction steps.
claimFor fixed δ ∈ ℤ, let Δ(δ) denote the set {x ∈ ℤ | ∃ n ∈ ℤ, x = n·δ}.
background
In LedgerUnits, DeltaSub reuses the subgroup definition from RecogSpec.Scales, where the doc-comment states: 'The subgroup of ℤ generated by δ. We specialize to δ = 1 for a clean order isomorphism.' The UnitMapping import supplies an abstract placeholder version treating the subgroup simply as ℤ for mapping purposes. This supplies the type for embedding Nat and ℤ into scaled ledger units via multiples of δ, supporting later equivalences that identify the subgroup with ℤ when δ ≠ 0.
proof idea
Direct subtype definition: DeltaSub δ is declared as {x : ℤ // ∃ n : ℤ, x = n * δ}. No lemmas or tactics are invoked; the body is a primitive type abbreviation.
why it matters in Recognition Science
The definition supplies the domain type for equiv_delta, equiv_delta_one, fromZ, toZ, fromNat and kOf. These equivalences realize the non-canonical isomorphism n·δ ↦ n for δ ≠ 0 and the canonical case δ = 1. It thereby anchors the ledger unit arithmetic that feeds the phi-ladder scaling and Recognition Composition Law applications downstream.
scope and limits
- Does not prove the subgroup is cyclic or compute its index in ℤ.
- Does not treat the degenerate case δ = 0.
- Does not supply the forward or inverse maps; those appear in downstream definitions.
- Does not impose any ordering or metric structure on the subgroup.
formal statement (Lean)
7def DeltaSub (δ : ℤ) := {x : ℤ // ∃ n : ℤ, x = n * δ}
proof body
Definition body.
8
9/-- Embed ℤ into the δ=1 subgroup. -/