← back to the atlas

d4-conf-atal-2013-0150 (d4-conf-atal-2013-0150)

Answer: $C(S,\kappa,T)=1$ whenever some supported type accepts a slot. If every acceptable neighborhood is empty, the defining infimum has an empty domain and equals $+\infty$ under the extended-real convention.

The anchor (named result in the paper)

Proposition 10 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateEvery online algorithm under Assumption UV has a worst-case approximation ratio of at most 3 4, even on an in- terval. If we relax Assumption UV, then the bound is at most 1 2. PROOF. Consider the following two sequences of n agents, where n = m. The first n/2 agents (denoted N ′) are of type (g1, n), with goal g1 and maximum distance to walk n.

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

The continuous mirror question, as graded

Given a finite two-goal interval geometry \(S\), per-capita slot capacities \(\kappa_s\), and a fixed support of at most \(\tau\) uniform-value MAXDISTANCE types \(\theta=(g,r)\) arriving in two successive nonatomic cohorts with rational masses, what is \(\sup_{\pi}\inf_{\mu}\mathrm{SW}(\pi,\mu)/\mathrm{OPT}_{\mathrm{frac}}(\mu)\)? Here \(\pi\) is a causal posted-price policy that knows the geometry and capacities but not future cohort masses; each infinitesimal arrival chooses an available slot maximizing \(\phi\mathbf{1}[d(g,s)\le r]-p_s\), with fixed tie-breaking; and \(\mathrm{OPT}_{\mathrm{frac}}\) is the offline maximum-welfare mass matching.

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

Let \(S\) contain \(m\geq1\) distinct rational slot locations in \([0,R]\), with rational \(R>0\), goals \(g_1=0,g_2=R\), distance \(d(x,y)=|x-y|\), and positive rational capacities \(\kappa_s\).
A society is given by its support: the list \(T\) of its \(\tau\) types with positive total mass, each with its mass as a binary rational; \(\tau\) is the support size, not the number of possible types. Types are \(\theta=(g,r)\), with \(g\in\{g_1,g_2\}\), rational \(r\geq0\), and common rational value \(\phi>0\).
Masses and capacities use a fixed reference-population unit; total mass need not equal \(1\). An arrival instance \(\mu\) specifies two successive positive-mass cohorts, each an ordered finite list of homogeneous nonatomic blocks of positive rational mass; their union has support exactly \(T\). The adversary fixes masses and block orders before policy randomization.
A causal, possibly randomized posted-price policy knows \(S,\kappa,T,\phi\), observes cumulative arrivals, purchases, rejections and the cohort boundary, and may update prices using only this history. Types, block boundaries and unarrived masses are not announced; prices are anonymous and lie in \([0,\infty]\).
Each infinitesimal arrival irrevocably consumes equal capacity mass from an available slot maximizing \(\phi\mathbf1[d(g,s)\leq r]-p_s\), provided this maximum is nonnegative; otherwise it takes the outside option, of value and utility \(0\). Utility ties prefer smaller distance, then smaller slot label; a slot is preferred to the outside option at zero utility. Exhausted capacity is unavailable and never replenished.
Restrict policies to those inducing well-defined measurable allocations. Welfare is the integral of allocated values, excluding payments. Writing \(a_\theta\) for total type mass, \(\mathrm{OPT}_{\mathrm{frac}}(\mu)\) is the maximum of \(\phi\sum_{\theta,s}x_{\theta s}\) subject to \(x\geq0\), \(\sum_sx_{\theta s}\leq a_\theta\), \(\sum_\theta x_{\theta s}\leq\kappa_s\), and \(x_{\theta s}=0\) whenever \(d(g,s)>r\).
State any running times in \(m,\tau,L,B\), where \(L\) is the total binary input length and \(B\) is the number of arrival blocks.

