separated copies alphabet
ProvedFreiman.separated_copies_alphabetcontinued-fractionshall-raynumber-theory
The separated copied word uses only digits of the original word and the separator 2, hence has a finite alphabet whenever the original does.
Preamble
import Definitions.Def_Freiman_wordRealization open Freiman
Formal statement
theorem Freiman.separated_copies_alphabet (a b : ℤ → ℕ+) (N : ℕ) (hcopy : SeparatedCopies a b N) (ha : HasFiniteAlphabet a) :
HasFiniteAlphabet b := by sorrySource
Freiman's Hall ray: Proof report and corrected English text, 8 September 2026, §1.6, Theorem 1.9 (found:separated-peaks), proof by separated copies.