toZ
plain-language theorem explainer
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 ℤ.
Claim. For δ ∈ ℤ 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.