Randomized quasipolynomial-time mean-payoff games

Proof. For a cycle of length \ell\in\{1,\ldots,n\} and integer w-sum c, the new sum is (n+1)c+\ell. If c\ge0 this is at least one. If c<0, then c\le-1, and the new sum is at most -(n+1)+n=-1. The calculation concerns the actual edges of the cycle and so also covers parallel edges.□

Proof. Suppose that d=\max_i(y_i-z_i)>0, and take a vertex attaining this maximum. There y_i>z_i\ge a_i and z_i<y_i\le b_i, so both defining inequalities apply. Since y\le z+d, monotonicity and translation give

Equality forces both comparison slacks to vanish:

We claim that a common tight edge leads to another vertex attaining d. At a Max vertex choose an edge e:i\to j attaining F_i(y); at a Min vertex choose one attaining F_i(z). In either case,

Every inequality is therefore an equality. The edge is tight for both vectors, and its head again attains the maximum difference.

Continue choosing edges in this way. Finiteness supplies a repeated vertex; stopping at the first repetition produces a simple cycle of edges satisfying y_i=t(e)+y_j. Summing these equalities gives a zero t-sum, in conflict with Lemma 2.1. Thus no positive maximum difference exists, proving the assertion on all coordinates.□

Proof. First inspect the fixed-point condition in one coordinate. In the strict interior it says F_i(p)=p_i, the conjunction of the two comparison inequalities. At p_i=a_i<b_i, clipping fixes p_i exactly when F_i(p)\le p_i, the active supersolution inequality. At a_i<p_i=b_i, it fixes p_i exactly when F_i(p)\ge p_i, the active subsolution inequality. A collapsed coordinate is always fixed by clipping and imposes neither comparison. Fixed points are thus precisely the vectors having both comparison properties.

The map T_{a,b} is monotone and takes the box into itself. Its first iterate is at least a, so all successive iterates from a are nondecreasing. Each strict update increases the integer sum of the coordinates by at least one, whereas the available total increase is \sum_i(b_i-a_i). This proves existence, termination, and the count, with one extra evaluation to recognize stability. If x,x' are fixed points, apply Lemma 2.3 to them in both orders to obtain x\le x' and x'\le x. Hence x=x'.□

Proof. We first locate all coordinates of x. At an interior coordinate, x_i=F_i(x), so an attaining edge is tight: x_i=t(e)+x_j. Follow such edges while the vertices remain interior. A repetition would give a simple zero-sum t-cycle, which Lemma 2.1 excludes. A boundary is therefore reached within n-1 edges. For a coordinate already on a boundary the path has length zero. Telescoping proves that every coordinate lies within nW of one boundary, giving the partition

The midpoint B_*/2=4nW separates these bands.

On the high band the subsolution inequality is active. At a high Max vertex choose an attaining edge; at a high Min vertex keep every edge. All these permitted edges satisfy

Their heads must also be high, since a low head would imply

for n\ge1. The selected Max edges, extended arbitrarily at low vertices, define a positional strategy preserving the high band against all choices of Min.

Every simple cycle in this permitted graph has nonnegative t-sum by Equation (2.6); hence it has nonnegative w-sum by Lemma 2.1. Set M=\max_e|w(e)|. Decompose any length-T prefix of any consistent play into simple cycles and a residual walk: repeatedly remove the segment ending at the first repeated vertex. The residual walk has at most n-1 edges, while the removed cycles have nonnegative original sums. The prefix weight is at least -(n-1)M. Dividing by T and taking the lower limit proves Max’s assertion, with no restriction on Min’s dependence on the past.

On the low band the supersolution inequality is active. At a low Min vertex choose an attaining edge, and at a low Max vertex keep all edges. These edges satisfy

A high head would give

so this permitted graph stays low. Extend the chosen Min edges to a positional strategy on all vertices. Each permitted simple cycle has nonpositive t-sum and therefore strictly negative integer w-sum, at most -1. In a decomposition of a length-T prefix into r simple cycles and a residual walk, the cycle lengths are at most n and the residual length at most n-1. Consequently

The upper limiting average is at most -1/n. This estimate holds for every play allowed by the chosen Min strategy, including those from history-dependent Max play. The partition into the two bands now proves the exact winning-set formula.□

Proof. Each summand km/(\alpha_i\beta_i) is smaller than one. Thus \alpha_i\beta_i>km: the two conditions \alpha_i\le k and \beta_i\le m cannot both hold. If \beta_i>m, an admissible supersolution has no support at i and must equal b_i=p_i, which is also at least y_i. Otherwise \alpha_i>k, so every admissible subsolution equals a_i=p_i there, which is at most z_i. This coordinatewise reasoning includes collapsed intervals and proves the full assertion.□

Proof. For the first change, the new support weight is

No supersolution parameter changes. Write A=\sum_i1/(\alpha_i\beta_i). Halving \alpha on H replaces this sum by

