toZ_fromZ
plain-language theorem explainer
The round-trip property for coefficient extraction in δ-generated subgroups of ℤ asserts that toZ recovers the original integer n after fromZ embeds it as a multiple of nonzero δ. Ledger unit constructions and rung mappings in Recognition Science cite this to preserve integer quantization labels across equivalent subgroups. The proof is a direct reflexivity reduction once the definitions of fromZ as the coefficient embedding and toZ as the chosen representative are inlined.
Claim. For nonzero integer $δ$ and any integer $n$, if fromZ$_δ(n)$ denotes the element $n·δ$ in the subgroup generated by $δ$ and toZ$_δ$ extracts the unique integer coefficient of that element, then toZ$_δ$(fromZ$_δ(n)) = n$.
background
UnitMapping supplies the basic maps between integer coefficients and elements of DeltaSub δ, the subgroup of ℤ generated by a fixed nonzero integer δ. fromZ δ n constructs the subgroup element corresponding to coefficient n while toZ δ p recovers that coefficient via Classical.choose on the subgroup membership proof. The module treats these maps as abstract placeholders that use integers only for the mapping structure, without reference to physical units.
proof idea
The proof is a one-line term-mode reflexivity. It follows at once from the definition of fromZ in UnitMapping together with the extraction performed by toZ, which by construction returns the coefficient that was supplied to fromZ.
why it matters
This lemma supplies the right-inverse direction required by the equivalence equiv_delta δ hδ : DeltaSub δ ≃ ℤ. Downstream lemmas such as kOf_fromZ, rungOf_fromZ, and kOf_step_succ apply it via simp to keep integer coefficients consistent in ledger unit arithmetic. It thereby supports the quantization steps that feed into the phi-ladder rung assignments and the eight-tick octave structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.