Answer: Polynomial-time solvable, using at most \((m-|A|+1)m\tau\) exact rational linear-programming feasibility tests and total bit complexity polynomial in \(m,\tau,p,L\).
Theorem 3 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateLet Op be a choice function satisfying (H), and let A be a subset of Ω. Define the sequence of sets B0, B1, . . . by B0 = Ω and for i ≥1, Bi = A∪(Bi−1 \Op(Bi−1)). There exists k ≤|Ω|−|A| such that Bk+1 = Bk, and Op(Bk) ⊆A, and for all i with 1 ≤i < k, Bi ⊊Bi−1; and Bk+1 = Bk. We have Op(π)(A) = Op(Bk).
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite catalog \(\Omega\), a finite support \(T\) of elicitation types with binary-rational masses \(\mu_t\) summing to \(1\), compact linear-utility inputs defining each type’s possibly optimal set \(\mathrm{PO}_t(B)\), a rational quorum \(q\), and a menu \(A\subseteq\Omega\), compute exactly \(F_\mu^{q\,(\pi)}(A)\). Here \(F_\mu^q(B)=\{\alpha\in B:\sum_{t:\,\alpha\in\mathrm{PO}_t(B)}\mu_t\ge q\}\), and \(F_\mu^{q\,(\pi)}\) is its path-independent enforcement.
Let \(\Omega\) be an explicitly listed catalog, with \(m=|\Omega|\), and let \(A\subseteq\Omega\). A society is given by its support: a list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\) summing to \(1\); \(\tau\) counts supported types, not all possible types.
Each alternative has an explicitly given vector \(x_\alpha\in\mathbb Q^p\). Each type has a nonempty rational polytope \(Y_t\subseteq\mathbb R^p\), specified by explicit weak linear inequalities, representing admissible utility weights. Coordinates and weights may have either sign; no normalization of weights is imposed.
For \(B\subseteq\Omega\), define \(\mathrm{PO}_t(B)=\{\alpha\in B:\exists w\in Y_t\ \forall\beta\in B,\ w\cdot x_\alpha\ge w\cdot x_\beta\}\); ties count as optimal. Given binary-rational \(0<q\le1\), define \(F_\mu^q(B)=\{\alpha\in B:\sum_{t:\alpha\in\mathrm{PO}_t(B)}\mu_t\ge q\}\).
A choice function \(G\) maps subsets of \(\Omega\) to subsets of themselves; empty outputs are allowed. It is path independent if \(G(B\cup C)=G(G(B)\cup C)\) for all \(B,C\subseteq\Omega\). Define \(F_\mu^{q\,(\pi)}(B)\) as the union of \(G(B)\) over all path-independent choice functions \(G\) satisfying \(G(C)\subseteq F_\mu^q(C)\) for every \(C\subseteq\Omega\).
Is exact computation of \(F_\mu^{q\,(\pi)}(A)\) polynomial-time solvable, or is it NP-hard? State running times in \(m,\tau,p,L\), where \(L\) is the total binary input length.
Known results: on a finite catalog, path-independent enforcement of any choice function satisfying Heritage, \(G(C)\cap B\subseteq G(B)\) whenever \(B\subseteq C\), is computable with at most \(m-|A|+1\) evaluations of that function. For two agents with linear-utility elicitation, exact enforcement of the intersection of their possibly optimal functions is polynomial-time computable. [Source](https://cora.ucc.ie/bitstreams/04a74408-d5a3-4e72-9725-b2d0ea982df0/download).
Exact computation of \(F_\mu^{q\,(\pi)}(A)\) is polynomial-time solvable in \(m,\tau,p,L\). The algorithm uses at most \((m-|A|+1)m\tau\) rational linear-programming feasibility tests.
The essential fact is that the threshold rule satisfies Heritage for every supported society and every admissible threshold.
Write \(F=F_\mu^q\). By definition, \(F(B)\subseteq B\), so \(F\) is a choice function.
Let \(B\subseteq C\subseteq\Omega\), and let \(\alpha\in F(C)\cap B\). For every type \(t\), if \(\alpha\in\mathrm{PO}_t(C)\), there is a weight \(w\in Y_t\) satisfying \(w\cdot x_\alpha\ge w\cdot x_\beta\) for every \(\beta\in C\). The same weight satisfies these inequalities for every \(\beta\in B\). Therefore,
\(\{t:\alpha\in\mathrm{PO}_t(C)\}\subseteq\{t:\alpha\in\mathrm{PO}_t(B)\}\).
Because the masses are positive, this inclusion implies
\(\displaystyle \sum_{t:\alpha\in\mathrm{PO}_t(B)}\mu_t\ge\sum_{t:\alpha\in\mathrm{PO}_t(C)}\mu_t\ge q\).
Thus \(\alpha\in F(B)\), proving \(F(C)\cap B\subseteq F(B)\).
This argument permits arbitrary signs in both the alternatives and the weights, and it includes ties.
Write the explicit description of \(Y_t\) as \(Y_t=\{w\in\mathbb R^p:H_tw\le b_t\}\), with \(h_t\) inequalities.
For each \(\alpha\in B\) and each supported type \(t\), test feasibility of
\(\displaystyle H_tw\le b_t,\qquad (x_\beta-x_\alpha)\cdot w\le0\quad\text{for every }\beta\in B\setminus\{\alpha\}\).
This system is feasible if and only if \(\alpha\in\mathrm{PO}_t(B)\): its constraints say precisely that an admissible weight makes \(\alpha\) weakly optimal in \(B\).
Each test is rational linear feasibility with \(p\) variables and at most \(h_t+|B|-1\) inequalities. Such feasibility is decidable exactly in time polynomial in the binary encoding length. Lower-dimensional polytopes and weak inequalities are allowed; neither an interior-point assumption nor weight normalization is required.
After these tests, add the masses of the feasible types and compare the sum with \(q\). This comparison also has polynomial bit complexity. Indeed, a common denominator obtained by multiplying the input denominators of the masses and \(q\) has \(O(L)\) bits. After scaling, all sums and comparisons use integers of \(O(L)\) bits, since every selected mass sum lies between zero and one.
Consequently, one evaluation of \(F(B)\) requires at most \(|B|\tau\le m\tau\) polynomial-time feasibility tests and polynomial-time exact arithmetic.
For a Heritage choice function, the enforcement theorem applies to the pointwise union of all path-independent choice functions lying below it—the definition used in this question. Its constructive form starts with \(B_0=\Omega\) and iterates
\(B_{i+1}=A\cup(B_i\setminus F(B_i))\).
At the first index \(k\) for which \(B_{k+1}=B_k\), it returns \(F(B_k)=F^{(\pi)}(A)\). This is [Theorem 3 of the supplied source](https://cora.ucc.ie/bitstreams/04a74408-d5a3-4e72-9725-b2d0ea982df0/download).
The hypotheses are satisfied: the catalog is finite, \(F\) is a choice function, and Section 1 proves Heritage. The theorem allows empty outputs.
Moreover, \(A\subseteq B_i\) throughout the iteration. Every nonterminal iteration removes at least one element outside \(A\), so there are at most \(m-|A|\) strict decreases and one final evaluation. Combining this with Section 2 gives the claimed bound of \((m-|A|+1)m\tau\) feasibility tests.
If \(A=\varnothing\), the output is immediately \(\varnothing\), since every choice function maps the empty set to itself.
For an explicit bound, let \(\mathsf{LP}(p,h,s)\) denote a polynomial upper bound for exact rational feasibility with \(p\) variables, at most \(h\) inequalities, and encoding length at most \(s\).
Each feasibility instance above has at most \(L+m\) inequalities and encoding length \(O((1+mp)L)\). The latter follows because the original polytope description occupies at most \(L\) bits, and each of the at most \(mp\) new rational coefficients has \(O(L)\) bits.
Precomputing all vector differences and scaling the masses takes \(O((m^2p+\tau+1)L^2)\) bit operations using elementary integer arithmetic. A conservative total bound is therefore
\(\displaystyle O\!\left((m^2p+\tau+1)L^2+(m-|A|+1)m\tau\left[\mathsf{LP}\!\left(p,L+m,O((1+mp)L)\right)+(1+mp)L\right]\right)\).
This is polynomial in \(m,\tau,p,L\), with \(\tau\) counting only explicitly supported types. Thus the target computation belongs to polynomial time; an NP-hardness classification under polynomial-time reductions would imply \(\mathrm P=\mathrm{NP}\).
⟨structured verdict parsed — rendered above⟩
The prover’s polynomial-time claim is correct. The argument resolves the stated task, and no major or minor mathematical gaps were found.
For arbitrary \(B\subseteq C\subseteq\Omega\) and \(\alpha\in F(C)\cap B\), every witness weight establishing \(\alpha\in\mathrm{PO}_t(C)\) also establishes \(\alpha\in\mathrm{PO}_t(B)\). Restricting the comparison set preserves every required weak inequality.
Consequently, the set of supporting types can only increase when passing from \(C\) to \(B\). Positive masses preserve the corresponding inequality between support sums, so the threshold remains satisfied. This proves Heritage for all subsets, types, and permitted thresholds.
The argument correctly accommodates ties, negative coordinates, negative weights, and weights without normalization. It requires no common witness across different types.
For each \(\alpha\in B\), the constraints
\[
H_tw\le b_t,\qquad (x_\beta-x_\alpha)\cdot w\le0
\]
for \(\beta\in B\setminus\{\alpha\}\) express precisely the existence of an admissible weight making \(\alpha\) weakly optimal. Omitting the comparison with \(\alpha\) itself removes only a tautology.
The stated count of \(p\) variables and at most \(h_t+|B|-1\) inequalities is correct. All coefficients are rational. The standard polynomial-time result for exact rational linear feasibility applies to explicit rational systems of weak linear inequalities, including infeasible and lower-dimensional systems. Its hypotheses are satisfied here.
Multiplying the input denominators gives a common denominator whose bit length is bounded by the sum of their bit lengths, hence \(O(L)\).
Each scaled mass is an integer. Because the masses are positive and sum to one, every selected mass sum lies in \([0,1]\); its scaled numerator therefore also has \(O(L)\) bits. Scaling \(q\), summing selected masses, and comparing with the threshold all have polynomial bit complexity.
Thus an evaluation of \(F(B)\) uses at most \(|B|\tau\) exact feasibility tests and polynomial additional arithmetic. Only explicitly supported types are enumerated.
I checked the cited source. Its definition of enforcement agrees with the task’s pointwise union over subordinate path-independent choice functions. Its choice-function definition permits empty outputs, and its path-independence identity matches the one in the task.
Theorem 3 applies to a choice function on a finite catalog satisfying Heritage. It gives the stated iteration and identifies the terminal output with the path-independent enforcement. The prover establishes all its hypotheses. No assumption of nonempty choice outputs is missing. [Supplied source, Definition 1 and Theorem 3](https://cora.ucc.ie/bitstreams/04a74408-d5a3-4e72-9725-b2d0ea982df0/download).
The iteration retains \(A\) and deletes only elements outside \(A\). Every nonterminal iteration deletes at least one such element. Therefore there are at most \(m-|A|\) strict decreases and one final evaluation.
The resulting upper bound of \((m-|A|+1)m\tau\) feasibility tests is valid. At termination, the cited theorem guarantees that the returned set is exactly \(F_\mu^{q\,(\pi)}(A)\), rather than merely a subset or approximation.
The empty-input case is correctly handled: every choice function returns the empty set on the empty set. When \(A=\Omega\), the iteration is stationary immediately and needs only its initial evaluation. The empty-catalog case is covered by the empty-input shortcut.
Explicitly encoded inequalities give \(h_t\le L\), so the claimed bound of \(L+m\) inequalities per feasibility instance is safe.
Subtracting rational coordinates produces coefficients with \(O(L)\) bits. There are at most \(mp\) added coefficients per instance, yielding the stated encoding bound \(O((1+mp)L)\).
The preprocessing estimate safely covers all vector differences and common-denominator scaling using elementary integer arithmetic. The additional term in the total bound covers instance construction and threshold arithmetic. Since \(\mathsf{LP}\) denotes a polynomial bound for exact rational feasibility, the displayed total running time is polynomial in \(m,\tau,p,L\).
The algorithm computes the exact requested set in polynomial time under the specified explicit input representation. The final qualification concerning NP-hardness and \(\mathrm P=\mathrm{NP}\) is correct.
No repair or additional mathematical 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.