equiv_delta_one
The declaration supplies an explicit order isomorphism between the subgroup of integers generated by 1 and ℤ itself. Ledger unit specialists cite it when reducing the δ=1 case to ordinary integer arithmetic inside the Recognition framework. The construction is a direct assembly of the embedding map, its projection inverse, and the two mutual-inverse lemmas already proved for those maps.
claimThe subgroup generated by 1, written as the set of all integer multiples of 1, is isomorphic to ℤ via the map that sends each multiple n·1 to the coefficient n.
background
The module defines DeltaSub δ as the subgroup of ℤ consisting of all integer multiples of a fixed generator δ. Specializing to δ = 1 yields the full group of integers and therefore admits a canonical order isomorphism. The sibling definitions supply the concrete embedding fromZ_one that sends n to the element n·1 and the projection toZ_one that recovers the coefficient.
proof idea
The definition is a one-line wrapper that assembles an equivalence structure by setting the forward map to toZ_one, the inverse map to fromZ_one, and the left and right inverse proofs to the lemmas fromZ_toZ_one and toZ_fromZ_one respectively.
why it matters in Recognition Science
This equivalence is invoked by the Scales module to reduce δ=1 ledger units to ordinary integer arithmetic. It completes the specialization step inside the ledger-unit construction, allowing integer properties to transfer directly into the Recognition framework before the general-δ case is treated. The construction supports the clean handling of the unity generator that appears in the forcing-chain specialization to D = 3.
scope and limits
- Does not treat subgroups generated by any δ other than 1.
- Does not address non-discrete or non-integer realizations.
- Does not incorporate phi-ladder scaling or mass formulas.
- Does not prove uniqueness of the isomorphism beyond the explicit maps supplied.
formal statement (Lean)
24def equiv_delta_one : DeltaSub 1 ≃ ℤ :=
proof body
Definition body.
25{ toFun := toZ_one
26, invFun := fromZ_one
27, left_inv := fromZ_toZ_one
28, right_inv := toZ_fromZ_one }
29
30/-! ### General δ ≠ 0: non-canonical equivalence n•δ ↦ n -/
31