toZ_one
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.
claimLet $Δ_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 in Recognition Science
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.
scope and limits
- Does not construct or prove properties of DeltaSub itself.
- Does not extend the projection to arbitrary δ values.
- Does not perform arithmetic or verify subgroup axioms.
- Does not handle non-integer generators or real-valued deltas.
Lean usage
def equiv_delta_one : DeltaSub 1 ≃ ℤ := { toFun := toZ_one, invFun := fromZ_one, left_inv := fromZ_toZ_one, right_inv := toZ_fromZ_one }formal statement (Lean)
13def toZ_one (p : DeltaSub 1) : ℤ := p.val
proof body
Definition body.
14