makoto-developer's テックブログ

連載「量子もつれ攻略ノート」 11/13

証明可能領域の境界から定理7へ —— 量子もつれ攻略ノート(11)

本稿の位置づけ

本稿は、毎日更新で書き溜めた攻略ノート旧第11〜22稿を、内容をそのまま保って1本に統合したものである。証明の詰めにあたる後半として、数値探索から厳密証明へ手法を切り替え、証明可能な範囲と未解決の範囲の境界、真実の粒度、そして三つの完全証明(定理5・6・7)までを収める。

本稿の見取り図(12本のノート)。ノート11〜13では「どこまでが証明でき、どこからが原理的にできないか」の境界と、証明が書かれるべき粒度を確定する。ここは行き止まりの報告を含む。ノート14〜16では二つの整列極(同順・反転)に完全な証明を与え(定理5・定理6)、その間で問題全体の座標系を取り出す。ノート17〜22では、二つの極を結ぶ回転Bell族を永年方程式に還元し、有理数区間演算で全域を証明する(定理7)。タイトルの「証明可能領域の境界から定理7へ」はこの道筋を指す。

各ノートの冒頭には、そのノートが何をしようとしているかを書いた「本ノートの位置づけ」を置いた。試行錯誤の記録なので、うまくいかなかった試みも同じ形式で並んでいる。

文中の「第N稿」という相互参照は統合前の通し番号を指す。第1〜10稿は公開済みの各記事、第11〜22稿は本稿の各ノート(ノートNが第N稿にあたる)、第23〜34稿は第12稿、第35〜51稿は第13稿に収録されている。


ノート11:双対証明書が存在する範囲の境界、釣り合った重みで消える理由

本ノートの位置づけ

第9稿の証明書探索は素朴な山登りで、違反 前後で止まっており、実行不能なのか探索器が弱いのか判別できずにいた。本ノートは正攻法に切り替える。証明書問題「」は3つの凸集合の共通部分を探す問題であり、これには交互射影法(Dykstra)という収束保証つきの標準手法がある。半正定値錐への射影は固有値クリップ、部分転置はフロベニウスノルムの等長写像なので、各射影が厳密に書ける。純Pythonでも実装できる。

答えは白黒はっきり出た。証明書が存在する領域と、原理的に存在しない領域とに、きれいに分かれたのである。前者は成果、後者は行き止まりの確定であり、どちらも証明戦略の地図になる。


1. 道具:Dykstraの交互射影

変数 エルミート)。制約集合:

  • :射影=固有値の負部分を0にクリップ
  • をクリップして引き戻す( は等長なので厳密な射影)
  • :同様

Dykstra反復は、共通部分が空でなければその点に収束し、空ならば違反が正の値で停留する。つまり実行可能・不能の判定器になる。

2. 結果:境界の発見

族F()に沿って、証明書が相手にする行列 (第10稿)の重みの釣り合い を変えながら判定した:

(釣り合い度)違反(400反復)違反(800反復)判定
0.020.0004実行可能
0.050.0028実行可能
0.10.013実行可能(遅い収束)
0.30.19境界域
0.50.71(完全均衡)(不動)実行不能

読み:

  1. 等号多様体の近くでは証明書が存在する。証明書は状態非依存なので、その幾何 を共有するすべての状態でM3'が成立する。数値が最も1に肉薄していた危険な領域(第6稿の比率0.988等)が、点ごとの証明で覆われた。存在の理由も見えている。 では (単一の射影、)となり で足りる。証明書 の実測スペクトルも 級で、ほぼ裸の が合格する。
  2. 釣り合い領域では証明書が存在しない。反復を倍にしても違反が微動だにしない。集合は交わっていない。つまり、 の領域では「その幾何を共有する全状態で成立」という形の証明は原理的に不可能である(実際、幾何だけ共有して負性配分の異なる仮想的な演算子が上限を破る。第8稿の非物理反例と同じ穴)。この領域の証明は、実際の状態のデータ(総量 ・自己整合)を使わざるを得ない。

3. 証明戦略の使い分け(更新)

これで証明戦略の適材適所が確定した:

