2026-10-01 · chapter ヤン–ミルズと質量ギャップ第 10 部 この端末の検討Lean の定理・仮定・既知との対応

Lean で閉じた言明と既存の結果の対応表 — 四十六の定理は何を仮定し、どの既知に当たるか

第 10 部の本文に散らばる Lean の札の定理を一か所に集め、各定理について「何を仮定し、何を言い、既に知られたどの事実に当たるか」を並べます。

表の列は六つです。定理名、仮定（引数に現れる条件。一番大事な列）、言明（結論を本書の記号で）。規約・読みには、記号の読み方のうち表 7 に無いもの、仮定 H に関わる行では 10-03 の八つの読みのどれを仮定するか（冪／帯・$\xi$／$\xi_{\rm RG}$・$\mathcal E_\vartheta$／$\mathcal E_A$）、そして f の量化を書きます。f の量化は、言明が「すべての試験関数 $f$」と「一つの $f$」のどちらについて語るかで、10-03 §03 の H↑・H↓ の区別に当たります。断りの無い行は「なし」（言明に試験関数が現れない）です。対応する既知は第 1〜7 部の章で、既知に当たるものが無い行は「—」とします。種別は次の五つの分類です。

R は文献にある事実を Lean で証明し直したもの、A は記録の定義や仮定を代数で言い換えたもの、C は「未証明の仮定から結論が出る」ことだけを確かめたもの、N は仮定を外すと結論が崩れる反例、M は記録の側の定理で、探した範囲で先行の記録が見当たらないものです。C の行の中身は仮定の側にあり、定理はその仮定を一歩も証明しません。

表に載せるのは、各章が結論として引く言明です。同じ言明の部品（補題・道具の不等式・数え上げ）は表に入れず、次の一覧に名前だけ置きます。どれも宣言と検査の記録を確かめました。10-02 の S4_fails_const・step_lowers_coupling・Chain.b_of_beta、10-09 の ratio_rg_invariant、10-05 の gap_ge_of_overlap・meff_var_ge・sqQuotient_isGreatest・sqQuotient_between・orbitAvg_continuous・sum_sub_eq_card_mul・periodic_violates_bound（周期的な箱では (3) の下界が外れる反例）、10-06 の rayleigh_le_tau、5-11 の star_S・star_S_sharp（定数 18 が達成される配位）・second_deriv_le・star_count・turan_series。本文の札のうち、この章で突き合わせた原稿の中に宣言が見当たらない名前は載せていません。

例。hup_is_gap_positivity は「$C_P=1/m^2$ かつ $C_P\le K\xi^2$ なら $1\le K(m\xi)^2$」です。両辺に $m^2$ を掛けるだけの代数なので種別は A、$C_P$ が上限であること（すべての $f$ を動かすこと）は Lean の外にあるので、f の量化は「なし」です。

定理の引数の型を見ると、その文が実際に何について語っているかが機械的に分かります。この端末で、表に載せた四十六の定理の宣言を読み、引数の型で五つの層に分けました。

左ほど語る対象が素朴で、右ほど物理の対象に近い、という順です。正確には包含関係ではなく、「定理の文を理解するのに要る構造の量」の目安です。

表 1　四十六の定理を、言明が直接に語る対象の型で分ける 計算

仮定の本数は、型が命題である引数（等式・不等式・$\forall$ の文・Tendsto など）を数えたもの。群の元や関数のような対象の引数は数えない。四十六の定理すべてについて、この端末に残る検査の記録（原稿より新しい）の #print axioms の行が標準の三つの公理の部分集合で、sorryAx を含まないことを読み直した。表 1 は定理の数で、表 2〜6 と図は行の数（対にした二つの定理は一行）で数える。

読み方。ちょうど半分の 23 個は、実数の不等式か恒等式です。hup_is_gap_positivity の $C_P$ も、chain_band の $\lambda_1$ も、Lean の中では名前の付いたただの実数です。それが「Wilson 測度の Poincaré 定数」であることは、本文が付けた読みで、Lean は検査していません。格子のゲージ場を型として持つのは 5-11 の三つで、Wilson の重み $e^{-S_W}$ が現れるのも一部のリンクを積分する恒等式 integral_star_links だけです。Wilson 測度の期待値・相関・隙間についての定理はありません。

