Canonical cyclic factors of the p-adic odometer
Abstract
Continuous symbolic observations of a p-adic adding machine have one finite cyclic resolution for every starting point and all integer times.
Theorem 1.1 (One residue depth reconstructs every symbolic coordinate).
Lean statement: D5/S1/Dynamics/OdometerCyclicFactor.exists_cyclic_factor_of_shift_equivariant
Proof. Machine-checked in Lean as D5/S1/Dynamics/OdometerCyclicFactor.exists_cyclic_factor_of_shift_equivariant (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let p be prime, A any discrete topological space, and Φ:Z_p→A^Z continuous. Assume Φ(x+1)(n)=Φ(x)(n+1) for every p-adic integer x and every integer n. Then there exist N≥0 and w:Z/(p^N)Z→A such that, simultaneously for every x and n, Φ(x)(n)=w(π_N(x)+n), where π_N is the actual Mathlib ring homomorphism PadicInt.toZModPow N. The alphabet A need not be finite.
The zero-coordinate observation c(x)=Φ(x)(0) is continuous and locally constant. Its fibers cover compact Z_p. A Lebesgue number gives one radius δ>0 on which c is constant, independently of x. Choose N with p^(-N)<δ. Equal π_N residues put x-y in the ideal generated by p^N; Mathlib’s kernel and norm theorems give distance at most p^(-N), so c agrees on every canonical residue fiber. Set w(a)=c(a.val), using the natural representative of the finite residue.
Integer induction on equivariance, with a separate backward step using x-1, shows Φ(x)(n)=c(x+n) for both positive and negative n. Applying the one quotient factorization and the ring-homomorphism addition law gives the displayed formula. The same N controls all initial points and all times; it is not chosen separately for each orbit. The case N=0 is retained and gives a constant symbolic factor.
This is a classical compactness and equicontinuity consequence. The existing EquicontinuousObservationPeriod theorem supplies a general positive observation period; this result additionally identifies the canonical p-power residue quotient and reconstructs the complete two-sided name through it. It supplies no effective algorithm for finding N from an arbitrary continuity proof and no uniform bound on N independent of the observer.