領域実測√r使える手法状態
片翼PPT(≤1(等号あり)個別支配(第7稿・定理1)証明済み
ロップサイド( 小・等号多様体近傍)→1証明書(本ノート)幾何ごとに証明済み(数値証明書)。解析的な証明書の閉形式化が次の目標
釣り合い×両翼NPT≤0.89LP(定理4): 1.03〜1.3未証明。状態非依存の証明は不可能と判明(本ノート)。自己整合を使う道具が必須

危険だった場所(等号多様体近傍)が最も安全になり、余裕のある場所(釣り合い領域・実測0.7〜0.89)だけが未証明で残る。逆説的だが健全な配置になった。残る区画に必要な道具の候補は二つある。(i) 自己整合SDP( が実際に固有ベクトルであるという制約を双対に組み込む)。(ii) 粗い不等式——釣り合い領域の実測は0.11以上の安全マージンをもつので、精密な評価でなくても届く可能性がある。第10稿が筆頭に挙げたLPの2次補正より、先にこちらを試すべきかもしれない。

4. 本ノートの結果

項目状態
Dykstra判定器(収束保証つき)実装・検証済み
等号多様体近傍の証明書存在(違反 数値証明書=点ごとの証明
釣り合い領域の証明書不在数値判定(反復不変の停留)
証明戦略の境界(状態非依存 vs 自己整合)特定
M3'完全証明未達。残る区画は「釣り合い×両翼NPT」一つ

参考文献

  • J. P. Boyle, R. L. Dykstra, A method for finding projections onto the intersection of convex sets in Hilbert spaces, Lecture Notes in Statistics 37 (1986) 28。
  • H. H. Bauschke, J. M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review 38 (1996) 367。
  • 第6〜10稿(本シリーズ)。
  • 検証コード:Dykstra交互射影(固有値クリップ射影・等長性)、素のPython。

ノート12:分解できない真実、円板則の粒度の境界

本ノートの位置づけ

数学の不等式を証明する常套手段は「原子に分解して各原子で示す」ことだ。補題L‡()の左辺の点 は、各負固有ベクトル が定める点 の凸結合である(、重みは )。円板は凸なので、各点が円板内なら凸結合も円板内。つまり原子版 が成り立てばL‡は自動で従う。成り立つのか。答えは否だった。本ノートは、その反例と、そこから確定する「証明が書かれるべき解像度」の話である。つまり分解による証明の道が閉じたという、失敗側の報告になる。


1. 検査と反例

ランダム混合状態228例から負固有ベクトル457本を採取し、各本で を計測した:

疑うべきは数値誤差だが、逆反復ではなく回転蓄積つきJacobiによる厳密固有ベクトルで再計算し、残差 (機械精度)を確認した。破れは本物である。ただし破れ幅はわずか 。原子は円板から髪の毛一本だけはみ出せる。

2. 真実の階層

これで三つの水準の真偽が出揃った:

水準主張判定余裕
M3'(観測量)予想(1万例で反例なし)
L‡(負部分の集団)予想(596例で反例なし)
L(原子)*(本ノート)

余裕が一段降りるごとに削られ、最後の一段で符号が反転する。真実には粒度の下限がある。個々の負固有ベクトルは規則を破れるが、 重みまで込めた集団全体では破れない。一本が円板の外に出るとき、相棒の固有ベクトル(97%の状態で負固有値は2本)と重みの配分が必ず内側へ引き戻している。なぜそうなるのかが、L‡の証明の核心になる。

3. 証明戦略への含意

  1. 原子化ルートは成立しない:「各固有ベクトルで示して足す」型の証明は存在しない(反例があるため)。橋の補題やLemma A等の単一ベクトル評価だけでは原理的に届かない。これで第10稿・第11稿の障害(定理3の限界・釣り合い領域の証明書不在)の根因も統一的に説明できる。すべて「原子レベルでは僅かに偽で、集団レベルでのみ真」という同じ構造の影だった。
  2. 書かれるべき証明の形:負部分 全体を一つの対象として扱い、(i) が直交し完全もつれ部分空間(すべての元がA|BCもつれをもつ部分空間。2⊗4では次元3以下という古典的制限が、負固有値3個以下の理由でもある)を張ること、(ii) 重み が正値性 で結ばれること。この二つを同時に使う集団的評価である。
  3. 反例の解剖が次の手がかり:はみ出した原子()の相棒がどこにいて、なぜ集団としては円板の内側に戻るのか。このペアの幾何を閉じ込める不等式が見つかれば、L‡はペア版の議論で閉じる可能性がある。

4. 本ノートの結果

項目状態
L* ⟹ L‡(凸結合)自明・証明済み
L*は偽(残差 の厳密反例)確定
真実の階層(測定済み
証明の最低解像度=負部分の集団レベル確定
M3'完全証明未達。次の目標:ペア(2本の負固有ベクトル+重み)レベルの円板則

参考文献

  • 第8〜11稿(本シリーズ):還元定理・証明書が存在する範囲の境界。
  • K. R. Parthasarathy, On the maximal dimension of a completely entangled subspace, Proc. Indian Acad. Sci. 114 (2004) 365:完全もつれ部分空間の次元。
  • N. Johnston, Non-positive-partial-transpose subspaces can be as large as any entangled subspace, Phys. Rev. A 87 (2013) 064302:PT負固有値数と部分空間の関係。
  • 検証コード:回転蓄積Jacobi・残差検証つき、素のPython。

ノート13:余裕は千分の一、重みつき円板則L†

本ノートの位置づけ

前のノート(第12稿)で「原子(各負固有ベクトル)は円板則を破れる」と確定した。破れ幅は 、しかし本物である。ならば集団はなぜ守られるのか。本ノートでは、正しい粒度の法則を特定し、証明済みの還元の連鎖を一段延長する。法則そのものは予想のままだが、還元は証明つきで一段伸びる。


1. 重みつき三角版 L†

各負固有ベクトル (重み )の点 に対し、原点からの距離の重みつき平均を考える:

還元(証明済み・三角不等式1行) 

のノルムは 以下。第8稿の還元定理と合成。)

検査結果:

母集団max 判定
ランダム262例0.969057成立
敵対的240例0.998485成立(余裕は

原子版L*は偽()、重みつき版L†は真()。粒度の境界は「重みを掛けるかどうか」のちょうど間にあった。

2. 補償機構の解剖

はみ出し原子を含む実例(第12稿の検査——ランダム混合状態228例・負固有ベクトル457本——で見つかった1件)の全データ:

原子重み
★円板の外0.81630.57851.00050.9013
相棒(内側)0.33820.37040.50150.0987
集団 0.76910.55800.9502

意外なことに、はみ出す原子が重みの9割を持っている。つまり補償は「外れ者の重みを削る」形では起きていない。効いているのは別の二つで、外れ幅が構造的に 級までしか許されないことと、相棒が深く内側にいることである。直交する2本の負固有ベクトルは同時に円板の縁には立てない:一方が縁に張り付くと、直交性と完全もつれ部分空間の制約が相棒を内側へ押し込む。この「同時最大化の禁止」がL†の核心であり、証明すべき最終補題の形である:

予想L† )の負固有ベクトル系 と、両縮約の負固有ベクトル に対し

3. 証明の全景(更新)

事実出典
片翼PPT領域は証明済み、ロップサイド領域は幾何ごとに数値証明書つき第7稿の定理1(個別支配)・証明書(第11稿)
状態非依存の証明は釣り合い領域で原理的に不可能第11稿
原子化は原理的に不可能(L*偽)第12稿
残る証明対象=L†:直交完全もつれ系の重みつき幾何本ノート
L†の余裕:(敵対的)本ノート

問題はもう「モノガミー」の顔をしていない。残っているのは純粋な行列幾何の一問、「直交する2〜3本のもつれベクトルは、2枚の積型射影に対して、重みつき平均で同時にどこまで整列できるか」であり、その答えが1を超えないことを示せば、10年開いていた予想の混合状態版が閉じる。ここまでの全還元・全数値・全反例つきで、この一問を後続の研究(または読者)に引き渡せる状態になった。

4. 本ノートの結果

項目状態
還元 L†⟹L‡⟹M3'証明済み
予想L†(502例・最大0.9985)数値的に強く支持
補償機構(同時最大化の禁止)解剖済み・定式化済み
M3'完全証明未達。残るはL†一問

参考文献

  • 第8・11・12稿(本シリーズ)。
  • K. R. Parthasarathy, Proc. Indian Acad. Sci. 114 (2004) 365:完全もつれ部分空間。
  • 検証コード:厳密固有ベクトル(回転蓄積Jacobi・残差検証つき)による502例の検査、素のPython。

ノート14:最難関の族に決着、定理5の完全証明

本ノートの位置づけ

震源の族に出会った第6稿から数えて9稿目、ようやく完全な証明が一つ取れた。本ノートの定理5は、本稿に収めた三つの完全証明(定理5・6・7)の一つ目である。決着がついたのは、このシリーズで一貫して最悪の数値(比率0.976〜0.99)を出し続け、Dykstra判定・LP上界・全数値探索の主対象だった敵対的な族、「二つのもつれペアが中央のAを取り合う」混合状態である。しかもSchmidt係数を任意化した一般族ごと証明できた。証明は誰でも検算できる初等計算なので、全文を載せる。


1. 定理5

定理5 任意の )、任意のSchmidt係数 に対し、族 はM3'()を満たす。等号は (下記記号)のとき、かつそのときに限る。

2. 証明

記号(各ペアの半コンカレンス×重み)、。ここでの は本ノート限りの記号で、相手ペアが持ち込む減衰を表す。第11稿で重みの釣り合い度に使った同名の記号とは別物なので注意されたい。

(i) 閉形式の導出。。その部分転置はブロック 上で となり(残りは対角非負)、唯一の負固有値から 対称性により 。全体の部分転置 は基底 上のブロック に唯一の負固有値 をもち(残りは対角非負)、 (数値照合:ランダムな 8組で全量 一致。)

(ii) 核心の1行。 を展開すると なので、示すべきは これは から自明である。等号は のとき、かつそのときに限る。

系(族F)  の場合が第6稿以来の敵対的な族F:。全域で厳密に成立、等号は のみ。

3. 何が決着したのか

この族は「危険な状態」の代表ではなく震源そのものだった。比率探索の最大値0.988(第6稿)、L‡の最大値0.983(第8稿)、L†の最大値0.9985(第13稿)、Dykstra証明書の存在境界(第11稿)は、全部この族とその摂動で観測された。その震源が、閉形式の前では1行で片づく。構造も透明になった。 成分を取り込むには (相手ペアの荷重)を必ず伴い、その分だけ円板の内側に沈む。等号(端点)は減衰がゼロの単一ペア極限だけである。

4. 命題R1候補の棄却と、残る課題

  • R1(ランク1⟹片翼PPT)は偽:6,000例中ランク1は244例、うち5例が両翼NPT(最大 、ただし と深い安全圏)。ランク1でも両翼が同時に負性をもつことはある。ただし、ごく弱くしか出ない。
  • 残る課題:定理5の族(以下、族G₀と呼ぶ)にA基底の回転( 側のAをひねる)と一般フラグを許した拡張族。数値探索200例では最大 で安全だが、閉形式は未導出。ここが次の(そして数値上は最後の)解析目標である。回転はふたたび状態を等号多様体へ近づける。「Aの取り合い」が最も強くなる配置であり、定理5の減衰メカニズムが回転でどう変形されるかが焦点になる。

5. 本ノートの結果

項目状態
定理5:族G₀(⊃族F)でM3'完全証明・等号条件決定証明完了
閉形式 照合)導出済み
R1候補反例5件で棄却
回転つき拡張族(max 数値安全・次の解析目標
M3'全体未完。次の対象は回転族

参考文献

  • 第6〜13稿(本シリーズ):この族が震源であることの全記録。
  • 検証コード:閉形式照合・鍵不等式の全域確認・回転族の数値探索、素のPython。

ノート15:三つの負性は一つの行列、ブロック座標と核心不等式の在処

本ノートの位置づけ

定理5(第14稿)の証明はなぜあれほど短かったのか。答えを一般化可能な形で抽出したところ、問題全体の最終座標系が得られた。M3'の3つの負性は、実はすべて一つの行列の異なる読み方である。これがその整理の記録である。新しい定理は出ないが、証明すべき対象の形が一つに絞られる。


1. ブロック座標

をAの基底で ブロックに書く:

すると部分転置はブロック転置になり、3つの負性の源が一望できる:

駆動する行列減衰
の特異値( が上限スケール)
)の特異値
の特異値

