quantization
plain-language theorem explainer
Every element x of the subgroup generated by nonzero integer δ admits a unique integer n such that x.val equals n times δ. Ledger constructions in periodic tables, fluid simulations, and phi-ladder arguments cite the result for coefficient extraction. The tactic proof obtains the witness via toZ_spec and establishes uniqueness via rep_unique.
Claim. Let $δ ∈ ℤ$ with $δ ≠ 0$. For every $x$ belonging to the subgroup of integers generated by δ, there exists a unique integer $n$ such that the underlying value of $x$ equals $n · δ$.
background
DeltaSub δ is defined as the set of integers x for which there exists an integer n with x = n δ. The auxiliary function toZ δ x returns the coefficient n witnessing membership, while toZ_spec asserts that the underlying value satisfies p.val = toZ δ p · δ. The supporting lemma rep_unique states that n δ = m δ together with δ ≠ 0 forces n = m.
proof idea
The tactic proof enables classical choice, then refines the witness toZ δ x paired with the equality supplied by toZ_spec. For uniqueness it assumes another multiplier m, equates the two representations of x.val, and invokes rep_unique to conclude the multipliers coincide.
why it matters
The result supplies the unique coefficient map required by phi_ladder_stable and by conservation_is_unconditional. It is also invoked by nobleGasZFull, ChernNumber, and decodeCoeff. The theorem therefore closes the quantization step that converts the δ-subgroup into an ordered copy of ℤ, feeding the eight-tick octave and D = 3 constructions downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.