← back to the atlas

Online Fair Division for Personalized 2-Value Instances (d4-conf-sagt-2025-0011)

Answer: Existence is polynomial-time solvable: every valid input admits a deterministic policy with \(\rho=1\). The maximum achievable value is always \(1\); decision and value computation take \(O(L)\) time including input reading.

The anchor (named result in the paper)

Theorem 5.4 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateFor any personalized 2-value instance augmented with foresight of length n −1, Algorithm 3 builds an allocation that is temporal-EF2, while it is EF1 (and, thus, 1/n-MMS) for every time step t = kn, k ∈ Z≥0. Moreover, if at any step t0 the allocation fails to be 1/2-EF1, then it remains 1/2-EF1 at the end of every time step t ≥⌈t0/n⌉n.

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

The continuous mirror question, as graded

Given finite types \(\Theta\) with rational masses \(\mu_\theta\), personalized \(2\)-value data, and complete valuation patterns on a finite-horizon scenario tree, goods arrive sequentially in per-capita blocks and a policy sees only revealed history plus the next block. Assign each individual an integral bundle through mass transports \(y_{\theta,B,q}\) from type/bundle states, irrevocably and nonanticipatorily, while enforcing pairwise \(\rho\)-\(\mathrm{EF2}\) at every prefix and \(\rho\)-\(\mathrm{EF1}\) at block boundaries. Compute the maximum achievable \(\rho\), in particular deciding whether \(\rho=1\) is achievable for every allowed arrival path.

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

