computo ergo sum

2026-10-09 · chapter ヤン–ミルズと質量ギャップ第 10 部 質量ギャップの証明へ向けて — 階段の一段目を組むLean・#print axioms・言明の符号化 · Kiichi, Shiori and Rin

この本の全体　目次と読む順
  1. 第 0 部 入口 — この本の読み方
  2. 0-01 この本の読み方
  3. 0-02 一枚の絵
  4. 0-03 問題文を一語ずつ読む
  5. 0-04 数学の四次元と物理の四次元
  6. 第 1 部 数学の準備
  7. 1-01 ベクトル空間と線形写像
  8. 1-02 群とは何か
  9. 1-03 リー群とリー環
  10. 1-04 SU(2) と SU(3)
  11. 1-05 多様体と接空間
  12. 1-06 微分形式と外微分
  13. 1-07 ベクトル束と接続
  14. 1-08 確率と測度
  15. 1-09 無限次元の確率
  16. 1-10 ヒルベルト空間と自己共役作用素
  17. 1-11 フーリエ解析と分布
  18. 1-12 寄り道：四次元でだけ起きること
  19. 第 2 部 物理の準備
  20. 2-01 ラグランジアンと作用
  21. 2-02 場という考え
  22. 2-03 電磁気学はゲージ理論である
  23. 2-04 特殊相対論と時空
  24. 2-05 量子力学の骨
  25. 2-06 調和振動子と生成消滅
  26. 2-07 経路積分の考え方
  27. 2-08 統計力学と相転移
  28. 2-09 寄り道：イジング模型で見るギャップと相関長
  29. 2-10 緩和の時間と動的指数 z
  30. 第 3 部 ヤン–ミルズ理論（古典）
  31. 3-01 ゲージ原理
  32. 3-02 非可換ゲージ場
  33. 3-03 作用と方程式
  34. 3-04 幾何としてのゲージ理論
  35. 3-05 インスタントンと位相
  36. 3-06 寄り道：Donaldson とエキゾチック R⁴
  37. 3-07 標準模型の中のヤン–ミルズ
  38. 第 4 部 量子化
  39. 4-01 正準量子化とハミルトニアン
  40. 4-02 経路積分とユークリッド化
  41. 4-03 摂動論と Feynman ダイアグラム
  42. 4-04 発散と繰り込み
  43. 4-05 発散の代数
  44. 4-06 漸近自由
  45. 4-07 次元転移と Λ
  46. 4-08 ゲージ固定と Faddeev–Popov
  47. 4-09 場の量子論の公理
  48. 4-10 Osterwalder–Schrader の公理と再構成
  49. 4-11 質量ギャップの定義
  50. 4-12 寄り道：摂動級数は発散する
  51. 第 5 部 格子ゲージ理論
  52. 5-01 Wilson の格子
  53. 5-02 強結合展開
  54. 5-03 反射正値性と転送行列
  55. 5-04 無限体積極限とクラスター展開
  56. 5-05 弱結合と連続極限
  57. 5-06 U(1) と非可換の違い
  58. 5-07 モンテカルロ法
  59. 5-08 グルーボールと弦張力の測定
  60. 5-09 何を固定して極限を取るか
  61. 5-10 有限群の格子ゲージ理論
  62. 5-11 寄り道：Bakry–Émery と一リンク積分
  63. 第 6 部 構成的場の理論
  64. 6-01 構成的場の理論とは
  65. 6-02 二次元の可解性とヤン–ミルズ測度
  66. 6-03 スカラー場の構成
  67. 6-04 クラスター展開
  68. 6-05 繰り込み群の段の列
  69. 6-06 三次元ヤン–ミルズの紫外安定性
  70. 6-07 四次元
  71. 6-08 四次元の φ⁴ の自明性
  72. 6-09 確率量子化と正則性構造
  73. 6-10 四次元で止まる場所
  74. 6-11 発散以外の障害
  75. 6-12 寄り道：「1/0 に記号を与えれば」
  76. 第 7 部 物理の側から
  77. 7-01 物理はどう見ているか
  78. 7-02 閉じ込めの機構
  79. 7-03 弦の絵
  80. 7-04 大 N
  81. 7-05 ひも理論と余剰次元
  82. 7-06 余剰次元が見えなくなる仕組み
  83. 7-07 ゲージ場はどこから来るか
  84. 7-08 ホログラフィー
  85. 7-09 質量ギャップが幾何になる
  86. 7-10 四次元に戻す
  87. 7-11 超対称と Seiberg–Witten
  88. 7-12 等価原理に当たる一文
  89. 7-13 物理の掘り方が数学と離れる場所
  90. 第 8 部 二つの言葉の辞書 — 物理の視点と数学の視点
  91. 8-01 辞書の読み方
  92. 8-02 辞書 A
  93. 8-03 辞書 B
  94. 8-04 辞書 C
  95. 8-05 私たちの仮定の物理側の対応
  96. 第 9 部 現在地と課題
  97. 9-01 世界はどこまで来ているか
  98. 9-02 二つの掘り方の切れ目
  99. 9-03 新しい概念の候補
  100. 9-04 課題の一覧
  101. 9-05 よくある誤解
  102. 第 10 部 質量ギャップの証明へ向けて — 階段の一段目を組む
  103. 10-00 入口 — 階段と、酔歩・物差し・時計
  104. 10-01 構成の筋と仮定 H
  105. 10-02 四次元格子で試した道と壁
  106. 10-03 階段の四段 — なぜ 0+1 次元から始めるか
  107. 10-04 二重井戸の経路の測度とキンク
  108. 10-05 一段目の言明 — 四条件と命題 4.5
  109. 10-06 (H1) 相の中の局所 Poincaré
  110. 10-07 (H2) の地図 — 七つの道筋と環の継ぎ目
  111. 10-08 計算機援用とは何か — 窓の中の鎖の条件
  112. 10-09 区画の枠組みと道筋 5 の三本の筋
  113. 10-10 迂回策の一覧 — 壊れ方の型
  114. 10-11 (H3)(H4) と芯の定数
  115. 10-12 統合表と依存グラフ
  116. 10-13 Lean の言明と機械検査の限界
  117. 10-14 突き合わせ — 記録の数と既知の数
  118. 10-15 残件と費用 — 定理までの距離
  119. 10-16 主張しないこと
  120. 10-17 ひらめきと小さな問い
  121. 第 11 部 今後の考察 — 仮定 H の先と、別の見方
  122. 11-00 今後の考察 — 入口
  123. 11-01 H を妨げる一つの形 — ほぼ保存される大域の量
  124. 11-02 物差しと座標を選び直す — 保存が壊れる長さ
  125. 11-03 区画の H と局所の H
  126. 11-04 片側の橋はどの H を要るか
  127. 11-05 時間を連続にする — Hamiltonian 格子と真空の測度
  128. 11-06 凸性の代わりに稀さで払う — 群の上の繰り込みと対数 Sobolev
  129. 11-07 四次元だからこそ — 無次元の結合と位相
  130. 11-08 問いと、主張しないこと
  131. 11-A1 第 11 部の記号の対応表
  132. 付録
  133. A-01 記号表
  134. A-02 用語集
  135. A-03 文献案内
  136. A-04 Lean と機械検査
  137. A-05 この本の作り方
  138. A-06 仮定の索引

