equiv_delta_one
plain-language theorem explainer
The definition supplies an explicit order isomorphism between the subgroup of integers generated by 1 and the integers themselves. Researchers modeling discrete scale hierarchies in Recognition Science cite it when indexing phi-exponential growth steps against the integer lattice. The construction directly assembles the forward and inverse maps from the embedding and projection functions already available for the delta-equals-1 case.
Claim. Let $Delta_1 = { x in Z | exists n in Z, x = n cdot 1 }$. There exists an equivalence $Delta_1 simeq Z$ sending the generator multiple $n cdot 1$ to the integer $n$.
background
DeltaSub delta is the subgroup of Z consisting of all integer multiples of a fixed generator delta; the case delta equals 1 recovers the full lattice Z. The module treats binary scales and phi-exponential wrappers, with the scale function defined upstream as phi raised to the power k. The from theorem reduces seven independent axioms to four structural conditions plus three definitional facts, while the for structure records meta-realization properties required by self-reference.
proof idea
The definition builds the equivalence by supplying toFun as the projection toZ_one, invFun as the embedding fromZ_one, and the two inverse properties fromZ_toZ_one and toZ_fromZ_one. It is a direct structure construction that reuses the already-established embedding and projection lemmas for the delta-equals-1 subgroup.
why it matters
The equivalence supplies clean integer indexing for the affine maps that project units onto scales in the Scales namespace. It supports the phi-ladder and eight-tick octave steps in the forcing chain by allowing direct mapping of rung indices. The result is referenced by the LedgerUnits handling of delta-subgroups and feeds into larger constructions that connect discrete steps to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.