Theoretical Computer Science

Motivation

In online routing of virtual circuits, connection requests between pairs of nodes of a capacitated network arrive one at a time. Each request must be accepted and routed on a single path with bandwidth $1$, or rejected, immediately and irrevocably, and no edge may carry more than its capacity. The goal is to maximize the number of accepted requests (the throughput). The model goes back to Awerbuch, Azar and Plotkin (FOCS 1993), whose deterministic algorithm has a logarithmic competitive ratio when edge capacities are at least logarithmic in the size of the network, and it underlies the analysis of admission control in circuit-switched and bandwidth-reserved networks.

Buchbinder and Naor (Math. Oper. Res. 2009) recover an algorithm with the same competitive factor from a general recipe: an online primal–dual scheme first produces a feasible fractional routing online, and an online version of Raghavan's pessimistic estimator (J. Comput. Syst. Sci. 1988) then rounds it, also online. This mission formalizes that construction and its guarantee (Section 5.2 of the paper, with the Section 3 scheme it uses).

Timeline:

• 1987–1988: Raghavan and Thompson introduce randomized rounding for multicommodity flow; Raghavan derandomizes it with pessimistic estimators.
• 1993: Awerbuch, Azar and Plotkin give the deterministic throughput-competitive online routing algorithm.
• 2005–2009: Buchbinder and Naor's primal–dual framework (ESA 2005; MOR 2009) derives an algorithm with the same factor systematically.

Setting

Let $E$ be a finite set of $m$ edges with capacities $u(e) > 0$, and $u(\min) = \min_e u(e)$. Requests $r_1, r_2, \dots$ arrive online; request $r_i$ comes with a finite list $\mathcal P(r_i)$ of admissible paths, each a set of edges, all of size at most $P(\max)$.

A fractional routing assigns flows $f(r_i, P) \ge 0$; it is feasible when $\sum_{P \in \mathcal P(r_i)} f(r_i, P) \le 1$ for every request and the load $\sum_{r_i}\sum_{P \ni e} f(r_i, P)$ of every edge is at most $u(e)$. Its value is $\mathrm{val}(f) = \sum_{r_i}\sum_P f(r_i, P)$; $\mathrm{OPT}$ is the largest value of a feasible routing of the arrived requests, an upper bound on the integral optimum.

