定理 #332

新規性調査・形式検証レポート（2026年9月13日、Codexによる）

評価：対象版のConjecture 5.6(i)・(ii)への数学的反例は証明済み。反例指摘の先行報告は調査範囲で未確認、初出は未確定である。数値の既出性と反例としての位置づけを区別する。

対象版との照合
Stephen McKean, Toda primes, arXiv:2511.19744v1（2025年11月24日）。2026年9月13日に確認したarXivのsubmission historyはv1のみで、同日に読んだ著者サイトのPDF第8頁でもConjecture 5.6の両項は同じ主張だった。
https://arxiv.org/abs/2511.19744
https://arxiv.org/html/2511.19744v1#S5.SS1
https://shmckean.github.io/research/toda.pdf#page=8

(i) a＝29、m＝59、d＝1770は、分母の一致だけでなくF(1770)＝116という最小性も満たすため、全前提を満たした反例である。原論文のTable 1にはT(29)＝{3,5,59}が既にある。T(1711)と組にして5.6(i)を否定する先行記述は確認できなかった。Lemma 5.7は追加条件の下の十分条件であり、この反例はその補題を否定しない。実際、p＝59に対する候補119,237,3423,6845はすべて合成数である。

(ii) T(11)＝{3,5,23}は原論文のTable 1、T(55)＝{3,23}はConjecture 5.6直後にも載っている。原論文ではa＝5、m＝11としてt(55)＝t(5)を説明している。同じ55に対してa＝11、m＝5と選べば、D(220)≠D(44)にもかかわらずt(55)＜t(11)となり、一般形を否定する。従ってこれらの数値を新発見とは扱わない。

今回の反例は、元の普遍存在問題、2個以上の予想、Conjecture 1.4、またはa＝3・5に限定した5.6(ii)を否定するものではない。

調査範囲と限界
公開ウェブで「Toda primes 5.6 counterexample」「2511.19744 counterexample」「2511.19744 errata」「Toda primes 29 59」「Toda primes 11 55」「Toda 1770 1711」「Toda 690 7590」「Toda素数 反例」等を検索し、arXiv本文・版履歴・著者サイトの論文を照合した。SUMIRE内ではToda、Tominaga、Bernoulli、4nを検索し、同内容の登録は見つからなかった。同じ反例の先行報告や訂正は今回の検索範囲では発見できなかったが、未索引の記録や未公開の連絡を含めた初出の保証はできない。著者への照会はしていない。

再現条件と検証対象
Lean: leanprover/lean4:v4.30.0
mathlib commit: c5ea00351c28e24afc9f0f84379aa41082b1188f
https://github.com/leanprover-community/mathlib4/tree/c5ea00351c28e24afc9f0f84379aa41082b1188f
以下の二つのソースをそれぞれ示したファイル名で保存し、このmathlibを導入したプロジェクトで lake env lean <ファイル名> を実行する。二ファイルとも2026年9月13日の再実行は終了コード0だった。
最終定理:
TodaDenominatorCounterexample.conjecture_5_6_i_counterexample
TodaCountCounterexample.conjecture_5_6_ii_counterexample
いずれも依存公理はpropext, Classical.choice, Quot.soundのみ。sorry、admit、独自公理、native_decideは使っていない。実際のmathlibのbernoulliとBernoulli.vonStaudt_clausenを使用する。
(i)の定理は分母・最小性・Toda集合の不一致を含む。(ii)の定理は分母の相違・個数の減少を含む。本文で補足したF(690)＝44の最小性は自然言語で証明したもので、(ii)のLean定理には含めていない。

ソース: TodaDenominatorCounterexample.lean
SHA-256: e6df624bb4fb49381a114897774c0bc187859063a955592d7cb437f1e9d64146
----- BEGIN TodaDenominatorCounterexample.lean -----
import Mathlib
namespace TodaDenominatorCounterexample

def Candidate (k p : ℕ) : Prop := Nat.Prime p ∧ p - 1 ∣ k

def Toda (n p : ℕ) : Prop :=
Nat.Prime p ∧ p ≠ 2 ∧ p - 1 ∣ 4*n ∧ ¬ p ∣ n

