fromZ_toZ_one
plain-language theorem explainer
The lemma shows that projecting an element of the δ=1 subgroup back to ℤ and re-embedding recovers the original element. Researchers building ledger unit isomorphisms and binary scales in Recognition Science cite it to confirm the left inverse. The proof reduces to case analysis on the subtype constructor followed by extensionality.
Claim. Let $p$ belong to the subgroup $Delta_1 = {x in Z | exists n in Z, x = n * 1}$. Then fromZ_1(toZ_1(p)) = p.
background
The module treats binary scales and φ-exponential wrappers. DeltaSub δ is the subgroup of integers consisting of all multiples of a fixed δ; the case δ=1 yields a clean copy of ℤ. The maps fromZ_one and toZ_one are the standard embedding of ℤ into this subgroup and the projection that extracts the underlying integer value. Upstream integer and rational constructions from IntegersFromLogic and RationalsFromLogic supply the arithmetic foundation for these maps.
proof idea
The term proof cases on the subtype constructor mk x hx of p. It then applies Subtype.ext to reduce equality of subtype elements to equality of their underlying integers, which holds by reflexivity.
why it matters
The lemma supplies the left inverse for equiv_delta_one : DeltaSub 1 ≃ ℤ, which is defined in both LedgerUnits and the present module. It supports the integer embeddings required for binary scales that later feed the φ-ladder and mass formulas. In the Recognition framework this isomorphism underpins the clean handling of integer multiples inside the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.