Whether the Machine Was Given Cases or Inequalities Changes What Kind of Proof It Is ── In the case-splitting kind the work is known before starting (1048576 cases for twenty binary choices), while in the inequality kind the margin decides ── and at a margin of 0 no amount of subdivision settles it ── [Paper 538]

Abstract

The four colour theorem and the Kepler conjecture are both called proofs by computer. What this paper shows is that whether the machine was handed cases or inequalities decides whether the amount of work is knowable in advance. No new theorem or law is claimed. Scope of this paper (scope note): No new theorem or law is claimed──the four colour theorem, the proof of the Kepler conjecture and interval arithmetic are all standard. Neither proof is reproduced──the properties of the two kinds are measured on small specimens; no reducibility check and no linear program from those proofs is run. The legitimacy of computer proof is not discussed──whether a proof no person can read may be believed is not entered. Formalisation is not treated──verification in a proof assistant is a different axis from this twofold division. Implementations of interval arithmetic are not compared──centred forms and affine arithmetic reduce the swelling; plain intervals were used here. No complexity classification is claimed──box counts are measurements of one implementation, not lower bounds. Relation to earlier papers: Paper 303 showed that a formula returns 4 while at that one point the proof does not reach──that paper looked at where proof fails to arrive; this one looks at what decides the cost of arriving. Paper 315 showed that which dimension is special depends on the question──the kissing number and sphere packing proofs both belong to the second kind here. Paper 260 showed that an equivalence is a theorem and a thesis is not──"checkable by machine" likewise belongs to the theorem, not to the machine. Paper 300 showed that sharing a root is decidable──the two kinds are separate roots under the criterion of what a quantity carries. What is added is setting the two kinds side by side on small specimens, confirming that case counts follow in closed form, measuring box counts from 77 to 1406877 by margin, showing non-termination at zero margin, and placing the separator on the existence of a margin. First, in the case-splitting kind the work is known in advance──ten binary choices give 1024 cases, fifteen give 32768 and twenty give 1048576, all countable before starting (Section 2). Second, and this is the core. In the inequality kind the margin decides──the same formula takes 77 boxes at a margin of 0.5 and 1406877 at 0.001, a factor of 18271.1 (Section 3). Third, at zero margin it never terminates──where equality occurs, no amount of subdivision lifts the lower bound above zero (Section 3). Fourth, part of the swelling comes from how the formula is written──writing (x-y)^2 as x^2-2xy+y^2 and evaluating over intervals loses the constraint that x and y take the same value (Section 3). Fifth, so the two kinds differ in what can be said beforehand──the case kind can promise a running time; the inequality kind cannot until it is done (Section 4). Sixth, the separator is whether a margin exists as a quantity──the case-splitting kind has no such quantity (Section 4). The four colour theorem and the Kepler conjecture are both called proofs by computer. In the case-splitting kind the work is known in advance──ten, fifteen and twenty binary choices give 1024, 32768 and 1048576 cases, and the enumerated counts match 2^k. The value follows from k before a single case is examined, so timing one case and multiplying gives the whole. The hard part is whether the enumeration is complete, and that is not the machine's work: it takes the cases one at a time after the set is fixed. In the inequality kind the margin decides──verifying one formula over [-1,1]^2 takes 77 boxes at a margin of 0.5, 1197 at 0.1, 45541 at 0.01 and 1406877 at 0.001, a swelling of 18271.1 with formula and domain unchanged. At zero margin nothing settles it, since (x-y)^2 vanishes along x=y and the lower bound cannot in principle rise above zero. Part of the swelling comes from the writing: (x-y)^2 shows non-negativity plainly, while x^2-2xy+y^2 over separate intervals loses the constraint that the two agree, which is the dependency problem. So the box counts measure one expression under plain intervals and are not lower bounds, and yet however it is written, zero margin never terminates. The separator is whether a margin exists as a quantity──the case-splitting kind has nothing corresponding to it: fix k and 2^k is fixed. So the promises differ. The case kind can state a running time in advance; the inequality kind cannot until the margin is measured, and that margin is part of the claim being proved. Under Paper 300, one kind of work carries a margin and the other only a count. Paper 303 looked at where proof fails to reach; this looks at what the reaching costs. The kissing numbers and packings of Paper 315 belong to the second kind, so the weight of those proofs depends on the margin in each dimension. To be honest──neither proof was reproduced; the two kinds were measured on small specimens, with no reducibility check and no linear program from the originals. Whether a proof no person can read may be believed was not discussed, and formal verification is a different axis. Implementations of interval arithmetic were not compared, and centred or affine forms would reduce the swelling. The box counts are measurements of one implementation, not lower bounds. What can be said is that handing a machine cases or inequalities decides whether the work is knowable in advance, and no further. On the making of this work: The ideas and content of this work stem from the author's own considerations. Assistance from an AI (a large language model) was used for structuring, English translation, and checking the algebra. Any remaining errors or misinterpretations are solely the author's. Feedback and corrections are sincerely appreciated. Keywords: computer-assisted proof, four colour theorem, Kepler conjecture, interval arithmetic, formal proof. ----- 四色定理もケプラー予想も「計算機による証明」と呼ばれる。本稿が示すのは、機械に任せたものが場合分けか不等式かで、手数が先に分かるかどうかが変わることである。新しい定理も法則も主張しない。 本稿の射程(射程注記):新しい定理も法則も主張しない──四色定理も、ケプラー予想の証明も、区間演算も標準的である。どちらかの証明を再現しない──本稿は二つの型の性質を、小さな見本で測るだけである。四色定理の可約性検査も、ケプラー予想の線形計画も実行していない。計算機による証明の正当性を論じない──人が読めない証明を信じてよいかという問いには入らない。形式化の話をしない──定理証明支援系による検証(フライスペック計画など)は、本稿の二分類とは別の軸である。区間演算の実装を比べない──中心形式やアフィン算術を使えば膨らみは減る。本稿が使ったのは素の区間である。計算量の分類を主張しない──箱の数は一つの実装での実測であり、下界ではない。既刊との関係:論文303 は公式が 4 を返すのにその一点だけ証明が効かないと示した──あちらは証明が届かない一点を見た。本稿は証明が届くまでの手数が、何で決まるかを見る。論文315 はどの次元が特別かは問いごとに違うと示した──接吻数の証明も球充填の証明も、本稿の第二の型に属する。論文260 は同値性が定理でテーゼが定理でないと示した──「計算機で確かめられる」も定理の性質であって、計算機の性質ではない。論文300 は同根か別根かが判定できると示した──二つの型は「量の持ち物」の基準で別根である。加えたのは、二つの型を小さな見本で並べたこと、場合分け型の手数が閉じた式で先に出ることを確かめたこと、不等式検証型の箱の数を余裕ごとに 77 から 1406877 まで測ったこと、余裕を零にすると終わらないことを示したこと、分離子を「余裕という量が在るか」に置いたことである。 第一に、場合分け型では手数が先に分かる──二値 10 個で 1024 通り、15 個で 32768 通り、20 個で 1048576 通りと、始める前に数えられる(第2節)。 第二に、これが本稿の芯である。不等式検証型では、手数を決めるのは余裕である──同じ式でも余裕 0.5 なら箱 77 個、0.001 なら 1406877 個で、18271.1 倍違う(第3節)。 第三に、余裕が零だと終わらない──等号が起きる場合は、いくら箱を割っても下界が 0 を超えない(第3節)。 第四に、膨らむ原因は式の書き方にある──(x-y)^2 を x^2-2xy+y^2 と書いて区間で評価すると、x と y が同じ値をとるという束縛が失われる(第3節)。 第五に、だから二つの型で、事前に言えることが違う──場合分け型は「何時間で終わる」が言え、不等式検証型は終わってみるまで言えない(第4節)。 第六に、分離子は、余裕という量が在るかどうかである──場合分け型にはその量が無い(第4節)。 四色定理もケプラー予想も「計算機による証明」と呼ばれる。場合分け型では手数が先に分かる──二値の判断を 10 個、15 個、20 個と並べたときの場合の数は 1024、32768、1048576 で、数え上げた値が 2^k に一致する。この値は一件も調べる前に k から計算できるので、一件あたりの時間を測れば全体の時間が掛け算で出る。難しいのは列挙が尽くしているかどうかで、そこは機械の仕事ではない。機械が担うのは尽くしたあとの一件ずつである。不等式検証型では、手数を決めるのは余裕である──同じ式を [-1,1]^2 の上で確かめるのに、余裕 0.5 なら箱 77 個、0.1 なら 1197 個、0.01 なら 45541 個、0.001 なら 1406877 個で、18271.1 倍に膨らむ。式も領域も同じで、変えたのは余裕だけである。余裕を 0 にすると、いくら割っても下界が 0 を超えない。(x-y)^2 は x=y の上で 0 になるからで、これは境目の反対側である。膨らむ原因は式の書き方にもある。(x-y)^2 と書けば非負が目で見えるのに、x^2-2xy+y^2 と書いて別々の区間で評価すると、同じ値をとるという束縛が失われる。だから箱の数は問題の難しさそのものではなく、一つの書き方での実測であって下界ではない。それでも、どんな書き方をしても余裕が零なら終わらない。分離子は、余裕という量が在るかどうかである──場合分け型には余裕に当たる量が無く、k を決めれば 2^k が決まる。だから事前に言えることが違う。場合分け型は「何時間で終わる」が言え、不等式検証型は余裕を測るまで言えず、しかもその余裕は証明しようとしている主張そのものの一部である。論文300 の「量の持ち物」でいえば、不等式検証型の手数は余裕を要り、場合分け型の手数は個数だけを要る。論文303 は証明が届かない一点を見た。本稿は届くまでの手数が何で決まるかを見たので、向きが違う。論文315 の接吻数も球充填も第二の型に属するので、「どの次元が特別か」の証明の重さは次元ごとの余裕に依る。正直に言えば──どちらの証明も再現していない。二つの型の性質を小さな見本で測っただけで、四色定理の可約性検査もケプラー予想の線形計画も実行していない。人が読めない証明を信じてよいかという問いにも入らず、定理証明支援系による形式化は本稿の二分類とは別の軸である。区間演算の実装も比べておらず、中心形式やアフィン算術を使えば膨らみは減る。箱の数は一つの実装での実測であって下界ではない。言えるのは、機械に任せたものが場合分けか不等式かで、手数が先に分かるかどうかが変わる、そこまでである。 作成にあたって:本稿の着想と内容は、著者自身の考察に基づくものです。文章の構成整理や英訳、数式の確認には AI(大規模言語モデル)の助力を得ました。最終的な内容の解釈や誤りがあれば、それらはすべて著者の責に帰します。お気づきの点があれば、ご教示いただければ幸いです。 キーワード:計算機による証明、四色定理、ケプラー予想、区間演算、形式証明。