Suffix-prefix avoidance: |A|·|B| ≤ q^(2n)/(e n) (Zakharov 2026)

If A and B are sets of words of length n over q letters and no nonempty suffix of a word in A equals a prefix of a word in B, then |A| · |B| ≤ q^(2n)/(e n); more precisely n · |A| · |B| ≤ q^(2n) (n/(n+1))^(n+1) (D. Zakharov, arXiv:2602.20143, Theorem 1.1). The statement and definitions are those of google-deepmind/formal-conjectures (suffix_prefix_avoidance_bound, stated there with sorry). Proof: the overlap sets of all lengths decompose into disjoint pieces, giving the renewal-type inequality γ_j ≤ Σ γ_i δ_{j−i}; weighting by ρ^{j−1} with Σ δ_i ρ^i = 1 gives α γ_n ≤ (ρ−1)/ρ^(n+1), and AM-GM bounds the right side.

Main results

• SuffixPrefixAvoidance.zakharov_sharp: sharp form: n·|A|·|B| ≤ q^(2n)·(n/(n+1))^(n+1)
• SuffixPrefixAvoidance.zakharov_bound: |A|·|B| ≤ q^(2n)/(e n) (the formal-conjectures statement)

References

• D. Zakharov, «An isoperimetric inequality for word overlap», arXiv:2602.20143 v2 (2026), Thm 1.1.
• google-deepmind/formal-conjectures, FormalConjectures/Other/SuffixPrefixAvoidance.lean (Apache-2.0).

def SuffixPrefixAvoidance.wordSuffix {n q : ℕ} (w : Fin n → Fin q) (k : Fin n) : Fin (↑k + 1) → Fin q

The suffix of a word w : Fin n → Fin q of length k + 1 (the last k + 1 characters).

Equations

• SuffixPrefixAvoidance.wordSuffix w k i = w ⟨n - ↑k - 1 + ↑i, ⋯⟩

def SuffixPrefixAvoidance.wordPrefix {n q : ℕ} (w : Fin n → Fin q) (k : Fin n) : Fin (↑k + 1) → Fin q

The prefix of a word w : Fin n → Fin q of length k + 1 (the first k + 1 characters).

Equations

• SuffixPrefixAvoidance.wordPrefix w k i = w ⟨↑i, ⋯⟩

def SuffixPrefixAvoidance.IsSuffixPrefixAvoiding {n q : ℕ} (A B : Finset (Fin n → Fin q)) : Prop

Two sets of words $A, B$ over Fin q of length n are suffix-prefix avoiding if no nonempty suffix of any word in $A$ equals any prefix of any word in $B$ of the same length.

Equations

• SuffixPrefixAvoidance.IsSuffixPrefixAvoiding A B = ∀ a ∈ A, ∀ b ∈ B, ∀ (k : Fin n), SuffixPrefixAvoidance.wordSuffix a k ≠ SuffixPrefixAvoidance.wordPrefix b k

Real-analysis lemmas

noncomputable def SuffixPrefixAvoidance.Qs (ρ : ℝ) (δ : ℕ → ℝ) (k : ℕ) : ℝ

Qs ρ δ k = ∑_{i<k} ρ^i δ(i+1).

Equations

• SuffixPrefixAvoidance.Qs ρ δ k = ∑ i ∈ Finset.range k, ρ ^ i * δ (i + 1)

theorem SuffixPrefixAvoidance.Qs_succ (ρ : ℝ) (δ : ℕ → ℝ) (k : ℕ) : Qs ρ δ (k + 1) = Qs ρ δ k + ρ ^ k * δ (k + 1)

theorem SuffixPrefixAvoidance.Qs_zero (ρ : ℝ) (δ : ℕ → ℝ) : Qs ρ δ 0 = 0

