【論文538】計算機に任せたのが場合分けか不等式かで、証明の性質が変わる

要旨

四色定理もケプラー予想も「計算機による証明」と呼ばれる。本稿が示すのは、機械に任せたものが場合分けか不等式かで、手数が先に分かるかどうかが変わることである。新しい定理も法則も主張しない。

第一に、場合分け型では手数が先に分かる。二値 $10$ 個で $\mathbf{1024}$ 通り、$15$ 個で $\mathbf{32768}$ 通り、$20$ 個で $\mathbf{1048576}$ 通りと、始める前に数えられる（第2節）。

第二に、これが本稿の芯である。不等式検証型では、手数を決めるのは余裕である。同じ式でも余裕 $\mathbf{0.5}$ なら箱 $\mathbf{77}$ 個、$\mathbf{0.001}$ なら $\mathbf{1406877}$ 個で、$\mathbf{18271.1}$ 倍違う（第3節）。

第三に、余裕が零だと終わらない。等号が起きる場合は、いくら箱を割っても下界が $0$ を超えない（第3節）。

第四に、膨らむ原因は式の書き方にある。$(x-y)^{2}$ を $x^{2}-2xy+y^{2}$ と書いて区間で評価すると、$x$ と $y$ が同じ値をとるという束縛が失われる（第3節）。

第五に、だから二つの型で、事前に言えることが違う。場合分け型は「何時間で終わる」が言え、不等式検証型は終わってみるまで言えない（第4節）。

第六に、分離子は、余裕という量が在るかどうかである。場合分け型にはその量が無い（第4節）。

キーワード：計算機による証明、四色定理、ケプラー予想、区間演算、形式証明。

射程（何を示さないか）

新しい定理も法則も主張しない。四色定理も、ケプラー予想の証明も、区間演算も標準的である。どちらかの証明を再現しない。本稿は二つの型の性質を、小さな見本で測るだけである。四色定理の可約性検査も、ケプラー予想の線形計画も実行していない。計算機による証明の正当性を論じない。人が読めない証明を信じてよいかという問いには入らない。形式化の話をしない。定理証明支援系による検証（フライスペック計画など）は、本稿の二分類とは別の軸である。区間演算の実装を比べない。中心形式やアフィン算術を使えば膨らみは減る。本稿が使ったのは素の区間である。計算量の分類を主張しない。箱の数は一つの実装での実測であり、下界ではない。既刊との関係：論文303 は公式が $4$ を返すのにその一点だけ証明が効かないと示した。あちらは証明が届かない一点を見た。本稿は証明が届くまでの手数が、何で決まるかを見る。論文315 はどの次元が特別かは問いごとに違うと示した。接吻数の証明も球充填の証明も、本稿の第二の型に属する。論文260 は同値性が定理でテーゼが定理でないと示した。「計算機で確かめられる」も定理の性質であって、計算機の性質ではない。論文300 は同根か別根かが判定できると示した。二つの型は「量の持ち物」の基準で別根である。加えたのは、二つの型を小さな見本で並べたこと、場合分け型の手数が閉じた式で先に出ることを確かめたこと、不等式検証型の箱の数を余裕ごとに $\mathbf{77}$ から $\mathbf{1406877}$ まで測ったこと、余裕を零にすると終わらないことを示したこと、分離子を「余裕という量が在るか」に置いたことである。

1. 記法と問い

設定：四色定理（$1976$）は、避けられない配置の集まりを列挙し、その一つ一つが可約であることを機械に確かめさせた。ケプラー予想（$1998$、形式化は $2014$）は、多数の不等式を機械に検証させた。

観察 1.1　どちらも「計算機による証明」と呼ばれる。人が全部は読めない量の計算が入る。しかし機械に任せているものが違う。

観察 1.2　片方は場合を数え、もう片方は大小を確かめる。場合の数は有限で、始める前に決まる。大小の確かめは、どこまで細かく割るかが最初には分からない。

問い：その違いは、数で出るか。

2. 場合分け型、手数が先に分かる

計算 2.1：二値の判断を $k$ 個並べたときの場合の数を、実際に数え上げて確かめた。

観察 2.2　数え上げた値が $2^{k}$ に一致する。数え落としが無いことの検査、そしてこの値は、一件も調べる前に $k$ から計算できる。

観察 2.3　だから見積もりが立つ。一件あたりの時間を測れば、全体の時間が掛け算で出る。「この証明は何時間で終わる」と、始める前に言える。

