toZ_spec
plain-language theorem explainer
The lemma asserts that for any p in the subgroup of integers generated by δ, the embedded value equals the coefficient returned by toZ multiplied by δ. It is cited by the quantization theorem and the fromZ/toZ round-trip lemmas. The proof is a one-line wrapper around Classical.choose_spec.
Claim. For any integer $\delta$ and $p$ in the subgroup $\DeltaSub(\delta) = \{x \in \mathbb{Z} \mid \exists n \in \mathbb{Z},\ x = n\delta\}$, one has $p.\mathrm{val} = \mathrm{toZ}(\delta,p) \cdot \delta$.
background
DeltaSub $\delta$ is the subgroup of $\mathbb{Z}$ consisting of all integer multiples of $\delta$, written ${x : \mathbb{Z} // \exists n : \mathbb{Z},\ x = n * \delta}$. The auxiliary definition toZ $\delta$ $p$ is the noncomputable selection, via Classical.choose, of an integer $n$ satisfying the membership witness in $p$.property. The module specializes the construction to $\delta=1$ to obtain a clean order isomorphism with $\mathbb{Z}$.
proof idea
The proof is a one-line wrapper that applies Classical.choose_spec directly to $p$.property.
why it matters
This lemma supplies the existence direction inside the quantization theorem of the same module, which states that every element of the $\delta$-subgroup admits a unique integer coefficient. It is invoked by fromZ_toZ and toZ_fromZ to close the round-trip identities. In the Recognition framework it anchors the ledger-unit construction that converts between abstract scales and integer coefficients, supporting the discrete structure required by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.