すべては一枚のコヒーレンス行列 の読み方の違いである:全体の負性は そのもの、周辺の負性は の2通りの部分トレース。正値性 )という形で を対角ブロックに従属させる。コヒーレンスは自由に取れるわけではなく、対角ブロックの大きさに制限される。

2. 核心不等式C★とその運命

定理5の族はこの座標で読むと透明である: はランク1、左ベクトルが積型、(無減衰)、 がそれぞれ を運び、減衰 が周辺だけを削る。つまりあの証明は、無減衰の核心不等式

の等号(族が飽和)と、減衰の一方向性(周辺のみ削る)の合わせ技だった。

ではC★は一般の で成り立つか。否である。次の表の比はC★の左辺を右辺で割った値で、1を超えていれば破れを意味する。

の母集団
ランダム4000例0.695(安全)
ランク1に制限1.938
ランク2に制限1.278
テンソル結合型1.230

破れの典型は (積型コヒーレンス):両部分トレースが を保ったまま となり、両方が同時に大きくなって比率2に迫る。だが、ここで正値性が効く。積型 をもつには対角に同じ積状態の成分が必要で、その成分の部分トレースが周辺のPT対角を持ち上げ、周辺負性をちょうどゼロにする(例: では )。第8稿の「正値性なしでは偽」、第12稿の「原子化不能」、本ノートの「C★単体は偽」という三つの障害は、すべて同じ一つの事実の三つの側面である:

