fromZ_toZ_one
plain-language theorem explainer
The lemma establishes that the projection from the δ=1 subgroup of integers back to ℤ is a left inverse for the embedding of ℤ into that subgroup. Ledger unit constructions and scale equivalences in Recognition Science cite this when assembling explicit order isomorphisms. The proof proceeds by case analysis on the subtype constructor, followed by an application of subtype extensionality and reflexivity.
Claim. Let $D_1 = { x : ℤ | ∃ n : ℤ, x = n · 1 }$. For every $p ∈ D_1$, the embedding of $p$'s underlying integer followed by the projection recovers $p$.
background
The LedgerUnits module introduces DeltaSub δ as the subgroup of ℤ consisting of all integer multiples of a fixed generator δ. Specializing to δ = 1 produces the full integers and permits a direct order isomorphism. The embedding fromZ_one sends an integer n to the subtype element whose witness is the trivial multiple n · 1, while toZ_one simply extracts the underlying integer value. Upstream integer constructors from IntegersFromLogic supply the pair-based representation used inside the subtype proofs.
proof idea
The term-mode proof performs case analysis on the subtype constructor mk x hx of the input p. It then invokes Subtype.ext to reduce the goal to equality of the underlying values, which holds by reflexivity.
why it matters
The result supplies the left-inverse leg of the equivalence between the δ=1 subgroup and ℤ. That equivalence is defined in the same module and re-exported in RecogSpec.Scales, where it supports ledger-unit arithmetic and scale constructions. The lemma therefore closes one direction of the bijection required for clean integer representations inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.