Answer: The \(1\)-additive guarantee always holds; choices are polynomial-time computable and independent of admissible \(N\). Writing \(u_* = \min_s U_s^T\), the deficit is \(D_N = \max\{0,T(m-1)/N-u_*\}\), hence \(D_N\to0\).
Theorem 8 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximate$LMin_{on}$ guarantees a $1$-additive approximation of $Prop$.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite support of complete Borda-ranking schedules with rational masses \(\mu_s\) summing to \(1\), revealed round by round, choose one candidate at each round by lexicographically maximizing the mass-weighted distribution of accumulated per-type utilities. For population scales \(N\) with \(N\mu_s\) integral, determine the computation required and whether the rule gives each type the paper's \(1\)-additive proportionality guarantee with benchmark \(T(m-1)/N\), including the limiting behavior as \(N\to\infty\).
Let \(C\) be a fixed set of \(m\geq2\) candidates and \(T\geq1\) rounds. A society is given by its support: \(\tau\geq1\) complete ranking schedules \(s\), with positive binary rational masses \(\mu_s\) satisfying \(\sum_s\mu_s=1\); \(\tau\) counts supported schedules, not possible schedules. Each schedule specifies a strict ranking in each round, converted to standard Borda utilities \(v_s^t\).
Masses and type identities are known initially; rankings are revealed only in their respective rounds. Choose one common candidate \(o^t\in C\) irrevocably each round, with \(U_s^0=0\) and \(U_s^t=\sum_{r=1}^t v_s^r(o^r)\).
For candidate \(c\) in round \(t\), define \(h_c(k)=\sum_{s:U_s^{t-1}+v_s^t(c)=k}\mu_s\), for integer \(0\leq k\leq t(m-1)\). Prefer \(c\) to \(d\) when \(h_c(k)<h_d(k)\) at the least \(k\) where their histograms differ. Choose a maximal candidate, breaking identical-histogram ties by a fixed candidate order.
An admissible population scale is an integer \(N\geq1\) with \(N\mu_s\in\mathbb Z\) for every supported type. Its per-individual proportional benchmark at round \(t\) is \(t(m-1)/N\), and its final additive deficit is \(D_N=\max_s\max\{0,T(m-1)/N-U_s^T\}\). Let \(L\) be the total binary encoding length of masses and ranking schedules; encode \(N\) in binary.
Does this rule always satisfy \(U_s^t+1\geq t(m-1)/N\) for every supported type, every round, and every admissible \(N\), or can this additive guarantee fail?
Is computing its choices polynomial-time or NP-hard, with running time measured in \(m,\tau,T,L,\log N\)?
For fixed masses and ranking schedules, what are the limiting behavior of its choices and \(D_N\) as admissible \(N\to\infty\)?
For finitely many individuals with Borda valuations, online leximin guarantees a \(1\)-additive approximation to proportionality and is efficiently computable; no mechanism uniformly guarantees an additive constant below \(1\). [Kahana–Hazon](https://arxiv.org/pdf/2305.18024)
The literature search located no result explicitly treating this support-encoded mass-distribution rule and its population-scale limit.
The additive guarantee always holds. The choices are computable in polynomial time from the supported schedules and rational masses. For fixed masses and schedules, the choices are independent of \(N\), and \(D_N\to0\) along admissible scales.
The proof uses the finite-population online leximin theorem stated in the question; the required correspondence is exact.
Write each mass in lowest terms as \(\mu_s=a_s/b_s\), and define \(N_0=\operatorname{lcm}_s b_s\). Since \(\gcd(a_s,b_s)=1\), the condition \(N\mu_s\in\mathbb Z\) is equivalent to \(b_s\mid N\). Thus the admissible scales are exactly the positive multiples of \(N_0\).
Fix an admissible \(N\). Replace each supported type \(s\) by \(n_s=N\mu_s\) individuals with that schedule. Positivity and admissibility imply \(n_s\geq1\), and \(\sum_s n_s=N\).
Suppose the replicated population has followed the same choices through round \(t-1\). Its number of individuals receiving accumulated utility \(k\) after choosing candidate \(c\) is
\(H_c(k)=\sum_{s:U_s^{t-1}+v_s^t(c)=k}n_s=Nh_c(k)\).
We now verify the ordering correspondence. For two different histograms, let \(k_0\) be their least differing utility level. If \(H_c(k_0)<H_d(k_0)\), their sorted individual-utility vectors have identical entries below \(k_0\). After the common entries equal to \(k_0\), the vector for \(d\) still has an entry equal to \(k_0\), while the next entry for \(c\) is larger. Hence the sorted vector for \(c\) is lexicographically larger.
Consequently, comparing mass histograms exactly implements finite-population leximin. Equal histograms give equal sorted vectors, so the specified candidate tie order also agrees.
Starting from zero utilities, induction over rounds proves that the two rules make identical choices.
The finite-population result we use is: with standard Borda utilities, online leximin on \(n\) individuals guarantees, for every individual \(i\) and every prefix \(t\),
\(u_i^t\geq\left\lfloor t(m-1)/n\right\rfloor\).
This stronger integer bound appears in the proof of Theorem 14 of [Kahana–Hazon](https://arxiv.org/pdf/2305.18024). Its online rule maximizes the sorted accumulated-utility vector over the current candidates.
All hypotheses hold for the replicated population: rankings are strict, utilities are standard Borda scores, accumulated utilities start at zero, and each decision uses only rankings revealed so far. Repeated schedules are allowed, and every histogram maximizer is a leximin maximizer. If \(N=1\), the sole supported type instead gives the conclusion directly: its top candidate is chosen every round.
Applying the theorem with \(n=N\), and using the equivalence proved above, gives
\(U_s^t\geq\left\lfloor t(m-1)/N\right\rfloor\)
for every supported type, round, and admissible scale. Because \(\lfloor x\rfloor+1>x\), this implies the requested guarantee, even strictly:
\(U_s^t+1>t(m-1)/N\).
Thus the additive guarantee cannot fail under the stated assumptions.
Replication is a proof device; the algorithm need not construct the individuals.
Let \(Q=\prod_s b_s\) and \(w_s=Q\mu_s=a_s(Q/b_s)\). These are integers, and \(\log Q\leq L\). Because the masses sum to one, \(\sum_s w_s=Q\). Define integer histograms
\(G_c(k)=\sum_{s:U_s^{t-1}+v_s^t(c)=k}w_s=Qh_c(k)\).
Multiplication by the common positive factor \(Q\) preserves every comparison.
At round \(t\), compute a candidate’s histogram by sorting the \(\tau\) pairs \((U_s^{t-1}+v_s^t(c),w_s)\) by utility and combining equal keys. The resulting list has at most \(\tau\) entries. Compare two lists by merging their utility keys, treating missing entries as zero, and stopping at the least differing key. A scan through the candidates maintains the best candidate, respecting the fixed order for equal histograms.
After selecting it, update all \(\tau\) accumulated utilities. This uses only the current round’s rankings.
Over all rounds, sorting and comparison require
\(O\!\left(Tm\tau\log(\tau+1)\right)\)
integer operations, in addition to polynomial-time preprocessing. Histogram weights have \(O(L)\) bits, since every histogram total is at most \(Q\). Utility keys have \(O(\log(Tm+1))\) bits. Thus exact arithmetic also has polynomial bit complexity.
The choice algorithm does not use \(N\). If admissibility must be checked, testing \(b_s\mid N\) for every type adds only polynomial time in \(L+\log N\).
Therefore, computing the choices is polynomial-time solvable in the parameters specified in the question.
The rule’s inputs and tie order are fixed, and its definition contains no \(N\). Therefore its choices—and consequently all \(U_s^T\)—are identical at every admissible scale.
Put \(A=T(m-1)\) and \(u_*=\min_s U_s^T\). The deficit has the exact expression
\(D_N=\max\{0,A/N-u_*\}\).
Indeed, among supported types, the largest shortfall occurs at the smallest accumulated utility. Since \(u_*\geq0\),
\(0\leq D_N\leq A/N\),
so \(D_N\to0\) along admissible \(N\to\infty\). More precisely:
The first case can occur. Take two candidates, one round, and two equally weighted types with opposite rankings. Both candidates have the same histogram, so the fixed tie order selects one. The final utilities are \(1\) and \(0\); admissible scales are the positive even integers, and \(D_N=1/N\).
Thus vanishing deficit need not mean that every type eventually receives positive utility: the fixed utility profile is compared with a benchmark that tends to zero.
⟨structured verdict parsed — rendered above⟩
Assessment: proved. The prover resolves all three questions. The replication correspondence is exact, the cited theorem supplies the stated prefix bound, the algorithm has polynomial bit complexity in the support encoding, and the population-scale limit follows from the exact deficit formula. No major or minor issues were found.
Writing each positive rational mass in lowest terms as \(\mu_s=a_s/b_s\) is valid. Coprimality gives the claimed equivalence between integrality of \(N\mu_s\) and divisibility of \(N\) by \(b_s\). Thus the admissible scales are precisely the positive multiples of \(N_0=\operatorname{lcm}_s b_s\). In particular, arbitrarily large admissible scales exist.
For any admissible \(N\), the multiplicities \(n_s=N\mu_s\) are positive integers and sum to \(N\). Every supported type therefore has at least one representative; a guarantee for every replicated individual covers every supported type.
Conditional on identical previous choices, the identity
\(H_c(k)=Nh_c(k)\)
is correct for every candidate and utility level. Replication does not change any individual’s accumulated utility.
The ordering correspondence is also correct. At the first differing level \(k_0\), the counts below \(k_0\) agree. If \(H_c(k_0)<H_d(k_0)\), the first differing position of the sorted vectors contains a value greater than \(k_0\) for \(c\) and equal to \(k_0\) for \(d\). That position exists because both vectors have the same total length \(N\). Thus the direction of preference agrees exactly with leximin.
Identical histograms yield identical sorted vectors. Using the specified candidate order for those ties is a valid leximin selection. The induction from zero initial utilities consequently establishes identical choices at every round.
The external dependency is accurately stated and applicable. Definition 5.8 in Kahana–Hazon defines online leximin by maximizing the accumulated-utility vector under leximin over current candidates. The proof of Theorem 14 explicitly establishes, for every round and individual, the bound \(u_i^t\geq\lfloor t(m-1)/n\rfloor\). It therefore supplies the stronger integer prefix bound claimed by the prover, rather than merely a final additive guarantee. The definition permits any maximizing candidate, and the theorem’s proof does not impose a special tie-breaking rule. [Kahana–Hazon, Definition 5.8 and Theorem 14](https://arxiv.org/pdf/2305.18024)
The replicated population satisfies the stated hypotheses: finitely many individuals, standard Borda scores from strict rankings, additive accumulated utilities initially zero, and online choices using current and previously revealed rankings. There is no requirement that individuals have distinct schedules.
The separate treatment of \(N=1\) is correct. Positive integral multiplicities summing to one force a single supported type. Maximizing its accumulated utility selects its unique top candidate each round.
Applying the cited bound with \(n=N\) therefore gives
\(U_s^t\geq\lfloor t(m-1)/N\rfloor\)
for every supported type and every prefix. The inequality \(\lfloor x\rfloor+1>x\) holds for all real \(x\), including integers, so the claimed strict additive inequality follows. Fixing an arbitrary admissible \(N\) establishes the required universal quantifier over scales.
The common-denominator construction is exact. Each \(b_s\) divides \(Q=\prod_s b_s\), so each weight \(w_s=a_s(Q/b_s)\) is integral. The normalization of masses gives \(\sum_s w_s=Q\), and hence every histogram entry lies between zero and \(Q\).
The binary length of \(Q\) is bounded by the sum of the denominator lengths, which is bounded by \(L\). Constructing \(Q\), performing the exact divisions, and computing the weights require polynomial-time integer arithmetic. Although \(Q\) can be numerically large, its binary representation remains polynomially bounded.
The sparse histogram construction correctly combines equal utility keys. Merging two sorted lists while assigning zero to absent keys identifies their least differing utility level and implements the prescribed comparison. Scanning all candidates with the fixed tie order returns the required candidate.
The stated operation bound
\(O(Tm\tau\log(\tau+1))\)
covers sorting, aggregation, candidate comparisons, and utility updates. Reading current rankings and converting them to Borda scores also fits within polynomial time.
Weights have \(O(L)\) bits, and utility keys have \(O(\log(Tm+1))\) bits. Thus the operation count yields polynomial bit complexity. No population expansion is needed, and the optional admissibility check is polynomial in \(L+\log N\).
The polynomial-time claim is established.
With masses, rankings, and tie order fixed, the rule contains no dependence on \(N\). Its choices and resulting utilities are consequently identical across admissible scales.
The exact formula
\(D_N=\max\{0,T(m-1)/N-u_*\}\),
where \(u_*=\min_s U_s^T\), follows directly from maximizing the shortfall over the finite support.
All utilities are nonnegative, so the bound
\(0\leq D_N\leq T(m-1)/N\)
is correct and proves convergence to zero along admissible scales.
Both refinements are valid:
The two-candidate example is correctly computed: opposite rankings with equal masses produce identical candidate histograms, final utilities \(1\) and \(0\), admissible positive even scales, and deficit \(1/N\).
No additional clarification or mathematical repair is needed. The output establishes every requested conclusion.
⟨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.