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

This prerelease hardens the review artifact for the candidate upper-bound improvement for Erdős Problem 160. No Lean theorem, assumption, constant, or proof was changed.

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 gives the candidate bound

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

and the Lean development checks the stated theorem chain, including the eventual form H(N) <= N^(1/3 + epsilon) for every real epsilon > 0. 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.

Changes since v0.2.0

• clarifies that the total Lean definition has the unused endpoint value siteH 0 = 0, while all stated bounds concern positive N;
• pins Tectonic 0.16.9, bundle v33, and the paper build timestamp, and checks a byte-identical PDF rebuild on Ubuntu 24.04;
• checks the exact names and count of the nine audited theorem endpoints;
• scans all first-party Lean sources for placeholders and conventional standalone primitive declarations;
• adds a one-file release manifest and verifies the remote tag, tagged PDF, and GitHub Release asset together.

Verification

• commit: fd426c9003c2acbae3e668c462b8fed73c41fb1c;
• main verification: https://github.com/ritabe-dev/ErdosProblem160-OneThirdUpper/actions/runs/29312298069;
• tag verification: https://github.com/ritabe-dev/ErdosProblem160-OneThirdUpper/actions/runs/29312311625;
• PDF SHA-256: acac777933a2f69a38e05844450be788bb37419354fd45b77a0cbb2f2aaee65a.

The manuscript has not been peer reviewed. No claim of priority or independently established novelty is made.

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