観察 2.4　難しいのは、列挙が尽くしているかどうかである。避けられない配置の集まりが本当に避けられないかは、機械が言うことではない。機械が担うのは尽くしたあとの一件ずつであって、尽くしたことの証明ではない。

3. 不等式検証型、余裕が決める

計算 3.1：$f(x,y)=x^{2}-2xy+y^{2}+\varepsilon>0$ を、$[-1,1]^{2}$ の上で素の区間演算で確かめる。下界が $0$ を超えるまで箱を四分割し、使った箱の数を数えた。

観察 3.2　これが本稿の芯である。余裕を $\mathbf{0.5}$ から $\mathbf{0.001}$ にすると、箱は $\mathbf{18271.1}$ 倍に膨らむ、式も領域も同じで、変えたのは余裕だけである。

観察 3.3　余裕が零だと終わらない。$f=(x-y)^{2}$ は $x=y$ の上で $0$ になる。そこでは下界が $0$ を超えることが原理的にありえない。境目の反対側である。

観察 3.4　膨らむ原因は式の書き方にある。$(x-y)^{2}$ と書けば非負であることが目で見えるのに、$x^{2}-2xy+y^{2}$ と書いて $x$ と $y$ を別々の区間で評価すると、同じ値をとるという束縛が失われる。これは区間演算の依存性問題と呼ばれる。式を書き換えれば箱は減る。

観察 3.5　だから箱の数は、問題の難しさそのものではない。式の表し方に依る。本稿の数は「素の区間演算で、この書き方をしたとき」の実測であって、下界ではない。

観察 3.6　それでも型の違いは残る。どんな書き方をしても、余裕が零なら終わらない。余裕という量が効くこと自体は、書き方に依らない。

4. 分離子

観察 4.1　分離子は、余裕という量が在るかどうかである。場合分け型には余裕に当たる量が無い。$k$ を決めれば $2^{k}$ が決まり、それ以上でもそれ以下でもない。

観察 4.2　事前に言えることが違う。場合分け型は「何時間で終わる」が言える。不等式検証型は、余裕を測るまで言えない。そして余裕は、証明しようとしている主張そのものの一部である。

観察 4.3　論文300 の「量の持ち物」で別根である。不等式検証型の手数は余裕という持ち物を要る。場合分け型の手数は個数だけを要る。同じ「計算機による証明」でも、必要な持ち物が違う。

観察 4.4　論文303 とは向きが違う。あちらは公式が値を返すのに、その一点で証明が届かないことを示した。本稿は証明が届くまでの手数が何で決まるかを見る。届くかどうかと、いくらかかるかは別である。

観察 4.5　論文315 の主題は第二の型に属する。接吻数も球充填も、不等式の検証で決まる。だから「どの次元が特別か」の証明の重さは、次元ごとの余裕に依る。

観察 4.6　言わないこと。人が読めない証明を信じてよいかは論じない。形式化による検証も、本稿の二分類とは別の軸である。

5. 点呼と結び

1. 二値 $20$ 個で $\mathbf{1048576}$ 通り（計算 2.1）：始める前に分かる。
2. 数え上げが $2^{k}$ に一致（観察 2.2）：数え落としが無い。
3. 見積もりが立つ（観察 2.3）：掛け算で時間が出る。
4. 列挙の網羅性は機械の仕事でない（観察 2.4）：尽くしたあとを担う。
5. 余裕 $\mathbf{0.5}$ で箱 $\mathbf{77}$ 個（計算 3.1）：$\mathbf{0.001}$ で $\mathbf{1406877}$ 個。
6. $\mathbf{18271.1}$ 倍に膨らむ（観察 3.2）：本稿の芯。
7. 余裕 $\mathbf{0}$ では決まらない（観察 3.3）：境目の反対側。
8. 原因は依存性問題（観察 3.4）：式の書き方に依る。
9. 箱の数は下界ではない（観察 3.5）：一つの実装の実測。
10. 分離子は余裕が在るか（観察 4.1）：場合分け型には無い。
11. 事前に言えることが違う（観察 4.2）：何時間かかるか。

