Answer: Polynomial-time solvable: \((m\tau^4L)^{O(1)}\) bit operations, using an LP with \(O(m\tau^2)\) variables and \(O(\tau^4+m\tau^2)\) constraints.
Proposition 3 — class: other
Given finite male and female type sets with positive rational masses (mu_i) and (nu_j), and a rational matching flow (pi_{ij}\ge 0) with those marginals, specify for each type pair its potential-match prices and income, and for each positive-flow current match its observed bundles and commitment status. Does there exist a type-level split of private consumption, personalized public-good prices, edge weights, and potentials satisfying the type-indexed feasibility constraints of Proposition 3, so that the observed matching flow is rationalizable as a core allocation with transfers? Dummy types may represent singles.
A society is given by its support: lists of male and female types with positive binary-rational masses \(\mu_i,\nu_j\); \(\tau\) is their combined support size, not the number of possible types. Normalize each side's total mass to \(1\), allowing a dummy type \(\emptyset\) on either side to represent singles. The input flow \(\pi_{ij}\geq0\) has these marginals and \(\pi_{\emptyset\emptyset}=0\).
There are \(k\geq1\) private and \(K\geq1\) household public goods; write \(m=k+K\). Every real potential pair and every real individual's single option has binary-rational prices \(p_{ij}\in\mathbb Q_{++}^k,P_{ij}\in\mathbb Q_{++}^K\) and income \(y_{ij}\in\mathbb Q_{++}\).
For each current household cell \(e=(i,j)\) in \(E=\{(i,j):\pi_{ij}>0\}\), the input gives aggregate private consumption \(q_e\in\mathbb Q_+^k\), public consumption \(Q_e\in\mathbb Q_+^K\), and commitment indicator \(v_e\in\{0,1\}\), with \(p_{ij}\cdot q_e+P_{ij}\cdot Q_e\leq y_{ij}\). Commitment requires mutual consent for divorce; single cells have \(v_e=0\).
Define the continuous feasibility problem using real unknowns \(x_e,r_e\in\mathbb R_+^k,z_e\in\mathbb R\) for each current cell, satisfying \(x_e+r_e=q_e\). All mass in a cell uses the same split and potential; different cells may use different ones. A dummy partner receives zero private consumption.
For each real potential pair \((i,\ell)\), choose personalized public-good prices \(A_{i\ell},B_{i\ell}\in\mathbb R_{++}^K\) with \(A_{i\ell}+B_{i\ell}=P_{i\ell}\), shared across all recombinations of those partner types.
For every \(e=(i,j),f=(h,\ell)\in E\) with real \(i,\ell\), including \(e=f\), require an edge weight \(a_{ef}\in\mathbb R\) satisfying \(a_{ef}=p_{i\ell}\cdot(x_e+r_f)+A_{i\ell}\cdot Q_e+B_{i\ell}\cdot Q_f-y_{i\ell}\) and \(v_ez_e-v_fz_f\leq a_{ef}\).
Include every real partner's option of becoming single: require \(v_ez_e\leq p_{i\emptyset}\cdot x_e+P_{i\emptyset}\cdot Q_e-y_{i\emptyset}\) when \(i\) is real, and \(-v_ez_e\leq p_{\emptyset j}\cdot r_e+P_{\emptyset j}\cdot Q_e-y_{\emptyset j}\) when \(j\) is real. Dummy partners impose no additional constraints.
Is this continuous feasibility problem solvable in polynomial time, or is it NP-hard? State running times in \(m,\tau,k,K\) and the total binary input length \(L\).
For finite individual societies, rationalizability as a core allocation with transfers is equivalent to path monotonicity, which admits the displayed form of linear feasibility characterization. [Freer and Surana](https://repository.essex.ac.uk/39852/1/1-s2.0-S0899825624001805-main.pdf)
No result settling exactly this flow-based feasibility problem was located.
The stated continuous feasibility problem is solvable in polynomial time. It reduces to one rational linear program with \(O(m\tau^2)\) variables and \(O(\tau^4+m\tau^2)\) constraints. A valid bit complexity bound is \((m\tau^4L)^{O(1)}\).
The argument applies directly to the displayed flow-based system. Strict positivity of personalized prices is handled exactly, rather than replaced by nonnegativity.
Let \(n=|E|\), let \(c\) be the number of committed cells, and let \(s\) be the number of real potential male–female type pairs.
For each current cell retain \(x_e\), and eliminate \(r_e\) by setting
\(r_e=q_e-x_e,\qquad 0\leq x_e\leq q_e.\)
The inequalities are coordinatewise. Enforce the dummy requirements by adding:
For each committed cell introduce a free scalar \(t_e\). For every uncommitted cell define \(t_e=0\). This represents \(v_ez_e\) exactly: recover \(z_e=t_e\) for committed cells and choose \(z_e=0\) otherwise.
For each real potential pair retain \(A_{i\ell}\), and eliminate \(B_{i\ell}\) by setting
\(B_{i\ell}=P_{i\ell}-A_{i\ell}.\)
Its strict positivity requirements become
\(0<A_{i\ell,g}<P_{i\ell,g}\qquad(g=1,\ldots,K).\)
Finally, eliminate every edge variable \(a_{ef}\) using its defining equality. For \(e=(i,j)\) and \(f=(h,\ell)\) with real \(i,\ell\), the resulting constraint is
\(t_e-t_f\leq p_{i\ell}\cdot(x_e-x_f+q_f)+A_{i\ell}\cdot(Q_e-Q_f)+P_{i\ell}\cdot Q_f-y_{i\ell}.\)
This is affine linear in the unknowns: the consumption vectors \(Q_e,Q_f\), prices, and income are fixed input data. Sharing one \(A_{i\ell}\) across all corresponding recombinations simply makes that variable appear in several linear constraints.
The single-option inequalities become
\(t_e\leq p_{i\emptyset}\cdot x_e+P_{i\emptyset}\cdot Q_e-y_{i\emptyset}\)
when \(i\) is real, and
\(-t_e\leq p_{\emptyset j}\cdot(q_e-x_e)+P_{\emptyset j}\cdot Q_e-y_{\emptyset j}\)
when \(j\) is real.
Every elimination is reversible. Thus this system, including its strict price inequalities, is equivalent to the original feasibility problem.
Introduce one additional scalar \(\delta\), and solve the following ordinary, closed linear program:
Maximize \(\delta\), subject to all the preceding non-strict constraints and
\(0\leq\delta\leq1,\)
\(\delta\leq A_{i\ell,g}\leq P_{i\ell,g}-\delta\qquad\text{for every real pair and every public good}.\)
Equivalence. The original problem is feasible if and only if this LP has a feasible point with \(\delta>0\).
Indeed, from an original feasible solution, all coordinates of \(A\) and \(B=P-A\) are positive. There are finitely many such coordinates, so
\(\delta=\min\bigl(\{1\}\cup\{A_{i\ell,g},B_{i\ell,g}:i,\ell\text{ real},\ 1\leq g\leq K\}\bigr)>0.\)
This gives an LP-feasible point. The definition also covers the case of no real potential pairs, when the minimum is \(1\).
Conversely, an LP-feasible point with \(\delta>0\) satisfies
\(A_{i\ell,g}\geq\delta>0,\qquad B_{i\ell,g}=P_{i\ell,g}-A_{i\ell,g}\geq\delta>0.\)
Reconstructing the eliminated variables therefore gives an original feasible solution.
If the LP is feasible, its feasible set is compact. The variables \(x_e\), \(A_{i\ell}\), and \(\delta\) are bounded by their displayed constraints.
Every committed cell has two real partners, because single cells are uncommitted. Its two single-option inequalities imply the fixed bounds
\(y_{\emptyset j}-p_{\emptyset j}\cdot q_e-P_{\emptyset j}\cdot Q_e\leq t_e\leq p_{i\emptyset}\cdot q_e+P_{i\emptyset}\cdot Q_e-y_{i\emptyset}.\)
Here the lower bound uses \(0\leq q_e-x_e\leq q_e\), and the upper bound uses \(0\leq x_e\leq q_e\). Thus every retained variable is bounded. The feasible set is closed, hence compact, and the continuous objective attains its maximum.
Consequently, the exact decision rule is:
An arbitrary fixed numerical tolerance would not establish this equivalence.
Let \(a,b\) be the numbers of listed male and female support types, including any dummy types. Then
\(a+b=\tau,\qquad n\leq ab\leq\tau^2/4,\qquad s\leq ab\leq\tau^2/4.\)
Let \(H\) count the required ordered recombinations. Since each uses two current cells,
\(H\leq n^2.\)
The LP retains exactly
\(N=kn+c+Ks+1\)
variables. In particular,
\(N=O((k+K+1)\tau^2)=O(m\tau^2).\)
After converting each dummy equality into two inequalities, an upper bound on the number of constraint rows is
\(R\leq4kn+H+2n+2Ks+2.\)
The terms account respectively for private bounds and dummy requirements, recombinations, single options, public-price margins, and the two bounds on \(\delta\). Therefore
\(R=O(\tau^4+(k+K)\tau^2)=O(\tau^4+m\tau^2).\)
Each recombination row has at most \(2k+K+2\) variable occurrences; each single-option row has at most \(k+1\). The total number of coefficient occurrences is consequently \(O(m\tau^4)\).
All coefficients are rational. Derived coefficients use differences, while right-hand sides additionally use dot products of input vectors. Each such expression uses input rationals whose total binary encoding length is \(O(L)\). Forming common denominators, multiplying numerators, and adding the resulting terms therefore produces rationals with \(O(L)\) bits. The LP’s sparse encoding length is thus
\(S=O(m\tau^4L),\)
and its construction takes polynomial time in this bound.
The standard rational linear-programming theorem gives an algorithm that detects infeasibility or returns an exact rational optimum in time polynomial in the LP encoding length. It applies to systems with equalities, free variables, and lower-dimensional feasible sets after the usual polynomial-size transformations. See the [MIT notes on polynomial-time linear optimization](https://ocw.mit.edu/courses/6-251j-introduction-to-mathematical-programming-fall-2009/e13f5e6650f7be1e21101a2e7bd0d5b8_MIT6_251JF09_lec18.pdf).
Applying that theorem gives the claimed bit complexity
\(T=(m\tau^4L)^{O(1)}.\)
Equivalently, displaying the private and public dimensions separately, the running time is
\(\operatorname{poly}\bigl((k+1)\tau^2+K\tau^2,\ \tau^4+(k+K)\tau^2,\ L\bigr).\)
Because the support lists and goods vectors are explicitly encoded, their dimensions are bounded by the input length. Hence this is also \(L^{O(1)}\) time.
The self-recombination constraints are included. For a real current household, setting \(e=f\) gives
\(0\leq p_{ij}\cdot q_e+P_{ij}\cdot Q_e-y_{ij}.\)
Together with the input budget inequality, this forces budget exhaustion. A current single cell also exhausts its budget: its dummy requirement and its real partner’s single-option constraint give the reverse of the input budget inequality.
The numerical masses determine which cells belong to \(E\), but otherwise do not enter the feasibility constraints. No expansion into individual agents is required, and the algorithm has no dependence on the magnitudes of mass denominators beyond their contribution to \(L\).
This proves polynomial-time solvability for exactly the specified continuous system. The finite-individual interpretation in [Freer and Surana, Appendix B.2](https://repository.essex.ac.uk/39852/1/1-s2.0-S0899825624001805-main.pdf) supplies context; extending their rationalizability theorem to another population model is unnecessary for this complexity conclusion.
⟨structured verdict parsed — rendered above⟩
The proof is correct and resolves the stated continuous feasibility problem in polynomial time. No major or minor mathematical issues were found. The reduction preserves all constraints, handles strict positivity exactly, and has polynomial encoding length.
The adjudication concerns the displayed feasibility system. It does not require an extension of the finite-individual rationalizability theorem to flow populations.
The substitution \(r_e=q_e-x_e\), together with the coordinatewise bounds \(0\leq x_e\leq q_e\), is exactly equivalent to \(x_e,r_e\geq0\) and \(x_e+r_e=q_e\).
The dummy restrictions are also correct:
There is no current cell with two dummy partners because \(\pi_{\emptyset\emptyset}=0\). Thus the two dummy restrictions cannot conflict within a current cell.
Finding: Correct and reversible.
For a committed cell, \(v_e=1\), so the free variable \(t_e\) represents \(z_e\). For an uncommitted cell, \(v_e=0\), and fixing \(t_e=0\) represents \(v_ez_e\) regardless of the original \(z_e\).
All occurrences of \(z_e\) in the original constraints are through \(v_ez_e\). Consequently, choosing \(z_e=0\) for uncommitted cells loses no feasible solutions.
Finding: Correct, including uncommitted and single cells.
Setting \(B_{i\ell}=P_{i\ell}-A_{i\ell}\) transforms the two strict positivity requirements exactly into \(0<A_{i\ell,g}<P_{i\ell,g}\).
Substitution into the edge equality gives
\(p_{i\ell}\cdot(x_e+q_f-x_f)+A_{i\ell}\cdot(Q_e-Q_f)+P_{i\ell}\cdot Q_f-y_{i\ell}\),
which matches the prover’s expression. The signs and the use of \(q_f\) are correct.
All quantities multiplying unknowns are fixed input data. In particular, \(A_{i\ell}\cdot(Q_e-Q_f)\) is linear, not bilinear. Retaining one price vector per real type pair correctly enforces sharing across recombinations.
The edge variables impose no independent restriction beyond their defining equalities and inequalities, so eliminating them is reversible.
Both single-option inequalities are transformed correctly.
Finding: The reduced system is exactly equivalent to the original system.
The common margin construction is exact. Any original feasible solution has finitely many positive personalized-price coordinates. Their minimum, capped at \(1\), supplies a positive feasible value of \(\delta\).
Conversely, \(\delta>0\) and
\(\delta\leq A_{i\ell,g}\leq P_{i\ell,g}-\delta\)
ensure strict positivity of both personalized prices.
The empty-pair case is explicitly covered by taking the minimum over a set containing \(1\). No prescribed numerical tolerance or uniform margin across different instances is assumed.
Finding: Correct equivalence between original feasibility and the existence of an LP-feasible point with positive objective.
The bounds on \(x_e\), \(A_{i\ell}\), and \(\delta\) are immediate from the closed LP constraints.
Every retained \(t_e\) belongs to a committed cell. Such a cell has two real partners because single cells are uncommitted. Both single-option inequalities therefore apply.
The female single-option inequality yields
\(t_e\geq y_{\emptyset j}-p_{\emptyset j}\cdot(q_e-x_e)-P_{\emptyset j}\cdot Q_e\).
Since prices are positive and \(0\leq q_e-x_e\leq q_e\), the stated fixed lower bound follows.
The male single-option inequality similarly yields the stated fixed upper bound using \(x_e\leq q_e\).
Thus the feasible set is closed and bounded in a finite-dimensional space. If nonempty, it is compact, and maximizing \(\delta\) attains an optimum.
Finding: Correct. The three-step decision rule follows.
The support bounds \(n,s\leq ab\leq\tau^2/4\) are valid. Ordered recombinations, including self-recombinations, number at most \(n^2\).
The variable count \(N=kn+c+Ks+1\) is correct, with \(c\leq n\).
The row bound is also valid:
Hence the asserted bounds \(N=O(m\tau^2)\) and \(R=O(\tau^4+m\tau^2)\) follow. The coefficient-occurrence bound \(O(m\tau^4)\) is valid; repeated variables in a self-recombination can only reduce the number after collecting coefficients.
Finding: Correct.
Derived coefficients are differences of input rationals. Derived constants use sums and products from the stated dot products. The total bit length of the participating input data bounds the bit lengths of common denominators and resulting numerators by \(O(L)\).
Sparse row and variable indices require only logarithmic overhead, absorbed by \(L\) under explicit encoding. Thus \(S=O(m\tau^4L)\) is a valid upper bound.
The invoked theorem is the standard polynomial-time theorem for explicitly encoded rational linear programming. Its hypotheses are satisfied: the constructed constraints and objective are rational, the representation has polynomial size, and every feasible instance has an attained finite optimum. Free variables and lower-dimensional feasible sets are allowed through polynomial-size standard transformations.
The cited [MIT lecture notes](https://ocw.mit.edu/courses/6-251j-introduction-to-mathematical-programming-fall-2009/e13f5e6650f7be1e21101a2e7bd0d5b8_MIT6_251JF09_lec18.pdf) explicitly address arbitrary polyhedra, polynomial binary precision, and polynomial-time linear optimization.
The bounds \((m\tau^4L)^{O(1)}\) and the separately parameterized polynomial bound in \(k,K,\tau,L\) are therefore justified. Explicit input encoding also makes this polynomial in \(L\).
Finding: Correct application of the complexity theorem.
For a real current household, self-recombination cancels the potentials, private split, and personalized public prices. The resulting reverse budget inequality forces budget exhaustion together with the input budget inequality.
For a current single cell, the dummy restriction and the real partner’s single-option inequality likewise force budget exhaustion.
Masses affect the stated system through the support \(E\); their numerical values do not appear in its constraints. No population expansion is needed.
Finding: Correct. These observations introduce no additional assumptions.
No repair is required. The output establishes polynomial-time solvability of exactly the assigned continuous feasibility problem, with the claimed parameter and binary-input bounds.
⟨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.