Lean の言明と機械検査の限界

この章で分かること — 機械検査（Lean）が保証するのは「書いてある命題（仮定の並び）から結論が出ること」だけで、仮定が正しいことも、Lean の中の実数が物理の量を表していることも保証しない、という約束を、一段目の束の一覧で確かめます。#print axioms が標準の三つの公理に収まっていても見抜けない二つの型（結論を定義に置く・依存の円）を、出典を伏せた例で見て、読者が自分で言明を点検する手順を置きます。

前提となる章 — A-04 Lean と機械検査（札「Lean」の意味）・10-12 §03（依存グラフと番号の規則）・10-08 §08（区間演算の出力を仮定に置いた組み立て）。Lean そのものの読み方は Lean の案内。

先に言うこと — 水準は〔二〕〜〔三〕です。§01〜§02 と §06 は〔二〕で読めます。この部は仮定 H を検討の軸に置いた部で、Lean はその組み立ての代数の段を確かめる道具として使っています。この章は質量ギャップも連続極限も示しません。

この章の順序
  1. 機械検査が保証すること — 仮定の並びから結論への矢印（例：命題 4.5 の合成）
  2. 三つの公理と #print axioms — 清さの基準・native_decide を使わない理由
  3. 一段目の束 — 束ごとの定理の数・何の代数か・仮定の置き方（表 1）・四次元格子の側（表 2）
  4. 仮定は定理名の隣に — 読み方の規律と、区間演算の層が Lean の外にあること
  5. 四つの限界 — 仮定の正しさ・対象の符号化・結論を定義に置く・依存の円（表 3）
  6. 読者が自分で点検する手順 — 六つの問い
  7. 規約の翻訳 — 同じ文字・同じ名前が別の量を指す所（表 4）
  8. 束の分け方 — 記事・論文・主題ごと
