λ(4), settled
In 2019 Idris Mercer proved the first two exact values of Chowla's cosine dip, conjectured the third, wrote "the current author is unaware of how to evaluate λ(4)", and left a strategy. This machine executed the strategy and finished it: every one of the nine remaining families is closed, and λ(4) = −L(1,2,3,4).
A machine-derived proof, published for scrutiny: not peer-reviewed. One independent re-verification has run: an outside audit with no shared code (rainrzk, 2026-09-30, AI-assisted by its own account) redid the computational steps with its own code, re-certified every finite case and checked Lemmas A–F by hand — the same verdict; three documentation findings in the write-up, folded in (commit 1c248ca); see §6. No formal proof exists. Every derivation below is re-executed at this page's own build from exact rational arithmetic, and the build refuses to ship if any step deviates. The mathematics the proof rests on — three elementary lemmas and one bookkeeping calculus — is restated on this page so it can be checked without reading code.
A length-n cosine sum is cos(a₁θ) + … + cos(aₙθ) with distinct positive integer frequencies. Its minimum is always negative; Chowla asked how shallow it can be kept. −λ(n) is the supremum of that minimum over all frequency sets — the shallowest possible dip. The asymptotic side of this question is Erdős problem #510 and has been busy (a 2025 preprint gives the first polynomial lower bound). The FINITE side — exact values of λ(n) — had exactly two entries.
Mercer (arXiv:1709.06612, INTEGERS 19 (2019) #A4) proved λ(2) = 9/8 and λ(3) = (17+7√7)/27, conjectured λ(4) = −L(1,2,3,4) ≈ 1.5195578816428 with extremal set {1,2,3,4}, and published — in his §5 — a possible route: reduce the problem to finitely many lower-dimensional families. He wrote that he was unaware how to evaluate λ(4), and in seven years no follow-up appeared on the finite front (the paper's one citation is on the asymptotic side).
The route works. This page is the record of executing it to the end.
Substituting c = cos θ, the sum is 8c⁴ + 4c³ − 6c² − 2c and its minimum over [−1,1] is an algebraic number: the exact resultant against the derivative gives the minimal cubic, so
Both facts are re-proved at this build: the enclosure by the certified minimum instrument (BigInt Sturm isolation + interval Newton), and the cubic by exact rational evaluation at the enclosure endpoints — it changes sign inside. So far as this lab has read, the closed form had not been printed anywhere.
For every set {a,b,c,d} of four distinct positive integers, the sum cos aθ + cos bθ + cos cθ + cos dθ reaches −λ(4) or deeper at some θ. Equality holds for {1,2,3,4} and its dilations, and — by the strictness of every family closure — for no other set.
Mercer's §5 weight argument: on the equispaced set where dθ ≡ π, the nonnegative weight (1−cos aθ) + (1−cos bθ) + 2(1−cos cθ)² forces cos aθ + cos bθ + cos cθ ≤ −3/5 somewhere — so the full sum dips to −8/5, strictly below −λ(4) — UNLESS the largest element d satisfies one of fourteen linear conditions. The engine derives the list symbolically (the exceptions are output, never input), and it matches his hand-written fourteen exactly. It also computes what the prose could not see: each condition's exact effect on the argument. Five of the fourteen make it stronger, not weaker — those families close with no further work.
| condition on d | effect (delta) | verdict | example set |
|---|---|---|---|
| 2a = d | 1/2 | needs its own proof | {3,4,5,6} |
| 2b = d | 1/2 | needs its own proof | {1,2,3,4} |
| 2c = a+d | -1/2 | closes itself | {1,2,3,5} |
| 2c = b+d | -1/2 | closes itself | {1,2,3,4} |
| 2c = d | 7/5 | needs its own proof | {1,2,3,6} |
| 3c = 2d | 1/2 | needs its own proof | {1,2,4,6} |
| 3c = d | -1/2 | closes itself | {1,2,3,9} |
| a+2c = 2d | 1/2 | needs its own proof | {2,3,4,5} |
| a+2c = d | -1/2 | closes itself | {1,2,3,7} |
| a+b = d | 1 | needs its own proof | {2,3,4,5} |
| a+c = d | 5/2 | needs its own proof | {1,2,3,4} |
| b+2c = 2d | 1/2 | needs its own proof | {1,2,3,4} |
| b+2c = d | -1/2 | closes itself | {1,2,3,8} |
| b+c = d | 5/2 | needs its own proof | {1,2,3,5} |
The built-in consistency check: {1,2,3,4} activates four conditions whose deltas sum to +3, so the generic argument correctly CANNOT close the extremizer — an engine that closed it would be proving a false statement, and the battery keeps a red control on exactly that.
| family | route | finite sets | equality handling |
|---|---|---|---|
| d = 2c | second-level weight on S(c, 2π/3); 4 subfamilies, one needing a two-closure union | 231 | strict |
| d = 2a | second-level weight on S(a, 2π/3); every exception negative — closed generically | 0 | strict |
| d = b+c | weight 2(1−cos a)² on S(b+c, π); one exception, negative — closed generically | 0 | strict |
| d = a+b | weight on S(a+b, π); one subfamily — closed on the half-frequency set S(γ, π/2) | 8 | strict |
| d = a+c | EQUALITY family; the AP subfamily {b−t, b, b+t, 2b} closes by a reflection estimate (companion anchor 0) | 21 | extremizer walled off |
| 2d = 2c+a | a = 2t substitution; four subfamilies, one triangulated into three cones | 215 | strict |
| d = 2b | EQUALITY family; triangulates on a vs c−b into three cones; six subfamilies, 1090-set finite box | 1361 | extremizer walled off |
| 2d = 2c+b | EQUALITY family; triangulates on a vs β; two sub-conditions ARE other closed families (delegated) | 368 | extremizer walled off |
| 2d = 3c | c = 2γ substitution; seven cones on S(γ, π/3); two closures ride the π/6 anchor | 27 | strict |
Each family repeats the §5 move one level down, on the family's own cone: a weight and an equispaced set whose symbolic inner product is an exact rational, piecewise over collision conditions the engine DISCOVERS; positive-delta conditions spawn 2-parameter subfamilies; those close by anchored estimates whose thresholds are derived, and what remains below the thresholds is a finite list, decided set by set by the certified minimum instrument. The three families containing {1,2,3,4} confine it to a single cone or ray, where the finite decision skips exactly that one set — the definitional witness, where equality holds — and certifies every neighbour strictly below the target.
Checked, at every build: the target enclosure and the cubic; the generic case with its 14/9 exception structure; the campaign record (nine families CLOSED, every finite part fully decided, only the extremizer skipped); a sample of finite certificates. Checked, at every test run: the engine re-derives Mercer's published λ(2) and λ(3) proofs end to end — exception families discovered, his thresholds (a ≥ 3, b ≥ 3, b ≥ 33) derived — before it is allowed to touch λ(4); 8 red controls must fire.
Independently walked: an adversarial audit sharing no code with the engine — inner products by direct trigonometric summation, membership by plain arithmetic, thresholds read from the record, finite-clause sets re-certified fresh — covered every gcd-reduced 4-set with max element ≤ 30: 25819 sets, every one reached by an explicit clause of the proof, 423 fresh certificates, zero holes; the full sweep found zero refuters. The prose write-up is paper/lambda4-proof.md (draft v0.9, every constant interpolated from the record).
Not yet: peer review, and a formal proof — the outside audit checked Lemmas A–F by hand, its stated caveat, and a Lean formalization is where that caveat would close. Until those happen the honest status of the theorem-level sentence is exactly what the scope line at the top of this page says. The full machine record is certs/lambda4-campaign.json; the statement and strategy are Mercer's, and the paper is the first thing to read: arXiv:1709.06612.
Cite this work: the repository snapshot carrying the proof, the record, the audit and the write-up is archived at doi:10.5281/zenodo.22225861 (all versions: doi:10.5281/zenodo.22225860); the release tag is lambda4-v1.0.1. Independent audit (2026-09-30): an outside audit with no shared code, AI-assisted by its own account, rainrzk/erdos510-lambda4-audit (posted on teorth/erdosproblems #392; the thread is pinned in corpus/sources/lambda4), re-derived the cubic, the 14 generic collisions and the nine families from the write-up, re-certified all finite cases with interval arithmetic, and swept every gcd-reduced 4-set with largest element ≤ 80 as a proof-independent control ({1,2,3,4} deepest; the nearest rival {2,3,4,6} at about −1.774). Its three documentation findings are folded into the write-up: the extremizer is skipped six times (once per finite part it lies on), the cone listing of family 2d = 2c+b now includes cone ii, and the cubic has three real roots, λ(4) the largest.