fromZ
plain-language theorem explainer
fromZ δ n constructs the element n·δ inside the subgroup generated by δ, supplying the witness n for membership. Downstream code in equiv_delta and rungOf_fromZ cites it to convert between coefficients and subgroup elements. The implementation is a one-line subtype constructor using multiplication and reflexivity.
Claim. Define fromZ(δ, n) := n δ where the codomain is the subgroup Δ_δ = {x ∈ ℤ | ∃ m ∈ ℤ, x = m δ}.
background
DeltaSub δ is the subgroup of ℤ consisting of all integer multiples of a fixed generator δ, formalized as the subtype {x : ℤ // ∃ n : ℤ, x = n * δ}. The LedgerUnits module introduces this to handle discrete steps in unit mappings, specializing to δ = 1 for an isomorphism with ℤ. Upstream results include the abstract DeltaSub placeholder in UnitMapping (where it reduces to ℤ) and the same definition in RecogSpec.Scales, which supply the subgroup structure used here.
proof idea
The definition is a direct subtype constructor that packages the value n * δ with the existential witness ⟨n, rfl⟩ certifying membership in DeltaSub δ.
why it matters
This definition supplies the inverse map for the equivalence equiv_delta (δ : ℤ) (hδ : δ ≠ 0) : DeltaSub δ ≃ ℤ, which is invoked by rungOf_fromZ, kOf_fromZ, and toZ_fromZ to extract coefficients for rung and k-index calculations. In the Recognition Science framework it supports the phi-ladder mass formula by providing the discrete embedding of rung steps, linking to the eight-tick octave through the unit mapping chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.