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, and no independent re-verification has run yet. 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 human read of the write-up. 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.