例。図 1 で一行ずつ選ぶと、その定理が左の層から、中の種別を通り、右の章（読まれる場所）へ渡る線が太く出ます。灰色の線は四十一行すべての流れです。

計算この図の数値はこの端末で計算した（宣言の型と仮定の数は宣言を読む小さなスクリプト、種別と章は表 2〜6 の列）。行で数える（対にした二つの定理は一行）。JavaScript が無効なら表 1 と表 8 が中身です。

寄り道：#print axioms に出る三つの公理

10-02 の一段の記帳は、格子を $b$ 倍に粗くする一段で結合 $\beta$ がどう下がるかを数える枠組みでした。定理は、一リンク積分の評価・格子の組合せの数え上げ・段の誤差の代数の三種です。中心の式は、段ごとの関数等式とその帰結です。

計算$3\pi^2/11=2.691710\ldots$。xi_eq_exp は (1) の矢印で、連続性も単調性も仮定しません。Lean の中身は関数方程式から指数関数を出す代数で、物理の内容は仮定の関数等式（一ループの走りを厳密な等式として置いたもの）に入っています。$\kappa$ は一ループ係数を $\beta=4/g^2$ に書き直した値です（4-06）。漸近スケーリング（5-05）は摂動論の水準の事実で、二ループの冪の補正を持ち、厳密な定理ではありません 物理。だから種別は A です。

表 2　一段の記帳（10-02）の定理

例。c2_ge_of_nonneg_weights の「$c_2$ は $S$ の増加するアフィン関数」は、記録が一ループ核の族で測った依り方です。定理はそれを前提に置いた一行の不等式で、「正値な核では $c_2\gt0$」を無条件に示してはいません。同じく S4_two_sided は段の誤差を加法的で有界とする模型の中の代数で、その模型が格子ヤン–ミルズの一段を表すことは仮定です（10-01）。

10-03 の仮定 H は、$C_P$ が $\xi^2$ と同じ冪で伸びるという冪の文で、記録が鎖と組み合わせて使うのは帯の文 (3)＝$\text{H}_{\rm band}[\mathcal E_\vartheta]$ と鎖 (ii)(iii) でした。この節の定理は主に後者を扱います。Lean の中での姿を一つ見ます。

theorem hup_is_gap_positivity {CP xi mlat K : ℝ}
    (hmlat : 0 < mlat) (hCP : CP = 1 / mlat ^ 2) (h : CP ≤ K * xi ^ 2) :
    1 ≤ K * (mlat * xi) ^ 2

四つの文字はすべて実数です。hCP の等式が、鎖 (i)（Langevin の隙間と質量の二乗が等しい）を一点で仮定しています。本文の式で書けば

で、$C_P=1/m^2$ は自由場で場 $A$ の正規化のときの値です（§08）。対になる hdown_is_mass_finiteness は不等号の向きを逆にした H↓ の読み替え $c(m\xi)^2\le1$ です。

表 3　仮定 H のまわり（10-03）の定理

例。conditional_scale_bound は仮定が十一本で、四十六の中で最も多い定理です。その一本 hproj が射影 (P)、すなわち「Hardy 不等式を満たす定数はどれも $C_P$ の上界を与える」という文で、すべての $f$ を動かす量化子は、この仮定の中に入っています。結論の有界性は、二重み Hardy 不等式の挟み込み（Muckenhoupt 1972、1-10）の再証明と、取りこぼしの部分和の評価を合わせたものです。中身が (P) の側にあることは 10-06 §07 で見ました。

10-05 の方向 12〜14 は、試験関数や試しの演算子から隙間を読む道でした。多くは変分原理の言い換えで、R が五つです。基本の形は非負の重みの相関の表示です。