M3'の最終形は「減衰つきC★」である。コヒーレンス の積型成分は両部分トレースに二重計上されうるが、正値性の制約がその成分に限って周辺の減衰を強制する。この「二重計上と、正値性による相殺」を一般の で定量化することが、残された唯一の問題である。

3. 本ノートの結果

項目状態
ブロック座標(3負性=1行列の読み替え)定式化完了
定理5の証明構造の同定(C★の等号+一方向減衰)完了
C★単体は偽(ランク1で1.938)確定
正値性の制約が反例を消す機構特定(定量化が残る)
M3'全域未完。最終形「減衰つきC★」一問に集約

参考文献

  • 第8・11・12・14稿(本シリーズ):三つの障害定理と定理5。
  • R. Bhatia, Matrix Analysis, Springer (1997):ブロック行列・特異値の一般論。
  • 検証コード:特異値計算(Jacobi)によるC★検査(母集団は§2の表のとおり、ランダム4000例と制限つき3種)、素のPython。

ノート16:鎖型の恒等式 n = a + b、定理6の完全証明

本ノートの位置づけ

定理5(第14稿)は「二つのペアのA側Schmidt基底が同じ向きに整列した」族を証明した。本ノートはその対蹠点、基底が反転して整列した鎖型の族に決着をつける。こちらは思いがけず美しい恒等式が現れた。全体の負性が周辺負性の和そのものになる。


1. 定理6

定理6(鎖型整列族) 任意の 、Schmidt係数 に対し、族 (第1項=AB ペア・Cフラグ、第2項=AC ペアだがAのSchmidt基底が反転)では が成り立つ。したがってM3'は より余裕 で成立、等号は に限る。

数値照合:Bell型()で全 、および任意Schmidt係数のランダム300例で

2. 証明

を成分計算すると、非対角は2箇所だけに現れ、 は対角非負部分と互いに素な2つの ブロックに分解する:

