toZ
plain-language theorem explainer
The toZ definition supplies the integer coefficient map for elements of the abstract δ-subgroup placeholder in UnitMapping. LedgerUnits results such as equiv_delta, quantization, rungOf and kOf cite it to convert subgroup members to multipliers. The definition is a direct identity on the placeholder type ℤ.
Claim. $\mathrm{toZ}(\delta, p) := p$ for $p \in \DeltaSub(\delta)$ where $\DeltaSub(\delta) := \mathbb{Z}$.
background
UnitMapping introduces DeltaSub δ as the type ℤ, described in the module doc as an abstract placeholder for the subgroup generated by δ using integers only for mapping. This differs from the precise subgroup in upstream LedgerUnits.DeltaSub and RecogSpec.Scales.DeltaSub, both defined as {x : ℤ // ∃ n : ℤ, x = n * δ}, whose toZ extracts the coefficient via Classical.choose.
The local setting treats the construction as a simplified interface for unit conversions without enforcing the full subgroup predicate at this layer. Upstream results also include LedgerUnits.toZ, which performs the extraction for the concrete subtype.
proof idea
One-line definition that returns the input p directly, serving as the identity on the placeholder ℤ type.
why it matters
This definition is the toFun component of equiv_delta in LedgerUnits, which establishes DeltaSub δ ≃ ℤ for nonzero δ. It is also invoked by fromZ_toZ, quantization (which asserts unique coefficients), rungOf and kOf. It supplies the integer extraction step that feeds the rung and quantization machinery in the unit-mapping layer of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.