01

機械検査が保証すること — 仮定の並びから結論への矢印

Lean は、数学の言明を型として書き、その証明を型の項として書くと、小さな核（カーネル）がその証明が言明に合っているかを機械的に検査する仕組みです（Lean の案内 01）。この本で「Lean」の札を付けた行は、その検査を通った定理を指します。札が保証することは一つだけです。

この本の約束

札「Lean」が付いた行で保証されているのは、定理の文に書いてある仮定が全て成り立てば、書いてある結論が成り立つことです。仮定が成り立つこと、文の中の記号が本文の量を表していること、その文が本文の主張と同じ意味であることは、保証されていません。

例として、命題 4.5 の合成（10-05 §04 段 3）の定理の文を写します。

theorem H3_H4_compose (CP Cbox n ca K4 C ξ D hbar S0 : ℝ) (hn : 0 < n) (hca : ca < 1)
    (hh : 0 < hbar) (hS : 0 < S0) (hD : D = hbar / S0)
    (hH3 : CP ≤ (1 + 1 / n) * Cbox / (1 - ca)) (hH4 : Cbox ≤ K4 * (C * ξ) ^ 2 / D) :
    CP ≤ (1 + 1 / n) * K4 * C ^ 2 / (1 - ca) * (ξ ^ 2 * S0 / hbar)

読み方。一行目の括弧の中は全て実数（ℝ）で、CP も ξ も名前の付いたただの実数です。hH3 は命題 H3 の結論 CP≤(1+1/n)Cbox/(1−calt)C_P\le(1+1/n)C_{\rm box}/(1-c_{\rm alt})、hH4 は命題 H4 の結論 Cbox≤K4(Cξ)2/DC_{\rm box}\le K_4(C\xi)^2/D を、仮定として受け取っています。定理が確かめたのは、この二つと D=ℏ/S0D=\hbar/S_0 から (13) CP≤Kξ2S0/ℏC_P\le K\xi^2S_0/\hbar が出る代数です。CP が T=∞T=\infty の経路の測度の Poincaré 定数であること、命題 H3・H4 の結論が実際に成り立つこと（つまり条件 (H1)〜(H4) と前提の行）は、Lean の外にあります。

この「矢印だけ」という性格は弱点ではなく、使い方の前提です。依存グラフ（10-12 §03）の「初」の節点の多くは、仮定の行を入力にとる代数で、その代数に写し間違いや符号の誤りが無いことを Lean が確かめます。何が仮定として入っているかが文の中で名指されるので、仮定の行の一覧（統合表）と突き合わせることができます。

02

三つの公理と #print axioms

Lean の核の型理論の上に、標準の道具立ては三つの公理を足します。命題の外延性 propext（同値な命題は等しい）、商の健全性 Quot.sound（同値な元は商で等しい）、選択 Classical.choice（存在の証明から元を取り出す）です。ある定理がどの公理に依るかは、命令 #print axioms 定理名 で一覧になります。