一方、周辺の部分転置を同様に計算すると:

  • の負性を担うブロック()=ブロック1と同一の行列
  • の負性を担うブロック()=ブロック2と同一の行列

(鎖型の整列では、部分トレースがこれらのブロックの成分を一切損なわない。各ブロックの結合相手が「トレースで消える方向」に居ないためである。)ゆえに の2つの負固有値はそれぞれ厳密に に等しく、

3. 意味:直列と並列

定理5と定理6で、二種類の整列が対照をなす:

構造恒等式M3'の余裕
定理5(同順整列)2つのコヒーレンスが1つの負方向を共有(並列合成)減衰項
定理6(反転整列)2つのコヒーレンスが別々の負方向(直列合成)

並列(ピタゴラス合成)では周辺が減衰で目減りして円板に収まり、直列(線形合成)では和が二乗和を自動的に支配する。どちらの極でもM3'は別の理由で成立する。一般の状態はこの2つの合成則の混合であり、どちらの理由もその極で消えない、というのが全域予想の姿だと言える。

4. 回転族の現在地

回転Bell族(第14稿で残った対象。定義式は次の第17稿の冒頭に書く)では が回転角 に依存しないことが示せる(Bellペアの周辺が のため減衰項が回転不変)。両端点は証明できた:

  • :定理5(同順整列)
  • :定理6(反転整列、本ノート)

内部 :数値では が単調減少して で底を打ち、余裕の最小値はちょうど 。残る課題は単調性(または )の証明一つ。

5. 本ノートの結果

項目状態
定理6:鎖型族の恒等式 とM3'(余裕 証明完了
直列/並列の二極構造の同定完了
回転Bell族:両端点証明済み・内部は 一問前進
M3'全域未完

参考文献

  • 第14・15稿(本シリーズ):定理5とブロック座標。
  • 検証コード:恒等式の照合(Bell型全p+任意Schmidt係数300例、)、素のPython。

ノート17:回転族の証明設計図、計算機援用証明のプログラム

本ノートの位置づけ