theorem SuffixPrefixAvoidance.abel_sum (g f : ℕ → ℝ) (m : ℕ) : ∑ i ∈ Finset.range m, g i * (f (i + 1) - f i) = g m * f m - g 0 * f 0 - ∑ i ∈ Finset.range m, (g (i + 1) - g i) * f (i + 1)

Abel summation.

theorem SuffixPrefixAvoidance.weighted_identity (ρ : ℝ) (γ δ : ℕ → ℝ) (N : ℕ) : ∑ j ∈ Finset.range N, ρ ^ j * (δ (j + 1) + ∑ i ∈ Finset.range j, γ (i + 1) * δ (j - i) - γ (j + 1)) = Qs ρ δ N - ∑ j ∈ Finset.range N, ρ ^ j * γ (j + 1) * (1 - ρ * Qs ρ δ (N - 1 - j))

identity (3a) of Zakharov, section 2.

theorem SuffixPrefixAvoidance.geometric_weight (ρ : ℝ) (δ : ℕ → ℝ) (N : ℕ) : (ρ - 1) * ∑ j ∈ Finset.range N, ρ ^ j * (1 - ρ * Qs ρ δ (N - 1 - j)) = (1 - ∑ i ∈ Finset.range N, δ (i + 1)) * ρ ^ N + ρ * Qs ρ δ N - 1

identity (3b) of Zakharov, section 2.

theorem SuffixPrefixAvoidance.Qs_mono {ρ : ℝ} (hρ : 0 ≤ ρ) {δ : ℕ → ℝ} {n : ℕ} (hδ : ∀ i < n, 0 ≤ δ (i + 1)) {k : ℕ} (hk : k ≤ n) : Qs ρ δ k ≤ Qs ρ δ n

theorem SuffixPrefixAvoidance.exists_root (n : ℕ) (δ : ℕ → ℝ) (hδ : ∀ i < n, 0 ≤ δ (i + 1)) (hS : ∑ i ∈ Finset.range n, δ (i + 1) < 1) (hpos : ∃ k < n, 0 < δ (k + 1)) : ∃ (ρ : ℝ), 1 < ρ ∧ ρ * Qs ρ δ n = 1

Existence of ρ > 1 with F(ρ) = 1.

theorem SuffixPrefixAvoidance.amgm_final (n : ℕ) (hn : 0 < n) (ρ t : ℝ) (hρ : 1 < ρ) (ht : t * ρ ^ (n + 1) ≤ ρ - 1) : ↑n * t ≤ (↑n / (↑n + 1)) ^ (n + 1)

Final one-variable inequality: from t ρ^(n+1) ≤ ρ - 1 conclude n t ≤ (n/(n+1))^(n+1).

Words as lists

def SuffixPrefixAvoidance.Wd (q j : ℕ) : Finset (List (Fin q))

All words of length j, as lists.

Equations

• SuffixPrefixAvoidance.Wd q j = Finset.image List.ofFn Finset.univ

theorem SuffixPrefixAvoidance.mem_Wd {q : ℕ} {l : List (Fin q)} {j : ℕ} : l ∈ Wd q j ↔ l.length = j

theorem SuffixPrefixAvoidance.card_Wd {q : ℕ} (j : ℕ) : (Wd q j).card = q ^ j

def SuffixPrefixAvoidance.sfx {q : ℕ} (n : ℕ) (A : Finset (List (Fin q))) (j : ℕ) : Finset (List (Fin q))

Suffixes of length j of the words of A (all of length n).

Equations

• SuffixPrefixAvoidance.sfx n A j = Finset.image (fun (l : List (Fin q)) => List.drop (n - j) l) A

theorem SuffixPrefixAvoidance.sfx_length {n q : ℕ} {A : Finset (List (Fin q))} (hA : ∀ l ∈ A, l.length = n) {j : ℕ} (hj : j ≤ n) {x : List (Fin q)} (hx : x ∈ sfx n A j) : x.length = j

