toZ_spec
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.
claimLet $δ ∈ ℤ$ 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 in Recognition Science
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.
scope and limits
- Does not establish uniqueness of the extracted coefficient.
- Does not assume or require δ ≠ 0.
- Applies only inside the subtype representation of DeltaSub.
- Does not extend to non-integer generators or other base rings.
formal statement (Lean)
37lemma toZ_spec (δ : ℤ) (p : DeltaSub δ) : p.val = toZ δ p * δ :=
proof body
One-line wrapper that applies Classical.choose_spec.
38 Classical.choose_spec p.property
39