定理5(同順整列・第14稿)と定理6(反転整列・第16稿)で両端点が証明できた回転Bell族(数値上M3'に残る最後の対象)の内部に決着をつけるため、計算機援用証明の完全な設計図を引く。四色定理やKepler予想の流儀で、解析的な骨格+有限個の検証可能な数値評価に分解し、各部品の数値を出し切る。本ノートで証明が完成するわけではない。ここで作った部品が、第21・22稿の定理7でそのまま使われる。


1. 対象と全体図

矩形 上で を示す。既知:

  • :定理5(等号は
  • :定理6、、margin (等号は
  • :単一ペア=等号多様体(margin

つまり margin は矩形の2辺で消える。内部の正値性を、(A) 角の帯の解析展開と (B) 内部コンパクト集合のグリッド証明に分けて示す。

2. 判明した構造(本ノートの計算結果)

(1) の回転不変性(証明済み) Bellペアの片翼周辺は で回転不変、かつ減衰項が と可換なため、 のスペクトルは に依存しない。ゆえに残るのは「 の下界」一問。

(2) での接触は2次的 差分測定で (全 )。 で滑らかに底 に接する。margin は 線上で (内部 )を保つため、この辺はすでに安全(定理6)。

(3) 角の帯の鍵定数(閉形式を同定)  展開の一次係数を支配する定数 =AB項のPT、=純AC項PTの負方向射影)を全域スキャンした結果: これより帯では となり、 で解析的に閉じる。 に達するのは ちょうど、すなわち等号多様体の二重角のみ。

(4) 内部グリッドの実測  グリッドで (最小は二重角方向)、margin はさらに の余裕を持つ。Lipschitz実測:

3. 残工程(2点)

  1. 二重角 の結合展開:帯の一次係数 線の保護 が同時に退化する角。2変数の同時展開( の斉次評価)で正値性を出す。定型的だが未実施。
  2. 証明可能なLipschitz上界:実測 に対し、素朴な解析上界()は粗すぎてグリッド密度が非現実的になる。トレースノルム摂動の構造(負部分のランク≤2・サポートの局所性)を使った sharpened bound が必要。

この2点が埋まれば、定理7(回転Bell族全域)は計算機援用証明として完結する。

4. 本ノートの結果

項目状態
の回転不変性証明済み
両端点(定理5・6)証明済み
の同定閉形式一致(解析導出は定型・未清書)
内部グリッド・Lipschitz実測完了
二重角の結合展開/証明可能なL上界残工程
M3'全域未完(残るのは本設計図の2点+一般ランク2)

参考文献

  • 第14・16稿(本シリーズ):定理5・6。
  • 計算機援用証明の先例:K. Appel, W. Haken(四色定理・1977);T. Hales(Kepler予想・2005/Flyspeck 2014)。
  • 検証コード:グリッド・微分・鍵定数スキャン、素のPython。

ノート18:永年方程式、回転族は一本の4次式に潰れた

本ノートの位置づけ

回転Bell族(M3'に数値上残る最後の対象)の内部を調べるうち、この族の全構造が一本の明示的な4次方程式に潰れることがわかった。導出は厳密(ランク2のレゾルベント縮約)で、両端点の定理5・6が方程式の因数分解として自動的に再現される。本ノートはその導出と、残った単一命題の特定である。


1. 構造表示

部分転置が最大もつれ射影をSWAPに変える恒等式 により:

=ABシングレット⊗=回転されたACシングレット⊗。全体の負性は、対角の正の背景から2本のシングレット方向を引き抜いた構造である。なお、ここで対角部分に付けた は本ノート限りの記号であり、第11稿の証明書問題に出てきた とは別物である。

2. 永年方程式(厳密導出)

負の方向はランク2なので、レゾルベント縮約 が固有値問題を に落とす。 は対角で、必要な行列要素は3つの初等関数だけになり:

結合パラメータ は、第14稿でSchmidt係数に使った とは無関係の記号である。

数値照合:負根和=直接固有値計算の と全格子点で 一致。

両端点の自動再現

  • :方程式は に因数分解。 の負根はちょうど の負根はちょうど (第16稿・定理6の恒等式 が「因数分解」として再導出される)
  • :完全結合となり定理5の構造(1本の負根 への合流)を再現

結合の強さはただ一つの項 が担い、回転角は としてのみ入る。

3. 精密化法則と最終命題

グリッド検証(直接固有値・):

そしてこの法則は、より簡潔な命題から従う:

命題M(最終形) 永年方程式の負根和 について非減少。

命題M ⟹ 定理7 より

命題Mは物理をすべて剥ぎ取った一変数族の明示的4次式の根の単調性であり、係数はすべて上に書いた初等式。数値では全域で成立(負根対の外側の根は とともに深く、内側の根は浅くなるが、和は常に増える。結合項 が外側の根で大きいためである)。残る作業は係数計算による機械的な検証(判別式・終結式の符号評価)である。

4. 本ノートの結果

項目状態
構造表示 恒等式(SWAP表示)
永年方程式(レゾルベント縮約)厳密導出照合
定理5・6の因数分解としての再現確認
精密化法則 グリッド検証(最小0)
命題M(4次式の負根和の単調性)数値成立・機械的検証が残工程
定理7命題M一問に還元
M3'全域未完(本族の先に一般ランク2)

参考文献

  • 第14・16・17稿(本シリーズ):定理5・6・証明設計図。
  • ランク落ち摂動のレゾルベント縮約:標準的手法(例:T. Kato, Perturbation Theory for Linear Operators)。
  • 検証コード:永年方程式の照合・グリッド、素のPython。

ノート19:等高線の傾き比べ、命題Mの一行化と区間証明の設計

本ノートの位置づけ

第18稿で回転族は永年方程式 に潰れ、定理7は「負根和 の単調性」(命題M)一問になった。ここで は、第18稿の永年方程式の右辺にあった結合項の係数である。本ノートはその命題をさらに削る。削った結果は、高校生に説明できる形になった。山の等高線上で、右の斜面と左の斜面のどちらが急か、という問いである。


1. 一行化

とおくと、負根 は方程式 の解、すなわち関数 の2つの外側枝の等高点である(左枝は へ下り、右枝は へ上る)。すると だから:

を使った)。ゆえに:

命題M(一行版) 等高点で、上り枝は下り枝より急である:

2. 多項式化と検証

分母を払うと(、等高条件 を使用)、命題Mは根号もτも含まない多項式条件になる。以下、下付きの1・2は2つの負根 での値を表す:

(実際 なので 。)

検証:曲線上 点( を59分割×59分割した格子のうち、曲線条件 を満たす点だけを採り、 は二分法で追跡)で全点 、最小値は の対称点近傍、スケール上の実質ゼロ=等号近接)。境界 )では に正側から収束することも確認。

の極構造も整理した:6本の単純極は2組が対消滅して

)。正の寄与は負根 の極から、負の寄与は有界な2項からしか来ない。等号()で右枝の極 が発散して支配する構造が、単調性の「物理的理由」である。

3. 残る厳密化:区間証明の設計

命題Mは2パラメータ のコンパクト領域上の多項式不等式(曲線制約つき)なので、有理数区間演算による箱分割検証(Flyspeck流の計算機援用証明)で完結できる:

  1. 領域を箱に分割し、各箱で の区間評価が を含まなければ棄却(曲線が通らない)
  2. 含む箱では の区間評価が なら証明済み、さもなくば細分
  3. 境界帯()は第17稿の展開( ほか)で解析的に処理

すべて有理数演算なので浮動小数の丸めに依存しない。実装は純Pythonで可能(Fraction区間)。これが定理7完結までの最後の工程である。

4. 本ノートの結果

項目状態
による一行化厳密導出
多項式化 (根号・τなし)厳密導出
曲線上2,151点の検証(全点成立・等号は境界のみ)完了
極構造の整理(対消滅・支配極の特定)完了
区間証明(箱分割・有理数演算)設計完了・実装が残工程
M3'全域未完(本族 → 一般ランク2 → 全域の順)