Multiplying by the new budget product 3km/5 gives the formula for R'. For the second change, the identical support calculation reads

The subsolution parameters are now unchanged, and the reciprocal-product sum again gains the factor 1+\mu(H). Finally \mu(H)\le1/2 gives the rank contraction, including equality at the endpoint.□

Proof. For the first projection, a'\le y'\le b. It is active exactly where y_i>a'_i. At such a coordinate y'_i=y_i>a'_i\ge a_i, and hence

The first inequality is the old active comparison; the second uses y'\ge y. This proves both the new comparison and support containment. At an inactive coordinate no inequality is required.

For the second projection, a\le z'\le b'. Its active coordinates are exactly those where z_i<b'_i, and at each of them z'_i=z_i<b'_i\le b_i. Thus

using the old supersolution inequality and z'\le z. Again the support can only shrink. Positive weights then give admissibility on both sides. Finally, only the lower bound defines a subsolution’s support and only the upper bound defines a supersolution’s support. Altering the other bound affects containment alone, which proves the remaining statements, including degenerate new intervals.□

Proof. The definition of d gives y-d+A\le q+A, so y' lies in the centered box. Its active-coordinate test is

Since d-2A\ge0, every active coordinate has y_i>q_i\ge a_i and belongs to the original support. At that coordinate, translation and monotonicity yield

Although y-d+A need not be in the parent box, F is defined on all integer vectors, and the old comparison was used only at an original support coordinate.

Such a coordinate has z_i<q_i\le b_i and is in S_z. There

This proves both support formulas and comparison properties. Positivity of the weights then transfers the budgets.□

Proof. We have B/(4s)>32, so \delta\ge32, whereas \delta\le B/4. In particular B-2\delta\ge B/2>0 and 2\delta\le B/(2s)\le hB. For part (i), set c=d-\delta. The threat d>B-\delta implies

It follows that a\le u=\max(y-c,a)\le y\le b. A coordinate is active precisely when y_i-a_i>c. At such a coordinate u_i=y_i-c and y_i>a_i, whence

Equation (3.3) also places every active coordinate strictly above a_i+B-hB, and therefore in the asserted inclusive set; no rounding of that real threshold is used. Finally,

with equality at a coordinate attaining d.

For part (ii), put c=e-\delta. The same inequalities show c>B-2\delta\ge B-hB and c>0, so a\le z\le v=\min(z+c,b)\le b. Its active test is b_i-z_i>c. At an active coordinate z_i<b_i, and

The active coordinate lies strictly below b_i-B+hB, giving the low set in the statement. Moreover,

with equality wherever e is attained. This proves the second part.□

Proof. We induct on the solver rank and establish the output assertions at the same time as termination. At rank zero, R<1, and the endpoint rule returns immediately in the given box. Fix a positive rank and assume these properties for every smaller-rank solver input.

An ordinary budget change multiplies R by 4/5. Reweighting a set with \mu(H)\le1/2 multiplies it by (3/5)(1+\mu(H))\le9/10. For either change,

so the child has smaller rank. Such \Ask calls terminate by the induction hypothesis. Their medians remain integer vectors in their input boxes, irrespective of comparison accuracy.

Orientation at the current rank. The only solver calls within orientation are through budget-reduced \Ask. At width B\le128s, \Basic terminates by Lemma 2.4; the returned set is either P of measure at most 1/2 or the complement of a set of measure greater than 1/2. At larger width, both D=\floor{B/(32s)} and E_0=\floor{B/8} are positive. Each reduced call uses a legitimate centered box with reference width 2D\le B/(16s). Its result lies between q_j-D and q_j+D. The integer floor of their average lies between these same integer endpoints. Since q_j\in[a,b], subsequent clipping keeps the next center in [a,b] and cannot increase its distance from q_j. Therefore

This proves that all s loop steps terminate with valid centers.

The early returns again use complements of sets with measure greater than 1/2. When both tests fail, the appended P,N each have measure at most 1/2. The child box has positive width 2E_0\le B/4 and unchanged support parameters, hence unchanged \mu. A separate induction on this decreasing positive integer width proves orientation termination and the measure assertion. After r child edges its width is at most B_*/4^r. Since g>\log_2 B_*, there are at most g edges, or g+1 invocations. The final one returns one set and each ancestor adds two, giving 1+2g\le2g+2 entries. Repeating this finite trial J times gives a well-defined majority because J is odd, and concatenation proves the list bound for \OrientPlus.

Tightening at the current rank. The solver’s small-width branch is already covered by basic iteration. Otherwise B>128s, and

Every tightening output is inside the current box. A lower update only raises a, an upper update only lowers b, and both preserve a\le b. At least one coordinate moves by \delta. The integer quantity \sum_i(b_i-a_i) starts at most nB and decreases by at least \delta at each update. There are at most nB/\delta\le8ns updates. A pass contains at most two \Ask calls and either restarts after an update or is the final pass. This gives 2(8ns+1)=16ns+2 calls.

