cert-machine · report · every champion re-certified at build

The Mercer program: mu, lambda, and a 40-year bracket

Chowla asked how negative a sum of n cosines must dip; Newman asked how large the minimum modulus of an n-term 0/1 polynomial can stay. This program certifies both landscapes with exact arithmetic: exhaustive box sweeps for the extremal tables (every set decided, a conservation identity per box), an equality no enclosure could ever decide, and a bracket on mu(5) pushed fourteen rungs past the literature — on the lineage Campbell–Ferguson–Forcade 1983 → Goddard 1992 → Mercer 2019 → here.

tl;dr
  • The finding. mu(5) ≤ 1 + π/20 certified — fourteen rungs past the literature on a forty-year lineage — plus certified mu(n) box maxima for n = 10..17, each the first CERTIFICATE over its named box (a claim about the certificate, not about priority — §7), and M(0,1,2,6,9) = 1 EXACTLY, by Sturm. Behind all of it, the part that never gets counted: 4,991,170,760 sets decided exhaustively, deflated (§6).
  • The mechanism. Exhaustive box sweeps with a conservation identity per box; every exceptional tuple closed by one exact rational evaluation against an exact bar; the equality decided by a Sturm chain no floating enclosure could ever reach.
  • Check it. node instruments/trigmin/mercer6-battery.js — Mercer's own Tables 5–7 must reproduce exactly before any new rung counts.
sets decided exactly
4,991,170,760
DISTINCT sets across every mu and lambda box; each box carries a conservation identity that must close, and 129,999,910 re-decided sets are subtracted, not counted twice (§6)
mu rows certified
12
n = 9..17 at box 30, n = 10..12 at box 40 — all 12 champions re-certified during THIS build
lambda rows
14
n = 4..17; 9 reproduce the source lab (n=4 to the per-stage kill split), 5 have no source-lab counterpart, all deepened to M = 30
mu(5) bracket
1 ≤ mu(5) ≤ 1 + π/20
1.157080 — 16 certified rungs, 11,718 exceptional tuples closed by exact points
one exact equality
M(0,1,2,6,9) = 1
re-proved this build by deflation + Sturm — a tie no interval enclosure can decide
framing
CERTIFICATES
first certificates over NAMED boxes — never "first witness": Boyd 1986 remains unread, and prose stays inside what is proved
§0 · the ladder

The bracket on μ(5), rung by rung

Every rung is a separate exhaustive claim: at that m, every exceptional tuple is closed by one exact rational evaluation against an exact bar. The curve is what those claims add up to.

1.0 1.2 1.4 1.6 5 7 9 11 13 15 17 19 20 rung m — each one an exhaustive exact search closing every exceptional tuple at that m certified upper bound on mu(5) the literature stops here mu(5) ≥ 1 1.1571
16 certified rungs, m = 5..20, closing 11,718 exceptional tuples between them. The bound falls from 1.6283 to 1.1571 against a floor of exactly 1, so the bracket on μ(5) is now 0.1571 wide. The shaded region is the literature's reach; the 14 rungs to its right are this machine's, and each one is an exhaustion, not a sample.
§1 · the program

Two extremal landscapes, one discipline

For a set A of n positive integers, write f_A(θ) = Σ cos(aθ) and λ(n) for the smallest possible dip −min f_A over all n-sets (Chowla's cosine problem asks if λ(N) ≫ √N). For nonnegative exponents, write M(A) = min |Σ z^a| on the unit circle and mu(n) = sup M over n-term sets (Newman polynomials; mu is indexed by TERMS throughout). Both are extremal quantities over infinite families, so no finite computation evaluates them — what a machine CAN hold is exact: exhaustive sweeps over named boxes {exponents ≤ M}, every set decided by integer kills at roots of unity, exact dyadic Chebyshev kills, and full certification of survivors, with a per-box conservation identity that throws if a single set goes unaccounted. A mu row is a certified BOX MAXIMUM — a lower bound for the box, and the dips at high n are box crowding, not mathematics (box 30 → 40 raised mu(12)'s floor by +0.135). A lambda row is a certified upper bound on an infimum. Neither is ever printed as "the value".

§2 · the mu table

Certified floors, n = 9..17 — and what wider boxes taught

