makoto-developer's テックブログ

国境線から定理10へ —— 回転Bell族、陥落の全記録 —— 量子もつれ攻略ノート(11)

国境線から定理10へ —— 回転Bell族、陥落の全記録

—— 量子もつれ攻略ノート(11)——

本稿の位置づけ

本稿は、毎日更新で書き溜めた攻略ノート旧第11〜22稿を、内容をそのまま保って1本に統合したものである。攻城戦の後半戦——数値探索から厳密証明へ武器を持ち替え、証明戦略の国境線、真実の粒度、そして三つの完全証明(定理8・9・10)までを収める。

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


ノート11:証書の国境線 —— 釣り合った重みで死ぬ理由

本稿の位置づけ

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


1. 道具:Dykstraの交互射影

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

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

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

2. 結果:国境線の発見

家族F()に沿って、重みの釣り合い を変えながら判定した:

(釣り合い度) 違反(400反復) 違反(800反復) 判定
0.02 0.0004 実行可能
0.05 0.0028 実行可能
0.1 0.013 実行可能(遅い収束)
0.3 0.19 境界域
0.5 0.71(完全均衡)(不動) 実行不能

読み:

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

3. 戦略地図の更新

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

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

危険だった場所(等号多様体近傍)が最も安全になり、余裕のある場所(釣り合い領域・実測0.7〜0.89)だけが未証明で残る——という逆説的だが健全な配置になった。残る区画に必要な道具の候補:(i) 自己整合SDP( が実際に固有ベクトルであるという制約を双対に組み込む)、(ii) 釣り合い領域での実測の深い安全マージン(0.11以上)を説明する粗い不等式で十分な可能性——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‡()の左辺の点 は、各負固有ベクトル が定める点 の凸結合である(、重みは )。円板は凸なので、各点が円板内なら凸結合も円板内——つまり原子版
MATHBLOCKTOKEN000
が成り立てばL‡は自動で従う。成り立つのか。答えはだった。本稿はその反例と、そこから確定する「証明が書かれるべき解像度」の話。


1. 検査と反例

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

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

2. 真実の階層

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

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

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

3. 証明戦略への含意

  1. 原子化ルートの死:「各固有ベクトルで示して足す」型の証明は存在しない(反例があるため)。橋の補題やLemma A等の単一ベクトル評価だけでは原理的に届かない——これで第10稿・第11稿の障害(定理5の壁・釣り合い領域の証書不在)の根因も統一的に説明できる。すべて「原子レベルでは僅かに偽で、集団レベルでのみ真」という同じ構造の影だった。
  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†

本稿の位置づけ

前稿で「原子(各負固有ベクトル)は円板則を破れる」と確定した。破れ幅は 、しかし本物。ならば集団はなぜ守られるのか——正しい粒度の法則を特定し、証明済みの還元の連鎖を一段延長する。


1. 重みつき三角版 L†

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

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

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

検査結果:

母集団 max 判定
ランダム262例 0.969057 成立
敵対的240例 0.998485 成立(カミソリ一枚)

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

2. 補償機構の解剖

はみ出し原子を含む実例(700例中1件)の全データ:

原子 重み
★円板の外 0.8163 0.5785 1.00050.9013
相棒(内側) 0.3382 0.3704 0.5015 0.0987
集団 0.7691 0.5580 0.9502

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

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

3. 攻略の全景(更新)

事実 出典
片翼PPT領域・ロップサイド領域は証明済み 定理4・証書(第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:完全もつれ部分空間。
  • 検証コード:厳密固有ベクトル(残差 級)による502例の検査——素のPython。

ノート14:最難関の家族、陥落 —— 定理8の完全証明

本稿の位置づけ

攻城戦9稿目にして、完全な証明が一つ取れた。落ちたのは、このシリーズで一貫して最悪の数値(比率0.976〜0.99)を出し続け、Dykstra判定・LP上界・全ハンティングの主戦場だった敵対的家族——「二つのもつれペアが中央のAを取り合う」混合状態——である。しかもSchmidt係数を任意化した一般族ごと落ちた。証明は誰でも検算できる初等計算なので、全文を載せる。


1. 定理8

定理8 任意の )、任意のSchmidt係数 に対し、族
MATHBLOCKTOKEN004
MATHBLOCKTOKEN005
はM3'()を満たす。等号は ——具体的には (下記記号)——のときに限る。

2. 証明

記号(各ペアの半コンカレンス×重み)、

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

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

系(家族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でも両翼は光れる——ただし極めて弱くしか光れない。
  • 残る前線:族G₀にA基底の回転( 側のAをひねる)と一般フラグを許した拡張族。数値偵察200例では最大 で安全だが、閉形式は未導出。ここが次の(そして数値上は最後の)解析目標である。回転はふたたび状態を等号多様体へ近づける——「Aの取り合い」が最も熾烈になる配置であり、定理8の対価メカニズムが回転でどう変形されるかが焦点になる。

5. 帳簿

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

参考文献

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

ノート15:コヒーレンスの簿記 —— ブロック座標と核心不等式の在処

本稿の位置づけ

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


1. ブロック座標

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

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

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

すべては一枚のコヒーレンス行列 の簿記である:全体の負性は そのもの、周辺の負性は の2通りの部分トレース。正値性 )という形で を対角ブロックに従属させる——コヒーレンスは無料ではなく、対角の質量を担保に発行される。

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

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

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

