fromZ
plain-language theorem explainer
The fromZ definition embeds an integer n directly into the abstract δ-subgroup by returning n, since DeltaSub δ is set to ℤ. Researchers building unit mappings and integer equivalences in LedgerUnits cite it when constructing fromNat, rungOf, and equiv_delta. The implementation is a one-line assignment that acts as a placeholder simplifying the subgroup structure.
Claim. For any integers $δ$ and $n$, fromZ$(δ, n) := n$, where $Δ$Sub$(δ)$ denotes the integers $ℤ$.
background
In the UnitMapping module, DeltaSub δ is defined as the type ℤ, serving as an abstract placeholder for the subgroup generated by δ. This differs from the upstream LedgerUnits definition, where DeltaSub δ = {x : ℤ // ∃ n : ℤ, x = n * δ} and fromZ embeds via the pair ⟨n * δ, ⟨n, rfl⟩⟩. The module doc describes the setting as an abstract placeholder using integers for mapping only.
proof idea
One-line definition that directly assigns the input n to the DeltaSub δ type (which is ℤ). No tactics or lemmas are applied; the body is the identity map in this simplified representation.
why it matters
This definition supplies the inverse map for equiv_delta in LedgerUnits and is used by fromNat, rungOf_fromZ, kOf_fromZ, and toZ_fromZ. It supports the unit-mapping layer that feeds rung and charge calculations in the Recognition framework, enabling the integer coefficient handling that underlies the phi-ladder and eight-tick octave steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.