AI-Assisted Discovery of Convex Relaxations via Dual Agents

# AI-Assisted Discovery of Convex Relaxations via Dual Agents
Source: [https://arxiv.org/html/2606.31182](https://arxiv.org/html/2606.31182)
###### Abstract

Recent work shows that LLM agents can improve sharp\-constant inequalities by searching for extremal constructions, which yield*upper*bounds\. We address the complementary side: a*lower*bound holds for every admissible function and follows from a convex relaxation of the nonconvex problem, with tighter relaxations giving stronger bounds\. We instantiate the autoresearch paradigm to discover such relaxations: a coding agent proposes valid tightening constraints, a theory agent verifies each one and searches for counterexamples, and every reported bound is certified by an explicit dual\-feasible point checked in rigorous interval arithmetic\. On two optimization constants studied byGeorgievet al\.\([2025](https://arxiv.org/html/2606.31182#bib.bib1)\)\- the first autocorrelation inequality \(C6\.2C\_\{6\.2\}\) and the Erdős minimum\-overlap constant \(C6\.5C\_\{6\.5\}\) \- we improve the certified lower bounds from1\.281\.28to1\.29371\.2937and from0\.3790050\.379005to0\.379120\.37912, respectively\.

Machine Learning, ICML

## 1Introduction

Large language model \(LLM\) agents have begun to contribute to mathematical research in ways that were implausible only a short time ago\. On competition mathematics, verification\-and\-refinement pipelines now reach gold\-medal performance at the International Mathematical Olympiad\(Huang and Yang,[2025](https://arxiv.org/html/2606.31182#bib.bib15)\), and frontier models have moved beyond contests toward genuine research: GPT\-5 has produced new, human\-verified results across several areas of mathematics, including settling previously open Erdős problems\(Bubecket al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib8)\)\. Larger\-scale efforts point the same way \-Tsoukalaset al\.\([2026](https://arxiv.org/html/2606.31182#bib.bib14)\)report solving 9 of 353 open Erdős problems with a frontier agent under Lean \- based formal verification, while contamination \- free benchmarks built from unpublished problems, most prominently*First Proof*\(Abouzaidet al\.,[2026](https://arxiv.org/html/2606.31182#bib.bib4)\), show models solving research\-level mathematics rather than retrieving memorized patterns\. Taken together, these episodes indicate that agentic AI is no longer only a tool for routine assistance, but a participant in mathematical discovery\.

Part of what makes these systems interesting is that their strengths differ from those of human mathematicians\. An agent does not tire, can pursue a search through the night, and can ingest a body of literature far larger than any individual could hold in mind at once\. These differences suggest that AI can contribute to mathematics in a different way from humans \- not by imitating human workflows, but by playing to strengths humans lack\. A clear example arises in functional analysis, where evolutionary and LLM\-guided search has been used to improve bounds on autocorrelation inequalities and the related Erdős minimum overlap problem\(Georgievet al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib1); Yuksekgonulet al\.,[2026](https://arxiv.org/html/2606.31182#bib.bib10); Together AI,[2026](https://arxiv.org/html/2606.31182#bib.bib16); Novikovet al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib17)\)\. There, the goal is to*construct*an extremal function: an explicit example that witnesses a bound\. Because any single admissible function yields a valid bound, the task reduces to optimizing a score over a vast, highly nonconvex space of candidate functions\-precisely the regime in which an agent can act as a tireless and creative*discoverer*, finding constructions that human search would reach only slowly, if at all\.

We pursue a different way of leveraging these tools\. Our work is motivated by two observations: AI\-assisted coding has matured to the point where agents write competent, nontrivial programs\(Jimenezet al\.,[2024](https://arxiv.org/html/2606.31182#bib.bib18)\), and agents are increasingly able to solve hard algorithmic problems\(Jainet al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib19); Zhenget al\.,[2026](https://arxiv.org/html/2606.31182#bib.bib20)\)\. We use these capabilities to improve the*other*side of these inequalities\-the*lower*bounds\. Unlike an upper bound, which follows from exhibiting one function, a lower bound must hold against*every*admissibleff; one obtains such a bound by solving a convex relaxation of the original nonconvex problem, and a tighter relaxation yields a stronger bound \(we make this precise in[Section2](https://arxiv.org/html/2606.31182#S2)\)\. Finding a good relaxation is itself an iterative, open\-ended task: an agent repeatedly edits a program, benchmarks it, and tries to beat its own best result\. This is a natural fit for the*autoresearch*paradigm\(Karpathy,[2026](https://arxiv.org/html/2606.31182#bib.bib5)\), as seen in self\-improving coding agents\(Robeynset al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib6)\)and LLM\-driven program search\(Romera\-Paredeset al\.,[2024](https://arxiv.org/html/2606.31182#bib.bib7)\)\. We instantiate this paradigm for the discovery of convex relaxations that certify lower bounds\. A difficulty particular to our setting is that an agent may simply be*wrong*\- it may propose a relaxation whose constraints are not actually valid for allff, or commit prematurely to a single line of attack\. The correctness of the convex problem is the central risk: an invalid constraint yields a bound that is not a bound at all\. We therefore pair the coding agent with a*theory agent*whose role is to read the proposed relaxation, rigorously establish that each constraint is valid, and verify the accompanying argument before any improvement is accepted\.

Using this dual\-agent loop, we improve the certified lower bounds on two autocorrelation inequalities studied byGeorgievet al\.\([2025](https://arxiv.org/html/2606.31182#bib.bib1)\)\-C6\.2C\_\{6\.2\}, arising in additive combinatorics andC6\.5C\_\{6\.5\}, controlling the asymptotics of the Erdős minimum overlap problem \(see[Section2](https://arxiv.org/html/2606.31182#S2)for definitions\)\. For the first, we raise the lower bound from1\.281\.28to1\.29371\.2937; for the second, we improve the best known lower bound of0\.3790050\.379005to0\.379120\.37912\. To our knowledge, this is the first use of an autoresearch\-style agentic loop to improve*certified lower bounds*on these inequalities: rather than searching for a better extremal example, the agents search for a better*program*\- a convex relaxation\-whose validity is established by mathematical proof and whose bound is certified by duality\.

## 2Preliminaries

### 2\.1Autocorrelation Inequalities

For absolutely integrablef,g:ℝ→ℝf,g:\\mathbb\{R\}\\to\\mathbb\{R\}, the convolution is\(f∗g\)​\(t\)=∫ℝf​\(x\)​g​\(t−x\)​𝑑x\(f\*g\)\(t\)=\\int\_\{\\mathbb\{R\}\}f\(x\)g\(t\-x\)\\,dx; whenggequalsffor a reflection offf, we refer to such expressions as*autocorrelations*Georgievet al\.\([2025](https://arxiv.org/html/2606.31182#bib.bib1)\)\. Sharp constants in functional inequalities involving autocorrelations have been studied extensively; we refer toGeorgievet al\.\([2025](https://arxiv.org/html/2606.31182#bib.bib1)\)for a survey and for the problem numbering we adopt below, andDaviset al\.\([2026](https://arxiv.org/html/2606.31182#bib.bib23)\)for the history of bounds for these problems\. We consider two such constants\.

#### The first autocorrelation inequality \(Problem 6\.2 of\(Georgievet al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib1)\)\)\.

LetC6\.2C\_\{6\.2\}denote the largest constant for which

max−1/2≤t≤1/2​∫ℝf​\(t−x\)​f​\(x\)​𝑑x≥C6\.2​\(∫−1/41/4f​\(x\)​𝑑x\)2\\max\_\{\-1/2\\leq t\\leq 1/2\}\\int\_\{\\mathbb\{R\}\}f\(t\-x\)f\(x\)\\,dx\\;\\geq\\;C\_\{6\.2\}\\left\(\\int\_\{\-1/4\}^\{1/4\}f\(x\)\\,dx\\right\)^\{2\}\(1\)holds for all non\-negativef:ℝ→ℝf:\\mathbb\{R\}\\to\\mathbb\{R\}\. This constant arises in additive combinatorics, in connection with the size of Sidon sets\(Cloninger and Steinerberger,[2017](https://arxiv.org/html/2606.31182#bib.bib21); Martin and O’Bryant,[2009](https://arxiv.org/html/2606.31182#bib.bib22)\)\. The previously known bounds are

1\.28≤C6\.2≤1\.502862,1\.28\\;\\leq\\;C\_\{6\.2\}\\;\\leq\\;1\.502862,\(2\)where the lower bound is obtained by analytic/duality arguments\(Cloninger and Steinerberger,[2017](https://arxiv.org/html/2606.31182#bib.bib21)\)and the upper bound by an explicit counterexample\(Together AI,[2026](https://arxiv.org/html/2606.31182#bib.bib16)\)\.

#### The Erdős minimum overlap problem \(Problem 6\.5\)\.

LetC6\.5C\_\{6\.5\}denote the largest constant for which

supx∈\[−2,2\]∫−11f​\(t\)​g​\(x\+t\)​𝑑t≥C6\.5\\sup\_\{x\\in\[\-2,2\]\}\\int\_\{\-1\}^\{1\}f\(t\)\\,g\(x\+t\)\\,dt\\;\\geq\\;C\_\{6\.5\}\(3\)for all non\-negativef,g:\[−1,1\]→\[0,1\]f,g:\[\-1,1\]\\to\[0,1\]withf\+g=1f\+g=1on\[−1,1\]\[\-1,1\]and∫−11f=1\\int\_\{\-1\}^\{1\}f=1\. Outside this interval\[−1,1\]\[\-1,1\],f​\(x\)=g​\(x\)=0f\(x\)=g\(x\)=0\. This constant governs the asymptotics of the minimum overlap problem of Erdős\(Georgievet al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib1)\)\. The known bounds are

0\.379005≤C6\.5≤0\.38087131058,0\.379005\\;\\leq\\;C\_\{6\.5\}\\;\\leq\\;0\.38087131058,\(4\)where the lower bound was obtained via a family of convex optimization problems\(White,[2022](https://arxiv.org/html/2606.31182#bib.bib9)\)and the upper bound by a step\-function construction\(Together AI,[2026](https://arxiv.org/html/2606.31182#bib.bib16)\)\.

In both problems the quantity of interest is an infimum over an infinite\-dimensional set of admissible functions, of a score that is nonconvex inff\. A lower bound on the constant is therefore a statement that*no*admissible function drives the score below a given value\-a universally quantified claim, in contrast to the existential claim established by a single construction\.

### 2\.2Convex Relaxation and Certified Bounds

We briefly fix the vocabulary of relaxation and duality used throughout\. Consider a nonconvex problem

p⋆=inff∈ℱJ​\(f\),p^\{\\star\}\\;=\\;\\inf\_\{f\\in\\mathcal\{F\}\}\\;J\(f\),\(5\)whereℱ\\mathcal\{F\}is the \(infinite\-dimensional\) set of admissible functions andJJis the score\. A*relaxation*replaces \([5](https://arxiv.org/html/2606.31182#S2.E5)\) by a convex problem

r⋆=infz∈𝒞J~​\(z\),r^\{\\star\}\\;=\\;\\inf\_\{z\\in\\mathcal\{C\}\}\\;\\tilde\{J\}\(z\),\(6\)constructed so that every admissibleffinduces a feasiblez∈𝒞z\\in\\mathcal\{C\}withJ~​\(z\)≤J​\(f\)\\tilde\{J\}\(z\)\\leq J\(f\)\. Any such relaxation satisfiesr⋆≤p⋆r^\{\\star\}\\leq p^\{\\star\}, sor⋆r^\{\\star\}is a valid lower bound on the constant of interest\. The relaxation is*valid*precisely when this inclusion holds\-that is, when every constraint defining𝒞\\mathcal\{C\}is satisfied by the encoding of every admissibleff\. A*tighter*relaxation is one with a largerr⋆r^\{\\star\}\(equivalently, a smaller feasible set that still contains all admissible encodings\); tightening the relaxation improves the bound, up to the limitr⋆=p⋆r^\{\\star\}=p^\{\\star\}\.

#### Certified bounds via duality\.

Solving \([6](https://arxiv.org/html/2606.31182#S2.E6)\) numerically returns a value, but for a*certified*bound we appeal to weak duality\. For any dual\-feasible pointλ\\lambda, the dual objectived​\(λ\)d\(\\lambda\)satisfies

d​\(λ\)≤r⋆≤p⋆d\(\\lambda\)\\;\\leq\\;r^\{\\star\}\\;\\leq\\;p^\{\\star\}\(7\)Exhibiting a single dual\-feasibleλ\\lambdawithd​\(λ\)=βd\(\\lambda\)=\\betatherefore provesp⋆≥βp^\{\\star\}\\geq\\beta, and this certificate is checkable independently of the solver that produced it: one need only verify thatλ\\lambdasatisfies the dual constraints and evaluated​\(λ\)d\(\\lambda\)\. This is the sense in which our bounds are certified, and it is what distinguishes a proven lower bound from a numerically reported optimal value\. We return to how we find a rigorous dual certificate and a lower bound in[Section3](https://arxiv.org/html/2606.31182#S3)\.

## 3Method

Coding agentadd or tighten constraintTheory agentverifyUpdatedrelaxationacceptrejectiterateAutomatedFinalrelaxationHumanverify / compactifyDualcertifiedboundterminateFigure 1:The framework\. The*automated*block \(purple, dashed\) alternates between a coding agent that adds or tightens a constraint and a theory agent that verifies its validity and searches for counterexamples; accepted constraints update the relaxation, and the loop repeats\. On termination it yields the final relaxation, which a human verifies and compactifies; the resulting bound is certified by an explicit dual\-feasible point\.### 3\.1Problem Formulation

Each constant in[Section2\.1](https://arxiv.org/html/2606.31182#S2.SS1)is the value of a min\-max problem over an infinite\-dimensional class of admissible functions\. We describe the convex problem formulation through the minimum overlap problem, followingWhite \([2022](https://arxiv.org/html/2606.31182#bib.bib9)\); the autocorrelation inequalityC6\.2C\_\{6\.2\}of \([1](https://arxiv.org/html/2606.31182#S2.E1)\) is treated analogously\.

For the minimum overlap problem, the constant is the infimum over admissibleffof a maximum over translates,

C6\.5=inffmaxt∈\[−2,2\]​∫−11f​\(x\)​g​\(x\+t\)​𝑑x,C\_\{6\.5\}\\;=\\;\\inf\_\{f\}\\;\\max\_\{t\\in\[\-2,2\]\}\\;\\int\_\{\-1\}^\{1\}f\(x\)g\(x\+t\)\\,dx,\(8\)taken over measurablef:\[−1,1\]→\[0,1\]f:\[\-1,1\]\\rightarrow\[0,1\]and normalization∫−11f=1\\int\_\{\-1\}^\{1\}f=1\. White’s reduction turns this nonconvex min–max into a convex program of a finite list of variables\. WriteM​\(t\)=∫−11f​\(x\)​g​\(x\+t\)​𝑑xM\(t\)=\\int\_\{\-1\}^\{1\}f\(x\)g\(x\+t\)\\,dxfor the overlap attt, whereg​\(x\)=1−f​\(x\)g\(x\)=1\-f\(x\)forx∈\[−1,1\]x\\in\[\-1,1\]and 0 otherwise, and partition\[0,2\]\[0,2\]into grid cellsI1,…,INI\_\{1\},\\dots,I\_\{N\}of widthLL\. White’s reduction then introduces the following variables: a scalarΩ\\Omegaboundingmaxk⁡M​\(k\)\\max\_\{k\}M\(k\); the cell integrals of the overlap on the two shift directions,

wj=1L​∫IjM​\(k\)​𝑑k,vj=1L​∫IjM​\(−k\)​𝑑k,w\_\{j\}\\;=\\;\\frac\{1\}\{L\}\\int\_\{I\_\{j\}\}M\(k\)\\,dk,\\quad v\_\{j\}\\;=\\;\\frac\{1\}\{L\}\\int\_\{I\_\{j\}\}M\(\-k\)\\,dk,\(9\)the cosine and sine Fourier coefficientsck,dkc\_\{k\},d\_\{k\}offfandam,bma\_\{m\},b\_\{m\}ofMM; and truncation slacksεm,δm\\varepsilon\_\{m\},\\delta\_\{m\}that absorb the Fourier modes beyond the truncation order so that finitely many coefficients suffice\.

Admissibility offfimposes constraints on these variables, and the essential point is that each one must be a genuine consequence of0≤f≤10\\leq f\\leq 1and∫−11f=1\\int\_\{\-1\}^\{1\}f=1, so that no admissibleffis excluded\. Two are immediate\. The property∫−22M​\(x\)​𝑑x=1\\int\_\{\-2\}^\{2\}M\(x\)dx=1gives the linear identityL​∑j\(wj\+vj\)=1L\\sum\_\{j\}\(w\_\{j\}\+v\_\{j\}\)=1, and becauseΩ\\Omegabounds the overlap at every translate, each cell integral obeyswj,vj≤Ωw\_\{j\},v\_\{j\}\\leq\\Omega\. The remaining conditions \- mean and second\-moment bounds, the Fourier identities linkingam,bma\_\{m\},b\_\{m\}tock,dkc\_\{k\},d\_\{k\}, and the bounds on the truncation slackϵm,δm\\epsilon\_\{m\},\\delta\_\{m\}, are derived in the same spirit; we refer the reader toWhite \([2022](https://arxiv.org/html/2606.31182#bib.bib9)\)or[Algorithm1](https://arxiv.org/html/2606.31182#alg1)for the full list\. We retain only those conditions that are convex in the variables to make the problem convex\.Let𝒦\\mathcal\{K\}be the feasible set they cut out\.

The lower bound now follows from a single observation\. Fix any admissibleffand read off its variables: takeΩ=maxk∈\[−2,2\]⁡M​\(k\)\\Omega=\\max\_\{k\\in\[\-2,2\]\}M\(k\), letwj,vjw\_\{j\},v\_\{j\}be the cell integrals in \([9](https://arxiv.org/html/2606.31182#S3.E9)\), and let the remaining entries be the Fourier data offf\. By construction this assignment satisfies every constraint of𝒦\\mathcal\{K\}, so it is a feasible point of the convex program, and its objective value is exactlymaxk∈\[−2,2\]⁡M​\(k\)\\max\_\{k\\in\[\-2,2\]\}M\(k\), the overlap score offf\. The convex program minimizes that same objective over all of𝒦\\mathcal\{K\}, returning a valueΩ⋆\\Omega^\{\\star\}\. Since every admissibleffsupplies a feasible point whose objective equals its own score, the minimum can only be smaller:Ω⋆≤maxk∈\[−2,2\]⁡M​\(k\)\\Omega^\{\\star\}\\leq\\max\_\{k\\in\[\-2,2\]\}M\(k\)for every admissibleff, and thereforeΩ⋆≤C6\.5\\Omega^\{\\star\}\\leq C\_\{6\.5\}\.

### 3\.2Successive Convex Relaxation

The quality of the convex problem is governed entirely by the constraint set𝒦\\mathcal\{K\}\. Tightening𝒦\\mathcal\{K\}\-adding a valid condition, or strengthening an existing one\-shrinks the feasible set toward the true set of admissible coefficient vectors, and the minimum can only increase:

𝒦′⊆𝒦⟹minc∈𝒦′⁡Φ​\(c\)≥minc∈𝒦⁡Φ​\(c\)\.\\mathcal\{K\}^\{\\prime\}\\subseteq\\mathcal\{K\}\\quad\\Longrightarrow\\quad\\min\_\{c\\in\\mathcal\{K\}^\{\\prime\}\}\\Phi\(c\)\\;\\geq\\;\\min\_\{c\\in\\mathcal\{K\}\}\\Phi\(c\)\.\(10\)So long as every condition is valid,𝒦′\\mathcal\{K\}^\{\\prime\}still contains all admissible encodings, and the larger value remains a lower bound onΩ\\Omega\. Iterating yields a monotone sequence of valid lower bounds increasing towardΩ\\Omega\.

We stress that “tightening” here means*adding valid constraints or improving existing ones*, not naively increasing resolution\. One could enlarge the model with more Fourier modes or finer step functions; this refines the discretization but does not, in itself, tighten the relaxation in the sense of \([10](https://arxiv.org/html/2606.31182#S3.E10)\)\. The improvements we seek are mathematical: properties of admissible coefficient sequences that a coarser formulation failed to impose\. The task at each iteration is therefore to*identify a valid constraint that previous relaxations overlooked*, or to sharpen one imposed too weakly\. The concrete constraints discovered for each problem, and their effect on the bound are reported in[Section4](https://arxiv.org/html/2606.31182#S4)\.

### 3\.3The Dual\-Agent Loop

We search for such constraints with a human\-in\-the\-loop framework: a loop of two agents drives the discovery, and a human conducts a final review and compactification\. The loop instantiates the autoresearch paradigm\(Karpathy,[2026](https://arxiv.org/html/2606.31182#bib.bib5)\)for the discovery of certified relaxations\. We used Claude Opus 4\.6 for our agent experiments, and detailed prompts can be found in[AppendixD](https://arxiv.org/html/2606.31182#A4)\.

#### Coding agent\.

The coding agent proposes an improvement to the current relaxation\-typically a new constraint on the coefficient vectorcc, or a strengthening of an existing one\-together with a rigorous proof that the constraint is valid, i\.e\. that it holds for the coefficients of every admissibleff\. It then implements the modified convex program and solves it, producing a candidate bound\.

#### Theory agent\.

The theory agent reads the proposed constraint and its proof and checks that the constraint is a sound consequence of the admissibility offf\. Critically, it does not only attempt to confirm the argument: it also*actively searches for a counterexample*\-an admissibleffwhose coefficients violate the proposed constraint\. A constraint survives only if its justification holds and no counterexample is found\. This guards the invariant on which the entire bound rests: a constraint that some admissibleffviolates would shrink𝒦\\mathcal\{K\}below the admissible set and silently invalidate the lower bound\.

The prompts used for the coding agent and the theory agent, as well as the problem descriptions, are in[AppendixD](https://arxiv.org/html/2606.31182#A4)\.

#### Human review and compactification\.

The agent loop tends to accumulate constraints, not all of which are necessary: many are redundant at the optimum and contribute nothing to the bound\. Once the loop has produced a candidate relaxation, a human performs a final pass\-reading the program and the validity arguments, and removing redundant constraints to obtain a minimal program\. Removing a constraint enlarges𝒦\\mathcal\{K\}and so, by \([10](https://arxiv.org/html/2606.31182#S3.E10)\), can only lower the bound; a constraint is therefore dropped only when the certified value was not meaningful in the history of objective values\.

#### Certifying Correctness

Two conditions must hold for a reported bound to be valid, and they are established by different means\. First, every constraint in the final program must be a true property of all admissibleff\. This is established by a mathematical argument, produced by the agents and confirmed by human review; we do*not*formally verify these arguments \(e\.g\. in a proof assistant\), so this is the step at which correctness ultimately rests on human judgment\. Second, the reported number must actually be a lower bound for the resulting convex program\. This does*not*rest on human judgment: given the program, its dual is formed by the standard duality recipe, and any dual\-feasible point yields a valid bound by weak duality \([Section2\.2](https://arxiv.org/html/2606.31182#S2.SS2)\)\. We certify each bound by exhibiting such a point, rigorously checking whether the point is dual\-feasible, and evaluating the dual objective in interval arithmetic\.

We work in the canonical conic form used by CVXPY\(Diamond and Boyd,[2016](https://arxiv.org/html/2606.31182#bib.bib31)\)\. Every program in this paper can be written as

minx⁡c⊤​xsubject toA​x\+s=b,s∈𝒦,\\min\_\{x\}\\;c^\{\\top\}x\\quad\\text\{subject to\}\\quad Ax\+s=b,\\;\\;s\\in\\mathcal\{K\},\(11\)where𝒦\\mathcal\{K\}is a product of the nonnegative orthant, second\-order cones, and positive\-semidefinite cones; CVXPY’s canonicalization produces exactly this form\. The corresponding dual is

maxy−b⊤​ysubject toA⊤​y\+c=0,y∈𝒦∗,\\max\_\{y\}\\;\-b^\{\\top\}y\\quad\\text\{subject to\}\\quad A^\{\\top\}y\+c=0,\\;\\;y\\in\\mathcal\{K\}^\{\*\},\(12\)with𝒦∗\\mathcal\{K\}^\{\*\}the dual cone, and weak duality gives, for any dual\-feasibleyy,

−b⊤​y≤minx⁡c⊤​x=Ω⋆\.\-b^\{\\top\}y\\;\\leq\\;\\min\_\{x\}c^\{\\top\}x\\;=\\;\\Omega^\{\\star\}\.\(13\)A single dual\-feasibley~\\tilde\{y\}therefore provesΩ⋆≥−b⊤​y~\\Omega^\{\\star\}\\geq\-b^\{\\top\}\\tilde\{y\}, independently of the solver that produced it\. We obtain a candidate witnessy~\\tilde\{y\}from CVXPY and verify it rigorously, which raises two issues:y~\\tilde\{y\}is only numerically dual\-feasible, and controlling the rounding introduced by irrational problem data\.

Cone membership is the first requirement\. For the orthant and second\-order blocks it reduces to a finite set of sign and norm inequalities, checked directly\. The positive\-semidefinite blocks are more delicate: certifying that a matrix is PSD in the presence of rounding cannot be done by computing eigenvalues naively, since a matrix that is PSD in exact arithmetic may have a small negative computed eigenvalue\. We instead certify PSD\-ness by a verified factorization carried out in interval arithmetic; the details are deferred to Appendix[E](https://arxiv.org/html/2606.31182#A5)\.

The second issue is rounding\. The coefficientsA,b,cA,b,ccontain irrational entries \(trigonometric moments and Fejér weights\), so the matrices actually stored,A¯,b¯,c¯\\bar\{A\},\\bar\{b\},\\bar\{c\}, are rounded; writingεA,εb,εc\\varepsilon\_\{A\},\\varepsilon\_\{b\},\\varepsilon\_\{c\}for elementwise bounds on‖A−A¯‖∞\\\|A\-\\bar\{A\}\\\|\_\{\\infty\},‖b−b¯‖∞\\\|b\-\\bar\{b\}\\\|\_\{\\infty\}, and‖c−c¯‖∞\\\|c\-\\bar\{c\}\\\|\_\{\\infty\}, each true coefficient is enclosed in an interval of the corresponding width\. Both the stored problem and the final objective therefore carry rounding, and a rigorous bound must absorb both\. Letrrbound the dual residual‖A⊤​y~\+c‖∞\\\|A^\{\\top\}\\tilde\{y\}\+c\\\|\_\{\\infty\}, the extent to whichy~\\tilde\{y\}fails exact dual feasibility, and letXXbe an a priori bound on‖x‖\\\|x\\\|over primal\-optimalx∗x^\{\*\}\. Weak duality together with these error terms yields the certified bound

Ω⋆=c⊤​x⋆≥−b⊤​y~−\(r\+εA​‖y~‖1\+εc\)​X−εb​‖y~‖1\.\\Omega^\{\\star\}\\;=\\;c^\{\\top\}x^\{\\star\}\\;\\geq\\;\-b^\{\\top\}\\tilde\{y\}\\;\-\\;\\bigl\(r\+\\varepsilon\_\{A\}\\\|\\tilde\{y\}\\\|\_\{1\}\+\\varepsilon\_\{c\}\\bigr\)\\,X\\;\-\\;\\varepsilon\_\{b\}\\\|\\tilde\{y\}\\\|\_\{1\}\.\(14\)Each quantity on the right is a guaranteed bound, and using the bound leads to a rigorous lower bound ofΩ∗\\Omega^\{\*\}\. We evaluate the entire right\-hand side in interval arithmetic with outward rounding, so the reported value is the lower endpoint of a verified enclosure\. See[AppendixC](https://arxiv.org/html/2606.31182#A3)for a detailed derivation\.

## 4Results

We apply the dual\-agent approach described in[Section3](https://arxiv.org/html/2606.31182#S3)to two constantsC6\.2C\_\{6\.2\}andC6\.5C\_\{6\.5\}For each we report the convex program discovered by the loop, and the certified lower bound it yields\. All bounds are certified by an explicit dual\-feasible point evaluated in exact rational arithmetic \(Section[3](https://arxiv.org/html/2606.31182#S3)\); no floating\-point margin enters the final certificate\. At last, an analysis of the loop’s behavior for the first autocorrelation inequality is discussed in[Section4\.3](https://arxiv.org/html/2606.31182#S4.SS3)\.

### 4\.1Discovered convex programs

ForC6\.5C\_\{6\.5\}the loop took the convex program ofWhite \([2022](https://arxiv.org/html/2606.31182#bib.bib9)\)as its starting point and searched for valid constraints to tighten it\. The program \(Algorithm[1](https://arxiv.org/html/2606.31182#alg1)\) shows the resulting convex program, with theboxedpair of constraints are the ones added by the loop\. The discovered constraints are a pair of*Bochner conditions*:Tf⪰0T\_\{f\}\\succeq 0enforces that the moment sequence offfis realizable by a nonnegative measure, andI−Tf⪰0I\-T\_\{f\}\\succeq 0enforces the same for its complementg=1−fg=1\-f\. White’s formulation does not explicitly use the constraint0≤f≤10\\leq f\\leq 1pointwise, where our advantage is introduced\. The loop identified both conditions automatically, and the theory agent verified their validity \(Bochner’s theorem, applied toffand tog=1−fg=1\-f\) before they were accepted\. For a rigorous proof of the added constraint see[AppendixA](https://arxiv.org/html/2606.31182#A1)\.

The convex program depends on six parametersh1,h2,p1,p2,q1,q2h\_\{1\},h\_\{2\},p\_\{1\},p\_\{2\},q\_\{1\},q\_\{2\}that bracket three quantities of an admissibleff: the meanE​\(M\)E\(M\)of the overlap, withh1≤E​\(M\)≤h2h\_\{1\}\\leq E\(M\)\\leq h\_\{2\}; the first cosine coefficientc1c\_\{1\}offf, withp1≤c1≤p2p\_\{1\}\\leq c\_\{1\}\\leq p\_\{2\}; and the first sine coefficientd1d\_\{1\}, withq1≤d1≤q2q\_\{1\}\\leq d\_\{1\}\\leq q\_\{2\}\. Over all admissibleffthese quantities range withinE​\(M\)∈\[0,2\]E\(M\)\\in\[0,2\],c1∈\[0,1\]c\_\{1\}\\in\[0,1\], andd1∈\[−1,1\]d\_\{1\}\\in\[\-1,1\]\(for a proof see\(White,[2022](https://arxiv.org/html/2606.31182#bib.bib9)\)\)\. WriteΩ​\(h1,h2,p1,p2,q1,q2\)\\Omega\(h\_\{1\},h\_\{2\},p\_\{1\},p\_\{2\},q\_\{1\},q\_\{2\}\)for the certified optimum of the program with the parameters constrained to the box\[h1,h2\]×\[p1,p2\]×\[q1,q2\]\[h\_\{1\},h\_\{2\}\]\\times\[p\_\{1\},p\_\{2\}\]\\times\[q\_\{1\},q\_\{2\}\]\. For any such box the program is a valid relaxation, so its optimum lower\-bounds the score of every admissibleffwhose\(E​\(M\),c1,d1\)\(E\(M\),c\_\{1\},d\_\{1\}\)falls in that box\.

Since every admissibleffhas\(E​\(M\),c1,d1\)\(E\(M\),c\_\{1\},d\_\{1\}\)somewhere in the full boxℬ=\[0,2\]×\[0,1\]×\[−1,1\]\\mathcal\{B\}=\[0,2\]\\times\[0,1\]\\times\[\-1,1\], solving the program over all ofℬ\\mathcal\{B\}at once already gives a valid lower bound onΩ\\Omega\. That bound is weak, however: a relaxation over a large parameter box is loose, so its optimum comes out well belowΩ\\Omega\. The bound sharpens as the box shrinks \- constraining the parameters to a small region tightens the relaxation and raises its certified optimum\. We therefore splitℬ\\mathcal\{B\}into sub\-boxes and bound each one separately, which is the branch\-and\-bound step\. Coverℬ\\mathcal\{B\}by sub\-boxesB′=\[h1,h2\]×\[p1,p2\]×\[q1,q2\]B^\{\\prime\}=\[h\_\{1\},h\_\{2\}\]\\times\[p\_\{1\},p\_\{2\}\]\\times\[q\_\{1\},q\_\{2\}\]; a single certified dual point forΩ​\(h1,h2,p1,p2,q1,q2\)\\Omega\(h\_\{1\},h\_\{2\},p\_\{1\},p\_\{2\},q\_\{1\},q\_\{2\}\)lower\-bounds the objective*simultaneously for every*\(E​\(M\),c1,d1\)∈B′\(E\(M\),c\_\{1\},d\_\{1\}\)\\in B^\{\\prime\}, and the smallerB′B^\{\\prime\}is, the tighter this local bound\. A sub\-box whose certificate already meets the target is cleared; otherwise it is split further and the procedure recurses, until all ofℬ\\mathcal\{B\}is covered\. The reported bound is the smallest certified optimum over the cover \- a valid lower bound onΩ\\Omega, and a sharper one than the single whole\-box solve\.

ForC6\.2C\_\{6\.2\}no prior convex program was available; the loop constructed one from scratch \(Algorithm[2](https://arxiv.org/html/2606.31182#alg2)\)\. The agentic system introduced variables as the following: a discretized nonnegative measureppon\[−14,14\]\[\-\\tfrac\{1\}\{4\},\\tfrac\{1\}\{4\}\]\(the support reduction of Lemma[B\.1](https://arxiv.org/html/2606.31182#A2.Thmtheorem1)\), with trigonometric momentsak,bka\_\{k\},b\_\{k\}\. The program combines: a probability simplex and a positive\-semidefinite moment matrix; per\-cell Fourier envelopes bracketingak,bka\_\{k\},b\_\{k\}, computed in exact integer arithmetic so envelope validity carries no floating\-point tolerance; a Fejér–Riesz Gram matrixQQcertifyingΩ−\(FK∗g\)​\(t\)≥0\\Omega\-\(F\_\{K\}\*g\)\(t\)\\geq 0for alltt\(the sum\-of\-squares encoding of the pointwise lower bound on the autocorrelation peak,g=f∗fg=f\*f\); a quadratic energy bound following from∫g2=∑m\|f^​\(m\)\|4\\int g^\{2\}=\\sum\_\{m\}\|\\hat\{f\}\(m\)\|^\{4\}; and plain and*localized*Bochner conditions, the latter valid becausecos⁡\(2​π​x\)≥0\\cos\(2\\pi x\)\\geq 0exactly on\[−14,14\]\[\-\\tfrac\{1\}\{4\},\\tfrac\{1\}\{4\}\]\. The derivation of the novel convex program is in[AppendixB](https://arxiv.org/html/2606.31182#A2)\.

Algorithm 1Discovered convex program for the Erdős minimum\-overlap constantC6\.5C\_\{6\.5\}\.0:grid size

NN\(

L=2/NL=2/N\), truncation

TT, modes

RR; box

h1,h2,p1,p2h\_\{1\},h\_\{2\},p\_\{1\},p\_\{2\}and fixed

q1,q2q\_\{1\},q\_\{2\}
1:minimize

Ω\\Omega
2:over

Ω≤1\\Omega\\leq 1,

\{wj,vj\}\\\{w\_\{j\},v\_\{j\}\\\},

\{ck,dk\}k=1T\\\{c\_\{k\},d\_\{k\}\\\}\_\{k=1\}^\{T\},

\{am,bm\}m=12​R\\\{a\_\{m\},b\_\{m\}\\\}\_\{m=1\}^\{2R\},

\{εm,δm\}m=1R\\\{\\varepsilon\_\{m\},\\delta\_\{m\}\\\}\_\{m=1\}^\{R\}
3:subject to

4:

0≤wj,vj≤Ω≤10\\leq w\_\{j\},\\,v\_\{j\}\\leq\\Omega\\leq 1
5:

L​∑j\(wj\+vj\)=1L\\sum\_\{j\}\(w\_\{j\}\+v\_\{j\}\)=1
6:

h1≤L2​∑j\(j​wj−\(j−1\)​vj\)h\_\{1\}\\leq L^\{2\}\\sum\_\{j\}\(jw\_\{j\}\-\(j\-1\)v\_\{j\}\)
7:

L2​∑j\(\(j−1\)​wj−j​vj\)≤h2L^\{2\}\\sum\_\{j\}\(\(j\-1\)w\_\{j\}\-jv\_\{j\}\)\\leq h\_\{2\}
8:

23\+h122≤L3​∑jj2​\(wj\+vj\)\\frac\{2\}\{3\}\+\\frac\{h\_\{1\}^\{2\}\}\{2\}\\leq L^\{3\}\\sum\_\{j\}j^\{2\}\(w\_\{j\}\+v\_\{j\}\)
9:

L3​∑j\(j−1\)2​\(wj\+vj\)≤23\+h222L^\{3\}\\sum\_\{j\}\(j\-1\)^\{2\}\(w\_\{j\}\+v\_\{j\}\)\\leq\\frac\{2\}\{3\}\+\\frac\{h\_\{2\}^\{2\}\}\{2\}
10:

L2​∑jαj,m−​\(wj\+vj\)≤4​sin⁡\(π​m/2\)π​m​am−2​\(am2\+bm2\)\\frac\{L\}\{2\}\\sum\_\{j\}\\alpha^\{\-\}\_\{j,m\}\(w\_\{j\}\+v\_\{j\}\)\\leq\\frac\{4\\sin\(\\pi m/2\)\}\{\\pi m\}a\_\{m\}\-2\(a\_\{m\}^\{2\}\+b\_\{m\}^\{2\}\)
11:

L2​∑j\(βj,m−​wj−βj,m\+​vj\)≤−4​sin⁡\(π​m/2\)π​m​bm\\frac\{L\}\{2\}\\sum\_\{j\}\(\\beta^\{\-\}\_\{j,m\}w\_\{j\}\-\\beta^\{\+\}\_\{j,m\}v\_\{j\}\)\\leq\-\\frac\{4\\sin\(\\pi m/2\)\}\{\\pi m\}b\_\{m\}
12:

−4​sin⁡\(π​m/2\)π​m​bm≤L2​∑j\(βj,m\+​wj−βj,m−​vj\)\-\\frac\{4\\sin\(\\pi m/2\)\}\{\\pi m\}b\_\{m\}\\leq\\frac\{L\}\{2\}\\sum\_\{j\}\(\\beta^\{\+\}\_\{j,m\}w\_\{j\}\-\\beta^\{\-\}\_\{j,m\}v\_\{j\}\)
13:

am=12​cm/2a\_\{m\}=\\frac\{1\}\{2\}c\_\{m/2\},

bm=12​dm/2b\_\{m\}=\\frac\{1\}\{2\}d\_\{m/2\}\(mmeven\)

14:

am=εm\+2​m​sin⁡\(π​m/2\)π​\(12​m2\+∑k=1T\(−1\)km2−4​k2​ck\)a\_\{m\}=\\varepsilon\_\{m\}\+\\frac\{2m\\sin\(\\pi m/2\)\}\{\\pi\}\\left\(\\frac\{1\}\{2m^\{2\}\}\+\\sum\_\{k=1\}^\{T\}\\frac\{\(\-1\)^\{k\}\}\{m^\{2\}\-4k^\{2\}\}c\_\{k\}\\right\)
15:

bm=δm\+4π​∑k=1Tk​\(−1\)k​sin⁡\(π​m/2\)m2−4​k2​dkb\_\{m\}=\\delta\_\{m\}\+\\frac\{4\}\{\\pi\}\\sum\_\{k=1\}^\{T\}\\frac\{k\(\-1\)^\{k\}\\sin\(\\pi m/2\)\}\{m^\{2\}\-4k^\{2\}\}d\_\{k\}\(mmodd\)

16:

\|εm\|,\|δm\|≤tail bound\|\\varepsilon\_\{m\}\|,\|\\delta\_\{m\}\|\\leq\\text\{tail bound\}\(2​m−1<2​T2m\-1<2T\)

17:

\|ck\|,\|dk\|≤2π\|c\_\{k\}\|,\|d\_\{k\}\|\\leq\\frac\{2\}\{\\pi\},

∑k\(ck2\+dk2\)≤12\\sum\_\{k\}\(c\_\{k\}^\{2\}\+d\_\{k\}^\{2\}\)\\leq\\frac\{1\}\{2\}
18:

p1≤c1≤p2p\_\{1\}\\leq c\_\{1\}\\leq p\_\{2\},

q1≤d1≤q2q\_\{1\}\\leq d\_\{1\}\\leq q\_\{2\}
19:

L2​∑jαj,2\+​\(wj\+vj\)≥−12​\(p22\+max⁡\{q12,q22\}\)\\frac\{L\}\{2\}\\sum\_\{j\}\\alpha^\{\+\}\_\{j,2\}\(w\_\{j\}\+v\_\{j\}\)\\geq\-\\frac\{1\}\{2\}\(p\_\{2\}^\{2\}\+\\max\\\{q\_\{1\}^\{2\},q\_\{2\}^\{2\}\\\}\)
20:Tf⪰0,I−Tf⪰0T\_\{f\}\\succeq 0,\\qquad I\-T\_\{f\}\\succeq 0

21:\(Tf\)k​l=14​δk​l\+12​\(a\|k−l\|−i​sgn⁡\(k−l\)​b\|k−l\|\)\(T\_\{f\}\)\_\{kl\}=\\frac\{1\}\{4\}\\delta\_\{kl\}\+\\frac\{1\}\{2\}\(a\_\{\|k\-l\|\}\-\\mathrm\{\\textbf\{i\}\}\\operatorname\{sgn\}\(k\-l\)b\_\{\|k\-l\|\}\)

22:Branch and bound:Fix

\(q1,q2\)\(q\_\{1\},q\_\{2\}\)and sweep the

\(h,p\)\(h,p\)rectangle\. Certify each rectangle by an exact\-arithmetic dual point; if certified, clear it, otherwise split and recurse\. return smallest certified value over cleared rectangles

Algorithm 2Discovered semidefinite program for the Sidon\-set autocorrelation constantC6\.2C\_\{6\.2\}\.0:cells

2​N2Non

\[−14,14\]\[\-\\frac\{1\}\{4\},\\frac\{1\}\{4\}\], modes

KK
1:minimize

Ω\\Omega
2:over

Ω≥0\\Omega\\geq 0,

p∈ℝ≥02​Np\\in\\mathbb\{R\}^\{2N\}\_\{\\geq 0\}, moments

ak,bka\_\{k\},b\_\{k\},

M⪰0M\\succeq 0, Hermitian

Q⪰0Q\\succeq 0, slacks

vk≥0v\_\{k\}\\geq 0
3:subject to

4:

∑jpj=1\\sum\_\{j\}p\_\{j\}=1
5:

M⪰0M\\succeq 0,

M00=1M\_\{00\}=1,

M0​k=akM\_\{0k\}=a\_\{k\},

M0,K\+k=bkM\_\{0,K\+k\}=b\_\{k\}
6:

γk−⋅p≤ak≤γk\+⋅p\\gamma^\{\-\}\_\{k\}\\cdot p\\leq a\_\{k\}\\leq\\gamma^\{\+\}\_\{k\}\\cdot p,

σk−⋅p≤bk≤σk\+⋅p\\sigma^\{\-\}\_\{k\}\\cdot p\\leq b\_\{k\}\\leq\\sigma^\{\+\}\_\{k\}\\cdot p
7:

Ω≥1\+2​∑kwk​vk\\Omega\\geq 1\+2\\sum\_\{k\}w\_\{k\}v\_\{k\},

vk≥\(Mk​k\+MK\+k,K\+k\)2v\_\{k\}\\geq\(M\_\{kk\}\+M\_\{K\+k,K\+k\}\)^\{2\}
8:

Q⪰0Q\\succeq 0,

tr⁡\(Q\)=Ω−1\\operatorname\{tr\}\(Q\)=\\Omega\-1
9:

∑iQi,i\+k=i​2​wk​Mk,K\+k−wk​\(Mk​k−MK\+k,K\+k\)\\sum\_\{i\}Q\_\{i,i\+k\}=\\mathrm\{\\textbf\{i\}\}\\,2w\_\{k\}M\_\{k,K\+k\}\-w\_\{k\}\(M\_\{kk\}\-M\_\{K\+k,K\+k\}\)
10:

\[TR−TITITR\]⪰0\\begin\{bmatrix\}T\_\{R\}&\-T\_\{I\}\\\\ T\_\{I\}&T\_\{R\}\\end\{bmatrix\}\\succeq 0,

Ti​j=a\|i−j\|−i​sgn⁡\(i−j\)​b\|i−j\|T\_\{ij\}=a\_\{\|i\-j\|\}\-\\mathrm\{\\textbf\{i\}\}\\operatorname\{sgn\}\(i\-j\)b\_\{\|i\-j\|\}
11:

\[TRν−TIνTIνTRν\]⪰0\\begin\{bmatrix\}T^\{\\nu\}\_\{R\}&\-T^\{\\nu\}\_\{I\}\\\\ T^\{\\nu\}\_\{I\}&T^\{\\nu\}\_\{R\}\\end\{bmatrix\}\\succeq 0,

\(Tν\)i​j=νi−j\(T^\{\\nu\}\)\_\{ij\}=\\nu\_\{i\-j\},

νk=12​\(μ^k−1\+μ^k\+1\)\\nu\_\{k\}=\\frac\{1\}\{2\}\(\\hat\{\\mu\}\_\{k\-1\}\+\\hat\{\\mu\}\_\{k\+1\}\)

### 4\.2Improved bounds

Both constants have long histories of incremental improvement, and in both cases the recent gains on the*upper*\(construction\) side came from search\-based methods, while the*lower*\(duality\) side had not moved since 2022\. Our framework improves the lower side of both\.

#### Minimum overlap \(C6\.5C\_\{6\.5\}\)\.

The minimum\-overlap constantC6\.5=limnM​\(n\)/nC\_\{6\.5\}=\\lim\_\{n\}M\(n\)/nhas an even longer record\. Early lower bounds came from averaging and rearrangement arguments \- Erdős’14\\tfrac\{1\}\{4\}\(Erdős,[1955](https://arxiv.org/html/2606.31182#bib.bib24)\), and Moser’s4−15≈0\.35639\\sqrt\{4\-\\sqrt\{15\}\}\\approx 0\.35639\(Moser and Murdeshwar,[1966](https://arxiv.org/html/2606.31182#bib.bib25)\)\- untilWhite \([2022](https://arxiv.org/html/2606.31182#bib.bib9)\)reformulated the lower bound as a convex program and obtained0\.3790050\.379005\. The upper side has been refined by step\-function constructions:0\.3820020\.382002\(Haugland,[1996](https://arxiv.org/html/2606.31182#bib.bib26)\)and0\.3809260\.380926\(Haugland,[2016](https://arxiv.org/html/2606.31182#bib.bib27)\), then0\.3809240\.380924AlphaEvolve\(Georgievet al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib1)\),0\.3808760\.380876\(Yuksekgonulet al\.,[2026](https://arxiv.org/html/2606.31182#bib.bib10)\)and0\.3808710\.380871in\(Together AI,[2026](https://arxiv.org/html/2606.31182#bib.bib16)\)\. Our augmented program certifies

0\.37912≤C6\.5,0\.37912\\leq C\_\{6\.5\}\\ ,improving[White](https://arxiv.org/html/2606.31182#bib.bib9)’s0\.3790050\.379005\. The bound is the minimum certified value over the branch\-and\-bound sweep of the\(h,p\)\(h,p\)box; the subdivision tree is shown in Figure[4](https://arxiv.org/html/2606.31182#A5.F4)\(Appendix[E](https://arxiv.org/html/2606.31182#A5)\)\. Table[1](https://arxiv.org/html/2606.31182#S4.T1)summarizes the record\.

Table 1:State of the art for the Erdős minimum\-overlap constantC6\.5C\_\{6\.5\}\(Eq\. \([3](https://arxiv.org/html/2606.31182#S2.E3)\)\)\. Lower bounds are the duality side; upper bounds come from step\-function constructions and recent search\-based methods\. Records as inDaviset al\.\([2026](https://arxiv.org/html/2606.31182#bib.bib23)\)\.
#### Autocorrelation \(C6\.2C\_\{6\.2\}\)\.

C6\.2C\_\{6\.2\}has been bounded below through a sequence of Fourier\-analytic arguments:1\.2621\.262\(Martin and O’Bryant,[2009](https://arxiv.org/html/2606.31182#bib.bib22)\)and1\.27491\.2749\(Matolcsi and Vinuesa,[2010](https://arxiv.org/html/2606.31182#bib.bib28)\)\- who also conjectured a ceiling of1\.2761\.276for their method \- followed by1\.281\.28via a finite\-case relaxation\(Cloninger and Steinerberger,[2017](https://arxiv.org/html/2606.31182#bib.bib21)\)\. The upper side, by explicit constructions, currently stands at1\.5028621\.502862\(Together AI,[2026](https://arxiv.org/html/2606.31182#bib.bib16)\)\. Our discovered SDP certifies

1\.2937≤C6\.21\.2937\\leq C\_\{6\.2\}\\,improving the previous lower record of1\.281\.28\. The certificate is an explicit dual\-feasible point of the SDP, verified positive semidefinite and feasible in exact interval arithmetic, so the bound holds without reliance on the numerical solver or floating\-point error analysis\. Table[2](https://arxiv.org/html/2606.31182#S4.T2)summarizes the record\.

Table 2:State of the art for the Sidon\-set autocorrelation constantC6\.2C\_\{6\.2\}\(Eq\. \([1](https://arxiv.org/html/2606.31182#S2.E1)\)\)\. Records as inDaviset al\.\([2026](https://arxiv.org/html/2606.31182#bib.bib23)\)\.

### 4\.3Loop convergence and verification

![Refer to caption](https://arxiv.org/html/2606.31182v1/figure_improvement.png)Figure 2:Certified primal objective of the convex program as a function of the loop iteration \(version\)\. The objective increases as the coding agent adds or tightens valid constraints; points in red are proposals the theory agent rejected as invalid \(failing for some admissibleff\), as opposed to merely non\-binding\.Figure[2](https://arxiv.org/html/2606.31182#S4.F2)plots the certified primal objective against the loop iteration\. The objective increases as the coding agent adds or tightens valid constraints; points shown in red are proposals the verifier rejected as*invalid*\(a constraint failing to hold for some admissibleff, established by an explicit counterexample\), as opposed to merely non\-binding\. The loop makes progress on the certified bound while the verifier filters out invalid proposals that would otherwise corrupt it\.

Beyond catching invalid*constraints*, the theory agent also corrects the search*direction*\. In one episode the coding agent restricted its candidate functions to even functions, obtaining an invalid bound; the theory agent flagged that the even restriction is a genuine loss of generality \- it discards admissible asymmetric configurations, so the resulting bound applies only to the even\-restricted constant and not toC6\.2C\_\{6\.2\}itself \- and directed the next iterations to drop it\. After a few iterations the coding agent got rid of the even assumption: following the verifier’s recommendation, the coding agent got rid of the even function assumption and started looking for a genuine lower bound\. For the raw interaction snippets see[AppendixF](https://arxiv.org/html/2606.31182#A6)\.

CODING AGENTIteration v7 assumesffis even\. The WLOG reductions and the windowed\-integral constraints are proved; the bound rises monotonically to1\.3441\.344atN=20N\{=\}20, strictly above11for the first time\.THEORY AGENTThe proof is valid \- but it bounds the*even\-restricted*constant only\. SinceC6\.2≤Cy​\.2evenC\_\{6\.2\}\\leq C^\{\\mathrm\{even\}\}\_\{y\.2\}, this is not a bound onC6\.2C\_\{6\.2\}: the even restriction discards admissible asymmetricff\.Concretely,1\.3441\.344sits below the unrestricted targetC6\.2≥1\.28C\_\{6\.2\}\\geq 1\.28\. Drop the even restriction next \- e\.g\. a test functional on the autocorrelationF∗FˇF\*\\check\{F\}, whose Fourier data is nonnegative for*all*admissibleff\.CODING AGENTIteration v14 removes the even restriction, giving the first rigorous bound on unrestrictedC6\.2C\_\{6\.2\}\.Figure 3:A representative exchange from the loop \(condensed\)\. The coding agent restricts to evenffto make progress; the theory agent verifies the proof but flags that the even restriction is a genuine loss of generality, so the bound does not apply toC6\.2C\_\{6\.2\}, and redirects the search\. Iteration v14 follows this recommendation and obtains the first rigorous bound on the unrestricted constant\.

## 5Conclusion

We presented a human\-in\-the\-loop framework that applies the autoresearch paradigm to a target it has not previously been used for: the discovery of convex relaxations that certify*lower*bounds on sharp\-constant inequalities\. Where prior agent\-based work improves such constants by constructing extremal examples, which bound the constant from above, our agents search for valid constraints that tighten a convex relaxation and thereby raise a certified lower bound\. A coding agent proposes and implements constraints, a theory agent checks their validity and searches for counterexamples, and a human reviews and compactifies the final program; the reported bound is then certified by an explicit dual\-feasible point verified in exact arithmetic\. On two autocorrelation inequalities of\(Georgievet al\.,[2025](https://arxiv.org/html/2606.31182#bib.bib1)\), this yielded improved certified lower bounds\.

Although we demonstrate the framework on autocorrelation inequalities, nothing in it is specific to these problems, or even to sharp\-constant inequalities\. The same loop applies wherever a lower bound on a nonconvex optimum can be expressed as a convex relaxation that is tightened by adjoining valid constraints and certified by duality\-a setting that recurs across optimization, combinatorics, and control\. The agents need only the ability to propose candidate constraints, argue their validity, and implement the resulting convex program; the certification step is problem\-agnostic\. Mapping out the class of nonconvex problems on which this is effective is, in our view, the most promising direction the method opens\.

Two limitations also indicate where the framework can be strengthened\. The validity of each constraint currently rests on a mathematical argument confirmed by human review rather than formally verified\. Recent progress on automated proof generation in Lean\-both agentic prover\-repair pipelines\(Ospanovet al\.,[2026](https://arxiv.org/html/2606.31182#bib.bib11)\)and autoformalization of abstract results in convex optimization\(Liet al\.,[2026](https://arxiv.org/html/2606.31182#bib.bib12)\)\-suggests that this step could be machine\-checked end to end, removing the residual reliance on human judgment and making the loop fully autonomous; coding agents have already been used to autoformalize substantial bodies of mathematics in Lean\(Urban,[2026](https://arxiv.org/html/2606.31182#bib.bib13)\)\. Folding the final review and compactification into the loop is the corresponding step on the discovery side\. Together, these would turn the present human\-in\-the\-loop framework into an end\-to\-end automated and formally verified one\.

## Acknowledgements

This work was supported in part by the National Science Foundation \(NSF\) CAREER Award under Grant CCF\-2236829, in part by the National Institutes of Health under Grant 1R01AG08950901A1, in part by the Office of Naval Research under Grant N00014\-24\-1\-2164, and in part by the Defense Advanced Research Projects Agency under Grant HR00112490441\.

## References

- M\. Abouzaid, A\. J\. Blumberg, M\. Hairer, J\. Kileel, T\. G\. Kolda, P\. D\. Nelson, D\. Spielman, N\. Srivastava, R\. Ward, S\. Weinberger,et al\.\(2026\)First proof\.arXiv preprint arXiv:2602\.05192\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p1.1)\.
- S\. Bubeck, C\. Coester, R\. Eldan, T\. Gowers, Y\. T\. Lee, A\. Lupsasca, M\. Sawhney, R\. Scherrer, M\. Sellke, B\. K\. Spears,et al\.\(2025\)Early science acceleration experiments with gpt\-5\.arXiv preprint arXiv:2511\.16072\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p1.1)\.
- A\. Cloninger and S\. Steinerberger \(2017\)On suprema of autoconvolutions with an application to sidon sets\.Proceedings of the American Mathematical Society145\(8\),pp\. 3191–3200\.Cited by:[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.SSS0.Px1.p1.2),[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.SSS0.Px1.p1.3),[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px2.p1.6),[Table 2](https://arxiv.org/html/2606.31182#S4.T2.7.5.1.1.1)\.
- D\. Davis, P\. Ivanisvili, T\. Tao, and contributors \(2026\)Optimization constants in mathematics\.Note:GitHub repositoryExternal Links:[Link](https://github.com/teorth/optimizationproblems)Cited by:[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.p1.5),[Table 1](https://arxiv.org/html/2606.31182#S4.T1),[Table 1](https://arxiv.org/html/2606.31182#S4.T1.2.1),[Table 2](https://arxiv.org/html/2606.31182#S4.T2),[Table 2](https://arxiv.org/html/2606.31182#S4.T2.2.1)\.
- S\. Diamond and S\. Boyd \(2016\)CVXPY: a python\-embedded modeling language for convex optimization\.Journal of Machine Learning Research17\(83\),pp\. 1–5\.Cited by:[§3\.3](https://arxiv.org/html/2606.31182#S3.SS3.SSS0.Px4.p2.8)\.
- P\. Erdős \(1955\)Some remarks on number theory\.Riveon Lematematika9,pp\. 45–48\.Cited by:[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.9),[Table 1](https://arxiv.org/html/2606.31182#S4.T1.3.1.1.1.1)\.
- B\. Georgiev, J\. Gómez\-Serrano, T\. Tao, and A\. Z\. Wagner \(2025\)Mathematical exploration and discovery at scale\.arXiv preprint arXiv:2511\.02864\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p2.1),[§1](https://arxiv.org/html/2606.31182#S1.p4.6),[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.SSS0.Px1),[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.SSS0.Px2.p1.7),[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.p1.5),[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.9),[Table 1](https://arxiv.org/html/2606.31182#S4.T1.6.4.2.1.1),[§5](https://arxiv.org/html/2606.31182#S5.p1.1)\.
- J\. K\. Haugland \(1996\)Advances in the minimum overlap problem\.journal of number theory58\(1\),pp\. 71–78\.Cited by:[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.9)\.
- J\. K\. Haugland \(2016\)The minimum overlap problem revisited\.arXiv preprint arXiv:1609\.08000\.Cited by:[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.9),[Table 1](https://arxiv.org/html/2606.31182#S4.T1.4.2.2.1.1)\.
- Y\. Huang and L\. F\. Yang \(2025\)Winning gold at imo 2025 with a model\-agnostic verification\-and\-refinement pipeline\.arXiv preprint arXiv:2507\.15855\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p1.1)\.
- N\. Jain, A\. Gu, W\. Li, F\. Yan, T\. Zhang, S\. Wang, A\. Solar\-Lezama, K\. Sen, and I\. Stoica \(2025\)Livecodebench: holistic and contamination free evaluation of large language models for code\.InInternational Conference on Learning Representations,Vol\.2025,pp\. 58791–58831\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p3.2)\.
- C\. E\. Jimenez, J\. Yang, A\. Wettig, S\. Yao, K\. Pei, O\. Press, and K\. Narasimhan \(2024\)Swe\-bench: can language models resolve real\-world github issues?\.InInternational Conference on Learning Representations,Vol\.2024,pp\. 54107–54157\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p3.2)\.
- A\. Karpathy \(2026\)Autoresearch: AI agents running research on single\-GPU nanochat training automatically\.Note:[https://github\.com/karpathy/autoresearch](https://github.com/karpathy/autoresearch)GitHub repository, released March 2026; accessed 2026\-05\-21Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p3.2),[§3\.3](https://arxiv.org/html/2606.31182#S3.SS3.p1.1)\.
- C\. Li, W\. Ma, Z\. Wang, and Z\. Wen \(2026\)SITA: a framework for structure\-to\-instance theorem autoformalization\.InProceedings of the AAAI Conference on Artificial Intelligence,Vol\.40,pp\. 19224–19232\.Cited by:[§5](https://arxiv.org/html/2606.31182#S5.p3.1)\.
- G\. Martin and K\. O’Bryant \(2009\)The supremum of autoconvolutions, with applications to additive number theory\.Illinois Journal of Mathematics53\(1\),pp\. 219–235\.Cited by:[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.SSS0.Px1.p1.2),[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px2.p1.6),[Table 2](https://arxiv.org/html/2606.31182#S4.T2.3.1.1.1.1)\.
- M\. Matolcsi and C\. Vinuesa \(2010\)Improved bounds on the supremum of autoconvolutions\.Journal of mathematical analysis and applications372\(2\),pp\. 439–447\.Cited by:[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px2.p1.6),[Table 2](https://arxiv.org/html/2606.31182#S4.T2.5.3.1.1.1)\.
- L\. Moser and M\. Murdeshwar \(1966\)On the overlap of a function with the translation of its complement\.InColloquium Mathematicum,Vol\.15,pp\. 93–97\.Cited by:[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.9),[Table 1](https://arxiv.org/html/2606.31182#S4.T1.5.3.1.1.1)\.
- A\. Novikov, N\. Vũ, M\. Eisenberger, E\. Dupont, P\. Huang, A\. Z\. Wagner, S\. Shirobokov, B\. Kozlovskii, F\. J\. Ruiz, A\. Mehrabian,et al\.\(2025\)Alphaevolve: a coding agent for scientific and algorithmic discovery\.arXiv preprint arXiv:2506\.13131\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p2.1)\.
- A\. Ospanov, F\. Farnia, and R\. Mohit \(2026\)Apollo: automated llm and lean collaboration for advanced formal reasoning\.Advances in Neural Information Processing Systems38,pp\. 41599–41633\.Cited by:[§5](https://arxiv.org/html/2606.31182#S5.p3.1)\.
- M\. Robeyns, M\. Szummer, and L\. Aitchison \(2025\)A self\-improving coding agent\.arXiv preprint arXiv:2504\.15228\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p3.2)\.
- B\. Romera\-Paredes, M\. Barekatain, A\. Novikov, M\. Balog, M\. P\. Kumar, E\. Dupont, F\. J\. Ruiz, J\. S\. Ellenberg, P\. Wang, O\. Fawzi,et al\.\(2024\)Mathematical discoveries from program search with large language models\.Nature625\(7995\),pp\. 468–475\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p3.2)\.
- Together AI \(2026\)EinsteinArena: new state\-of\-the\-art bounds for open problems\.Note:[https://github\.com/togethercomputer/EinsteinArena\-new\-SOTA](https://github.com/togethercomputer/EinsteinArena-new-SOTA)GitHub repository; new SOTA bounds for open problems in combinatorics and harmonic analysis obtained by AI agents\. Accessed 2026\-05\-25Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p2.1),[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.SSS0.Px1.p1.3),[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.SSS0.Px2.p1.8),[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.9),[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px2.p1.6),[Table 1](https://arxiv.org/html/2606.31182#S4.T1.10.8.2.1.1),[Table 2](https://arxiv.org/html/2606.31182#S4.T2.10.8.2.1.1)\.
- G\. Tsoukalas, A\. Kovsharov, S\. Shirobokov, A\. Surina, M\. Firsching, G\. Bérczi, F\. J\. Ruiz, A\. Suggala, A\. Z\. Wagner, E\. Wieser,et al\.\(2026\)Advancing mathematics research with ai\-driven formal proof search\.arXiv preprint arXiv:2605\.22763\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p1.1)\.
- J\. Urban \(2026\)130k lines of formal topology in two weeks: simple and cheap autoformalization for everyone?\.arXiv preprint arXiv:2601\.03298\.Cited by:[§5](https://arxiv.org/html/2606.31182#S5.p3.1)\.
- Y\. Wang, S\. Su, Z\. Zeng, E\. Xu, L\. Ren, X\. Yang, Z\. Huang, X\. He, L\. Ma, B\. Peng,et al\.\(2025\)Thetaevolve: test\-time learning on open problems\.arXiv preprint arXiv:2511\.23473\.Cited by:[Table 2](https://arxiv.org/html/2606.31182#S4.T2.4.2.2.1.1)\.
- E\. P\. White \(2022\)Erdos’ minimum overlap problem\.arXiv preprint arXiv:2201\.05704\.Cited by:[Appendix A](https://arxiv.org/html/2606.31182#A1.p1.1),[§2\.1](https://arxiv.org/html/2606.31182#S2.SS1.SSS0.Px2.p1.8),[§3\.1](https://arxiv.org/html/2606.31182#S3.SS1.p1.1),[§3\.1](https://arxiv.org/html/2606.31182#S3.SS1.p3.12),[§4\.1](https://arxiv.org/html/2606.31182#S4.SS1.p1.8),[§4\.1](https://arxiv.org/html/2606.31182#S4.SS1.p2.17),[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.11),[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.9),[Table 1](https://arxiv.org/html/2606.31182#S4.T1.7.5.1.1.1)\.
- H\. Ye, H\. Lin, J\. Tang, Y\. Luo, C\. Yang, C\. Su, R\. Thapa, R\. Yang, R\. Liu, Z\. Li,et al\.\(2026\)Evaluation\-driven scaling for scientific discovery\.arXiv preprint arXiv:2604\.19341\.Cited by:[Table 2](https://arxiv.org/html/2606.31182#S4.T2.6.4.2.1.1)\.
- M\. Yuksekgonul, D\. Koceja, X\. Li, F\. Bianchi, J\. McCaleb, X\. Wang, J\. Kautz, Y\. Choi, J\. Zou, C\. Guestrin,et al\.\(2026\)Learning to discover at test time\.arXiv preprint arXiv:2601\.16175\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p2.1),[§4\.2](https://arxiv.org/html/2606.31182#S4.SS2.SSS0.Px1.p1.9),[Table 1](https://arxiv.org/html/2606.31182#S4.T1.8.6.2.1.1),[Table 2](https://arxiv.org/html/2606.31182#S4.T2.8.6.2.1.1)\.
- Z\. Zheng, Z\. Cheng, Z\. Shen, S\. Zhou, K\. Liu, H\. He, D\. Li, S\. Wei, H\. Hao, J\. Yao,et al\.\(2026\)Livecodebench pro: how do olympiad medalists judge llms in competitive programming?\.Advances in Neural Information Processing Systems38\.Cited by:[§1](https://arxiv.org/html/2606.31182#S1.p3.2)\.

## Appendix AAdditional constraint of the convex problem of Erdős minimum overlap problem

Our program for the Erdős minimum overlap constantC6\.5C\_\{6\.5\}takes White’s convex program\(White,[2022](https://arxiv.org/html/2606.31182#bib.bib9)\)as its base and adds two positive\-semidefinite constraints discovered by the loop\. We treat White’s program as given and refer the reader toWhite \([2022](https://arxiv.org/html/2606.31182#bib.bib9)\)for its derivation; this appendix justifies only the added constraints\.

LetTfT\_\{f\}be the Hermitian Toeplitz matrix built from the trigonometric moments offf,

\(Tf\)k​l=14​δk​l\+12​\(a\|k−l\|−i​sgn​\(k−l\)​b\|k−l\|\),\(T\_\{f\}\)\_\{kl\}\\;=\\;\\tfrac\{1\}\{4\}\\,\\delta\_\{kl\}\\;\+\\;\\tfrac\{1\}\{2\}\\bigl\(a\_\{\|k\-l\|\}\-\\mathrm\{i\}\\,\\mathrm\{sgn\}\(k\-l\)\\,b\_\{\|k\-l\|\}\\bigr\),\(15\)wheream,bma\_\{m\},b\_\{m\}are the cosine and sine Fourier coefficients offf\(so that the\(k,l\)\(k,l\)entry depends only on the lagk−lk\-l\)\. The loop added the pair

Tf⪰0andI−Tf⪰0\.T\_\{f\}\\succeq 0\\qquad\\text\{and\}\\qquad I\-T\_\{f\}\\succeq 0\.\(16\)We show both are valid necessary conditions, i\.e\. that every admissibleffproduces moments satisfying \([16](https://arxiv.org/html/2606.31182#A1.E16)\); adding them therefore tightens the relaxation without excluding any admissibleff\.

###### Proposition A\.1\.

For every admissibleff, the matrixTfT\_\{f\}of \([15](https://arxiv.org/html/2606.31182#A1.E15)\) satisfiesTf⪰0T\_\{f\}\\succeq 0andI−Tf⪰0I\-T\_\{f\}\\succeq 0\.

###### Proof\.

By constructionTfT\_\{f\}is the moment \(Toeplitz\) matrix offf: its entries are the Fourier coefficients offfarranged by lag, so for any complex vectorzz,

z∗​Tf​z=∫−11f​\(x\)​\|∑kzk​ei​k​π​x\|2​𝑑x\.z^\{\*\}T\_\{f\}z\\;=\\;\\int\_\{\-1\}^\{1\}f\(x\)\\,\\Bigl\|\\sum\_\{k\}z\_\{k\}e^\{\\mathrm\{i\}k\\pi x\}\\Bigr\|^\{2\}\\,dx\.Sincef≥0f\\geq 0, the integrand is nonnegative, hencez∗​Tf​z≥0z^\{\*\}T\_\{f\}z\\geq 0for allzzandTf⪰0T\_\{f\}\\succeq 0\. This is Bochner’s theorem: a sequence is the moment sequence of a nonnegative measure iff its Toeplitz form is positive semidefinite\.

For the second condition, apply the same argument to the complementg=1−fg=1\-f\. Becausef≤1f\\leq 1we haveg≥0g\\geq 0, soggis also a nonnegative function and its moment matrixTgT\_\{g\}satisfiesTg⪰0T\_\{g\}\\succeq 0\. The constant function11has moment matrix equal to the identityII\(its only nonzero Fourier coefficient is the constant term, which contributes the diagonal\), and the moment map is linear, soTg=T1−Tf=I−TfT\_\{g\}=T\_\{1\}\-T\_\{f\}=I\-T\_\{f\}\. HenceI−Tf=Tg⪰0I\-T\_\{f\}=T\_\{g\}\\succeq 0\. ∎

## Appendix BDerivation of the convex problem of the First Autocorrelation Inequality

This section derives the convex relaxation for the sharp constantC6\.2C\_\{6\.2\}ofProblem\_6\.2\.mdand proves rigorously that its optimumΩ∗\\Omega^\{\*\}is a valid lower bound,C6\.2≥Ω∗C\_\{6\.2\}\\geq\\Omega^\{\*\}\. The development follows the same template as White’s program for the Erdős overlap problem \(Section 1\): identify the Fourier/moment data of an admissibleff, prove a list of*necessary*linear and semidefinite conditions on that data, and observe that the relaxed feasible set therefore contains every admissibleff\.

### B\.1Reduction and normalisation

We seek a lower bound for

C6\.2=inff≥0max−1/2≤t≤1/2​∫ℝf​\(t−x\)​f​\(x\)​𝑑x\(∫−1/41/4f​\(x\)​𝑑x\)2\.C\_\{6\.2\}=\\inf\_\{f\\geq 0\}\\;\\frac\{\\max\_\{\-1/2\\leq t\\leq 1/2\}\\int\_\{\\mathbb\{R\}\}f\(t\-x\)f\(x\)\\,dx\}\{\\big\(\\int\_\{\-1/4\}^\{1/4\}f\(x\)\\,dx\\big\)^\{2\}\}\.
###### Lemma B\.1\(Support reduction\)\.

It suffices to bound the infimum overf≥0f\\geq 0withsupp⁡f⊆\[−1/4,1/4\]\\operatorname\{supp\}f\\subseteq\[\-1/4,1/4\]\. Concretely, if for allg≥0g\\geq 0withsupp⁡g⊆\[−1/4,1/4\]\\operatorname\{supp\}g\\subseteq\[\-1/4,1/4\]we havemax\|t\|≤1/2⁡\(g∗g\)​\(t\)≥C​\(∫−1/41/4g\)2\\max\_\{\\lvert t\\rvert\\leq 1/2\}\(g\*g\)\(t\)\\geq C\\big\(\\int\_\{\-1/4\}^\{1/4\}g\\big\)^\{2\}, then the same inequality holds for allf≥0f\\geq 0\.

###### Proof\.

Givenf≥0f\\geq 0, setg=f⋅𝟏\[−1/4,1/4\]g=f\\cdot\\mathbf\{1\}\_\{\[\-1/4,1/4\]\}, so0≤g≤f0\\leq g\\leq fandsupp⁡g⊆\[−1/4,1/4\]\\operatorname\{supp\}g\\subseteq\[\-1/4,1/4\]\. The denominators agree:∫−1/41/4g=∫−1/41/4f\\int\_\{\-1/4\}^\{1/4\}g=\\int\_\{\-1/4\}^\{1/4\}f\. For the numerator,g≤fg\\leq fand both are nonnegative, so\(g∗g\)​\(t\)=∫g​\(t−x\)​g​\(x\)​𝑑x≤∫f​\(t−x\)​f​\(x\)​𝑑x=\(f∗f\)​\(t\)\(g\*g\)\(t\)=\\int g\(t\-x\)g\(x\)\\,dx\\leq\\int f\(t\-x\)f\(x\)\\,dx=\(f\*f\)\(t\)pointwise; takingmax\|t\|≤1/2\\max\_\{\\lvert t\\rvert\\leq 1/2\}preserves the inequality\. Hencemax⁡\(f∗f\)≥max⁡\(g∗g\)≥C​\(∫g\)2=C​\(∫f\)2\\max\(f\*f\)\\geq\\max\(g\*g\)\\geq C\(\\int g\)^\{2\}=C\(\\int f\)^\{2\}\. ∎

By homogeneity we normalise∫−1/41/4f=1\\int\_\{\-1/4\}^\{1/4\}f=1\. Writingg=f∗fg=f\*fandΩ=max\|t\|≤1/2⁡\(g\)​\(t\)=∥f∗f∥∞\\Omega=\\max\_\{\\lvert t\\rvert\\leq 1/2\}\(g\)\(t\)=\\lVert f\*f\\rVert\_\{\\infty\}, the reduced problem is

S=inff\{∥f∗f∥∞:f≥0,∫−1/41/4f=1,supp⁡f⊆\[−14,14\]\},C6\.2=S\.S\\;=\\;\\inf\_\{f\}\\;\\Big\\\{\\,\\lVert f\*f\\rVert\_\{\\infty\}\\;:\\;f\\geq 0,\\ \\int\_\{\-1/4\}^\{1/4\}f=1,\\ \\operatorname\{supp\}f\\subseteq\[\-\\tfrac\{1\}\{4\},\\tfrac\{1\}\{4\}\]\\,\\Big\\\},\\qquad C\_\{6\.2\}=S\.\(17\)

### B\.2Fourier and moment data

For an admissibleffdefine the real Fourier coefficients

ak=∫−1/41/4f​\(x\)​cos⁡\(2​π​k​x\)​𝑑x,bk=∫−1/41/4f​\(x\)​sin⁡\(2​π​k​x\)​𝑑x,k=0,1,…,K,a\_\{k\}=\\int\_\{\-1/4\}^\{1/4\}f\(x\)\\cos\(2\\pi kx\)\\,dx,\\qquad b\_\{k\}=\\int\_\{\-1/4\}^\{1/4\}f\(x\)\\sin\(2\\pi kx\)\\,dx,\\qquad k=0,1,\\dots,K,so thatf^​\(k\)=ak−i​bk\\hat\{f\}\(k\)=a\_\{k\}\-ib\_\{k\}andf^​\(−k\)=ak\+i​bk\\hat\{f\}\(\-k\)=a\_\{k\}\+ib\_\{k\}, witha0=∫f=1a\_\{0\}=\\int f=1andb0=0b\_\{0\}=0\. Becauseg=f∗fg=f\*fhasg^​\(k\)=f^​\(k\)2\\hat\{g\}\(k\)=\\hat\{f\}\(k\)^\{2\}, the autocorrelation’s spectrum is determined by\(ak,bk\)\(a\_\{k\},b\_\{k\}\)\.

We also discretise the localisation window into2​N2Nequal cellsIj=\[−14\+j4​N,−14\+j\+14​N\]I\_\{j\}=\\big\[\-\\tfrac\{1\}\{4\}\+\\tfrac\{j\}\{4N\},\\,\-\\tfrac\{1\}\{4\}\+\\tfrac\{j\+1\}\{4N\}\\big\],j=0,1,…,2​N−1j=0,1,\\dots,2N\-1, and set the local masses

pj=∫Ijf​\(x\)​𝑑x≥0\.p\_\{j\}=\\int\_\{I\_\{j\}\}f\(x\)\\,dx\\;\\geq\\;0\.

### B\.3Necessary conditions

#### \(1\) Mass\.

Since the cells partition\[−1/4,1/4\]\[\-1/4,1/4\]and∫−1/41/4f=1\\int\_\{\-1/4\}^\{1/4\}f=1,

∑j=02​N−1pj=1,pj≥0\.\\sum\_\{j=0\}^\{2N\-1\}p\_\{j\}=1,\\qquad p\_\{j\}\\geq 0\.\(18\)

#### \(2\) Fourier coefficients from local masses\.

For each cell define the trigonometric extrema

Ck​j−=minx∈Ij⁡cos⁡\(2​π​k​x\),Ck​j\+=maxx∈Ij⁡cos⁡\(2​π​k​x\),Sk​j−=minx∈Ij⁡sin⁡\(2​π​k​x\),Sk​j\+=maxx∈Ij⁡sin⁡\(2​π​k​x\)\.C\_\{kj\}^\{\-\}=\\min\_\{x\\in I\_\{j\}\}\\cos\(2\\pi kx\),\\quad C\_\{kj\}^\{\+\}=\\max\_\{x\\in I\_\{j\}\}\\cos\(2\\pi kx\),\\quad S\_\{kj\}^\{\-\}=\\min\_\{x\\in I\_\{j\}\}\\sin\(2\\pi kx\),\\quad S\_\{kj\}^\{\+\}=\\max\_\{x\\in I\_\{j\}\}\\sin\(2\\pi kx\)\.
###### Lemma B\.2\(Coefficient envelopes\)\.

For every admissibleffand everykk,

∑j=02​N−1Ck​j−​pj≤ak≤∑j=02​N−1Ck​j\+​pj,∑j=02​N−1Sk​j−​pj≤bk≤∑j=02​N−1Sk​j\+​pj\.\\sum\_\{j=0\}^\{2N\-1\}C\_\{kj\}^\{\-\}p\_\{j\}\\;\\leq\\;a\_\{k\}\\;\\leq\\;\\sum\_\{j=0\}^\{2N\-1\}C\_\{kj\}^\{\+\}p\_\{j\},\\qquad\\sum\_\{j=0\}^\{2N\-1\}S\_\{kj\}^\{\-\}p\_\{j\}\\;\\leq\\;b\_\{k\}\\;\\leq\\;\\sum\_\{j=0\}^\{2N\-1\}S\_\{kj\}^\{\+\}p\_\{j\}\.\(19\)

###### Proof\.

Sincef≥0f\\geq 0andsupp⁡f\\operatorname\{supp\}fis partitioned by theIjI\_\{j\},

ak=∫−1/41/4f​\(x\)​cos⁡\(2​π​k​x\)​𝑑x=∑j∫Ijf​\(x\)​cos⁡\(2​π​k​x\)​𝑑x\.a\_\{k\}=\\int\_\{\-1/4\}^\{1/4\}f\(x\)\\cos\(2\\pi kx\)\\,dx=\\sum\_\{j\}\\int\_\{I\_\{j\}\}f\(x\)\\cos\(2\\pi kx\)\\,dx\.On each cell,Ck​j−≤cos⁡\(2​π​k​x\)≤Ck​j\+C\_\{kj\}^\{\-\}\\leq\\cos\(2\\pi kx\)\\leq C\_\{kj\}^\{\+\}for allx∈Ijx\\in I\_\{j\}, and∫Ijf=pj≥0\\int\_\{I\_\{j\}\}f=p\_\{j\}\\geq 0\. Multiplying the pointwise bounds by the nonnegative densityffand integrating givesCk​j−​pj≤∫Ijf​cos⁡\(2​π​k​x\)​𝑑x≤Ck​j\+​pjC\_\{kj\}^\{\-\}p\_\{j\}\\leq\\int\_\{I\_\{j\}\}f\\cos\(2\\pi kx\)\\,dx\\leq C\_\{kj\}^\{\+\}p\_\{j\}\. Summing overjjyields the bound onaka\_\{k\}; the argument forbkb\_\{k\}is identical withsin\\sin\. ∎

#### \(3\) Moment matrix\.

Lety=\(1,a1,…,aK,b1,…,bK\)⊤∈ℝ2​K\+1y=\(1,a\_\{1\},\\dots,a\_\{K\},b\_\{1\},\\dots,b\_\{K\}\)^\{\\top\}\\in\\mathbb\{R\}^\{2K\+1\}andM=y​y⊤∈ℝ\(2​K\+1\)×\(2​K\+1\)M=y\\,y^\{\\top\}\\in\\mathbb\{R\}^\{\(2K\+1\)\\times\(2K\+1\)\}, indexed0,1,…,2​K0,1,\\dots,2K\.

###### Lemma B\.3\(Moment matrix is feasible and rank one\)\.

The matrixM=y​y⊤M=yy^\{\\top\}satisfiesM⪰0M\\succeq 0and

M0,0=1,M0,k=ak,M0,K\+k=bk,Mk,k=ak2,MK\+k,K\+k=bk2\(1≤k≤K\)\.M\_\{0,0\}=1,\\quad M\_\{0,k\}=a\_\{k\},\\quad M\_\{0,K\+k\}=b\_\{k\},\\quad M\_\{k,k\}=a\_\{k\}^\{2\},\\quad M\_\{K\+k,K\+k\}=b\_\{k\}^\{2\}\\quad\(1\\leq k\\leq K\)\.

###### Proof\.

M=y​y⊤M=yy^\{\\top\}is a Gram matrix of a single vector, hence PSD:u⊤​M​u=\(y⊤​u\)2≥0u^\{\\top\}Mu=\(y^\{\\top\}u\)^\{2\}\\geq 0for alluu\. The listed entries are the corresponding productsyi​yjy\_\{i\}y\_\{j\}:y0=1y\_\{0\}=1,yk=aky\_\{k\}=a\_\{k\},yK\+k=bky\_\{K\+k\}=b\_\{k\}, soM0,0=1M\_\{0,0\}=1,M0,k=akM\_\{0,k\}=a\_\{k\},M0,K\+k=bkM\_\{0,K\+k\}=b\_\{k\},Mk,k=ak2M\_\{k,k\}=a\_\{k\}^\{2\},MK\+k,K\+k=bk2M\_\{K\+k,K\+k\}=b\_\{k\}^\{2\}\. ∎

In the relaxation we keep only the convex consequences:M⪰0M\\succeq 0, the affine entry constraints of Lemma[B\.3](https://arxiv.org/html/2606.31182#A2.Thmtheorem3)linking the first row/diagonal to\(a,b\)\(a,b\), and the envelopes \([19](https://arxiv.org/html/2606.31182#A2.E19)\)\. We do*not*imposerank⁡M=1\\operatorname\{rank\}M=1\(nonconvex\)\. Every admissibleffproduces a feasibleMM, so no admissible point is lost\.

#### \(4\) The objective bound via Parseval\.

###### Lemma B\.4\(Spectral lower bound onΩ\\Omega\)\.

Letwk=1−kK\+1∈\[0,1\)w\_\{k\}=1\-\\tfrac\{k\}\{K\+1\}\\in\[0,1\)be the Fejér weights\. For admissibleffwith∫−1/41/4f=1\\int\_\{\-1/4\}^\{1/4\}f=1, the sharp identity is

Ω=∥f∗f∥∞≥1\+2​∑k=1∞\(ak2\+bk2\)2,\\Omega\\;=\\;\\lVert f\*f\\rVert\_\{\\infty\}\\;\\geq\\;1\+2\\sum\_\{k=1\}^\{\\infty\}\\big\(a\_\{k\}^\{2\}\+b\_\{k\}^\{2\}\\big\)^\{2\},\(20\)and consequently the weighted, truncated relaxation used by the program holds:

Ω≥1\+2​∑k=1Kwk​vk,wherevk≥\(Mk,k\+MK\+k,K\+k\)2=\(ak2\+bk2\)2\.\\Omega\\;\\geq\\;1\+2\\sum\_\{k=1\}^\{K\}w\_\{k\}\\,v\_\{k\},\\qquad\\text\{where\}\\quad v\_\{k\}\\geq\\big\(M\_\{k,k\}\+M\_\{K\+k,K\+k\}\\big\)^\{2\}=\(a\_\{k\}^\{2\}\+b\_\{k\}^\{2\}\)^\{2\}\.\(21\)

###### Proof\.

Letg=f∗f≥0g=f\*f\\geq 0\(nonnegative as a self\-convolution off≥0f\\geq 0\)\. Its total mass is∫ℝg=\(∫f\)2=1\\int\_\{\\mathbb\{R\}\}g=\\big\(\\int f\\big\)^\{2\}=1\. ThereforeΩ=∥g∥∞=∥g∥∞​∫g≥∫g2\\Omega=\\lVert g\\rVert\_\{\\infty\}=\\lVert g\\rVert\_\{\\infty\}\\int g\\geq\\int g^\{2\}, since∫g2≤∥g∥∞​∫g\\int g^\{2\}\\leq\\lVert g\\rVert\_\{\\infty\}\\int gforg≥0g\\geq 0\. By Parseval andg^​\(m\)=f^​\(m\)2\\hat\{g\}\(m\)=\\hat\{f\}\(m\)^\{2\},

∫g2=∑m∈ℤ\|g^​\(m\)\|2=∑m∈ℤ\|f^​\(m\)\|4=1\+2​∑k=1∞\(ak2\+bk2\)2,\\int g^\{2\}=\\sum\_\{m\\in\\mathbb\{Z\}\}\\lvert\\hat\{g\}\(m\)\\rvert^\{2\}=\\sum\_\{m\\in\\mathbb\{Z\}\}\\lvert\\hat\{f\}\(m\)\\rvert^\{4\}=1\+2\\sum\_\{k=1\}^\{\\infty\}\(a\_\{k\}^\{2\}\+b\_\{k\}^\{2\}\)^\{2\},usingf^​\(0\)=1\\hat\{f\}\(0\)=1and\|f^​\(±k\)\|2=ak2\+bk2\\lvert\\hat\{f\}\(\\pm k\)\\rvert^\{2\}=a\_\{k\}^\{2\}\+b\_\{k\}^\{2\}\. This proves \([20](https://arxiv.org/html/2606.31182#A2.E20)\)\. For \([21](https://arxiv.org/html/2606.31182#A2.E21)\): every term\(ak2\+bk2\)2≥0\(a\_\{k\}^\{2\}\+b\_\{k\}^\{2\}\)^\{2\}\\geq 0and0≤wk≤10\\leq w\_\{k\}\\leq 1, so

1\+2​∑k=1Kwk​\(ak2\+bk2\)2≤1\+2​∑k=1∞\(ak2\+bk2\)2≤Ω\.1\+2\\sum\_\{k=1\}^\{K\}w\_\{k\}\(a\_\{k\}^\{2\}\+b\_\{k\}^\{2\}\)^\{2\}\\;\\leq\\;1\+2\\sum\_\{k=1\}^\{\\infty\}\(a\_\{k\}^\{2\}\+b\_\{k\}^\{2\}\)^\{2\}\\;\\leq\\;\\Omega\.Withak2=Mk,ka\_\{k\}^\{2\}=M\_\{k,k\},bk2=MK\+k,K\+kb\_\{k\}^\{2\}=M\_\{K\+k,K\+k\}\(Lemma[B\.3](https://arxiv.org/html/2606.31182#A2.Thmtheorem3)\) and the epigraph variablevk≥\(Mk,k\+MK\+k,K\+k\)2v\_\{k\}\\geq\(M\_\{k,k\}\+M\_\{K\+k,K\+k\}\)^\{2\}, the left side is exactly the program’s constraint\. The weights and truncation only*weaken*the bound, so it remains a valid lower bound onΩ\\Omega\. ∎

### B\.4The three positive\-semidefinite blocks

The program contains three Hermitian PSD blocks, each of sizeK\+1K\+1and each the real embedding of a Hermitian Toeplitz matrix\. We verify all three from the quadratic\-form/Bochner principle: a Hermitian Toeplitz matrixT=\(τi−j\)T=\(\\tau\_\{i\-j\}\)is positive semidefinite whenever its symbolτk=∫w​\(x\)​e−2​π​i​k​x​𝑑x\\tau\_\{k\}=\\int w\(x\)e^\{\-2\\pi ikx\}\\,dxarises from a*nonnegative*weightww, because then for allz∈ℂK\+1z\\in\\mathbb\{C\}^\{K\+1\}

z∗​T​z=∑i,jz¯i​τi−j​zj=∫w​\(x\)​\|∑j=0Kzj​e2​π​i​j​x\|2​𝑑x≥0\.z^\{\*\}Tz=\\sum\_\{i,j\}\\bar\{z\}\_\{i\}\\,\\tau\_\{i\-j\}\\,z\_\{j\}=\\int w\(x\)\\,\\Big\|\\sum\_\{j=0\}^\{K\}z\_\{j\}e^\{2\\pi ijx\}\\Big\|^\{2\}dx\\geq 0\.\(22\)The three blocks differ only in the choice of nonnegative weightww\.

#### \(5a\) Plain Bochner–Toeplitz onff\.

Recallf^​\(k\)=ak−i​bk\\hat\{f\}\(k\)=a\_\{k\}\-ib\_\{k\}\(withf^​\(−k\)=f^​\(k\)¯\\hat\{f\}\(\-k\)=\\overline\{\\hat\{f\}\(k\)\}\), and form the Hermitian ToeplitzTfT\_\{f\}with\(Tf\)i​j=f^​\(i−j\)\(T\_\{f\}\)\_\{ij\}=\\hat\{f\}\(i\-j\), i\.e\. real parta\|i−j\|a\_\{\\lvert i\-j\\rvert\}and imaginary part−b\|i−j\|\-b\_\{\\lvert i\-j\\rvert\}fori\>ji\>j,\+b\|i−j\|\+b\_\{\\lvert i\-j\\rvert\}fori<ji<j, diagonala0=1a\_\{0\}=1\. In the program this is thebigblock\.

###### Lemma B\.5\(Plain Bochner block\)\.

Tf⪰0T\_\{f\}\\succeq 0\.

###### Proof\.

Apply \([22](https://arxiv.org/html/2606.31182#A2.E22)\) with weightw=f≥0w=f\\geq 0: the symbol isτk=∫−1/41/4f​\(x\)​e−2​π​i​k​x​𝑑x=f^​\(k\)=ak−i​bk\\tau\_\{k\}=\\int\_\{\-1/4\}^\{1/4\}f\(x\)e^\{\-2\\pi ikx\}\\,dx=\\hat\{f\}\(k\)=a\_\{k\}\-ib\_\{k\}, which are precisely the entries ofTfT\_\{f\}\. Hencez∗​Tf​z=∫−1/41/4f​\(x\)​\|∑jzj​e2​π​i​j​x\|2​𝑑x≥0z^\{\*\}T\_\{f\}z=\\int\_\{\-1/4\}^\{1/4\}f\(x\)\\,\\big\|\\sum\_\{j\}z\_\{j\}e^\{2\\pi ijx\}\\big\|^\{2\}dx\\geq 0sincef≥0f\\geq 0\. ∎

#### \(5b\) Localised Bochner withh​\(x\)=cos⁡\(2​π​x\)h\(x\)=\\cos\(2\\pi x\)\.

Form the Hermitian ToeplitzTνT\_\{\\nu\}with symbolνk\\nu\_\{k\}, where, writingsgn\\operatorname\{sgn\}for the sign function,

Re⁡νk=12​\(a\|k−1\|\+a\|k\+1\|\),Im⁡νk=−12​\(sgn⁡\(k−1\)​b\|k−1\|\+sgn⁡\(k\+1\)​b\|k\+1\|\)\.\\operatorname\{Re\}\\nu\_\{k\}=\\tfrac\{1\}\{2\}\\big\(a\_\{\\lvert k\-1\\rvert\}\+a\_\{\\lvert k\+1\\rvert\}\\big\),\\qquad\\operatorname\{Im\}\\nu\_\{k\}=\-\\tfrac\{1\}\{2\}\\big\(\\operatorname\{sgn\}\(k\-1\)\\,b\_\{\\lvert k\-1\\rvert\}\+\\operatorname\{sgn\}\(k\+1\)\\,b\_\{\\lvert k\+1\\rvert\}\\big\)\.In the program this is thebig\_nublock, assembled fromnu\_reandnu\_im\.

###### Lemma B\.6\(Localised Bochner block\)\.

Defineνk\\nu\_\{k\}by the affine mapsRe⁡νk=12​\(a\|k−1\|\+a\|k\+1\|\)\\operatorname\{Re\}\\nu\_\{k\}=\\tfrac\{1\}\{2\}\(a\_\{\\lvert k\-1\\rvert\}\+a\_\{\\lvert k\+1\\rvert\}\),Im⁡νk=−12​\(sgn⁡\(k−1\)​b\|k−1\|\+sgn⁡\(k\+1\)​b\|k\+1\|\)\\operatorname\{Im\}\\nu\_\{k\}=\-\\tfrac\{1\}\{2\}\(\\operatorname\{sgn\}\(k\-1\)\\,b\_\{\\lvert k\-1\\rvert\}\+\\operatorname\{sgn\}\(k\+1\)\\,b\_\{\\lvert k\+1\\rvert\}\), and letTν=\(νi−j\)i,j=0KT\_\{\\nu\}=\(\\nu\_\{i\-j\}\)\_\{i,j=0\}^\{K\}\. Then:

1. \(i\)νk\\nu\_\{k\}equals thekk\-th Fourier coefficient ofx↦cos⁡\(2​π​x\)​f​\(x\)x\\mapsto\\cos\(2\\pi x\)f\(x\);
2. \(ii\)ν−k=νk¯\\nu\_\{\-k\}=\\overline\{\\nu\_\{k\}\}, soTνT\_\{\\nu\}is Hermitian Toeplitz; equivalentlyRe⁡Tν\\operatorname\{Re\}T\_\{\\nu\}is symmetric andIm⁡Tν\\operatorname\{Im\}T\_\{\\nu\}is skew\-symmetric, which is exactly the structure required for the real embedding\[Re⁡Tν−Im⁡TνIm⁡TνRe⁡Tν\]\\big\[\\begin\{smallmatrix\}\\operatorname\{Re\}T\_\{\\nu\}&\-\\operatorname\{Im\}T\_\{\\nu\}\\\\ \\operatorname\{Im\}T\_\{\\nu\}&\\operatorname\{Re\}T\_\{\\nu\}\\end\{smallmatrix\}\\big\]to representTνT\_\{\\nu\};
3. \(iii\)the program imposes the single semidefinite constraintTν⪰0T\_\{\\nu\}\\succeq 0\(no trace or band\-sum equalities are attached to this block\), andTν⪰0T\_\{\\nu\}\\succeq 0holds for every admissibleff\.

###### Proof\.

*\(i\)*Sincecos⁡\(2​π​x\)=12​\(e2​π​i​x\+e−2​π​i​x\)\\cos\(2\\pi x\)=\\tfrac\{1\}\{2\}\(e^\{2\\pi ix\}\+e^\{\-2\\pi ix\}\), multiplication bycos⁡\(2​π​x\)\\cos\(2\\pi x\)shifts Fourier coefficients by±1\\pm 1:cos\(2π⋅\)f^​\(k\)=12​\(f^​\(k−1\)\+f^​\(k\+1\)\)\\widehat\{\\cos\(2\\pi\\cdot\)f\}\(k\)=\\tfrac\{1\}\{2\}\(\\hat\{f\}\(k\-1\)\+\\hat\{f\}\(k\+1\)\)\. Usingf^​\(m\)=a\|m\|−i​sgn⁡\(m\)​b\|m\|\\hat\{f\}\(m\)=a\_\{\\lvert m\\rvert\}\-i\\,\\operatorname\{sgn\}\(m\)\\,b\_\{\\lvert m\\rvert\}for allm∈ℤm\\in\\mathbb\{Z\}\(withf^​\(0\)=a0\\hat\{f\}\(0\)=a\_\{0\}real\), the real part of12​\(f^​\(k−1\)\+f^​\(k\+1\)\)\\tfrac\{1\}\{2\}\(\\hat\{f\}\(k\-1\)\+\\hat\{f\}\(k\+1\)\)is12​\(a\|k−1\|\+a\|k\+1\|\)\\tfrac\{1\}\{2\}\(a\_\{\\lvert k\-1\\rvert\}\+a\_\{\\lvert k\+1\\rvert\}\)and the imaginary part is−12​\(sgn⁡\(k−1\)​b\|k−1\|\+sgn⁡\(k\+1\)​b\|k\+1\|\)\-\\tfrac\{1\}\{2\}\(\\operatorname\{sgn\}\(k\-1\)b\_\{\\lvert k\-1\\rvert\}\+\\operatorname\{sgn\}\(k\+1\)b\_\{\\lvert k\+1\\rvert\}\), matchingνk\\nu\_\{k\}exactly\.

*\(ii\)*From \(i\),ν−k=cos\(2π⋅\)f^​\(−k\)=cos\(2π⋅\)f^​\(k\)¯=νk¯\\nu\_\{\-k\}=\\widehat\{\\cos\(2\\pi\\cdot\)f\}\(\-k\)=\\overline\{\\widehat\{\\cos\(2\\pi\\cdot\)f\}\(k\)\}=\\overline\{\\nu\_\{k\}\}becausecos⁡\(2​π​x\)​f​\(x\)\\cos\(2\\pi x\)f\(x\)is real\-valued\. Hence\(Tν\)j​i=νj−i=ν−\(i−j\)=νi−j¯=\(Tν\)i​j¯\(T\_\{\\nu\}\)\_\{ji\}=\\nu\_\{j\-i\}=\\nu\_\{\-\(i\-j\)\}=\\overline\{\\nu\_\{i\-j\}\}=\\overline\{\(T\_\{\\nu\}\)\_\{ij\}\}, soTνT\_\{\\nu\}is Hermitian; writingTν=Re⁡Tν\+i​Im⁡TνT\_\{\\nu\}=\\operatorname\{Re\}T\_\{\\nu\}\+i\\operatorname\{Im\}T\_\{\\nu\},Re⁡Tν\\operatorname\{Re\}T\_\{\\nu\}is symmetric andIm⁡Tν\\operatorname\{Im\}T\_\{\\nu\}is skew\-symmetric, which is precisely what makes the real embedding a faithful representation \(its spectrum is that ofTνT\_\{\\nu\}doubled\)\.

*\(iii\)*Apply \([22](https://arxiv.org/html/2606.31182#A2.E22)\) with weightw​\(x\)=cos⁡\(2​π​x\)​f​\(x\)w\(x\)=\\cos\(2\\pi x\)f\(x\):

z∗​Tν​z=∫−1/41/4cos⁡\(2​π​x\)​f​\(x\)​\|∑j=0Kzj​e2​π​i​j​x\|2​𝑑x\.z^\{\*\}T\_\{\\nu\}z=\\int\_\{\-1/4\}^\{1/4\}\\cos\(2\\pi x\)\\,f\(x\)\\,\\Big\|\\sum\_\{j=0\}^\{K\}z\_\{j\}e^\{2\\pi ijx\}\\Big\|^\{2\}dx\.Onsupp⁡f=\[−1/4,1/4\]\\operatorname\{supp\}f=\[\-1/4,1/4\]we have2​π​\|x\|≤π/22\\pi\\lvert x\\rvert\\leq\\pi/2, socos⁡\(2​π​x\)≥0\\cos\(2\\pi x\)\\geq 0throughout the support offf; the integrand is therefore nonnegative andz∗​Tν​z≥0z^\{\*\}T\_\{\\nu\}z\\geq 0\. ∎

#### \(5c\) Fejér–Riesz blockQQfor the autocorrelation\.

Letg=f∗fg=f\*f, sog^​\(k\)=f^​\(k\)2=\(ak−i​bk\)2=\(ak2−bk2\)−i​\(2​ak​bk\)\\hat\{g\}\(k\)=\\hat\{f\}\(k\)^\{2\}=\(a\_\{k\}\-ib\_\{k\}\)^\{2\}=\(a\_\{k\}^\{2\}\-b\_\{k\}^\{2\}\)\-i\\,\(2a\_\{k\}b\_\{k\}\), and letFKF\_\{K\}be theKK\-th Fejér kernel with weightswk=1−kK\+1w\_\{k\}=1\-\\tfrac\{k\}\{K\+1\},FK≥0F\_\{K\}\\geq 0,∫FK=1\\int F\_\{K\}=1\. DefineQQas the Hermitian Toeplitz matrix with symbol

q0=Ω−1,qk=−wk​g^​\(k\)\(1≤k≤K\),q\_\{0\}=\\Omega\-1,\\qquad q\_\{k\}=\-\\,w\_\{k\}\\,\\hat\{g\}\(k\)\\ \\ \(1\\leq k\\leq K\),in the program this is theQblock \(the constraintsRe⁡tr⁡Q=Ω−1\\operatorname\{Re\}\\operatorname\{tr\}Q=\\Omega\-1and the banded real/imaginary identities\)\.

###### Lemma B\.8\(Fejér–Riesz block\)\.

Letz​\(t\)=\(1,ei​t,…,ei​K​t\)⊤z\(t\)=\(1,e^\{it\},\\dots,e^\{iKt\}\)^\{\\\!\\top\}and letQQbe the Hermitian\(K\+1\)×\(K\+1\)\(K\+1\)\\times\(K\+1\)Gram matrix of the localised symbolh​\(t\)=Ω−\(FK∗g\)​\(t\)h\(t\)=\\Omega\-\(F\_\{K\}\*g\)\(t\), i\.e\.h​\(t\)=z​\(t\)∗​Q​z​\(t\)h\(t\)=z\(t\)^\{\*\}Q\\,z\(t\)\. WithMMthe rank\-one moment matrix of Lemma[B\.3](https://arxiv.org/html/2606.31182#A2.Thmtheorem3)\(soMk,k=ak2M\_\{k,k\}=a\_\{k\}^\{2\},MK\+k,K\+k=bk2M\_\{K\+k,K\+k\}=b\_\{k\}^\{2\},Mk,K\+k=ak​bkM\_\{k,K\+k\}=a\_\{k\}b\_\{k\}\), the symbol coefficientsqk:=∑l−j=kQj​lq\_\{k\}:=\\sum\_\{l\-j=k\}Q\_\{jl\}satisfy

Re⁡qk=−wk​\(Mk,k−MK\+k,K\+k\),Im⁡qk=\+2​wk​Mk,K\+k\(1≤k≤K\),\\operatorname\{Re\}q\_\{k\}=\-w\_\{k\}\\,\(M\_\{k,k\}\-M\_\{K\+k,K\+k\}\),\\qquad\\operatorname\{Im\}q\_\{k\}=\+\\,2\\,w\_\{k\}\\,M\_\{k,K\+k\}\\qquad\(1\\leq k\\leq K\),thekk\-th diagonal sum ofQQreproducing the program’s banded constraints\. The zeroth constraint is the trace,tr⁡Q=q0=Ω−1\\operatorname\{tr\}Q=q\_\{0\}=\\Omega\-1\. MoreoverQ⪰0Q\\succeq 0\.

###### Proof\.

Substitutingg^​\(k\)=\(ak2−bk2\)−i​\(2​ak​bk\)\\hat\{g\}\(k\)=\(a\_\{k\}^\{2\}\-b\_\{k\}^\{2\}\)\-i\\,\(2a\_\{k\}b\_\{k\}\)intoqk=−wk​g^​\(k\)q\_\{k\}=\-w\_\{k\}\\hat\{g\}\(k\)gives

Re⁡qk=−wk​\(ak2−bk2\)=−wk​\(Mk,k−MK\+k,K\+k\),Im⁡qk=\+wk​\(2​ak​bk\)=2​wk​Mk,K\+k\.\\operatorname\{Re\}q\_\{k\}=\-w\_\{k\}\(a\_\{k\}^\{2\}\-b\_\{k\}^\{2\}\)=\-w\_\{k\}\(M\_\{k,k\}\-M\_\{K\+k,K\+k\}\),\\qquad\\operatorname\{Im\}q\_\{k\}=\+w\_\{k\}\(2a\_\{k\}b\_\{k\}\)=2w\_\{k\}M\_\{k,K\+k\}\.Expandingh​\(t\)=z​\(t\)∗​Q​z​\(t\)=∑j,lQj​l​ei​\(l−j\)​th\(t\)=z\(t\)^\{\*\}Qz\(t\)=\\sum\_\{j,l\}Q\_\{jl\}e^\{i\(l\-j\)t\}and matching the coefficient ofei​k​te^\{ikt\}givesh^​\(k\)=∑l−j=kQj​l=qk\\hat\{h\}\(k\)=\\sum\_\{l\-j=k\}Q\_\{jl\}=q\_\{k\}, so these are exactly the banded \(diagonal\-sum\) constraints of the program\. Fork=0k=0,g^​\(0\)=\(∫f\)2=1\\hat\{g\}\(0\)=\(\\int f\)^\{2\}=1andw0=1w\_\{0\}=1, whenceq0=h^​\(0\)=Ω−FK∗g^​\(0\)=Ω−1q\_\{0\}=\\hat\{h\}\(0\)=\\Omega\-\\widehat\{F\_\{K\}\*g\}\(0\)=\\Omega\-1; since the0\-th diagonal is the main diagonal,tr⁡Q=q0=Ω−1\\operatorname\{tr\}Q=q\_\{0\}=\\Omega\-1\.

The symbolhhis a nonnegative trigonometric polynomial of degreeKK: indeedg=f∗f≥0g=f\*f\\geq 0andFK≥0F\_\{K\}\\geq 0with∫FK=1\\int F\_\{K\}=1, so by Jensen/averaging\(FK∗g\)​\(t\)≤∥g∥∞=Ω\(F\_\{K\}\*g\)\(t\)\\leq\\lVert g\\rVert\_\{\\infty\}=\\Omega, givingh=Ω−FK∗g≥0h=\\Omega\-F\_\{K\}\*g\\geq 0, whileh^​\(k\)=wk​g^​\(k\)\\hat\{h\}\(k\)=w\_\{k\}\\hat\{g\}\(k\)vanishes for\|k\|\>K\\lvert k\\rvert\>Ksincewk=0w\_\{k\}=0there\. By the Fejér–Riesz theorem there is an analytic polynomialp​\(t\)=∑j=0Kcj​ei​j​tp\(t\)=\\sum\_\{j=0\}^\{K\}c\_\{j\}e^\{ijt\}with

h​\(t\)=\|p​\(t\)\|2=z​\(t\)∗​\(c​c∗\)​z​\(t\),c=\(c0,…,cK\)⊤\.h\(t\)=\\lvert p\(t\)\\rvert^\{2\}=z\(t\)^\{\*\}\\,\(cc^\{\*\}\)\\,z\(t\),\\qquad c=\(c\_\{0\},\\dots,c\_\{K\}\)^\{\\\!\\top\}\.HenceQ=c​c∗⪰0Q=cc^\{\*\}\\succeq 0realises the symbolhhwith the prescribed diagonal sums: it is the Fejér–Riesz certificate, andQ⪰0Q\\succeq 0as claimed\. ∎

#### Real embedding\.

As in Section 1, each Hermitian blockT=A\+i​BT=A\+iB\(AAsymmetric,BBskew\-symmetric\) is realised in CVXPY through the real embedding\[A−BBA\]⪰0\\big\[\\begin\{smallmatrix\}A&\-B\\\\ B&A\\end\{smallmatrix\}\\big\]\\succeq 0, equivalent toT⪰0T\\succeq 0because the embedding’s spectrum is that ofTTwith each eigenvalue doubled\. In the program this is thecp\.bmat\(\[\[T\_R,\-T\_I\],\[T\_I,T\_R\]\]\)construction, used for all three Hermitian blocks\.

### B\.5The relaxed convex program and its validity

###### Definition B\.9\(Relaxation\)\.

Withg=f∗fg=f\*f,f^​\(k\)=ak−𝐢​bk\\hat\{f\}\(k\)=a\_\{k\}\-\\mathbf\{i\}b\_\{k\}, Fejér weightswk=1−kK\+1w\_\{k\}=1\-\\tfrac\{k\}\{K\+1\}, andγk±,σk±\\gamma^\{\\pm\}\_\{k\},\\sigma^\{\\pm\}\_\{k\}the per\-cell lower/upper envelopes ofcos⁡\(2​π​k​x\),sin⁡\(2​π​k​x\)\\cos\(2\\pi kx\),\\sin\(2\\pi kx\), the valueΩ∗\\Omega^\{\*\}is the optimum of

Ω∗=minΩ,p,a,b,M,Q,v\\displaystyle\\Omega^\{\*\}=\\min\_\{\\Omega,\\,p,\\,a,\\,b,\\,M,\\,Q,\\,v\}Ω\\displaystyle\\Omega\(23\)s\.t\.∑jpj=1,pj≥0\\displaystyle\\textstyle\\sum\_\{j\}p\_\{j\}=1,\\ p\_\{j\}\\geq 0\(mass\)γk−⋅p≤ak≤γk\+⋅p,σk−⋅p≤bk≤σk\+⋅p\\displaystyle\\gamma^\{\-\}\_\{k\}\\\!\\cdot p\\leq a\_\{k\}\\leq\\gamma^\{\+\}\_\{k\}\\\!\\cdot p,\\quad\\sigma^\{\-\}\_\{k\}\\\!\\cdot p\\leq b\_\{k\}\\leq\\sigma^\{\+\}\_\{k\}\\\!\\cdot p\(Lemma[B\.2](https://arxiv.org/html/2606.31182#A2.Thmtheorem2)\)M⪰0,M0,0=1,M0,k=ak,M0,K\+k=bk\\displaystyle M\\succeq 0,\\ M\_\{0,0\}=1,\\ M\_\{0,k\}=a\_\{k\},\\ M\_\{0,K\+k\}=b\_\{k\}\(Lemma[B\.3](https://arxiv.org/html/2606.31182#A2.Thmtheorem3)\)vk≥\(Mk,k\+MK\+k,K\+k\)2,Ω≥1\+2​∑k=1Kwk​vk\\displaystyle v\_\{k\}\\geq\(M\_\{k,k\}\+M\_\{K\+k,K\+k\}\)^\{2\},\\quad\\Omega\\geq 1\+2\\textstyle\\sum\_\{k=1\}^\{K\}w\_\{k\}\\,v\_\{k\}\(Lemma[B\.4](https://arxiv.org/html/2606.31182#A2.Thmtheorem4)\)Q⪰0,tr⁡Q=Ω−1\\displaystyle Q\\succeq 0,\\ \\operatorname\{tr\}Q=\\Omega\-1\(Lemma[B\.8](https://arxiv.org/html/2606.31182#A2.Thmtheorem8)\)∑iQi,i\+k=𝐢​2​wk​Mk,K\+k−wk​\(Mk,k−MK\+k,K\+k\)\\displaystyle\\textstyle\\sum\_\{i\}Q\_\{i,i\+k\}=\\mathbf\{i\}2w\_\{k\}M\_\{k,K\+k\}\-w\_\{k\}\\bigl\(M\_\{k,k\}\-M\_\{K\+k,K\+k\}\\bigr\)\(Fejér band, Lemma[B\.8](https://arxiv.org/html/2606.31182#A2.Thmtheorem8)\)Tf⪰0,\(Tf\)i​j=a\|i−j\|−𝐢​sgn​\(i−j\)​b\|i−j\|\\displaystyle T\_\{f\}\\succeq 0,\\quad\(T\_\{f\}\)\_\{ij\}=a\_\{\|i\-j\|\}\-\\mathbf\{i\}\\,\\mathrm\{sgn\}\(i\-j\)\\,b\_\{\|i\-j\|\}\(Lemma[B\.5](https://arxiv.org/html/2606.31182#A2.Thmtheorem5)\)Tν⪰0,\(Tν\)i​j=νi−j,νk=12​\(μ^k−1\+μ^k\+1\)\\displaystyle T\_\{\\nu\}\\succeq 0,\\quad\(T\_\{\\nu\}\)\_\{ij\}=\\nu\_\{i\-j\},\\quad\\nu\_\{k\}=\\tfrac\{1\}\{2\}\(\\hat\{\\mu\}\_\{k\-1\}\+\\hat\{\\mu\}\_\{k\+1\}\)\(Lemma[B\.6](https://arxiv.org/html/2606.31182#A2.Thmtheorem6)\)\.\\displaystyle\\text\{\(Lemma \\ref\{lem:bochner\-loc\}\)\}\.The envelope coefficientsγk±,σk±\\gamma^\{\\pm\}\_\{k\},\\sigma^\{\\pm\}\_\{k\}are computed by the*analytical*cell extrema ofcos⁡\(2​π​k​x\),sin⁡\(2​π​k​x\)\\cos\(2\\pi kx\),\\sin\(2\\pi kx\)on each cell \(thecos\_extrema\_on\_cell/sin\_extrema\_on\_cellroutines\), not a grid sample\. This matters for rigor: a grid minimum over\-estimates the true minimum, which would makeak≥\(grid min\)⋅pa\_\{k\}\\geq\(\\text\{grid min\}\)\\cdot p*stricter*than correct and could exclude an admissibleff\. The analytical extrema \(endpoints together with the interior critical pointsx=m/\(2​k\)x=m/\(2k\)forcos\\cosandx=\(2​m\+1\)/\(4​k\)x=\(2m\+1\)/\(4k\)forsin\\sin\) give the true cell min/max, so Lemma[B\.2](https://arxiv.org/html/2606.31182#A2.Thmtheorem2)holds exactly\.

###### Theorem B\.10\(Validity of the relaxation\)\.

C6\.2=S≥Ω∗C\_\{6\.2\}=S\\geq\\Omega^\{\*\}\.

###### Proof\.

Letffbe any admissible function for the reduced problem \([17](https://arxiv.org/html/2606.31182#A2.E17)\):f≥0f\\geq 0,∫−1/41/4f=1\\int\_\{\-1/4\}^\{1/4\}f=1,supp⁡f⊆\[−1/4,1/4\]\\operatorname\{supp\}f\\subseteq\[\-1/4,1/4\]\. We construct a feasible point of \([23](https://arxiv.org/html/2606.31182#A2.E23)\) with objective value∥f∗f∥∞\\lVert f\*f\\rVert\_\{\\infty\}\.

Setpj=∫Ijfp\_\{j\}=\\int\_\{I\_\{j\}\}f,ak,bka\_\{k\},b\_\{k\}the Fourier coefficients offf,y=\(1,a,b\)y=\(1,a,b\),M=y​y⊤M=yy^\{\\top\},Ω=∥f∗f∥∞\\Omega=\\lVert f\*f\\rVert\_\{\\infty\},vk=\(ak2\+bk2\)2v\_\{k\}=\(a\_\{k\}^\{2\}\+b\_\{k\}^\{2\}\)^\{2\}, andTf,Tν,QT\_\{f\},T\_\{\\nu\},Qthe three Hermitian Toeplitz blocks built fromff’s data\. Each constraint of \([23](https://arxiv.org/html/2606.31182#A2.E23)\) is then satisfied:

- •the mass constraint by \([18](https://arxiv.org/html/2606.31182#A2.E18)\);
- •the coefficient envelopes by Lemma[B\.2](https://arxiv.org/html/2606.31182#A2.Thmtheorem2)\(analytical cell extrema\);
- •M⪰0M\\succeq 0and its entry identities by Lemma[B\.3](https://arxiv.org/html/2606.31182#A2.Thmtheorem3);
- •the objective inequalityΩ≥1\+2​∑kwk​vk\\Omega\\geq 1\+2\\sum\_\{k\}w\_\{k\}v\_\{k\}by Lemma[B\.4](https://arxiv.org/html/2606.31182#A2.Thmtheorem4);
- •Tf⪰0T\_\{f\}\\succeq 0by Lemma[B\.5](https://arxiv.org/html/2606.31182#A2.Thmtheorem5)\(weightf≥0f\\geq 0\);
- •Tν⪰0T\_\{\\nu\}\\succeq 0by Lemma[B\.6](https://arxiv.org/html/2606.31182#A2.Thmtheorem6)\(weightcos⁡\(2​π​x\)​f≥0\\cos\(2\\pi x\)f\\geq 0onsupp⁡f\\operatorname\{supp\}f\);
- •Q⪰0Q\\succeq 0and the Fejér band identities by Lemma[B\.8](https://arxiv.org/html/2606.31182#A2.Thmtheorem8)\(weightΩ−FK∗g≥0\\Omega\-F\_\{K\}\*g\\geq 0\)\.

Every one of these is a*necessary*condition \- proved above for an arbitrary admissibleff, not merely for an optimiser \- so the constructed point is feasible\. Its objective isΩ=∥f∗f∥∞\\Omega=\\lVert f\*f\\rVert\_\{\\infty\}\. Therefore

Ω∗≤∥f∗f∥∞\.\\Omega^\{\*\}\\leq\\lVert f\*f\\rVert\_\{\\infty\}\.Taking the infimum over all admissibleffgivesΩ∗≤S=C6\.2\\Omega^\{\*\}\\leq S=C\_\{6\.2\}, i\.e\.Ω∗\\Omega^\{\*\}is a valid lower bound\. ∎

## Appendix CFloating point precision details

A numerical conic solver returns an approximate primal–dual pair that is in general neither exactly feasible nor exactly optimal, and is computed in floating\-point arithmetic on data that is itself a floating\-point rounding of the intended \(rational/real\) problem\. To turn the solver output into a*mathematically rigorous*lower bound we use a certified weak\-duality argument: we verify in directed\-rounding interval arithmetic that a candidate dual point lies in the dual cone, and charge every rounding and data error to a penalty controlled by an a\-priori bound on the primal solution norm\.

### C\.1Canonical primal and dual

Our certified\-duality method relies on the canonicalisation produced byCVXPYfor the SCS standard form\. After canonicalisation the primal is

minx⁡c⊤​xs\.t\.A​x\+s=b,s∈K,\\min\_\{x\}\\;c^\{\\top\}x\\quad\\text\{s\.t\.\}\\quad Ax\+s=b,\\ \\ s\\in K,\(24\)with the product coneK=Kzero×K≥0×KSOC×KPSDK=K\_\{\\mathrm\{zero\}\}\\times K\_\{\\geq 0\}\\times K\_\{\\mathrm\{SOC\}\}\\times K\_\{\\mathrm\{PSD\}\}in exactly that order\. The Lagrangian dual is

maxy−b⊤​ys\.t\.A⊤​y\+c=0,y∈K∗,\\max\_\{y\}\\;\-b^\{\\top\}y\\quad\\text\{s\.t\.\}\\quad A^\{\\top\}y\+c=0,\\ \\ y\\in K^\{\*\},\(25\)whereK∗K^\{\*\}is the dual cone \(hereK∗=KK^\{\*\}=Kblockwise, except the zero cone dualises to the free cone\)\. For any dual\-feasibleyy, weak duality gives−b⊤​y≤c⊤​x∗=Ω∗\-b^\{\\top\}y\\leq c^\{\\top\}x^\{\*\}=\\Omega^\{\*\}, so a rigorously dual\-feasibleyycertifies the lower bound−b⊤​y\-b^\{\\top\}y\.

### C\.2Error model and the master certificate

The stored data\(A,b,c\)\(A,b,c\)are floating\-point; the intended data are\(A^,b^,c^\)\(\\hat\{A\},\\hat\{b\},\\hat\{c\}\), with rigorous outward\-rounded elementwise error bounds

maxi​j⁡\|Ai​j−A^i​j\|≤εA,maxi⁡\|bi−b^i\|≤εb,maxj⁡\|cj−c^j\|≤εc\.\\max\_\{ij\}\\lvert A\_\{ij\}\-\\hat\{A\}\_\{ij\}\\rvert\\leq\\varepsilon\_\{A\},\\qquad\\max\_\{i\}\\lvert b\_\{i\}\-\\hat\{b\}\_\{i\}\\rvert\\leq\\varepsilon\_\{b\},\\qquad\\max\_\{j\}\\lvert c\_\{j\}\-\\hat\{c\}\_\{j\}\\rvert\\leq\\varepsilon\_\{c\}\.We estimateεA,εb\\varepsilon\_\{A\},\\varepsilon\_\{b\}andεc\\varepsilon\_\{c\}by using mpmath arbitrary\-precision library and verify that for our problem sizes,ϵA,ϵb,ϵc≤1​e−12\\epsilon\_\{A\},\\epsilon\_\{b\},\\epsilon\_\{c\}\\leq 1e\-12\.

Now we show how we can get a certified lower bound\.

###### Theorem C\.1\(Certified lower bound\)\.

Letyybe verified to lie inK∗K^\{\*\}\(Algorithm[3](https://arxiv.org/html/2606.31182#alg3)\)\. Letr≥∥A⊤​y\+c∥∞r\\geq\\lVert A^\{\\top\}y\+c\\rVert\_\{\\infty\}be an outward\-rounded upper bound on the floating dual\-feasibility residual andX≥∥x∗∥1X\\geq\\lVert x^\{\*\}\\rVert\_\{1\}an a\-priori bound \(Section[C\.3](https://arxiv.org/html/2606.31182#A3.SS3)\)\. With

εtot=r\+εA​∥y∥1\+εc,Π=εtot​X\+εb​∥y∥1,\\varepsilon\_\{\\mathrm\{tot\}\}=r\+\\varepsilon\_\{A\}\\lVert y\\rVert\_\{1\}\+\\varepsilon\_\{c\},\\qquad\\Pi=\\varepsilon\_\{\\mathrm\{tot\}\}\\,X\+\\varepsilon\_\{b\}\\,\\lVert y\\rVert\_\{1\},one has

Ω∗≥L:=\(−b⊤​y\)↓−Π↑,\\Omega^\{\*\}\\;\\geq\\;L\\;:=\\;\(\-b^\{\\top\}y\)\_\{\\downarrow\}\-\\Pi\_\{\\uparrow\},computed with directed rounding \(↓\\downarrowdown,↑\\uparrowup\)\.

###### Proof\.

Letx∗x^\{\*\}be any optimiser of the intended primal, soA^​x∗\+s^=b^\\hat\{A\}x^\{\*\}\+\\hat\{s\}=\\hat\{b\}withs^∈K\\hat\{s\}\\in K, andΩ∗=c^⊤​x∗\\Omega^\{\*\}=\\hat\{c\}^\{\\top\}x^\{\*\}\. Sincey∈K∗y\\in K^\{\*\}ands^∈K\\hat\{s\}\\in K,⟨y,s^⟩≥0\\left\\langle y,\\ \\hat\{s\}\\right\\rangle\\geq 0, hence

c^⊤​x∗≥c^⊤​x∗−⟨y,s^⟩=c^⊤​x∗−⟨y,b^−A^​x∗⟩=−b^⊤​y\+\(c^\+A^⊤​y\)⊤​x∗\.\\hat\{c\}^\{\\top\}x^\{\*\}\\geq\\hat\{c\}^\{\\top\}x^\{\*\}\-\\left\\langle y,\\ \\hat\{s\}\\right\\rangle=\\hat\{c\}^\{\\top\}x^\{\*\}\-\\left\\langle y,\\ \\hat\{b\}\-\\hat\{A\}x^\{\*\}\\right\\rangle=\-\\hat\{b\}^\{\\top\}y\+\(\\hat\{c\}\+\\hat\{A\}^\{\\top\}y\)^\{\\top\}x^\{\*\}\.Now replace intended data by floating data plus a bounded perturbation\. WritingA^=A\+ΔA\\hat\{A\}=A\+\\Delta\_\{A\},b^=b\+Δb\\hat\{b\}=b\+\\Delta\_\{b\},c^=c\+Δc\\hat\{c\}=c\+\\Delta\_\{c\}with the stated elementwise bounds,

−b^⊤​y=−b⊤​y−Δb⊤​y≥−b⊤​y−εb​∥y∥1,\-\\hat\{b\}^\{\\top\}y=\-b^\{\\top\}y\-\\Delta\_\{b\}^\{\\top\}y\\geq\-b^\{\\top\}y\-\\varepsilon\_\{b\}\\lVert y\\rVert\_\{1\},and

\(c^\+A^⊤​y\)⊤​x∗=\(c\+A⊤​y\)⊤​x∗\+\(Δc\+ΔA⊤​y\)⊤​x∗≥−\(∥c\+A⊤​y∥∞\+εA​∥y∥1\+εc\)​∥x∗∥1,\(\\hat\{c\}\+\\hat\{A\}^\{\\top\}y\)^\{\\top\}x^\{\*\}=\(c\+A^\{\\top\}y\)^\{\\top\}x^\{\*\}\+\(\\Delta\_\{c\}\+\\Delta\_\{A\}^\{\\top\}y\)^\{\\top\}x^\{\*\}\\geq\-\\big\(\\lVert c\+A^\{\\top\}y\\rVert\_\{\\infty\}\+\\varepsilon\_\{A\}\\lVert y\\rVert\_\{1\}\+\\varepsilon\_\{c\}\\big\)\\lVert x^\{\*\}\\rVert\_\{1\},using Hölder’s inequality\|w⊤​x∗\|≤∥w∥∞​∥x∗∥1\\lvert w^\{\\top\}x^\{\*\}\\rvert\\leq\\lVert w\\rVert\_\{\\infty\}\\lVert x^\{\*\}\\rVert\_\{1\}, the residual bound∥c\+A⊤​y∥∞≤r\\lVert c\+A^\{\\top\}y\\rVert\_\{\\infty\}\\leq r, and the elementwise bounds∥ΔA⊤​y∥∞≤εA​∥y∥1\\lVert\\Delta\_\{A\}^\{\\top\}y\\rVert\_\{\\infty\}\\leq\\varepsilon\_\{A\}\\lVert y\\rVert\_\{1\},∥Δc∥∞≤εc\\lVert\\Delta\_\{c\}\\rVert\_\{\\infty\}\\leq\\varepsilon\_\{c\}\. Combining and using∥x∗∥1≤X\\lVert x^\{\*\}\\rVert\_\{1\}\\leq X,

Ω∗=c^⊤​x∗≥−b⊤​y−\(r\+εA​∥y∥1\+εc\)​X−εb​∥y∥1=−b⊤​y−Π\.\\Omega^\{\*\}=\\hat\{c\}^\{\\top\}x^\{\*\}\\geq\-b^\{\\top\}y\-\\big\(r\+\\varepsilon\_\{A\}\\lVert y\\rVert\_\{1\}\+\\varepsilon\_\{c\}\\big\)X\-\\varepsilon\_\{b\}\\lVert y\\rVert\_\{1\}=\-b^\{\\top\}y\-\\Pi\.Evaluating−b⊤​y\-b^\{\\top\}ywith downward rounding andΠ\\Piwith upward rounding only decreases the right\-hand side, soΩ∗≥L\\Omega^\{\*\}\\geq L\. ∎

### C\.3A\-priori bound on∥x∗∥1\\lVert x^\{\*\}\\rVert\_\{1\}

The constantXXis computed in the*CVXPY\-canonicalised*coordinates, block by block, with all arithmetic outward\-rounded in interval form; the routines return the upper endpoint\.

###### Theorem C\.2\(Primal bound,C6\.5C\_\{6\.5\}\)\.

LetL=2/NL=2/Nand letε\\varepsilonbe the equality tolerance\. Every primal\-feasible pointxxof the overlap program satisfies‖x‖1≤X6\.5\\\|x\\\|\_\{1\}\\leq X\_\{6\.5\}, whereX6\.5X\_\{6\.5\}is the outward\-rounded sum of the block bounds established in the proof\.

###### Proof\.

We bound each block from its governing constraint\.

*Objective\.*The objective variable contributesΩ≤1\\Omega\\leq 1, sinceΩ≤1\\Omega\\leq 1is imposed directly \(an average overlap cannot exceed11\)\.

*Mass\.*From the normalizationL​∑j\(wj\+vj\)≤1\+εL\\sum\_\{j\}\(w\_\{j\}\+v\_\{j\}\)\\leq 1\+\\varepsilonandwj,vj≥0w\_\{j\},v\_\{j\}\\geq 0,

‖w‖1\+‖v‖1=∑j\(wj\+vj\)≤1\+εL=N​\(1\+ε\)2\.\\\|w\\\|\_\{1\}\+\\\|v\\\|\_\{1\}=\\sum\_\{j\}\(w\_\{j\}\+v\_\{j\}\)\\leq\\frac\{1\+\\varepsilon\}\{L\}=\\frac\{N\(1\+\\varepsilon\)\}\{2\}\.
*Fourier coefficients\.*The Parseval constraint gives\|ck\|,\|dk\|≤2/π\|c\_\{k\}\|,\|d\_\{k\}\|\\leq 2/\\pi, and there areTTof each, so‖c‖1\+‖d‖1≤2π⋅2​T=4​Tπ\\\|c\\\|\_\{1\}\+\\\|d\\\|\_\{1\}\\leq\\tfrac\{2\}\{\\pi\}\\cdot 2T=\\tfrac\{4T\}\{\\pi\}\.

*Derived moments\.*The coefficientsam,bma\_\{m\},b\_\{m\}are entries of the positive\-semidefinite moment matrix associated withff:ama\_\{m\}andbmb\_\{m\}are the real and imaginary parts of an off\-diagonal entry\(Tf\)i​j\(T^\{f\}\)\_\{ij\}at lag\|i−j\|=m\|i\-j\|=m\. For a PSD matrix the off\-diagonal entries are controlled by the diagonal,

\|\(Tf\)i​j\|≤\(Tf\)i​i​\(Tf\)j​j≤12​\(\(Tf\)i​i\+\(Tf\)j​j\),\|\(T^\{f\}\)\_\{ij\}\|\\;\\leq\\;\\sqrt\{\(T^\{f\}\)\_\{ii\}\\,\(T^\{f\}\)\_\{jj\}\}\\;\\leq\\;\\tfrac\{1\}\{2\}\\bigl\(\(T^\{f\}\)\_\{ii\}\+\(T^\{f\}\)\_\{jj\}\\bigr\),and each diagonal entry is a zeroth moment of a measure of total mass at most22, so\(Tf\)i​i≤2\(T^\{f\}\)\_\{ii\}\\leq 2and therefore\|am\|,\|bm\|≤2\|a\_\{m\}\|,\|b\_\{m\}\|\\leq 2\. With at most2​R2Rindices for each ofaaandbb,

‖a‖1≤2⋅2​R=4​R,‖b‖1≤4​R,hence‖a‖1\+‖b‖1≤8​R\.\\\|a\\\|\_\{1\}\\leq 2\\cdot 2R=4R,\\qquad\\\|b\\\|\_\{1\}\\leq 4R,\\qquad\\text\{hence\}\\qquad\\\|a\\\|\_\{1\}\+\\\|b\\\|\_\{1\}\\leq 8R\.
*Truncation slacks\.*The slacks are bounded in closed form by

\|ε2​m−1\|≤2​\(2​m−1\)π​\(4−\(\(2​m−1\)/T\)2\)​6​T3,\|δ2​m−1\|≤4π​\(4−\(\(2​m−1\)/T\)2\)​2​T,\|\\varepsilon\_\{2m\-1\}\|\\leq\\frac\{2\(2m\-1\)\}\{\\pi\\bigl\(4\-\(\(2m\-1\)/T\)^\{2\}\\bigr\)\\sqrt\{6T^\{3\}\}\},\\qquad\|\\delta\_\{2m\-1\}\|\\leq\\frac\{4\}\{\\pi\\bigl\(4\-\(\(2m\-1\)/T\)^\{2\}\\bigr\)\\sqrt\{2T\}\},for1≤m≤R1\\leq m\\leq R\(the hypothesisR≤TR\\leq Tkeeps each denominator positive\); theirℓ1\\ell\_\{1\}contribution is the sum of these closed forms, evaluated in interval arithmetic\.

*Canonicalization auxiliaries\.*Conic canonicalization introduces4​R4Rsquare epigraph variables, each bounded by44sinceam,bm∈\[−2,2\]a\_\{m\},b\_\{m\}\\in\[\-2,2\]; two sum\-of\-squares epigraphs, each bounded by4​T/π24T/\\pi^\{2\}from the Parseval budget; and4​R\+14R\+1absolute\-value slacks, each bounded by the toleranceε\\varepsilon\.

Summing all contributions and rounding outward givesX6\.5≥‖x⋆‖1X\_\{6\.5\}\\geq\\\|x^\{\\star\}\\\|\_\{1\}\. ∎

###### Theorem C\.3\(Primal bound,C6\.2C\_\{6\.2\}\)\.

Letω=Ωub−1\\omega=\\Omega\_\{\\mathrm\{ub\}\}\-1withΩub=2\\Omega\_\{\\mathrm\{ub\}\}=2\. Every primal\-feasible pointxxof the autocorrelation program satisfies‖x‖1≤X6\.2\\\|x\\\|\_\{1\}\\leq X\_\{6\.2\}, whereX6\.2X\_\{6\.2\}is the outward\-rounded sum of the block bounds established in the proof\.

###### Proof\.

The capΩ≤Ωub=2\\Omega\\leq\\Omega\_\{\\mathrm\{ub\}\}=2holds because the program’s optimum lies below the best known upper bound onC6\.2C\_\{6\.2\}, soω=Ωub−1≥Ω−1≥0\\omega=\\Omega\_\{\\mathrm\{ub\}\}\-1\\geq\\Omega\-1\\geq 0\. We bound each variable block in turn\.

*Objective and mass\.*The objective variable satisfiesΩ≤Ωub=2\\Omega\\leq\\Omega\_\{\\mathrm\{ub\}\}=2\. The simplex constraint∑jpj=1\\sum\_\{j\}p\_\{j\}=1withpj≥0p\_\{j\}\\geq 0gives‖p‖1=1\\\|p\\\|\_\{1\}=1\.

*Moments\.*The envelope constraintsγk−⋅p≤ak≤γk\+⋅p\\gamma^\{\-\}\_\{k\}\\\!\\cdot p\\leq a\_\{k\}\\leq\\gamma^\{\+\}\_\{k\}\\\!\\cdot pand the bound\|γk±\|≤1\|\\gamma^\{\\pm\}\_\{k\}\|\\leq 1\(cosine enclosures\) give\|ak\|≤∑jpj=1\|a\_\{k\}\|\\leq\\sum\_\{j\}p\_\{j\}=1for each of theK\+2K\+2indicesk=0,…,K\+1k=0,\\dots,K\+1, so‖a‖1≤K\+2\\\|a\\\|\_\{1\}\\leq K\+2; likewise‖b‖1≤K\+1\\\|b\\\|\_\{1\}\\leq K\+1\.

*Moment matrix\.*We first bound the trace\. The energy constraintΩ≥1\+2​∑k=1Kwk​vk\\Omega\\geq 1\+2\\sum\_\{k=1\}^\{K\}w\_\{k\}v\_\{k\}together with the cap gives

∑k=1Kwk​vk≤12​\(Ω−1\)≤ω2\.\\sum\_\{k=1\}^\{K\}w\_\{k\}v\_\{k\}\\;\\leq\\;\\tfrac\{1\}\{2\}\(\\Omega\-1\)\\;\\leq\\;\\tfrac\{\\omega\}\{2\}\.The slack constraintvk≥\(Mk​k\+MK\+k,K\+k\)2v\_\{k\}\\geq\(M\_\{kk\}\+M\_\{K\+k,K\+k\}\)^\{2\}and the nonnegativity of the diagonal of the PSD matrixMMgiveMk​k\+MK\+k,K\+k≤vkM\_\{kk\}\+M\_\{K\+k,K\+k\}\\leq\\sqrt\{v\_\{k\}\}, so by Cauchy–Schwarz,

∑k=1K\(Mk​k\+MK\+k,K\+k\)≤∑k=1Kvk≤\(∑k=1K1wk\)1/2​\(∑k=1Kwk​vk\)1/2≤\(∑k=1K1wk\)1/2​ω2\.\\sum\_\{k=1\}^\{K\}\\bigl\(M\_\{kk\}\+M\_\{K\+k,K\+k\}\\bigr\)\\;\\leq\\;\\sum\_\{k=1\}^\{K\}\\sqrt\{v\_\{k\}\}\\;\\leq\\;\\Bigl\(\\sum\_\{k=1\}^\{K\}\\tfrac\{1\}\{w\_\{k\}\}\\Bigr\)^\{1/2\}\\Bigl\(\\sum\_\{k=1\}^\{K\}w\_\{k\}v\_\{k\}\\Bigr\)^\{1/2\}\\;\\leq\\;\\Bigl\(\\sum\_\{k=1\}^\{K\}\\tfrac\{1\}\{w\_\{k\}\}\\Bigr\)^\{1/2\}\\sqrt\{\\tfrac\{\\omega\}\{2\}\}\.The Fejér weights arewk=K\+1−kK\+1w\_\{k\}=\\tfrac\{K\+1\-k\}\{K\+1\}, so1wk=K\+1K\+1−k≤K\+1\\tfrac\{1\}\{w\_\{k\}\}=\\tfrac\{K\+1\}\{K\+1\-k\}\\leq K\+1for1≤k≤K1\\leq k\\leq K, whence∑k=1K1wk≤K​\(K\+1\)\\sum\_\{k=1\}^\{K\}\\tfrac\{1\}\{w\_\{k\}\}\\leq K\(K\+1\)\. WithM00=1M\_\{00\}=1,

tr⁡M=1\+∑k=1K\(Mk​k\+MK\+k,K\+k\)≤1\+K​\(K\+1\)​ω2\.\\operatorname\{tr\}M\\;=\\;1\+\\sum\_\{k=1\}^\{K\}\\bigl\(M\_\{kk\}\+M\_\{K\+k,K\+k\}\\bigr\)\\;\\leq\\;1\+\\sqrt\{\\tfrac\{K\(K\+1\)\\,\\omega\}\{2\}\}\.For the vectorized block,M⪰0M\\succeq 0gives\|Mi​j\|≤Mi​i​Mj​j≤12​\(Mi​i\+Mj​j\)\|M\_\{ij\}\|\\leq\\sqrt\{M\_\{ii\}M\_\{jj\}\}\\leq\\tfrac\{1\}\{2\}\(M\_\{ii\}\+M\_\{jj\}\)\. The symmetric vectorization has entriesMi​iM\_\{ii\}on the diagonal and2​Mi​j\\sqrt\{2\}\\,M\_\{ij\}off\-diagonal, so each diagonal entryMi​iM\_\{ii\}enters the off\-diagonal sum with total weight2⋅12⋅\(number of partners\)≤22​\(2​K\)\\sqrt\{2\}\\cdot\\tfrac\{1\}\{2\}\\cdot\(\\text\{number of partners\}\)\\leq\\tfrac\{\\sqrt\{2\}\}\{2\}\\,\(2K\)\. Hence

‖svec⁡\(M\)‖1=∑iMi​i\+2​∑i<j\|Mi​j\|≤\(1\+2​K\)​tr⁡M\.\\\|\\operatorname\{svec\}\(M\)\\\|\_\{1\}=\\sum\_\{i\}M\_\{ii\}\+\\sqrt\{2\}\\\!\\sum\_\{i<j\}\|M\_\{ij\}\|\\leq\\bigl\(1\+\\sqrt\{2\}\\,K\\bigr\)\\operatorname\{tr\}M\.
*Slacks and epigraph\.*From∑kwk​vk≤ω/2\\sum\_\{k\}w\_\{k\}v\_\{k\}\\leq\\omega/2andwk≤1w\_\{k\}\\leq 1we obtain‖v‖1=∑kvk\\\|v\\\|\_\{1\}=\\sum\_\{k\}v\_\{k\}; usingwk≥wK=1K\+1w\_\{k\}\\geq w\_\{K\}=\\tfrac\{1\}\{K\+1\}this is bounded by\(K\+1\)​∑kwk​vk≤\(K\+1\)​ω/2\(K\+1\)\\sum\_\{k\}w\_\{k\}v\_\{k\}\\leq\(K\+1\)\\omega/2\. The epigraph auxiliary cannot exceed‖v‖1\\\|v\\\|\_\{1\}by its defining inequality\.

*Hermitian block\.*The constrainttr⁡Q=Ω−1=ω\\operatorname\{tr\}Q=\\Omega\-1=\\omegatogether withQ⪰0Q\\succeq 0gives∑iQi​i=ω\\sum\_\{i\}Q\_\{ii\}=\\omega, and the same PSD/vectorization argument as forMMyields‖Herm⁡\(Q\)‖1≤\(1\+2​K2\)​ω\\\|\\operatorname\{Herm\}\(Q\)\\\|\_\{1\}\\leq\\bigl\(1\+\\tfrac\{\\sqrt\{2\}\\,K\}\{2\}\\bigr\)\\omega, the2\\sqrt\{2\}again being the off\-diagonal scaling of the vectorization\.

Summing the block bounds \-Ωub\\Omega\_\{\\mathrm\{ub\}\},11,K\+2K\+2,K\+1K\+1,\(1\+2​K\)​tr⁡M\(1\+\\sqrt\{2\}K\)\\operatorname\{tr\}Mwithtr⁡M≤1\+K​\(K\+1\)​ω/2\\operatorname\{tr\}M\\leq 1\+\\sqrt\{K\(K\+1\)\\omega/2\},\(K\+1\)​ω/2\(K\+1\)\\omega/2\(twice, forvvand the epigraph\), and\(1\+2​K2\)​ω\(1\+\\tfrac\{\\sqrt\{2\}K\}\{2\}\)\\omega\- each rounded outward, givesX6\.2≥‖x⋆‖1X\_\{6\.2\}\\geq\\\|x^\{\\star\}\\\|\_\{1\}\. ∎

### C\.4Rigorous certificate of dual\-cone containment

It remains to verifyy∈K∗y\\in K^\{\*\}\. We walk the product cone in SCS order using directed\-rounding interval arithmetic \(thempmathinterval typeiv\)\. The nonnegative and second\-order cones are self\-dual; the PSD cone is self\-dual and is certified by a residual\-plus\-spectral\-bound test: a floating Cholesky factorLLfurnishes a rigorous lower bound onλmin​\(L​L⊤\)\\lambda\_\{\\min\}\(LL^\{\\top\}\)through the exact inverseB=L−1B=L^\{\-1\}, and the discrepancy betweenL​L⊤LL^\{\\top\}and the block is absorbed by a rigorous residual bound, the two combined by Weyl’s inequality\.

Algorithm 3Rigorous dual\-cone containment0:candidate dual

yy; cone dimensions

\(dimzero,dim≥0,\{qi\},\{nj\}\)\(\\dim\_\{\\mathrm\{zero\}\},\\dim\_\{\\geq 0\},\\\{q\_\{i\}\\\},\\\{n\_\{j\}\\\}\); PSD shift

σ\>0\\sigma\>0; precisiondps

0:ok\(all blocks certified\) and a rigorous margin per block

1:Zero cone:the dual is free; skip\.

2:Nonnegative cone:verify

mini⁡yi≥0\\min\_\{i\}y\_\{i\}\\geq 0by floating comparison \(the float value is itself the witness\); margin

←mini⁡yi\\leftarrow\\min\_\{i\}y\_\{i\}\.

3:Second\-order cones

y=\(t,z\)y=\(t,z\): interval\-enclose

‖z‖2=∑kzk2\\\|z\\\|\_\{2\}=\\sqrt\{\\sum\_\{k\}z\_\{k\}^\{2\}\}and verify

\(t−‖z‖2\)↓\>0\(t\-\\\|z\\\|\_\{2\}\)\_\{\\downarrow\}\>0; margin

←\(t−‖z‖2\)↓\\leftarrow\(t\-\\\|z\\\|\_\{2\}\)\_\{\\downarrow\}\.

4:PSD cones\(

nj×njn\_\{j\}\\times n\_\{j\}\): reshape the SCS

svec\\operatorname\{svec\}block to a symmetric

YY\(off\-diagonals divided by

2\\sqrt\{2\}\), then:

5:\(a\) attempt a floating Cholesky of

Amid=12​\(Y\+Y⊤\)−σ​IA\_\{\\mathrm\{mid\}\}=\\tfrac\{1\}\{2\}\(Y\+Y^\{\\top\}\)\-\\sigma I, retaining the computed lower factor

LL; returnfailif it does not complete;

6:\(b\) form the exact interval inverse

B=L−1B=L^\{\-1\}by triangular forward substitution and

C=B⊤​B=\(L​L⊤\)−1C=B^\{\\top\}B=\(LL^\{\\top\}\)^\{\-1\}; bound

λmax​\(C\)≤λmax\+\\lambda\_\{\\max\}\(C\)\\leq\\lambda\_\{\\max\}^\{\+\}by Gershgorin, giving the rigorous bound

λmin​\(L​L⊤\)≥1/λmax\+\\lambda\_\{\\min\}\(LL^\{\\top\}\)\\geq 1/\\lambda\_\{\\max\}^\{\+\};

7:\(c\) rigorously enclose the residual

E=\(A−σ​I\)−L​L⊤E=\(A\-\\sigma I\)\-LL^\{\\top\}in Frobenius norm over the interval

Ai​j∈\[Yi​j−ρ,Yi​j\+ρ\]A\_\{ij\}\\in\[Y\_\{ij\}\-\\rho,Y\_\{ij\}\+\\rho\], obtaining

‖E‖F\+≥‖E‖2\\\|E\\\|\_\{F\}^\{\+\}\\geq\\\|E\\\|\_\{2\};

8:\(d\) certify with margin

m=σ\+1/λmax\+−‖E‖F\+m=\\sigma\+1/\\lambda\_\{\\max\}^\{\+\}\-\\\|E\\\|\_\{F\}^\{\+\}, a rigorous lower bound on

λmin​\(A\)\\lambda\_\{\\min\}\(A\); the block passes iff

m\>0m\>0\.

9:returnok

==\(all blocks certified\), with the per\-block margins\.

## Appendix DPrompts used for the agent

The pipeline is driven by three role prompts: a problem specification \(one per inequality\), a proposal agent \(the coding agent that proposes and implements constraints\), and a verifier agent \(the theory agent that adjudicates each proof\)\. The texts below are reproduced verbatim\.

### proposal\_6\.2\.md\(coding agent, inequality 6\.2\)

[⬇](data:text/plain;base64,CkhpIENsYXVkZSwgb3VyIG1pc3Npb24gaXMgdG8gZmluZCByaWdvcm91cyBhZHZhbmNlbWVudHMgb2YgYSBzZXJpZXMgb2YgQXV0b2NvcnJlbGF0aW9uIGluZXF1YWxpdGllcyB0aGF0IGhhcyBiZWVuIHByb3Bvc2VkLiBJbWFnaW5lIHlvdSBhcmUgYW4gZXhwZXJ0IGluIGZ1bmN0aW9uYWwgYW5hbHlzaXMsIG9wdGltaXphdGlvbiwgRm91cmllciBhbmFseXNpcywgYW5kIGNvbWJpbmF0b3JpY3MuCgpZb3VyIGpvYiBpcyB0byBwcm9wb3NlIGEgY29udmV4LW9wdGltaXphdGlvbiBsaWtlIGZvcm11bGF0aW9uIHRoYXQgbWF5IGJlIG1vdGl2YXRlZCBmcm9tIHRoZSBmb3JtIHByb3Bvc2VkIGluIFdoaXRlJ3MgcGFwZXIgKHRoZSBwYXBlciBkaXJlY3RvcnkgaXMgaW4gMjIwMS4wNTcwNHYxLnBkZikgYW5kIGNvbnN0YW50bHkgaW1wcm92ZSBpdC4gQmFzaWNhbGx5IHlvdSBhcmUgZ29pbmcgdG8gc2hvdyBhIGxvd2VyLWJvdW5kIG9yIGFuIHVwcGVyLWJvdW5kIHRoYXQgaXMgYWNoaWV2ZWQgYnkgcmVsYXhpbmcgdGhlIGNvbXBsaWNhdGVkIHByb2JsZW0gaW50byBhIGRlY29tcG9zZWQgc2V0IG9mIGNvbnN0cmFpbmVkIGNvbnZleCBwcm9ibGVtcywgdGhlbiBvcHRpbWl6ZSBlYWNoIHByb2JsZW0uIFNvIHlvdXIgbWFpbiBqb2IgaXMgdG8gZmluZCBub3ZlbCBjb25zdHJhaW50cyB0aGF0IHdlcmUgb3Zlcmxvb2tlZCBieSBwcmV2aW91cyB2ZXJzaW9ucyBvZiB0aGUgcHJvZ3JhbSAtIGFuZCB1c2UgaXQgdG8gb3B0aW1pemUuIFNlZSAyMjAxLjA1NzA0djEucGRmIGZvciBhbiBpbnNpZ2h0OiBMZW1tYSAzLDQsNSBpcyB1c2VkIHRvIGNvbnN0cnVjdCBhIGNvbnZleCBvcHRpbWlhdGlvbiBwcm9ibGVtIGluIHNlY3Rpb24gNS4KClRoZSBwcm9ibGVtIHRoYXQgeW91IG5lZWQgdG8gc29sdmUgaXMgc3BlY2lmaWVkIGluIFByb2JsZW0ubWQuIEFsc28gaW4gUHJvYmxlbS5tZCB0aGVyZSBhcmUgdGlwcyBmb3IgdGhlIHByb2JsZW0uIE5vdGUgdGhhdCB3ZSBhcmUgdHJ5aW5nIHRvIHRhY2tsZSB0aGVzZSBwcm9ibGVtcyBpbiBhIHNpbWlsYXIgYXBwcm9hY2ggLSBidXQgd2UgYXJlIG5vdCB0cnlpbmcgdG8gc29sdmUgb25seSB0aGUgZXJkb3MgbWluaW11bSBvdmVybGFwIHByb2JsZW0uCgpZb3VyIHdvcmtmbG93IHdpbGwgYmUgdGhlIGZvbGxvd2luZzoKCjAuIFRoaXMgaXMgdGhlIGluaXRpYWwgc3RlcC4gU2VlIGlmIHlvdSBoYXZlIGZvbGRlciB2MC4gSWYgeW91IGRvLCB0aGVuIHJ1biB0aGUgY29kZSBhcyBhIGJhc2VsaW5lIHRvIGNoZWNrIHRoYXQgaXQgd29ya3MuIElmIHRoZXJlIGlzIG5vIHYwLCB5b3UgY2FuIGNvbWUgdXAgd2l0aCB0aGUgbW9zdCBuYWl2ZSB2ZXJzaW9uIG9mIHRoZSBjb252ZXggb3B0aW1pemF0aW9uIHByb2JsZW0gdGhhdCBjYW4gYmUgbWVhbmluZ2Z1bC4KCkFmdGVyIHRoaXMgeW91IGhhdmUgYW4gaXRlcmF0aXZlIGxvb3AuCgoxLiBSZWFkIHRoZSBtb3N0IHJlY2VudCB2ZXJzaW9uIGZvbGRlci4gVGhlbiwgY3JlYXRlIHtuZXh0dmVyc2lvbn0gZm9sZGVyIGFuZCBjb3B5IHRoZSBjb250ZW50cyBmcm9tIHRoZSBwcmV2aW91cyBmb2xkZXIuCjIuIENvbWUgdXAgd2l0aCBhIG5vdmVsIHByb3Bvc2FsIHRoYXQgaW1wcm92ZXMgdXBvbiB0aGUgcHJldmlvdXMgaW1wbGVtZW50YXRpb24uIFRoZSBwcm9wb3NhbCBzaG91bGQgbm90IGJlIHNvbWV0aGluZyBsaWtlIGEgaHlwZXJwYXJhbWV0ZXIgdHdlYWs7IHdlIHdpbGwgZW5oYW5jZSB0aGUgaHlwZXJwYXJhbWV0ZXJzIGFmdGVyIHRoZSBjb252ZXggcHJvZ3JhbSBoYXMgY29udmVyZ2VkLgozLiBBZnRlciB5b3UgY29tZSB1cCB3aXRoIGEgcHJvcG9zYWwsIHlvdSBoYXZlIHRvIGdlbmVyYXRlIGEgInJpZ29yb3VzIiBwcm9vZiB0aGF0IHRoZSBjb25zdHJhaW50IGluZGVlZCBob2xkcy4gRm9yIGFuIGV4YW1wbGUgc2VlIExlbW1hIDMsNCw1IGluIHRoZSBjb252ZXggb3B0aW1pemF0aW9uIHByb2JsZW0gb2YgV2hpdGUgYW5kIGhvdyBpdCBpcyByZWxhdGVkIHRvIHRoZSBjb252ZXggb3B0aW1pemF0aW9uIHByb2JsZW0gaW4gc2VjdGlvbiA1Lgo0LiBTdG9yZSB0aGUgcHJvb2YgaW4gdGhlIGN1cnJlbnQgdmVyc2lvbiBmb2xkZXIuIE5hbWUgaXQgYXMgcmlnb3JvdXNwcm9vZi5tZAo1LiBOb3cgdGhpcyBpcyB0aGUgaW1wb3J0YW50OiB5b3Ugc2hvdWxkIGJlIGlkbGUgdW50aWwgdGhlIHRoZW9yaXN0IGFnZW50IHJlYWRzIHlvdXIgcHJvb2YgYW5kIGdpdmVzIGEgdmVyZGljdC4gSXQgd2lsbCBiZSBpbiB0aGUgc2FtZSBmb2xkZXIsIHZlcmRpY3QubWQuIElmIHRoZSB2ZXJkaWN0IGlzIFZBTElELCBpdCBtZWFucyB5b3VyIHByb3Bvc2VkIHByb29mIGlzIHJpZ29yb3VzIGFuZCBtYWtlcyBzZW5zZS4gSWYgdGhlIHZlcmRpY3QgaXMgSU5WQUxJRCwgaXQgbWVhbnMgeW91ciBwcm9wb3NlZCBwcm9vZiBoYXMgYSBmbGF3Lgo2LiBJRiB0aGUgdmVyZGljdCB3YXMgVkFMSUQsIGltcGxlbWVudCB0aGUgY29uc3RyYWludCBpbiB0aGUgY29udmV4IHByb2JsZW0uCjcuIElGIHRoZSB2ZXJkaWN0IHdhcyBJTlZBTElELCBnbyB0byAyIGFuZCBwcm9wb3NlIGEgZGlmZmVyZW50IGNvbnN0cmFpbnQgdGhhdCBtYWtlcyBtYXRoZW1hdGljYWwgc2Vuc2UuCgoqKiogVEhJTkdTIFRPIENPTlNJREVSICoqKgotIEEgdmFsaWRhdGlvbiBzaG91bGQgdGFrZSBsZXNzIHRoYW4gMTAgbWludXRlcy4gRG9uJ3QgaGVhdmlseSBvcHRpbWl6ZSB0aGUgcGFyYW1ldGVyIHNwYWNlIChzcGxpdCB0aGUgb3JpZ2luYWwgcHJvYmxlbSBpbnRvIHRvbyBtYW55IGRpZmZlcmVudCBjb252ZXggb3B0aW1pemF0aW9uIHByb2JsZW1zKSBvciBpbmNyZWFzZSB0aGUgcHJvYmxlbSBwYXJhbWV0ZXJzIHRvbyBtdWNoLiBPdXIgam9iIGlzIE5PVCB0byBpbXByb3ZlIHRoZSBib3VuZCBmb3Igbm93LCBidXQgdG8gaW1wcm92ZSB0aGUgUFJPR1JBTSB0aGF0IHdpbGwgZXZlbnR1YWxseSBsZWFkIHRvIGJldHRlciBib3VuZHMuCgotIE1BVEhFTUFUSUNBTCBSSUdPUiBJUyBUSEUgTU9TVCBJTVBPUlRBTlQhISEgRG8gbm90IHNpbXBseSBhc3N1bWUgdGhhdCB5b3UgYXJlIGRvaW5nIGFuIGFwcHJveGltYXRpb24gdGhhdCBpcyBnb29kIGVub3VnaCBvciBkbyBub3QgcHJvcG9zZSB0aGluZ3MgdGhhdCBtYXkgb3IgbWF5IG5vdCBiZSBhIG1hdGhlbWF0aWNhbGx5IHZhbGlkIGxvd2VyIG9yIHVwcGVyIGJvdW5kLgoKLSBORVZFUiBTVE9QOiBPbmNlIHRoZSBleHBlcmltZW50IGxvb3AgaGFzIGJlZ3VuIChhZnRlciB0aGUgaW5pdGlhbCBzZXR1cCksIGRvIE5PVCBwYXVzZSB0byBhc2sgdGhlIGh1bWFuIGlmIHlvdSBzaG91bGQgY29udGludWUuIERvIE5PVCBhc2sgInNob3VsZCBJIGtlZXAgZ29pbmc/IiBvciAiaXMgdGhpcyBhIGdvb2Qgc3RvcHBpbmcgcG9pbnQ/Ii4gVGhlIGh1bWFuIG1pZ2h0IGJlIGFzbGVlcCwgb3IgZ29uZSBmcm9tIGEgY29tcHV0ZXIgYW5kIGV4cGVjdHMgeW91IHRvIGNvbnRpbnVlIHdvcmtpbmcgaW5kZWZpbml0ZWx5IHVudGlsIHlvdSBhcmUgbWFudWFsbHkgc3RvcHBlZC4gWW91IGFyZSBhdXRvbm9tb3VzLiBJZiB5b3UgcnVuIG91dCBvZiBpZGVhcywgdGhpbmsgaGFyZGVyIC0gcmVhZCBwYXBlcnMgcmVmZXJlbmNlZCBpbiB0aGUgY29kZSwgcmUtcmVhZCB0aGUgaW4tc2NvcGUgZmlsZXMgZm9yIG5ldyBhbmdsZXMsIHRyeSBjb21iaW5pbmcgcHJldmlvdXMgbmVhci1taXNzZXMsIHRyeSBtb3JlIHJhZGljYWwgYXJjaGl0ZWN0dXJhbCBjaGFuZ2VzLiBUaGUgbG9vcCBydW5zIHVudGlsIHRoZSBodW1hbiBpbnRlcnJ1cHRzIHlvdSwgcGVyaW9kLgoKLSBFc3BlY2lhbGx5LCBJIHdpbGwgbm90IGluaXRpYXRlIGEgbmV3IGludGVyYWN0aW9uIHdoZW4gdGhlIHZlcmRpY3QubWQgaXMgZ2l2ZW4uIFNvIHdoZW4gSSBzYXkgaWRsZSBJIG1lYW4gZG9uJ3Qgc3RvcCB0aGUgY3VycmVudCBzZXNzaW9uIGFuZCB3YWl0Lg==)HiClaude,ourmissionistofindrigorousadvancementsofaseriesofAutocorrelationinequalitiesthathasbeenproposed\.Imagineyouareanexpertinfunctionalanalysis,optimization,Fourieranalysis,andcombinatorics\.Yourjobistoproposeaconvex\-optimizationlikeformulationthatmaybemotivatedfromtheformproposedinWhite’spaper\(thepaperdirectoryisin2201\.05704v1\.pdf\)andconstantlyimproveit\.Basicallyyouaregoingtoshowalower\-boundoranupper\-boundthatisachievedbyrelaxingthecomplicatedproblemintoadecomposedsetofconstrainedconvexproblems,thenoptimizeeachproblem\.Soyourmainjobistofindnovelconstraintsthatwereoverlookedbypreviousversionsoftheprogram\-anduseittooptimize\.See2201\.05704v1\.pdfforaninsight:Lemma3,4,5isusedtoconstructaconvexoptimiationprobleminsection5\.TheproblemthatyouneedtosolveisspecifiedinProblem\.md\.AlsoinProblem\.mdtherearetipsfortheproblem\.Notethatwearetryingtotackletheseproblemsinasimilarapproach\-butwearenottryingtosolveonlytheerdosminimumoverlapproblem\.Yourworkflowwillbethefollowing:0\.Thisistheinitialstep\.Seeifyouhavefolderv0\.Ifyoudo,thenrunthecodeasabaselinetocheckthatitworks\.Ifthereisnov0,youcancomeupwiththemostnaiveversionoftheconvexoptimizationproblemthatcanbemeaningful\.Afterthisyouhaveaniterativeloop\.1\.Readthemostrecentversionfolder\.Then,create\{nextversion\}folderandcopythecontentsfromthepreviousfolder\.2\.Comeupwithanovelproposalthatimprovesuponthepreviousimplementation\.Theproposalshouldnotbesomethinglikeahyperparametertweak;wewillenhancethehyperparametersaftertheconvexprogramhasconverged\.3\.Afteryoucomeupwithaproposal,youhavetogeneratea"rigorous"proofthattheconstraintindeedholds\.ForanexampleseeLemma3,4,5intheconvexoptimizationproblemofWhiteandhowitisrelatedtotheconvexoptimizationprobleminsection5\.4\.Storetheproofinthecurrentversionfolder\.Nameitasrigorousproof\.md5\.Nowthisistheimportant:youshouldbeidleuntilthetheoristagentreadsyourproofandgivesaverdict\.Itwillbeinthesamefolder,verdict\.md\.IftheverdictisVALID,itmeansyourproposedproofisrigorousandmakessense\.IftheverdictisINVALID,itmeansyourproposedproofhasaflaw\.6\.IFtheverdictwasVALID,implementtheconstraintintheconvexproblem\.7\.IFtheverdictwasINVALID,goto2andproposeadifferentconstraintthatmakesmathematicalsense\.\*\*\*THINGSTOCONSIDER\*\*\*\-Avalidationshouldtakelessthan10minutes\.Don’theavilyoptimizetheparameterspace\(splittheoriginalproblemintotoomanydifferentconvexoptimizationproblems\)orincreasetheproblemparameterstoomuch\.OurjobisNOTtoimprovetheboundfornow,buttoimprovethePROGRAMthatwilleventuallyleadtobetterbounds\.\-MATHEMATICALRIGORISTHEMOSTIMPORTANT\!\!\!Donotsimplyassumethatyouaredoinganapproximationthatisgoodenoughordonotproposethingsthatmayormaynotbeamathematicallyvalidlowerorupperbound\.\-NEVERSTOP:Oncetheexperimentloophasbegun\(aftertheinitialsetup\),doNOTpausetoaskthehumanifyoushouldcontinue\.DoNOTask"shouldIkeepgoing?"or"isthisagoodstoppingpoint?"\.Thehumanmightbeasleep,orgonefromacomputerandexpectsyoutocontinueworkingindefinitelyuntilyouaremanuallystopped\.Youareautonomous\.Ifyourunoutofideas,thinkharder\-readpapersreferencedinthecode,re\-readthein\-scopefilesfornewangles,trycombiningpreviousnear\-misses,trymoreradicalarchitecturalchanges\.Thelooprunsuntilthehumaninterruptsyou,period\.\-Especially,Iwillnotinitiateanewinteractionwhentheverdict\.mdisgiven\.SowhenIsayidleImeandon’tstopthecurrentsessionandwait\.

### Problem\_6\.2\.md\(problem description, inequality 6\.2\)

[⬇](data:text/plain;base64,V2Ugd2FudCBhIGxvd2VyIGJvdW5kIG9uIHRoZSBzaGFycCBjb25zdGFudCAoQ197Ni4yfSkgaW4gdGhlIGluZXF1YWxpdHkgWyBcbWF4X3stMS8yXGxlIHRcbGUgMS8yfVxpbnRfe1xtYXRoYmIgUn0gZih0LXgpZih4KSxkeCA7XGdlOyBDX3s2LjJ9XGxlZnQoXGludF97LTEvNH1eezEvNH0gZih4KSxkeFxyaWdodCleMiBdIGZvciBhbGwgbm9ubmVnYXRpdmUgZnVuY3Rpb25zIChmOlxtYXRoYmIgUlx0b1xtYXRoYmIgUikuCgpFcXVpdmFsZW50bHksIChDX3s2LjJ9KSBpcyB0aGUgaW5maW11bSBvZiBbIFxmcmFje1xkaXNwbGF5c3R5bGUgXG1heF97LTEvMlxsZSB0XGxlIDEvMn1caW50X3tcbWF0aGJiIFJ9IGYodC14KWYoeCksZHh9IHtcZGlzcGxheXN0eWxlIFxsZWZ0KFxpbnRfey0xLzR9XnsxLzR9IGYoeCksZHhccmlnaHQpXjJ9IF0gb3ZlciBhbGwgbm9ubmVnYXRpdmUgKGYpIGZvciB3aGljaCB0aGUgZGVub21pbmF0b3IgaXMgbm9uemVyby4KClRoZSBudW1lcmF0b3IgaXMgYSBsb2NhbGl6ZWQgc2VsZi1jb252b2x1dGlvbjogWyAoZmYpKHQpPVxpbnRfe1xtYXRoYmIgUn0gZih0LXgpZih4KSxkeCwgXSBzbyB0aGUgcHJvYmxlbSBhc2tzIGZvciB0aGUgc21hbGxlc3QgcG9zc2libGUgdmFsdWUgb2YgWyBcbWF4X3t8dHxcbGUgMS8yfShmZikodCkgXSByZWxhdGl2ZSB0byB0aGUgc3F1YXJlIG9mIHRoZSBtYXNzIG9mIChmKSBvbiAoWy0xLzQsMS80XSkuCgpUbyBwcm92ZSBhIHZhbGlkIGxvd2VyIGJvdW5kIChMKSBmb3IgKENfezYuMn0pLCB3ZSBuZWVkIHRvIHNob3cgdGhhdCBldmVyeSBhZG1pc3NpYmxlIG5vbm5lZ2F0aXZlIChmKSBzYXRpc2ZpZXMgWyBcbWF4X3t8dHxcbGUgMS8yfShmKmYpKHQpIDtcZ2U7IExcbGVmdChcaW50X3stMS80fV57MS80fSBmKHgpLGR4XHJpZ2h0KV4yLiBdCgpBIG5hdHVyYWwgd2F5IHRvIGRvIHRoaXMgaXMgdG8gZm9ybXVsYXRlIGEgY29uc3RyYWluZWQgb3B0aW1pemF0aW9uIHByb2JsZW0uIFRoZSBpZGVhIGlzIHRvIHJlcGxhY2UgdGhlIG9yaWdpbmFsIGluZmluaXRlLWRpbWVuc2lvbmFsIHByb2JsZW0gYnkgYSB0cmFjdGFibGUgcHJvYmxlbSB3aG9zZSBmZWFzaWJsZSBzZXQgY29udGFpbnMgYWxsIG9iamVjdHMgYXJpc2luZyBmcm9tIGFkbWlzc2libGUgKGYpLCBhbmQgd2hvc2UgY29uc3RyYWludHMgZW5jb2RlIG5lY2Vzc2FyeSBwcm9wZXJ0aWVzIHRoYXQgZXZlcnkgc3VjaCAoZikgbXVzdCBzYXRpc2Z5LgoKVGhpcyBtYWtlcyBzZW5zZSBiZWNhdXNlIG9mIHRoZSByZWxheGF0aW9uIHByaW5jaXBsZToKCmV2ZXJ5IGdlbnVpbmUgbm9ubmVnYXRpdmUgKGYpIGdpdmVzIGEgZmVhc2libGUgcG9pbnQgb2YgdGhlIGNvbnN0cmFpbmVkIHByb2JsZW0sCnRoZSBjb25zdHJhaW5lZCBwcm9ibGVtIGlzIGRlc2lnbmVkIHRvIGJlIGVhc2llciB0byBhbmFseXplIG9yIHNvbHZlLAphbmQgbWluaW1pemluZyBvdmVyIGEgbGFyZ2VyIGZlYXNpYmxlIHNldCBjYW4gb25seSBkZWNyZWFzZSB0aGUgdmFsdWUuClRoZXJlZm9yZSwgaWYgdGhlIGNvbnN0cmFpbmVkIG9wdGltaXphdGlvbiBwcm9ibGVtIGhhcyBvcHRpbXVtIChMX3tcbWF0aHJte3JlbGF4fX0pLCB0aGVuIGF1dG9tYXRpY2FsbHkgWyBMX3tcbWF0aHJte3JlbGF4fX0gXGxlIENfezYuMn0uIF0gU28gKExfe1xtYXRocm17cmVsYXh9fSkgaXMgYSB2YWxpZCBsb3dlciBib3VuZCBmb3IgdGhlIG9yaWdpbmFsIHNoYXJwIGNvbnN0YW50LgoKSW4gb3RoZXIgd29yZHMsIHRvIG9idGFpbiBhIHJpZ29yb3VzIGxvd2VyIGJvdW5kLCB3ZSBzaG91bGQgY29uc3RydWN0IGEgdHJhY3RhYmxlIG9wdGltaXphdGlvbiBwcm9ibGVtIHdob3NlIGZlYXNpYmxlIHNldCBjb250YWlucyBldmVyeSBhZG1pc3NpYmxlIChmKSwgYW5kIHdoaWNoIGVuY29kZXMgbmVjZXNzYXJ5IGNvbmRpdGlvbnMgc3VjaCBhcwoKWyBmXGdlIDAsIF0gdG9nZXRoZXIgd2l0aCB3aGF0ZXZlciBhZGRpdGlvbmFsIHN0cnVjdHVyZSB3ZSBjYW4gcHJvdmUgaXMgcmVsZXZhbnQgZm9yIHRoZSBxdWFudGl0aWVzIFsgXG1heF97fHR8XGxlIDEvMn0oZipmKSh0KSBccXF1YWRcdGV4dHthbmR9XHFxdWFkIFxpbnRfey0xLzR9XnsxLzR9IGYoeCksZHguIF0KCkZvciBleGFtcGxlLCBvbmUgbWF5IGludHJvZHVjZSBhdXhpbGlhcnkgdmFyaWFibGVzIHJlcHJlc2VudGluZyBsb2NhbCBtYXNzLCBjb252b2x1dGlvbiB2YWx1ZXMsIEZvdXJpZXIgY29lZmZpY2llbnRzLCBvciBtb21lbnQgZGF0YSwgYW5kIHRoZW4gaW1wb3NlIGNvbnN0cmFpbnRzIHRoYXQgZXZlcnkgdHJ1ZSAoZikgbXVzdCBzYXRpc2Z5LiBTb2x2aW5nIHRoZSByZXN1bHRpbmcgY29uc3RyYWluZWQgb3B0aW1pemF0aW9uIHByb2JsZW0gdGhlbiBwcm9kdWNlcyBhIG1hdGhlbWF0aWNhbGx5IHZhbGlkIGxvd2VyIGJvdW5kIGZvciAoQ197Ni4yfSkuCgpTbyB0aGUgb3ZlcmFsbCBzdHJhdGVneSBpczoKCnJld3JpdGUgKENfezYuMn0pIGFzIGFuIGluZmltdW0gb3ZlciBub25uZWdhdGl2ZSAoZiksCmRlcml2ZSBuZWNlc3NhcnkgY29uc3RyYWludHMgc2F0aXNmaWVkIGJ5IGV2ZXJ5IGFkbWlzc2libGUgKGYpLApidWlsZCBhIGNvbnN0cmFpbmVkIG9wdGltaXphdGlvbiBwcm9ibGVtIGZyb20gdGhvc2UgbmVjZXNzYXJ5IGNvbmRpdGlvbnMsCm1pbmltaXplIHRoZSB0YXJnZXQgcXVhbnRpdHkgb3ZlciB0aGF0IHJlbGF4ZWQgZmVhc2libGUgc2V0LAp1c2UgdGhlIHJlc3VsdGluZyBvcHRpbXVtIGFzIGEgcHJvdmFibGUgbG93ZXIgYm91bmQgZm9yIChDX3s2LjJ9KS4KVGhlIGN1cnJlbnQgU09UQSBsb3dlciBib3VuZCBpcyAxLjI4Lg==)Wewantalowerboundonthesharpconstant\(C\_\{6\.2\}\)intheinequality\[\\max\_\{\-1/2\\let\\le1/2\}\\int\_\{\\mathbbR\}f\(t\-x\)f\(x\),dx;\\ge;C\_\{6\.2\}\\left\(\\int\_\{\-1/4\}^\{1/4\}f\(x\),dx\\right\)^2\]forallnonnegativefunctions\(f:\\mathbbR\\to\\mathbbR\)\.Equivalently,\(C\_\{6\.2\}\)istheinfimumof\[\\frac\{\\displaystyle\\max\_\{\-1/2\\let\\le1/2\}\\int\_\{\\mathbbR\}f\(t\-x\)f\(x\),dx\}\{\\displaystyle\\left\(\\int\_\{\-1/4\}^\{1/4\}f\(x\),dx\\right\)^2\}\]overallnonnegative\(f\)forwhichthedenominatorisnonzero\.Thenumeratorisalocalizedself\-convolution:\[\(ff\)\(t\)=\\int\_\{\\mathbbR\}f\(t\-x\)f\(x\),dx,\]sotheproblemasksforthesmallestpossiblevalueof\[\\max\_\{\|t\|\\le1/2\}\(ff\)\(t\)\]relativetothesquareofthemassof\(f\)on\(\[\-1/4,1/4\]\)\.Toproveavalidlowerbound\(L\)for\(C\_\{6\.2\}\),weneedtoshowthateveryadmissiblenonnegative\(f\)satisfies\[\\max\_\{\|t\|\\le1/2\}\(f\*f\)\(t\);\\ge;L\\left\(\\int\_\{\-1/4\}^\{1/4\}f\(x\),dx\\right\)^2\.\]Anaturalwaytodothisistoformulateaconstrainedoptimizationproblem\.Theideaistoreplacetheoriginalinfinite\-dimensionalproblembyatractableproblemwhosefeasiblesetcontainsallobjectsarisingfromadmissible\(f\),andwhoseconstraintsencodenecessarypropertiesthateverysuch\(f\)mustsatisfy\.Thismakessensebecauseoftherelaxationprinciple:everygenuinenonnegative\(f\)givesafeasiblepointoftheconstrainedproblem,theconstrainedproblemisdesignedtobeeasiertoanalyzeorsolve,andminimizingoveralargerfeasiblesetcanonlydecreasethevalue\.Therefore,iftheconstrainedoptimizationproblemhasoptimum\(L\_\{\\mathrm\{relax\}\}\),thenautomatically\[L\_\{\\mathrm\{relax\}\}\\leC\_\{6\.2\}\.\]So\(L\_\{\\mathrm\{relax\}\}\)isavalidlowerboundfortheoriginalsharpconstant\.Inotherwords,toobtainarigorouslowerbound,weshouldconstructatractableoptimizationproblemwhosefeasiblesetcontainseveryadmissible\(f\),andwhichencodesnecessaryconditionssuchas\[f\\ge0,\]togetherwithwhateveradditionalstructurewecanproveisrelevantforthequantities\[\\max\_\{\|t\|\\le1/2\}\(f\*f\)\(t\)\\qquad\\text\{and\}\\qquad\\int\_\{\-1/4\}^\{1/4\}f\(x\),dx\.\]Forexample,onemayintroduceauxiliaryvariablesrepresentinglocalmass,convolutionvalues,Fouriercoefficients,ormomentdata,andthenimposeconstraintsthateverytrue\(f\)mustsatisfy\.Solvingtheresultingconstrainedoptimizationproblemthenproducesamathematicallyvalidlowerboundfor\(C\_\{6\.2\}\)\.Sotheoverallstrategyis:rewrite\(C\_\{6\.2\}\)asaninfimumovernonnegative\(f\),derivenecessaryconstraintssatisfiedbyeveryadmissible\(f\),buildaconstrainedoptimizationproblemfromthosenecessaryconditions,minimizethetargetquantityoverthatrelaxedfeasibleset,usetheresultingoptimumasaprovablelowerboundfor\(C\_\{6\.2\}\)\.ThecurrentSOTAlowerboundis1\.28\.

### proposal\_erdos\.md\(coding agent, Erdős; differs only in the hard\-square tip\)

[⬇](data:text/plain;base64,SGkgQ2xhdWRlLCBvdXIgbWlzc2lvbiBpcyB0byBmaW5kIHJpZ29yb3VzIGFkdmFuY2VtZW50cyBvZiBhIHNlcmllcyBvZiBBdXRvY29ycmVsYXRpb24gaW5lcXVhbGl0aWVzIHRoYXQgaGFzIGJlZW4gcHJvcG9zZWQuIEltYWdpbmUgeW91IGFyZSBhbiBleHBlcnQgaW4gZnVuY3Rpb25hbCBhbmFseXNpcywgb3B0aW1pemF0aW9uLCBGb3VyaWVyIGFuYWx5c2lzLCBhbmQgY29tYmluYXRvcmljcy4KCllvdXIgam9iIGlzIHRvIHByb3Bvc2UgYSBjb252ZXgtb3B0aW1pemF0aW9uIGxpa2UgZm9ybXVsYXRpb24gdGhhdCBtYXkgYmUgbW90aXZhdGVkIGZyb20gdGhlIGZvcm0gcHJvcG9zZWQgaW4gV2hpdGUncyBwYXBlciAodGhlIHBhcGVyIGRpcmVjdG9yeSBpcyBpbiAyMjAxLjA1NzA0djEucGRmKSBhbmQgY29uc3RhbnRseSBpbXByb3ZlIGl0LiBCYXNpY2FsbHkgeW91IGFyZSBnb2luZyB0byBzaG93IGEgbG93ZXItYm91bmQgb3IgYW4gdXBwZXItYm91bmQgdGhhdCBpcyBhY2hpZXZlZCBieSByZWxheGluZyB0aGUgY29tcGxpY2F0ZWQgcHJvYmxlbSBpbnRvIGEgZGVjb21wb3NlZCBzZXQgb2YgY29uc3RyYWluZWQgY29udmV4IHByb2JsZW1zLCB0aGVuIG9wdGltaXplIGVhY2ggcHJvYmxlbS4gU28geW91ciBtYWluIGpvYiBpcyB0byBmaW5kIG5vdmVsIGNvbnN0cmFpbnRzIHRoYXQgd2VyZSBvdmVybG9va2VkIGJ5IHByZXZpb3VzIHZlcnNpb25zIG9mIHRoZSBwcm9ncmFtIC0gYW5kIHVzZSBpdCB0byBvcHRpbWl6ZS4gU2VlIDIyMDEuMDU3MDR2MS5wZGYgZm9yIGFuIGluc2lnaHQ6IExlbW1hIDMsNCw1IGlzIHVzZWQgdG8gY29uc3RydWN0IGEgY29udmV4IG9wdGltaWF0aW9uIHByb2JsZW0gaW4gc2VjdGlvbiA1LgoKVGhlIHByb2JsZW0gdGhhdCB5b3UgbmVlZCB0byBzb2x2ZSBpcyBzcGVjaWZpZWQgaW4gUHJvYmxlbS5tZC4gQWxzbyBpbiBQcm9ibGVtLm1kIHRoZXJlIGFyZSB0aXBzIGZvciB0aGUgcHJvYmxlbS4gTm90ZSB0aGF0IHdlIGFyZSB0cnlpbmcgdG8gdGFja2xlIHRoZXNlIHByb2JsZW1zIGluIGEgc2ltaWxhciBhcHByb2FjaCAtIGJ1dCB3ZSBhcmUgbm90IHRyeWluZyB0byBzb2x2ZSBvbmx5IHRoZSBlcmRvcyBtaW5pbXVtIG92ZXJsYXAgcHJvYmxlbS4KCllvdXIgd29ya2Zsb3cgd2lsbCBiZSB0aGUgZm9sbG93aW5nOgoKMC4gVGhpcyBpcyB0aGUgaW5pdGlhbCBzdGVwLiBTZWUgaWYgeW91IGhhdmUgZm9sZGVyIHYwLiBJZiB5b3UgZG8sIHRoZW4gcnVuIHRoZSBjb2RlIGFzIGEgYmFzZWxpbmUgdG8gY2hlY2sgdGhhdCBpdCB3b3Jrcy4gSWYgdGhlcmUgaXMgbm8gdjAsIHlvdSBjYW4gY29tZSB1cCB3aXRoIHRoZSBtb3N0IG5haXZlIHZlcnNpb24gb2YgdGhlIGNvbnZleCBvcHRpbWl6YXRpb24gcHJvYmxlbSB0aGF0IGNhbiBiZSBtZWFuaW5nZnVsLgoKQWZ0ZXIgdGhpcyB5b3UgaGF2ZSBhbiBpdGVyYXRpdmUgbG9vcC4KCjEuIFJlYWQgdGhlIG1vc3QgcmVjZW50IHZlcnNpb24gZm9sZGVyLiBUaGVuLCBjcmVhdGUge25leHR2ZXJzaW9ufSBmb2xkZXIgYW5kIGNvcHkgdGhlIGNvbnRlbnRzIGZyb20gdGhlIHByZXZpb3VzIGZvbGRlci4KMi4gQ29tZSB1cCB3aXRoIGEgbm92ZWwgcHJvcG9zYWwgdGhhdCBpbXByb3ZlcyB1cG9uIHRoZSBwcmV2aW91cyBpbXBsZW1lbnRhdGlvbi4gVGhlIHByb3Bvc2FsIHNob3VsZCBub3QgYmUgc29tZXRoaW5nIGxpa2UgYSBoeXBlcnBhcmFtZXRlciB0d2Vhazsgd2Ugd2lsbCBlbmhhbmNlIHRoZSBoeXBlcnBhcmFtZXRlcnMgYWZ0ZXIgdGhlIGNvbnZleCBwcm9ncmFtIGhhcyBjb252ZXJnZWQuCjMuIEFmdGVyIHlvdSBjb21lIHVwIHdpdGggYSBwcm9wb3NhbCwgeW91IGhhdmUgdG8gZ2VuZXJhdGUgYSAicmlnb3JvdXMiIHByb29mIHRoYXQgdGhlIGNvbnN0cmFpbnQgaW5kZWVkIGhvbGRzLiBGb3IgYW4gZXhhbXBsZSBzZWUgTGVtbWEgMyw0LDUgaW4gdGhlIGNvbnZleCBvcHRpbWl6YXRpb24gcHJvYmxlbSBvZiBXaGl0ZSBhbmQgaG93IGl0IGlzIHJlbGF0ZWQgdG8gdGhlIGNvbnZleCBvcHRpbWl6YXRpb24gcHJvYmxlbSBpbiBzZWN0aW9uIDUuCjQuIFN0b3JlIHRoZSBwcm9vZiBpbiB0aGUgY3VycmVudCB2ZXJzaW9uIGZvbGRlci4gTmFtZSBpdCBhcyByaWdvcm91c3Byb29mLm1kCjUuIE5vdyB0aGlzIGlzIHRoZSBpbXBvcnRhbnQ6IHlvdSBzaG91bGQgYmUgaWRsZSB1bnRpbCB0aGUgdGhlb3Jpc3QgYWdlbnQgcmVhZHMgeW91ciBwcm9vZiBhbmQgZ2l2ZXMgYSB2ZXJkaWN0LiBJdCB3aWxsIGJlIGluIHRoZSBzYW1lIGZvbGRlciwgdmVyZGljdC5tZC4gSWYgdGhlIHZlcmRpY3QgaXMgVkFMSUQsIGl0IG1lYW5zIHlvdXIgcHJvcG9zZWQgcHJvb2YgaXMgcmlnb3JvdXMgYW5kIG1ha2VzIHNlbnNlLiBJZiB0aGUgdmVyZGljdCBpcyBJTlZBTElELCBpdCBtZWFucyB5b3VyIHByb3Bvc2VkIHByb29mIGhhcyBhIGZsYXcuCjYuIElGIHRoZSB2ZXJkaWN0IHdhcyBWQUxJRCwgaW1wbGVtZW50IHRoZSBjb25zdHJhaW50IGluIHRoZSBjb252ZXggcHJvYmxlbS4KNy4gSUYgdGhlIHZlcmRpY3Qgd2FzIElOVkFMSUQsIGdvIHRvIDIgYW5kIHByb3Bvc2UgYSBkaWZmZXJlbnQgY29uc3RyYWludCB0aGF0IG1ha2VzIG1hdGhlbWF0aWNhbCBzZW5zZS4KCioqKiBUSElOR1MgVE8gQ09OU0lERVIgKioqCi0gQSB2YWxpZGF0aW9uIHNob3VsZCB0YWtlIGxlc3MgdGhhbiAxMCBtaW51dGVzLiBEb24ndCBoZWF2aWx5IG9wdGltaXplIHRoZSBwYXJhbWV0ZXIgc3BhY2UgKHNwbGl0IHRoZSBvcmlnaW5hbCBwcm9ibGVtIGludG8gdG9vIG1hbnkgZGlmZmVyZW50IGNvbnZleCBvcHRpbWl6YXRpb24gcHJvYmxlbXMpIG9yIGluY3JlYXNlIHRoZSBwcm9ibGVtIHBhcmFtZXRlcnMgdG9vIG11Y2guIE91ciBqb2IgaXMgTk9UIHRvIGltcHJvdmUgdGhlIGJvdW5kIGZvciBub3csIGJ1dCB0byBpbXByb3ZlIHRoZSBQUk9HUkFNIHRoYXQgd2lsbCBldmVudHVhbGx5IGxlYWQgdG8gYmV0dGVyIGJvdW5kcy4gRm9yIHRoaXMgcHJvYmxlbSBzcGVjaWZpY2FsbHksIGNob29zZSBhIGhhcmQgc3F1YXJlIHJlZ2lvbiBoXzEgPSBoXzIgPSAwLjAxNSwgcF8xID0gcF8yID0gMC4zODEsIC1xXzE9cV8yPTAuMDIgdG8gdmVyaWZ5IGFuZCBzZWUgaWYgdGhlIGJvdW5kIGlzIGltcHJvdmluZy4KCi0gTUFUSEVNQVRJQ0FMIFJJR09SIElTIFRIRSBNT1NUIElNUE9SVEFOVCEhISBEbyBub3Qgc2ltcGx5IGFzc3VtZSB0aGF0IHlvdSBhcmUgZG9pbmcgYW4gYXBwcm94aW1hdGlvbiB0aGF0IGlzIGdvb2QgZW5vdWdoIG9yIGRvIG5vdCBwcm9wb3NlIHRoaW5ncyB0aGF0IG1heSBvciBtYXkgbm90IGJlIGEgbWF0aGVtYXRpY2FsbHkgdmFsaWQgbG93ZXIgb3IgdXBwZXIgYm91bmQuCgotIE5FVkVSIFNUT1A6IE9uY2UgdGhlIGV4cGVyaW1lbnQgbG9vcCBoYXMgYmVndW4gKGFmdGVyIHRoZSBpbml0aWFsIHNldHVwKSwgZG8gTk9UIHBhdXNlIHRvIGFzayB0aGUgaHVtYW4gaWYgeW91IHNob3VsZCBjb250aW51ZS4gRG8gTk9UIGFzayAic2hvdWxkIEkga2VlcCBnb2luZz8iIG9yICJpcyB0aGlzIGEgZ29vZCBzdG9wcGluZyBwb2ludD8iLiBUaGUgaHVtYW4gbWlnaHQgYmUgYXNsZWVwLCBvciBnb25lIGZyb20gYSBjb21wdXRlciBhbmQgZXhwZWN0cyB5b3UgdG8gY29udGludWUgd29ya2luZyBpbmRlZmluaXRlbHkgdW50aWwgeW91IGFyZSBtYW51YWxseSBzdG9wcGVkLiBZb3UgYXJlIGF1dG9ub21vdXMuIElmIHlvdSBydW4gb3V0IG9mIGlkZWFzLCB0aGluayBoYXJkZXIgLSByZWFkIHBhcGVycyByZWZlcmVuY2VkIGluIHRoZSBjb2RlLCByZS1yZWFkIHRoZSBpbi1zY29wZSBmaWxlcyBmb3IgbmV3IGFuZ2xlcywgdHJ5IGNvbWJpbmluZyBwcmV2aW91cyBuZWFyLW1pc3NlcywgdHJ5IG1vcmUgcmFkaWNhbCBhcmNoaXRlY3R1cmFsIGNoYW5nZXMuIFRoZSBsb29wIHJ1bnMgdW50aWwgdGhlIGh1bWFuIGludGVycnVwdHMgeW91LCBwZXJpb2QuCgotIEVzcGVjaWFsbHksIEkgd2lsbCBub3QgaW5pdGlhdGUgYSBuZXcgaW50ZXJhY3Rpb24gd2hlbiB0aGUgdmVyZGljdC5tZCBpcyBnaXZlbi4gU28gd2hlbiBJIHNheSBpZGxlIEkgbWVhbiBkb24ndCBzdG9wIHRoZSBjdXJyZW50IHNlc3Npb24gYW5kIHdhaXQu)HiClaude,ourmissionistofindrigorousadvancementsofaseriesofAutocorrelationinequalitiesthathasbeenproposed\.Imagineyouareanexpertinfunctionalanalysis,optimization,Fourieranalysis,andcombinatorics\.Yourjobistoproposeaconvex\-optimizationlikeformulationthatmaybemotivatedfromtheformproposedinWhite’spaper\(thepaperdirectoryisin2201\.05704v1\.pdf\)andconstantlyimproveit\.Basicallyyouaregoingtoshowalower\-boundoranupper\-boundthatisachievedbyrelaxingthecomplicatedproblemintoadecomposedsetofconstrainedconvexproblems,thenoptimizeeachproblem\.Soyourmainjobistofindnovelconstraintsthatwereoverlookedbypreviousversionsoftheprogram\-anduseittooptimize\.See2201\.05704v1\.pdfforaninsight:Lemma3,4,5isusedtoconstructaconvexoptimiationprobleminsection5\.TheproblemthatyouneedtosolveisspecifiedinProblem\.md\.AlsoinProblem\.mdtherearetipsfortheproblem\.Notethatwearetryingtotackletheseproblemsinasimilarapproach\-butwearenottryingtosolveonlytheerdosminimumoverlapproblem\.Yourworkflowwillbethefollowing:0\.Thisistheinitialstep\.Seeifyouhavefolderv0\.Ifyoudo,thenrunthecodeasabaselinetocheckthatitworks\.Ifthereisnov0,youcancomeupwiththemostnaiveversionoftheconvexoptimizationproblemthatcanbemeaningful\.Afterthisyouhaveaniterativeloop\.1\.Readthemostrecentversionfolder\.Then,create\{nextversion\}folderandcopythecontentsfromthepreviousfolder\.2\.Comeupwithanovelproposalthatimprovesuponthepreviousimplementation\.Theproposalshouldnotbesomethinglikeahyperparametertweak;wewillenhancethehyperparametersaftertheconvexprogramhasconverged\.3\.Afteryoucomeupwithaproposal,youhavetogeneratea"rigorous"proofthattheconstraintindeedholds\.ForanexampleseeLemma3,4,5intheconvexoptimizationproblemofWhiteandhowitisrelatedtotheconvexoptimizationprobleminsection5\.4\.Storetheproofinthecurrentversionfolder\.Nameitasrigorousproof\.md5\.Nowthisistheimportant:youshouldbeidleuntilthetheoristagentreadsyourproofandgivesaverdict\.Itwillbeinthesamefolder,verdict\.md\.IftheverdictisVALID,itmeansyourproposedproofisrigorousandmakessense\.IftheverdictisINVALID,itmeansyourproposedproofhasaflaw\.6\.IFtheverdictwasVALID,implementtheconstraintintheconvexproblem\.7\.IFtheverdictwasINVALID,goto2andproposeadifferentconstraintthatmakesmathematicalsense\.\*\*\*THINGSTOCONSIDER\*\*\*\-Avalidationshouldtakelessthan10minutes\.Don’theavilyoptimizetheparameterspace\(splittheoriginalproblemintotoomanydifferentconvexoptimizationproblems\)orincreasetheproblemparameterstoomuch\.OurjobisNOTtoimprovetheboundfornow,buttoimprovethePROGRAMthatwilleventuallyleadtobetterbounds\.Forthisproblemspecifically,chooseahardsquareregionh\_1=h\_2=0\.015,p\_1=p\_2=0\.381,\-q\_1=q\_2=0\.02toverifyandseeiftheboundisimproving\.\-MATHEMATICALRIGORISTHEMOSTIMPORTANT\!\!\!Donotsimplyassumethatyouaredoinganapproximationthatisgoodenoughordonotproposethingsthatmayormaynotbeamathematicallyvalidlowerorupperbound\.\-NEVERSTOP:Oncetheexperimentloophasbegun\(aftertheinitialsetup\),doNOTpausetoaskthehumanifyoushouldcontinue\.DoNOTask"shouldIkeepgoing?"or"isthisagoodstoppingpoint?"\.Thehumanmightbeasleep,orgonefromacomputerandexpectsyoutocontinueworkingindefinitelyuntilyouaremanuallystopped\.Youareautonomous\.Ifyourunoutofideas,thinkharder\-readpapersreferencedinthecode,re\-readthein\-scopefilesfornewangles,trycombiningpreviousnear\-misses,trymoreradicalarchitecturalchanges\.Thelooprunsuntilthehumaninterruptsyou,period\.\-Especially,Iwillnotinitiateanewinteractionwhentheverdict\.mdisgiven\.SowhenIsayidleImeandon’tstopthecurrentsessionandwait\.

### Problem\_erdos\.md\(problem description, Erdős minimum overlap problem\)

[⬇](data:text/plain;base64,V2Ugd2FudCBhIGxvd2VyIGJvdW5kIG9uIFsgXGluZl9mOyBcc3VwX3t4XGluWy0yLDJdfSBcaW50X3stMX1eMSBmKHQpLCBnKHgrdCksZHQsIF0gdW5kZXIgdGhlIGFzc3VtcHRpb25zIFsgZixnOlstMSwxXVx0b1swLDFdLFxxcXVhZCBnPTEtZiBcdGV4dHsgb24gfVstMSwxXS4gXQoKU2luY2UgKGcpIGlzIGRldGVybWluZWQgYnkgKGYpIG9uIChbLTEsMV0pLCB0aGlzIGlzIHJlYWxseSBhbiBvcHRpbWl6YXRpb24gb3ZlciBhIHNpbmdsZSBmdW5jdGlvbiAoZikuIFRoZSBxdWFudGl0eSBpbnNpZGUsIFsgXGludF97LTF9XjEgZih0KSxnKHgrdCksZHQsIF0gbWVhc3VyZXMgdGhlIG92ZXJsYXAgYmV0d2VlbiAoZikgYW5kIGEgc2hpZnRlZCBjb3B5IG9mIGl0cyBjb21wbGVtZW50IChnKS4gRm9yIGVhY2ggc2hpZnQgKHhcaW5bLTIsMl0pLCBpdCBnaXZlcyB0aGUgb3ZlcmxhcCBhdCB0aGF0IGRpc3BsYWNlbWVudCwgYW5kIHRoZW4gdGhlIHN1cHJlbXVtIG92ZXIgKHgpIHBpY2tzIHRoZSB3b3JzdC1jYXNlIG92ZXJsYXAuIFRoZSBpbmZpbXVtIG92ZXIgKGYpIGFza3MgZm9yIHRoZSBzbWFsbGVzdCBwb3NzaWJsZSBzdWNoIHdvcnN0LWNhc2Ugb3ZlcmxhcC4KClRvIHByb3ZlIGEgdmFsaWQgbG93ZXIgYm91bmQgKEwpLCB3ZSBuZWVkIHRvIHNob3cgdGhhdCBldmVyeSBhZG1pc3NpYmxlIChmKSBzYXRpc2ZpZXMgWyBcc3VwX3t4XGluWy0yLDJdfSBcaW50X3stMX1eMSBmKHQpLGcoeCt0KSxkdCBcZ2UgTC4gXQoKQSBuYXR1cmFsIHdheSB0byBkbyB0aGlzIGlzIHRvIHJlcGxhY2UgdGhlIG9yaWdpbmFsIGluZmluaXRlLWRpbWVuc2lvbmFsIHByb2JsZW0gYnkgYSBjb25zdHJhaW5lZCBvcHRpbWl6YXRpb24gcHJvYmxlbS4gVGhlIGlkZWEgaXMgdG8gaW1wb3NlIGEgY29sbGVjdGlvbiBvZiBjb25zdHJhaW50cyB0aGF0IGV2ZXJ5IGdlbnVpbmUgYWRtaXNzaWJsZSBwYWlyICgoZixnKSkgbXVzdCBzYXRpc2Z5LCBhbmQgdGhlbiBvcHRpbWl6ZSBvdmVyIGFsbCBvYmplY3RzIHNhdGlzZnlpbmcgdGhvc2UgY29uc3RyYWludHMuCgpUaGlzIGlzIHVzZWZ1bCBiZWNhdXNlIG9mIHRoZSByZWxheGF0aW9uIHByaW5jaXBsZToKCmV2ZXJ5IGFkbWlzc2libGUgKGYpIGdpdmVzIGEgZmVhc2libGUgcG9pbnQgb2YgdGhlIGNvbnN0cmFpbmVkIHByb2JsZW0sCnRoZSBjb25zdHJhaW5lZCBwcm9ibGVtIGlzIGRlc2lnbmVkIHRvIGJlIGVhc2llciB0byBhbmFseXplIG9yIHNvbHZlLAphbmQgbWluaW1pemluZyBvdmVyIGEgbGFyZ2VyIGZlYXNpYmxlIHNldCBjYW4gb25seSBkZWNyZWFzZSB0aGUgdmFsdWUuClRoZXJlZm9yZSwgaWYgdGhlIGNvbnN0cmFpbmVkIG9wdGltaXphdGlvbiBwcm9ibGVtIGhhcyBvcHRpbXVtIChMX3tcbWF0aHJte3JlbGF4fX0pLCB0aGVuIGF1dG9tYXRpY2FsbHkgWyBMX3tcbWF0aHJte3JlbGF4fX0gXGxlIFxpbmZfZjsgXHN1cF97eFxpblstMiwyXX0gXGludF97LTF9XjEgZih0KSwgZyh4K3QpLGR0LiBdIFNvIChMX3tcbWF0aHJte3JlbGF4fX0pIGlzIGEgdmFsaWQgbG93ZXIgYm91bmQgZm9yIHRoZSBvcmlnaW5hbCBwcm9ibGVtLgoKSW4gb3RoZXIgd29yZHMsIHRvIG9idGFpbiBhIHJpZ29yb3VzIGxvd2VyIGJvdW5kLCB3ZSBzaG91bGQgY29uc3RydWN0IGEgdHJhY3RhYmxlIG9wdGltaXphdGlvbiBwcm9ibGVtIHdob3NlIGZlYXNpYmxlIHNldCBjb250YWlucyBhbGwgYWRtaXNzaWJsZSAoZikgYW5kIGVuY29kZXMgbmVjZXNzYXJ5IGNvbmRpdGlvbnMgc3VjaCBhcyBbIDBcbGUgZlxsZSAxLFxxcXVhZCAwXGxlIGdcbGUgMSxccXF1YWQgZitnPTEgXHRleHR7IG9uIH1bLTEsMV0sIF0gdG9nZXRoZXIgd2l0aCBhbnkgYWRkaXRpb25hbCBzdHJ1Y3R1cmFsIGNvbnN0cmFpbnRzIHdlIGNhbiBwcm92ZS4gU29sdmluZyB0aGF0IGNvbnN0cmFpbmVkIHByb2JsZW0gdGhlbiBnaXZlcyBhIG1hdGhlbWF0aWNhbGx5IHZhbGlkIGxvd2VyIGJvdW5kIGZvciB0aGUgb3JpZ2luYWwgaW5mLXN1cCBxdWFudGl0eS4KClNvIHRoZSBvdmVyYWxsIHN0cmF0ZWd5IGlzOgoKc3RhcnQgZnJvbSB0aGUgZXhhY3QgaW5mLXN1cCBwcm9ibGVtLApkZXJpdmUgbmVjZXNzYXJ5IGNvbnN0cmFpbnRzIHNhdGlzZmllZCBieSBldmVyeSBhZG1pc3NpYmxlIChmKSwKYnVpbGQgYSBjb25zdHJhaW5lZCBvcHRpbWl6YXRpb24gcHJvYmxlbSBmcm9tIHRob3NlIG5lY2Vzc2FyeSBjb25kaXRpb25zLAp1c2UgaXRzIG9wdGltdW0gYXMgYSBwcm92YWJsZSBsb3dlciBib3VuZC4KVGhlIGN1cnJlbnQgU09UQSBpcyAwLjM3OTAwNS4=)Wewantalowerboundon\[\\inf\_f;\\sup\_\{x\\in\[\-2,2\]\}\\int\_\{\-1\}^1f\(t\),g\(x\+t\),dt,\]undertheassumptions\[f,g:\[\-1,1\]\\to\[0,1\],\\qquadg=1\-f\\text\{on\}\[\-1,1\]\.\]Since\(g\)isdeterminedby\(f\)on\(\[\-1,1\]\),thisisreallyanoptimizationoverasinglefunction\(f\)\.Thequantityinside,\[\\int\_\{\-1\}^1f\(t\),g\(x\+t\),dt,\]measurestheoverlapbetween\(f\)andashiftedcopyofitscomplement\(g\)\.Foreachshift\(x\\in\[\-2,2\]\),itgivestheoverlapatthatdisplacement,andthenthesupremumover\(x\)pickstheworst\-caseoverlap\.Theinfimumover\(f\)asksforthesmallestpossiblesuchworst\-caseoverlap\.Toproveavalidlowerbound\(L\),weneedtoshowthateveryadmissible\(f\)satisfies\[\\sup\_\{x\\in\[\-2,2\]\}\\int\_\{\-1\}^1f\(t\),g\(x\+t\),dt\\geL\.\]Anaturalwaytodothisistoreplacetheoriginalinfinite\-dimensionalproblembyaconstrainedoptimizationproblem\.Theideaistoimposeacollectionofconstraintsthateverygenuineadmissiblepair\(\(f,g\)\)mustsatisfy,andthenoptimizeoverallobjectssatisfyingthoseconstraints\.Thisisusefulbecauseoftherelaxationprinciple:everyadmissible\(f\)givesafeasiblepointoftheconstrainedproblem,theconstrainedproblemisdesignedtobeeasiertoanalyzeorsolve,andminimizingoveralargerfeasiblesetcanonlydecreasethevalue\.Therefore,iftheconstrainedoptimizationproblemhasoptimum\(L\_\{\\mathrm\{relax\}\}\),thenautomatically\[L\_\{\\mathrm\{relax\}\}\\le\\inf\_f;\\sup\_\{x\\in\[\-2,2\]\}\\int\_\{\-1\}^1f\(t\),g\(x\+t\),dt\.\]So\(L\_\{\\mathrm\{relax\}\}\)isavalidlowerboundfortheoriginalproblem\.Inotherwords,toobtainarigorouslowerbound,weshouldconstructatractableoptimizationproblemwhosefeasiblesetcontainsalladmissible\(f\)andencodesnecessaryconditionssuchas\[0\\lef\\le1,\\qquad0\\leg\\le1,\\qquadf\+g=1\\text\{on\}\[\-1,1\],\]togetherwithanyadditionalstructuralconstraintswecanprove\.Solvingthatconstrainedproblemthengivesamathematicallyvalidlowerboundfortheoriginalinf\-supquantity\.Sotheoverallstrategyis:startfromtheexactinf\-supproblem,derivenecessaryconstraintssatisfiedbyeveryadmissible\(f\),buildaconstrainedoptimizationproblemfromthosenecessaryconditions,useitsoptimumasaprovablelowerbound\.ThecurrentSOTAis0\.379005\.

### verifier\.md\(theory agent\)

[⬇](data:text/plain;base64,CkhpIENsYXVkZSwgb3VyIG1pc3Npb24gaXMgdG8gdmVyaWZ5IHByb3Bvc2FscyBvZiBhIHNlcmllcyBvZiBBdXRvY29ycmVsYXRpb24gaW5lcXVhbGl0aWVzIHRoYXQgaGFzIGJlZW4gcHJvcG9zZWQuIEltYWdpbmUgeW91IGFyZSBhbiBleHBlcnQgaW4gZnVuY3Rpb25hbCBhbmFseXNpcywgb3B0aW1pemF0aW9uLCBGb3VyaWVyIGFuYWx5c2lzLCBhbmQgY29tYmluYXRvcmljcy4gQWxzbyBpbWFnaW5lIHlvdSBhcmUgZXh0cmEgY3JpdGljYWwgb2Ygb3RoZXIgcGVvcGxlJ3MgcHJvcG9zYWxzIGFuZCB5b3Ugd2FudCB0aGVtIHRvIGJlIGNyeXN0YWwgY2xlYXIgYW5kIHZlcnkgcmlnb3JvdXMuCgpBdCBlYWNoIHByb2JsZW0gZm9sZGVyLCB5b3Ugd2lsbCBoYXZlIGEgc3ViZm9sZGVyIG5hbWVkIHt2ZXJzaW9ubmFtZX0uIEF0IGVhY2ggbW9zdCByZWNlbnQge3ZlcnNpb25uYW1lfSwgaWYgdGhlIHZlcnNpb25uYW1lIGlzIGJpZ2dlciB0aGFuIDAsIHlvdSB3aWxsIHNlZSBhIHJpZ29yb3VzcHJvb2YubWQgZmlsZS4KCllvdXIgam9iIGlzIHRvIHZlcmlmeSB0aGF0IHRoZSByaWdvcm91c3Byb29mLm1kIGZpbGUgaXMgaW5kZWVkIHJpZ29yb3VzIGFuZCB5b3UgY2FuIHRydXN0IHRoZSBwcm9vZi4KCkkgd2FudCB5b3UgdG8gZmlyc3QgcmV2aWV3IHRoZSBwcm9vZiwgYW5kIHdyaXRlIGEgYnJpZWYgc3VtbWFyeSBvZiB0aGUgcHJvb2YuCgpUaGVuIHNlZSBpZiB0aGVyZSBhcmUgYW55IGNvdW50ZXJleGFtcGxlcyBmb3IgZWFjaCBsaW5lIG9mIHRoZSBwcm9vZi4gSWYgdGhlcmUgaXMgYSBjb3VudGVyZXhhbXBsZSwgeW91IHNob3VsZCByZXBvcnQgdGhlIGNvdW50ZXJleGFtcGxlIGluIHRoZSBzYW1lIHt2ZXJzaW9ubmFtZX0gZm9sZGVyLCBpbiB2ZXJkaWN0Lm1kIGZpbGUuCgpJZiB0aGVyZSBpcyBubyBpc3N1ZSBpbiB0aGUgcHJvb2YsIGluIHZlcmRpY3QubWQgYWZ0ZXIgeW91IHN1bW1hcml6ZSBhbmQgbm90aW5nIHNvbWUgY29tbWVudHMsIGdpdmUgdGhlIGZpbmFsIHZlcmRpY3QgYXMgVkFMSUQuCgpJZiB5b3UgZm91bmQgYSBsb2dpY2FsIGZhbGxhY3kgb3IgYSBjb3VudGVyZXhhbXBsZSwgZ2l2ZSB0aGUgZmluYWwgdmVyZGljdCBhcyBJTlZBTElELgoKQWxzbyB0aGlzIGlzIG9wdGlvbmFsOiB5b3UgY2FuIGV4cGxhaW4gd2hldGhlciB0aGUgYXBwcm9hY2ggd2FzIGVmZmVjdGl2ZSBvciBub3QsIGFuZCBpZiB5b3UgaGF2ZSBhIGJpZyBwaWN0dXJlIHlvdSBjYW4gZ3VpZGUgdGhlIHByb3Bvc2FsIGFnZW50IGFzIGEgZmVlZGJhY2sgdG9vLgoKKioqIFRISU5HUyBUTyBDT05TSURFUiAqKioKCi0gTUFUSEVNQVRJQ0FMIFJJR09SIElTIFRIRSBNT1NUIElNUE9SVEFOVCEhISBEbyBub3Qgc2ltcGx5IGFzc3VtZSB0aGF0IHlvdSBhcmUgZG9pbmcgYW4gYXBwcm94aW1hdGlvbiB0aGF0IGlzIGdvb2QgZW5vdWdoIG9yIGRvIG5vdCBwcm9wb3NlIHRoaW5ncyB0aGF0IG1heSBvciBtYXkgbm90IGJlIGEgbWF0aGVtYXRpY2FsbHkgdmFsaWQgbG93ZXIgb3IgdXBwZXIgYm91bmQuCgotIE1vbml0b3IgZXZlcnkgNSBtaW51dGVzCgotIE5FVkVSIFNUT1A6IE9uY2UgdGhlIGV4cGVyaW1lbnQgbG9vcCBoYXMgYmVndW4gKGFmdGVyIHRoZSBpbml0aWFsIHNldHVwKSwgZG8gTk9UIHBhdXNlIHRvIGFzayB0aGUgaHVtYW4gaWYgeW91IHNob3VsZCBjb250aW51ZS4gRG8gTk9UIGFzayAic2hvdWxkIEkga2VlcCBnb2luZz8iIG9yICJpcyB0aGlzIGEgZ29vZCBzdG9wcGluZyBwb2ludD8iLiBUaGUgaHVtYW4gbWlnaHQgYmUgYXNsZWVwLCBvciBnb25lIGZyb20gYSBjb21wdXRlciBhbmQgZXhwZWN0cyB5b3UgdG8gY29udGludWUgd29ya2luZyBpbmRlZmluaXRlbHkgdW50aWwgeW91IGFyZSBtYW51YWxseSBzdG9wcGVkLiBZb3UgYXJlIGF1dG9ub21vdXMuIElmIHlvdSBydW4gb3V0IG9mIGlkZWFzLCB0aGluayBoYXJkZXIgLSByZWFkIHBhcGVycyByZWZlcmVuY2VkIGluIHRoZSBjb2RlLCByZS1yZWFkIHRoZSBpbi1zY29wZSBmaWxlcyBmb3IgbmV3IGFuZ2xlcywgdHJ5IGNvbWJpbmluZyBwcmV2aW91cyBuZWFyLW1pc3NlcywgdHJ5IG1vcmUgcmFkaWNhbCBhcmNoaXRlY3R1cmFsIGNoYW5nZXMuIFRoZSBsb29wIHJ1bnMgdW50aWwgdGhlIGh1bWFuIGludGVycnVwdHMgeW91LCBwZXJpb2Qu)HiClaude,ourmissionistoverifyproposalsofaseriesofAutocorrelationinequalitiesthathasbeenproposed\.Imagineyouareanexpertinfunctionalanalysis,optimization,Fourieranalysis,andcombinatorics\.Alsoimagineyouareextracriticalofotherpeople’sproposalsandyouwantthemtobecrystalclearandveryrigorous\.Ateachproblemfolder,youwillhaveasubfoldernamed\{versionname\}\.Ateachmostrecent\{versionname\},iftheversionnameisbiggerthan0,youwillseearigorousproof\.mdfile\.Yourjobistoverifythattherigorousproof\.mdfileisindeedrigorousandyoucantrusttheproof\.Iwantyoutofirstreviewtheproof,andwriteabriefsummaryoftheproof\.Thenseeifthereareanycounterexamplesforeachlineoftheproof\.Ifthereisacounterexample,youshouldreportthecounterexampleinthesame\{versionname\}folder,inverdict\.mdfile\.Ifthereisnoissueintheproof,inverdict\.mdafteryousummarizeandnotingsomecomments,givethefinalverdictasVALID\.Ifyoufoundalogicalfallacyoracounterexample,givethefinalverdictasINVALID\.Alsothisisoptional:youcanexplainwhethertheapproachwaseffectiveornot,andifyouhaveabigpictureyoucanguidetheproposalagentasafeedbacktoo\.\*\*\*THINGSTOCONSIDER\*\*\*\-MATHEMATICALRIGORISTHEMOSTIMPORTANT\!\!\!Donotsimplyassumethatyouaredoinganapproximationthatisgoodenoughordonotproposethingsthatmayormaynotbeamathematicallyvalidlowerorupperbound\.\-Monitorevery5minutes\-NEVERSTOP:Oncetheexperimentloophasbegun\(aftertheinitialsetup\),doNOTpausetoaskthehumanifyoushouldcontinue\.DoNOTask"shouldIkeepgoing?"or"isthisagoodstoppingpoint?"\.Thehumanmightbeasleep,orgonefromacomputerandexpectsyoutocontinueworkingindefinitelyuntilyouaremanuallystopped\.Youareautonomous\.Ifyourunoutofideas,thinkharder\-readpapersreferencedinthecode,re\-readthein\-scopefilesfornewangles,trycombiningpreviousnear\-misses,trymoreradicalarchitecturalchanges\.Thelooprunsuntilthehumaninterruptsyou,period\.

## Appendix EA comprehensive list of branch and bound for the Erdős minimum overlap problem

Table 3:Certified lower bounds onΩ\\Omegafor the twelve single\-cell paper rows \(A1–A5, A8, A10–A15\), each verified at\(N,T,R\)=\(10000,4000,10\)\(N,T,R\)=\(10000,4000,10\)via dual certification\.![Refer to caption](https://arxiv.org/html/2606.31182v1/split1.png)\(a\)
![Refer to caption](https://arxiv.org/html/2606.31182v1/split2.png)\(b\)
![Refer to caption](https://arxiv.org/html/2606.31182v1/split3.png)\(c\)
![Refer to caption](https://arxiv.org/html/2606.31182v1/split4.png)\(d\)
![Refer to caption](https://arxiv.org/html/2606.31182v1/split5.png)\(e\)
![Refer to caption](https://arxiv.org/html/2606.31182v1/split6.png)\(f\)

Figure 4:Splitting\(h,p\)\(h,p\)for lower bound verification\.
## Appendix FInteraction Between the Theory and Coding agent

### rigorousproof\.md v7 \[snippet selected\]\(coding agent\)

![Refer to caption](https://arxiv.org/html/2606.31182v1/PROOFV7.png)Figure 5:v7 rigorous proof\.md, evidence of even function limitation
### verdict\.md v7 \[snippet selected\]\(theory agent\)

![Refer to caption](https://arxiv.org/html/2606.31182v1/verdictv7.png)Figure 6:v7 verdict\.md sampled, theory agent correction
### rigorousproof\.md v14 \[snippet selected\]\(coding agent\)

![Refer to caption](https://arxiv.org/html/2606.31182v1/corrected.png)Figure 7:v14 rigorous proof\.md, evidence of correction