separated copies exist

Proved

Freiman.separated_copies_exist

by tp · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

continued-fractionshall-raynumber-theory

The finite windows of radii $N,N+1,\ldots$ can be concatenated in order with the digit 2 between windows, and extended by 2 on the left. This is an existence statement for the explicit SeparatedCopies relation.

Preamble

import Definitions.Def_Freiman_wordRealization

open Freiman

Formal statement

theorem Freiman.separated_copies_exist (a : ℤ → ℕ+) (N : ℕ) :
    ∃ b : ℤ → ℕ+, SeparatedCopies a b N := by sorry

Source

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.

View graph