DeltaSub
DeltaSub δ is defined as the integers ℤ to serve as an abstract placeholder for the subgroup generated by δ during unit-mapping constructions. Ledger and scale-mapping code cites this alias to avoid repeated subgroup notation while preserving integer arithmetic. The definition is a direct one-line alias with no computation or proof obligations.
claimFor any integer $δ$, define $ΔSub(δ) := ℤ$, where this stands in for the subgroup of $ℤ$ generated by $δ$ in mapping contexts.
background
In the UnitMapping module the declaration supplies a simplified interface for integer subgroups that appear in ledger equivalences. Upstream definitions in LedgerUnits and RecogSpec.Scales give the concrete subgroup $ΔSub(δ) := {x : ℤ // ∃ n : ℤ, x = n · δ}$, which is the set of all integer multiples of δ. The present alias replaces that construction with plain $ℤ$ so that mapping functions can treat elements directly as integers once the isomorphism is assumed. The module imports Constants and the two sibling DeltaSub declarations, indicating that the alias is intended only for internal mapping use rather than for the full subgroup theory.
proof idea
The declaration is a one-line definition that directly sets DeltaSub δ to ℤ. No lemmas are applied; the body is simply the type ℤ.
why it matters in Recognition Science
The alias feeds the equivalence constructions in LedgerUnits (equiv_delta, equiv_delta_one, fromZ, toZ) that map δ-subgroups onto ℤ. It supplies the integer layer required for the Recognition Composition Law and the phi-ladder rung calculations that appear in downstream scale mappings. The definition closes a notational gap between the abstract subgroup in RecogSpec.Scales and the concrete integer arithmetic used for unit conversions.
scope and limits
- Does not construct or prove membership in the actual subgroup generated by δ.
- Does not handle the degenerate case δ = 0.
- Does not supply the embedding or projection functions fromZ or toZ.
- Does not establish any isomorphism or order properties.
formal statement (Lean)
11def DeltaSub (δ : ℤ) := ℤ
proof body
Definition body.
12