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

論文538 の記録のページです。住所（YOI）は https://www.yamagishiyuuki.com/yoi/538 で、論文の本文は下の PDF にあります。ファイルは自分で用意した置き場所（https://yamagishi.sakuraweb.com）に置き、日付の証拠（.ots）を添えています。Zenodo でも公開しています（DOI：10.5281/zenodo.23014127）。

本文はサイトの記事でも読めます：【論文538】計算機に任せたのが場合分けか不等式かで、証明の性質が変わる

@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}
}

日付の証拠（OpenTimestamps）

2026年10月1日に、2 本の PDF の指紋（SHA-256）をまとめて OpenTimestamps に送り、ビットコインのブロック 969428・969440・969461 に記録されました（2026年10月01日 17:42（日本時間））。この .ots があれば、PDF がその時点で存在したことを、このサイトや運営者を信用しなくても、誰でも確かめられます。

書誌

要旨

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

第一に、場合分け型では手数が先に分かる。二値 $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節）。

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

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.

First, in the case-splitting kind the work is known in advance、ten binary choices give $\mathbf{1024}$ cases, fifteen give $\mathbf{32768}$ and twenty give $\mathbf{1048576}$, all countable before starting (Section 2).

Second, and this is the core.In the inequality kind the margin decides、the same formula takes $\mathbf{77}$ boxes at a margin of $\mathbf{0.5}$ and $\mathbf{1406877}$ at $\mathbf{0.001}$, a factor of $\mathbf{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).

Keywords: computer-assisted proof, four colour theorem, Kepler conjecture, interval arithmetic, formal proof

版の記録

ここの PDF（倉庫の v1）は第1版（2026年9月）の原稿から作りました。ファイルは版ごとに分けて置いています（/yoi/538/v1/ の下）。中身を直すときは、このファイルを書き換えず、新しい版を足します（住所 https://www.yamagishiyuuki.com/yoi/538 はいつも最新の版を指します）。Zenodo の記録とは、Zenodo に上げる前の改訂のぶんだけ違うことがあります。

YOI の一覧へ