(3) の下で $m_{\rm eff}$ は単調に減り（meff_antitone）、すべての $\rho_n\le R$ なら $m_{\rm eff}(k)\ge-\ln R$ です（meff_ge_of_corr）。前者は「平坦部には上から近づく」という格子分光の標準の事実、後者は Rayleigh–Ritz の原理です（1-10 §06・5-08）。

表 4　試験関数と分光（10-05）の定理

例。light_admixture_invisible は二準位 $\rho=(1/2,\,9/10)$、重み $(1,\varepsilon)$ の具体例で、軽い方の準位を足しても相関は $\varepsilon$ しか変わりません。有限個の測定から隙間の下界が出ないことの最小の例です（4-11 §04 の言い換え、種別 N）。規約・読みの列に「一つの演算子」とある行は、どれも H↓ の側（ある $f$）にしか届きません。

10-06 の方向 15 は、閉じ込めの管の重さに $c/\ell$ の欠損があれば質量の下界が出る、という道でした。七つのうち三つが陰性対照です。中心の還元は相加相乗平均です。

mass_sq_ge_of_tube は (4) を転送作用素のノルム $t\le e^{-2\sqrt{c\sigma}}$ の形で仮定し、$m=-\ln t$ について結論します。仮定の中身は $T(c,1)$ で、その証明の型は在りません。

表 5　管（10-06）の定理

例。三つの陰性対照が示すことは、それぞれ違います。casimir_only_no_bound は、短い管の欠損の仮定を外せないこと（Casimir の床 $-\kappa/\ell$ だけでは $\ell\to0$ で負）を示します。linear_deficit_breaks_inv は、欠損を異方性を引いた後の形で置かねばならないこと（生の周長では欠損の仮定そのものが偽）を示します。linear_regime_breaks_onescale は、強結合の収束域では一尺度の下半分そのものが偽であることを示す、別の原稿の定理です。つなぎ目の仮定が要るかどうかは、Lean では確かめていません。

表 1 の右端の層、格子のゲージ場を型として持つ定理は 5-11 の三つです。$SU(2)$ の元は単位四元数 $u$、Haar 測度は $S^3$ の上の一様な確率です。一リンク積分は

で（$I_1$ は変形 Bessel 関数）、IsHaarS3.one_link は Haar の性質だけからこれを示します。式は熱浴法の標準の式で、種別は R です。

どのプラケットにもちょうど一本ずつ含まれるリンクの族（完全な族）を先に積分すると、残りのリンクの周辺密度は $e^{-\Phi}$ になります。この $\Phi$ を有効作用と呼びます。integral_star_links はこの積分の恒等式で、一本ずつは (5) です。

表 6　一リンクと完全な族（5-11・10-02・10-13）の定理

例。hess_gauge の仮定は「周期 $L$ が偶数で $L\ge3$」「リンクは単位四元数」「摂動は純虚」の三種で、$\beta$ の小ささは仮定しません。全ての配位で $\Phi$ の Hesse 形式が $-27\beta^2$ 以上という言明です。これを $S^3$ の Ricci 曲率 2 既知 と合わせて Bakry–Émery の判定法 既知 に入れると、残りのリンクの周辺測度の曲率は $2-27\beta^2$ 以上で、閾値 $\beta\lt\sqrt{2/27}=0.2722$ 計算 が出ます。判定法から質量ギャップへ進む段は紙の概略で、Lean の定理ではありません（5-11）。no_perfectZ_of_five は $d\ge5$ の $\mathbb Z^d$ に辺の完全な族が無いという組合せの定理です。周期の箱では perfectK_one_iff が「$d\le4$ かつ $L$ が偶数」と同値を与えます。この 4 は物理の四次元時空とは関係しない一致です（10-10 §09）。

Lean の定理は記号の意味を知らず、同じ文字が別のファイルで別の量を指しても検査は通ります。定理の中の規約を本書の記号表（付録 A-01）に翻訳し、食い違いは食い違いとして書きます。