theorem SuffixPrefixAvoidance.sfx_drop {n q : ℕ} {A : Finset (List (Fin q))} {i j : ℕ} (hij : i ≤ j) (hj : j ≤ n) {x : List (Fin q)} (hx : x ∈ sfx n A j) : List.drop i x ∈ sfx n A (j - i)

theorem SuffixPrefixAvoidance.sfx_zero {n q : ℕ} {A : Finset (List (Fin q))} (hA : ∀ l ∈ A, l.length = n) (hne : A.Nonempty) : (sfx n A 0).card = 1

theorem SuffixPrefixAvoidance.card_sfx_succ_le {n q : ℕ} {A : Finset (List (Fin q))} (hA : ∀ l ∈ A, l.length = n) {j : ℕ} (hj1 : 1 ≤ j) (hjn : j ≤ n) : (sfx n A j).card ≤ q * (sfx n A (j - 1)).card

noncomputable def SuffixPrefixAvoidance.Dd {q : ℕ} (n : ℕ) (A : Finset (List (Fin q))) (i : ℕ) : Finset (List (Fin q))

Suffixes none of whose proper nonempty prefixes is again a suffix of that length.

Equations

• SuffixPrefixAvoidance.Dd n A i = {u ∈ SuffixPrefixAvoidance.sfx n A i | ∀ (k : ℕ), 1 ≤ k → k < i → List.take k u ∉ SuffixPrefixAvoidance.sfx n A k}

theorem SuffixPrefixAvoidance.mem_Dd {n q : ℕ} {A : Finset (List (Fin q))} {i : ℕ} {u : List (Fin q)} : u ∈ Dd n A i ↔ u ∈ sfx n A i ∧ ∀ (k : ℕ), 1 ≤ k → k < i → List.take k u ∉ sfx n A k

theorem SuffixPrefixAvoidance.card_sfx_le_sum {n q : ℕ} {A : Finset (List (Fin q))} (hA : ∀ l ∈ A, l.length = n) {j : ℕ} (hj1 : 1 ≤ j) (hjn : j ≤ n) : (sfx n A j).card ≤ ∑ i ∈ Finset.range j, (Dd n A (i + 1)).card * (sfx n A (j - 1 - i)).card

The renewal inequality (R): a_j ≤ ∑_{i=1}^{j} d_i a_{j-i}.

noncomputable def SuffixPrefixAvoidance.Ufin {q : ℕ} (n : ℕ) (A : Finset (List (Fin q))) : Finset (List (Fin q))

Words of length n with no prefix u.take k (1 ≤ k ≤ n) among the suffixes of length k.

Equations

• SuffixPrefixAvoidance.Ufin n A = {u ∈ SuffixPrefixAvoidance.Wd q n | ∀ (k : ℕ), 1 ≤ k → k ≤ n → List.take k u ∉ SuffixPrefixAvoidance.sfx n A k}

theorem SuffixPrefixAvoidance.mem_Ufin {n q : ℕ} {A : Finset (List (Fin q))} {u : List (Fin q)} : u ∈ Ufin n A ↔ u.length = n ∧ ∀ (k : ℕ), 1 ≤ k → k ≤ n → List.take k u ∉ sfx n A k

noncomputable def SuffixPrefixAvoidance.Xs {q : ℕ} (n : ℕ) (A : Finset (List (Fin q))) (i : ℕ) : Finset (List (Fin q))

Words of length n whose prefix of length i+1 is in D_{i+1}.

Equations

• SuffixPrefixAvoidance.Xs n A i = Finset.image (fun (p : List (Fin q) × List (Fin q)) => p.1 ++ p.2) (SuffixPrefixAvoidance.Dd n A (i + 1) ×ˢ SuffixPrefixAvoidance.Wd q (n - 1 - i))

