← back to the atlas

d4-conf-ijcai-2021-0609 (d4-conf-ijcai-2021-0609)

Answer: —

The anchor (named result in the paper)

Theorem 1. — class: other

PDF text-layer excerpt — equations and symbol order may be approximateThere exists time-step $t_{conv}$ such that $\forall t > t_{conv}: r_{start}^n(t) = r_{start}^n(t_{conv})$, where $r_{start}^n(t)$ denotes the starting resource $r_{start}$ of agent $n$ at the stage game of time-step $t$.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given rational masses \(\mu_t\) on finitely many base types, rational per-capita capacities \(q_r\), and rational utilities and ALMA-Learning parameters, consider integer-sized populations with \(N\mu_t\) agents of type \(t\) and \(Nq_r\) unit-capacity appointments of class \(r\). Define the fluid limit of the empirical law of complete learner states, including reward histories, loss estimates, and starting resources, under the paper’s stochastic updates. Does the limiting process have a vanishing mass of agents who change starting class at some round \(s\ge H\) as \(H\to\infty\), independently of integer rounding; and, when it does, can an algorithm compute a horizon \(H(\varepsilon)\) after which that mass is at most \(\varepsilon\)?

Packaged proof task (what the prover saw — nothing else)

A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. There are \(m\ge2\) appointment classes, with rational \(\mu_t,q_r>0\), \(\sum_t\mu_t=\sum_rq_r=1\), and rational utilities \(u_t(r)\in[0,1]\). Every type can access every class; its distinct class utilities are separated by an input rational \(\delta>0\).
Parameters are a history length \(\ell\ge1\) and rational \(0<\alpha\le1\), \(\beta>0\), \(0<\eta<1/2\). Let \(L\) be the total input bit length. State algorithmic running times in \(m,\tau,L,\ell\) and the accuracy parameter.
For each \(N\), use integer type counts \(a_t^{(N)}\) and class capacities \(k_r^{(N)}\), both totaling \(N\), with \(a_t^{(N)}/N\to\mu_t\) and \(k_r^{(N)}/N\to q_r\). Appointments are distinct unit-capacity copies \((r,j)\), \(1\le j\le k_r^{(N)}\), with utility \(u_t(r)\). Order them by decreasing utility, breaking ties by class index and then copy index.
Each agent stores, separately for every appointment \(a\), a FIFO reward history of capacity \(\ell\), its mean \(v_a\), a loss estimate \(d_a\), and a starting appointment \(b\). Initially the history is the singleton \([u_t(a)]\), \(d_a=u_t(a)-u_t(a_{\mathrm{next}})\), with terminal successor utility zero, and \(b\) maximizes \(v_a\). Every maximization uses the fixed appointment order to break ties.
Each learning round resets all appointments to free and runs synchronous contention to completion. Agents initially attempt \(b\); an unclaimed appointment with exactly one requester is permanently assigned for that round. Requesters colliding with other requesters or an existing holder independently yield with probability \(p(d)=(\min\{1-\eta,\max\{\eta,1-d\}\})^\beta\); otherwise they retry. Holders retain their appointments.
A yielding agent scans the fixed appointment order cyclically, starting at its first entry after its first yield in that round. Each scan tick advances its pointer once; if the inspected appointment has neither a holder nor a current requester, the agent attempts it on the next tick. All observations refer to the beginning of the tick; all Bernoulli draws are independent across agents, ticks, and rounds.
If an agent wins \(w\), append \(u_t(w)\) only to the history of its previous start \(b\), discard the oldest entry if needed, and recompute \(v_b\). Update \(d_b\leftarrow(1-\alpha)d_b+\alpha(u_t(b)-u_t(w))\) only when \(u_t(b)>u_t(w)\). Replace \(b\) by a maximizer of \(v_a\) only when \(w\ne b\), including when the two appointments have the same class.
To compare complete states across population sizes, encode each agent's arrays by their default entries \(([u_t(r)],u_t(r),0)\) plus a finite table containing every class's final copy and every appointment ever used as a start. Preserve table-entry identities over rounds, store all histories and losses and the current-start pointer, and mark a copy by \((r,j/k_r^{(N)},j,k_r^{(N)}-j)\). Use the usual topology for normalized coordinates and one-point compactifications for the integer coordinates; table structure and identities are discrete. This encoding reconstructs the entire finite-population learner state.
A fluid limit means that, for every finite number of learning rounds, the empirical distribution of these complete state trajectories converges weakly in probability to consistent deterministic laws, yielding a trajectory law \(\nu\). Define \(A(H)=\nu\{\exists s\ge H:C_{s+1}\ne C_s\}\), where \(C_s\) is the starting appointment's class before round \(s\); take the population limit before the infinite-round tail.
Does a fluid limit independent of the integer approximations exist for every admissible input, and does it satisfy \(A(H)\to0\), or can either property fail?
On inputs for which both properties hold, can an algorithm compute, for every rational \(0<\varepsilon<1\), a finite \(H(\varepsilon)\) with \(A(H(\varepsilon))\le\varepsilon\), or can effective convergence fail?
The published finite-population convergence theorem asserts eventual almost-sure stabilization of every agent's starting appointment; it supplies no effective learning horizon ([Danassis, Wiedemair and Faltings](https://arxiv.org/pdf/2105.04027)).
The underlying finite ALMA contention procedure has a published polynomial expected convergence bound depending on its extreme back-off probabilities ([Danassis, Filos-Ratsikas and Faltings](https://www.ijcai.org/proceedings/2019/0031.pdf)). No result settling this complete-state fluid-limit question was found.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Partial solution

I prove a new existence result for a nontrivial class of inputs: if all types have the same appointment order and every utility is at most $\eta$, then the complete-state fluid limit exists and is independent of the integer approximations. In this limit, successive winning classes are independent, with probabilities $q_r$.

I also re-prove the general fixed-horizon invariant from the notes. It implies that every fluid limit, whenever it exists, satisfies $A(H)=0$ for every $H\ge 1$. Thus the promised effective-horizon problem has the constant solution $H(\varepsilon)=1$.

Universal fluid-limit existence remains unresolved.

1. Finite contention rounds terminate almost surely

For any stored loss, clipping gives
$$ p_-=\eta^\beta\le p(d)\le (1-\eta)^\beta=p_+. $$
Both endpoints lie strictly between zero and one. Consequently, with
$$ c=\min\{p_-,1-p_+\}>0, $$
every prescribed yield or retry outcome has conditional probability at least $c$.

Here is a uniform positive-probability route to obtaining another holder from any unfinished contention state.

If an unheld appointment has multiple requesters, prescribe that exactly one retries and all others yield. On the next tick, the remaining requester acquires it. No scanner can introduce another requester on that tick: its preceding observation saw a nonempty requester set.

If no unheld appointment has requesters, prescribe yielding by agents colliding with holders. Any already scheduled requests at appointments that have just acquired holders are cleared within two ticks unless an unheld request appears sooner. Otherwise, unassigned agents scan. There is an unheld appointment, because holders and assigned agents are in one-to-one correspondence and some agent remains unassigned. Within one full scan, either an unheld request appears or a scanner schedules such a request. A singleton acquires the appointment; a collision is resolved by the preceding prescription.

Thus $B=N+6$ ticks suffice for a prescribed route to another holder. At most $NB$ Bernoulli outcomes are prescribed, so the conditional probability of progress within this block is at least $c^{NB}$. The probability of no progress in $j$ successive blocks is therefore at most
$$ (1-c^{NB})^j. $$
Every additional holder is obtained almost surely. Since holders never leave and only $N$ appointments exist, the round terminates almost surely.

Taking a countable intersection establishes simultaneous termination of all learning rounds. No published contention bound is needed for this argument.

2. A fixed-horizon invariant for every admissible input

For type $t$, define
$$ U_t=\max_{1\le r\le m}u_t(r), $$
and let $r_t$ be the first class attaining this maximum in the prescribed appointment order.

Fix an integer $H\ge 1$. Positivity of every $q_r$ implies that, along any admissible capacity sequence, eventually
$$ k_r^{(N)}\ge H+2 \qquad\text{for every }r. $$
Work at such a population size. For a particular type-$t$ agent, write $z_i$ for its reward in round $i$.

Invariant. Before round $s$, for $1\le s\le H+1$, its start is
$$ b_s=(r_t,j_s), \qquad j_s=1+\#\{i<s:z_i<U_t\}. $$
The current-start history contains only $U_t$, and its loss is zero. Every previously abandoned start has mean strictly below $U_t$.

Proof. Initially the first maximizer is $(r_t,1)$. Its history is $[U_t]$, and its loss is zero because its successor is another copy of class $r_t$.

Suppose the invariant holds before round $s$. Every history entry at every appointment is an actual utility or an initial utility, hence is at most $U_t$.

If $z_s=U_t$, appending the reward preserves the current mean $U_t$, and no loss update occurs. If maximization is triggered, the current copy remains its first maximizer: all earlier copies in class $r_t$ were abandoned with strictly smaller means, while every other appointment attaining mean $U_t$ follows the current copy. Thus the start does not change.

If $z_s<U_t$, the appended reward survives FIFO truncation, including when $\ell=1$. The updated mean is strictly below $U_t$. Moreover, the winner differs from the start, so maximization is triggered. Previously abandoned copies still have strictly smaller means, since only the current start was updated. The next copy $(r_t,j_s+1)$ is untouched, has mean $U_t$, and is the first maximizer.

The new start has singleton history $[U_t]$ and zero loss. The capacity assumption ensures that it is not the final copy of its class. This proves the induction. $\square$

In particular, within this horizon:

These conclusions allow utility ties and require no quantitative use of $\delta$.

3. Conditional class stabilization and an effective horizon

Assume that a complete-state fluid limit $\nu$ exists.

For each fixed $s$, Section 2 shows that, eventually in population size, every type-$t$ agent has starting class $r_t$ before round $s$. Type and starting class are discrete coordinates of the encoded state. Passing to the assumed weak limit therefore gives
$$ \nu\{C_s=r_t\mid t\}=1. $$
Since $\mu_t>0$, this conditioning is legitimate.

Intersecting these probability-one statements over the finitely many types and countably many rounds yields
$$ \nu\{C_s=r_t\text{ for every }s\mid t\}=1. $$
Consequently,
$$ A(H)=0 \qquad\text{for every }H\ge 1. $$
This first takes the population limit at each fixed horizon and only afterward considers the infinite-round trajectory law.

An algorithm on the promised domain can therefore return
$$ H(\varepsilon)=1. $$
If $b_\varepsilon$ denotes the bit length of $\varepsilon$, its running time is $O(L+b_\varepsilon)$ including input reading, and constant after reading. There is no additional dependence on $m,\tau,\ell$, or $1/\varepsilon$. The algorithm need not decide whether the fluid-limit promise holds.

4. New existence theorem: common order and constant back-off

Consider the following additional hypotheses:

$$ u_t(\pi(1))\ge\cdots\ge u_t(\pi(m)) $$
for every type, with tied classes appearing in their prescribed class-index order.

$$ 0\le u_t(r)\le\eta. $$

These hypotheses permit strictly ordered utilities and distinct utility vectors.

Every initial loss is a difference of consecutive utilities, or the terminal utility. Hence it belongs to $[0,\eta]$. Every subsequent loss update is a convex combination of the previous loss and a positive utility difference, both in $[0,\eta]$. Thus, at every population size and every round,
$$ 0\le d_a\le\eta. $$
It follows that all back-off probabilities equal the same constant
$$ p(d_a)=p=(1-\eta)^\beta\in(0,1). $$

All agents also have the same scan order. After their first yield in a round, their contention behavior therefore depends on their random draws and the shared contention state, but not on their type, learning histories, losses, or previous start.

The following lemma makes this observation quantitative.

5. A one-round decorrelation lemma

Suppose a contention round has $N$ agents and $N$ appointments, with class capacities $k_r$. Assume that all agents have the same scan order and the same constant yield probability $p\in(0,1)$.

Give each agent one of $K$ labels. A label may encode an arbitrary previous history, but it specifies the agent’s initial starting appointment. Let $n_\lambda$ be the number with label $\lambda$, and suppose there are at most $G$ distinct starting appointments. Let $X_{\lambda r}$ count label-$\lambda$ agents ultimately assigned class $r$.

Lemma. For fixed $K,G,p$, uniformly over label counts, initial starts and capacities,
$$ \max_{\lambda,r} \left| \frac{X_{\lambda r}}N - \frac{n_\lambda}N\frac{k_r}N \right| \xrightarrow{\mathbb P}0. $$

More explicitly, put $\theta=1-p$. For all sufficiently large $N$ and every $\rho>0$,
$$ \begin{aligned} &\mathbb P\left\{ \max_{\lambda,r} \left| \frac{X_{\lambda r}}N - \frac{n_\lambda}N\frac{k_r}N \right|>\rho \right\}\\ &\quad\le G(1+N)\exp\left(-\frac{N^{1/4}}2\right) +\frac6\rho\left(GN^{-1/2}+\theta^{-1}N^{-1/4}\right) +\frac{4Km}{N\rho^2}. \end{aligned} $$

Proof: initial collision groups

Because contention rules do not use agent identities, randomly permuting the initial labels over agent identities does not change the distribution of the empirical output counts. We may therefore assume that their placement is uniform, independently of all random tapes.

Pre-generate independent geometric variables $Y_i$, with
$$ \mathbb P(Y_i>T)=\theta^T. $$
These specify the tick of an agent’s first yield if it continues colliding at its initial start. Use separate independent random tapes for its behavior after that yield. If it acquires its initial start earlier, unused draws are simply ignored. This construction has the required law of independent Bernoulli draws.

Set
$$ T_N=\left\lfloor \frac{\log N}{4(-\log\theta)} \right\rfloor. $$
Then
$$ N^{-1/4}\le\theta^{T_N}\le\theta^{-1}N^{-1/4}. $$

Call an initial-start group large if its size is at least $\sqrt N$, and small otherwise. The total size of small groups is at most $G\sqrt N$.

Let $F_N$ be the event that each large group contains at least two agents with $Y_i>T_N$. On this event, those agents remain requesters throughout the first $T_N$ collision ticks. Thus every large initial appointment stays unheld and has at least two requesters throughout that interval. In particular, every member of a large group with $Y_i\le T_N$ actually first yields at tick $Y_i$.

For a large group of size $n$, its number of such persistent requesters is binomial with mean
$$ n\theta^{T_N}\ge N^{1/4}. $$
Writing $s=\theta^{T_N}$ and using $n\ge 2$,
$$ \begin{aligned} \mathbb P\{\operatorname{Bin}(n,s)\le 1\} &=(1-s)^n+ns(1-s)^{n-1}\\ &\le e^{-ns}+ns\,e^{-s(n-1)}\\ &\le(1+N)e^{-ns/2}\\ &\le(1+N)\exp(-N^{1/4}/2). \end{aligned} $$
A union bound gives
$$ \mathbb P(F_N^c) \le G(1+N)\exp(-N^{1/4}/2). $$

Exclude all agents from small groups and all large-group agents with $Y_i>T_N$. Let $D$ be the excluded count. Then
$$ \mathbb E[D] \le G\sqrt N+N\theta^{T_N} \le G\sqrt N+\theta^{-1}N^{3/4}. $$

Proof: permutation symmetry of the remaining agents

Let $E$ be the set of nonexcluded agents, so $|E|=N-D$. On $F_N$, every agent in $E$ has yielded by tick $T_N$.

Condition on all random tapes, the excluded agents’ identities and labels, and the event $F_N$. The remaining labels are uniformly distributed over $E$, subject to their remaining counts.

Any permutation of these remaining labels leaves the entire mechanical contention trajectory unchanged:

It follows that the winning class of each agent identity is fixed under these label permutations. This conclusion concerns the complete round, whose almost-sure termination was established in Section 1.

Let $e_\lambda$ be the number of remaining labels $\lambda$, and let $K_r$ be the number of agents in $E$ winning class $r$. If $|E|>0$, the count $X^E_{\lambda r}$ is therefore hypergeometric, with conditional mean
$$ M_{\lambda r}=\frac{e_\lambda K_r}{|E|} $$
and conditional variance at most $N$. If $E$ is empty, set both quantities to zero.

Proof: comparison with the product counts

Write
$$ d_\lambda=n_\lambda-e_\lambda, \qquad d_r=k_r-K_r. $$
Both quantities are between zero and $D$. When $|E|>0$,
$$ \left| \frac{K_r}{|E|}-\frac{k_r}{N} \right| = \frac{|Dk_r/N-d_r|}{|E|} \le\frac D{|E|}. $$
Consequently,
$$ \left| M_{\lambda r}-\frac{n_\lambda k_r}{N} \right| \le e_\lambda\frac D{|E|} +d_\lambda\frac{k_r}{N} \le 2D. $$
Adding the excluded label-$\lambda$, class-$r$ winners gives
$$ \left| X_{\lambda r}-\frac{n_\lambda k_r}{N} \right| \le |X^E_{\lambda r}-M_{\lambda r}|+3D. $$
This also holds when $E$ is empty.

Conditional Chebyshev inequalities and a union bound give
$$ \mathbb P\left( F_N\cap \left\{\max_{\lambda,r} |X^E_{\lambda r}-M_{\lambda r}|>\frac{\rho N}{2} \right\} \right) \le\frac{4Km}{N\rho^2}. $$
Markov’s inequality gives
$$ \mathbb P\{D>\rho N/6\} \le \frac6\rho \left(GN^{-1/2}+\theta^{-1}N^{-1/4}\right). $$
Combining these estimates proves the displayed bound and the lemma. $\square$

6. Complete-state fluid-limit existence under the additional hypotheses

Assume the hypotheses of Section 4. The common first class is
$$ r_*=\pi(1). $$

Fix $H$. For sufficiently large populations, Section 2 applies through round $H$, and every initial start in round $s\le H$ is among
$$ (r_*,1),\ldots,(r_*,s). $$

Label an agent before round $s$ by its type and its previous winning-class word
$$ (t,r_1,\ldots,r_{s-1}). $$
There are at most
$$ K_s=\tau m^{s-1} $$
labels. Such a label determines its complete previous learner-state trajectory and its current start. There are at most $s$ distinct starts.

Let
$$ P_{N,s}(t,r_1,\ldots,r_s) $$
be the empirical fraction with that type and winning-class word. Conditional on the entire past, future draws are independent. The lemma applies uniformly with $G\le s$, giving
$$ P_{N,s}(t,r_1,\ldots,r_s) - P_{N,s-1}(t,r_1,\ldots,r_{s-1}) \frac{k_{r_s}^{(N)}}N \xrightarrow{\mathbb P}0. $$
The base case is
$$ P_{N,0}(t)=\frac{a_t^{(N)}}N\longrightarrow\mu_t. $$
Induction, using $k_r^{(N)}/N\to q_r$, now yields
$$ P_{N,H}(t,r_1,\ldots,r_H) \xrightarrow{\mathbb P} \mu_t\prod_{i=1}^H q_{r_i}. $$
All finitely many coordinates converge jointly.

Reconstruction of complete learner trajectories

For fixed type and winning-class word, the rewards are
$$ z_i=u_t(r_i). $$
Section 2 determines every starting-copy index. A current copy accumulates only optimal rewards until its first suboptimal reward. Upon abandonment, its history is the FIFO truncation of those optimal entries followed by that suboptimal reward, and its loss becomes
$$ \alpha(U_t-z_i). $$
Other nonfinal, unused copies retain their defaults. Final-copy initial losses are determined by the next class in the fixed order, or by terminal successor utility zero.

Thus the word determines the complete encoded trajectory.

At a fixed horizon, every starting-copy index $j$ is fixed independently of $N$. Its mark converges to
$$ (r_*,0,j,\infty). $$
The final copy of class $r$ has mark converging to
$$ (r,1,\infty,0). $$
The relevant table structures and entry identities are fixed for each word once capacities exceed $H+1$. Histories, means, losses and pointers are determined exactly as above. Hence each finite-population trajectory atom converges to a deterministic atom $x_{t,r_1,\ldots,r_H}$, independently of the capacity approximation.

The empirical trajectory measure is a mixture of these finitely many atoms. Its weights converge in probability to the deterministic product weights. Therefore it converges weakly in probability to
$$ \nu_H = \sum_{t=1}^{\tau} \sum_{(r_1,\ldots,r_H)\in\{1,\ldots,m\}^H} \mu_t\prod_{i=1}^Hq_{r_i}\, \delta_{x_{t,r_1,\ldots,r_H}}. $$

These laws are consistent. Explicitly, choose a type with distribution $(\mu_t)$ and, independently, an infinite sequence of independent classes with distribution $(q_r)$. Apply the learner-state reconstruction to each finite prefix. This constructs the required trajectory law $\nu$.

Proven conclusion. Under the hypotheses of Section 4, the complete-state fluid limit exists, is deterministic and independent of the integer approximations. Conditional on type, its winning classes are independent with probabilities $q_r$.

7. Algorithmic consequences

The general promised-horizon algorithm remains
$$ H(\varepsilon)=1, $$
with running time $O(L+b_\varepsilon)$ including reading.

For the additional class of inputs in Section 4, the complete fluid law through any supplied finite horizon $H$ is also exactly computable. Enumerate type and class words, assign each weight
$$ \mu_t\prod_{i=1}^Hq_{r_i}, $$
and construct its limiting complete-state trajectory as in Section 6. Coincident atoms may remain as separate mixture terms.

Here is a conservative bit-complexity bound using schoolbook arithmetic. Put
$$ h=\min\{\ell,H+1\}. $$
Checking the common orders and constructing the exact finite-horizon mixture takes
$$ O\left( \tau m\log(m+1)(L+1)^2 + \tau m^H(m+H+1)H^3h \bigl(L+\log(H+2)+1\bigr)^2 \right). $$
To justify the bound:

The mixture is exact, so this computation requires no numerical accuracy parameter. This is not an algorithm for computing limiting weights on arbitrary admissible inputs.

8. A strictly ordered example with infinite starting-copy motion

Take
$$ m=2,\qquad \tau=1,\qquad q_1=q_2=\frac12, $$
and
$$ u(1)=\frac18,\qquad u(2)=0,\qquad \eta=\frac14,\qquad \delta=\frac18,\qquad \alpha=\beta=1. $$
Any $\ell\ge1$ is allowed. This is admissible, with strictly distinct class utilities, and satisfies Section 4.

In its fluid limit, the winning classes are independent fair draws. Section 2 gives the starting-copy index before round $s$ as
$$ j_s=1+\sum_{i<s}\mathbf 1_{\{R_i=2\}}. $$
In particular,
$$ j_s\ \text{has distribution}\ 1+\operatorname{Bin}(s-1,1/2). $$

For any fixed $h$, the probability of never winning class $2$ after round $h$ is
$$ \lim_{n\to\infty}2^{-n}=0. $$
A countable union over $h$ shows that class $2$ is won infinitely often almost surely. Therefore the starting-copy index increases infinitely often almost surely, while the starting class is always class $1$ and
$$ A(H)=0 \qquad\text{for every }H\ge1. $$

Thus class stabilization and appointment-identity stabilization differ sharply in this population-first limit. The cited [finite-population learning theorem](https://arxiv.org/pdf/2105.04027) cannot by itself establish appointment stabilization in that limit. Likewise, the [finite contention-time bound](https://www.ijcai.org/proceedings/2019/0031.pdf) does not supply the concentration argument proved here.

9. What remains open

The argument proves complete-state fluid-limit existence for all common-order inputs whose utilities lie in $[0,\eta]$. It does not establish existence when scan orders differ, or when contention probabilities depend on losses.

For arbitrary admissible inputs, neither universal deterministic, approximation-independent existence nor an admissible counterexample is proved here. That is the remaining target question. Conditional class stabilization and the promised effective-horizon question are settled by Sections 2–3.

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

Verification report

Overall assessment: partial, with sound substantive progress. The fixed-horizon invariant establishes class stabilization and the constant effective horizon whenever a complete-state fluid limit exists. The additional existence theorem is supported by the decorrelation and reconstruction arguments. However, the output explicitly leaves universal existence unresolved and provides no counterexample to it, so it does not settle the entire USER_TASK.

I found no false central step or mathematical gap in the results actually proved.

1. Almost-sure termination of finite contention rounds

The clipping bounds are correct:
$$ 0<\eta^\beta\le p(d)\le(1-\eta)^\beta<1. $$
Thus every prescribed yield or retry has conditional probability at least
$$ c=\min\{\eta^\beta,1-(1-\eta)^\beta\}>0. $$

The proposed progress route respects the synchronous observation rule:

The block length
$$ B=N+6 $$
allows the full scan and the additional scheduling, clearing, and collision-resolution ticks. At most $NB$ Bernoulli outcomes occur within a block, so the probability lower bound $c^{NB}$ is valid.

The geometric failure estimate proves almost-sure acquisition of another holder. Iterating over the finitely many remaining appointments proves termination of the round. The countable intersection over learning rounds is legitimate.

Assessment: correct. This argument establishes termination, without claiming an efficient contention bound.

2. Fixed-horizon invariant

For a fixed horizon, positivity of each $q_r$ indeed implies that eventually
$$ k_r^{(N)}\ge H+2 $$
for every class.

The invariant correctly uses appointment copies rather than treating a class as one learning option.

Initialization

The first maximizer is the first copy of the earliest maximum-utility class. Its successor is another copy of that class, so its initial loss is zero. The capacity condition guarantees this successor exists.

Optimal reward

When $z_s=U_t$, appending the reward preserves the current mean and loss. Even if winning a different appointment triggers maximization, the current start remains the earliest maximizer:

This also handles ties between classes.

Suboptimal reward

When $z_s<U_t$, the newly appended reward survives FIFO truncation even for $\ell=1$. Therefore the updated mean is strictly below $U_t$.

The winner cannot equal the current start, so maximization is triggered. Previously abandoned starts retain their smaller means, and the next untouched copy is the earliest remaining maximizer. Its initial history is the singleton $[U_t]$, and its loss is zero because it is not final within the stated invariant horizon.

The index formula
$$ j_s=1+\#\{i<s:z_i<U_t\} $$
therefore follows. The claims about abandonment, loss updates, and absence of revisits also follow.

Assessment: correct, including the FIFO edge case and utility ties.

3. Conditional stabilization and effective horizon

For each fixed round, the invariant eventually places every type-$t$ agent’s start in class $r_t$. Type and starting class are discrete coordinates of the supplied encoding, so this property passes to an assumed weak limit.

Because there are finitely many types and countably many rounds, intersecting the resulting probability-one events is valid. Consequently,
$$ A(H)=0 \qquad\text{for every }H\ge1. $$

This argument correctly respects the required order of limits. It does not infer a uniform finite-population learning horizon.

The promised-domain algorithm
$$ H(\varepsilon)=1 $$
is therefore valid. Its stated running time
$$ O(L+b_\varepsilon) $$
including input reading is appropriate, and it need not recognize whether the promise holds.

Assessment: correct. Conditional on fluid-limit existence, neither class-tail convergence nor effective convergence can fail.

4. Constant back-off under the additional hypotheses

Under the restriction
$$ 0\le u_t(r)\le\eta, $$
all initial losses belong to $[0,\eta]$. Every performed update is a convex combination of a previous loss in this interval and a positive utility difference in this interval. Hence the interval is preserved.

It follows that
$$ p(d)=(1-\eta)^\beta $$
for every stored loss.

Common appointment order and constant back-off remove the stated dependence on type, history, and previous start after first yield.

Assessment: correct.

5. One-round decorrelation lemma

This is the main nontrivial probabilistic argument. Its conditioning and symmetry are valid.

Persistent initial requesters

For $\theta=1-p$, the chosen cutoff satisfies
$$ N^{-1/4}\le\theta^{T_N}\le\theta^{-1}N^{-1/4}. $$

On $F_N$, each large initial group has at least two agents whose first-yield variables exceed $T_N$. Those agents prevent singleton assignment throughout the relevant interval. Consequently, each nonexcluded agent actually yields at its prescribed tick.

The binomial estimate is correct. In particular, $n\ge2$ gives
$$ s(n-1)\ge\frac{ns}{2}, $$
and $ns\le N$ justifies the displayed factor $1+N$. The union bound and the estimate
$$ \mathbb E[D]\le G\sqrt N+\theta^{-1}N^{3/4} $$
are also correct.

Conditional label symmetry

Randomizing initial labels is legitimate because agent identities do not affect the rules and random tapes are independent and identically distributed.

After conditioning on excluded identities and labels, all remaining labels belong to large groups, and all remaining agents have first-yield variables at most $T_N$. Permuting those labels preserves exclusion and $F_N$.

The persistent excluded requesters ensure that these permutations do not change:

Thus the mechanical winning classes are fixed under the admissible label permutations. The resulting count is hypergeometric with the stated conditional mean. The variance bound by $N$ is sufficient.

Error bound

The comparison with product counts correctly yields
$$ \left|X_{\lambda r}-\frac{n_\lambda k_r}{N}\right| \le |X^E_{\lambda r}-M_{\lambda r}|+3D. $$

The thresholds $\rho N/2$ and $\rho N/6$ produce the constants in the displayed Chebyshev and Markov bounds. For fixed input parameters, these bounds tend to zero.

Assessment: correct. In particular, the proof does not incorrectly assume independence between final assignments and labels; it establishes the required conditional symmetry.

6. Complete-state fluid-limit construction

At each fixed horizon, the invariant bounds the number of possible starts independently of population size. Labels consisting of type and previous winning-class word determine the learner trajectory and current start.

Fresh randomness permits conditional application of the uniform decorrelation bound. Induction therefore gives
$$ P_{N,H}(t,r_1,\ldots,r_H) \xrightarrow{\mathbb P} \mu_t\prod_{i=1}^Hq_{r_i}. $$

The reconstruction accounts for every part of the specified learner encoding:

At fixed horizon, used starting-copy indices remain bounded, while final-copy indices diverge. Their asserted limiting marks match the specified coordinate topology. Table structures stabilize once capacities are sufficiently large.

Finite mixtures with convergent weights and convergent atoms therefore converge weakly in probability. The explicit construction using an infinite class sequence supplies consistent trajectory laws.

Assessment: correct. The restricted theorem proves deterministic, approximation-independent complete-state fluid-limit existence.

7. Computation and example

The exact finite-horizon mixture algorithm follows from the reconstruction. Its exponential dependence on the supplied horizon is openly stated.

The history-length bound
$$ h=\min\{\ell,H+1\} $$
is correct. The claimed bit sizes for histories, means, losses, and product weights support the conservative arithmetic bound.

The example satisfies the input restrictions. Its starting-copy index has the stated binomial distribution and increases infinitely often almost surely, while its starting class remains fixed.

Assessment: correct. The example demonstrates infinite appointment-copy motion; it is not a counterexample to either property asked about in USER_TASK.

8. Remaining issue and actionable feedback

Major scope issue — universal fluid-limit existence remains unresolved.

Sections 4–6 require common appointment order and utilities bounded by $\eta$. They establish neither existence for every admissible input nor an admissible example where existence fails.

This limitation is explicitly acknowledged and does not invalidate the restricted theorem. Nevertheless, it prevents the output from resolving the full task.

To complete the task, the prover must supply either a verified argument covering all admissible inputs or a verified admissible counterexample to deterministic, approximation-independent fluid-limit existence. Additional exposition alone cannot close this gap.

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