一番影響の大きいのは $C_P$ の正規化です。Dirichlet 形は $\mathcal E(f)=E|\nabla f|^2$ で、$C_P$ は $\operatorname{Var}f\le C_P\,\mathcal E(f)$ を満たす最小の定数でした（1-10）。記録はリンクを $U=e^{i\vartheta\cdot\sigma}$ と角度 $\vartheta$ で書き、場を $A=\sqrt\beta\,\vartheta$ とします。$\mathcal E$ を $c$ 倍すると $C_P$ は $1/c$ 倍なので

です（8-05）。例：$\beta=2.5$（$g^2=1.6$）では二つの正規化の比は 0.4、$\beta=10$ では 0.1 で 計算、比は $\beta$ とともに 0 に向かいます。hup_is_gap_positivity の仮定 $C_P=1/m^2$ は $A$ の正規化の値なので、角度の正規化で読むとこの仮定は自由場でも $g^2/4$ 倍ずれます。

表 7　Lean の中の規約と本書の記号

例。drain_exponent のファイルの注は $\eta$ を「零運動量の重なり $Z\asymp\xi^{1-\eta}$ の冪、したがって $C_P\asymp\xi^{2-\eta}$」と書きます。本書は $C_P/\xi^2\propto\xi^{-\eta_{\rm dyn}}$ で $\eta_{\rm dyn}$ を定義するので、注の $\eta$ は $C_P$ の冪としては $\eta_{\rm dyn}$ と同じ量を指します。注はそれを重なりの冪から導いており、その重なりの冪が静的な $\eta_s$ と一致するかが Lean の外の問いです（8-03）。定理そのものは $\eta$ に何の意味も要求しないので、どちらの読みでも成り立ちます。

四十一行を五つの種別で数えると、表 8 になります。既知の再証明と記録の整理で二十六行、全体の六割を超えます。条件つきの還元の七行は、どれも未証明の仮定（模型・測定・$T(c,1)$・(P)・感受率の有界性・自己相関の時間の下界）を引数に持ちます。

表 8　種別と、読まれる章（行で数える） 計算

計算この図の数値はこの端末で計算した（表 8 と、型の層の章ごとの行数）。表 1 は定理で数えるので、層ごとの数は表 1 と少し違う。JavaScript が無効なら表 8 と表 1 が中身です。

既知の結果と比べて記録の側に定理として残るのは、M の三行です。C の行は仮定つきの組み立てで、その中身は仮定の側にあります。hess_gauge から出る閾値 $\sqrt{2/27}$ は、完全な族を積分した後に残るリンクの周辺測度の曲率で見たものです。それが Shen–Zhu–Zhu の Wilson 測度そのものの閾値（同じ規約で $1/12$）の $4\sqrt{2/3}\approx3.27$ 倍 計算 になります。比べている二つの測度は同じではありません。別の組み立てとして、Cao–Nissim–Sheffield（2025）は模型を頂点の上のスピン系として扱って Bakry–Émery を当て、Shen–Zhu–Zhu の閾値の 2 倍を得ています 既知。このサイトの論文（5-11）は、探した範囲で同じ組み立ては見当たらないとしつつ、強結合の範囲を広げたとは主張していません（5-11）。完全な族が $d\le4$ に限ることは、探した範囲で先行の記録が見当たらない組合せの事実で、既知かもしれません。どちらも連続極限からは反対側の、相関長が格子間隔の数倍の世界の話です。

例。図 2 を「対象の型で分ける」に切り替えると、10-03 と 10-06 の帯は実数と数列の層だけでほぼ埋まります。機械検査が届いているのは仮定を置いたあとの代数の部分で、残るのは仮定を格子ヤン–ミルズの測度について証明する部分です。何が足りないかは 10-08 壁の一覧 と 10-11 で扱います。数値の側のつじつま合わせは 10-12 です。

この章が言えている範囲

出典と再現

次に読む章：10-08 壁の一覧 — 仮定の側に何が残っているか。

← 10-06 方向 15・15′目次10-08 壁の一覧 →