参考文献

  • 第18稿(本シリーズ):永年方程式。
  • T. Hales et al., A formal proof of the Kepler conjecture (Flyspeck), Forum Math. Pi 5 (2017):区間証明の範例。
  • 検証コード:等高追跡・W評価、素のPython。

ノート20:有理数の箱で証明する、区間証明コアの完成

本ノートの位置づけ

第19稿で設計した区間証明を実装し、走らせ、コア領域の証明が完成した。使ったのは分数(有理数)演算だけ。浮動小数の丸めに依存する箇所はゼロであり、各箱の判定は厳密な不等式の連鎖である。ただし完全決着ではない。境界の3つの補題が箱で閉じずに残る(その始末は第21稿でつく)。20稿目なので、シリーズ後半のまとめも付ける。


1. 何を証明したか

命題M(永年方程式の負根和の単調性、⟹定理7⟹回転Bell族のM3')は、多項式条件

に同値変形済み(第19稿)。ここで は第19稿の を曲線上で書き直した形、 は探索領域である。これを箱分割で証明する:各箱で (i) 枝マーカー()の区間violation→棄却、(ii) の区間が を含まない→曲線が通らず棄却、(iii) の区間下限が正→証明済み、いずれでもなければ分割。

2. 技術の要:中心形式

素朴な区間評価(一次収束)は依存性問題で失敗した。13万箱を訪問して3万箱が未解決だった。解決したのは中心形式である:

中心値は分数で厳密に、勾配は粗い区間で評価する。誤差が箱幅の二乗で縮む(二次収束)ため、同じ領域が1,925箱・10秒・未解決ゼロで閉じた。 の勾配()はすべて明示的な多項式なので、これも厳密である。

3. 証明された領域と残る3補題

領域結果
(退化角の箱 を除く)証明済み(8,041箱・45秒)
証明済み(1,925箱・10秒)
スライバー( まで)証明済み(149箱)
側全域B↔C相対称性()より従う

残る補題(すべて局所解析・設計済み)。以下のR1〜R3は本ノート内の補題番号で、第14稿で棄却した命題R1とは別物である:

  • R1(退化角) の微小箱。 となり が二次接触の極小をもつ退化。等高点対は極小の両側に対称に乗り、(数値)。三次項の非対称性による正値性の局所展開。
  • R2( 連続帯):残り 端点は定理5で証明済みなので、margin の Lipschitz 連続性(明示定数)で閉じる。
  • R3( 帯)。単一ペア等号多様体への接近で、第17稿の鍵定数 の剰余つき展開で閉じる( は対称)。

4. 後半のまとめ(第11〜20稿)

#成果等級
11証明書が存在する範囲の境界(Dykstra判定・状態非依存証明の不可能領域)数値判定+構造定理
12原子化不能(L*の厳密反例・粒度の境界)確定
13重みつき円板則L†・還元連鎖の完成証明済み還元+予想
14定理5:同順整列族の完全証明証明完了
15ブロック座標・核心不等式C★の在処定式化+反例
16定理6:鎖型族の恒等式 証明完了
17回転族の証明設計図・部品確定
18永年方程式(レゾルベント縮約・照合)厳密導出
19命題Mの一行化(等高傾き比較)・多項式化厳密導出
20区間証明コア(有理数演算・中心形式)証明完了(コア領域)

参考文献

  • 第17〜19稿(本シリーズ)。
  • R. E. Moore, Interval Analysis (1966);中心形式:Krawczyk, Neumaier の標準教科書的手法。
  • T. Hales et al., Forum Math. Pi 5 (2017):Flyspeck(区間証明の範例)。
  • 証明コード:interval3.py / interval4.py(分数演算のみ・乱数不使用・決定的)。

ノート21:8秒の証明、定理7・主要部の完全証明

本ノートの位置づけ

第20稿の区間証明コアは「単調性(命題M)」を証明対象にしていたため、退化角( が二次接触する点)の近傍が箱で閉じず、3つの境界補題が残っていた。本ノートの発見は単純である。証明したいのは単調性ではなくM3'そのものなのだから、marginを直接証明対象にすればよい。この置き換えで障害が消滅した。


1. 発想の転換

証明対象を変更する:

記号が紛らわしいので断っておくと、ここで導入した は margin の頭文字であり、単調性を主張する命題Mとは別物である。以後 と書けば margin を指す。

新しい対象の利点:

  1. 退化角が消える は旧対象では の特異点だったが、新対象では のただの内点である。
  2. の境界が消える)では )では となり、どちらも曲線上の普通の点として箱で覆える( で負固有値が1本になる縮退も、 として自動的に正しく扱われる)。
  3. 等号多様体は の両端の線だけに退く。

コスト: は根号を含むが、有理数の検証つき平方根区間(候補値を縮小・拡大して を厳密に確認)で処理できる。

2. 実行結果

領域 (物理枝は なので全曲線を内包;枝はマーカー の区間判定で選別):

定理7(主要部・証明完了) 回転Bell族 の全域でM3'を満たす:(狭義)。