The main continuation and its returned vector. Orientation now terminates by the argument just given. All of its sets have the required measure on every tape, so every reweighted call has smaller rank and terminates. The sole main successor has a valid subbox and reference width C. Along a chain of such successors,

After 8s(g+1) edges this last bound would be below one, because g+1>\ln B_*. In fact a chain stops already at width at most 128s. Thus it has at most K invocations. This reasoning uses the reference width, so it remains valid when a cap leaves the actual box unchanged.

Work backwards along this finite chain. All reweighted outputs lie in the node’s final tightening box, and the main output lies in its specified subbox. Their coordinatewise maximum or minimum is still in the tightening box, itself contained in the node’s input box. Backward induction therefore proves the solver output assertion and termination at the current rank. No correctness event has been used at any stage. Since orientation is invoked only after the test R<1 fails, all uses of positive rank above apply to the actual calls. This completes the rank induction.□

Proof. Fix the input and y. Count a trial as successful only when its entire output dominates y. If a strict majority of the J trials succeeds, then at each coordinate a strict majority of the entries is at least the corresponding coordinate of y. The coordinatewise median therefore dominates y. Consequently its failure requires at least t=(J+1)/2 unsuccessful trials. The lower-rank hypothesis and independence bound the probability that any specified t trials all fail by 16^{-t}. Taking a union bound over at most 2^J choices of such trials gives

For a fixed z, count a trial as successful when its entire output is at most z. A strict majority of these trials places the median below z in every coordinate, and the same count proves its bound.

To apply either argument conditionally, first fix the history preceding the call. It specifies a deterministic input and a deterministic comparison. Whenever that comparison is admissible for the specified input, the fresh independent trial bits give exactly the experiment just analyzed. Averaging these conditional bounds gives the unconditional assertion. The proof uses whole-vector trial events; it requires neither independence among coordinates nor an event valid simultaneously for different comparison vectors.□

Proof. The output-type assertion of Proposition 4.5 puts both answers at time j, and therefore their floored average, in [q_j-D,q_j+D]. Since q_j\in[a,b], clipping that average to [a,b] cannot move a coordinate farther from q_j. Starting with q_0\in[a,b], induction proves containment and the step bound without any comparison-success assumption.

For the radius estimates, B/(32s)>4, so its floor is at least half its value. Also,

Here B>128s and the global bound s\geq16 justify the middle inequality. Dividing the resulting inequality sD\leq E_0 by s gives the last inequality in Equation (5.4).

To compare a core coordinate with the initial center, write \ell_i=b_i-a_i. Then 0\leq\ell_i\leq B and

On the subsolution side, y_i\leq b_i implies

A coordinate of the high core, however, satisfies

The difference between these two bounds is at most hB+1/2, which proves Equation (5.6). During the loop each coordinate moves by at most sD in total. Keeping any one high-core coordinate in the maximum defining d_j therefore gives d_j\geq B/2-hB-sD, and in particular the first inequality of Equation (5.5).

For the supersolution, z_i\geq a_i instead gives

At a coordinate in the low core,

This proves the initial-deficit bound (5.8). Subtracting the possible movement sD proves the first inequality in Equation (5.7).

It remains to place both deviations above the child-box width. Using sD\leq B/32 and 2E_0\leq B/4, we obtain

The final inequality follows from s\geq16 and B>128s. It completes both deviation estimates.□

Proof. We first work with y and condition on the history before time j. The projection y^{j,D} is now fixed and is admissible for the second call, which retains the subsolution budget k and reduces m. This call has rank less than r, so Lemma 5.2 gives, with conditional error at most \varepsilon,

The first answer satisfies, without a correctness assumption,

Averaging gives the integer lower bound y-d_j, which is preserved by flooring. Since b\geq y\geq y-d_j, upper clipping preserves it as well; lower clipping can only help. Thus the next center obeys q_{j+1}\geq y-d_j, equivalently d_{j+1}\leq d_j.

At a light time, the exact support formula (5.10) and the qualification (5.11) also make y^{j,D} admissible for the first call, whose budget is \eta k. Allowing one more conditional error of at most \varepsilon, both answers are at least y-d_j+D. Their floored average retains this integer lower bound. Furthermore, d_j\geq2E_0\geq2D, so y-d_j+D\leq y\leq b; clipping also retains it. This yields q_{j+1}\geq y-d_j+D, or d_{j+1}\leq d_j-D.

For the separate supersolution argument, condition on the same kind of pre-step history. The first call retains the full supersolution budget, so its comparison with z^{j,D} gives, except with conditional probability \varepsilon,

The second answer always satisfies

Their average is at most z+e_j, and flooring preserves an upper bound. Lower clipping preserves it because a\leq z\leq z+e_j; upper clipping can only help. We obtain q_{j+1}\leq z+e_j and therefore e_{j+1}\leq e_j.

