The definition introduces the subgroup of integers consisting of all multiples of a fixed integer parameter δ. It is referenced in ledger unit mappings and scale equivalences within Recognition Science when constructing order isomorphisms, especially for the case δ=1. The implementation is a direct subtype comprehension with no separate proof obligations or lemmas.
claimFor a fixed integer parameter δ, the set of all integer multiples of δ is the subgroup {x ∈ ℤ | ∃ n ∈ ℤ, x = n · δ}.
background
The module treats binary scales and φ-exponential wrappers. This supplies the integer subgroup generated by δ, which is specialized to δ=1 to obtain a clean order isomorphism with ℤ. Upstream results supply the identical definition in LedgerUnits (for embeddings) and an abstract placeholder version in UnitMapping (for mapping purposes only).
proof idea
The definition is a direct subtype comprehension encoding multiples of δ. No lemmas are applied and no tactics are used; it serves as the base type for downstream equivalence functions.
why it matters in Recognition Science
It underpins the equivalence constructions in LedgerUnits such as equiv_delta (for nonzero δ) and equiv_delta_one (for δ=1), which map the generated subgroup back to ℤ. This supports discrete scale handling in the Recognition framework, particularly for binary scales and φ-exponential wrappers.
scope and limits
Does not prove that the set forms a subgroup under addition.
Does not restrict δ to nonzero values.
Does not connect to the φ constant or exponential scales.
Does not supply embedding or projection functions.
formal statement (Lean)
112def DeltaSub (δ : ℤ) := {x : ℤ // ∃ n : ℤ, x = n * δ}
proof body
Definition body.
113 114/-- Embed ℤ into the δ=1 subgroup. -/
used by (28)
From the project-wide theorem graph. These declarations reference this one in their body.