toZ_spec
plain-language theorem explainer
The lemma asserts that the embedded value of any element p in the subgroup generated by an integer δ equals δ multiplied by the coefficient extracted via the choice operator. Researchers formalizing integer quantization for ledger units cite this when confirming that the extraction recovers the defining multiple. The proof is a direct one-line wrapper around the specification property of Classical.choose.
Claim. Let $\delta \in \mathbb{Z}$ and let $p$ belong to the subgroup of $\mathbb{Z}$ generated by $\delta$. Then the embedded integer value of $p$ equals $\delta$ multiplied by the integer coefficient selected for $p$ by the choice-based extraction map.
background
DeltaSub $\delta$ is the set of all integers $x$ for which there exists an integer $n$ satisfying $x = n \delta$; this is the subgroup generated by $\delta$. The extraction map toZ $\delta$ $p$ is defined noncomputably by applying Classical.choose to the existence witness stored in the subtype property of $p$. The module specializes the construction to $\delta = 1$ to obtain a clean order isomorphism with $\mathbb{Z}$.
proof idea
This is a one-line wrapper that applies Classical.choose_spec directly to the property field of the input subtype element.
why it matters
The result supplies the existence direction used inside the quantization theorem of the same module and is invoked by the round-trip lemmas fromZ_toZ and toZ_fromZ. It thereby supports the claim that every element of the $\delta$-subgroup admits an integer coefficient representation. In the Recognition framework this step anchors the ledger-unit mapping that connects abstract coefficients to physical scales via the $\phi$-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.