Skip to content

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

Pre-release
Pre-release

Choose a tag to compare

View all tags
@ritabe-dev ritabe-dev released this 14 Jul 06:49
v0.2.1-review-candidate
fd426c9

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

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

Assets 3
Loading