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.
Scope (what is not claimed)
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 $\mathbf{77}$ to $\mathbf{1406877}$ by margin, showing non-termination at zero margin, and placing the separator on the existence of a margin.
1. Notation and the Question
Setting: the four colour theorem (1976) enumerated an unavoidable set of configurations and had a machine check that each was reducible. The Kepler conjecture (1998, formalised 2014) had a machine verify a great many inequalities.
Observation 1.1 both are called proofs by computer. Each contains more computation than a person can read——and yet what was handed to the machine differs.
Observation 1.2 one counts cases, the other checks magnitudes. A number of cases is finite and settled before starting——how finely a magnitude must be subdivided is not known at the outset.
Question: does that difference show in numbers?
2. The Case-Splitting Kind: Work Known in Advance
Computation 2.1: counting the cases for $k$ binary choices by explicit enumeration.
| binary choices $k$ | cases |
|---|---|
| $10$ | $\mathbf{1024}$ |
| $15$ | $\mathbf{32768}$ |
| $20$ | $\mathbf{1048576}$ |
Observation 2.2 the enumerated count matches $2^{k}$. A check that nothing was dropped——and the value follows from $k$ before a single case is examined.
Observation 2.3 so an estimate can be made. Time one case and multiply——one can say before starting how long the proof will take.
Observation 2.4 the hard part is whether the enumeration is complete. Whether an unavoidable set really is unavoidable is not for the machine to say——the machine takes the cases one at a time after the set is fixed, not the proof that the set is fixed.
3. The Inequality Kind: the Margin Decides
Computation 3.1: verifying $f(x,y)=x^{2}-2xy+y^{2}+\varepsilon>0$ over $[-1,1]^{2}$ with plain interval arithmetic, subdividing each box into four until the lower bound exceeds zero, and counting boxes.
| margin $\varepsilon$ | boxes used |
|---|---|
| $0.5$ | $\mathbf{77}$ |
| $0.1$ | $\mathbf{1197}$ |
| $0.01$ | $\mathbf{45541}$ |
| $0.001$ | $\mathbf{1406877}$ |
| $0$ | never settles |
Observation 3.2 this is the core. Going from $\mathbf{0.5}$ to $\mathbf{0.001}$ swells the count by $\mathbf{18271.1}$——formula and domain unchanged; only the margin moved.
Observation 3.3 at zero margin it never terminates. $f=(x-y)^{2}$ vanishes along $x=y$——there the lower bound cannot in principle exceed zero. The far side of the boundary.
Observation 3.4 part of the swelling comes from how the formula is written. Written as $(x-y)^{2}$ non-negativity is visible, while $x^{2}-2xy+y^{2}$ evaluated over separate intervals loses the constraint that $x$ and $y$ agree——this is the dependency problem of interval arithmetic, and rewriting reduces the count.
Observation 3.5 so the box count is not the difficulty of the problem. It depends on the expression——these numbers are measurements for plain intervals and this expression, not lower bounds.
Observation 3.6 the difference in kind survives. However it is written, zero margin never terminates——that a margin governs at all does not depend on the expression.
4. The Separator
Observation 4.1 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, no more and no less.
Observation 4.2 what can be said beforehand differs. The case kind can promise a running time——the inequality kind cannot until the margin is measured, and that margin is part of the very claim being proved.
Observation 4.3 separate roots under Paper 300. The inequality kind’s work carries a margin——the case kind’s carries only a count. One phrase, different belongings.
Observation 4.4 the orientation differs from Paper 303. There a formula returns a value while proof fails to reach that point——here the question is what decides the cost of reaching. Reaching and paying are different.
Observation 4.5 the subject of Paper 315 belongs to the second kind. Kissing numbers and sphere packing are settled by verifying inequalities——so the weight of proving which dimension is special depends on the margin in each dimension.
Observation 4.6 what is not said. Whether a proof no person can read may be believed is not discussed——and formal verification is a different axis from this division.
5. Roll Call and Closing
- $\mathbf{1048576}$ cases for twenty choices (Computation 2.1): known in advance.
- the count matches $2^{k}$ (Observation 2.2): nothing dropped.
- an estimate can be made (Observation 2.3): time by multiplication.
- completeness is not the machine’s (Observation 2.4): it takes the cases after.
- $\mathbf{77}$ boxes at margin $\mathbf{0.5}$ (Computation 3.1): $\mathbf{1406877}$ at $\mathbf{0.001}$.
- a factor of $\mathbf{18271.1}$ (Observation 3.2): the core.
- zero margin never settles (Observation 3.3): the far side.
- the dependency problem (Observation 3.4): the expression matters.
- box counts are not lower bounds (Observation 3.5): one implementation.
- the separator is the margin (Observation 4.1): absent in the case kind.
- different promises beforehand (Observation 4.2): how long it will take.
Closing: 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 $\mathbf{1024}$, $\mathbf{32768}$ and $\mathbf{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 $\mathbf{77}$ boxes at a margin of $\mathbf{0.5}$, $\mathbf{1197}$ at $\mathbf{0.1}$, $\mathbf{45541}$ at $\mathbf{0.01}$ and $\mathbf{1406877}$ at $\mathbf{0.001}$, a swelling of $\mathbf{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.
References
- Appel, K., & Haken, W. (1977). Every Planar Map Is Four Colorable. Illinois Journal of Mathematics.
- Hales, T. C. (2005). A Proof of the Kepler Conjecture. Annals of Mathematics.
- Hales, T. C., et al. (2017). A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi, 5, e2.
- Moore, R. E., Kearfott, R. B., & Cloud, M. J. (2009). Introduction to Interval Analysis. SIAM.
- Yamagishi, Y. (2026). The Equivalence Is a Theorem and the Thesis Is Not [Paper 260]. Zenodo. 10.5281/zenodo.22169292
- Yamagishi, Y. (2026). The Three Hundredth Census: Whether Two Things Share a Root Is Decidable [Paper 300]. Zenodo. 10.5281/zenodo.22171914
- Yamagishi, Y. (2026). The Formula Returns $4$, and at That One Point the Proof Does Not Reach [Paper 303]. Zenodo. 10.5281/zenodo.22172026
- Yamagishi, Y. (2026). Which Dimension Is Special Depends on the Question [Paper 315]. Zenodo. 10.5281/zenodo.22208139
Reference
Yamagishi, Y. (2026). Whether the Machine Was Given Cases or Inequalities Changes What Kind of Proof It Is [Paper 538]. YOI: https://www.yamagishiyuuki.com/yoi/538
DOI: 10.5281/zenodo.23014127
ORCID: 0009-0006-8587-3450
PDF (English) · PDF (Japanese) · Date proof of the English PDF (OpenTimestamps .ots) · SHA256SUMS
The record page for this paper (in Japanese, with the PDFs in each language and the date proof): YOI 538. This paper is a preprint and has not been peer reviewed.