toZ
toZ extracts the integer coefficient from an element of the subgroup generated by δ. It is invoked in LedgerUnits for constructing the equivalence equiv_delta and for extracting rung indices via rungOf and kOf. The definition reduces to the identity map because the local DeltaSub δ is defined directly as ℤ.
claimFor δ ∈ ℤ and p in the subgroup Δ_δ generated by δ, toZ(δ, p) returns the coefficient n such that p = n δ. In this module the map is the identity on ℤ.
background
The UnitMapping module defines DeltaSub δ as the type ℤ itself, serving as an abstract placeholder for the subgroup generated by δ to facilitate integer mappings. This contrasts with the precise subtype definition in LedgerUnits, where DeltaSub δ consists of elements x : ℤ such that ∃ n : ℤ, x = n * δ. The local theoretical setting is unit mapping for ledger quantization using integers only.
proof idea
The definition is a one-line identity toZ δ p := p. No lemmas are applied and no tactics are used; the simp attribute is attached for rewriting in downstream proofs.
why it matters in Recognition Science
It supplies the forward map in equiv_delta, which establishes DeltaSub δ ≃ ℤ for nonzero δ. This supports downstream results including rungOf, kOf, fromNat, and the quantization theorem that asserts a unique integer coefficient for every element. The construction enables discrete indexing on the phi-ladder in the Recognition framework.
scope and limits
- Does not verify that p is a multiple of δ.
- Does not extend to real numbers or other fields.
- Does not compute physical constants or units.
- Does not handle the case δ = 0.
Lean usage
example (δ : ℤ) (p : DeltaSub δ) : toZ δ p = p := rflformal statement (Lean)
14@[simp] def toZ (δ : ℤ) (p : DeltaSub δ) : ℤ := p
proof body
Definition body.
15