この本の束では、各ファイルの末尾に主な定理の #print axioms を置き、その出力の全ての行が三つの公理の部分集合であることを、清さの基準にしています。証明を飛ばす sorry を使うと一覧に sorryAx が加わり、自分で axiom を宣言するとその名が加わるので、この基準は「証明に穴が無く、勝手な公理も足していない」ことの機械的な確認になります。表 1 の全ての束（「公理の写し」の欄。2026-10-09 に別の計算機で取り直した写しを含む）で、三つ以外の公理の名が一つも無いことを読み直しました。三つのうち Classical.choice を使わない定理もあります（例えば tb_range は propext と Quot.sound だけ）。

寄り道 native_decide を使わない理由。

decide は、有限の場合分けで決まる命題を核の中の計算で確かめます。native_decide は同じ計算を、Lean のプログラムとして翻訳して機械語で走らせ、その答えを信頼します。速い代わりに、信頼の範囲が核から翻訳器と実行環境にまで広がり、その信頼は一覧に追加の公理として現れます（版によっては宣言ごとに別の名前の公理が生える）。この本の束では native_decide を使わず、清さの基準を「一覧の全ての行が三つの公理の部分集合」に置いています。特定の公理の名の有無で見ると、名前の付き方が版で変わったときに見落とすからです。

03

一段目の束 — 何の代数を確かめたか

一段目の Lean の定理は、主題ごとのファイル（束）に分かれています。表 1 は主な束を、本文で引いた章の順に並べたものです。「定理の数」はファイルの中の theorem／lemma の宣言の数、「代表の定理」の欄には定理名と、その定理の仮定を同じ欄に書きます。

表 1　一段目の主な束（定理の数は宣言の数。公理の写し：○＝末尾の #print axioms の出力が別に残っていて、全ての行が三つの公理の部分集合であることを読み直した。2026-10-09 に別の計算機で取り直した写しを含む）
束定理の数何の代数か代表の定理（仮定）章公理の写し
LatticeGaugeOneScale12H↑・H↓ と質量の読み替え（等号の版）hup_is_gap_positivity（0<m0\lt m・CP=1/m2C_P=1/m^2・CP≤Kξ2C_P\le K\xi^2）10-01○
LatticeGaugeHupBridge18片側の橋・冪の下の半分・陰性対照hup_is_gap_positivity_of_lower（0<mlat0\lt m_{\rm lat}・κ/mlat2≤CP\kappa/m_{\rm lat}^2\le C_P・CP≤Kξ2C_P\le K\xi^2）・first_power_does_not_bridge（陰性対照）10-01○
LatticeGaugeDoubleWellTestbed7命題 L の有限和の骨local_rayleigh_ratio_le_one（0<m0\lt m・ak≥ma_k\ge m・ck≥0c_k\ge0・∑ckak>0\sum c_ka_k\gt0）10-04○
LatticeGaugeTwoScalePoincare8分散の分割・凸な芯の曲率・縮約した二状態の値・Glauber の帯の比split_poincare_le（分割の式・二つの局所 Poincaré・平均差・形の加法・定数が非負）10-04・10-05○
LatticeGaugeDoubleWellKramers10比の挟みから冪の H へpower_H_of_kink_ratio（0<K,s,δ0\lt K,s,\delta・1≤R≤K/ℏ1\le R\le K/\hbar・s/ℏ≤ln⁡ξs/\hbar\le\ln\xi）10-04・10-05○
LatticeGaugeH1Assembly17命題 H1 の率の代数・六節点の余白の算術・環の GershgorinH1_assembly（名前つきの七つ：分解・細かい側・Helffer の判定・余白・0<λ0\lt\lambda・(T4)・率の条件）10-06○
LatticeGaugeCoarseSideUniform20(T4) の算術・Muckenhoupt の両側の形T4_paper_numeric（λc≥1.3×10−4\lambda_c\ge1.3\times10^{-4}）10-06○
LatticeGaugeIntervalQfreeWindow150補題 TAU の一次分数・傾けの恒等式・被覆から窓へ・律速のセルの再計算win_qfree_window_le_of_interval_table（区間演算の出力の表）10-08○
LatticeGaugeRingUnconditionedWindow20環の外の鎖の窓の組み立てunc_window_lt_one_of_table（区間演算の出力の表）10-07・10-08○
LatticeGaugeRingInnerChain22壁の角の比・環の SWS_Wsw_inner_le（qin≤13/10q_{\rm in}\le13/10・qout≤0.998888530q_{\rm out}\le0.998888530）10-07○
LatticeGaugePartitionFramework14区画の和・Gibbs の段・合成と閉じる条件comp_close（X>0X\gt0・b,A≥0b,A\ge0・ℓ>0\ell\gt0・Barta・(Σ.3)・Bochner の三つの不等式）10-09○
LatticeGaugeRemVProxy23命題 P5 の組み立てpath5_conditional（剰余の不等式・代理の比・稀さ・算術の余裕を名前つきで）10-09○
LatticeGaugeDetourKills・…217・16迂回策の「殺した一行」の算術型ごとの補題（10-10 表 4）10-10○
LatticeGaugeBoxReduction23補題 TP・偶奇の箱・ずらしの平均・陽性と陰性の対照box_shift_average（各ずらしで二族の不等式・Cbox≥0C_{\rm box}\ge0・重なりの和 ≤E\le\mathcal E）10-05・10-11○
LatticeGaugeBoxGap18命題 H4・ckgc_{\rm kg} の代数・H3 と H4 の合成H3_H4_compose（§01 の文）10-05・10-11○
LatticeGaugeCoreMixing・CoreMaxCorr・CoreThreeStage15・20・18芯の三段（補題 BV・命題 G・補題 TB・三段の合わせ）three_stage（各段の上界）10-11○
LatticeGaugeCoreActionGap15局所の項が消えること・端の線引きcloc_term_vanishes（(ΔScore)・ξ\xi の読み・ΔS∗<2S0\Delta S_*\lt2S_0）10-11○
LatticeGaugeGlobalLyapunov21Lyapunov の判定の代数と一次元ガウスの陽性対照gauss1d_bbcg・gauss1d_equality（仮定なし）10-14○

