fromZ_one
plain-language theorem explainer
Defines the embedding of each integer into the subgroup of integers generated by one. Researchers constructing scale equivalences and ledger unit maps in Recognition Science cite this construction. The definition proceeds by direct packaging of the integer with its membership witness via the multiplicative identity.
Claim. Let $Δ_1$ denote the subgroup of $ℤ$ consisting of all integer multiples of 1. The embedding $ι:ℤ→Δ_1$ sends each integer $n$ to the element $n$, witnessed by the factorization $n=n·1$.
background
LedgerUnits defines DeltaSub δ as the set of integers x for which there exists an integer k with x equal to k times δ. Specializing to δ equal to 1 produces a subgroup that coincides with all of ℤ, enabling a direct order isomorphism as noted in the module documentation. This choice supports clean algebraic handling of units without additional scaling factors.
proof idea
The definition constructs the subtype element by pairing the input integer with an explicit witness of membership. It invokes the mul_one identity from ArithmeticFromLogic and packages the result via the subtype constructor and simpa tactic.
why it matters
This embedding supplies the inverse map required by the equivalence equiv_delta_one that identifies the δ=1 subgroup with ℤ. It is reused in the Scales module for delta mappings and step functions. The construction supports invertible transformations in ledger accounting within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.