ではC★は一般の で成り立つか。

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

破れの典型は (積型コヒーレンス):両部分トレースが を保ったまま ——両取りで比率2に迫る。だが正値性がここで牙をむく:積型 を発行するには対角に同じ積状態の担保が必要で、その担保の部分トレースが周辺のPT対角を持ち上げ、周辺負性を正確に全滅させる(例: では )。第8稿の「正値性なしでは偽」、第12稿の「原子化不能」、本稿の「C★単体は偽」——三つの障害はすべて同じ一つの事実の three views である:

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

3. 帳簿

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

参考文献

  • 第8・11・12・14稿(本シリーズ):三つの障害定理と定理8。
  • R. Bhatia, Matrix Analysis, Springer (1997):ブロック行列・特異値の一般論。
  • 検証コード:特異値計算(Jacobi)によるC★検査8000例——素のPython。

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

本稿の位置づけ

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


1. 定理9

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

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

2. 証明

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

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

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

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

3. 意味:直列と並列

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

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

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

4. 回転族の現在地

回転Bell族(第14稿の前線)では が回転角 に依存しないことが示せる(Bellペアの周辺が のため減衰項が回転不変)。両端点は落ちた:

  • :定理8(同順整列)
  • :定理9(反転整列)——本稿

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

5. 帳簿

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

参考文献

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

ノート17:回転族の攻略図面 —— 計算機援用証明のプログラム

本稿の位置づけ

定理8(同順整列・第14稿)と定理9(反転整列・第16稿)で両端点が落ちた回転Bell族——数値上M3'の「最後の前線」——の内部を落とすための、計算機援用証明の完全な図面を引く。四色定理やKepler予想の流儀:解析的な骨格+有限個の検証可能な数値評価に分解し、各部品の数値を出し切る。


1. 対象と全体図

矩形 上で を示す。既知:

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

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

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

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

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

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

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

3. 残工程(2点)

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

4. 帳簿

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

参考文献

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

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

本稿の位置づけ

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


1. 構造表示

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

=ABシングレット⊗=回転されたACシングレット⊗全体の負性は、対角の正の背景から2本のシングレット方向を引き抜いた構造である。

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

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

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

両端点の自動再現

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

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

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

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

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

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

命題M ⟹ 定理10 より

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

4. 帳簿

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

参考文献

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

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

本稿の位置づけ

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


1. 一行化

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

を使った)。ゆえに:

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

2. 多項式化と検証

分母を払うと(、等高条件 を使用)、命題Mは根号もτも含まない多項式条件になる:

(実際 なので 。)

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

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

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

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

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

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

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

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稿で設計した区間証明を実装し、走らせ、コア領域の証明が完成した。使ったのは分数(有理数)演算だけ——浮動小数の丸めに依存する箇所はゼロであり、各箱の判定は厳密な不等式の連鎖である。20稿目なので、シリーズ後半戦の帳簿も付ける。


1. 何を証明したか

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

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

2. 技術の要:中心形式

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

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

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

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

残る補題(すべて局所解析・設計済み):

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

4. 後半戦の帳簿(第11〜20稿)

# 成果 等級
11 証書の国境線(Dykstra判定・状態非依存証明の不可能領域) 数値判定+構造定理
12 原子化不能(L*の厳密反例・粒度の境界) 確定
13 重みつき円板則L†・還元連鎖の完成 証明済み還元+予想
14 定理8:同順整列族の完全証明 証明完了
15 ブロック座標・核心不等式C★の在処 定式化+反例
16 定理9:鎖型族の恒等式 証明完了
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秒の証明 —— 定理10・主要部の完全証明

本稿の位置づけ

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


1. 発想の転換

証明対象を変更する:

新しい対象の利点:

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

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

2. 実行結果

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

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

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

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

3. 残るはp端の帯だけ

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

4. 帳簿

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

参考文献

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

ノート22:定理10、完全証明 —— 回転族の陥落

本稿の位置づけ

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


定理10(完全版)

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

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

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

部品2(帯  試験ベクトル下界 =ABシングレットのRayleigh商+ブロックの負固有値;直交する2方向なので和が正当な下界)に対し、 を区間証明。実装の要は2つの破滅的相殺の除去:(i) boost を有理化 に、(ii) 差 を中心形式( が小さいことを直接利用)に。この2点で、10分でタイムアウトしていた計算が3,429箱・2秒・未解決0になった。

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

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

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

何が落ちたのか

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

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

帳簿

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

参考文献

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