← back to the atlas

Class Fairness in Online Matching (aaai23-25704)

Answer: —

The anchor (named result in the paper)

Theorem 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor deterministic matching of divisible items, EQUAL-FILLING (Algorithm 2) satisfies non-wastefulness, (1 −1/e)-CEF, (1 −1/e)-CPROP, and 1/2-USW.

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

The continuous mirror question, as graded

Given a finite known set \(T\) of complete agent types, each specifying a class and binary likes over a finite item-signature universe, rational masses \(\mu_t\) summing to \(1\), an adversarial online sequence of item signatures and sizes \(w_j\), and target ratios, can one compute a deterministic irrevocable mass-allocation policy \(x_{t,j}\) satisfying type-capacity and item-capacity constraints, non-wastefulness, and the paper's \(\alpha\)-CEF, \(\alpha\)-CPROP, and \(\alpha\)-USW guarantees at every stopping time?

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

A society is given by its support: a list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types. Each type specifies a class \(c(t)\in\{1,\ldots,k\}\) and binary likes \(\ell_t:S\to\{0,1\}\) over a known signature universe of size \(m\); every class has positive mass.
Each unit of agent mass has capacity \(1\). An adversary reveals items \((s_j,w_j)\), with \(s_j\in S\) and positive binary-rational size \(w_j\), sequentially; signatures may repeat, and neither future arrivals nor the stopping time is known.
A deterministic policy irrevocably chooses allocated amounts \(x_{t,j}\geq0\) using only the society and revealed history, with \(\sum_{j\leq r}x_{t,j}\leq\mu_t\), \(\sum_t x_{t,j}\leq w_j\), and \(x_{t,j}=0\) whenever \(\ell_t(s_j)=0\).
Non-wastefulness requires, at every prefix \(r\), that each underallocated item \(j\leq r\) has every liking type saturated: \(\sum_t x_{t,j}<w_j\Rightarrow\sum_{q\leq r}x_{t,q}=\mu_t\) for every \(t\) with \(\ell_t(s_j)=1\).
For a prefix, let \(\mathcal F_r\) be all nonnegative matrices satisfying its type and item capacities, including matrices assigning disliked items. Define \(Y_{h,j}(Z)=\sum_{t:c(t)=h}z_{t,j}\), \(V_i(Z)=\sum_{t:c(t)=i}\sum_{j\leq r}\ell_t(s_j)z_{t,j}\), and \(\operatorname{USW}(Z)=\sum_iV_i(Z)\).
For an item-amount vector \(y\), define \(V_i^*(y)\) as the maximum total allocation to liking types in class \(i\), with type capacities \(\mu_t\) and item capacities \(y_j\). Set \(\operatorname{prop}_i(r)=\max_{Z\in\mathcal F_r}\min_h V_i^*(Y_h(Z))\) and \(\operatorname{OPT}(r)=\max_{Z\in\mathcal F_r}\operatorname{USW}(Z)\).
Given binary-rational targets \((\alpha_E,\alpha_P,\alpha_U)\in(0,1]^3\), the requested guarantees at every prefix are \(V_i(X)\geq\alpha_E V_i^*(Y_h(X))\) for all classes \(i,h\), \(V_i(X)\geq\alpha_P\operatorname{prop}_i(r)\) for every class \(i\), and \(\operatorname{USW}(X)\geq\alpha_U\operatorname{OPT}(r)\).
For a given society, which target triples are simultaneously attainable with non-wastefulness by a deterministic online policy, and which are impossible? Can attainable triples be implemented in polynomial time in \(m,\tau,k,r,L\), where \(L\) is the total binary input length through prefix \(r\), including the targets?
For finite unit-capacity agents and divisible unit-size items, Equal-Filling simultaneously guarantees non-wastefulness and ratios \((1-1/e,1-1/e,1/2)\); the proportionality ratio is tight. A later result bounds non-wasteful deterministic CEF by \(0.677\). [Original result](https://www.cs.toronto.edu/~nisarg/papers/fair-online-matching.pdf), [later bound](https://proceedings.neurips.cc/paper_files/paper/2024/file/20ceffa1fcec0f882868e5b891e3e7fa-Paper-Conference.pdf).
For that finite-agent model, a subsequent algorithm simultaneously guarantees CEF ratio \(1-e^{-\gamma}\) and USW ratio \(1-e^{\gamma-1}/(\gamma+1)\), for \(\gamma\in[0,1]\). [Source](https://arxiv.org/html/2605.23408v1).
No result settling the specified support-encoded mass model with known complete types and all three requested guarantees was identified.

Modeling choices made when packaging the task

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

Partial results: an effective finite-horizon characterization and a sharp two-class frontier

1. Status and conventions

The general society-specific attainable region, and polynomial-time implementation for every attainable triple, remain unresolved.

The results proved here are:

Existence statements allow real allocation amounts, as permitted by the task. Rationality is asserted separately for the implementations proved below. In particular, finite-horizon rational implementations do not imply a rational infinite-horizon implementation.

2. Exact benchmark formulas

Write
$$ T_i=\{t:c(t)=i\},\qquad C_i=\sum_{t\in T_i}\mu_t,\qquad C_{\min}=\min_i C_i. $$

For a signature-capacity vector $y=(y_s)_{s\in S}$, define $F_i(y)$ as the maximum flow in the following network:

Let $F(y)$ denote the corresponding network containing all types.

For a prefix, put
$$ W_s=\sum_{j:s_j=s}w_j. $$

Proposition 1: aggregation and proportionality

For every item-amount vector $y$,
$$ V_i^*(y)=F_i(\bar y), \qquad \bar y_s=\sum_{j:s_j=s}y_j. $$

Moreover,
$$ \operatorname{OPT}(r)=F(W), \qquad \operatorname{prop}_i(r) =\min\{C_{\min},F_i(W/k)\}. $$

Proof.

Aggregating an item-level matching by signature preserves type capacities and matching value.

Conversely, suppose an aggregate matching assigns $a_{t,s}$ to type $t$ from signature $s$. For $\bar y_s>0$, set
$$ z_{t,j}=a_{t,s}\frac{y_j}{\bar y_s} \quad\text{when }s_j=s. $$
This preserves every type total. Also,
$$ \sum_t z_{t,j} =\frac{y_j}{\bar y_s}\sum_t a_{t,s} \leq y_j. $$
Zero-capacity signatures carry no flow. This proves the optimistic-valuation formula. Deleting disliked allocations preserves welfare, so the same argument proves the formula for $\operatorname{OPT}(r)$.

For proportionality, $F_i$ is monotone and concave in its signature capacities. Monotonicity follows from inclusion of feasible sets. For concavity, convex combinations of feasible matchings remain feasible for the corresponding convex combinations of capacity vectors.

Given $Z\in\mathcal F_r$, let $y_h$ be class $h$’s aggregate signature bundle. Then
$$ \sum_h y_h\leq W, \qquad \sum_s y_{h,s}\leq C_h. $$
Consequently,
$$ \min_h F_i(y_h) \leq \frac1k\sum_h F_i(y_h) \leq F_i\!\left(\frac1k\sum_h y_h\right) \leq F_i(W/k). $$
Furthermore, $F_i(y_h)\leq C_h$, so the minimum is at most $C_{\min}$.

For the reverse inequality, put
$$ B=\min\{C_{\min},F_i(W/k)\}. $$
Take a liked matching for class $i$ of value exactly $B$ under signature capacities $W/k$, scaling an optimal matching if necessary. Let $b_s$ be its signature totals. Thus
$$ b_s\leq W_s/k,\qquad \sum_s b_s=B. $$
Assign the same signature bundle $b$ to every class. Within class $h$, distribute it proportionally to the type masses. At item level, for $W_s>0$, use
$$ z_{t,j} =\frac{\mu_t}{C_h}\,b_s\,\frac{w_j}{W_s}, \qquad c(t)=h,\quad s_j=s. $$
Each type receives total $\mu_t B/C_h\leq\mu_t$. Each item receives
$$ \sum_t z_{t,j} =k b_s\frac{w_j}{W_s}\leq w_j. $$
Disliked allocations are permitted in $\mathcal F_r$, so this construction is admissible.

Every class receives aggregate bundle $b$. The selected matching proves $F_i(b)\geq B$, while its total supply proves $F_i(b)\leq B$. Thus every class’s bundle has optimistic value exactly $B$ for class $i$. ∎

Max-flow/min-cut also gives
$$ F_i(y)= \min_{A\subseteq T_i} \left( \sum_{t\in T_i\setminus A}\mu_t+ \sum_{s\in N(A)}y_s \right), $$
where
$$ N(A)=\{s:\ell_t(s)=1\text{ for some }t\in A\}. $$
Indeed, if $A$ is the source-side type set, all its neighboring signatures must be on the source side. The displayed expression is the resulting cut capacity, minimized over $A$.

Thus these valuations are continuous minima of finitely many rational affine functions. Their values can be computed by polynomial-size maximum-flow networks. Clearing rational denominators produces integers with bit lengths polynomial in the total input length, so benchmark evaluation is exact and polynomial-time.

3. A bounded sufficient state

Proposition 2: supply clipping

Set
$$ v_s=\min\{1,W_s\}. $$
Then
$$ F(v)=F(W), \qquad \min\{C_{\min},F_i(v/k)\} =\min\{C_{\min},F_i(W/k)\}. $$

Proof.

Every matching has total value at most $1$, so no signature needs capacity exceeding $1$. This proves the first equality.

For the second, let
$$ B=\min\{C_{\min},F_i(W/k)\}. $$
Choose a matching of value exactly $B$ under capacities $W/k$. Its flow through any individual signature is at most $B$. Since
$$ C_{\min}\leq \frac1k, $$
every signature whose supply is clipped still has capacity
$$ v_s/k=1/k\geq B. $$
Unclipped capacities remain unchanged. The matching therefore remains feasible under $v/k$. Monotonicity proves the opposite inequality. ∎

Define the state
$$ z=(b,q,v), $$
where
$$ b_t=\sum_{j\leq r}x_{t,j}, \qquad q_{h,s}=\sum_{\substack{j\leq r\\s_j=s}}Y_{h,j}(X), \qquad v_s=\min\{1,W_s\}. $$
Write
$$ B_i=\sum_{t\in T_i}b_t. $$
Because the policy allocates only liked items, $B_i=V_i(X)$.

All three guarantees depend only on this state:
$$ B_i\geq\alpha_E F_i(q_h), $$
$$ B_i\geq\alpha_P\min\{C_{\min},F_i(v/k)\}, $$
$$ \sum_i B_i\geq\alpha_U F(v). $$

The state has $\tau+km+m$ real coordinates, independent of the number of arrivals.

Take as its ambient domain the compact rational polytope $D$ defined by
$$ 0\leq b_t\leq\mu_t,\qquad q_{h,s}\geq0,\qquad 0\leq v_s\leq1, $$
$$ \sum_s q_{h,s}=B_h, \qquad \sum_h q_{h,s}\leq v_s. $$
Every actual allocation history produces a state in $D$.

Let $G\subseteq D$ consist of states satisfying the three displayed guarantees. By the min-cut formulas, each guarantee is a finite disjunction of rational linear inequalities. Hence $G$ is a finite union of compact rational polytopes.

Local non-wastefulness

For an arriving item $(s,w)$, an action is a vector $a=(a_t)$ satisfying
$$ 0\leq a_t\leq\mu_t-b_t, \qquad a_t=0\text{ if }\ell_t(s)=0, \qquad \sum_t a_t\leq w. $$
Require additionally
$$ \sum_t a_t=w \quad\text{or}\quad b_t+a_t=\mu_t \text{ for every }t\text{ liking }s. $$

This local condition is equivalent to non-wastefulness for the current item. Enforcing it on arrival also enforces the condition at every later prefix, because saturated types remain saturated.

The successor state is
$$ b'_t=b_t+a_t, $$
$$ q'_{h,s}=q_{h,s}+\sum_{t\in T_h}a_t, \qquad v'_s=\min\{1,v_s+w\}, $$
with other signature coordinates unchanged. Denote this successor by $\Phi(z,s,w,a)$.

Both the action relation and the transition relation are finite unions of rational polyhedral relations.

Items larger than $1$

It suffices to consider sizes in $[0,1]$.

If $w>1$, non-wastefulness forces every liking type to be saturated, since total allocation cannot exceed $1$. For $w=1$, either the allocation is less than $1$ and the same saturation condition applies, or allocation equals $1$, which saturates all types because their total capacity is $1$.

Thus the admissible action sets for $w>1$ and $w=1$ coincide. Their successor states also coincide after supply clipping. A policy for clipped sizes therefore implements a policy for the original sizes. A zero-size item is harmless and may be added to the input alphabet.

4. An effective finite-horizon characterization

Define
$$ K_0=G, $$
and recursively
$$ K_{n+1} = \left\{ z\in G: \text{ for every }s\in S,\ w\in[0,1], \text{ there is an admissible }a \text{ with }\Phi(z,s,w,a)\in K_n \right\}. $$

Here $K_n$ is the set of states from which all requirements can be maintained for the next $n$ arrivals.

Theorem 3

For a fixed rational society and rational target triple:

$$ 0\in\bigcap_{n=0}^{\infty}K_n. $$

No polynomial bound is asserted for computing $K_n$, and no computability assertion is made for the infinite-horizon policy in part 5.

Proof.

Compactness

The sets are nested:
$$ K_{n+1}\subseteq K_n. $$
This follows directly from the zero-size input, whose only action is zero and whose successor is the current state.

Assume $K_n$ is compact. Let $z_j\in K_{n+1}$ converge to $z$. Since $G$ is closed, $z\in G$.

Fix an input $(s,w)$. For each $j$, choose an admissible action $a_j$ with successor in $K_n$. Actions lie in the compact box
$$ \prod_t[0,\mu_t]. $$
A subsequence therefore converges to some $a$.

The admissible-action relation is closed: all its constraints are closed linear constraints or a finite disjunction of such constraints. The transition map is continuous. Therefore $a$ is admissible at $z$, and its successor lies in the closed set $K_n$.

This holds for every input, so $z\in K_{n+1}$. Thus $K_{n+1}$ is closed and bounded, hence compact.

Effective polyhedral description

For fixed targets, all coefficients in the definition of $K_{n+1}$ are rational constants. Its definition is a first-order formula consisting solely of rational linear inequalities, Boolean operations, and quantifiers over real variables.

Such formulas admit effective quantifier elimination. One elementary construction eliminates existentially quantified variables by distributing into conjunctions and applying Fourier–Motzkin elimination, retaining strict inequalities where necessary. Universal quantifiers are handled through negation.

Consequently, $K_{n+1}$ has an effectively computable description as a finite union of sets defined by rational strict and non-strict linear inequalities.

Because $K_{n+1}$ is closed, it can be represented using closed rational polyhedra. To justify this last step, consider a nonempty conjunction $P$ of strict and non-strict inequalities. Its closure is obtained by replacing strict inequalities with their non-strict versions: if $x_0\in P$ and $y$ satisfies the relaxed inequalities, then
$$ (1-\varepsilon)y+\varepsilon x_0\in P \quad\text{for }0<\varepsilon\leq1, $$
and these points approach $y$.

For a finite union, closure commutes with union. Since the union describing $K_{n+1}$ is already closed, replacing its nonempty pieces by their closures preserves it. Intersecting with the bounded domain $D$ gives rational polytopes.

Rational finite-horizon implementation

Suppose $z\in K_n$ is rational and the next input has rational size. The actions whose successors lie in $K_{n-1}$ form a nonempty finite union of rational polytopes.

A nonempty rational polytope contains a rational point: a vertex is obtained by solving a nonsingular system of rational linear equations. Such a point can be found effectively by examining the finitely many polyhedral pieces.

Choose one deterministically. Its successor is rational and lies in $K_{n-1}$. Repeating this construction gives a rational-output policy for the remaining horizon.

Rational arrivals versus real arrivals

Using every real size in $[0,1]$ does not strengthen the finite-horizon requirement.

For a fixed state and signature, the sizes admitting an action into $K_n$ form a closed set. Indeed, if feasible sizes converge, compactness supplies a convergent subsequence of their actions, and closedness supplies a feasible limiting action.

The admissible binary-rational sizes are dense in $[0,1]$, including under a dyadic interpretation. Feasibility for every admissible size therefore implies feasibility for every real size. Induction on the horizon proves that $K_n$ also characterizes the original input alphabet.

Infinite horizon

Put
$$ K_\infty=\bigcap_{n=0}^{\infty}K_n. $$
Fix $z\in K_\infty$ and an input $(s,w)$. Let
$$ A_n= \{a:a\text{ is admissible at }z,\ \Phi(z,s,w,a)\in K_n\}. $$
Each $A_n$ is nonempty because $z\in K_{n+1}$. These sets are compact and nested. Their intersection is therefore nonempty.

Choose deterministically an action in that intersection; for example, choose its lexicographically least element, obtained by successively minimizing the finitely many coordinates over compact sets. Its successor lies in $K_\infty$.

Starting at $0\in K_\infty$ and repeating this rule preserves all requirements forever. Earlier non-wastefulness conditions remain valid by persistent saturation.

Conversely, any infinite-horizon policy works for every finite horizon. The finite-horizon characterization therefore gives $0\in K_n$ for every $n$. ∎

Consequences and limitation

This supplies an exact characterization:
$$ (\alpha_E,\alpha_P,\alpha_U)\text{ is attainable} \quad\Longleftrightarrow\quad 0\in K_n\text{ for every }n. $$

It also gives an algorithm that halts on every impossible triple: compute successive $K_n$ and stop when $0\notin K_n$.

The unresolved issue is detecting attainability after finitely many computations. No stabilization bound is proved. Moreover, although every finite-horizon action set has a rational witness, the compact intersection used for the infinite horizon may contain only irrational actions.

5. A useful welfare bound for every non-wasteful allocation

Proposition 4

At a prefix, let $A$ be the saturated types and let $J$ be the items liked by at least one unsaturated type. Every feasible, liked, non-wasteful allocation $X$ satisfies
$$ \operatorname{OPT}(r) \leq \operatorname{USW}(X) + \sum_{t\in A}\sum_{j\in J}x_{t,j}. $$
In particular,
$$ \operatorname{USW}(X)\geq\frac12\operatorname{OPT}(r). $$

Proof.

Every item in $J$ is fully allocated; otherwise its unsaturated liking type would violate non-wastefulness.

An offline liked allocation obtains at most $\sum_{t\in A}\mu_t$ from saturated types. Its allocations to unsaturated types use only items in $J$, so their value is at most $\sum_{j\in J}w_j$. Hence
$$ \operatorname{OPT}(r) \leq \sum_{t\in A}\mu_t+\sum_{j\in J}w_j. $$

All allocation to unsaturated types occurs on items in $J$. Since these items are fully allocated,
$$ \sum_{j\in J}w_j = \sum_{t\notin A}b_t + \sum_{t\in A}\sum_{j\in J}x_{t,j}. $$
Also, saturation gives $\mu_t=b_t$ for $t\in A$. Substitution proves the refined bound. The additional term is at most $\operatorname{USW}(X)$, proving the factor $1/2$. ∎

6. A sharp frontier for two unequal homogeneous classes

Consider two types in distinct classes, with masses
$$ a,\qquad b=1-a,\qquad 0<a\leq b. $$
The known universe consists of:

Define
$$ R(a)= \begin{cases} \frac23,&0<a\leq\frac13,\\[2mm] \frac{1+a}{2},&\frac13\leq a\leq\frac12. \end{cases} $$

Theorem 5

For this society:

$$ \alpha_U\leq R(a). $$

Thus this determines the complete attainable region on the two faces where either fairness target equals $1$.

6.1. Policy and exact fairness

Allocate each private item up to its liking type’s remaining capacity. For shared items, allocate at equal absolute rates to the unsaturated types. Once one saturates, allocate the remainder to the other until it saturates or the item is exhausted.

The policy is non-wasteful.

If a type is saturated, its value equals its capacity, which bounds all its optimistic valuations. If it is unsaturated at the current prefix, it remained unsaturated during every earlier shared arrival. It therefore received at least the other type’s share of each shared item. The other type’s private items are disliked. This proves exact envy-freeness.

By Proposition 1,
$$ \operatorname{prop}_i(r) = \min\left\{a,\frac{W_{s_0}+W_{s_i}}2\right\}. $$
A saturated type meets this bound. An unsaturated type receives at least half of every shared item and all of every private item it likes. Hence it also meets the bound. The proportionality ratio is therefore $1$.

6.2. Welfare guarantee

If both types are saturated, welfare is optimal. If neither is saturated, every item is fully allocated, so welfare is again optimal.

Suppose exactly one type is saturated. Let its capacity be $c$, the other capacity be $d=1-c$, and the other type’s load be $u<d$. Let $A$ be the shared allocation to the saturated type.

Because the other type remained unsaturated, it received at least as much shared allocation. Thus
$$ A\leq u,\qquad A\leq c. $$
Proposition 4 gives
$$ \operatorname{OPT}(r) \leq \min\{1,c+u+\min(c,u)\}, $$
while the policy’s welfare is $c+u$.

First suppose the larger type is saturated, so $c=b\geq1/2$. Since $u<d=a\leq c$,
$$ \operatorname{OPT}(r)\leq\min\{1,c+2u\}. $$
Before $u=d/2$, the ratio
$$ \frac{c+u}{c+2u} $$
decreases; its derivative is $-c/(c+2u)^2$. After $u=d/2$, the denominator bound is $1$ and $c+u$ increases. Consequently,
$$ \frac{\operatorname{USW}(X)}{\operatorname{OPT}(r)} \geq c+\frac d2 =\frac{1+b}{2} \geq R(a). $$

Now suppose the smaller type is saturated, so $c=a$.

If $a\leq1/3$ and $u\leq a$, then
$$ \frac{\operatorname{USW}(X)}{\operatorname{OPT}(r)} \geq\frac{a+u}{a+2u}\geq\frac23, $$
where the last inequality is equivalent to $u\leq a$.

If $a\leq1/3$ and $u\geq a$, then
$$ \frac{\operatorname{USW}(X)}{\operatorname{OPT}(r)} \geq\frac{a+u}{2a+u}\geq\frac23, $$
where the last inequality is equivalent to $u\geq a$.

Finally, suppose $a\geq1/3$. For $u\leq a$, the bound
$$ \operatorname{OPT}(r)\leq\min\{1,a+2u\} $$
gives its minimum ratio at $u=b/2$, which belongs to $[0,a]$. That minimum is
$$ a+\frac b2=\frac{1+a}{2}. $$
For $u\geq a$,
$$ \operatorname{USW}(X)\geq2a \geq\frac{1+a}{2}, $$
and $\operatorname{OPT}(r)\leq1$. This completes the welfare proof.

6.3. Sharpness when either fairness target equals $1$

Reveal a shared item of size
$$ z=\min\{2a,b\}. $$
Non-wastefulness forces full allocation. Write its allocation as $x$ to the smaller type and $y=z-x$ to the larger.

If $\alpha_P=1$, both proportionality benchmarks are $z/2$, because $z\leq2a$. Hence $x=y=z/2$.

If $\alpha_E=1$, the initial envy constraints give
$$ x\geq\min\{a,y\}, \qquad y\geq\min\{b,x\}=x. $$
If $x<a$, the first inequality forces $y\leq x$, so $x=y$. If $x=a$, the second inequality and $z\leq2a$ again force $x=y=a$. Thus exact envy-freeness also forces $x=y=z/2$.

Next reveal a private item of size $a$ for the smaller type. Online welfare is at most
$$ a+\frac z2. $$
Offline, assign the shared item entirely to the larger type and the private item to the smaller type. This is feasible because $z\leq b$, and achieves $a+z$. Therefore
$$ \alpha_U\leq\frac{a+z/2}{a+z} = \begin{cases} \frac23,&a\leq\frac13,\\[2mm] \frac{1+a}{2},&a\geq\frac13. \end{cases} $$
This matches the proved policy guarantee.

6.4. Polynomial-time implementation

Each item requires only comparisons, additions, subtractions, and division of its size by $2$. A shared item has at most two allocation phases.

Through prefix $r$, a common denominator can be chosen as twice the product of the denominators of the masses and arriving sizes. Its bit length is polynomial in the total binary input length. Allocations and loads are bounded, so their numerator lengths are polynomial as well.

Thus the policy is exact, rational, and polynomial-time.

7. Additional necessary bounds for this society

The same two-class society yields obstructions when both fairness targets are below $1$.

Fairness-dependent obstruction

Let $z=\min\{2a,b\}$ and define
$$ D= \max\left\{ \frac{\alpha_P z}{2}, \min\left\{\alpha_E a,\frac{\alpha_E z}{1+\alpha_E}\right\} \right\}. $$
Every attainable triple satisfies
$$ \alpha_U\leq1-\frac{D}{a+z}. $$

Proof.

After the first shared item of size $z$, let the smaller type receive $x$. Proportionality requires
$$ x\geq\alpha_P z/2. $$
Its envy constraint requires
$$ x\geq\alpha_E\min\{a,z-x\}. $$
This inequality is equivalent to the disjunction
$$ x\geq\alpha_E a \quad\text{or}\quad (1+\alpha_E)x\geq\alpha_E z, $$
and hence implies $x\geq D$.

After a private item of size $a$ for that type, welfare is at most $a+z-x$, while optimum is $a+z$. The claimed bound follows. ∎

In particular, when $a\leq1/3$,
$$ \alpha_U\leq1-\frac{\max\{\alpha_E,\alpha_P\}}3. $$

An obstruction independent of fairness

Every attainable triple also satisfies
$$ \alpha_U\leq\frac{1+a}{1+2a}. $$

Proof.

Reveal a shared item of size $a$, and let the smaller type receive $x$.

A subsequent private item of size $a$ for the smaller type gives an online-to-offline ratio at most
$$ 1-\frac{x}{2a}. $$
A subsequent private item of size $b$ for the larger type gives a ratio at most
$$ b+x. $$
Both continuations are admissible. The maximum over $x$ of the smaller of these two expressions occurs at their intersection:
$$ x=\frac{2a^2}{1+2a}. $$
The resulting ratio is $(1+a)/(1+2a)$. ∎

These bounds are necessary. Sufficiency outside the faces characterized in Theorem 5 is not established.

8. Remaining open points

The finite-horizon hierarchy gives exact tests and an infinite intersection characterization, but not a terminating general attainability algorithm. Its infinite-horizon selector may be noncomputable or irrational.

The unequal-mass example also leaves a concrete smaller problem: determine its full frontier when both fairness targets are strictly below $1$.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Assessment: partial, with sound proved content. The benchmark formulas, finite-horizon characterization, welfare bound, and stated two-class frontier are correct. I found no false central step or substantive gap in those arguments. The output expressly leaves the general implementation question unresolved, so it does not fully resolve USER_TASK.

The distinction matters: the infinite intersection is an exact mathematical characterization of attainability, but the construction does not establish a terminating membership test or a polynomial-time implementation for every attainable triple.

1. Benchmarks

Signature aggregation

The identity
$$ V_i^*(y)=F_i(\bar y) $$
is correct for nonnegative item capacities.

Aggregating a feasible matching preserves capacities. Conversely, the displayed proportional distribution across items of the same signature preserves each type’s total and respects each item’s capacity. Signatures with zero aggregate capacity necessarily carry zero matching flow, so the omitted division in that case causes no problem.

The formula
$$ \operatorname{OPT}(r)=F(W) $$
also follows correctly. Removing disliked allocations preserves welfare and cannot violate any capacity constraint.

Proportionality

Both directions of
$$ \operatorname{prop}_i(r)=\min\{C_{\min},F_i(W/k)\} $$
are justified.

For the upper bound:

For the lower bound, the construction respects both type and item capacities:
$$ \sum_j z_{t,j}=\frac{\mu_t B}{C_h}\leq\mu_t, \qquad \sum_t z_{t,j}=k b_s\frac{w_j}{W_s}\leq w_j. $$
Its use of disliked allocations is explicitly permitted by $\mathcal F_r$. Every class receives the same signature bundle, whose optimistic value is exactly $B$.

Min-cut formula and computational claim

The displayed min-cut formula is correct. A finite cut with source-side type set $A$ must place every signature in $N(A)$ on the source side. Including further signatures cannot reduce the cut capacity because capacities are nonnegative.

The networks have polynomial size in the support and signature universe. Clearing rational denominators incurs only polynomial bit length in the binary input length. Thus the exact polynomial-time benchmark claim is justified.

2. Supply clipping and sufficient state

Supply clipping

The welfare equality $F(v)=F(W)$ is correct because every feasible matching has total value at most $1$.

The proportionality argument also works. Its critical inequality,
$$ C_{\min}\leq\frac1k, $$
follows from the positive class masses summing to $1$. A matching of value $B\leq C_{\min}$ uses at most $B$ at any individual signature, so replacing a clipped signature’s capacity by $1/k$ preserves that matching.

State sufficiency

The state coordinates retain everything needed for the displayed prefix guarantees:

The domain $D$ is compact. In particular, the equality
$$ \sum_s q_{h,s}=B_h $$
and the type-capacity bounds also bound every $q_{h,s}$.

Although $D$ may contain states that do not arise from an actual liked allocation history, this does not invalidate the construction. The transition rules preserve actual histories starting from zero, and future requirements depend only on the recorded quantities.

The finite-union description of $G$ is correct: an inequality bounding a finite minimum from above is a finite disjunction of the corresponding affine inequalities.

Non-wastefulness and transitions

The local condition is exactly the required condition for the newly arriving item. Once an underallocated item’s liking types are saturated, they remain saturated. Consequently, enforcing the condition on arrival also enforces it at all later prefixes.

The transition correctly updates clipped supply even when supply has already reached $1$.

Large and zero sizes

The reduction of sizes larger than $1$ is valid. For both $w>1$ and $w=1$, admissibility forces all liking types to be saturated after the action. In the full-allocation case at $w=1$, total allocated mass equals total society capacity, so all types are saturated.

A zero-size arrival has only the zero action and changes no state. Adding it is harmless.

3. Finite-horizon characterization

Compactness and nesting

The zero-size arrival proves
$$ K_{n+1}\subseteq K_n. $$

The compactness proof correctly handles the quantifiers. After fixing an input, a convergent subsequence of its witness actions supplies a limiting witness. The subsequence may depend on that input; the conclusion requires only a separate witness for each input.

The admissible-action relation is closed, the transition is continuous, and $K_n$ is closed. These are exactly the hypotheses needed for the limiting argument.

Effective polyhedral descriptions

The quantifier-elimination argument applies because signatures range over a finite set and all remaining expressions are rational linear relations after expanding the finitely many branches.

The step replacing strict inequalities by non-strict inequalities is justified for each nonempty conjunction by the displayed convex-combination argument. Empty conjunction pieces must be discarded, as the output explicitly specifies. Closure commutes with a finite union, so closedness of $K_{n+1}$ makes the replacement legitimate.

Intersecting the resulting polyhedra with $D$ yields bounded rational polyhedra, hence rational polytopes.

Rational finite-horizon policies

For a rational state and rational arrival, the successful action set is a nonempty finite union of bounded rational polyhedra. A nonempty rational polytope has a rational vertex, including when it lies in a lower-dimensional affine subspace.

Choosing such a point effectively and repeating the procedure gives the claimed rational finite-horizon implementation. No polynomial running-time or output-length bound follows from this construction, and none is asserted.

Rational versus real arrivals

The density argument is sound. For a fixed state, the feasible-size set is closed because witness actions lie in a fixed compact box. Feasibility on the dense admissible rational alphabet therefore implies feasibility for all real sizes in the interval.

Applied inductively, this establishes the claimed equivalence of the finite-horizon games. It also covers a dyadic interpretation of binary-rational arrivals.

Infinite horizon

For each state in $K_\infty$ and each input, the sets $A_n$ are nonempty, compact, and nested. Their intersection is therefore nonempty.

Successive coordinate minimization over this compact intersection defines a unique lexicographically least action. Its successor remains in $K_\infty$, yielding a deterministic state-based policy.

The converse follows from the finite-horizon characterization: a policy that succeeds indefinitely succeeds for every finite horizon.

Thus
$$ 0\in\bigcap_{n=0}^{\infty}K_n $$
is genuinely equivalent to attainability. Computing successive finite-horizon tests also genuinely semidecides impossibility.

The proof does not establish termination on attainable inputs, computability of the infinite-horizon selector, rational infinite-horizon outputs, or polynomial-time implementation. The output correctly acknowledges these limitations.

4. General welfare bound

Proposition 4 is correct.

Every item in $J$ is fully allocated by non-wastefulness. An offline liked allocation can obtain at most the saturated types’ total capacity from those types, and at most the total supply of $J$ from unsaturated types.

Every actual allocation to an unsaturated type is on an item in $J$, so the displayed decomposition of that supply is exact. Substituting the saturated types’ loads gives the refined bound.

The additional term is a subset of the actual liked allocation, hence is at most $\operatorname{USW}(X)$. This proves the factor $1/2$, including prefixes with zero optimum.

5. Two-class frontier

Theorem 5 concerns the explicitly specified society with two types and the three listed signatures. It does not establish a frontier for arbitrary heterogeneous two-class societies.

Exact fairness

The policy is non-wasteful.

An unsaturated type has remained unsaturated throughout the history. On every shared arrival, it receives at least the other type’s share under equal absolute filling. The other type’s private allocation contributes nothing to its optimistic valuation. This proves exact envy-freeness.

The proportionality formula
$$ \operatorname{prop}_i(r) = \min\left\{a,\frac{W_{s_0}+W_{s_i}}2\right\} $$
is correct for both classes: the outer bound by $a$ absorbs the larger class’s own capacity bound.

An unsaturated type receives at least half the entire size of every shared item and all of every private item it likes. Such items cannot be underallocated while that type remains unsaturated. The proportionality argument is therefore valid.

Welfare calculation

When exactly one type is saturated, Proposition 4’s extra term is precisely its shared allocation $A$. The bounds
$$ A\leq u,\qquad A\leq c $$
are justified by the policy and capacity constraints.

The resulting bound
$$ \operatorname{OPT}(r)\leq\min\{1,c+u+\min(c,u)\} $$
is correct.

The subsequent minimizations check out:

The claimed welfare guarantee follows.

Sharpness on the exact-fairness faces

The first shared item is fully allocated because its size is below total capacity.

Exact proportionality forces equal shares. The exact envy constraints also force equal shares, including the boundary case $x=a$.

The second private item produces online welfare at most $a+z/2$. The specified offline allocation is feasible because $z\leq b$ and attains all arriving supply, namely $a+z$. The resulting ratio has exactly the stated two branches.

This establishes the claimed necessary and sufficient condition on either exact-fairness face.

Implementation

The policy uses a bounded number of rational arithmetic operations per item. Its allocations involve input sizes halved, remaining capacities, and differences of these quantities.

The stated common denominator suffices; repeated shared arrivals do not require repeated halving of previously accumulated loads. Its bit length is polynomial in the input length. The polynomial-time implementation claim for this particular society is justified.

6. Additional necessary bounds

Fairness-dependent obstruction

The equivalence
$$ x\geq\alpha_E\min\{a,z-x\} $$
to the stated disjunction is valid because multiplication by the positive target preserves the minimum.

Combining it with the proportionality constraint gives exactly the displayed lower bound $D$. The continuation and welfare calculation then prove the obstruction.

For $a\leq1/3$, substituting $z=2a$ gives
$$ D=a\max\{\alpha_E,\alpha_P\}, $$
so the stated specialization is correct.

Fairness-independent obstruction

Both continuations have the stated offline optima and online upper bounds. Their ratio bounds are respectively decreasing and increasing in $x$.

The intersection
$$ x=\frac{2a^2}{1+2a} $$
lies in the feasible interval $[0,a]$, and its common value is
$$ \frac{1+a}{1+2a}. $$
Thus the obstruction is valid. The output correctly does not claim sufficiency.

7. Outstanding issue and actionable feedback

Major scope issue — general implementation remains unresolved. The output does not determine whether every attainable target triple for an arbitrary support-encoded society admits a polynomial-time implementation. It also supplies no terminating general membership procedure beyond its infinite-intersection characterization.

This is an acknowledged unresolved part of the assignment, rather than a flaw in the proved partial results. No expositional clarification alone resolves it. A subsequent write-up must supply a result answering the implementation question, with the claimed computational bounds or a justified obstruction. Any claim of a terminating general decision procedure would additionally require justification beyond the current finite-horizon hierarchy.

No repairs are required to the mathematical arguments audited above.

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