証明 永年方程式(第18稿・厳密)により負根対 ∩枝マーカー領域にあり、 は上記の箱分割による有理数区間演算で機械的に検証された(中心形式・二次収束、平方根は検証つき区間、浮動小数不使用・決定的)。

第6稿で比率0.988を出した敵対的な族も、第11稿で証明書の不在が判明した釣り合い領域も、第20稿で残った退化角も、すべてこの8秒の中で一括処理された。

3. 残るはp端の帯だけ

未証明は 。B↔C相対称性()により実質1本の帯である。ここは単一ペア等号多様体への接近域で、margin は とともに消える( 側では の線形、 側では 。後者の縁は定理6が全 で証明済みなので、帯の中身だけが残る)。必要なのは2変数 の摂動補題1本:一次係数 の非負性と剰余評価。第17稿の の計算がその主要部品である。

4. 本ノートの結果

項目状態
定理7主要部(・全証明完了(8秒・未解決0)
発想の転換(margin直接証明で退化と境界が消滅)本ノート
検証つき平方根区間実装済み
p端の帯(実質1本・摂動補題)残工程
M3'全域未完(本族完結 → 一般ランク2 → 全域)

参考文献

  • 第18〜20稿(本シリーズ):永年方程式・一行化・区間証明コア。
  • 証明コード:interval5.py(決定的・分数演算のみ・8秒で再現可能)。

ノート22:定理7の完全証明、回転族の決着

本ノートの位置づけ

第14稿の定理5から9稿かけて追い続けた回転Bell族が、ついに全域で証明できた。本ノートは証明の完全な組み立てを記す。計算機援用部分は決定的(乱数なし)・有理数演算のみ(丸め誤差なし)・数秒で誰でも再検証可能。解析部分はLagrange剰余の明示定数まで書き下した初等評価である。


定理7(完全版)

回転Bell族 は、すべての でM3'を満たす:

証明の組み立て(4部品)

部品1(主要部  第21稿。永年方程式(第18稿・厳密)による負根対の特徴づけの上で、margin を直接、有理数区間演算(中心形式・検証つき平方根)で証明。3,253箱・8秒・未解決0。

部品2(帯  試験ベクトル下界 =ABシングレットのRayleigh商+ブロックの負固有値;直交する2方向なので和が正当な下界。以下、第1項すなわちRayleigh商の部分を と書く)に対し、 を区間証明。実装の要は2つの破滅的相殺の除去:(i) boost を有理化 に、(ii) 差 を中心形式( が小さいことを直接利用)に。この2点で、10分でタイムアウトしていた計算が3,429箱・2秒・未解決0になった。なお、ここに出てくる は本ノート限りの記号で、第13稿の (重みつき距離平均)や第11稿・第18稿の とは別物である。

部品3(尾部 ・解析補題) 全定数明示の初等評価。 とおくと恒等式 を2回微分して得る)から 上で 。Lagrange剰余により

  • 領域A):boostを捨て、 より
  • 領域B): なのでboost有効、 より boost を足しても 、よって

部品4(端と対称性) :単一ペア()で等号成立・自明。:BとCのラベル交換は族を で自身に移し、 不変なのでM3'は転送される。

何が決着したのか

この族は、シリーズが発見したすべての危険な領域を含む。等号多様体に肉薄する敵対的な族(第6稿・比率0.988)、状態非依存の証明書が存在しない釣り合い領域(第11稿)、二重根の退化角(第20稿)。それらが一つの定理の中で、それぞれ適した手法(区間演算・相殺除去・初等展開)で処理された。

証明の構造自体にも収穫がある。「どの手法がどこで効くか」の地図、すなわち大域は計算機の箱、境界帯は試験ベクトル+区間、漸近尾部は明示剰余の手計算という配置は、次の対象(一般ランク2)でもそのまま使える形をしている。

本稿12本のノートを通してみると、出発点は「どこまでが証明できるか」の境界だった。状態非依存の証明書は釣り合い領域には存在せず(第11稿)、原子ごとに分解して足す証明も存在しない(第12稿)。証明は負部分の集団を丸ごと扱うしかない、という制約が先に確定したのである。そこから方針を変え、扱える族を一つずつ閉じにいった。同順整列(定理5)、反転整列(定理6)、その二つの極を結ぶ回転(定理7)である。タイトルの「証明可能領域の境界から定理7へ」は、この移動を指している。M3'そのものはまだ予想のままで、残っているのは重みつき円板則L†と、一般フラグの二ペア族から一般ランク2へ向かう道である。

本ノートの結果

項目状態
定理7(回転Bell族・全域)証明完了
部品1〜4(それぞれ独立に検証可能)公開済み(コード+本ノートの初等評価)
M3'全域未完。次の対象:一般フラグの二ペア族 → 一般ランク2 → 全域

参考文献

  • 第14・16・18・19・20・21稿(本シリーズ):部品の開発史。
  • 証明コード:interval5.py(部品1)・strip4.py(部品2)、決定的・分数演算のみ。
  • 尾部補題:本ノートに全文(外部依存なし・初等)。