At a light time for z, Equation (5.12) lets us request the comparison with z^{j,D} from the second call too. With one additional conditional error of at most \varepsilon, both answers are at most z+e_j-D. Flooring respects this bound, and e_j\geq2D gives z+e_j-D\geq z\geq a, so lower clipping respects it. Hence e_{j+1}\leq e_j-D.

For either chosen side, at most two amplified comparisons are requested per step. The comparison vector and any reduced-budget qualification are determined before the appropriate fresh call. Applying the conditional assertion of Lemma 5.2 and summing over the s steps bounds the chance of any required failure by 2s\varepsilon.□

Proof. For i\in I_y, compare the definition of d_s with the initial-deficit estimate (5.6):

On the stipulated event, d_0-d_s\geq0. Since hB=B/s>128, the last expression is greater than -2hB, excluding N. More than 256 light times means at least 257 drops, and gives

Substituting this stronger bound yields

The strict inequality is exactly what is needed for i\in P.

For i\in I_z, use (5.8) to get

Nonincrease of e_j makes this strictly less than 2hB, excluding P. With at least 257 light times, e_0-e_s\geq257D, so the same arithmetic gives

Thus i\in N, as asserted.□

Proof of Proposition 5.1. We prove a quantitative version of each pointwise statement by width induction. Define the error allowance per nonterminal level by

and define the number of such levels recursively by

A recursive width is at most B/4, so \lambda(B)\leq g+1. We will bound the failure probability for each fixed qualifying comparison by \lambda(B)\gamma.

Exact orientation at small width. When B\leq128s, the procedure computes the box solution p and uses

Lemma 2.3 gives y\leq p\leq z. For a high-core coordinate, p_i\geq y_i\geq a_i+(1-h)B>a_i+B/2; hence I_y\subseteq P. For a low-core coordinate, the reference-width bound gives

so I_z\subseteq V\setminus P. If \mu(P)>1/2, the returned choice Y protects the subsolution, and the returned set V\setminus P contains the low core. Otherwise the choice Z protects the supersolution, and the returned set P contains the high core. Core containment in support transfers the assumed strict weight bound to the indicated exceptional set. In either branch that set has measure at most 1/2. Both alternatives therefore hold with zero error.

A fixed subsolution: returns explained by motion. Now take B>128s and fix y with \alpha(I_y)>\eta k. The core is nonempty. Charge an error of at most 2s\varepsilon for the event that the deviation conclusions fail, and first work on the complementary event from Lemma 5.4. Lemma 5.5 is then available for this y.

If \mu(P)>1/2, the procedure returns Y, proving the alternative directly. If it returns instead at the second test, \mu(N)>1/2, it supplies V\setminus N. Since I_y\cap N=\varnothing,

This exceptional set proves the alternative in the second early-return case as well.

Suppose neither test returns. Both P and N have measure at most 1/2 and will be appended to the child’s list. If there are more than 256 light times for y, the displacement lemma gives I_y\subseteq P. Thus \alpha(S_y\cap P)>\eta k, and the appended set already proves the parent assertion, whatever happens in the recursive call.

A fixed subsolution: transfer at the chosen iterate. It remains to handle a completed loop with at most 256 light times. Fix its entire history. The index j is chosen only now, using fresh bits, so its conditional distribution is uniform on \{0,\ldots,s-1\}. Its probability of being light is at most 256/s. This remains true on the histories where all required loop comparisons succeeded, since that event is determined before sampling.

For a sampled index that is not light, write

Then \alpha(T_y)>\eta k. In the child box use the comparison

The projection formula (5.10) makes y' admissible and gives S_{y'}\subseteq S_y. For i\in T_y,

The last inequality uses 2D\leq hB' from Equation (5.4). It places all of T_y in the child’s high core, so \alpha(I_{y'})>\eta k. In particular, the strict inequality in the preceding line is compatible with the inclusive threshold defining that core.

The completed loop and the sampled index together determine the child input and y'. Fix this information before drawing the child’s fresh bits. The width induction applies conditionally, with failure probability at most \lambda(B')\gamma. On success the child either returns Y, which the parent copies, or supplies a set H satisfying

