Answer: For every fixed rational \(\alpha\in[0,1)\), clearing existence is \(\exists\mathbb{R}\)-complete and hence \(\mathrm{NP}\)-hard, even with equal masses. An exact decision algorithm runs in \((\tau+1)^{O(\tau)}L^{O(1)}\) bit operations.
Theorem 3 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateThe problem CDS-HasClearing(α, 1) is ∃R-complete for all α < 1.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given finitely many types \(T\) with positive rational masses μ_t summing to \(1\), per-institution external assets \(e_t\), and debt and CDS schedules \(d_{st}\) and \(h_{st\mid v}\) between types, with obligations allocated pro rata, decide whether there exists \(r\in[0,1]^T\) satisfying the paper's clearing equations for fixed α<1 and β=1. Here \(q_{st}(r)=d_{st}+\sum_v(1-r_v)h_{st\mid v}\), \(L_s(r)=\sum_t q_{st}(r)\), and \(I_t(r)=\sum_s(\mu_s/\mu_t)r_s q_{st}(r)\); type \(t\)'s assets are \(A_t=e_t+I_t\) and its post-default-cost assets are \(A'_t=\alpha e_t+I_t\).
A society is given by its support: a nonempty list \(T\) of \(\tau\) institution types with positive binary rational masses \(\mu_t\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
Each type has per-institution external assets \(e_t\geq0\), debt notionals \(d_{st}\geq0\), and CDS notionals \(h_{st\mid v}\geq0\), all binary rationals. Debt requires \(s\neq t\); CDSs require pairwise distinct \(s,t,v\); all other entries are zero. Require \(e_t>0\) or \(\sum_u d_{tu}>0\) for every \(t\). Fix a rational \(\alpha\in[0,1)\) and \(\beta=1\).
The schedules specify each writer institution's total obligations to a recipient type, distributed uniformly over that type's mass. All institutions of type \(t\) share recovery rate \(r_t\).
For \(r\in[0,1]^T\), define \(q_{st}(r)=d_{st}+\sum_v(1-r_v)h_{st\mid v}\), \(L_s(r)=\sum_tq_{st}(r)\), and \(I_t(r)=\sum_s(\mu_s/\mu_t)r_sq_{st}(r)\).
Set \(A_t(r)=e_t+I_t(r)\) and \(A'_t(r)=\alpha e_t+I_t(r)\). A vector is clearing precisely when every \(t\) satisfies \(r_t=1\) if \(A_t(r)\geq L_t(r)\), and \(r_t=A'_t(r)/L_t(r)\) otherwise. In particular, zero liabilities force \(r_t=1\), and equality belongs to the solvent branch.
For each fixed rational \(\alpha\in[0,1)\), is deciding whether such a clearing vector exists in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard? State running times in \(\tau\) and the total input bit length \(L\); there is no separate alternative-count parameter \(m\).
For finite networks of individual banks under the same nondegeneracy condition, exact clearing existence with \(\beta=1\) is \(\exists\mathbb{R}\)-complete for every fixed \(\alpha<1\). [Discrete clearing-existence result](https://arxiv.org/html/2409.18717#S4)
No result settling the specified mass model was located.
For every fixed rational \(\alpha\in[0,1)\), deciding clearing existence in the specified mass model is \(\exists\mathbb{R}\)-complete, and therefore \(\mathrm{NP}\)-hard. Hardness already holds when every mass equals \(1/\tau\).
An exact decision algorithm runs in \((\tau+1)^{O(\tau)}L^{O(1)}\) bit operations. Thus the problem is polynomial-time solvable for each fixed support size, but a polynomial-time algorithm for unrestricted support size would imply \(\mathrm{P}=\mathrm{NP}\).
Fix a valid mass-model instance. Construct a finite network with one bank for each \(t\in T\), external assets and notionals
\[ \widehat e_t=\mu_t e_t,\qquad \widehat d_{st}=\mu_s d_{st},\qquad \widehat h_{st\mid v}=\mu_s h_{st\mid v}. \]
Here and below these formulas use the given per-writer interpretation of the schedules.
For any recovery vector \(r\in[0,1]^T\), the finite network’s liability from bank \(s\) to bank \(t\) is
\[ \widehat q_{st}(r) =\widehat d_{st}+\sum_v(1-r_v)\widehat h_{st\mid v} =\mu_s q_{st}(r). \]
Consequently, its total liabilities and incoming payments satisfy
\[ \widehat L_t(r)=\mu_t L_t(r), \qquad \widehat I_t(r) =\sum_s r_s\widehat q_{st}(r) =\sum_s\mu_s r_s q_{st}(r) =\mu_t I_t(r). \]
Its assets before and after default costs therefore satisfy
\[ \widehat A_t(r)=\mu_t A_t(r), \qquad \widehat A'_t(r)=\mu_t A'_t(r), \]
where both models use the same \(\alpha\) and \(\beta=1\).
Since \(\mu_t>0\), we have
\[ \widehat A_t(r)\geq\widehat L_t(r) \quad\Longleftrightarrow\quad A_t(r)\geq L_t(r). \]
On the default branch, \(A_t(r)<L_t(r)\) implies \(L_t(r)>0\), because assets are nonnegative. Hence
\[ \frac{\widehat A'_t(r)}{\widehat L_t(r)} =\frac{\mu_t A'_t(r)}{\mu_t L_t(r)} =\frac{A'_t(r)}{L_t(r)}. \]
These identities prove that the two instances have exactly the same clearing vectors. They also preserve equality on the solvent branch and zero liabilities.
All required restrictions survive the construction. Multiplication by positive masses preserves nonnegativity and all forbidden zero entries. Furthermore,
\[ \widehat e_t>0\quad\Longleftrightarrow\quad e_t>0, \qquad \sum_u\widehat d_{tu}>0 \quad\Longleftrightarrow\quad \sum_u d_{tu}>0. \]
Thus nondegeneracy is preserved. The construction uses exactly \(\tau\) banks and has polynomial bit complexity: multiplying binary rationals increases their encoding lengths by at most the sum of the operand lengths.
We use the supplied discrete theorem precisely as follows: for every fixed rational \(\alpha<1\), exact clearing existence in nondegenerate finite networks with \(\beta=1\) is \(\exists\mathbb{R}\)-complete. Its contract restrictions, nondegeneracy condition, and clearing branches agree with those in this question. This is Theorem 3 of [Dohn, Hansen, and Klinkby](https://arxiv.org/html/2409.18717#S4).
Given such a finite network with \(\tau\) banks, create one type per bank and set
\[ \mu_t=\frac1\tau \]
for every type. Copy each bank’s external assets, debt notionals, and CDS notionals unchanged.
The masses are positive binary rationals and sum to \(1\). The copied data satisfy the distinctness and nondegeneracy requirements. For every pair of types, \(\mu_s/\mu_t=1\), so incoming payments in the mass model become
\[ I_t(r)=\sum_s r_s q_{st}(r), \]
exactly the incoming payments in the original finite network. Liabilities, external assets, and both clearing branches likewise coincide. Therefore, for every \(r\),
\[ r\text{ clears the finite network} \quad\Longleftrightarrow\quad r\text{ clears the mass-model instance}. \]
This is a polynomial-time many-one reduction. The mass fields add only \(O(\tau\log(\tau+1))\) bits; copying or explicitly padding the contract tables also takes polynomial time.
The cited theorem therefore establishes \(\exists\mathbb{R}\)-hardness, including \(\alpha=0\), already on equal-mass instances. Since \(\mathrm{NP}\subseteq\exists\mathbb{R}\), it establishes the requested \(\mathrm{NP}\)-hardness.
For completeness, we give a direct existential-real formulation that preserves the strict default condition.
Use the finite-network quantities from Section 1. Clearing existence is equivalent to the truth of
\[ \exists(r_t)_{t\in T}\; \bigwedge_{t\in T} \left[ 0\leq r_t\leq1 \;\land\; \left( \bigl(r_t=1\land\widehat A_t(r)-\widehat L_t(r)\geq0\bigr) \;\lor\; \bigl( \widehat A_t(r)-\widehat L_t(r)<0 \land r_t\widehat L_t(r)-\widehat A'_t(r)=0 \bigr) \right) \right]. \]
To verify the default branch, note that its strict inequality forces \(\widehat L_t(r)>0\). Dividing its polynomial equality by that positive quantity gives the required recovery ratio. Conversely, every clearing vector satisfies the corresponding branch. At equality, only the solvent branch applies. When liabilities vanish, nonnegative assets exclude the default branch and force \(r_t=1\).
Each \(\widehat q_{st}\) and \(\widehat L_t\) is affine in \(r\). Incoming payments are sums of products \(r_s\widehat q_{st}(r)\), so \(\widehat A_t\) and \(\widehat A'_t\) have degree at most \(2\). The polynomial \(r_t\widehat L_t-\widehat A'_t\) also has degree at most \(2\).
The formula therefore has exactly \(\tau\) variables, \(O(\tau)\) polynomial predicates, and maximum degree \(2\). Its rational coefficients can be computed and converted to integer coefficients in polynomial time. Multiplication by positive common denominators preserves every equality and inequality, including strict inequalities, and produces coefficient bit lengths polynomial in \(L\). This proves membership in \(\exists\mathbb{R}\).
The standard singly exponential decision bound for existential-real formulas with \(k\) variables, \(p\) polynomial predicates, maximum degree \(d\), and coefficient bit length \(B\) is \((pd)^{O(k)}B^{O(1)}\), with a polynomial factor for the Boolean formula’s length. See [Renegar’s decision theorem](https://doi.org/10.1016/S0747-7171(10)80003-3) and the complexity discussion in [Vorobjov’s notes](https://arxiv.org/pdf/2112.00456).
Here all its hypotheses hold: the coefficients are integers, the formula is existential, and its predicates include permitted equalities and inequalities. Substituting \(k=\tau\), \(p=O(\tau)\), \(d=2\), and \(B=L^{O(1)}\) gives
\[ (\tau+1)^{O(\tau)}L^{O(1)} \]
bit operations, including polynomial preprocessing. There is no separate alternative-count parameter: the number of recovery variables is precisely the support size \(\tau\).
⟨structured verdict parsed — rendered above⟩
The prover resolves the assigned task. The argument is correct and rigorous: for every fixed rational \(\alpha\in[0,1)\), the specified mass-model problem is \(\exists\mathbb{R}\)-complete, hence \(\mathrm{NP}\)-hard. The stated running-time bound is also justified. I found no major or minor mathematical issues.
The scaling uses the writer’s mass for each obligation and the recipient’s mass for external assets:
\(\widehat d_{st}=\mu_s d_{st}\), \(\widehat h_{st\mid v}=\mu_s h_{st\mid v}\), and \(\widehat e_t=\mu_t e_t\). This agrees with the schedules’ per-writer interpretation.
Each displayed identity checks correctly. In particular, summing outgoing obligations gives \(\widehat L_t=\mu_t L_t\), while summing incoming payments gives \(\widehat I_t=\mu_t I_t\). Consequently, both pre-default and post-default assets scale by \(\mu_t\). There is no missing mass factor.
Positivity of \(\mu_t\) preserves the comparison between assets and liabilities, including equality. On the default branch, nonnegative assets and \(A_t<L_t\) imply \(L_t>0\), so cancellation in the recovery ratio is legitimate.
When liabilities vanish, the default inequality is impossible and the solvent branch forces recovery \(1\). Thus the correspondence preserves precisely the clearing definition in the task, including its boundary convention. These arguments hold for every \(r\in[0,1]^T\), establishing equality of the entire sets of clearing vectors.
Positive scaling preserves nonnegative notionals, forbidden zero entries, and both alternatives in the nondegeneracy condition. The construction adds no banks: its size is exactly \(\tau\).
The rational-arithmetic encoding claim is valid. Products of binary-encoded rationals have encoding lengths bounded by the sums of the operand lengths, up to routine encoding overhead. Reusing masses across contract entries still produces only polynomial total output length and polynomial construction time.
The cited theorem is correctly identified. Theorem 3 concerns clearing existence in nondegenerate finite networks with \(\beta=1\), for every \(\alpha<1\). The paper’s parameter domain, distinctness restrictions, nondegeneracy definition, and exact clearing branches match those required here. In particular, the theorem includes \(\alpha=0\); no positive lower bound on \(\alpha\) is required. [Dohn, Hansen, and Klinkby, Definitions 1–2 and Theorem 3](https://arxiv.org/html/2409.18717#S4).
The prover therefore applies the cited theorem with its hypotheses satisfied.
Assigning one type to each bank and taking \(\mu_t=1/\tau\) produces positive rational masses summing to \(1\). Their binary numerator-denominator representations require \(O(\log(\tau+1))\) bits each.
Copying the financial data preserves every input restriction. Because every mass ratio equals \(1\), the incoming-payment expressions coincide exactly with those of the original network. Liabilities and external assets also coincide, so both clearing branches agree for every recovery vector. The claimed polynomial-time many-one reduction and its direction are correct.
Combining this reduction with the cited theorem establishes \(\exists\mathbb{R}\)-hardness. The inference to \(\mathrm{NP}\)-hardness from \(\mathrm{NP}\subseteq\exists\mathbb{R}\) is valid.
The formula quantifies precisely the recovery variables and explicitly restricts them to \([0,1]\). Its disjunction enforces the solvent branch at equality and the default branch only under the strict asset deficit.
The polynomial equality on the default branch is equivalent to the recovery ratio because the accompanying inequality guarantees a positive denominator. Zero liabilities cannot create spurious solutions.
The degree calculation is correct: liabilities are affine, incoming payments have degree at most \(2\), and multiplying liabilities by one recovery variable still gives degree at most \(2\). The formula has \(O(\tau)\) predicates and polynomial encoding length. Clearing positive rational denominators preserves all predicate signs and yields polynomial coefficient bit lengths. Membership in \(\exists\mathbb{R}\) follows.
The stated existential-real decision bound applies to integer polynomial predicates, including strict inequalities and Boolean combinations. The cited complexity discussion supports singly exponential dependence on the variable count and polynomial dependence on coefficient bit length. [Vorobjov’s notes, Sections 2 and 5](https://arxiv.org/pdf/2112.00456).
Substituting the prover’s parameters gives \((\tau+1)^{O(\tau)}L^{O(1)}\) bit operations. Polynomial preprocessing is absorbed in this bound. For fixed \(\tau\), it is polynomial in \(L\). For unrestricted \(\tau\), the established hardness gives the stated consequence for a hypothetical polynomial-time algorithm.
No repair or additional clarification is necessary. The output establishes the requested hardness classification and supplies the requested dependence on \(\tau\) and \(L\).
⟨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.