toZ_one
plain-language theorem explainer
The projection extracts the integer value from an element of the subgroup generated by one. Researchers establishing ledger unit equivalences cite this map when constructing the order isomorphism to the integers. The definition performs a direct field projection on the subtype.
Claim. Let $\DeltaSub(1) := \{ x \in \mathbb{Z} \mid \exists n \in \mathbb{Z}.\ x = n \cdot 1 \}$. Define the map $\mathrm{toZ\_one} : \DeltaSub(1) \to \mathbb{Z}$ by $\mathrm{toZ\_one}(p) := p.\mathrm{val}$.
background
LedgerUnits defines $\DeltaSub(\delta)$ as the subgroup of $\mathbb{Z}$ consisting of all integer multiples of $\delta$. Specializing to $\delta = 1$ produces a clean order isomorphism with $\mathbb{Z}$. Parallel definitions of $\DeltaSub$ appear in RecogSpec.Scales and UnitMapping, the latter treating it as an abstract placeholder for unit mappings.
The module documentation states that the subgroup of $\mathbb{Z}$ generated by $\delta$ is specialized to $\delta = 1$ for a clean order isomorphism. Upstream results supply the same $\DeltaSub$ definition across modules, confirming the subtype structure ${x : \mathbb{Z} // \exists n, x = n * \delta}$.
proof idea
One-line definition that directly accesses the .val field of the subtype.
why it matters
This projection supplies the forward map in the equivalence equiv_delta_one : DeltaSub 1 ≃ ℤ. That equivalence is invoked by fromZ_toZ_one, toZ_fromZ_one, and multiple delta-mapping lemmas in Scales. The construction realizes the module's specialization to δ = 1, enabling discrete scale handling in ledger units without extra structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.