結び：四色定理もケプラー予想も「計算機による証明」と呼ばれる。場合分け型では手数が先に分かる。二値の判断を $10$ 個、$15$ 個、$20$ 個と並べたときの場合の数は $\mathbf{1024}$、$\mathbf{32768}$、$\mathbf{1048576}$ で、数え上げた値が $2^{k}$ に一致する。この値は一件も調べる前に $k$ から計算できるので、一件あたりの時間を測れば全体の時間が掛け算で出る。難しいのは列挙が尽くしているかどうかで、そこは機械の仕事ではない。機械が担うのは尽くしたあとの一件ずつである。不等式検証型では、手数を決めるのは余裕である。同じ式を $[-1,1]^{2}$ の上で確かめるのに、余裕 $\mathbf{0.5}$ なら箱 $\mathbf{77}$ 個、$\mathbf{0.1}$ なら $\mathbf{1197}$ 個、$\mathbf{0.01}$ なら $\mathbf{45541}$ 個、$\mathbf{0.001}$ なら $\mathbf{1406877}$ 個で、$\mathbf{18271.1}$ 倍に膨らむ。式も領域も同じで、変えたのは余裕だけである。余裕を $\mathbf{0}$ にすると、いくら割っても下界が $0$ を超えない。$(x-y)^{2}$ は $x=y$ の上で $0$ になるからで、これは境目の反対側である。膨らむ原因は式の書き方にもある。$(x-y)^{2}$ と書けば非負が目で見えるのに、$x^{2}-2xy+y^{2}$ と書いて別々の区間で評価すると、同じ値をとるという束縛が失われる。だから箱の数は問題の難しさそのものではなく、一つの書き方での実測であって下界ではない。それでも、どんな書き方をしても余裕が零なら終わらない。分離子は、余裕という量が在るかどうかである。場合分け型には余裕に当たる量が無く、$k$ を決めれば $2^{k}$ が決まる。だから事前に言えることが違う。場合分け型は「何時間で終わる」が言え、不等式検証型は余裕を測るまで言えず、しかもその余裕は証明しようとしている主張そのものの一部である。論文300 の「量の持ち物」でいえば、不等式検証型の手数は余裕を要り、場合分け型の手数は個数だけを要る。論文303 は証明が届かない一点を見た。本稿は届くまでの手数が何で決まるかを見たので、向きが違う。論文315 の接吻数も球充填も第二の型に属するので、「どの次元が特別か」の証明の重さは次元ごとの余裕に依る。正直に言えば、どちらの証明も再現していない。二つの型の性質を小さな見本で測っただけで、四色定理の可約性検査もケプラー予想の線形計画も実行していない。人が読めない証明を信じてよいかという問いにも入らず、定理証明支援系による形式化は本稿の二分類とは別の軸である。区間演算の実装も比べておらず、中心形式やアフィン算術を使えば膨らみは減る。箱の数は一つの実装での実測であって下界ではない。言えるのは、機械に任せたものが場合分けか不等式かで、手数が先に分かるかどうかが変わる、そこまでである。

参考文献

1. Appel, K., & Haken, W. (1977). Every Planar Map Is Four Colorable. Illinois Journal of Mathematics.
2. Hales, T. C. (2005). A Proof of the Kepler Conjecture. Annals of Mathematics.
3. Hales, T. C., et al. (2017). A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi, 5, e2.
4. Moore, R. E., Kearfott, R. B., & Cloud, M. J. (2009). Introduction to Interval Analysis. SIAM.
5. 山岸勇輝 (2026). 『同値性は定理であり、テーゼは定理ではない』[論文260]. Zenodo. 10.5281/zenodo.22169292
6. 山岸勇輝 (2026). 『三百本目の点呼、同根か別根かは、判定できる』[論文300]. Zenodo. 10.5281/zenodo.22171914
7. 山岸勇輝 (2026). 『公式は $4$ を返すが、その一点だけ証明が効かない』[論文303]. Zenodo. 10.5281/zenodo.22172026
8. 山岸勇輝 (2026). 『どの次元が特別かは、問いごとに違う』[論文315]. Zenodo. 10.5281/zenodo.22208139

作成にあたって：本稿の着想と内容は、著者自身の考察に基づくものです。文章の構成整理や英訳、数式の確認には AI（大規模言語モデル）の助力を得ました。最終的な内容の解釈や誤りがあれば、それらはすべて著者の責に帰します。お気づきの点があれば、ご教示いただければ幸いです。

書誌

山岸勇輝（2026）「計算機に任せたのが場合分けか不等式かで、証明の性質が変わる」［論文538］. Zenodo.
DOI: 10.5281/zenodo.23014127

@misc{yamagishi2026yoi538,
  author = {Yamagishi, Yuuki},
  title = {Whether the Machine Was Given Cases or Inequalities Changes What Kind of Proof It Is},
  year = {2026},
  howpublished = {YOI: https://www.yamagishiyuuki.com/yoi/538},
  doi = {10.5281/zenodo.23014127},
  note = {Preprint, edition 1}
}