Answer: Both \(L_a\) and \(L_b\) exist for every permitted input. Computing both to additive error \(2^{-k}\) is possible in deterministic time polynomial in \(L+k\), hence polynomial in \(m,\tau,L,k\) on the specified domain \(m=\tau=2\).
Theorem 3.2 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateFor a bipartite matching market (da, db, p) with da ≥db, we have La(Patient2) ≤da −db da + log (db + 3) da and Lb(Patient2) ≤e −max n da−db, da 1+db o when λa, λb, T →∞. Therefore, when λa, λb, T →∞, it holds that L(Patient2) ≤da −db da + db + log (db + 3) da + db + e −max n da−db, da 1+db o . (3) If da = db, then we have a better bound: L(Patient2) ≤2e−Cda for some constant C. We observe from Theorems 3.1 and 3.2 that, when da = db, L(Greedy2) = O log da da and L(Patient2) = e−O(da). It indicates that the upper bound of L(Patient2) is exponentially smaller than that of L(Greedy2).
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(d_a\ge d_b>0\), take the population limit of bipartite markets with arrival rates \(Nd_a,Nd_b\), compatibility probability \(1/N\), and unit-rate exponential departures. Under Patient2, determine or bound the limiting unmatched-mass fractions \(L_a,L_b\), including whether the bounds of Theorem 3.2 hold.
A society is given by its support: the list of the \(\tau\) types with positive binary-rational masses; \(\tau\) denotes support size, not the number of possible types. Here \(m=\tau=2\), with types \(a,b\) and unnormalized arrival masses \(d_a\ge d_b>0\); let \(L\) be their total encoding length.
For each integer \(N\ge2\), start with an empty bipartite market. Independent Poisson arrivals have rates \(Nd_a,Nd_b\); each arrival independently forms an edge to each currently present opposite-type agent with probability \(1/N\). Edges persist until an endpoint leaves.
Each agent has an independent exponential lifetime of rate one. Patient2 observes impending expiration on either side and then matches that agent to a uniformly chosen compatible agent, if available; both immediately leave. Otherwise the expiring agent leaves unmatched. No other matches occur.
Let \(D_i^N(T)\) count type-\(i\) agents who expire unmatched by time \(T\), excluding agents still present. Define \(\ell_i^N=\lim_{T\to\infty}\mathbb E[D_i^N(T)]/(Nd_iT)\) and \(L_i=\lim_{N\to\infty}\ell_i^N\), whenever these limits exist.
Do \(L_a,L_b\) exist for every permitted input, and is computing both to additive error \(2^{-k}\) possible in time polynomial in \(m,\tau,L,k\), or is this numerical evaluation problem NP-hard?
Known results: For the finite-agent stochastic markets, asymptotic performance bounds give \(\limsup_{N\to\infty}\ell_a^N\le(d_a-d_b+\log(d_b+3))/d_a\) and \(\limsup_{N\to\infty}\ell_b^N\le\exp(-\max\{d_a-d_b,d_a/(1+d_b)\})\); for \(d_a=d_b=d\), total loss is at most \(2e^{-Cd}\) for an absolute \(C>0\). These already cover the specified steady-state population scaling. [Verified source](https://arxiv.org/html/2110.10824v1).
No resolution of the numerical evaluation question was found in the literature searched.
Result. Both limits exist for every permitted input. For the specified domain \(m=\tau=2\), both losses can be computed to additive error \(2^{-k}\) in deterministic time polynomial in \(L+k\).
More precisely, let \((x_*,y_*)\) be the unique positive solution of
\[ d_a=x_*+y_*(1-e^{-x_*}),\qquad d_b=y_*+x_*(1-e^{-y_*}). \]
Then
\[ L_a=\frac{x_*e^{-y_*}}{d_a},\qquad L_b=\frac{y_*e^{-x_*}}{d_b}. \]
The proof requires both a stationary-limit argument and a numerical algorithm whose running time remains polynomial when the masses are exponentially large in their encoding length.
1. The exact finite-market chain. Write \(A^N(t),B^N(t)\) for the pool sizes and put \(q_N=1-1/N\).
One can defer revealing each edge until an endpoint expires. At such an event, reveal the expiring agent’s incident edges and, if its neighborhood is nonempty, use independent randomness to select a uniformly random neighbor. All revealed edges have an endpoint that immediately leaves. The choice of the departing partner therefore uses no edges between surviving agents.
Inductively, conditional on this revealed history, all edges between surviving agents remain independent Bernoulli variables with parameter \(1/N\). Exponential memorylessness also leaves the surviving agents with independent rate-one expiration clocks. Thus the pool sizes themselves form a continuous-time Markov chain.
Its transitions from \((A,B)\) are:
| Destination | Rate |
|---|---|
| \((A+1,B)\) | \(Nd_a\) |
| \((A,B+1)\) | \(Nd_b\) |
| \((A-1,B)\) | \(Aq_N^B\) |
| \((A,B-1)\) | \(Bq_N^A\) |
| \((A-1,B-1)\) | \(A(1-q_N^B)+B(1-q_N^A)\) |
Transitions leaving the nonnegative quadrant have rate zero. These rates agree with the Patient2 chain in [Kakimura–Zhu, Section 6.3](https://arxiv.org/html/2110.10824v1#S6.SS3).
Let \(Q_N\) denote its generator and \(V(A,B)=A+B\). Direct calculation gives
\[ Q_NV(A,B) =N(d_a+d_b)-A-B-A(1-q_N^B)-B(1-q_N^A) \le N(d_a+d_b)-V(A,B). \]
The chain is nonexplosive: on a bounded time interval there are finitely many arrivals, and every expiration event decreases the population. It is irreducible because arrivals and single-agent departures have positive rates whenever applicable.
We use the standard continuous-time Foster recurrence criterion: a nonexplosive irreducible countable-state chain is positive recurrent if a nonnegative function with finite sublevel sets has generator drift at most a negative constant outside a finite set. Here \(V\) has finite sublevel sets, and the displayed bound gives drift at most \(-1\) outside a finite set. Consequently there is a unique stationary law \(\pi_N\), and the chain converges to it from the empty state.
For moment control, couple the actual market with a market that retains every agent until its natural expiration, using the same arrivals and lifetimes. Each actual pool is always a subset of the corresponding comparison pool. Starting empty, the latter pool of type \(i\) has distribution
\[ \operatorname{Poisson}\!\bigl(Nd_i(1-e^{-t})\bigr). \]
Passing to stationarity gives stochastic domination by \(\operatorname{Poisson}(Nd_i)\). In particular,
\[ \mathbb E_{\pi_N}[A^2]\le (Nd_a)^2+Nd_a,\qquad \mathbb E_{\pi_N}[B^2]\le (Nd_b)^2+Nd_b. \]
The same bounds hold uniformly in time when starting empty.
The unmatched-expiration intensities are \(Aq_N^B\) and \(Bq_N^A\). Hence
\[ \mathbb E[D_a^N(T)] =\int_0^T\mathbb E[A^N(t)q_N^{B^N(t)}]\,dt, \]
and likewise for type \(b\). Convergence to stationarity, together with the second-moment bounds and \(Aq_N^B\le A\), implies convergence of these expected intensities. Taking their Cesàro averages proves that every finite-\(N\) limit exists and that
\[ \ell_a^N=\frac{\mathbb E_{\pi_N}[Aq_N^B]}{Nd_a}, \qquad \ell_b^N=\frac{\mathbb E_{\pi_N}[Bq_N^A]}{Nd_b}. \]
2. The limiting differential equation and its equilibrium. Define
\[ f_1(x,y)=d_a-x-y(1-e^{-x}),\qquad f_2(x,y)=d_b-y-x(1-e^{-y}). \]
The limiting population equation is \(\dot z=f(z)\).
For every \(x\ge0\), define \(Y(x)\) as the unique solution in \((0,d_b]\) of
\[ Y(x)+x(1-e^{-Y(x)})=d_b. \]
Existence and uniqueness follow because the left side, as a function of \(y\), is zero at \(y=0\), at least \(d_b\) at \(y=d_b\), and has derivative \(1+xe^{-y}\ge1\).
Implicit differentiation gives
\[ Y'(x)=-\frac{1-e^{-Y(x)}}{1+xe^{-Y(x)}}, \qquad -1\le Y'(x)\le0. \]
Now put
\[ H(x)=x+Y(x)(1-e^{-x}). \]
Then
\[ H'(x) =1+Y(x)e^{-x}+(1-e^{-x})Y'(x) \ge (1+Y(x))e^{-x} \ge e^{-x}>0. \]
Furthermore, \(H(0)=0\) and \(H(d_a)>d_a\). Thus there is exactly one \(x_*\in(0,d_a)\) satisfying \(H(x_*)=d_a\). Setting \(y_*=Y(x_*)\) gives exactly one positive equilibrium.
We next prove attraction, which will justify the stationary limit. The rectangle
\[ K=[0,d_a]\times[0,d_b] \]
is invariant: on each lower boundary the corresponding drift is positive, and on each upper boundary it is nonpositive. More generally, every nonnegative solution exists globally, since \(\dot x\le d_a-x\) and \(\dot y\le d_b-y\).
The derivatives satisfy
\[ \partial_xf_1=-1-ye^{-x},\qquad \partial_yf_1=-(1-e^{-x}), \]
\[ \partial_xf_2=-(1-e^{-y}),\qquad \partial_yf_2=-1-xe^{-y}. \]
Consequently, throughout \(K\),
\[ \partial_xf_1+|\partial_yf_1|=-(1+y)e^{-x}\le-e^{-d_a}, \]
\[ \partial_yf_2+|\partial_xf_2|=-(1+x)e^{-y}\le-e^{-d_a}, \]
where the second inequality uses \(d_b\le d_a\).
For two trajectories in \(K\), their difference satisfies a linear differential equation whose coefficient matrix is the Jacobian averaged along the segment joining them. Its off-diagonal entries remain nonpositive, and both row diagonal-dominance margins are at least \(c=e^{-d_a}>0\). At a coordinate attaining the maximum absolute difference, these inequalities give
\[ D^+\|z(t)-\widetilde z(t)\|_\infty \le-c\|z(t)-\widetilde z(t)\|_\infty. \]
Therefore the flow \(\phi_t\) satisfies
\[ \|\phi_t(z)-\phi_t(\widetilde z)\|_\infty \le e^{-ct}\|z-\widetilde z\|_\infty \quad\text{for }z,\widetilde z\in K. \]
In particular, every trajectory in \(K\) converges to \((x_*,y_*)\).
3. Convergence of the stationary populations. Let \(\nu_N\) be the stationary distribution of the scaled populations \((A/N,B/N)\).
The domination already proved gives
\[ \mathbb E_{\nu_N}[x^2]\le d_a^2+\frac{d_a}{N}, \qquad \mathbb E_{\nu_N}[y^2]\le d_b^2+\frac{d_b}{N}. \]
Thus the laws \(\nu_N\) are tight and their coordinates are uniformly integrable. Moreover, Poisson concentration implies that every weak subsequential limit is supported on \(K\). For example, for every \(\eta>0\),
\[ \nu_N\{x>d_a+\eta\} \le \mathbb P\{\operatorname{Poisson}(Nd_a)>N(d_a+\eta)\} \le \frac{d_a}{N\eta^2}. \]
We verify that such subsequential limits are invariant under \(\phi_t\).
Start the scaled chain \(X^N(t)\) in stationarity. Put \(\alpha_N=-N\log q_N\); then \(\alpha_N\to1\). Its drift, extended to the nonnegative quadrant, is
\[ f_N(x,y) = \bigl(d_a-x-y(1-e^{-\alpha_Nx}), \ d_b-y-x(1-e^{-\alpha_Ny})\bigr). \]
On every fixed compact rectangle, \(f_N\to f\) uniformly, and the \(f_N\) have a common Lipschitz bound.
The compensated-jump representation is
\[ X^N(t) =X^N(0)+\int_0^t f_N(X^N(s))\,ds+M^N(t). \]
Each coordinate jump has magnitude \(1/N\). The total event rate is \(N(d_a+d_b)+A+B\), and stationarity gives \(\mathbb E[A+B]\le N(d_a+d_b)\). Doob’s inequality therefore yields, for each coordinate \(i\) and each fixed \(T\),
\[ \mathbb E\!\left[\sup_{0\le t\le T}|M_i^N(t)|^2\right] \le \frac{8T(d_a+d_b)}{N}. \]
Localization on a fixed compact rectangle is justified directly: a pool can increase only through arrivals, so
\[ \sup_{0\le t\le T}X_i^N(t) \le X_i^N(0)+\frac{P_i^N(T)}{N}, \]
where \(P_i^N(T)\) is Poisson with mean \(Nd_iT\). The initial populations and these arrival counts concentrate below fixed bounds. The corresponding deterministic trajectories are also bounded, because \(\dot z_i\le d_i-z_i\).
Subtracting the deterministic integral equation and applying Gronwall’s inequality on this compact rectangle now proves
\[ \sup_{0\le t\le T} \|X^N(t)-\phi_t(X^N(0))\|_\infty \longrightarrow0 \quad\text{in probability}. \]
If \(\nu_{N_j}\) converges weakly to \(\nu\), stationarity and this approximation imply, for every bounded continuous \(g\),
\[ \int g(z)\,\nu(dz) =\int g(\phi_t(z))\,\nu(dz). \]
Thus \(\nu\) is invariant under the deterministic flow. It is supported on \(K\), where contraction gives
\[ \int\|z-(x_*,y_*)\|_\infty\,\nu(dz) \le e^{-ct}\int\|z-(x_*,y_*)\|_\infty\,\nu(dz). \]
The integral is finite, and \(e^{-ct}<1\) for \(t>0\); hence it is zero. Therefore \(\nu=\delta_{(x_*,y_*)}\). Since every subsequential limit is this point mass,
\[ \nu_N\Longrightarrow\delta_{(x_*,y_*)}. \]
Finally,
\[ \ell_a^N=\frac1{d_a}\mathbb E_{\nu_N}[xe^{-\alpha_Ny}], \qquad \ell_b^N=\frac1{d_b}\mathbb E_{\nu_N}[ye^{-\alpha_Nx}]. \]
The integrands converge uniformly on compact sets and are bounded respectively by \(x\) and \(y\). Uniform integrability therefore proves the stated formulas for \(L_a,L_b\), and proves existence of both limits.
Subtracting the equilibrium equations also gives the useful exact identity
\[ d_a-d_b=x_*e^{-y_*}-y_*e^{-x_*}, \]
or equivalently,
\[ L_a=1-\frac{d_b}{d_a}+\frac{d_b}{d_a}L_b. \]
Thus it suffices numerically to approximate \(L_b\).
4. A certified polynomial-time algorithm. Assume \(k\ge0\), and write \(\varepsilon=2^{-k}\). Under the usual binary encoding of rational numerators and denominators, the total encoding length \(L\) permits the bounds
\[ B^{-1}\le d_b\le d_a\le B,\qquad B=2^{L+1}. \]
Define
\[ R=k+3,\qquad h=2^{-2R},\qquad \delta=\frac{\varepsilon}{32B},\qquad \theta=\frac{h\delta}{16}. \]
All these rationals have encoding length polynomial in \(L+k\). Let \(S(x)=H(x)-d_a\). On \([0,R]\), since \(e<4\),
\[ S'(x)\ge e^{-R}\ge h. \]
The algorithm evaluates \(S\) to absolute error at most \(\theta\), using the subroutine justified below.
First compute such an approximation \(\widetilde S(R)\).
We justify both branches.
In the first branch, \(S(R)\le2\theta\). If \(x_*\le R\), the derivative bound implies
\[ R-x_*\le\frac{2\theta}{h}=\frac{\delta}{8}<1. \]
If \(x_*>R\), the conclusion \(x_*>R-1\) is immediate. Since \(Y(x_*)\le d_b\), in either case
\[ L_b=\frac{Y(x_*)}{d_b}e^{-x_*} \le e^{-(R-1)} =e^{-(k+2)} <\frac{\varepsilon}{4}. \]
The exact balance identity shows that the type-\(a\) candidate has error at most \(\varepsilon/4\) as well.
In the second branch, \(S(R)>0\), whereas \(S(0)=-d_a<0\), so the root lies in \((0,R)\). At a bisection midpoint \(u\):
Thus every interval reduction uses a certified sign. Stop at the third case, or when the interval width is at most \(\delta\). The resulting \(\widehat x\) satisfies \(|\widehat x-x_*|\le\delta\).
Define \(b(x)=Y(x)e^{-x}/d_b\). Using \(|Y'|\le1\), \(Y\le d_b\), and \(d_b^{-1}\le B\), we obtain
\[ |b'(x)| =\frac{e^{-x}}{d_b}|Y'(x)-Y(x)| \le B+1\le2B. \]
Hence
\[ |b(\widehat x)-L_b|\le2B\delta=\frac{\varepsilon}{16}. \]
Compute \(Y(\widehat x)\) to absolute error \(\delta\), and \(e^{-\widehat x}\) to absolute error \(\varepsilon/32\). Clip these approximations to \([0,d_b]\) and \([0,1]\), respectively. Their product divided by \(d_b\) approximates \(b(\widehat x)\) with error at most
\[ B\delta+\frac{\varepsilon}{32}=\frac{\varepsilon}{16}. \]
The resulting approximation to \(L_b\) therefore has error at most \(\varepsilon/8\). Recover \(L_a\) from the balance identity; because \(d_b/d_a\le1\), its error is no larger.
Finally, round each candidate to the nearest multiple of \(2^{-(k+2)}\). This adds at most \(\varepsilon/8\), leaving both errors strictly below \(\varepsilon\) in either branch.
5. Bit complexity of the evaluation subroutines. It remains to verify that the preceding certified evaluations require only polynomial time.
For \(0\le x\le R\), evaluate \(Y(x)\) by bisection on \([0,d_b]\) for
\[ G_x(y)=y+x(1-e^{-y})-d_b. \]
Its derivative satisfies
\[ G_x'(y)=1+xe^{-y}\ge1. \]
To obtain absolute root error at most \(\zeta\), evaluate each midpoint residual to error at most \(\zeta/4\). If the approximate residual has absolute value at most \(\zeta/4\), the true residual has absolute value at most \(\zeta/2\), and the derivative bound certifies root error at most \(\zeta/2\). Otherwise its sign is certified, so bisection continues. An interval width at most \(\zeta\) also suffices.
There are at most \(O(\log(B/\zeta)+1)\) iterations. Evaluating the exponential to error at most \(\zeta/[4(R+1)]\) gives the required residual accuracy.
To evaluate \(S(x)\) to error \(\theta\), compute \(Y(x)\) to error \(\theta/4\) and \(e^{-x}\) to error \(\theta/(4B)\). After clipping the approximations to their valid ranges, substitution into \(S\) has error at most
\[ \frac{\theta}{4}+B\frac{\theta}{4B} =\frac{\theta}{2}\le\theta. \]
Because
\[ \log_2(1/\theta)=O(L+k), \]
the inner bisections and the outer bisection both have polynomially many iterations, using rational numbers with polynomially many bits.
For completeness, exponentials themselves admit the necessary polynomial-time approximation even when their arguments are large. Given a nonnegative rational \(t\) and requested absolute error \(2^{-P}\):
In the second case, Taylor’s theorem and \((n+1)!\ge((n+1)/e)^{n+1}\) give remainder at most
\[ \frac{t^{n+1}}{(n+1)!} \le \left(\frac{eP}{n+1}\right)^{n+1} <2^{-P}. \]
The polynomial can be evaluated with exact rational arithmetic. If the argument has bit length \(s\), a common denominator has \(O(ns+n\log n)\) bits, so this computation is polynomial in \(s+P\). Clipping its value to \([0,1]\) cannot increase the error.
All requested precision parameters satisfy \(P=O(L+k+\log(R+1))\). Consequently every subroutine, and the whole algorithm, runs in deterministic time polynomial in \(L+k\).
The argument establishes the polynomial-time alternative for the specified two-type problem.
⟨structured verdict parsed — rendered above⟩
The prover’s argument resolves the stated two-type problem. Both limits are justified, and the numerical algorithm has polynomial bit complexity under the explicitly stated ordinary binary encoding of rational numerators and denominators. I found no major or minor mathematical issues.
Deferred edge revelation is legitimate for the specified matching rule. At an expiration event, the revealed edges belong to the expiring agent, which immediately departs. Selecting its partner uses only those edges and independent selection randomness. Consequently, this event does not reveal or condition on any edge between the surviving agents.
The independence assertion concerns the deferred-revelation history, as the prover expressly states. It does not incorrectly assert independence conditional on observation of the entire graph.
Exponential memorylessness applies because neither partner selection nor prior survival uses a surviving agent’s future expiration time. The surviving expiration clocks therefore retain the stated independent rate-one laws.
All five transition rates are correct. In particular, the simultaneous-departure rate includes successful expiration events from both sides. The rates also agree with the cited [Kakimura–Zhu, Section 6.3](https://arxiv.org/html/2110.10824v1#S6.SS3) after substituting \(\lambda_i=Nd_i\) and \(p=1/N\). The restriction \(N\ge2\) ensures \(q_N>0\), so the claimed single-agent departure rates are positive whenever the corresponding population is positive.
The generator calculation for \(V=A+B\) correctly counts a matched departure as a decrease of two. Its drift bound is sufficient for the stated Foster criterion: the chain is nonexplosive and irreducible, the sublevel sets are finite, and the drift is at most a negative constant outside a finite set. The function’s generator is well defined because each state has finitely many possible transitions.
Nonexplosion follows from finite arrival counts on bounded intervals and the fact that each expiration event removes at least one agent. Irreducibility follows from positive arrival rates and positive single-agent departure rates.
The comparison process is a valid pathwise domination. Matching removes agents earlier than their natural expiration and therefore preserves the subset relation. Its Poisson marginal distributions yield the stated second-moment bounds, both from the empty initial state and under stationarity.
The unmatched-expiration intensities are exactly \(Aq_N^B\) and \(Bq_N^A\). The counting-process expectation identities therefore apply. Convergence to stationarity and the second-moment bounds justify convergence of the unbounded intensity expectations through uniform integrability. Taking Cesàro averages establishes each \(\ell_i^N\) with the claimed normalization.
The limiting drift includes an agent’s own expiration and its possible removal as the partner of an opposite-type expiring agent. The displayed \(f_1,f_2\) correctly represent both contributions.
For every \(x\ge0\), the equation defining \(Y(x)\) has a unique solution in \((0,d_b]\). The endpoint inequalities, strict positivity, and derivative lower bound are correct. Implicit differentiation gives the stated derivative, including \(-1\le Y'(x)\le0\).
The calculation of \(H'\) and its lower bound are correct. Thus \(H\) is strictly increasing. The endpoint claims \(H(0)=0\) and \(H(d_a)>d_a\) use the permitted strict positivity of both masses and establish exactly one positive equilibrium. No balanced-case exception is needed.
All boundary signs for \(K=[0,d_a]\times[0,d_b]\) are correct. The componentwise upper drift bounds, together with preservation of the nonnegative quadrant, justify global existence.
The four Jacobian entries are correct. Both row inequalities hold throughout \(K\); the second correctly uses \(d_b\le d_a\).
Averaging the Jacobian along the segment between two trajectories preserves the nonpositive off-diagonal entries and the stated row margins. The resulting upper-Dini-derivative inequality for the maximum norm correctly yields contraction with \(c=e^{-d_a}>0\).
This proves convergence within \(K\). The prover does not require attraction outside \(K\), and does not use this potentially very small contraction rate to claim an efficient numerical algorithm.
The stationary second-moment bounds establish tightness and uniform integrability. The displayed Poisson tail bound is correct and ensures that every weak subsequential limit is supported on \(K\).
The finite-\(N\) drift \(f_N\) is correctly computed, including the placement of \(\alpha_N\) in each exponential. Uniform convergence and common Lipschitz bounds hold on each fixed compact rectangle.
The total event rate is correctly identified as \(N(d_a+d_b)+A+B\). Coordinate jumps have magnitude \(1/N\), and the stationary mean population bound gives the stated Doob estimate with constant \(8\).
The arrival-count bound provides the needed localization. Both stationary initial populations and normalized arrival counts lie below suitable fixed bounds with probability tending to one. The compact-set drift estimates, martingale bound, and Gronwall argument consequently justify the stated finite-time approximation.
Stationarity and this approximation imply invariance of each subsequential limit under the deterministic flow. Contraction on \(K\) then forces that invariant law to be the equilibrium point mass. This correctly establishes convergence of the full sequence of stationary population laws.
The loss integrands converge uniformly on compact sets and are bounded by their respective population coordinates. The previously established uniform integrability therefore justifies passage to expectations.
Both formulas for \(L_a,L_b\) follow, and both limits exist in the order specified by the task.
Subtracting the equilibrium equations gives the displayed balance identity with the correct signs. Its normalized form is also correct. Since \(0<d_b/d_a\le1\), recovering \(L_a\) from an approximation to \(L_b\) cannot amplify its absolute error.
The bounds using \(B=2^{L+1}\) are valid under the explicitly stated rational encoding. All precision parameters have polynomial encoding length.
On \([0,R]\), the lower derivative bound \(S'\ge h\) is correct. The two initial branches cover all possible outcomes of the certified approximate evaluation.
In the first branch, the residual bound correctly implies \(x_*>R-1\), whether the root lies below or above \(R\). The estimate
\(e^{-(k+2)}<2^{-k}/4\)
holds for every \(k\ge0\). Both candidate losses therefore have the claimed error.
In the second branch, every retained sign is certified. The small-residual stopping rule and interval-width stopping rule both give the claimed root accuracy. The derivative estimate for \(b(x)\) is correct, as are the subsequent root, product-evaluation, and rounding error bounds.
The branch boundary, equality cases in approximate comparisons, and \(k=0\) are all handled.
The inner bisection uses \(G_x'\ge1\) correctly: a small residual certifies proximity to the root, while a residual exceeding the error threshold has a certified sign.
The exponential precision requested for residual evaluation is sufficient. The error budget for evaluating \(S(x)\) is also correct after clipping.
Both bisection depths are polynomial in \(L+k\). Their rational endpoints have polynomial bit length, including when the masses are exponentially large in \(L\).
The exponential subroutine is valid. Returning zero for \(t\ge P\) meets the requested absolute error. Otherwise, the displayed Taylor remainder bound holds for the chosen degree. Exact rational evaluation has the stated polynomial bit complexity despite cancellation in the alternating polynomial.
Thus the algorithm’s running time depends polynomially on encoding length and requested precision, rather than on the numerical magnitudes of the masses.
No repair or additional clarification is needed. The conclusion applies to the specified domain \(m=\tau=2\); the prover does not claim a result for variable support size.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.