nboxcertified floor (rounds DOWN)champion Asets decidedprior witness ON FILE here
9≤ 30mu(9) ≥ 1.378187726393{0,1,2,3,9,12,19,23,27}5,852,925anchor — Boyd 1986 · inside this box, floor exceeded
10≤ 30mu(10) ≥ 1.323607352522{0,1,4,8,9,10,14,20,23,25}14,307,150none on file at this n
11≤ 30mu(11) ≥ 1.534618201728{0,1,2,7,8,10,12,21,24,25,28}30,045,015none on file at this n
12≤ 30mu(12) ≥ 1.553608237398{0,1,2,9,12,13,14,16,18,19,22,24}54,627,300none on file at this n
13≤ 30mu(13) ≥ 1.899892237678{0,1,2,4,6,7,8,13,16,17,20,25,28}86,493,225none on file at this n
14≤ 30mu(14) ≥ 1.724078989317{0,2,3,4,5,7,10,12,13,14,16,20,21,25}119,759,850none on file at this n
15≤ 30mu(15) ≥ 1.664681927869{0,1,2,3,4,5,9,10,14,17,20,22,24,26,28}145,422,675none on file at this n
16≤ 30mu(16) ≥ 1.721441131519{0,1,2,3,5,6,7,8,11,14,15,16,18,23,25,27}155,117,520none on file at this n
17≤ 30mu(17) ≥ 1.676123906933{0,1,2,3,8,11,13,14,16,17,18,20,22,23,26,27,30}145,422,675adopted — HJ minus {16,22}; only one of 171 subsets clearing bar(17) · OUTSIDE this box, floor exceeded
10≤ 40mu(10) ≥ 1.420064490311{0,1,4,7,8,13,22,24,32,34}273,438,880box 30 maximum — this lab · certs/mu-table.json · inside this box, floor exceeded
11≤ 40mu(11) ≥ 1.546098106216{0,2,4,12,19,20,24,25,27,30,33}847,660,528box 30 maximum — this lab · certs/mu-table.json · inside this box, floor exceeded
12≤ 40mu(12) ≥ 1.688969021141{0,1,11,12,16,18,19,21,24,25,27,33}2,311,801,440box 30 maximum — this lab · certs/mu-table.json · inside this box, floor exceeded

n = 9 validates cross-lab: the six-survivor, two-orbit structure of the source lab's record reproduces with the published witness floor to the last digit — Boyd's anchor witness {0,1,2,3,4,7,8,10,12} comes back as a survivor of this sweep, and the box maximum stands above it. For n = 10..17 this lab holds no earlier certificate at all; whether any printed table holds those rows is precisely the question Boyd 1986 would settle, and it is unread (§7). The box-extension lesson is three for three: at n ≥ 10 the box-30 maxima were crowding artifacts, and box 40 lifted every floor it touched — mu(10) past even mu(9)'s, killing the "dip" reading. Every champion above was re-certified during this build; a champion that fails to reproduce its floor refuses the page.

where that last column comes from

The mu certificates carry NO provenance field — unlike the lambda rows, which record sourceLab and reproduces as structure, certs/mu-table.json and certs/mu-table-40.json have neither on any row, so "n = 9 is a reproduction, n = 10..17 are not" lived only in prose. The column is therefore sourced from instruments/trigmin/envelope.js, the registry that splits ANCHORS (literature and the source lab, each with a named src) from ADOPTED (what this lab certified and promoted). Its incumbent witness is re-certified during this build and compared against the champion at the strict end, and every box-30 champion must BE the envelope's adopted row for its n or the page refuses. Read it as "what this lab had on file before the sweep" — 7 of the 12 rows had nothing — never as a statement about the printed record. The n = 17 incumbent reaches exponent 38 and so was never inside box 30 at all; the row still names it, because a comparison the sweep could not make is worth showing.

§3 · the lambda table

n = 4..17, deepened to M = 30

