fromZ_toZ
plain-language theorem explainer
Lemma fromZ_toZ asserts that the composition fromZ δ ∘ toZ δ recovers the original element of the subgroup DeltaSub δ. Researchers building ledger unit equivalences in Recognition Science cite this to confirm the left inverse when defining equiv_delta. The short proof reduces the subtype equality via Subtype.ext and simplifies directly with toZ_spec.
Claim. For any integer δ and any p in the subgroup Δ_δ = {x ∈ ℤ | ∃ n ∈ ℤ, x = n δ}, the maps satisfy fromZ_δ(toZ_δ(p)) = p.
background
DeltaSub δ is the subtype of ℤ consisting of all integer multiples of δ. The map fromZ δ n embeds n as the element n·δ inside this subtype, while toZ δ p extracts the coefficient n such that the underlying value of p equals n·δ, using Classical.choose on the existence witness from the subtype property. The module LedgerUnits introduces these maps to support order isomorphisms, with a specialization to δ = 1 noted in the module documentation.
proof idea
The proof applies Subtype.ext to reduce the claim to equality of the underlying integer values. It then invokes simpa with the definitions of fromZ and the specification lemma toZ_spec δ p, which directly yields the required identity.
why it matters
This lemma supplies the left inverse for equiv_delta, the equivalence DeltaSub δ ≃ ℤ used for any nonzero δ. It completes the round-trip property inside the ledger unit construction that supports discrete scaling steps on the phi-ladder. No open questions are addressed; the result closes the embedding for the subgroup without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.