表 1 の定理は、どれも実数・有限の和・数列の上の不等式と等式です。測度・作用素・経路の空間を型として持つ定理はありません。区間演算の束（IntervalQfreeWindow の 150 の宣言の大半）は、最後の段の上界の式をセルごとに有理数で計算し直したもので、数は多いが中身は算術です。全ての束の索引は 付録 A-04 と分担します。

四次元格子の側。四次元格子で試した道の定理（10-02 §07 表 4）は、言明が直接に語る対象の型で分けると表 2 です。

表 2　四次元格子の側の定理の対象の型と性格（行は定理、性格の記号は 10-02 の表 4 の分類に対応：R＝再証明・A＝整理・C＝条件つき・N＝陰性対照・M＝格子の定理）
対象の型定理の数例
実数（と自然数）だけ23chain_band・drain_exponent
数列・実関数11S4_two_sided・conditional_scale_bound
有限集合・有限群の上の和8intact_frac_le・meff_ge_of_corr
内積空間の作用素1tau_int_le
格子のゲージ場（四元数・Haar 測度）3one_link・hess_gauge
計46性格で数えると（対にした二つの定理を一行として 41 行）R 11・A 15・C 7・N 5・M 3

格子のゲージ場を型として持つ定理は三つで、Wilson 測度の期待値・相関・隙間についての定理はありません。性格の対応は、10-02 の表 4 の「再証明・整理・条件つき・陰性対照・格子の定理」が、この表の R・A・C・N・M に一つずつ当たります。

04

仮定は定理名の隣に

この部の本文と表では、定理名を書くときにその定理の仮定を同じ欄に並べます（例：H1_assembly（仮定：名前つきの七つ））。定理名だけを書くと、要約の段で「Lean で確定」と読まれ、条件つきの代数が無条件の結果に膨らむからです。統合表（10-12）でも、グラフの各節点の下に定理名と仮定を書きました。

計算機援用の行では、Lean の欄は三つの層に分かれます（10-08 §08）。(1) 代数の核（一次分数の単調性・傾けの恒等式・被覆から窓への代数）、(2) 律速のセルと無作為に選んだセルの再計算（全てのセルではない）、(3) 区間演算の出力の表を仮定に置き、窓の全体の結論を出す組み立てです。区間演算そのもの（段の写像の区間の評価・求積・不変集合・丸めの規約）は Lean の外にあり、その正しさは照合と対照の検査（10-08 §07）に依ります。表を仮定に置いた定理の札は、「区間演算の出力が正しいなら、窓の全体の結論は代数として正しい」と読みます。