theorem candidates_6844 (p : ℕ) :
Candidate 6844 p ↔ p = 2 ∨ p = 3 ∨ p = 5 ∨ p = 59 := by
constructor
· intro ht
have hpge := ht.1.two_le
have hd : p - 1 ∣ 4*(2959) := ht.2
obtain ⟨a, r, ha, hr, heq⟩ := exists_dvd_and_dvd_of_dvd_mul hd
obtain ⟨b, c, hb, hc, heq'⟩ := exists_dvd_and_dvd_of_dvd_mul hr
have h29 : b = 1 ∨ b = 29 := (Nat.dvd_prime (by norm_num)).mp hb
have h59 : c = 1 ∨ c = 59 := (Nat.dvd_prime (by norm_num)).mp hc
have ha_le : a ≤ 4 := Nat.le_of_dvd (by norm_num) ha
have h4 : a = 1 ∨ a = 2 ∨ a = 4 := by
interval_cases a <;> norm_num at ha <;> norm_num
have hvalue : p = a(b*c)+1 := by
rw [heq'] at heq
omega
rcases h4 with rfl | rfl | rfl <;>
rcases h29 with rfl | rfl <;>
rcases h59 with rfl | rfl <;>
norm_num at hvalue <;> subst p <;> norm_num [Candidate] at ht <;> norm_num
· rintro (rfl | rfl | rfl | rfl) <;> norm_num [Candidate]

theorem candidates_116 (p : ℕ) :
Candidate 116 p ↔ p = 2 ∨ p = 3 ∨ p = 5 ∨ p = 59 := by
constructor
· intro h
exact (candidates_6844 p).mp ⟨h.1, dvd_trans h.2 (by norm_num)⟩
· rintro (rfl | rfl | rfl | rfl) <;> norm_num [Candidate]

theorem same_candidates (p : ℕ) : Candidate 116 p ↔ Candidate 6844 p := by
rw [candidates_116, candidates_6844]

theorem index_minimal {k : ℕ} (hk : 0 < k)
(hc : ∀ p, Candidate k p ↔ Candidate 116 p) : 116 ≤ k := by
have h4 : 4 ∣ k := ((hc 5).mpr (by norm_num [Candidate])).2
have h58 : 58 ∣ k := ((hc 59).mpr (by norm_num [Candidate])).2
have h116 : 116 ∣ k := by
simpa using Nat.lcm_dvd h4 h58
exact Nat.le_of_dvd hk h116

theorem toda_29 (p : ℕ) : Toda 29 p ↔ p = 3 ∨ p = 5 ∨ p = 59 := by
constructor
· intro h
have hc := (candidates_116 p).mp ⟨h.1, h.2.2.1⟩
rcases hc with rfl | rfl | rfl | rfl <;> norm_num [Toda] at h <;> norm_num
· rintro (rfl | rfl | rfl) <;> norm_num [Toda]

theorem toda_1711 (p : ℕ) : Toda 1711 p ↔ p = 3 ∨ p = 5 := by
constructor
· intro h
have hc := (candidates_6844 p).mp ⟨h.1, h.2.2.1⟩
rcases hc with rfl | rfl | rfl | rfl <;> norm_num [Toda] at h <;> norm_num
· rintro (rfl | rfl) <;> norm_num [Toda]

theorem toda_changes : ¬ (∀ p, Toda 29 p ↔ Toda (29*59) p) := by
intro h
have hx := (h 59).mp (by norm_num [Toda])
norm_num [Toda] at hx

theorem bernoulli_den_116 : (bernoulli 116).den = 1770 := by
have hs : (Finset.range (116+2)).filter (fun p => Nat.Prime p ∧ p-1 ∣ 116) =
({2,3,5,59} : Finset ℕ) := by
ext p
simp only [Finset.mem_filter, Finset.mem_range, Finset.mem_insert, Finset.mem_singleton]
change (p < 116+2 ∧ Candidate 116 p) ↔ _
rw [candidates_116]
omega
have hv := Bernoulli.vonStaudt_clausen 58
change bernoulli 116 + ∑ p ∈ (Finset.range (116+2)).filter
(fun p => Nat.Prime p ∧ p-1 ∣ 116), (1 : ℚ)/p ∈ Set.range Int.cast at hv
rw [hs] at hv
norm_num at hv
obtain ⟨z, hz⟩ := hv
have heq : bernoulli 116 = (z : ℚ) - (1859/1770 : ℚ) := by linarith
rw [heq, Rat.intCast_sub_den]
norm_num

theorem bernoulli_den_6844 : (bernoulli 6844).den = 1770 := by
have hs : (Finset.range (6844+2)).filter (fun p => Nat.Prime p ∧ p-1 ∣ 6844) =
({2,3,5,59} : Finset ℕ) := by
ext p
simp only [Finset.mem_filter, Finset.mem_range, Finset.mem_insert, Finset.mem_singleton]
change (p < 6844+2 ∧ Candidate 6844 p) ↔ _
rw [candidates_6844]
omega
have hv := Bernoulli.vonStaudt_clausen 3422
change bernoulli 6844 + ∑ p ∈ (Finset.range (6844+2)).filter
(fun p => Nat.Prime p ∧ p-1 ∣ 6844), (1 : ℚ)/p ∈ Set.range Int.cast at hv
rw [hs] at hv
norm_num at hv
obtain ⟨z, hz⟩ := hv
have heq : bernoulli 6844 = (z : ℚ) - (1859/1770 : ℚ) := by linarith
rw [heq, Rat.intCast_sub_den]
norm_num

/-- Prime divisors of an even Bernoulli denominator satisfy the predecessor condition. -/
theorem prime_dvd_den_predecessor (k p : ℕ) (hp : Nat.Prime p)
(hd : p ∣ (bernoulli (2k)).den) : p-1 ∣ 2k := by
let S := (Finset.range (2k+2)).filter (fun q => Nat.Prime q ∧ q-1 ∣ 2k)
let Q : ℚ := ∑ q ∈ S, (1 : ℚ)/q
have hv : bernoulli (2k) + Q ∈ Set.range Int.cast := Bernoulli.vonStaudt_clausen k
obtain ⟨z, hz⟩ := hv
have heq : bernoulli (2k) = (z : ℚ) - Q := by linarith
have hdQ : p ∣ Q.den := by simpa only [heq, Rat.intCast_sub_den] using hd
have hprod : p ∣ ∏ q ∈ S, ((1 : ℚ)/q).den :=
dvd_trans hdQ (Finset.Rat.den_sum_dvd_prod_den S (fun q => (1 : ℚ)/q))
obtain ⟨q, hq, hdiv⟩ := (hp.prime.dvd_finsetProd_iff (fun q : ℕ => ((1 : ℚ)/q).den)).mp hprod
have hqprime : Nat.Prime q := (Finset.mem_filter.mp hq).2.1
have hqden : ((1 : ℚ)/q).den = q := by
simpa only [one_div] using Rat.inv_natCast_den_of_pos hqprime.pos
rw [hqden] at hdiv
have heqpq : p = q := (Nat.prime_dvd_prime_iff_eq hp hqprime).mp hdiv
simpa only [heqpq] using (Finset.mem_filter.mp hq).2.2

theorem bernoulli_index_minimal {k : ℕ} (hk : 0 < k)
(hd : (bernoulli (2k)).den = 1770) : 116 ≤ 2k := by
have h4 : 4 ∣ 2k := prime_dvd_den_predecessor k 5 (by norm_num) (by rw [hd]; norm_num)
have h58 : 58 ∣ 2k := prime_dvd_den_predecessor k 59 (by norm_num) (by rw [hd]; norm_num)
have h116 : 116 ∣ 2*k := by simpa using Nat.lcm_dvd h4 h58
exact Nat.le_of_dvd (by omega) h116

/-- The first positive even index with denominator 1770 is 116. -/
theorem first_index_1770 : (bernoulli 116).den = 1770 ∧
∀ k, 0 < k → (bernoulli (2k)).den = 1770 → 116 ≤ 2k :=
⟨bernoulli_den_116, fun _ hk hd => bernoulli_index_minimal hk hd⟩

/-- A fully arithmetic counterexample to the denominator-invariance conjecture. -/
theorem conjecture_5_6_i_counterexample :
(bernoulli (429)).den = 1770 ∧
(∀ k, 0 < k → (bernoulli (2k)).den = 1770 → 429 ≤ 2k) ∧
(bernoulli (4*(2959))).den = (bernoulli (429)).den ∧
¬ (∀ p, Toda (29*59) p ↔ Toda 29 p) := by
refine ⟨bernoulli_den_116, first_index_1770.2, ?, ?⟩
· exact bernoulli_den_6844.trans bernoulli_den_116.symm
· intro h
exact toda_changes (fun p => (h p).symm)

end TodaDenominatorCounterexample
#print axioms TodaDenominatorCounterexample.same_candidates
#print axioms TodaDenominatorCounterexample.index_minimal
#print axioms TodaDenominatorCounterexample.toda_changes

#print axioms TodaDenominatorCounterexample.bernoulli_den_116
#print axioms TodaDenominatorCounterexample.bernoulli_den_6844

#print axioms TodaDenominatorCounterexample.conjecture_5_6_i_counterexample
----- END TodaDenominatorCounterexample.lean -----

ソース: TodaCountCounterexample.lean
SHA-256: c387e3e0fb4ca1735e70dd2793df4848d7ebc61baf0d968a3c5e5e359abdfea8
----- BEGIN TodaCountCounterexample.lean -----
import Mathlib
namespace TodaCountCounterexample

def Candidate (k p : ℕ) : Prop := Nat.Prime p ∧ p-1 ∣ k

def Toda (n p : ℕ) : Prop := Nat.Prime p ∧ p ≠ 2 ∧ p-1 ∣ 4*n ∧ ¬ p ∣ n

theorem candidates_220 (p : ℕ) :
Candidate 220 p ↔ p = 2 ∨ p = 3 ∨ p = 5 ∨ p = 11 ∨ p = 23 := by
constructor
· intro ht
have hpge := ht.1.two_le
have hd : p - 1 ∣ 4*(511) := ht.2
obtain ⟨a, r, ha, hr, heq⟩ := exists_dvd_and_dvd_of_dvd_mul hd
obtain ⟨b, c, hb, hc, heq'⟩ := exists_dvd_and_dvd_of_dvd_mul hr
have h5 : b = 1 ∨ b = 5 := (Nat.dvd_prime (by norm_num)).mp hb
have h11 : c = 1 ∨ c = 11 := (Nat.dvd_prime (by norm_num)).mp hc
have ha_le : a ≤ 4 := Nat.le_of_dvd (by norm_num) ha
have h4 : a = 1 ∨ a = 2 ∨ a = 4 := by
interval_cases a <;> norm_num at ha <;> norm_num
have hvalue : p = a(b*c)+1 := by
rw [heq'] at heq
omega
rcases h4 with rfl | rfl | rfl <;>
rcases h5 with rfl | rfl <;>
rcases h11 with rfl | rfl <;>
norm_num at hvalue <;> subst p <;> norm_num [Candidate] at ht <;> norm_num
· rintro (rfl | rfl | rfl | rfl | rfl) <;> norm_num [Candidate]

theorem candidates_44 (p : ℕ) : Candidate 44 p ↔ p=2 ∨ p=3 ∨ p=5 ∨ p=23 := by
constructor
· intro h
have hc := (candidates_220 p).mp ⟨h.1, dvd_trans h.2 (by norm_num)⟩
rcases hc with rfl | rfl | rfl | rfl | rfl <;> norm_num [Candidate] at h <;> norm_num
· rintro (rfl | rfl | rfl | rfl) <;> norm_num [Candidate]

theorem toda_11 (p : ℕ) : Toda 11 p ↔ p=3 ∨ p=5 ∨ p=23 := by
constructor
· intro h
have hc := (candidates_44 p).mp ⟨h.1, h.2.2.1⟩
rcases hc with rfl | rfl | rfl | rfl <;> norm_num [Toda] at h <;> norm_num
· rintro (rfl | rfl | rfl) <;> norm_num [Toda]

theorem toda_55 (p : ℕ) : Toda 55 p ↔ p=3 ∨ p=23 := by
constructor
· intro h
have hc := (candidates_220 p).mp ⟨h.1, h.2.2.1⟩
rcases hc with rfl | rfl | rfl | rfl | rfl <;> norm_num [Toda] at h <;> norm_num
· rintro (rfl | rfl) <;> norm_num [Toda]

def todaSet (n : ℕ) : Finset ℕ :=
(Finset.range (4n+2)).filter (fun p => Nat.Prime p ∧ p ≠ 2 ∧ p-1 ∣ 4n ∧ ¬ p ∣ n)

theorem todaSet_11 : todaSet 11 = {3,5,23} := by
ext p
simp only [todaSet, Finset.mem_filter, Finset.mem_range, Finset.mem_insert, Finset.mem_singleton]
change (p < 4*11+2 ∧ Toda 11 p) ↔ _
rw [toda_11]
omega

theorem todaSet_55 : todaSet 55 = {3,23} := by
ext p
simp only [todaSet, Finset.mem_filter, Finset.mem_range, Finset.mem_insert, Finset.mem_singleton]
change (p < 4*55+2 ∧ Toda 55 p) ↔ _
rw [toda_55]
omega

theorem count_drop : (todaSet 55).card < (todaSet 11).card := by
rw [todaSet_11,todaSet_55]
norm_num

theorem bernoulli_den_44 : (bernoulli 44).den = 690 := by
have hs : (Finset.range (44+2)).filter (fun p => Nat.Prime p ∧ p-1 ∣ 44) =
({2,3,5,23} : Finset ℕ) := by
ext p
simp only [Finset.mem_filter, Finset.mem_range, Finset.mem_insert, Finset.mem_singleton]
change (p < 44+2 ∧ Candidate 44 p) ↔ _
rw [candidates_44]
omega
have hv := Bernoulli.vonStaudt_clausen 22
change bernoulli 44 + ∑ p ∈ (Finset.range (44+2)).filter
(fun p => Nat.Prime p ∧ p-1 ∣ 44), (1 : ℚ)/p ∈ Set.range Int.cast at hv
rw [hs] at hv
norm_num at hv
obtain ⟨z,hz⟩ := hv
have heq : bernoulli 44 = (z : ℚ) - (743/690 : ℚ) := by linarith
rw [heq,Rat.intCast_sub_den]
norm_num

theorem bernoulli_den_220 : (bernoulli 220).den = 7590 := by
have hs : (Finset.range (220+2)).filter (fun p => Nat.Prime p ∧ p-1 ∣ 220) =
({2,3,5,11,23} : Finset ℕ) := by
ext p
simp only [Finset.mem_filter, Finset.mem_range, Finset.mem_insert, Finset.mem_singleton]
change (p < 220+2 ∧ Candidate 220 p) ↔ _
rw [candidates_220]
omega
have hv := Bernoulli.vonStaudt_clausen 110
change bernoulli 220 + ∑ p ∈ (Finset.range (220+2)).filter
(fun p => Nat.Prime p ∧ p-1 ∣ 220), (1 : ℚ)/p ∈ Set.range Int.cast at hv
rw [hs] at hv
norm_num at hv
obtain ⟨z,hz⟩ := hv
have heq : bernoulli 220 = (z : ℚ) - (8863/7590 : ℚ) := by linarith
rw [heq,Rat.intCast_sub_den]
norm_num

theorem conjecture_5_6_ii_counterexample :
(bernoulli (4*(115))).den ≠ (bernoulli (411)).den ∧
(todaSet (115)).card < (todaSet 11).card := by
refine ⟨?_,count_drop⟩
rw [show 4(115)=220 by norm_num, show 411=44 by norm_num,
bernoulli_den_220,bernoulli_den_44]
norm_num

end TodaCountCounterexample
#print axioms TodaCountCounterexample.conjecture_5_6_ii_counterexample
----- END TodaCountCounterexample.lean -----