Mercer proved the first two exact values of Chowla's cosine dip in 2019 and conjectured the rest. This machine proved the third, and here the fourth: λ(5) = −L(1,2,4,5,6), an algebraic number of degree exactly five. One consequence needs nothing further — λ(6) < λ(5), so the sequence that had been climbing turns down at six.
A machine-derived proof, published for scrutiny: not peer-reviewed. An independent audit has walked the theorem, the first level of the reduction and the obstruction — but NOT the interior of the eight closure trees, which λ(4)'s audit does walk for λ(4). Every derivation below is re-executed at this page's own build in exact rational arithmetic, and the build refuses to ship if any step deviates; the algebra is calibrated first against two published closed forms it must reproduce. The mathematics is restated here 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, and Chowla asked how shallow it can be kept. λ(n) is the infimum over frequency sets of −min — the shallowest dip any n-term sum can manage. The asymptotic side is Erdős problem #510; the FINITE side is the exact values, and until 2026 it had 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), λ(5) = −L(1,2,4,5,6) and λ(6) = −L(1,2,4,6,7,8), and left a §5 strategy. This lab executed that strategy for λ(4) (the proof page). λ(5) is the next value, and the first whose optimiser is not an initial segment: {1,2,4,5,6} skips 3.
Why the skip matters. An optimiser that is not an initial segment is what makes the sequence able to turn: Mercer conjectured λ(6) < λ(5), which would be the first non-monotonicity. §3 shows that consequence is already available.
Substituting c = cos θ, the sum is 32c⁶ + 16c⁵ − 40c⁴ − 20c³ + 12c² + 6c − 1. Its endpoint values are the exact integers P(1) = 5 and P(−1) = 1, both far above the minimum, so the minimum is attained in the open interval and is therefore a CRITICAL value. The critical values of P are exactly the roots of the resultant R(y) = Res_c(P′(c), P(c) − y), an integer polynomial computed here by a fraction-free Sylvester determinant. Sturm's theorem counts exactly one root of R inside the certified enclosure, so that root is the minimum:
The quintic is irreducible over ℚ — it stays degree 5 and is irreducible modulo 7, which is enough — so it IS the minimal polynomial and λ(5) is an algebraic number of degree exactly five. So far as this lab has read, that polynomial has not been printed anywhere, as was the case for λ(4)'s cubic; Mercer states the conjecture, and no follow-up on the finite front has been located in seven years. The same instrument, run first as calibration, re-derives Mercer's published λ(3) = (17+7√7)/27 as the root of 27λ² − 34λ − 2 and this lab's 512λ³ − 1227λ² + 600λ + 125 for λ(4), before it is trusted on λ(5).
For every set of five distinct positive integers, the sum cos aθ + … + cos eθ reaches −λ(5) or deeper at some θ. Equality holds for {1,2,4,5,6} and its dilations, and — by the strictness of every family closure — for no other set. What is NOT decided here: whether λ(5) can be written in radicals. That is the Galois group of the quintic, and nothing in this campaign computes it.
λ(n) is an INFIMUM over n-element sets, so any single set is an upper bound: {1,2,4,6,7,8} gives λ(6) ≤ −L(1,2,4,6,7,8) ≤ 1.5918323293239, certified by the same minimum instrument. With λ(5) = 1.6274606644666 now proved, the comparison is immediate:
So the sequence λ(2) < λ(3) < λ(4) < λ(5) does not continue: λ(6) < λ(5). Mercer conjectured this non-monotonicity and it follows from λ(5) alone plus one exhibited set — the λ(6) campaign is not needed for it. What the campaign IS needed for is the stronger statement: that λ(6) EQUALS −L(1,2,4,6,7,8). Nine of its ten families are closed in the same record; the tenth is still computing, and until it lands λ(6) has an upper bound here and no exact value.
A bound in one direction and an exact value in the other is enough to order two numbers, and not enough to state either as known. λ(6) ≤ 1.5918323293239 is unconditional; λ(6) = 1.5918323293239 is still a conjecture on this site.
The §5 move, at n = 5. On the equispaced set where eθ ≡ π, take the single nonnegative weight 2(1 − cos dθ)² against g₀ = 2/3. At that g₀ the atom lands base EXACTLY 0 — the (1−cos) atoms Mercer used die at the heavier constant, and the squared atom is precisely neutral — and the dip is −5/3, strictly below −λ(5). A single atom on the second-largest member also minimises the exception count: eight positive families here, where a four-atom weight gives thirty-two. The engine derives the conditions symbolically; they are OUTPUT, never input, and each one is checked inhabited by an explicit integer set.
| condition | effect (delta) | verdict | example set |
|---|---|---|---|
| 2d = a+e | -1/2 | closes itself | {1,2,3,4,7} |
| 2d = b+e | -1/2 | closes itself | {1,2,3,4,6} |
| 2d = c+e | -1/2 | closes itself | {1,2,3,4,5} |
| 2d = e | 4/3 | needs its own proof | {1,2,3,4,8} |
| 3d = 2e | 1/2 | needs its own proof | {1,2,3,4,6} |
| 3d = e | -1/2 | closes itself | {1,2,3,4,12} |
| a+2d = 2e | 1/2 | needs its own proof | {2,3,4,5,6} |
| a+2d = e | -1/2 | closes itself | {1,2,3,4,9} |
| a+d = e | 2 | needs its own proof | {1,2,3,4,5} |
| b+2d = 2e | 1/2 | needs its own proof | {1,2,3,4,5} |
| b+2d = e | -1/2 | closes itself | {1,2,3,4,10} |
| b+d = e | 2 | needs its own proof | {1,2,3,4,6} |
| c+2d = 2e | 1/2 | needs its own proof | {1,2,4,5,7} |
| c+2d = e | -1/2 | closes itself | {1,2,3,4,11} |
| c+d = e | 2 | needs its own proof | {1,2,3,4,7} |
The built-in consistency check: {1,2,4,5,6} activates 3 conditions — 2d = c+e, a+d = e, b+2d = 2e — whose deltas sum to 2, positive, 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 | delta | root shape | dot theorems | closures | finite sets | equality handling |
|---|---|---|---|---|---|---|
| 2d = e | 4/3 | single cone | 4 | 6 | 153 | strict |
| 3d = 2e | 1/2 | split into 17 root cones | 28 | 10 | 188 | strict |
| a+2d = 2e | 1/2 | single cone | 11 | 28 | 570 | strict |
| a+d = e | 2 | single cone | 7 | 12 | 323 | 4 × extremizer walled |
| b+2d = 2e | 1/2 | split into 3 root cones | 9 | 12 | 246 | 2 × extremizer walled |
| b+d = e | 2 | single cone | 2 | 1 | 9 | strict |
| c+2d = 2e | 1/2 | split into 7 root cones | 12 | 7 | 236 | strict |
| c+d = e | 2 | single cone | 1 | 0 | 0 | strict |
Each family repeats the move one level down on its 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 subfamilies; those close by anchored estimates whose thresholds are derived; what remains below every threshold is a finite list, decided set by set by the certified minimum instrument. In total 74 dot theorems, 76 anchored closures and 1,725 finite sets, with 15,330 coverage points checked. The extremizer is walled as the definitional witness on exactly 6 leaves, and only inside the 2 families whose condition {1,2,4,5,6} actually satisfies (a+d = e on 4, b+2d = 2e on 2); a wall anywhere else would be a set skipped without cause, and the build refuses it. Every neighbour of the extremizer is certified strictly below the target.
The family a+d = e contains the sub-cone b+c = a+d = e — a DOUBLE sum system, and {1,2,4,5,6} is one of its points (2+4 = 1+5 = 6). On the equispaced set where eθ ≡ π the members pair into complements: (a,d) and (b,c) both sum to e, and cos(kπ) + cos((k−1)π) = 0 identically, so every match a weight can earn is annihilated by its complement. The base is w₀·g₀ > 0 for EVERY nonnegative weight — the argument cannot start. This is not a failure of search: it is a structural obstruction, and the battery proves it fresh at every run by requiring all four classical atoms, at both anchors, to refuse.
The way through is to change the anchor and the weight together. On S(e, 2π/3) the wrap sum at k ≡ 1 (mod 3) is −1 with no cancellation, and a Fejér–Riesz comb along the frequency classes m+e — the squared-modulus atom |(1 + z_a)(5 + 7z_b + 5z_b²)|² with z_m = e^{i(m+e)θ} — lands base -8 at g₀ = 7/6, with dip -5/3 still clearing the target. Its 6 positive conditions are ordinary two-parameter cones, and the family closes from there. The comb atom is additive to the inner-product calculus: the λ(4) engine is untouched by it, and its battery stays green.
If some classical atom ever DID close the double-sum core, the comb would be unnecessary and this section would be a story rather than a theorem. So the check runs the other way: eight classical attempts must all refuse, at every build of this page and every run of the battery. The moment one succeeds, the page stops building.
Checked, at every build of this page: the target enclosure; the minimal polynomial end to end (interior minimum from exact endpoint values, resultant, exact sign change, Sturm count 1, irreducibility) AFTER the same instrument reproduces the published λ(3) and λ(4) closed forms; the generic case with its 15/8 exception structure and the extremizer escaping; the double-sum-core theorem and the eight classical refusals that justify its comb weight; the record walk — eight families CLOSED, every finite part decided, only the extremizer skipped, 6 walls and each one inside a family the extremizer belongs to; and a sample of finite certificates.
Checked, at every test run: instruments/lambda56/battery.js — the λ(4) calibration that must pass before any λ(5) claim is computed, the record walk that makes a rotted record refuse rather than linger, the audit record pinned against this target, and red controls that must fire: a classical atom closing the double-sum core, a comb at too light a constant, an unregistered condition, a wrong sub-cone, a skip list naming an absent set, a quintic off by one coefficient, a reducible polynomial called irreducible.
Independently audited, at this box: a second walk sharing no code with the symbolic engine — inner products by direct trigonometric summation, condition membership by plain integer arithmetic on the record's condition vectors, sets re-certified from scratch — covered every gcd-reduced 5-set with largest element ≤ 30: 139,246 sets, 0 refuters of the theorem, 3,481 screened sets re-certified exactly to audit the screen itself. It also cross-validates the engine's whole symbolic layer: the model says an inner product is its base plus the deltas of the active conditions, and direct summation agrees at every set in the box to 5.3e-14. The obstruction is confirmed by its mechanism rather than by search — on all 798 double-sum-core points in the box the cosines cancel identically on S(e, π) (worst residual 8.1e-14), so no nonnegative weight can start, and the comb closes every core point where no positive condition is active. Record: certs/lambda5-audit.json.
Not yet, and these are the gaps: the audit above walks the THEOREM, the first level of the reduction and the obstruction — it does NOT walk the interior of the eight closure trees, the subfamily cones, the derived thresholds or the finite parts inside them. λ(4)'s audit does walk those for λ(4); no equivalent exists here yet. There is also no prose write-up, no peer review and no human read. Until those exist 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/lambda56-campaign.json; the statement and strategy are Mercer's, and his paper is the first thing to read: arXiv:1709.06612.
Related here: λ(4), settled — the third exact value, with its audit; and the Mercer program for the rest of the finite front.