05

四つの限界 — 三つの公理に収まっていても見抜けないもの

清さの基準（§02）を満たす定理でも、次の四つは保証されません。前の二つは §01 の約束の言い換えで、後の二つは、言明の書き方そのものが結論を空にしてしまう型です。

(1) 仮定の正しさ。定理は仮定を一歩も証明しません。H3_H4_compose の hH4 が偽なら、結論は何も言いません。

(2) 対象の符号化。Lean の中の CP は名前の付いた実数で、それが経路の測度の Poincaré 定数であることは本文の読みです。同じ名前が別の束で別の量を指しても検査は通ります。例えば measured_ratio という名の定理は一段目の二つの束（CoreActionGap と HierarchicalLink）にあり、別の名前空間の別の量についての文です。名前は内容の保証になりません。

(3) 結論を定義に置く。欲しい性質をそのまま定義の中に書き、その定義を仮定に取ると、結論は仮定の書き写しになり、証明は一行で閉じます。次は型だけを示す擬似の Lean です。

結論を定義に置くと何でも閉じる（擬似の Lean・型の例） 
def InSpectrum (E : ℝ) : Prop := E = 0 ∨ c ≤ E          -- 欲しい性質を「スペクトル」の定義に書く
theorem gap (E : ℝ) (h : InSpectrum E) : E = 0 ∨ c ≤ E := h   -- 仮定をそのまま返すだけ
def massGap : ℝ := 1 / 2                                  -- 値を字面で置けば正であることも閉じる

三行とも検査を通り、#print axioms の一覧も空か三つの公理の中に収まります。それでも「スペクトル」がどの作用素のスペクトルとも結ばれていないので、数学の内容はありません。ある文書は、主定理の連言の一つをこの型で書き、別の一つを字面で置いた数で書いていました。定理名に「質量ギャップ」が入り、検査は全て通っていても、言明が対象を符号化していない例です。

(4) 依存の円。Lean は定理を一つずつ検査します。定理 A が B の結論を仮定に取り、定理 B が A の結論を仮定に取っていても、二つとも検査を通ります。どちらの結論も無条件には出ていないのに、二つを並べると「示された」ように見えます。証明が文章で書かれた場合も同じで、ある文書では、隙間が正であるという最後の結論を、途中の段（クラスター性・真空の一意性）の前提に「後で示す」として置いていました。依存グラフに描くと、大きな番号の結論から小さな番号の段へ辺が戻り、番号の規則（10-12 §03）が破れます。

表 3　四つの限界と、この本の防ぎ方
限界検査で見えるかこの本の防ぎ方
(1) 仮定の正しさ見えない（仮定は引数）仮定を定理名の隣に書く（§04）・仮定の行を統合表で一つずつ数える（10-12 表 1）
(2) 対象の符号化見えない（実数に名前を付けただけ）Lean の対象の型を本文で言う（§03 の「実数・有限の和」）・規約の翻訳（§07）・本文の量と定理の文の記号の対応を章ごとに書く
(3) 結論を定義に置く見えない（三つの公理に収まる）定理の文を本文に写し、定義を遡って読む（§06 の問い 3・4）・陰性対照の定理（仮定を外すと崩れる例）を置く
(4) 依存の円見えない（定理は一つずつ検査される）依存グラフの番号の規則・仮定の行が結論の量を含まないことの確かめ（10-12 §03）

陰性対照の定理は、(3) への防ぎとして働きます。例えば no_bound_when_c_one（二つの σ\sigma-代数が同じ c=1c=1 なら箱への帰着は何も言わない）や first_power_does_not_bridge（一乗の冪では橋が架からない）は、仮定を外したときに結論が崩れることを示し、仮定が飾りでなく結論に効いていることの確かめになります。

06

読者が自分で点検する手順 — 六つの問い

