toZ_fromZ_one
plain-language theorem explainer
The lemma asserts that projecting an integer after embedding it into the δ=1 subgroup recovers the original value. Researchers defining equivalences between ℤ and DeltaSub 1 in scale constructions cite it to enable simplification during round-trip proofs. The proof is immediate reflexivity from the mutual definitions of the embedding and projection.
Claim. For every integer $n$, the projection toZ$_1$ applied to the embedding fromZ$_1(n)$ equals $n$, where fromZ$_1$ sends $n$ to the element $n·1$ in the δ=1 subgroup and toZ$_1$ extracts the integer coefficient.
background
The RecogSpec.Scales module treats binary scales via embeddings into delta subgroups. DeltaSub 1 is the subgroup of elements whose value is an integer multiple of the unit 1. The embedding fromZ_one maps $n : ℤ$ to the pair ⟨n, ⟨n, by simpa using (Int.mul_one n)⟩⟩, while toZ_one simply returns the .val component of any such pair.
proof idea
The proof is a one-line wrapper that applies reflexivity, which holds because fromZ_one and toZ_one are defined as literal inverses on the δ=1 subgroup.
why it matters
This lemma supplies the right inverse for equiv_delta_one, the explicit equivalence DeltaSub 1 ≃ ℤ that appears in both LedgerUnits and RecogSpec.Scales. It closes the integer round-trip needed for binary scale definitions and the φ-exponential wrappers described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.