nλ(n) ≤ (rounds UP)witness Abox Mprovenance (from the record's own field)
41.519557881643{1,2,3,4}20reproduces source lab
51.627460664467{1,2,4,5,6}60reproduces source lab
61.591832329324{1,2,4,6,7,8}50reproduces source lab
71.893455418993{1,2,3,5,6,7,8}30reproduces source lab
81.956787693633{2,3,4,5,7,8,10,12}30reproduces source lab
92.069282587092{2,3,4,5,7,9,10,12,14}30reproduces source lab — via M = 25, optimiser CONFIRMED at M = 30
102.057447274609{1,2,3,5,6,7,8,10,11,13}30reproduces source lab — via M = 25, optimiser CONFIRMED at M = 30
112.102381279243{1,2,3,4,5,6,8,9,10,11,14}30reproduces source lab — via M = 25, optimiser CONFIRMED at M = 30
122.213895922406{1,2,3,4,5,6,7,8,9,10,11,15}30reproduces source lab — via M = 25, optimiser CONFIRMED at M = 30
132.318232650153{1,2,3,4,5,6,7,9,10,11,12,13,16}30no source-lab counterpart
142.320690691855{1,3,4,5,9,10,12,13,14,17,22,23,26,27}30no source-lab counterpart
152.418912126896{1,2,3,4,6,7,8,9,10,11,12,14,18,20,21}30no source-lab counterpart
162.454832753028{1,2,3,4,5,6,7,8,10,11,13,14,15,16,17,21}30no source-lab counterpart
172.564897120546{1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,19,22}30no source-lab counterpart

The 9 source-lab rows reproduce exactly — n = 4 down to the per-stage kill split (2818 + 2022 + 0 + 5), with proved closed forms COMPUTED, never remembered (λ(2) = 9/8 exact; λ(3) = (17+7√7)/27 via certified square root). Rows n = 13, 14, 15, 16, 17 have no counterpart in the source lab's record and none in any table this lab has read. The last column is not prose: it is the record's own sourceLab + reproduces fields, and where the displayed M = 30 row does not carry them the chain is FOLLOWED — the M = 25 row that does carry them, plus that deepening's own verdict that the optimiser did not move — never assumed. A caution priced into every row: these are upper bounds on an infimum, exact only within their named boxes, and rows at different n order nothing.

What the M = 30 deepening actually returned. 9 rows were re-decided in the wider box after a settled M = 25 answer. 1 improved — λ(14) fell, the wider box finding {1,3,4,5,9,10,12,13,14,17,22,23,26,27}, reaching exponent 27, structurally unlike the near-interval shallow-box optimiser. The other 8 returned the incumbent: at n = 9, 10, 11, 12, 13, 15, 16, 17 the M = 25 optimiser is CONFIRMED as the M = 30 optimiser. That verdict cost 725,532,585 sets decided exactly, 698,969,540 of them never inside a certified box before, and the collective answer is nothing beat the incumbent. It is a proved negative over 725,532,585 sets, not a search that came up empty — §6 counts it as such.

§4 · the bracket

mu(5) ≤ 1 + π/20, 16 certified rungs

Mercer proved mu(5) ≤ 1 + π/5 and SKETCHED 1 + π/6, reducing the hard cases to a finite search over fractions with bounded denominators plus per-tuple checks — "a finite search (aided by computer)" and "one can verify". This lab certified both computer-aided components at GENERAL m: the search runs in exact rationals (m = 5 reproduces his Table 5's unique quadruple; m = 6 his Tables 6 and 7, and the source lab's record row for row), and every exceptional tuple is closed by ONE exact rational evaluation of |f|² against the exact bar (1 + πLo/m)². The ladder now runs m = 5..20 — 11,718 tuples across 16 rungs, every one certified — ending at mu(5) ≤ 1.157080. With §5's witness this brackets 1 ≤ mu(5) ≤ 1 + π/20. Component (i), the reduction, is consumed from Mercer 2019 (his Lemma 6.2; general m stated on his p. 16) the way Krawczyk's theorem is consumed in validated numerics — named in the certificate, checked at its calibrations.

§5 · the equality

M(0,1,2,6,9) = 1 — exactly, by Sturm

Mercer observed M(0,1,2,6,9) = 1 and suspected mu(5) = 1. An enclosure can never decide that tie — the minimum SITS on the bar. The certificate that can: |f|² − 1 factors as (y+1)·H(y) exactly (y = cos θ), H(−1) = 92 > 0, and a Sturm chain counts ZERO roots of H in [−1, 1] — so the minimum is EXACTLY 1, attained at z = −1 and nowhere else. Re-proved during this build in under a millisecond. The same tuple reappears in §4's ladder from m = 10 as the reversal (3,7,8,9), and its case closes with g(−1) = 1 ≤ bar at every rung — the two results agreeing is not a coincidence; it is the same exact arithmetic.

§6 · the negatives, by kind

What has been decided exhaustively — and why there is no single number

mu sets · box 40
3,432,900,848
unit: SETS. n = 10..12, every set {0} ∪ (n−1 exponents ≤ 40), each decided against an exact bar
mu sets · box 30
757,048,335
unit: SETS. n = 9..17; 98,979,465 also lie inside box 40 and are never counted twice on this page
lambda sets
900,201,042
unit: SETS. Deepest box per n over n = 4..17; the 23 recorded rows sum to 931,221,487 only by re-counting shallower boxes
Hénon boxes
1,972,325,286
unit: BOXES — a different object entirely. p = 13, 14, 15, 16, plane exhausted, 3,844 points found, 0 unmatched on recheck
closed forms tested
54,629,173
unit: CANDIDATE CLOSED FORMS — a third object. 54,628,296 refuted against certified enclosures (54,628,275 in double, 21 exactly in BigInt), 0 surviving
the total
NOT ONE NUMBER
sets, boxes and closed forms do not add. A headline that summed them would be exactly the inflated number this machine exists to refuse
kindunitdecided exhaustivelywhat ONE decision saysrecord read at build
Newman box sweep, box 40 · n = 10..12sets3,432,900,848this 0/1 polynomial's min |f| on the circle is below the bar — or it survives and is certifiedcerts/mu-table-40.json
Newman box sweep, box 30 · n = 9..17sets757,048,335the same decision in the narrower box; 98,979,465 of these sets lie inside box 40 too and are counted ONCEcerts/mu-table.json
Chowla box sweep · n = 4..17sets900,201,042this set's certified dip does not beat the bar — deepest box per n; the 31,020,445 sets re-decided at a shallower M are not counted againcerts/lambda-table.json
Hénon periodic-point census · p = 13..16boxes1,972,325,286no period-p point lies in this box — or exactly one does, certified; the plane is exhausted and the recheck leaves 0 unmatchedcerts/census-high-periods.json
closed-form hunt · 95 certified enclosurescandidate closed forms54,629,173the certified value provably lies OUTSIDE this form — 54,628,296 refuted, 877 already on the OEIS record, 0 survivingledger.json
one headline figureREFUSEDthree different objects; the only sum this page makes is 4,090,969,718 + 900,201,042 = 4,991,170,760 DISTINCT sets, because mu sets and lambda sets are the same unit and disjoint populationsthis page

Every number above is a NEGATIVE at scale. A box sweep publishes one champion and quietly decides everything else against it; a census publishes a point count and quietly proves the rest of the plane empty; the closed-form hunt publishes zero discoveries and refutes 54,628,296 forms exactly. Those refusals are the work, and each one is proved — not a truncated-decimal miss, not a search that timed out. They are listed here by kind and never added, because the units differ; the counting rule that forbids the sum is the same rule that makes each row worth printing.

The single largest one is the quietest. 725,532,585 sets were re-decided when the lambda table was deepened from M = 25 to M = 30 at n = 9, 10, 11, 12, 13, 15, 16, 17 — 698,969,540 of them never inside a certified box before — and the collective answer was the incumbent still stands: at all 8 of those n the M = 25 optimiser is CONFIRMED as the M = 30 optimiser. That is a proved negative over 725,532,585 sets, not a failed search. Exactly 1 of the 9 deepenings moved a bound (λ(14), on 145,422,675 sets), and that one improvement is what the page used to report — the 725,532,585 sets behind the other answer were a single subordinate clause.

the deflation, stated

A naive row sum over the mu tables gives 4,189,949,183 sets; box 30 sits inside box 40 at n = 10..12, so 98,979,465 sets would be counted twice and the honest figure is 4,090,969,718. A naive row sum over the 23 recorded lambda boxes gives 931,221,487; each M = 25 box sits inside its M = 30 successor, so 31,020,445 sets would be counted twice and the honest figure is 900,201,042. Re-deciding a set in a wider box is real work and a real check — it is simply not a second set. Every count on this page is the right-hand side of a conservation identity that the build re-adds row by row and refuses if it does not close.

§7 · honesty

What "first certificate" claims, and what it does not

Boyd's 1986 survey of large Newman polynomials (LMS Lecture Notes 109) is not yet read first-party in this lab — the volume is access-restricted and an ILL request is the operator's open action. Until those bytes are read, no sentence here claims a "first witness" or priority over the printed record: every row is a FIRST CERTIFICATE — an exhaustion over a named box with a conservation identity, re-checkable by the repository's batteries on every run — which is a claim about the certificate, not about history. Three secondary sources support the framing without the paper; the paper decides nothing computational either way. Where this program's own instruments found their bugs, controls found them: the wrong-endpoint bar refused BY NAME, the fabricated-decimal battery catch, the dilated-champion tie-break — none by reading code.

The same discipline governs the wording. No row on this page is called a first in the historical record, and none is called the only such row in existence — both would be claims about what has been printed, and this lab has not read what has been printed. What §2's last column reports is what this lab HAD ON FILE at that n before the sweep ran — 7 of 12 mu rows had nothing on file — which is a fact about instruments/trigmin/envelope.js, a file anyone can open, not a fact about what has been printed. And §6 refuses the other tempting overstatement: the negatives are published by kind, never summed across units, and deflated within a kind before they are published at all.