Lean の札の付いた主張を読むとき、次の六つを順に問います。この本の定理にも、他の文書の定理にも同じように使えます。

  1. 清さ。#print axioms の出力の全ての行が propext・Classical.choice・Quot.sound の部分集合か。出力が手元に無ければ、それは「未確認」です。
  2. 仮定の一覧。定理の文の、コロンより前の括弧（型が命題の引数）を全て書き出す。本文が「無条件」と言っている主張に、命題の引数が残っていないか。
  3. 結論の定義を遡る。結論に現れる名前（InSpectrum のようなもの）の定義を開き、それが結論と同じ文を中に持っていないか。仮定と結論が同じ命題の展開になっていないか。
  4. 対象の型。主張が語るはずの対象（測度・作用素・場）が、定理の文の中に型として現れているか。現れているのが実数・自然数・有限の和だけなら、対象との結び付きは本文の読みにあります。
  5. 依存の向き。複数の定理をつないだ主張なら、どの定理がどの定理の結論を仮定に取っているかを番号つきの節点に並べ、前提の番号が結論の番号より小さく置けるか。置けなければ円の候補です。
  6. 陰性対照。仮定を一つ外すと結論が崩れる例が示されているか。示されていなければ、その仮定が結論に効いているかを自分で確かめる。

例。§01 の H3_H4_compose に当てると、(1) 三つの公理の部分集合、(2) 命題の引数は hn・hca・hh・hS・hD・hH3・hH4 の七つ、(3) 結論は実数の不等式で、定義の遡りは要らない、(4) 対象は全て実数、(5) hH3・hH4 は命題 H3・H4 の結論で、統合のグラフでは [072]・[075]・[104] が [105] より小さい、(6) calt=1c_{\rm alt}=1 では箱への帰着が何も言わないことを no_bound_when_c_one が示す（hca は飾りでない）、となります。答えは「命題 H3 と H4 が成り立てば、命題 4.5 の不等式が代数として出る」で、それ以上ではありません。

07

規約の翻訳 — 同じ文字・同じ名前が別の量を指す所

Lean の定理は記号の意味を知らないので、同じ文字が別のファイルで別の量を指しても検査は通ります。表 4 は、定理の中の規約を本書の記号表（付録 A-01）に翻訳し、食い違いを食い違いとして書いたものです。上の六行は四次元格子の側、下の五行は一段目の側です。

表 4　Lean の中の規約と本書の記号
量Lean の中本書食い違い
β\beta一リンク積分の eβ⟨u,M⟩e^{\beta\langle u,M\rangle}、⟨u,M⟩=12Re tr(UM†)\langle u,M\rangle=\tfrac12{\rm Re\,tr}(UM^\dagger)β=2N/g2\beta=2N/g^2無い（N=2N=2 で β=4/g2\beta=4/g^2）。Shen–Zhu–Zhu の規約とは β=4βSZZ\beta=4\beta_{\rm SZZ}
tr と角度リンク角 U=eiϑ⋅σU=e^{i\vartheta\cdot\sigma}Ta=σa/2T^a=\sigma^a/2、U=eiθaTaU=e^{i\theta^aT^a}θ=2ϑ\theta=2\vartheta、CP(θ)=4CP(ϑ)C_P^{(\theta)}=4C_P^{(\vartheta)}。定数倍なので冪には効かない
aadrain_exponent の a格子間隔Lean の aa は記帳の長さの逆数 1/ξRG1/\xi_{\rm RG}
η\eta静的な冪・感受率の冪・重なりの冪ηs\eta_s と ηdyn\eta_{\rm dyn} を添字で分ける在る（同じ文字が三つの量）
κ\kappa一ループの傾き・模型の係数・Casimir 項の係数・辺を共有しない面の寄与一ループの傾き 11/(3π2)11/(3\pi^2) だけ在る（同じ文字が四つの量）
CPC_P（四次元）名前の付いた実数Langevin の Poincaré 定数。正規化を名指す場 AA と角度 ϑ\vartheta の正規化で CP(A)=βCP(ϑ)C_P^{(A)}=\beta C_P^{(\vartheta)}
ℏ\hbar と ε\varepsilonhbar（実数）。格子の刻みは数として入るE(f)=(ℏ/ε)∑iE∣∂if∣2\mathcal E(f)=(\hbar/\varepsilon)\sum_i\mathbb E|\partial_if|^2、ε=12\varepsilon=\tfrac12無い。ε=0.25\varepsilon=0.25 の読みと ε=12\varepsilon=\tfrac12 の読みの間の換算は書いていない（10-14 §05）
芯の CPC_P の目盛り芯の段の定理の CPC_P10-11 は E\mathcal E の規約、10-09 は ℏ∫∣∇g∣2\hbar\int|\nabla g|^2 の規約C(10-09)=C/ε=2CC^{(10\text{-}09)}=C/\varepsilon=2C（10-11 §05）
KKpower_H_of_kink_ratio の K命題 4.5 の KK と K′=KS0K'=KS_0Lean の KK は本文の K′K'（10-05 段 5）
定理名measured_ratio—二つの束に同じ名の別の定理（§05 の (2)）
読みの値K_ff_C2・three_stage_3em4 などの数の定理読測った値を仮定に置いた算術。値の分類は「読」のまま（Lean の札で「初」にならない）
08

