toZ_spec
plain-language theorem explainer
The lemma asserts that the representative value of any element p in the δ-generated subgroup of ℤ equals the coefficient returned by toZ multiplied by δ. Ledger unit quantization arguments cite this to justify extracting integer coefficients from subgroup elements. The proof is a one-line wrapper invoking the specification property of Classical.choose on the existence witness inside p.
Claim. Let $δ ∈ ℤ$ and let $p$ belong to the subgroup $ΔSub(δ) = {x ∈ ℤ | ∃ n ∈ ℤ, x = n δ}$. Then the representative value satisfies $p.val = toZ(δ, p) · δ$.
background
DeltaSub δ is the subtype {x : ℤ // ∃ n : ℤ, x = n * δ}, the subgroup of ℤ generated by δ. The noncomputable function toZ extracts a coefficient by applying Classical.choose to the existence proof stored in p.property. The module specializes this construction to δ = 1 to obtain a clean order isomorphism between ℤ and the subgroup.
proof idea
One-line wrapper that applies Classical.choose_spec directly to the property field of p.
why it matters
Supplies the existence half of the quantization theorem, which states that every element of the δ-subgroup admits a unique integer coefficient when δ ≠ 0. It is invoked inside the proofs of fromZ_toZ and toZ_fromZ to close the round-trip identities. In the Recognition framework this supports the integer coefficient extraction required for the phi-ladder mass formulas and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.