論文
論文の草稿を置く場所です。記事とは体裁を分けてあります。原本は英語で、この頁には日本語の要約を置いています。各論文の先頭に、その論文がどの問題を扱っていて、どこを見れば問題の全体が分かるかの短い案内を添えました。要約そのものは専門の言葉で書かれているので、案内だけ読んでいただいても構いません。
札は四つ。Lean機械検査済み（sorry なし・native_decide なし・標準三公理のみ）
紙証明はあるが機械検査は未了
計算この端末で確かめた範囲
既知既知の定理・言い換え。一本ごとに「何を言い、何を言っていないか」を一行添えています。
日本語 — 五本の要約
SU(2) 格子ヤン–ミルズ — Bakry–Émery の前に一リンク積分を済ませる
この論文が扱う問題。クレイ数学研究所が掲げるミレニアム懸賞問題の一つに「ヤン–ミルズ理論と質量ギャップ」があります（クレイ数学研究所の問題の頁）。素粒子の間に働く力を記述するヤン–ミルズ理論を数学的に厳密に構成し、最も軽い粒子の質量が正であること（質量ギャップ）を示せ、という問題です。この論文はその本体には触れません。空間を碁盤の目のような格子で置き換えた「格子ゲージ理論」という有限の模型の中で、Bakry–Émery と呼ばれる既存の方法に現れる一つの定数を改善したもので、言えるのはその範囲だけです。
格子 (Z/L)⁴ 上の SU(2) ウィルソン作用で、どのプラケット（格子の最小の正方形）もちょうど一本だけ含む「完全な族」 I* のリンク（格子の辺）を先に厳密に積分してしまう。I* のリンクはプラケットを共有しないのでハール積分は「星」ごとに分かれ、残りのリンクの周辺密度は exp(−Φ)、Φ = −Σ log F₀(β²‖M‖²/4) の形になる。この Φ について、測地線 U ↦ U e^{τX} に沿う二階微分が −27β² Σ‖X‖² 以上であることを示した（全ての β・全ての配位で成立）。単位 S³ の Ric = 2 と合わせて Bakry–Émery 曲率 2 − 27β²、閾値 β < √(2/27) = 0.2722 になる（先行する数え上げによる 1/12 = 0.0833 と比べる）。ウィルソン作用から Φ の下界までの鎖は Lean 4 で閉じている。そこから対数ソボレフ不等式と質量ギャップに至る段は形式化しておらず、紙で、しかも概略である。付随してもう一つ：完全な族が Z^d に存在するのは d ≤ 4 のときに限る（単位立方体に制限すると長さ d−1・大きさ 2^{d−3}・最小距離 3 の二元符号になり、ハミング限界が d ≤ 4 を与える）。周期込みの形、k-胞体版（密度はちょうど 1/(2(k+1))・d ≤ 3k+1）、d ≥ 5 での詰め込み密度 ≤ 1/d も機械検査済み。定数 27 は 21 までしか改善できない（厳密演算で確かめた配位がある）。
Leanヘッセ行列の下界と完全な族の組合せ論 紙質量ギャップ・対数ソボレフ・一意性（概略） 計算探索と数値
何を言い、何を言っていないか。言っているのは「Bakry–Émery の方法の中で定数倍ぶん良くなる」ことだけである。連続極限については何も言っていない。クレイのミレニアム問題（ヤン–ミルズの存在と質量ギャップ）を解いたとは言っていない。質量ギャップ自体は Lean の定理ではない。
PDF ym-onelink-bakry-emery.pdf · LaTeX 源 ym-onelink-bakry-emery.tex · Lean LatticeGaugeOneLink.lean（StarInequality・StapleCurve・OneLinkSeries・CompleteFamilyLattice・StaplePerturbation・WilsonOneLink）、PerfectFamily*.lean、PlaquetteCounting.lean。主な定理は WilsonOneLink.SW_eq・IsHaarS3.one_link・StaplePerturbation.hess_gauge・PerfectFamily.no_perfectZ_of_five・PlaquetteCounting.perfect_torus_d_le_four。公理ログは同じ名前の axioms-*.txt（sorry 0・native_decide 不使用・propext／Classical.choice／Quot.sound のみ）（機械検査の一覧）
異常素点での p 進高さ対の p 整性は、E(Q_p) の位数 p の点と同値
この論文が扱う問題。楕円曲線とは y² = x³ + ax + b の形の式で定まる曲線で、その上に有理数の座標を持つ点がどれだけあるかは整数論の中心的な問いです。ミレニアム懸賞問題「バーチ・スウィンナートン=ダイヤー予想」（クレイ数学研究所の問題の頁）は、その点の多さ（階数）が L 関数という解析的な量から読み取れる、と予想するものです。この論文は予想そのものには触れません。予想の周辺に現れる「p 進レギュレーター」という量が、ある特別な素数 p（異常素点）でどれだけ分母を持ちうるかを調べたものです。
E/Q を楕円曲線、p ≥ 5 を良順序還元の素点、Reg_p を円分 p 進レギュレーターとする。p が異常（p ∣ #E(F_p)）のとき Reg_p は p 整とは限らず、指数を数えるだけで v_p(Reg_p) ≥ r − 2 が出る（定理 A。これは既知で、ここの寄与ではない）。この草稿が足すのは、その欠損を支配する局所的な仕組みである：#E(F_p) = p で Λ = E(Q)/tors が E(F_p) に全射するとき、高さ行列の成分が全て Z_p に入ること ⟺ E(Q_p)[p] ≠ 0（分裂）。階数 1 では v_p(Reg_p) ≥ 0 ⟺ 分裂で、非分裂のときの値はちょうど −1。証明は局所的で、p 分多項式 φ_p の Fermat 商 λ ∈ F_p 一つを通る。分裂なら Vélu の分解が λ を消し（定理 C・系 D）、逆に λ = 0 は分裂を強いる（命題 6。これは既知の判定条件で、ここでは重み付き斉次性のオイラー恒等式と尖点での留数計算による独立の証明を与えた）。CM 曲線は良還元の異常素点で常に分裂する（定理 F）。算術の段は Lean 4 の定理で、幾何の入力は仮定として入る。
紙全体の骨組み Lean算術の段（高さの分解・Fermat 商・線形代数・重みと留数の勘定） 既知基準（定理 A）と局所判定（命題 6） 計算§5 の PARI/GP
何を言い、何を言っていないか。BSD 予想には何も及ばない。Ш（テイト–シャファレヴィッチ群）・L 関数・階数についても何も言っていない。主張は全て「一つの素点での還元に仮定を置いたときの、p 進レギュレーターの付値」についてである。階数 2 以上では下界であって、分裂の場合の値は予測しない。
PDF padic-regulator-valuation.pdf · LaTeX 源 padic-regulator-valuation.tex · Lean PadicHeightValuation4–8.lean（主定理の線形代数の段は regulator_valuation_of_split_anomalous、同値は regulator_valuation_of_split_anomalous_iff_split、判定は lambda_eq_zero_iff_split）。公理ログは axioms-PadicHeightValuation4–8.txt。対応表は論文 §6 と statements-and-dependencies.md（機械検査の一覧）
一般化ペテルセングラフ GP(n,3) のハミルトン閉路の個数は、n が奇数なら n で割り切れる
この論文が扱う問題。一般化ピーターセングラフ GP(n,k) は、外側の n 角形と、内側の n 点を k 個おきに結んだ星形とを、対応する頂点どうし n 本の辺でつないだグラフです（Wikipedia: Generalized Petersen graph）。ハミルトン閉路とは、グラフの全ての頂点をちょうど一回ずつ通って出発点に戻る道のことです。この論文は、k = 3 の場合のハミルトン閉路の本数について、n が奇数なら n で割り切れるという性質を証明したものです。本数そのものはすでに知られています。
GP(n,k) を頂点 O_a・I_a（a ∈ Z/n）、辺 O_aO_{a+1}・I_aI_{a+k}・O_aI_a の三価グラフ（各頂点から辺が 3 本）とし、#HC(GP(n,3)) をそのハミルトン閉路の個数（辺集合として数える）とする。7 以上の奇数 n について n ∣ #HC(GP(n,3))。より強く、非自明な回転 ρ^i（0 < i < n）で不変なハミルトン閉路は存在しない——すなわち Z/n = ⟨ρ⟩ が閉路の集合に自由に作用する。証明は初等的で、向き付き閉路の保存則、商の長さが奇数のとき巻き数が {0, ±2} に押し込められること、2 が Z/d で可逆なときだけ存在する「欠けた辺のブロック構造」、置換の符号による障害、の四つからなる。全体が Lean 4 と Mathlib で閉じており、一般の n の証明に核計算（Lean の核に直接走らせる計算）は入っていない。偶数の n では主張は成り立たず（n = 8, …, 38）、回転で不変な閉路が実在する。n = 7, …, 15 の値 7, 9, 11, 26, 75 は核計算で別に検査した。値そのものは既知（Haugland が線形漸化式を与えている）。
Lean主定理（gp3_dvd_hc_odd）と n = 7…15 の値 計算n ≤ 23 の全列挙と既知の表との一致 既知個数そのもの
何を言い、何を言っていないか。形式化されているのは主定理と五つの値だけである。既知かどうかは「探した範囲で見当たらない」までにとどめる。書誌のうち一次資料を読めていないものは論文の中で明示している。
PDF gp3-hamiltonian-count.pdf · LaTeX 源 gp3-hamiltonian-count.tex · Lean GeneralizedPetersenBase / Blocks / Count / Descent / Small / FreeAction.lean（計 6,947 行）と ChkGeneralizedPetersen.lean。主定理は GeneralizedPetersen.Descent.gp3_dvd_hc_odd。公理ログは axioms-GeneralizedPetersen*.txt（機械検査の一覧）
周長欠損 2 の三価二部グラフの最小位数は 30
この論文が扱う問題。3 正則（三価）グラフとは、どの頂点からもちょうど 3 本の辺が出ているグラフです。二部グラフとは、頂点を二つの組に分けて、どの辺も組をまたぐようにできるグラフです。グラフの中で最も長い閉路の長さを周長と呼び、それが頂点数にどれだけ届かないかが周長欠損です。欠損 0 は「全ての頂点を一周する閉路がある」（ハミルトン閉路を持つ）ことにあたります。この論文は、欠損がちょうど 2 の連結な 3 正則二部グラフは最小で何頂点か、という問いに 30 と答えたものです。
連結・三価・二部のグラフ G について def(G) := |V(G)| − circ(G)（頂点数から最長の閉路の長さを引いたもの。周長欠損）を考える。三価二部では def は偶数なので、非ハミルトン性の最小の破れ方は def = 2 である。def = 2 の連結三価二部グラフの最小位数は 30 で、30 頂点の例は（x ~ y の場合に）ちょうど三つである。三つのグラフ G_I・G_II・G_III が三価・二部・連結で、長さ 28 の閉路を持ち、どの閉路も長さ 28 以下であること（＝非ハミルトンかつ circ = n − 2）は Lean 4 で閉じている（探索の完全性を歩道の構造帰納法で証明し、探索木を核で回した）。n ≤ 28 に例が無いことと 30 頂点での分類は全数計算で、これは形式化していない。独立な第二の道（2-辺切断による分解）でも n ≥ 30 を確かめた。
Lean定理 A（30 頂点の三つの例） 計算定理 B（n ≤ 28 に無い・30 での分類）と不変量 既知周辺の最小性（3-連結 50・平面 26）
何を言い、何を言っていないか。定理 B は形式化していない。三類の個数は x ≁ y 側の 4 葉の同型判定をしていない。既知かどうかは、探した範囲で見当たらない、までにとどめる。
PDF def2-cubic-bipartite.pdf · LaTeX 源 def2-cubic-bipartite.tex · Lean CubicBipartiteGap2.lean（1,385 行）と ChkCubicBipartite.lean。定理は CubicBipartite.ClassI.G30_def2・CubicBipartite.Search.G30b_def2・CubicBipartite.Search.G30c_def2。公理ログは axioms-CubicBipartiteGap2.txt（機械検査の一覧）
エルデシュ #827：n₄ = 7 の機械検査された証明
この論文が扱う問題。エルデシュ問題集（erdosproblems.com）は、数学者ポール・エルデシュが残した問題を番号付きで集めた Web サイトで、この論文が扱うのはその問題 827 です（erdosproblems.com/827）。平面上に点を置いたとき、「四つの三角形の外接半径（三点を通る円の半径）がすべて異なる 4 点」を必ず含むには最低で何点あればよいか、その最小の点数 n₄ を求める問題で、答えは n₄ = 7 で、この問題は 2026-09-22 に同じサイトのフォーラムで既に解かれています。この論文はその後追いで、別の道による証明を鎖の全体まで Lean の検査にかけた、独立な検証の形です。先行記録の側も、他の人による検証を求めていました。
nk を、一般の位置（相異なる・3 点非共線・4 点非共円）の N 点が必ず「C(k,3) 個の三点組の外接半径が全て相異なる k 点」を含むような最小の N とする（エルデシュ #827）。n₄ = 7 の証明を Lean 4 で組み、機械検査を通した。下界は六点 {±(1,0), ±(1,1), ±(2,3)}——十五個ある四点部分集合のどれにも、外接半径の等しい二つの三角形がある。上界は 6 点の証人構造の全数分類による。四点 {u,v,c,d} と共有辺 u v を枡と呼ぶと 6 点には枡が 90 個あり、二つの三角形の外接半径が一致する枡を証人と呼ぶ。どの四点部分集合にも証人がある配置を悪い配置と呼ぶ。悪い 6 点の証人集合は、点の付け替えを除いてちょうど 35 類（204,890 節点の探索を、1,820 本の部分木定理として Lean の核が回した）で、そのうち 34 類は一般の位置では実現せず、残る一類は六点が八面体型（三対の八つの横断三角形が一つの外接半径を共有する）であることを強いる。八面体型の 6 点は一点について対称で、7 点の六点部分集合が全部そうなることはできない——ゆえに n₄ ≤ 7。鎖の全体が Lean 4 の一本の言明 sInf {N | IsGood N} = 7 で、仮定は無く、sorry も native_decide も無く、公理は標準の三つだけである。先行記録（2026-09-22、問題のフォーラム）の証明は SAT と Singular 上の飽和によるもので、本稿の道とは別である。
Lean下界・上界・35 類の全数性・34 類の非実現・繋ぎ（鎖の全体） 計算証書の探索・枝の数・実測 既知n₄ ≤ 9（Martínez–Roldán-Pensado）・n₄ = 7 の値の先行記録
何を言い、何を言っていないか。言っているのは k = 4・平面のただ一つの値である。k ≥ 5 と漸近については何も言っていない。値は一般の位置の規約に依存する（4 点非共円を外すと 7 ≤ n₄ ≤ 9 までしか出ない）。census は機械の計算であって人が読み通せる形ではない。先行記録の計算は検査していない。
PDF erdos827-distinct-circumradii.pdf · LaTeX 源 erdos827-distinct-circumradii.tex · Lean 配布物 principia-src.tar.gz の Principia.DistinctCircumradii.* 100 本（土台 Basic、探索木 Census.Tree301〜Tree373 の 73 本、Census.Statement / SixPoints / SevenPoints、非実現の部品 22 本、Final）。主定理は DistinctCircumradii.sInf_isGood_eq_seven、二本の柱は censusComplete と restUnrealizable。公理ログは axioms-principia.txt。対応表は論文 §8.2（機械検査の一覧）
article ＋ amsmath・amsthm・amssymb・longtable・hyperref）から作っています。各論文の LaTeX 源は上の行から辿れます。