Suffix-prefix avoidance bound

Let $A$ and $B$ be sets of words of length $n$ over an alphabet with $q$ letters. If no (nonempty) suffix of any word in $A$ coincides with a prefix of any word in $B$, then $$|A| \cdot |B| \leq \frac{q^{2n}}{en}.$$

References:

• X post by Dmitry Rybin
• [Maximal sets of strings with no prefix-suffix overlap] (https://mathoverflow.net/questions/508648/maximal-sets-of-strings-with-no-prefix-suffix-overlap) by Dmitry Rybin, MathOverflow (2026)
• An isoperimetric inequality for word overlap by Dmitrii Zakharov (2026)

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

theorem SuffixPrefixAvoidance.words_naive_bound {n q : ℕ} (A B : Finset (Fin n → Fin q)) : A.card * B.card ≤ q ^ (2 * n)

$A$ and $B$ are sets of words of length $n$ over alphabet with $q$ letters. Trivially then $|A| \cdot |B|$ is at most $q^{2n}$.

theorem SuffixPrefixAvoidance.suffix_prefix_avoidance_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)

$A$ and $B$ are sets of words of length $n$ over alphabet with $q \geq 1$ letters. No suffix of a word in $A$ coincides with a prefix of a word in $B$. Then $|A| \cdot |B|$ is at most $\frac{q^{2n}}{en}$.

This problem is from Maximal sets of strings with no prefix-suffix overlap and was proved in An isoperimetric inequality for word overlap.

theorem SuffixPrefixAvoidance.suffix_prefix_avoidance_weaker_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) / ↑n

$A$ and $B$ are sets of words of length $n$ over alphabet with $q \geq 1$ letters. No suffix of a word in $A$ coincides with a prefix of a word in $B$. Then $|A| \cdot |B|$ is at most $\frac{q^{2n}}{n}$.