toZ_fromZ_one
plain-language theorem explainer
The lemma shows that embedding any integer n into the δ=1 subgroup and projecting back recovers n exactly. It is referenced when building order isomorphisms between the subgroup and ℤ in ledger and scale constructions. The proof is immediate reflexivity because the embedding stores n as the subtype value and the projection returns that value.
Claim. For every integer $n$, if $ι$ embeds $n$ into the subgroup $Δ_1$ generated by 1 and $π$ projects by extracting the coefficient, then $π(ι(n)) = n$.
background
The LedgerUnits module defines DeltaSub δ as the subgroup of ℤ generated by a fixed δ. Here δ is specialized to 1. The embedding fromZ_one maps n to the subtype element ⟨n, proof that n is a multiple of 1⟩. The projection toZ_one returns the underlying integer value p.val. The module documentation states that this specialization yields a clean order isomorphism. Parallel definitions exist in the RecogSpec.Scales module.
proof idea
One-line reflexivity proof. The term fromZ_one n constructs a subtype whose .val field is n, and toZ_one returns exactly that field, so the composition equals n by definition.
why it matters
Supplies the right inverse for equiv_delta_one, the explicit equivalence DeltaSub 1 ≃ ℤ. It is used in both LedgerUnits and RecogSpec.Scales. This supports integer lattice handling that feeds into the phi-ladder and the eight-tick octave in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.