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

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".

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.

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.

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.