fromZ
The fromZ definition embeds an integer n directly into the abstract δ-subgroup by returning n, since DeltaSub δ is set to ℤ. Researchers building unit mappings and integer equivalences in LedgerUnits cite it when constructing fromNat, rungOf, and equiv_delta. The implementation is a one-line assignment that acts as a placeholder simplifying the subgroup structure.
claimFor any integers $δ$ and $n$, fromZ$(δ, n) := n$, where $Δ$Sub$(δ)$ denotes the integers $ℤ$.
background
In the UnitMapping module, DeltaSub δ is defined as the type ℤ, serving as an abstract placeholder for the subgroup generated by δ. This differs from the upstream LedgerUnits definition, where DeltaSub δ = {x : ℤ // ∃ n : ℤ, x = n * δ} and fromZ embeds via the pair ⟨n * δ, ⟨n, rfl⟩⟩. The module doc describes the setting as an abstract placeholder using integers for mapping only.
proof idea
One-line definition that directly assigns the input n to the DeltaSub δ type (which is ℤ). No tactics or lemmas are applied; the body is the identity map in this simplified representation.
why it matters in Recognition Science
This definition supplies the inverse map for equiv_delta in LedgerUnits and is used by fromNat, rungOf_fromZ, kOf_fromZ, and toZ_fromZ. It supports the unit-mapping layer that feeds rung and charge calculations in the Recognition framework, enabling the integer coefficient handling that underlies the phi-ladder and eight-tick octave steps.
scope and limits
- Does not construct the actual subgroup membership witness for general δ.
- Does not enforce or check the condition δ ≠ 0.
- Does not compute derived quantities such as rungOf or kOf.
- Does not reference J-cost, phi, or Recognition Composition Law.
Lean usage
noncomputable def fromNat (δ : ℤ) (m : Nat) : DeltaSub δ := fromZ δ (Int.ofNat m)formal statement (Lean)
13@[simp] def fromZ (δ : ℤ) (n : ℤ) : DeltaSub δ := n