equiv_delta_one
plain-language theorem explainer
The definition supplies an explicit isomorphism between the subgroup of integers generated by 1 and the integers themselves. Ledger unit calculations in the Recognition framework cite this when specializing the δ-generated subgroup to the unit case. It is assembled directly from the embedding map, its inverse, and the two lemmas establishing that they are mutual inverses.
Claim. Let $Δ_1 = { x ∈ ℤ | ∃ n ∈ ℤ, x = n · 1 }$. Then there is an equivalence $Δ_1 ≃ ℤ$ whose forward map sends the integer $n$ to the element $n$ in the subgroup and whose inverse projects back to the integer value.
background
The module LedgerUnits defines DeltaSub δ as the subgroup of ℤ consisting of all integer multiples of a fixed generator δ. Specializing to δ = 1 makes this subgroup coincide with all of ℤ, allowing a clean order isomorphism. The equivalence is built from the embedding fromZ_one that sends n to the pair (n, proof that n is a multiple of 1) and the projection toZ_one that recovers the integer.
proof idea
This is a direct definition that assembles the equivalence by setting the forward map to toZ_one, the inverse map to fromZ_one, and verifying the inverses with the lemmas fromZ_toZ_one and toZ_fromZ_one.
why it matters
It provides the identification needed for δ = 1 cases in the ledger units and is referenced by the equiv_delta_one declaration in RecogSpec.Scales. This supports the framework's handling of generated subgroups in the context of the Recognition Composition Law and the forcing chain steps leading to integer arithmetic. It closes a step for reducing subgroup statements to standard ℤ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.