The parent retains H. Since S_{y'}\subseteq S_y and the support weights and budgets have not changed, \alpha(S_y\cap H)>\eta k follows with the same strict threshold.

The motion argument has already settled all successful-loop histories with more than 256 light times. On the remaining successful-loop histories, the conditional sampling error is at most 256/s, and the conditional child error is at most \lambda(B')\gamma. Averaging these conditional bounds and adding the loop error gives a total failure probability for the fixed y of at most

A fixed supersolution: returns explained by motion. Fix now z with \beta(I_z)>\eta m, for a separate analysis. Its core is nonempty. Outside an error event of probability at most 2s\varepsilon, the corresponding deviation and displacement conclusions hold; in particular I_z\cap P=\varnothing. A first-test return of Y supplies V\setminus P, which contains I_z and therefore satisfies \beta(S_z\cap(V\setminus P))>\eta m. A second-test return chooses Z and directly proves the alternative.

If neither return occurs, both displacement sets have measure at most 1/2. More than 256 light times now give I_z\subseteq N. The appended set N then satisfies \beta(S_z\cap N)>\eta m, independently of the child’s outcome.

A fixed supersolution: transfer at the chosen iterate. With at most 256 light times, condition on the completed loop as before. The fresh uniform index is light with probability at most 256/s. For an index that is not light, put

Here \beta(T_z)>\eta m. The projection z' is an admissible supersolution in [a',b']=[q_j-E_0,q_j+E_0], with reference width B'=2E_0, and S_{z'}\subseteq S_z. For i\in T_z,

Thus T_z lies in the child’s low core, giving \beta(I_{z'})>\eta m. Once the loop history and j have been fixed, this is a qualified comparison determined before the recursive randomness. The induction hypothesis therefore applies. A successful child returns Z, copied by the parent, or a retained set H with \beta(S_{z'}\cap H)>\eta m. Support containment then gives \beta(S_z\cap H)>\eta m. Adding the loop, sampling, and child errors proves the same bound \lambda(B)\gamma for this fixed supersolution.

Measures, total error, and conditioning. The measure assertion holds independently of either comparison event. Every early return uses a set of measure at most 1/2, or the complement of a set of measure greater than 1/2. A recursive return appends only P,N of measure at most 1/2. Its child retains \alpha,\beta,k,m, and hence the same measure \mu; the measure bounds for its sets transfer unchanged. This proves the assertion by width induction, also in agreement with Proposition 4.5.

The accumulated error is bounded by

Indeed, s\geq2^{17}(g+1) controls the sampling term, while 2s(g+1)\leq s^2\leq J controls the loop term. Finally, J\geq16 gives J2^{-J}\leq16\,2^{-16}=1/4096. This closes both width inductions.

At each probabilistic step we fixed the relevant input and one qualified comparison before exposing fresh bits. The same sequence of arguments therefore applies after fixing any history before the initial call that determines its input and qualifying comparison. This proves the conditional assertions as well.□

Proof. Fix an input and a qualifying y. Failure of the amplified alternative means that the majority choice is Z and that no set anywhere in the concatenated list has \alpha(S_y\cap H)>\eta k. Every trial voting Z consequently failed its own alternative: it neither chose Y nor returned a qualifying set. There are at least (J+1)/2 such trials. By Proposition 5.1, each trial has failure probability at most 1/16. Independence and the same subset count used for median amplification give

For a fixed qualifying z, failure instead means a majority choice Y and no set with heavy intersection with S_z. Every Y-voting trial then failed the supersolution alternative. There are again at least (J+1)/2 such trials, giving the same probability bound.

Because all lists are retained, including those of minority trials, the absence of a qualifying set from the amplified list implies its absence from every trial’s list. Each retained entry has measure at most 1/2 by Proposition 5.1. There are at most 2g+2 entries per trial by Proposition 4.5, so concatenating the J lists has the asserted length even when entries repeat. Lastly, fixing a pre-call history fixes the trial inputs and the chosen comparison. The trial bits remain fresh and independent, so the same amplification proof gives the conditional bound.□

Proof. Condition on a possible history. If the comparison does not qualify, the event on the left is empty. Otherwise that history specifies one deterministic eligible input and comparison. The fresh bits retain their original distribution independently of the history, so the assumed pointwise bound applies. Averaging these conditional bounds proves the assertion, including its restriction to a pre-call event.□

Proof. We specify at most one comparison to request from each actual \Ask call. The analysis stops at its first failed request; the algorithm continues to execute its prescribed instructions on every tape.

The subsolution. Let y denote the current protected projection. Before a reduced-k call, the box, y, and d=\max_i(y_i-a_i) are already determined. If d>C, form

By Lemma 3.6, this is a subsolution of the current box. Its support is contained in I_y=\{i:y_i\ge a_i+B-hB\}: at an active coordinate,

At a coordinate attaining d, the projected value is u_i=a_i+\delta. If \alpha(S_u)\le\eta k, request that the call return a vector at least u. The vector and this qualification are fixed before the call, and success forces a lower-bound update. If d\le C, or if u fails to qualify, make no request at this call.

Whenever the algorithm raises the lower bound to an output r, replace the protected vector by \max(y,r). Both vectors lie below the unchanged upper bound. Lemma 3.4 therefore gives an admissible subsolution for the new box, with no larger support and no smaller coordinates. This projection needs only the unconditional fact that r lies in the old box.

At every reduced-m call that is reached, request comparison with the current y. Its full subsolution weights and budget are unchanged, so it qualifies. Success gives r\ge y; lowering the upper bound to r, if an update occurs, still contains y and leaves its defining support and inequalities unchanged.

Consider now the final pass, in which neither bound changes. Its reduced-k call used the final box and the final protected vector. If d>C but \alpha(I_y)\le\eta k, the candidate u at that call qualifies because S_u\subseteq I_y. In the absence of a charged failure its output forces an update, contradicting that this was the final pass. This proves Equation (6.1). Every candidate was fixed before its own call; identifying the final pass afterwards makes no additional probabilistic demand.

The supersolution. Let z now denote the current protected vector. At each reduced-k call request an output at most z. The call retains the full supersolution parameters, and its successful output keeps z inside the box if the lower bound is raised. Before a reduced-m call, put e=\max_i(b_i-z_i). If e>C, define

Lemma 3.6 makes v a supersolution. Its support lies in I_z=\{i:z_i\le b_i-B+hB\}, since an active coordinate satisfies b_i-z_i>e-\delta>B-2\delta\ge B-hB. A coordinate attaining e has v_i=b_i-\delta. Whenever v qualifies for the reduced budget, request an output at most v; success forces an upper-bound update. After any upper-bound update to r, project z to \min(z,r). Lemma 3.4 preserves admissibility and keeps the support from increasing. At the final pass, e>C together with \beta(I_z)\le\eta m would again force an update. This proves Equation (6.2).

The error count. For either fixed side, every requested comparison qualifies and is determined before its call until the first error. There is at most one request per call. Proposition 4.5 bounds the loop by 8ns updates, hence 8ns+1 passes and 16ns+2 calls. The first-error bound from Lemma 6.1 gives (16ns+2)\varepsilon. Conditioning first on the history before the loop gives the asserted conditional version.□

Proof. Induct on d(R), allowing every permitted box and all positive rational support parameters at each rank. Rank zero means R<1, so Lemma 3.2 proves both assertions without error. At any rank, the small-width branch B\le128s returns the exact box solution. Lemmas 2.3 and 2.4 put it above every subsolution and below every supersolution.

Now fix a positive rank and assume the assertions at all smaller ranks. Budget reductions and the reweightings of Lemma 3.3 strictly decrease rank. Thus the amplification and orientation results, and all conditional estimates proved above, are available. In particular, orientation correctness has already been established by its own width induction from these smaller-rank solver guarantees.

Fix one admissible subsolution before the present invocation starts. Follow its obligation along the actual main chain according to the preceding subsection. On arrival at a node, the entry box and comparison are functions of the computations already completed. Until the first charged error, tightening preserves admissibility and increases the protected vector. The subsequent local work either completes its obligation or passes one admissible comparison to the main successor. In the latter case, we analyze that successor’s local work next; we do not invoke an unproved same-rank guarantee.

By Equation (4.2), every tape has at most K=8s(g+1)+1 nodes in this chain. Combining the tightening count with Equation (6.4), the first-error charge at any one reached node is at most \Lambda\varepsilon, where

The 16ns+2 possible tightening requests give the first part of the count, followed by one orientation request and at most J(2g+2) reweighted requests. This conditional charge applies on precisely the histories that reach the node with no earlier error, for those histories retain the necessary comparison invariants. The first-error union bound over the whole chain gives total probability at most K\Lambda\varepsilon.

To verify success when no charged error occurs, start at the node that completes the obligation, or at the exact terminal solver if it is passed all the way to the end. Its output has the required inequality. Work backwards through the preceding nodes. Each has the local inequalities required by its maximum or minimum rule, and the main successor supplies the one passed inequality. Consequently its output dominates its protected vector. The tightening projections dominate the vector at that node’s entry, so the inequality propagates to the initial comparison. The algorithm still executes a main call below a node that completes the obligation; that computation is irrelevant to this implication.

For a fixed supersolution, follow instead the upper comparisons specified above. Tightening decreases the protected vector, the passed comparisons remain admissible, and the same backwards argument establishes the original upper bound. Its request count is again \Lambda. This is a separate analysis for the chosen supersolution; no guarantee simultaneous over all admissible comparison vectors has been used.

It remains to check the numerical error bound. Set Q=s(n+1). The global choices give Q\ge2, g+2\le s\le Q, and J=2Q^6+1\ge32. In particular,

where the last step uses J\ge10. Since Q^3\le J,

Indeed, J^2 2^{-J} decreases for integers J\ge3, and 180\cdot32^2 2^{-32}<1/16. This proves both pointwise assertions at the current rank and completes the induction.□

Proof. The vector x is both a subsolution and a supersolution, and each support has cardinality at most n. It qualifies on both sides for the prescribed unit weights and budgets. Apply Theorem 6.3 to this same deterministic vector in its two roles and to the same output p. Then

The intersection is equality of entire vectors; independence of the two events is unnecessary. On that event, Proposition 2.5 identifies the thresholded output with the complete winning set.□

Proof. There are two parts to the cost bound. We first count the solver invocations by contracting each chain of main continuations. We then show that the work attached to one invocation has polynomial bit cost, including the arithmetic in boxes that extend beyond their parents.

Write x=L+2. Explicit encoding of the graph, ownership, and edge list gives n=O(x) and |E|=O(x), and every input weight uses at most L bits. The transformation t(e)=(n+1)w(e)+1 and the definitions of W,B_* consequently imply

For the bound on s, its choice as the least sufficiently large power of two gives s<2^{18}(g+1). These estimates use the binary length of the weights, even when their magnitudes are exponential in that length.

Counting the calls made at one rank. The initial parameter is R=n^3. No descendant increases it, so the largest rank on an ancestry is

In particular, the strict rank convention gives D_*=1 when n=1.

Consider one node on a main \Solve chain. Expose the calls to \Solve inside its amplification and orientation routines, but leave smaller-rank solver calls unexpanded. The resulting counts are as follows.

• •

  The tightening loop makes at most 16ns+2 calls to \Ask, each consisting of J solver invocations. Its contribution is at most (16ns+2)J.

• •

  The \OrientPlus call performs J orientation trials. Each trial has at most g+1 levels, with at most 2s \Ask calls per level and J solver invocations per such call. This contributes at most 2s(g+1)J^2.

• •

  The concatenated exceptional list has at most J(2g+2) entries. Every entry triggers an amplified reweighted call of J solver invocations, contributing at most (2g+2)J^2.

Proposition 4.5 makes all three counts unconditional. Their sum is

Both quadratic amplification terms are needed: orientation trials contain amplified comparisons, and every entry returned by the amplified orientation has its own amplified reweighted call. Entries from minority trials and duplicate sets are all counted. Besides these smaller-rank calls, a nonterminal solver invocation makes exactly one unamplified main continuation, as shown in Figure 1.

Let N_d bound the total number of solver invocations generated by one invocation of rank at most d, including that invocation, for the fixed graph and global parameters. A rank-zero invocation returns directly. For positive rank, contract the main chain of at most K invocations from Equation (4.2). At each node of this chain there are at most A_0 immediately smaller-rank solver descendants. It follows that

There is only one main successor at each node, and its call is not amplified. This is the reason one chain can be contracted. The separation of one full-precision continuation from reduced-precision calls also appears in Parys’s parity-game recursion [22, Algorithm 2 and Section 5]; here Equation (7.3) supplies the count for our particular routines.

Equation (7.1) gives

With A=KA_0, induction in Equation (7.4) yields N_d\le(K+1)(A+1)^d. Since D_*=O(\log x), we obtain

Every step of this count used a deterministic bound on every tape. We must still bound the bit cost of the work done between these solver calls.

Controlling integer magnitudes along an ancestry. The number of calls alone does not bound coordinate sizes, because centered boxes can extend outside their parents. Consider any path of ancestry in the full subroutine tree. Every child box is contained in its parent except possibly a centered box

formed by \Orient. On every tape, its center q belongs to the parent box, its radius satisfies A\le B/8, and its reference width is 2A\le B/4. All other transitions preserve or decrease the reference width.

List the radii of just these centered transitions as A_1,A_2,\ldots. The first is at most B_*/8. After a transition of radius A_r, the width is 2A_r and cannot increase before the next such transition. Therefore A_{r+1}\le(2A_r)/8=A_r/4. The possible outward displacement of either endpoint is bounded by the convergent sum

Starting from [0,B_*], this proves that every actual endpoint, center, and returned coordinate lies in

These are real bounds on integer values; no rounding of the displayed endpoints is intended.

The temporary sums used for midpoints, differences, scalar shifts, and caps also have magnitude O(B_*). The operator F never changes, and |t(e)|\le W\le B_*, so each intermediate value t(e)+p_j has the same order of magnitude. All such integers therefore have O(\log_2(B_*+1))=O(x) bits. This includes computations in centered boxes outside the original box, independently of all comparison outcomes.

Representing the rational parameters exactly. Weights and budgets change only on a parameter-reducing edge into a solver call. There are at most D_* such edges on any ancestry. Starting from unit weights, every reachable coordinate weight is

Starting from k=m=n, the budgets have the forms

with nonnegative integer exponents. Hence each numerator and denominator of a budget or weight has O(\log(n+1)) bits. One may store reduced fractions with binary integer numerators and denominators, or store the exponents in these explicit forms.

Support sums admit a common power-of-two denominator of exponent at most D_*. The reciprocal-product sums used by R and \mu are even simpler: for S\subseteq V,

Their bit lengths are O(\log(n+1)). Exact integer arithmetic thus computes these sums and tests R<1 or \mu(S)>1/2. The support-budget tests and the height-threshold tests are likewise exact after multiplication by positive denominators. Alternatively, normalizing fractions with the Euclidean algorithm after each operation gives polynomial bit cost without retaining a special common-denominator representation.

The global integers g,s are computable by binary lengths and integer comparisons with powers of two. Neither the rank nor the real logarithms appearing in this proof must be evaluated by the algorithm. The number 2^{-J} is also solely an error bound; no rational of that value is constructed.

Bounding the local work, including terminal iterations. The bit sizes are now controlled. For the small-width branch, \Basic is used only when B\le128s, and Lemma 2.4 bounds it by

operator evaluations. Each evaluation scans the explicit edge list, adding and comparing O(x)-bit integers, then clips the result. This iteration count is independent of endpoint offsets and numerical weight magnitudes. The other terminal branch, R<1, uses no iteration. Thus neither branch entails work proportional to W or B_*.

For a concrete representation, store a subset of V as an n-bit incidence vector. Compute a coordinatewise median by sorting the J entries in each coordinate and selecting entry (J+1)/2. Majority votes, list concatenation, clipping, floored averages, and coordinate extrema take polynomially many operations on the bounded-size values above.

The work attached to one main-chain node includes at most J(g+1) orientation invocations and polynomially many local vector-loop steps. Terminal \Basic calls in these orientation invocations contribute at most J(g+1)(1+128ns) operator evaluations; they are not additional solver invocations in N_d. Keeping every center iterate and every exceptional-list entry still uses polynomial local data and work. Consequently the local work attached to one node, leaving its solver calls unexpanded, is bounded by a polynomial P(L) of absolute degree.

Generating bits and implementing the recursion. The only random primitive selects an iterate index. Because s is a power of two, exactly \log_2s fair bits select a uniform index from \{0,\ldots,s-1\}, without a rejection loop. The J trials in either amplification are run sequentially, taking fresh bits from one tape. By Proposition 4.5, each preceding subroutine terminates on every tape. Under fair randomness the unread tail after this finite stopping time supplies independent fresh bits, as required by the correctness proof. On a fixed arbitrary tape the same execution respects every deterministic call bound used above. Each orientation invocation reads at most \log_2s bits of its own, already covered by its polynomial local cost.

All routines are finite binary computations: \Ask performs its J solver calls, and \OrientPlus performs its J orientation calls. The final winning set requires n comparisons with B_*/2. Enlarge P to include this output step and the preprocessing. For the total bit cost T_d, contracting the main chain as before gives

The estimates used in Equation (7.5) now yield T_{D_*}=2^{O((\log_2(L+2))^2)}.

A uniform machine can perform every instruction on binary strings. Polynomial simulation overhead for data access or recursion in a chosen standard model changes only the absolute constant in the exponent. Arithmetic, storage manipulation, preprocessing, random bits, and all recursive simulations are thereby included, on every tape, in the asserted bound.□

Proof of Theorem 1.1. From the explicit input compute t,W,B_* according to Equation (2.1), and initialize the global parameters of Equation (4.1). Run

and return U_p=\{i\in V:p_i>B_*/2\}. Scalars in the box positions denote constant vectors.

Lemma 2.4 gives the unique deterministic solution x of [0,B_*]. Its two supports have size at most n and so satisfy the root budgets. By Corollary 6.4, the single event p=x has probability at least 7/8. On that event, Proposition 2.5 identifies U_p with the entire zero-threshold winning set for the original weights and liminf payoff, including against every opposing history-dependent strategy.

The computation terminates on every random tape by Proposition 4.5. Its full bit cost is bounded by Theorem 7.1, which already includes the preprocessing and the n final threshold comparisons. The procedures use uniform finite instructions on binary integers, exact rationals, and fair bits. Thus they supply both the stated output probability and the asserted bound on every tape.□

Proof. Run the root solver to obtain p\in[0,B_*] and check

Accept precisely when this equality holds. By Lemma 2.4, it holds if and only if p=x, the unique top-box solution. Thus acceptance certifies every coordinate, and Corollary 6.4 gives acceptance probability at least 7/8.

On acceptance, form U=\{i:p_i>B_*/2\}. At each Max vertex in U, choose an outgoing edge attaining F_i(p); at each Min vertex outside U, choose an attaining edge as well. Complete the two strategies arbitrarily at their other vertices. The two-band proof of Proposition 2.5 applies to the verified vector p=x and proves both strategy guarantees. The check and the edge selections require a scan of the explicit edge list and arithmetic on O(L+1)-bit integers, so they add only polynomial bit cost to the bounded-time trial.

For independent repetitions, the probability that the first r trials all reject is at most 8^{-r}. Hence acceptance occurs almost surely, and the expected number of trials is at most \sum_{r\ge0}8^{-r}=8/7. Multiplying by the worst-case bit cost of one trial proves the expected-time bound. This repeated procedure has no asserted time bound on every tape; each individual certifying trial retains that bound.□