The fractional scheme. The covering LP paired with the routing LP (the paper's primal, Fig. 3) has variables $x(e)$ (cost $u(e)$) and $Z(r_i)$ (cost $1$) with constraints $\sum_{e \in P} x(e) + Z(r_i) \ge 1$. When $r_i$ arrives, its paths are visited in order; for each path whose constraint fails, $f(r_i,P)$ is raised from $0$ to the least value restoring it, while $x(e) = \max\big(x(e), \tfrac1\ell(e^{B' F_e/(2u(e))}-1)\big)$ for $e \in P$ and $Z(r_i) = \max\big(Z(r_i), \tfrac1\ell(e^{B' f(r_i)/2}-1)\big)$ follow the flow ($F_e$ the load of $e$, $f(r_i)$ the flow of $r_i$). The parameters are $\ell = P(\max)+1$ and $B' = 2\ln(1+\ell)$.

The rounding. With the rounding scale $B = \exp(1 + \ln(2m)/u(\min)) - 1$, the integral edge usage $\chi(e)$ and the number $s$ of served requests, the potential is $\Phi = \Phi_1 + \Phi_2$,

After the fractional round of $r_i$, the algorithm serves $r_i$ on a path $P \in \mathcal P(r_i)$ (adding $1$ to $\chi(e)$ for $e \in P$) if this gives potential at most the potential $\Phi^{\mathrm{start}}$ before the round; otherwise it rejects $r_i$.

Formalization targets

Goal: Lemma 5.4

For every request sequence, the algorithm never exceeds a capacity, and for every feasible fractional routing $f$,

Milestone: Theorem 3.2 (packing half, on routing)

The fractional scheme's flows $f^{\mathrm{alg}}$ are feasible and $\mathrm{val}(f) \le 2\ln(P(\max)+2)\,\mathrm{val}(f^{\mathrm{alg}})$ for every feasible $f$.

Milestone: Lemma 5.3

$\Phi \le 1$ initially, $\Phi > 0$ always, and whenever the flows of a request are raised by a non-negative amount of total at most $1$, serving the request on some path or rejecting it does not increase $\Phi$.

Significance

The result shows that a deterministic online algorithm for throughput-competitive routing, previously designed by hand, falls out of two generic components: an online fractional packing scheme and an online pessimistic estimator. A side product is that the fractional phase alone produces, online, a near-optimal routing that respects all capacities exactly, independently of their size. When $u(\min) \ge \log n$ the rounding loses only a constant factor and the algorithm is $O(\log P(\max))$-competitive, as in Awerbuch–Azar–Plotkin.

The results are proved in the paper; none is machine-checked. A formalization supplies a checked instance of the online primal–dual method together with derandomized online rounding, and fixes the constants the paper leaves inside $O(\cdot)$. Related platform content: the monograph's OnlinePrimalDual.Routing.per_copy_guarantee and routing_competitive concern the Buchbinder–Naor $(1, O(\log n))$-competitive algorithm with copies of the graph, a different scheme.

Difficulty

The fractional guarantee is argued in the paper continuously (rates of change of the primal and dual values), while the scheme as formalized is discrete: each flow is the least value restoring a constraint, and every primal variable is a maximum whose branch may switch during the increase. The continuous argument does not transfer verbatim, and feasibility depends on the least value restoring the constraint with equality.

The rounding is a derandomization. The existence of a good path or a good rejection is established in the paper as an expectation over a random trial; a deterministic statement about finitely many alternatives is what the mission asks for, with all $m+1$ exponential terms of $\Phi$ under control at once. A frequent first attempt compares with the potential after the fractional round; the rule compares with $\Phi^{\mathrm{start}}$, before the flow increase, and the guarantee is stated for that comparison.

Formalization scope

• Edges are a non-empty Fintype E; capacities are real and positive. A request is a List (Finset E) of paths; the request sequence is a list. Simple paths of a graph are a special case; nothing in the argument uses graph structure. $P(\max)$ is a parameter with every path of size at most $P(\max)$.
• A routing is a List (List ℝ) of the shape of the request sequence. $\mathrm{OPT}$ is quantified as "every feasible fractional routing".
• The continuous increase is its discrete equivalent (an attained sInf). Ties among good paths are broken by list order; only paths that received flow in the current round are candidates for serving, so a request whose flow was not increased is rejected.
• Explicit constants replacing $O(\cdot)$: Theorem 3.2's $O(\log \ell)$ becomes $2\ln(1+\ell) = 2\ln(P(\max)+2)$; Lemma 5.4's $O(\log P(\max)\cdot[\exp(1+2\ln m/u(\min))-1])$ becomes $4B\ln 2\cdot\ln(P(\max)+2)$ with additive $-1$, where $B = \exp(1+\ln(2m)/u(\min))-1$ is the scale chosen on p. 15. The printed "$2\ln m$" differs from the proof's "$\ln 2m$"; the proof's constant is used (it is at least as strong for $m \ge 2$). All logarithms are natural.
• The algorithm is a fully specified function: a formalization in which requests are never served, or $\mathrm{OPT}$ is a free variable pinned by hypotheses, would trivialize the goal and is ruled out.
• Not included: the covering half of Theorem 3.2, and the remark on $u(\min) \ge \log n$.

Contributions welcome: proofs of the milestones, a reusable lemma "convex combination $\le$ value $\Rightarrow$ some outcome $\le$ value" for derandomization, and the discrete-to-continuous bridge for the Section 3 scheme.

Selected references

• N. Buchbinder, J. Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research, 2009. https://doi.org/10.1287/moor.1080.0363
• B. Awerbuch, Y. Azar, S. Plotkin, Throughput-Competitive On-Line Routing, Proc. 34th FOCS, pp. 32–40, 1993. https://doi.org/10.1109/SFCS.1993.366884
• P. Raghavan, Probabilistic construction of deterministic algorithms: approximating packing integer programs, J. Comput. Syst. Sci. 37(2), 1988. https://doi.org/10.1016/0022-0000(88)90003-7
• P. Raghavan, C. D. Thompson, Randomized rounding: a technique for provably good algorithms and algorithmic proofs, Combinatorica 7(4), 1987. https://doi.org/10.1007/BF02579324

Motivation

Many resource-allocation problems arrive one request at a time and must be answered immediately: a bandwidth request is admitted or refused when it appears, an advertiser's budget is charged when a query arrives, a job is accepted before later jobs are seen. Their linear-programming relaxations are packing problems: maximize a total profit subject to capacity constraints, where the variables are revealed online and each must be set irrevocably when it is revealed. A standard yardstick for such an online algorithm is its competitive ratio, the worst-case ratio between the offline optimum and the algorithm's value.

Buchbinder and Naor (Math. Oper. Res. 2009) gave a single online primal-dual scheme for the general online fractional packing problem, together with a matching scheme for covering. The scheme raises the newly revealed packing variable while increasing the dual covering variables along an exponential curve, and its analysis is a short primal-dual argument. Earlier online algorithms for throughput-competitive routing and for set cover (Alon et al. 2009) can be read as instances of it, and the same template later became the basis of a monograph on the primal-dual approach to online algorithms (Buchbinder, Naor 2009).

This mission formalizes the paper's headline result, Theorem 3.1, for the scheme exactly as the paper defines it.

Setting

Fix a finite set $I$ of $n\ge1$ packing constraints (equivalently, primal covering variables), with known capacities $c(i)>0$. Packing variables $y(1),\dots,y(m)$ arrive one per round; in round $j$ the variable $y(j)$ is revealed together with its non-negative column $a(i,j)$, $i\in I$. The offline problems form the primal-dual pair of Figure 1 of the paper:

The profit of every $y(j)$ is normalized to $1$. Every column is assumed to have a positive entry; otherwise the packing problem is unbounded. An online algorithm may set $y(j)$ only in round $j$ and never changes it later.

The scheme with parameter $B>0$ keeps a primal vector $x$ (initially $0$) and the dual vector $y$. In round $j$ it computes the prefix maximum $a_i(\max)=\max_{k\le j}a(i,k)$. If the new covering constraint $\sum_i a(i,j)x(i)\ge1$ already holds, it sets $y(j)=0$. Otherwise it sets $y(j)$ to the least $t\ge0$ at which the constraint holds after every $x(i)$ is replaced by

After $r$ rounds, $X(r)=\sum_i c(i)x(i)$ is the primal value and $Y(r)=\sum_{k\le r}y(k)$ the dual value. For the analysis, $a_i(\max)$ and $a_i(\min)$ also denote the largest and the smallest non-zero coefficient of row $i$ over all $m$ columns.

Formalization targets

Goal: Theorem 3.1

For every $B>0$, the scheme's dual solution is non-negative; after every round $r$, every non-negative $y'$ that satisfies the packing constraints restricted to the first $r$ columns has $\sum_{k\le r}y'(k)\le B\,Y(r)$ (the scheme is $B$-competitive); and after all $m$ rounds, for every $i$,

The paper states the second part as $c(i)\cdot O\big((\log n+\log(a_i(\max)/a_i(\min)))/B\big)$; the bound above is the one its proof establishes.

Milestones: the three claims of the proof

1. Claim (i): $X(r)\le B\cdot Y(r)$ after every round $r$.
2. Claim (ii): after every round, $x\ge0$ and $x$ satisfies every covering constraint revealed so far; no $x(i)$ ever decreases.
3. Claim (iii): the violation bound of the goal.

Significance

Theorem 3.1 says that a solution within factor $B$ of the optimum can be maintained online at the price of overloading each packing constraint by a factor of order $(\log n+\log(a_{\max}/a_{\min}))/B$. Scaling the output down by the overload gives a feasible online packing solution with competitive ratio $O(\log n+\log(a_{\max}/a_{\min}))$, and Lemma 3.1 of the paper shows that no online algorithm does better up to constant factors. The same trade-off underlies the paper's online rounding results for routing (§5.2) and, through the covering counterpart, for set cover (§5.1).

The result is proved in the paper. As far as the platform's record shows, it is not formalized: the published OnlinePrimalDual.GeneralPacking.theorem14_1 (a restatement of the monograph's version) takes the inequality $X\le BY$ and primal feasibility as hypotheses on arbitrary vectors $x,y$ and derives competitiveness by weak duality; it does not mention the scheme and has no violation bound. The published OnlinePrimalDual.GeneralPacking.lemma14_2 is the matching lower bound (Lemma 3.1) and is not part of this mission. A formalization here would give the first machine-checked guarantee for the scheme itself and a reusable analysis pattern (a potential bound integrated along a monotone path) for the other schemes of the paper.

Difficulty

The paper's argument is a derivative comparison along a continuous process: while $y(j)$ rises, $\partial X/\partial y(j)\le B$. In the discrete formulation each round jumps directly to the least admissible $y(j)$, and each $x(i)$ is a maximum of its old value and an exponential, so it is continuous but not differentiable where the maximum switches; the comparison must be turned into an integral inequality over $[0,y(j)]$ for such functions. The prefix maximum $a_i(\max)$ changes between rounds, and the claim that this never lowers or raises the primal value needs an invariant ($x(i)$ is always at least the current increment value). The violation bound rests on a second invariant, $x(i)\le1/a_i(\min)$, which holds because $y(j)$ is the least admissible value; any formalization that loses minimality (for example by taking an arbitrary admissible $t$) loses claim (iii).

Formalization scope

• The instance is the published OnlinePrimalDual.GeneralPacking.GeneralInstance I (Fin m) (costs $c>0$, coefficients $a\ge0$); $n=|I|$ with [Nonempty I]; columns are Fin m, arrive in index order, and are 0-based in Lean, so "the first $r$ columns" is (k : ℕ) < r. $m\ge1$ is [NeZero m].
• $a_i(\max)$, $a_i(\min)$ over all columns are the published aMax and aMin. For a row with no non-zero coefficient aMin is $0$ and both sides of the violation bound are $0$.
• The scheme is a function, stateAfter inst B r. The continuous loop of the paper is replaced by its discrete implementation, which the paper itself prescribes (p. 4): $y(j)$ is the least $t\ge0$ restoring the new covering constraint, written as sInf. Every theorem assumes that every column has a positive entry (the paper's standing assumption, p. 4); this makes the infimum attained. If the prefix maximum is $0$, Lean's $1/0=0$ gives increment $0$, which agrees with the paper's bracket being $0$.
• Explicit constant. The paper's $c(i)\cdot O((\log n+\log(a_i(\max)/a_i(\min)))/B)$ is instantiated as $c(i)\cdot 2\log(1+n\,a_i(\max)/a_i(\min))/B$, from claim (iii) of the proof. Logarithms are natural (Real.log), since they invert Real.exp.
• $B$-competitiveness is stated against every non-negative feasible packing solution of every prefix of the input, not only at the end.
• A formalization in which the inequality $X\le BY$, primal feasibility, or the bound $x(i)\le1/a_i(\min)$ is assumed rather than derived from the scheme is ruled out: every statement here is about the vectors the scheme computes from the instance.
• Needed infrastructure: monotonicity and continuity of the per-round primal path, attainment of the infimum, an integral (or mean-value) form of the derivative comparison for maxima of exponentials, and weak duality for finite LPs. The weak-duality step and the per-round integration lemma are reusable for missions 2–4 of this series. Proofs of the milestones, and of helper lemmas such as the invariant $x(i)\le1/a_i(\min)$, are welcome.

Selected references

• N. Buchbinder, J. Naor, Online Primal-Dual Algorithms for Covering and Packing, Mathematics of Operations Research, 2009. https://doi.org/10.1287/moor.1080.0363
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal-Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3), 2009. https://doi.org/10.1561/0400000024
• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2), 2009. https://doi.org/10.1137/060661946

Motivation

A disjunctive normal form (DNF) is a disjunction of terms, each term a conjunction of Boolean literals. An unambiguous DNF has pairwise disjoint terms: no Boolean assignment satisfies two different terms. This restriction makes several tasks easy. In particular, the cited open-problem entry records polynomial-time algorithms for weighted satisfiability on unambiguous DNFs and for unweighted falsifiability. The unresolved boundary is weighted falsifiability: can one find a high-weight assignment outside the union of the terms, without enumerating all assignments?

This question is relevant to the complexity of negating compact representations of Boolean functions. Amarilli's entry observes that, since unambiguous DNFs are d-DNNFs, a polynomial-time negation procedure for d-DNNFs would yield a polynomial-time solution to weighted falsifiability on unambiguous DNFs by applying weighted satisfiability to the negated representation. Conversely, if weighted falsifiability for unambiguous DNFs—or even for d-DNNFs—is NP-hard, then, unless $\mathrm{P}=\mathrm{NP}$, d-DNNFs cannot be negated in polynomial time. These are implications stated by the source, not results established by this mission.

Historical note

The question appears on Albertine Amarilli's open-problem list. The entry cites a Theoretical Computer Science Stack Exchange question by Mikaël Monet and credits him with helping prepare the entry. It records two partial tractability results: weighted satisfiability with binary weights, and weighted falsifiability when the variable weights are unary. The entry gives no date for when the problem was posed or last seen open, so this description does not assign one. The linked discussion is useful context, not a novelty or resolution certificate.

Setting

Let $X=\{x_0,\ldots,x_{n-1}\}$ be exactly the variables occurring in the DNF. The formal input declares this finite universe by its size $n$; validity requires every declared variable to occur in at least one literal. An input DNF is a finite list of terms, and each term is a finite list of signed variable indices. An assignment is a function $\nu:X\to\{0,1\}$. A positive literal $x_i$ is true when $\nu(x_i)=1$; a negative literal $\neg x_i$ is true when $\nu(x_i)=0$. A term is true when all its literals are true, and the DNF is true when at least one term is true. Thus the empty DNF is false and an empty term is true.

The input also contains one positive integer weight $c_i$ for each variable and a positive threshold $t$. The weight of an assignment is

The DNF is valid for this problem when every literal index is below $n$ and every pair of distinct terms is mutually unsatisfiable. The decision question is whether there exists an assignment that falsifies the DNF and has weight at least $t$.

Formalization targets

Partial result — weighted satisfiability

For valid unambiguous DNF inputs with positive binary-encoded weights and threshold, the decision problem asking whether a satisfying assignment has weight at least $t$ has a deterministic polynomial-time algorithm. This is the weighted-satisfiability baseline recorded in the source entry. It is a separate result from the goal below.

Partial result — unary-weight falsifiability

For the same valid DNF model, when each variable weight is encoded in unary, weighted falsifiability has a deterministic polynomial-time algorithm. The threshold remains binary-encoded in this formalization. The source entry records this unary-weight restriction as tractable.

Goal — binary-weight falsifiability

For arbitrary positive binary-encoded variable weights and a positive binary-encoded threshold, determine whether one fixed deterministic Turing machine and one polynomial time bound decide weighted falsifiability for every valid input. The machine must be correct on all valid instances; its running-time bound is uniform and measured in the length of the explicit input code. No witness output is required.

The two partial results are reference points, not assumptions from which the goal is claimed to follow. The goal is the open binary-weight case; it must not be replaced by the satisfiability problem or by the unary-weight restriction.

Dependency graph

Input, semantics, validity, and serialization definitions
├── binary-weight weighted satisfiability (source baseline)
├── unary-weight weighted falsifiability (source baseline)
└── binary-weight weighted falsifiability (open goal)

Each branch shares the same finite DNF model and correctness predicates. The arrows indicate required definitions and scope, not a claim that either partial theorem implies the open goal.

Significance

A positive result would give a uniform algorithm for finding whether a disjoint union of Boolean subcubes omits any sufficiently heavy point, even when weights are represented compactly in binary. A negative complexity result would identify a sharp obstruction to efficient complement-related operations on these representations. The exact-weight version (asking for weight exactly $t$) is a different problem and is outside this mission's scope; the goal here is specifically weight at least $t$.

Formalizing the question fixes the universe of variables, signed-literal semantics, unambiguity condition, threshold direction, input encoding, and computational model. It also makes the unary and satisfiability baselines comparable to the binary-weight goal without treating a finite search or a candidate implementation as a complexity proof. No solution is supplied or presumed here.

Difficulty

The direct search over all $2^n$ assignments is exponential in $n$. Counting satisfying assignments is enough to settle ordinary falsifiability, but a weighted threshold partitions assignments by exponentially many possible total weights when the weights are binary. The unary dynamic program therefore does not by itself give a polynomial bound in the binary input length. Conversely, solving weighted satisfiability on the DNF does not answer whether a heavy assignment lies outside it. The task is to settle that gap without silently replacing binary magnitude by unary size.

Formalization scope

The Lean model uses Input, an explicit variable count, a list of signed-index terms, a weight list, and a threshold. validInput requires exactly one positive weight per variable, positive weights and threshold, in-range literal indices, that every declared variable occurs in the formula, and pairwise unsatisfiable distinct terms. The finite assignment type is Fin n → Bool; unused variables remain part of the input. The decision predicate is existential and exact.

The binary code includes the variable count, every list count and delimiter, all signed indices, all weights, and the threshold. Natural-number payloads use canonical binary digits with an explicit unary length prefix. The unary-weight code changes only the variable-weight payloads to unary; formula data and threshold remain binary. The complexity statements use Mathlib's bundled deterministic Turing.TM2ComputableInPolyTime model, with a single machine and polynomial bound in the chosen code length. This formalization does not claim refinement to JSON, CPython, or any runtime implementation. Human review should check the encoding/decoder round-trip and the source correspondence before launch.

The reusable definitions are the finite DNF semantics, weighted assignment score, validity predicate, binary/unary encoders, and exact decision predicates. Formalizing the two cited partial results is part of the mission's milestone path; neither is evidence that the binary-weight goal is solved.

Selected references

• Albertine Amarilli, “Weighted falsifiability for unambiguous DNFs,” List of open questions in theoretical computer science, https://a3nm.net/work/research/questions/#weighted-falsifiability-for-unambiguous-dnfs.
• Mikaël Monet, “Is this problem on unambiguous DNFs hard?”, Theoretical Computer Science Stack Exchange, https://cstheory.stackexchange.com/questions/53733/is-this-problem-on-unambiguous-dnfs-hard.

Motivation

A QMA verifier receives a quantum witness and checks it with a circuit generated efficiently from the input. An acceptance probability separated by an inverse-polynomial gap is enough to define the class, but applications often need the probability of a wrong answer to be exponentially small. Repeating the verifier on many supplied witness registers achieves this error reduction while allowing the witness to grow. Marriott and Watrous proved the stronger statement that the same error reduction can be obtained without increasing the number of witness qubits Quantum Arthur–Merlin Games, Section 3.

The existing Lean development verifies the copy-based theorem, including soundness for witnesses entangled across the copies, and constructs a uniform circuit family with polynomial resources. This mission asks for the separate witness-preserving theorem. The paper already proves that mathematical statement; the open work here is its formalization in the stated QMA circuit model.

Setting

At each input length $n$, a verifier has $m(n)$ witness qubits, a finite work register, a designated output wire, and a quantum circuit. A uniformly generated family has a polynomial-time classical procedure that emits the complete circuit description, including the witness and work-register sizes. On yes-instances, some normalized witness makes the verifier accept with probability at least $a(n)$. On no-instances, every normalized witness is accepted with probability at most $b(n)$. The thresholds satisfy $0\le b(n)\le a(n)\le1$ and $a(n)-b(n)\ge1/q(n)$ for a polynomial $q$.

The existing formalization represents witnesses as complex amplitude functions on bit strings, requires normalization explicitly, and uses layered circuits over its specified finite gate set. It also represents efficiently available real thresholds by polynomial-time procedures that output dyadic approximations. These are part of the formal statement's interface and must be made visible to users of the mission.

Target

For every polynomial error exponent $r$ and every source verifier satisfying the conditions above, construct a uniformly generated, well-formed, polynomial-resource verifier for the same language, with completeness at least $1-2^{-r(n)}$ and soundness at most $2^{-r(n)}$, while keeping the witness count exactly $m(n)$ at every input length:

This is the witness-preserving strong error-reduction result of Marriott and Watrous (Theorem 4). The existing copy-based result corresponds to the weaker QMA class inclusion in Theorem 3 and will be linked as a proved background result. The mission goal must state the witness-count equation explicitly so that a copy-based amplifier cannot satisfy it.

Significance

Witness-preserving amplification lets a QMA protocol demand much stronger reliability without asking the prover for a longer message. That matters whenever witness size is itself a resource being compared or bounded. The copy-based theorem shows that the QMA class is robust under error reduction, but does not establish this fixed-message guarantee.

Formalizing the stronger result would add a reusable account of a verifier that reuses one witness, proves soundness for every normalized input state, and compiles its behavior into an ordinary uniform circuit family. Those components can support later formalizations that reason about repeated quantum verification under a fixed witness budget.

Difficulty

The completed copy-based proof uses three independent verifier blocks in each amplification round and bounds arbitrary entangled witnesses across those blocks. Its circuit resource analysis therefore allows the witness count to grow. A witness-preserving argument cannot use that construction. It must analyze repeated verification on one register and establish exponentially small error without assuming the input witness has a special spectral form. The formal circuit model currently exposes final-output measurements; any additional measurement behavior used in the analysis must be justified in that model and shown implementable by a finite, uniformly generated circuit.

The central audit point is the exact witness-length equation. A theorem that merely returns another polynomial-size witness, or that changes the source verifier's witness definition, is a useful class-level result but does not prove this mission's target.

Formalization scope

The goal is parameterized by input-length-dependent completeness and soundness thresholds with an inverse-polynomial gap, and by a polynomial target exponent. Every witness quantifier is over normalized states. The output verifier must satisfy the same well-formedness and polynomial-resource conditions as the completed copy-based development. The platform statement uses its existing ShiClassQMAU.UniformQMA circuit-family encoding, which includes the witness and ancilla counts separately. A final proof should be kernel checked with only Lean's standard logical axioms and should not assume an amplification transducer or an unproved measurement lemma.

The paper quantifies over the class poly of unary-time constructible functions. This proposal represents the gap denominator and target exponent as literal Polynomial ℕ values, matching the checked copy-based development. It therefore formalizes a polynomial-parameter instance of Theorem 4 rather than the paper's full function-class generality. The threshold functions are supplied by polynomial-time dyadic approximators in place of the paper's informal efficient-computation convention. These interface choices are explicit in the Lean goal and should not be read as a proof of the broader formulation.

The local copy-based proof is complete and audited, but it has not yet been transplanted to Prove2Me. Its publication is preparatory work for this mission, not evidence that the witness-preserving goal is already solved. The proposal should reference the published copy-based endpoint and include only a few substantial milestones, so each item is meaningful to audit.

Selected references

• C. Marriott and J. Watrous, Quantum Arthur–Merlin Games, Computational Complexity 14 (2005), Section 3, Theorems 3 and 4. Paper.
• A. Kitaev, A. Shen, and M. Vyalyi, Classical and Quantum Computation, Graduate Studies in Mathematics 47, American Mathematical Society (2002), Section 14.2, cited by Marriott and Watrous for the copy-based amplification proof.

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$-competitive, and the best randomized algorithms are $\Theta(\log k)$-competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

• 1966: Bélády's furthest-in-future rule is optimal offline.
• 1985: Sleator and Tarjan show that deterministic online paging is at best $k$-competitive.
• 1991: Fiat et al. introduce the Marker algorithm, $2H_k$-competitive, and the clean-element lower bound on the optimum.
• 2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$-accurate predictor.
• 2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$. A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$.

With each request $z_i$ the algorithm receives a real prediction $h_i$. The true label $y_i$ is the position of the next request of $z_i$, or $n+1$ if there is none. For a loss function $\ell \ge 0$, the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$, and the predictions are $\epsilon$-accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$.

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$.

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$, the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$.

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$, every tie-breaking rule, and every sequence with $\epsilon$-accurate predictions,

Milestones

• Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$.
• Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$.
• Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$, where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
• Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$.

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ($\epsilon = 0$) the ratio is a constant, $2(1 + 2S(0))$, independent of $k$; for an arbitrary predictor it is $4H_k$, within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$, so the ratio grows like $\sqrt\epsilon$. The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$.

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$, not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$.

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$.

The spread takes real arguments and lengths $T \ge 1$. $S$ must be concave on $[0,\infty)$, finite, and at least the spread. It must also be continuous at $0$, which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$-accuracy is the pointwise condition on the given pair $(\sigma, h)$. The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$, with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$.

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

• T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
• D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
• A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716

Motivation

Metrical task systems, introduced by Borodin, Linial and Saks (J. ACM 39(4), 1992), are a common abstraction of on-line problems in which a server occupies one of finitely many states, pays a cost for each task depending on its current state, and may pay a transition cost to change state first. Paging, list update and the $k$-server problem all fit into this framework. The paper's first main result is that every deterministic on-line algorithm on an $n$-state metrical task system has competitive ratio at least $2n-1$, and that $2n-1$ is attained. The lower bound comes from an adversary that always charges the state the algorithm currently occupies. That adversary needs to know the algorithm's state, which suggests that randomization can help.

Section 7 of the paper makes this precise for the simplest system, the uniform task system, in which all transitions cost $1$. There the randomized competitive ratio against an oblivious adversary is between $H(n)$ and $2H(n)$, where $H(n)=1+\tfrac12+\cdots+\tfrac1n$ is between $\ln n$ and $1+\ln n$. This was the first logarithmic bound for a task system.

Timeline:

• 1985: Sleator and Tarjan introduce competitive analysis for list update and paging (CACM 28(2)).
• 1987/1992: Borodin, Linial and Saks define metrical task systems, prove the deterministic ratio $2n-1$, and prove $H(n)\le\bar w\le 2H(n)$ for the uniform system (conference version STOC 1987; journal version cited above).
• 1991: Fiat, Karp, Luby, McGeoch, Sleator and Young prove the analogous $2H_k$ upper bound for randomized paging (J. Algorithms 12(4)).

Setting

A task system $(S,d)$ is a finite set $S$ of $n$ states with a transition-cost matrix $d$: $d(i,i)=0$, $d(i,j)>0$ for $i\ne j$, and $d(i,k)\le d(i,j)+d(j,k)$. In the uniform task system, $d(i,j)=1$ for all $i\neq j$. A task is a vector $T\in\mathbb R_{\ge0}^S$ of processing costs. Given an initial state $s_0$ and tasks $\mathbf T=T^1\cdots T^m$, a schedule is $\sigma:\{0,\dots,m\}\to S$ with $\sigma(0)=s_0$, of cost

The off-line optimum $c_0(\mathbf T)$ is the least cost over all schedules.

A deterministic on-line algorithm chooses $\sigma(i)$ from $s_0$ and $T^1,\dots,T^i$. A randomized on-line algorithm $R$ chooses $\sigma(i)$ at random, with a distribution that depends on $s_0$, on $T^1,\dots,T^i$ and on the states $\sigma(0),\dots,\sigma(i-1)$ already visited. The task sequence is fixed before any random choice is made (an oblivious adversary). With $\mathrm{pr}(\sigma\mid\mathbf T)$ the probability that $R$ follows $\sigma$, the expected cost is $\bar c_R(\mathbf T)=\sum_\sigma c(\mathbf T;\sigma)\,\mathrm{pr}(\sigma\mid\mathbf T)$. For $w>0$, $R$ is expected $w$-competitive if there is a constant $K$ with

for every finite task sequence and every initial state. The randomized competitive ratio $\bar w(S,d)$ is the infimum of all such $w$ over all $R$.

Formalization targets

Goal: Theorem 7.1

For the uniform task system on $n\ge1$ states,

Milestones

1. Upper bound (p. 759). Some randomized on-line algorithm is expected $2H(n)$-competitive on the uniform task system.
2. Lemma 7.2 (p. 759). Let $D$ be a distribution on infinite task sequences over a finite task alphabet, with $E(c_0(\mathbf T^j))\to\infty$, and let $m_j=\inf_A E(c_A(\mathbf T^j))$ over deterministic on-line algorithms. Then every achievable $w$ satisfies

3. $m_j\ge j/n$ (p. 760) when the tasks are independent uniformly random unit elementary tasks $U_s$ (cost $1$ in $s$, $0$ elsewhere).
4. Coupon collector (p. 760). For i.i.d. uniform states on $S$, the expected number of draws until every state has appeared is $nH(n)$.
5. Off-line cost (p. 760). Under the same distribution, $E(c_0(\mathbf T^j))\le j/(nH(n))+C$ for a constant $C$ independent of $j$.

Significance

The theorem shows that randomization reduces the competitive ratio of the uniform task system from $2n-1$ to $\Theta(\log n)$. That is an exponential improvement, and it identifies the adversary's knowledge of the algorithm's state as the source of the deterministic lower bound. Lemma 7.2 is a form of Yao's principle adapted to the additive-constant definition of competitiveness. It is the standard tool for randomized lower bounds in on-line computation, and the same argument shape reappears for paging and $k$-server lower bounds.

On the formalization side, the result is proved but, as far as is known, has not been machine-checked. A complete development yields a reusable model of randomized on-line algorithms with oblivious adversaries, a Yao-type lemma usable for other on-line problems, and a coupon-collector expectation in the product-measure setting. The upper half additionally needs the continuous-time reduction of the paper's Lemma 3.1 in randomized form, or a direct discrete-time algorithm.

Difficulty

For the upper bound, the natural algorithm is continuous-time. It proceeds in phases, and inside a phase it stays in a state until that state has accumulated cost $1$. A discrete task can saturate several states at once and straddle a phase boundary. So a discrete algorithm must either simulate the continuous one or be analyzed directly, and the expected transition count per phase must be controlled with the first phase starting in a deterministic state.

For the lower bound, the first obstacle is that the natural statement "$\bar w\ge\limsup m_j/E(c_0)$" silently assumes that a randomized algorithm's expected cost, averaged over random inputs, is at least that of the best deterministic algorithm. With the behavioural (kernel) definition used here, this requires converting a kernel into a mixture of deterministic algorithms, which is Kuhn's theorem on each finite horizon. The second obstacle is that the paper's claim $E(c_0(\mathbf T^j))\le j/(nH(n))+O(1)$ is supported only by the elementary renewal theorem, which gives a limit of ratios; the additive bound needs a sharper renewal estimate. Mathlib has no renewal theory. The hypothesis $E(c_0(\mathbf T^j))\to\infty$ of Lemma 7.2 must also be established for the uniform distribution; the paper does not prove it separately.

Formalization scope

• States form a finite nonempty type S, and $n$ = Fintype.card S; no $n\ge2$ assumption is made (at $n=1$ the goal reads $1\le\bar w\le2$, and $\bar w=1$). $H(n)$ is Mathlib's harmonic n, cast to $\mathbb R$. The uniform system has unit transition cost.
• Tasks are finite and nonnegative. The paper also allows $+\infty$ entries; these are excluded. Task sequences are Fin m → S → ℝ and schedules are Fin (m+1) → S with σ 0 = s₀. $c_0$ is a finite minimum.
• A randomized algorithm is a kernel S → List (S → ℝ) → List S → PMF S. This is the paper's scheduler–taskmaster description (p. 758), equivalent to a distribution over deterministic algorithms on every finite task sequence. $\mathrm{pr}(\sigma\mid\mathbf T)$ is the product of kernel probabilities, and $\bar c_R$ is a finite sum. That $\mathrm{pr}(\cdot\mid\mathbf T)$ sums to $1$ has been checked locally.
• $\bar w(S,d)$ is the real sInf of $\{w : \exists R,\ R \text{ expected } w\text{-competitive}\}$. On the empty set this would be $0$, so the upper bound is stated as the existence of an expected $2H(n)$-competitive algorithm, and Lemma 7.2 is stated for every achievable $w$. The goal's lower half forces the set to be nonempty. Statements of the form "$\bar w\le c$" alone are therefore not acceptable substitutes for milestones 1 and 2.
• Lemma 7.2 is restricted to task sequences over a finite alphabet, with the product $\sigma$-algebra and measurable singletons. This makes every $E(c_A(\mathbf T^j))$ a genuine integral for every deterministic $A$, and it covers the paper's application. The $\limsup$ of Lemma 7.2 is taken in EReal.
• The coupon-collector time takes values in $[0,\infty]$ and its expectation is a lower Lebesgue integral. Milestone 5 renders the paper's $O(1)$ as an explicit constant $C$ chosen before $j$.

Contributions welcome: proofs of any milestone; a discrete-time randomized phase algorithm; a general Kuhn-type conversion from kernels to mixtures of deterministic algorithms; renewal-theoretic lemmas.

Selected references

• A. Borodin, N. Linial, M. Saks, An Optimal On-Line Algorithm for Metrical Task System, J. ACM 39(4):745–763, 1992. https://doi.org/10.1145/146585.146588
• D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Commun. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• A. C.-C. Yao, Probabilistic Computations: Toward a Unified Measure of Complexity, FOCS 1977, 222–227. https://doi.org/10.1109/SFCS.1977.24
• S. M. Ross, Applied Probability Models with Optimization Applications, Holden-Day, 1970 (the elementary renewal theorem cited as [20] in the paper).