toZ
plain-language theorem explainer
The definition extracts the integer coefficient n for which an element p of the subgroup generated by a fixed integer δ satisfies p = n δ. Ledger unit constructions and quantization arguments cite this map to obtain rung indices and coefficients. It is realized by a one-line classical choice on the existence witness inside the subtype.
Claim. For a fixed integer $δ$ and an element $p$ of the subgroup of integers generated by $δ$, that is $p ∈ {x ∈ ℤ | ∃ n ∈ ℤ, x = n δ}$, the value toZ(δ, p) is an integer $n$ such that $p = n δ$.
background
DeltaSub δ is the subtype of ℤ consisting of all integer multiples of δ. The module document states that this subgroup is specialized to δ = 1 to obtain a clean order isomorphism with ℤ. Upstream definitions of the same subgroup appear in RecogSpec.Scales and UnitMapping, where the latter defines its toZ simply as the identity on the placeholder type.
proof idea
The definition is a one-line wrapper that invokes Classical.choose on the property field of the subtype element p, which encodes the existence of the coefficient n.
why it matters
This extraction is used to build the equivalence equiv_delta that identifies DeltaSub δ with ℤ for nonzero δ, and it appears inside the quantization theorem asserting unique integer coefficients for every element. It also defines rungOf and kOf for indexing. In the Recognition Science framework it supplies the integer steps required for the phi-ladder mass formula and scaling relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.