E160 one-third upper bound - unreviewed candidate v0.2.0

This prerelease contains a proof manuscript and Lean 4 formalization of the
stated theorem chain for a candidate upper-bound improvement for Erdős Problem
160.

Result

Let H(N) be the least number of colours needed so that every nontrivial
four-term arithmetic progression in {1, ..., N} uses at least three colours.
The manuscript proves

H(N) <= N^(1/3 + o(1)).

More precisely, for every real epsilon > 0, it proves the eventual bound

H(N) <= N^(1/3 + epsilon).

This would improve the exponent log(3)/log(22) currently recorded on the
maintained Erdős Problems page. It is an upper-bound partial result and does
not solve Problem 160. The manuscript has not been peer reviewed, and no claim
of priority is made.

Contents

• the proof manuscript, TeX source, and compiled PDF;
• a Lean 4 formalization of the stated theorem chain and source-convention bridge;
• pinned Lean and mathlib versions with a one-command verification check;
• a theorem map, source-statement audit, and literature search.

Reproduce the formal artifact with:

bash scripts/check_release.sh

Tag v0.2.0-review-candidate points to root commit
42604f944f7367e13e9ae43072bded87930864df. Both the main-branch and tagged
GitHub Actions verification runs passed for this tree.

PDF SHA-256:

703081d94eebaceda64f4e90cc79aa0007994b874e44f66c46231c36984ab74d