束の分け方 — 記事・論文・主題ごと

束（ファイル）は、一つの主題（一つの命題とその補題）ごとに分けています。一つの章や記事が引く定理が複数の束にまたがるのは普通で、表 1 の「章」の欄がその対応です。分け方の規律は四つです。

この部は仮定 H を検討の軸に置き、Lean は一段目の組み立ての代数の段に使いました。証明の検査を別の形（例えば対象そのものを型にした形式化）で行う視点は、第 11 部で扱います。

この章が言えている範囲

言えている言えていない
Lean 表 1 の束の定理は、仮定を引数に明示した形で機械検査を通っている。表 1 の全ての束で、残っている #print axioms の出力の全ての行が三つの公理の部分集合仮定の行の正しさ。Lean の実数を経路の測度の量と読むことそのものの検査
一段目の Lean の定理は全て実数・有限の和・数列の上の文で、測度・作用素を型として持つ定理は無い測度や作用素を型にした形式化
四つの限界と防ぎ方（表 3）・点検の六つの問い六つの問いを通った主張が正しいこと（問いは必要な確かめで、十分ではない）
区間演算の層が Lean の外にあり、表を仮定に置いた組み立てだけが Lean の中にあること区間演算の実装の形式的な検証

出典と再現

もの種別出典・道具
束の定理の宣言と数Lean各束の原稿（Lean 4・Mathlib）の宣言を読み、theorem／lemma の行を数えた。定理名と仮定は本文の各行
公理の写しLean各束の #print axioms の出力の写しを読み、三つ以外の公理の名（sorryAx など）が無いことを、それを含む対照の写しで検出できることを確かめてから数えた
三つの公理と #print axioms典J. Avigad, L. de Moura, S. Kong, S. Ullrich ほか『Theorem Proving in Lean 4』の章 Axioms and Computation
四次元格子の側の型の層と性格（表 2）本書10-02 §07 と旧版の対応表の数え（同じ 46 定理）
結論を定義に置く型・依存の円の型の例本書構成や証明を主張する外部の二つの文書の読み（出典は伏せ、型だけを書いた。文書の正否は判定しない）

この章で使った語 — 機械検査・束・清さの基準・三つの公理・#print axioms・native_decide・対象の符号化・結論を定義に置く・依存の円・陰性対照の定理・規約の翻訳。意味は A-02 用語集 にあります。

次に読む章：10-14 突き合わせ — 記録の数と既知の数 — 一段目の各条件に最も近い既知の定理との距離、書誌の確かめの要約、陽性対照に使った既知の数を、記録の数と一行ずつ並べる。

← 10-12 統合表と依存グラフ目次10-14 突き合わせ — 記録の数と既知の数 →

改訂 2026-10-09：初版。
2026-10-09：表 1 の「公理の写し」が △ だった四束（HupBridge・RemVProxy・DetourKills・GlobalLyapunov）を、別の計算機で #print axioms を取り直して ○ にした。