toZ_one
plain-language theorem explainer
Defines the projection from the subgroup of integers generated by 1 back to the integers by extracting the underlying value of the subtype. Ledger unit and scale mappings in Recognition Science cite this when building explicit order isomorphisms. The definition is a direct one-line extraction from the subtype constructor.
Claim. Let $\DeltaSub(1)$ be the subgroup of $\mathbb{Z}$ consisting of all integer multiples of 1. The projection map $\DeltaSub(1) \to \mathbb{Z}$ sends each subtype element $p$ to its underlying integer value $p.\mathrm{val}$.
background
DeltaSub($\delta$) is the subtype of $\mathbb{Z}$ whose elements are integer multiples of a fixed generator $\delta$. The module specializes to $\delta = 1$ to obtain a clean order isomorphism with $\mathbb{Z}$ itself. The same subgroup definition appears in RecogSpec.Scales and UnitMapping, where it serves as an abstract placeholder for integer-based mappings.
The local setting is the subgroup of $\mathbb{Z}$ generated by $\delta$, with the $\delta=1$ case chosen to simplify the correspondence between subgroup elements and ordinary integers. Upstream results supply the identical DeltaSub definition in three modules, confirming that the construction is shared across ledger and scale layers.
proof idea
One-line definition that returns the .val field of the subtype p : DeltaSub 1.
why it matters
This definition supplies the forward component of the equivalence equiv_delta_one that identifies DeltaSub 1 with $\mathbb{Z}$. It therefore anchors the order-isomorphism machinery used by fromZ_toZ_one, toZ_fromZ_one and the mapDeltaOne lemmas in both LedgerUnits and RecogSpec.Scales. The construction directly supports the clean integer representation required for unit mappings in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.