What is the optimal competitive ratio \(C(S,\kappa,T)=\sup_\pi\inf_{\mu:\mathrm{OPT}_{\mathrm{frac}}(\mu)>0}\mathbb E[\mathrm{SW}(\pi,\mu)]/\mathrm{OPT}_{\mathrm{frac}}(\mu)\) for this two-cohort posted-price problem?

For discrete uniform-value interval instances with unknown population, every randomized online algorithm has worst-case competitive ratio at most \(3/4\), even with types revealed on arrival. [Meir–Chen–Feldman](https://cs.tau.ac.il/~mfeldman/papers/MCFc13.pdf)
For centrally allocated fractional bipartite matching with each batch fully revealed, the optimal two-batch competitive ratio is \(3/4\); that model does not impose private-type posted-price implementation. [Feng–Niazadeh](https://arxiv.org/html/2211.16581v1) No result settling the exact model above was located.

Modeling choices made when packaging the task

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

Result and information model

For the policy class specified in the question, every nonvacuous society satisfies
$$ \boxed{C(S,\kappa,T)=1.} $$

Here the masses $a_\theta$ supplied with $T$ are known and fixed. Admissible arrival instances vary their block decomposition, order, and cohort split.

The proof uses a substantive feature of the stated model: arbitrary measurable price changes and exact observations of cumulative purchases are permitted. Diagnostic menus can occupy arbitrarily little arrival mass while occurring with positive mass in every interval. Because there are finitely many homogeneous blocks, these observations reveal the current acceptable slots almost everywhere, using only strictly preceding history. I prove this carefully below.

If every supported type accepts no slot, there is no instance with positive fractional optimum. The defining infimum then has an empty domain; under the extended-real convention, its value is $+\infty$.

1. Normalization and the universal upper bound

Write
$$ N_\theta=\{s\in S:|g-s|\leq r\}, \qquad A=\sum_{\theta\in T}a_\theta. $$
Parameterize arrivals by cumulative mass $t\in[0,A]$. For each admissible instance, the type function $\theta(t)$ is constant on finitely many intervals. Block endpoints form a finite set of Lebesgue measure zero.

Let $Z$ denote the maximum acceptable mass in the fractional allocation problem:
$$ Z=\max\left\{ \sum_{\theta,s}x_{\theta s}: x\geq0,\ \sum_sx_{\theta s}\leq a_\theta,\ \sum_\theta x_{\theta s}\leq\kappa_s,\ x_{\theta s}=0\text{ if }s\notin N_\theta \right\}. $$
Because the type totals are fixed,
$$ \mathrm{OPT}_{\mathrm{frac}}(\mu)=\phi Z $$
for every admissible arrival instance.

Any policy’s positive-value allocations, after discarding zero-value allocations, give a feasible vector in this optimization problem. Thus, for every realization of policy randomness,
$$ \mathrm{SW}(\pi,\mu)\leq\phi Z. $$
Consequently,
$$ C(S,\kappa,T)\leq1. $$

Henceforth assume $Z>0$. This holds precisely when some supported type accepts some slot: the reverse implication follows by allocating positive mass on one such edge, using the positive mass and capacity hypotheses.

2. Reserve a nearly optimal fractional allocation

Fix a rational number $\varepsilon\in(0,1)$. Choose an acceptable pair $(\theta_0,s_0)$ and put
$$ z_0=\min\{a_{\theta_0},\kappa_{s_0}\}>0. $$
Then $Z\geq z_0$.

Choose a positive rational $\delta$ satisfying
$$ \delta< \min\left\{ \min_{\theta\in T}a_\theta,\ \min_{s\in S}\kappa_s,\ \frac{\varepsilon z_0}{m+\tau} \right\}. $$
Consider the reduced allocation problem with type masses $a_\theta-\delta$ and capacities $\kappa_s-\delta$. Let $x^\delta$ be an optimal allocation and let
$$ Z_\delta=\sum_{\theta,s}x^\delta_{\theta s}. $$

Claim.
$$ Z_\delta\geq Z-(m+\tau)\delta>(1-\varepsilon)Z. $$

Proof. Start with an optimal allocation for the original problem. For each type, delete any mass exceeding the reduced row bound $a_\theta-\delta$. Each row requires deletion of at most $\delta$, so these deletions total at most $\tau\delta$.

Next, for each slot, delete any mass exceeding its reduced capacity $\kappa_s-\delta$. Each column requires deletion of at most $\delta$, because its mass before these deletions is at most $\kappa_s$. Column deletions preserve all reduced row bounds and total at most $m\delta$.

The resulting allocation is feasible for the reduced problem and has mass at least $Z-(m+\tau)\delta$. Finally,
$$ (m+\tau)\delta<\varepsilon z_0\leq\varepsilon Z. $$
This proves the claim. $\square$

Define the active slots
$$ J=\left\{s\in S:\sum_\theta x^\delta_{\theta s}>0\right\}. $$
Since $Z_\delta>0$, the set $J$ is nonempty. Slots outside $J$ will always have price $\infty$.

Group types according to their acceptable sets restricted to $J$. For each occurring set $H\subseteq J$, define
$$ T_H=\{\theta\in T:N_\theta\cap J=H\}, \qquad a_H=\sum_{\theta\in T_H}a_\theta, $$
and initialize reservation quantities
$$ q^0_{Hs}=\sum_{\theta\in T_H}x^\delta_{\theta s}, \qquad Q_H=\sum_{s\in J}q^0_{Hs}. $$
Feasibility gives
$$ q^0_{Hs}=0\quad\text{when }s\notin H. $$
Also, since $T_H$ is nonempty,
$$ Q_H \leq\sum_{\theta\in T_H}(a_\theta-\delta) \leq a_H-\delta. $$
For each active slot,
$$ \sum_Hq^0_{Hs}\leq\kappa_s-\delta. $$

These reservations specify which normal purchases the policy will permit.

3. Diagnostic sets of arbitrarily small total mass

Let $\lambda$ denote Lebesgue measure.

Lemma. There are pairwise disjoint Borel sets $E_s\subseteq(0,A)$, one for each $s\in J$, such that
$$ \lambda\left(\bigcup_{s\in J}E_s\right)<\delta $$
and, for every nonempty open interval $I\subseteq(0,A)$,
$$ \lambda(E_s\cap I)>0 \qquad\text{for every }s\in J. $$

Proof. Enumerate all pairs $(s,I)$ where $s\in J$ and $I$ is an open interval with rational endpoints contained in $(0,A)$.

At step $n$, choose a compact nowhere dense set $F_n$ of positive measure inside the interval specified by that pair, avoiding all previously chosen sets, and with
$$ \lambda(F_n)<\delta\,2^{-n-1}. $$
This choice is possible. A finite union of compact nowhere dense sets leaves an open subinterval of the specified interval. Inside a sufficiently short closed subinterval, remove open neighborhoods of a countable dense set whose total length is less than half the subinterval’s length. The remaining set is compact, nowhere dense, and has positive measure.

Let $E_s$ be the union of the sets $F_n$ assigned to $s$. These sets are Borel and pairwise disjoint, and their total measure is less than $\delta$.

Every nonempty open interval contains an interval with rational endpoints. The construction places a positive-measure set for each slot inside that smaller interval. $\square$

Put
$$ E=\bigcup_{s\in J}E_s, \qquad E_0=[0,A]\setminus E. $$
Times in $E$ will use diagnostic menus; times in $E_0$ will use reservation menus.

4. Causal recovery of the current acceptable set

At every diagnostic time $t\in E_s$, post price $\phi/2$ at $s$ and price $\infty$ everywhere else.

Whenever $s$ remains available, the arriving mass purchases precisely when $s$ is acceptable: an acceptable slot offers utility $\phi/2>0$, whereas an unacceptable slot offers utility $-\phi/2<0$.

Let $Y_s(t)$ be the observed cumulative mass purchased at slot $s$. The policy can extract from its recorded history the cumulative diagnostic purchases
$$ D_s(t)=\int_{[0,t)\cap E_s}dY_s(u). $$
It also knows the deterministic function
$$ e_s(t)=\lambda([0,t)\cap E_s). $$

For $t>0$, set $h_n=t/2^n$ and define
$$ b_s(t)= \limsup_{n\to\infty} \frac{D_s(t)-D_s(t-h_n)} {e_s(t)-e_s(t-h_n)}. $$
Every denominator is positive by the diagnostic-set lemma. Define
$$ \widehat H(t)=\{s\in J:b_s(t)>1/2\}. $$
At $t=0$, use an arbitrary default estimate.

This estimate is causal. Every integral used in its definition concerns mass strictly preceding $t$. Taking a limit of these historical quantities uses no future observation.

Recovery claim. If the active slots remain available, then, outside the finite set of block endpoints,
$$ \widehat H(t)=N_{\theta(t)}\cap J. $$

Proof. Fix a time $t$ strictly inside a homogeneous block. For all sufficiently large $n$, the entire interval $(t-h_n,t)$ belongs to that block.

Throughout such an interval, a diagnostic arrival at $s$ purchases exactly when $s\in N_{\theta(t)}$. Therefore
$$ D_s(t)-D_s(t-h_n) = \mathbf1[s\in N_{\theta(t)}]\, \bigl(e_s(t)-e_s(t-h_n)\bigr). $$
The displayed ratio is eventually exactly zero or exactly one. Its limsup therefore recovers acceptability for every $s\in J$. $\square$

Crucially, the policy need not know whether $t$ is inside a block. The historical limit gives the correct estimate at every interior time automatically.

5. The posted-price policy

Maintain reservation balances $q_{Hs}(t)$, initialized to $q^0_{Hs}$.

The deterministic policy is:

All prices are anonymous. Each menu offers at most one finite-price slot, so the prescribed utility tie rules introduce no additional choices.

Capacity safety

At any slot $s\in J$, reservation purchases total at most its initial reservations:
$$ \text{reservation purchases at }s \leq\sum_Hq^0_{Hs} \leq\kappa_s-\delta. $$
Diagnostic purchases there total at most $\lambda(E_s)$, which is less than $\delta$. Hence, at every point in the process,
$$ Y_s(t) \leq\sum_Hq^0_{Hs}+\lambda(E_s) <\kappa_s. $$
Thus every active slot remains available throughout. Slots outside $J$ receive no purchases.

This verifies the availability hypothesis in the recovery claim.

6. Well-definedness and measurability

I give an explicit allocation construction to justify the feedback rule.

For a fixed admissible arrival instance, let
$$ H(t)=N_{\theta(t)}\cap J. $$
This is a measurable function, constant on finitely many intervals.

At diagnostic times in $E_s$, assign the arriving mass to $s$ exactly when $s\in H(t)$.

For each group $H$, define its cumulative non-diagnostic arrival mass
$$ v_H(t)= \int_0^t \mathbf1[u\in E_0]\, \mathbf1[H(u)=H]\,du. $$
Order that group’s positive reservations by slot label. Assign its non-diagnostic arrivals consecutively to those reservations, using $v_H(t)$ to determine the current reservation. Once $v_H(t)$ reaches $Q_H$, reject further non-diagnostic arrivals of that group.

This allocation is measurable: the diagnostic sets are Borel, the type function is measurable, and each $v_H$ is absolutely continuous. Reservation choices are determined by finitely many thresholds of these functions.

It also respects capacities, by the capacity bound just proved. Consequently, its diagnostic purchase history gives
$$ \widehat H(t)=H(t) $$
outside block endpoints. Its reservation balances therefore produce exactly the menus specified by the causal policy, and buyers accept the intended reservation slot because it belongs to $H(t)$.

At block endpoints, apply the stipulated buyer choice to the menu computed from past history. Altering allocations at these finitely many points changes no mass, reservation balance, or welfare.

This establishes existence of a measurable allocation consistent with the policy. It also determines the allocation almost everywhere: capacity safety forces the diagnostic purchase history, that history determines the group estimate almost everywhere, and the fixed reservation order then determines normal purchases.

The dense diagnostic schedule therefore induces a well-defined measurable allocation, despite its unrestricted price variation.

7. Welfare guarantee

For every occurring group $H$, its total diagnostic arrival mass is less than $\delta$. Its non-diagnostic arrival mass consequently satisfies
$$ v_H(A)>a_H-\delta\geq Q_H. $$
Thus every reservation of every group is fully consumed.

Every reservation purchase has value $\phi$, because its assigned slot belongs to the correctly inferred acceptable set almost everywhere. Diagnostic purchases also have value $\phi$. Therefore
$$ \frac{\mathrm{SW}(\pi_\varepsilon,\mu)}{\phi} \geq\sum_HQ_H =\sum_{\theta,s}x^\delta_{\theta s} =Z_\delta >(1-\varepsilon)Z. $$
For every admissible arrival instance,
$$ \frac{\mathrm{SW}(\pi_\varepsilon,\mu)} {\mathrm{OPT}_{\mathrm{frac}}(\mu)} >1-\varepsilon. $$

The diagnostic budget covers the whole known mass horizon. This bound is uniform in the number $B$ of blocks, their orders, and the cohort boundary.

For every positive rational $\varepsilon$, we have constructed one admissible deterministic policy with this guarantee. Taking the supremum over policies yields
$$ C(S,\kappa,T)\geq1. $$
Together with the universal upper bound,
$$ C(S,\kappa,T)=1. $$

This proves the value of the supremum. It does not assert that a single policy attains welfare exactly equal to the optimum on every arrival instance.

8. Computation and scope

Checking whether the society is nonvacuous takes at most $m\tau$ rational distance comparisons, hence polynomial time in $m,\tau,L$. Once nonvacuity is established, the exact competitive-ratio value is $1$; computing that value does not depend on $B$.

For each fixed rational $\varepsilon$, the reservation allocation can be computed in polynomial time in $m,\tau,L$. Its reduced problem is a rational maximum-flow network with $m+\tau+2$ vertices and at most $m\tau+m+\tau$ arcs. Clearing denominators gives integer capacities of polynomial bit length, so a polynomial-time maximum-flow algorithm applies.

The witnessing online policy uses countable Borel diagnostic sets and limits of exact historical observations. No finite online computation-time or finite price-update bound is asserted. The measurability restriction in the question is verified explicitly above.

The proof actually applies to any finite family of acceptable sets; the endpoint geometry is unnecessary for this construction. Its essential assumptions are known type totals, finitely many homogeneous arrival blocks, and the permitted measurable policies.

The cited unknown-population obstruction concerns different information: [Meir–Chen–Feldman, Proposition 10](https://cs.tau.ac.il/~mfeldman/papers/MCFc13.pdf) varies the population. The [Feng–Niazadeh model](https://arxiv.org/html/2211.16581v1) reveals batch information before allocating it. The argument here directly verifies private-type posted-price implementation in the stated nonatomic model.

⟨structured verdict parsed — rendered above⟩

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

The output proves the claimed value under the policy class stated in the task. I found no substantive gap or false step. Its use of exact historical limits is essential, but the task permits such policies and imposes measurability rather than finite computation or finitely many price updates.

For societies with positive fractional optimum, the conclusion is
$$ C(S,\kappa,T)=1. $$
The output also correctly separates this supremum statement from existence of a policy attaining the optimum exactly.

Step-by-step verification

1. Interpretation of the supplied masses

The prover treats the masses $a_\theta$ as known, fixed society data. This agrees with the task: the society is supplied as a support list containing each type’s total mass, and the policy knows that society.

Thus admissible instances change block decomposition, arrival order, and cohort split while preserving the total mass of each type. Consequently, the fractional optimum is independent of those choices.

No additional population-information assumption is introduced.

2. Normalization and upper bound

Parameterizing arrivals by cumulative mass on $[0,A]$ is legitimate because every block has positive mass and there are finitely many blocks. The type function is therefore piecewise constant, with finitely many exceptional endpoints.

The optimization defining $Z$ is exactly the task’s fractional optimization after dividing its objective by the common positive value $\phi$. Hence
$$ \mathrm{OPT}_{\mathrm{frac}}(\mu)=\phi Z. $$

For any realized policy allocation, retaining only acceptable purchases gives feasible type-slot totals: no type receives more than its arriving mass, and no slot supplies more than its capacity. Zero-value purchases cannot increase welfare. Therefore
$$ \mathrm{SW}(\pi,\mu)\leq \phi Z. $$
This proves the universal upper bound whenever the denominator is positive.

The nonvacuity test is also correct. An acceptable edge supports a positive allocation because both its type mass and slot capacity are positive; without any acceptable edge, the optimum is zero.

3. Reduced allocation and reservation margins

The chosen $\delta$ makes every reduced type mass and capacity positive.

The deletion argument correctly bounds the loss:

Thus
$$ Z_\delta\geq Z-(m+\tau)\delta. $$
The stipulated bound on $\delta$, together with $z_0\leq Z$, gives the claimed strict inequality
$$ Z_\delta>(1-\varepsilon)Z. $$

Grouping types by their acceptable sets on $J$ preserves reservation acceptability. The group and slot margins follow directly from feasibility:
$$ Q_H\leq a_H-|T_H|\delta\leq a_H-\delta, \qquad \sum_Hq^0_{Hs}\leq\kappa_s-\delta. $$

These margins cover diagnostic losses separately from reservation purchases.

4. Diagnostic-set lemma

The construction is valid.

At each finite stage, the previously chosen sets form a compact nowhere dense union. Its complement inside the designated open interval contains an open subinterval. The described removal of small open neighborhoods of a countable dense set produces a compact nowhere dense set of positive measure inside that subinterval.

The geometric measure bounds ensure total diagnostic measure below $\delta$. Avoiding all preceding sets ensures pairwise disjointness.

Every nonempty open interval contains a rational-endpoint subinterval, and the enumeration assigns a positive-measure set to every slot in every such subinterval. Therefore the required property is positive measure in every interval, rather than merely density.

No missing measure-theoretic lemma is needed here.

5. Diagnostic observations and causal recovery

The diagnostic menu implements the asserted acceptability test:

The policy can recover $D_s$ from its purchase history and its own deterministic diagnostic schedule. The denominator in every historical ratio is positive by the diagnostic-set lemma.

For a time strictly inside a homogeneous block, every sufficiently short preceding interval lies wholly within that block. Provided the slot remains available, the diagnostic purchase measure on that interval is exactly its diagnostic arrival measure multiplied by the block’s acceptability indicator. The ratios are therefore eventually exactly zero or exactly one.

The estimator uses only observations at times strictly preceding the current arrival. Its limit does not introduce future information. At a block endpoint, recovery may fail, but these finitely many points carry zero arrival mass.

This is the crucial unusual step, and it is valid under the stated information and policy restrictions.

6. Capacity safety and absence of circular reasoning

The safety bound does not require correct type recovery.

Reservation purchases at a slot cannot exceed its initial reservation balances, regardless of which group is inferred. Diagnostic purchases cannot exceed the measure of that slot’s diagnostic set. Hence
$$ Y_s(t)\leq \sum_Hq^0_{Hs}+\lambda(E_s)<\kappa_s. $$

Every active slot consequently stays available throughout the process. This independently establishes the availability hypothesis used in recovery.

The strict capacity margin also rules out exhaustion at the final cumulative mass.

7. Posted-price implementation

Every menu offers at most one finite-price slot. Thus there is no unresolved interaction with the distance or label tie rules.

Once recovery is correct, a reservation menu offers a slot belonging to the arriving group’s acceptable set. The arriving mass purchases it at positive utility. Purchases decrease the applicable reservation balance, and switching upon depletion enforces the reservation bounds.

The policy is anonymous: its menus depend on observed history and reservation state, without requiring the current type to be announced.

8. Existence, measurability, and uniqueness of the induced allocation

Section 6 supplies an explicit allocation for each fixed admissible instance:

The explicit allocation satisfies capacity constraints. Its diagnostic history therefore produces the correct group estimate away from block endpoints, so its reservation assignments agree with the causal pricing rule almost everywhere.

Using the actual type function to verify this candidate allocation does not give the policy extra information: the policy itself uses the historical estimator.

The uniqueness argument also holds. Capacity safety fixes diagnostic behavior; diagnostic behavior fixes the estimated group almost everywhere; the fixed reservation order then fixes reservation purchases. Endpoint choices do not affect cumulative quantities or welfare.

Accordingly, the measurability and well-definedness restriction is satisfied.

9. Welfare and quantifiers

For each group, diagnostic arrivals remove less than $\delta$ of its total mass. Consequently,
$$ v_H(A)>a_H-\delta\geq Q_H. $$
Every reservation is therefore consumed.

All reservation purchases have value $\phi$ almost everywhere, and diagnostic purchases also have value $\phi$. The resulting guarantee is
$$ \mathrm{SW}(\pi_\varepsilon,\mu)\geq \phi Z_\delta >(1-\varepsilon)\phi Z. $$

The same policy works for every admissible block decomposition, order, and cohort split. It does not depend on the unknown number or locations of block boundaries.

Although strict inequalities for individual instances need not yield a strict inequality after taking an infimum, the established bound still gives
$$ \inf_\mu \frac{\mathrm{SW}(\pi_\varepsilon,\mu)} {\mathrm{OPT}_{\mathrm{frac}}(\mu)} \geq 1-\varepsilon. $$
That is sufficient for the prover’s supremum argument. Taking arbitrarily small positive rational $\varepsilon$ proves the lower bound of one.

10. Degenerate case, computation, and cited models

When all acceptable neighborhoods are empty, every fractional optimum is zero. The infimum in the task’s displayed definition then has an empty domain. The prover explicitly states its extended-real convention, under which the value is $+\infty$. This correctly identifies a definitional edge case and does not use it to settle the substantive positive-optimum case.

Checking acceptability uses at most $m\tau$ rational comparisons and is polynomial in the binary input length. Thus the exact ratio value can be determined in polynomial time, independently of $B$.

The reduced allocation is a finite rational maximum-flow problem with the claimed vertex and arc bounds. For fixed rational $\varepsilon$, the required rational margins can have polynomial encoding length, and denominator clearing preserves polynomial bit length. The preprocessing claim is sound.

The output makes no polynomial execution-time claim for the online policy. Its countable diagnostic schedule and exact historical limits should not be confused with a finitely executable online algorithm.

The literature distinctions are accurate. Proposition 10 changes the population between its indistinguishable instances, while the present task supplies fixed type totals. [Meir–Chen–Feldman, Proposition 10](https://cs.tau.ac.il/~mfeldman/papers/MCFc13.pdf). The other cited model reveals batch information before stage-wise allocation. [Feng–Niazadeh, model description](https://arxiv.org/html/2211.16581v1).

Required repairs

None. The argument establishes the claimed supremum under the exact measurable-policy model, while explicitly limiting its computational claims.

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