A society is nonatomic and given by its support: the list of the \(\tau\) types with positive binary-rational masses \(\mu_\theta\), summing to \(1\); \(\tau\) counts supported types, not possible types. Each type has additive valuations with binary-rational \(\alpha_\theta\geq\beta_\theta\geq0\), \(\alpha_\theta>0\), and every good's value belongs to \(\{\alpha_\theta,\beta_\theta\}\).
The input explicitly lists a finite scenario tree with \(S\) nodes and horizon \(H\), including all valuation patterns. Each node specifies an ordered block of distinct good labels \(q\), with positive binary-rational supplies \(s_q\) summing to \(1\); labels do not recur along a path. Let \(m\) count labels in the input and \(L\) be its total bit length.
A supply is a mass of indivisible copies: an individual may receive at most one copy of each label, and holds an integral bundle \(B\) of labels. Initially \(x_{\theta,\varnothing}=\mu_\theta\). On arrival of \(q\), choose real transports \(0\leq y_{\theta,B,q}\leq x_{\theta,B}\) with \(\sum_{\theta,B}y_{\theta,B,q}=s_q\), moving that mass from \((\theta,B)\) to \((\theta,B\cup\{q\})\); goods cannot be discarded or reassigned.
The current block's complete ordered supplies and valuations are revealed before its first arrival. A deterministic policy may use the known scenario set, revealed history, current allocation, and current block, but must make identical decisions on identical observations; future branch choices are hidden.
At every prefix after a supply arrival, every ordered pair of positive-mass states \((\theta,B),(\theta',C)\) must satisfy \(v_\theta(B)\geq\rho\min_{D\subseteq C,\,|D|\leq2}v_\theta(C\setminus D)\). At each block boundary require the same inequality with \(|D|\leq1\). These requirements hold on every root-to-leaf path; no restriction limits the number of different goods an individual receives in a block.

For an input binary-rational \(\rho\in[0,1]\), is existence of such a policy in \(\mathrm P\), or is it NP-hard, including the case \(\rho=1\)? What is the complexity of computing the maximum achievable \(\rho\)? State running times in \(m,\tau,L,S,H\).

For finite societies of \(n\) agents, a polynomial-time algorithm with foresight of \(n-1\) goods guarantees EF2 after every arrival and EF1 every \(n\) arrivals. [Source](https://arxiv.org/html/2505.22174v1)
No result settling this precise mass-transport problem was located.

Modeling choices made when packaging the task

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

Result

Every valid input admits a deterministic policy with \(\rho=1\). Consequently, the existence problem is in \(\mathrm P\), and the maximum achievable value is always \(\rho_{\max}=1\).

The essential point is that each block has total supply exactly \(1\). After a rational expansion, it becomes a batch containing exactly as many copies as virtual agents. The finite-agent algorithm supplied in the question allocates such a batch by a perfect matching.

1. The finite-agent result used

We use the following properties of Priority-Matching, Algorithm 3 in the cited paper. For \(N\) agents with personalized two-value additive valuations, starting from empty bundles, it:

The first and third properties follow from Algorithm 3, lines 6–13; the fairness guarantees are Theorem 5.4. Fix deterministic tie-breaking for every topological sort and maximum-weight matching. The hypotheses permit both \(\beta_i=0\) and \(\alpha_i=\beta_i>0\). [Algorithm 3 and Theorem 5.4](https://arxiv.org/html/2505.22174v1#S5.SS2)

The third property matters: although the theorem is phrased using rolling foresight, its algorithm only consults the preview when a batch begins. Thus revealing the whole current batch suffices.

2. Exact rational expansion

Choose a positive integer \(N\) divisible by the denominators of every type mass and every supply occurring anywhere in the scenario tree. For example, their product suffices. Consequently,

\(N\mu_\theta\in\mathbb Z_{>0}\quad\text{and}\quad Ns_q\in\mathbb Z_{>0}.\)

For every supported type \(\theta\), create \(N\mu_\theta\) virtual agents of that type. Since the type masses sum to \(1\), there are exactly \(N\) virtual agents. Each represents a population cell of mass \(1/N\).

When a block is revealed, replace its arrival of label \(q\) by \(Ns_q\) distinct virtual copies, each having the value of \(q\) for every type. Order these copies consecutively, respecting the block’s label order. Because the block’s supplies sum to \(1\), the expanded block contains exactly

\(\sum_{q\text{ in the block}}Ns_q=N\)

virtual goods.

Run Priority-Matching on these virtual agents, treating each expanded block as one complete batch. All its valuation hypotheses hold: a virtual agent of type \(\theta\) values every copy in \(\{\alpha_\theta,\beta_\theta\}\).

This is an exact finite construction, with no limiting or approximation argument.

3. The construction respects integral bundles of labels

Priority-Matching gives each virtual agent exactly one copy per expanded block.

Within a block, a virtual agent therefore cannot receive two copies of the same label. Across blocks on a path, the input promises that labels never recur. Hence no virtual agent ever receives two copies with the same label.

Let \(A_i\) denote virtual agent \(i\)’s bundle of copies, and let \(B_i\) be its bundle after replacing each copy by its label. The replacement map is injective on \(A_i\). In particular, if \(i\) has type \(\theta\), then

\(v_i(A_i)=v_\theta(B_i).\)

More generally, deleting any subset \(E\subseteq A_i\) corresponds to deleting a subset \(D\subseteq B_i\) with \(|D|=|E|\), and preserves the resulting valuation.

Give the population cell represented by \(i\) the integral label bundle \(B_i\). Choosing one label per individual per block is a property of this construction; it imposes no additional restriction on the problem’s feasible policies.

4. The virtual allocation defines legal transports

Immediately before an actual arrival \(q\), define

\(x_{\theta,B}=\frac{1}{N}\bigl|\{i:\operatorname{type}(i)=\theta,\ B_i=B\}\bigr|.\)

The matching for the current block has already been selected. Let \(R_q\) be the virtual agents matched to the copies of \(q\), and set

\(y_{\theta,B,q}=\frac{1}{N}\bigl|\{i\in R_q:\operatorname{type}(i)=\theta,\ B_i=B\}\bigr|.\)

These transports satisfy

\(0\leq y_{\theta,B,q}\leq x_{\theta,B}\)

because their counted agents form a subset of the agents in the corresponding state. Moreover,

\(\sum_{\theta,B}y_{\theta,B,q}=\frac{|R_q|}{N}=\frac{Ns_q}{N}=s_q.\)

Every recipient lacks label \(q\), by the preceding section. Moving these cells from \(B\) to \(B\cup\{q\}\) therefore performs exactly the permitted transport.

The resulting aggregate allocation is precisely the virtual allocation after all copies of \(q\) have arrived. No supply is discarded, and no previous allocation is reassigned.

5. Fairness survives aggregation

Consider any actual prefix immediately after a supply arrival, and any two positive-mass states \((\theta,B)\) and \((\theta',C)\). Positivity ensures that there are virtual representatives \(i,j\) with these respective types and bundles.

At the corresponding virtual prefix, EF2 gives a subset \(E\subseteq A_j\), with \(|E|\leq2\), such that

\(v_i(A_i)\geq v_i(A_j\setminus E).\)

Let \(D\subseteq C\) be the labels corresponding to \(E\). The injectivity established above gives \(|D|=|E|\), and the valuation identity yields

\(v_\theta(B)\geq v_\theta(C\setminus D)\geq\min_{\substack{D'\subseteq C\\|D'|\leq2}}v_\theta(C\setminus D').\)

Thus the actual allocation satisfies the required inequality with \(\rho=1\).

At a block boundary, the virtual prefix is a complete-batch boundary. Applying EF1 instead gives the identical argument with \(|D|\leq1\). If both states coincide, the inequality also follows directly from nonnegative valuations.

This proves both fairness requirements on every path.

6. Hidden branches and identical observations

Assign fixed identifiers to virtual agents initially, and use fixed identifiers for the copies generated from each revealed block. Fix all algorithmic tie-breaking.

At the beginning of a block, compute its matching from the virtual allocation reconstructed from the revealed history and the newly revealed block. Subsequently execute the corresponding transports as its labels arrive.

Inductively, identical revealed histories produce identical virtual allocations: they start from the same virtual population, and each next matching is a deterministic function of the previous virtual allocation and the revealed block. The resulting transports are therefore identical on identical observations.

The construction never uses the realized identity of a hidden branch. Its choice of the common denominator uses the known scenario set, which the problem explicitly allows.

For any particular root-to-leaf path, its execution is exactly Priority-Matching on that path’s expanded sequence. The finite-agent guarantee consequently applies on every path, proving the existence of one admissible deterministic policy for the entire tree.

7. Complexity

For every promised valid input and every permitted \(\rho\in[0,1]\), the policy above works: nonnegative residual valuations make the inequalities for \(\rho=1\) imply those for smaller \(\rho\).

Therefore:

Both computations take \(O(1)\) time once the promised input is available, or \(O(L)\) including reading it. These bounds have no further dependence on \(m,\tau,S,H\).

For completeness, explicitly constructing a policy by the expansion has a different bound. The product-denominator choice satisfies \(\log_2N=O(L)\), so \(N=2^{O(L)}\). Each node requires one matching on \(N\) virtual agents and \(N\) virtual goods. Exact matching weights have polynomial bit length in \(N\). Thus direct simulation throughout the explicit tree takes

\(S\cdot\operatorname{poly}(N,m,\tau,H,L)=2^{O(L)}\operatorname{poly}(m,\tau,S,H,L)\)

bit operations.

This exponential construction bound does not affect the requested decision and optimum-value computations, which are polynomial-time.

⟨structured verdict parsed — rendered above⟩

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

Verification report

Result: proved. The output resolves the promised decision problem and the computation of the optimum value. The rational expansion is exact, the cited algorithm has the required properties, and the resulting transports satisfy both fairness requirements and the policy’s information restrictions. No major or minor issues were found.

1. Cited finite-agent result

The citation supports the properties used in Section 1:

The algorithm’s required topological sorting is justified by the boundary acyclicity invariant in the theorem’s proof. Its matching choices require maximum weight, without an additional tie-breaking hypothesis. Thus fixed deterministic tie-breaking is compatible with the guarantee. These points are verified in [Definition 2.1, Algorithm 3, and Theorem 5.4](https://arxiv.org/html/2505.22174v1#S5.SS2).

The distinction between rolling foresight and block revelation is handled correctly: the algorithm consults future valuations only when selecting the round’s matching. Every expanded block provides exactly that information.

Finding: The theorem is applied with satisfied hypotheses.

2. Rational expansion

The common denominator is taken over all supported type masses and all supplies throughout the scenario tree. Consequently, the same virtual population works on every branch.

The arithmetic is correct:

\[ \sum_\theta N\mu_\theta=N, \qquad \sum_{q\text{ in a block}}Ns_q=N. \]

All multiplicities are positive integers. Every expanded block is therefore a complete round, including the final block of each path; no incomplete-round case is needed.

Each copy retains its label’s valuation for every type, so the expansion preserves personalized two-value valuations. The virtual population represents finitely many cells of equal mass in the nonatomic society. This uses only subdivision of population mass, consistent with the specified transport model.

Finding: The expansion is exact and introduces no approximation or limiting argument.

3. Integral bundles and copy restrictions

The one-good-per-agent-per-round property prevents any virtual agent from receiving two copies of a label within a block. The prohibition on label recurrence along a path prevents duplicates across blocks.

Thus the copy-to-label map is injective on every recipient bundle, at every relevant prefix. This justifies both:

The valuation preservation also holds when one agent evaluates another agent’s bundle: copies have the original label’s value for every type.

Choosing one label per individual per block is a permissible construction. The task allows policies with that property even though it does not require them.

Finding: The virtual allocation produces legal integral label bundles.

4. Transport feasibility

For each actual arrival, Section 4 counts recipients within their states immediately before that arrival. Therefore its subset argument establishes

\[ 0\leq y_{\theta,B,q}\leq x_{\theta,B}. \]

The matching contains exactly \(Ns_q\) recipients for label \(q\), giving

\[ \sum_{\theta,B}y_{\theta,B,q}=s_q. \]

Every counted recipient lacks \(q\). The resulting movement therefore changes its bundle from \(B\) to \(B\cup\{q\}\), as required.

Sequentially processing the virtual copies and performing the corresponding actual transport have the same resulting aggregate allocation. Other labels do not arrive between these copies, and no recipient receives the label twice. Consequently, aggregation creates no discrepancy in the before-arrival counts.

No supply is discarded and no previous good is moved.

Finding: Every proposed transport satisfies the model’s constraints.

5. Fairness after aggregation

Every positive-mass state contains at least one virtual representative because its mass is an integer multiple of \(1/N\). The finite-agent guarantee therefore applies to representatives of every ordered pair of supported states.

At an actual arrival endpoint, all virtual copies of that label have been allocated. This endpoint is a virtual arrival prefix, so EF2 supplies a deletion witness of size at most two.

Injectivity translates that witness into a label subset \(D\subseteq C\) of the same size. The displayed comparison is in the correct direction:

\[ v_\theta(B)\geq v_\theta(C\setminus D) \geq \min_{\substack{D'\subseteq C\\|D'|\leq2}} v_\theta(C\setminus D'). \]

At a block boundary, the virtual time is a multiple of \(N\), so EF1 gives the required version with at most one deletion.

Empty bundles are covered by the allowed empty deletion subset. Coincident states satisfy the inequality directly by nonnegativity, as the output observes.

Finding: Both fairness requirements hold for every required ordered pair and prefix.

6. Hidden branches and deterministic observations

The policy reconstructs virtual allocations from revealed history, using fixed identifiers and deterministic tie-breaking. It does not require the aggregate allocation alone to determine the virtual state: the task expressly permits use of revealed history.

Identical revealed histories and current blocks therefore produce identical virtual allocations, matchings, and transports. Decisions do not depend on an unrevealed successor node.

The common denominator depends on the known scenario set, which is permitted. Each realized path executes the same finite-agent algorithm on that path’s expanded sequence. Together with observation consistency, this establishes one admissible policy for the entire tree.

Finding: The construction satisfies the information and determinism requirements.

7. Complexity and optimum

Nonnegative residual values justify monotonicity in \(\rho\): feasibility at \(\rho=1\) implies feasibility throughout \(\rho\in[0,1]\). Since the optimization domain has upper endpoint \(1\), the demonstrated feasible value establishes \(\rho_{\max}=1\).

For promised valid inputs, returning YES and returning \(1\) require constant computation; \(O(L)\) including reading the input is a valid bound. The potentially exponential policy representation does not invalidate these decision and optimum-value algorithms.

The supplementary construction bound is also consistent. The product of explicitly encoded denominators has \(\log_2N=O(L)\). Matching weights have polynomial bit length in \(N\), and direct simulation over the explicit tree consequently fits the stated exponential bound.

Finding: The claimed decision, value-computation, and supplementary construction bounds are justified.

No repair or additional clarification is required.

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