toZ_one
plain-language theorem explainer
The projection extracts the underlying integer from any element of the subgroup generated by δ=1. Ledger unit mappings and scale equivalences cite this when converting between the subtype and base integers. It is realized as a direct field access on the subtype constructor.
Claim. Let $Δ_1 = {x ∈ ℤ | ∃ n ∈ ℤ, x = n · 1}$. The map toZ_one : $Δ_1 → ℤ$ is defined by toZ_one(p) = p.val for p ∈ $Δ_1$.
background
DeltaSub δ is the subgroup of ℤ consisting of all integer multiples of δ. Specializing to δ=1 produces the full ring ℤ equipped with a clean order isomorphism. The module uses this case to support ledger unit mappings that convert scaled deltas back to base integers. Upstream definitions in Scales and UnitMapping supply the identical subgroup construction for cross-module consistency.
proof idea
One-line definition that returns the .val field of the subtype element p : DeltaSub 1.
why it matters
It supplies the forward map for equiv_delta_one, the explicit equivalence DeltaSub 1 ≃ ℤ. This equivalence underpins ledger unit isomorphisms and feeds into affine map lemmas such as mapDeltaOne_fromZ_one in RecogSpec.Scales. The construction closes the δ=1 case of the order isomorphism used throughout the ledger and scale layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.