theorem SuffixPrefixAvoidance.mem_Xs {n q : ℕ} {A : Finset (List (Fin q))} {i : ℕ} {u : List (Fin q)} : u ∈ Xs n A i ↔ ∃ a ∈ Dd n A (i + 1), ∃ (b : List (Fin q)), b.length = n - 1 - i ∧ u = a ++ b

theorem SuffixPrefixAvoidance.card_Ufin_add_sum_le {n q : ℕ} {A : Finset (List (Fin q))} (hA : ∀ l ∈ A, l.length = n) : (Ufin n A).card + ∑ i ∈ Finset.range n, (Dd n A (i + 1)).card * q ^ (n - 1 - i) ≤ q ^ n

Bridge from functions to lists

theorem SuffixPrefixAvoidance.ofFn_wordSuffix {n q : ℕ} (w : Fin n → Fin q) (k : Fin n) : List.ofFn (wordSuffix w k) = List.drop (n - (↑k + 1)) (List.ofFn w)

theorem SuffixPrefixAvoidance.ofFn_wordPrefix {n q : ℕ} (w : Fin n → Fin q) (k : Fin n) : List.ofFn (wordPrefix w k) = List.take (↑k + 1) (List.ofFn w)

theorem SuffixPrefixAvoidance.comb_facts {n q : ℕ} (A B : Finset (Fin n → Fin q)) (h : IsSuffixPrefixAvoiding A B) (hne : A.Nonempty) : ∃ (a : ℕ → ℕ) (d : ℕ → ℕ) (u : ℕ), a 0 = 1 ∧ a n = A.card ∧ B.card ≤ u ∧ (∀ (j : ℕ), 1 ≤ j → j ≤ n → a j ≤ q * a (j - 1)) ∧ (∀ (j : ℕ), 1 ≤ j → j ≤ n → a j ≤ ∑ i ∈ Finset.range j, d (i + 1) * a (j - 1 - i)) ∧ u + ∑ i ∈ Finset.range n, d (i + 1) * q ^ (n - 1 - i) ≤ q ^ n

The combinatorial facts.

The analytic core

theorem SuffixPrefixAvoidance.analytic_core (n : ℕ) (hn : 0 < n) (α e : ℕ → ℝ) (u : ℝ) (h0 : α 0 = 1) (hα0 : ∀ j ≤ n, 0 ≤ α j) (hmono : ∀ j < n, α (j + 1) ≤ α j) (he : ∀ j < n, 0 ≤ e (j + 1)) (hR : ∀ j < n, α (j + 1) ≤ ∑ i ∈ Finset.range (j + 1), e (i + 1) * α (j - i)) (hu : u + ∑ i ∈ Finset.range n, e (i + 1) ≤ 1) : ↑n * (α n * u) ≤ (↑n / (↑n + 1)) ^ (n + 1)

Zakharov's argument, section 2, on real sequences: α_j (suffix densities), e_j = |D_j| / q^j, u the density of the avoiding set.

The sharp inequality

theorem SuffixPrefixAvoidance.zakharov_sharp {n q : ℕ} (A B : Finset (Fin n → Fin q)) (hq : 0 < q) (hn : 0 < n) (h : IsSuffixPrefixAvoiding A B) : ↑n * ↑A.card * ↑B.card ≤ ↑q ^ (2 * n) * (↑n / (↑n + 1)) ^ (n + 1)

theorem SuffixPrefixAvoidance.pow_div_le_exp_neg_one (n : ℕ) (hn : 0 < n) : (↑n / (↑n + 1)) ^ (n + 1) ≤ Real.exp (-1)

(n/(n+1))^(n+1) ≤ exp (-1).

theorem SuffixPrefixAvoidance.zakharov_bound {n q : ℕ} (A B : Finset (Fin n → Fin q)) (hq : 0 < q) (hn : 0 < n) (h : IsSuffixPrefixAvoiding A B) : ↑A.card * ↑B.card ≤ ↑q ^ (2 * n) / (Real.exp 1 * ↑n)

Zakharov (2026), formal-conjectures form.