toZ_fromZ
plain-language theorem explainer
The lemma establishes that coefficient extraction recovers the input integer after embedding an arbitrary integer into the subgroup generated by a nonzero integer δ. It is cited in constructions of equivalences between the subgroup and the integers, as well as in definitions of rung and step maps. The proof is a short term reduction that applies value computation, the specification of the extractor, and uniqueness of representation.
Claim. Let $Δ_δ$ denote the subgroup of $ℤ$ generated by a nonzero integer $δ$. For any integer $n$, the coefficient extraction map satisfies $toZ_δ(fromZ_δ(n)) = n$.
background
LedgerUnits models the cyclic subgroup $Δ_δ = {k δ | k ∈ ℤ}$ of the integers. The embedding fromZ δ n constructs the element whose value is n·δ, tagged with the witness n. The extractor toZ δ p returns the integer coefficient k such that p.val = k·δ, using choice on the property, with toZ_spec confirming the equality. rep_unique guarantees that this coefficient is unique when δ ≠ 0. The module document notes that the subgroup generated by δ specializes to δ = 1 for an order isomorphism to ℤ. Upstream results in UnitMapping supply the direct identification case when δ = 1.
proof idea
The proof first records that the value of the embedded element is n·δ. It introduces k as the result of applying the extractor to this element and uses toZ_spec to equate the value to k·δ. rep_unique with the hypothesis δ ≠ 0 then forces n = k. The concluding simplification substitutes the equality to finish the proof.
why it matters
This right-inverse property completes the data for the equivalence between the δ-subgroup and ℤ. It is applied in the definitions of coefficient extraction for from-natural and rung maps, as well as successor steps. In the Recognition Science setting these support the assignment of integer rungs on the phi-ladder for mass quantization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.