Answer: —
Theorem 7 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateLet P = (P(M), P(N), P(L)) be the true preference profile. Let P ′(L) be a strong Nash equilibrium, and μ be the induced matching by (P(M), P(N), P ′(L)). P ′(L) is a super-strong Nash equilibrium if and only if for all w ∈L and m ∈P(w) with m ≻w μ(w), there exists one manipulator w′ ∈L such that w′ becomes unmatched under preference lists (P(M), P(N), P ′ w,m(L)).
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given rational masses on finitely many types on each side of a two-sided matching market, strict rankings of opposite-side types, a set of manipulable types, and a candidate report profile promised to be a strong equilibrium, is that profile super-strong under mass deferred acceptance? Here mass deferred acceptance lets a type split at a preference cutoff; a deviation may split manipulable mass among reports. The profile is super-strong exactly when no positive-mass coalition can deviate so that, under some coupling of its old and new partner-type assignments respecting true rankings, no deviator is worse off and positive mass is strictly better off.
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible rankings. Let \(M,W\) be the nonempty proposing and receiving supports, with total mass \(1\) on each side, \(m=\max\{|M|,|W|\}\), and \(L\) the total input bit length.
Each type has a true strict ranking of opposite-side types and the unmatched outcome \(\bot\); types above \(\bot\) are acceptable. Only types in a specified set \(D\subseteq W\) may manipulate. A report is any strict ordered list of any subset of \(M\), including the empty list; omitted types are rejected. Other types report truthfully.
The candidate profile specifies one report per receiving type. After a deviation, receiving mass is grouped into classes \((w,r)\) by true type and report, with identical classes merged. Men rank classes first by their true ranking of \(w\), then lexicographically by the report list using the fixed input enumeration of \(M\); a shorter prefix precedes its extension.
Mass deferred acceptance is the limit of synchronous men-proposing deferred acceptance on these classes: free mass proposes to its next unrejected acceptable class; each class holds its capacity of the most preferred proposer-type mass according to its report, splitting mass at the cutoff and rejecting the rest. Exhausted proposer mass remains unmatched.
A coalition may select any positive submass of manipulable types, including selection according to old partner type, and divide it among reports using arbitrary nonnegative real masses. All mass outside the coalition retains its report. Within each resulting class, coalition mass receives the class's partner-type distribution proportionally to its share of that class.
Compare the selected coalition's old and new assignment measures, including \(\bot\), by a coupling separately within each true receiving type. A weak improvement coupling assigns no mass to a worse new partner; a strict improvement coupling assigns almost all coalition mass to strictly better new partners.
The candidate is promised strong: no positive-mass coalition has a strict improvement coupling. It is super-strong exactly when no positive-mass coalition has a weak improvement coupling assigning positive mass to strictly better new partners.
Is deciding whether this promised strong profile is super-strong solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?
For finite agents with arbitrary incomplete receiving-side reports, the corresponding promised equilibrium test takes \(O(n^4)\) time when each side has \(n\) agents ([Deng, Shen, and Tang](https://www.weiran-shen.info/page_files/coalition_manipulation_of_gale_shapley_algorithm.pdf)).
For a different fractional model with indifferences, a stable allocation satisfying fairness on both sides can be computed in polynomial time ([Cookson and Shah](https://www.cs.toronto.edu/~nisarg/papers/dfda.pdf)); this result does not establish the complexity of the specified mass equilibrium test.
I do not establish polynomial-time solvability or NP-hardness of the requested promised problem.
The results proved below advance the unresolved search problem:
The missing step is a polynomial bound or an efficiently searchable description of the reports needed by a profitable deviation.
Write $a_i$ for the mass of proposing type $i$. For a fixed reported profile, let $C$ be its positive-capacity receiving classes, and write $q_c$ for the capacity of class $c$.
Construct a bipartite graph with proposing types on one side and receiving classes on the other. Include the edge $(i,c)$ exactly when:
Proposing types order their incident classes using the task’s true-type order and lexicographic report order. Receiving classes order incident proposing types according to their reports. Thus both vertex orders are strict.
For an allocation $X$, feasibility means
$$
X_{ic}\geq 0,\qquad
\sum_c X_{ic}\leq a_i,\qquad
\sum_i X_{ic}\leq q_c.
$$
For an included edge $(i,c)$, define
$$
P_{ic}(X)
=
a_i-\sum_{d:\,d\succeq_i c}X_{id},
$$
and
$$
Q_{ic}(X)
=
q_c-\sum_{j:\,j\succeq_c i}X_{jc}.
$$
The first quantity is the proposing mass assigned below $c$, including unmatched mass. The second is the capacity assigned below $i$, including vacant capacity. Both are nonnegative.
Consequently, $(i,c)$ blocks exactly when
$$
P_{ic}(X)>0
\quad\text{and}\quad
Q_{ic}(X)>0.
$$
Indeed, under these two inequalities, a sufficiently small positive mass can be moved onto $(i,c)$ by replacing inferior assignments or using unmatched mass and vacant capacity. Conversely, an improving increase on that edge requires both quantities to be positive. Stability therefore has the exact description
$$
P_{ic}(X)=0
\quad\text{or}\quad
Q_{ic}(X)=0
\qquad\text{for every included edge }(i,c).
$$
Known stable-allocation result used. On a bipartite graph with strict preferences, real vertex quotas, and edge capacities, batch Gale–Shapley returns the unique allocation that lexicographically maximizes each proposing vertex’s allocation vector among stable allocations, independently of proposal order. A strongly polynomial augmentation algorithm computes that allocation. Its implementation without dynamic trees uses polynomially many additions, subtractions, comparisons, and minima. These statements are given in Lemmas 1 and 5 and Section 3 of [Dean and Munshi, *Faster Algorithms for Stable Allocation Problems*](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf).
Here are the hypothesis checks and the connection to the specified mechanism.
First, set the capacity of edge $(i,c)$ to $\min(a_i,q_c)$. This introduces no additional restriction: every feasible allocation already satisfies that bound. Unmatched mass and vacant capacity can be represented by a dummy receiver and a dummy proposer, respectively, ranked last by real vertices.
Second, synchronous DA has the same aggregate outcome as batch DA. To see the relevant serialization, fix a synchronous round and process its incoming proposals sequentially, while delaying newly rejected mass until the next round. At each receiving class, sequentially retaining its best mass produces exactly the result of retaining its best mass from all incoming proposals together.
A class that has rejected positive mass of type $i$ cannot subsequently increase its holding of $i$: at the rejection it is full with types ranked at least as highly as $i$, and its cumulative holdings of better types never decrease. Subsequent proposals of $i$ to that class therefore produce no net increase and may be skipped. After skipping these futile proposals, the serialization is a valid batch-DA execution on the graph above. Proposal-order independence identifies its outcome with the specified synchronous outcome.
It follows that a fixed rational profile with $K$ classes has its actual DA allocation computable in time polynomial in $m,K$ and its binary encoding length.
The bit complexity is also polynomial. A common denominator for the rational input has bit length at most the total input length. Additions, subtractions, and minima preserve that denominator. Polynomially many such operations produce intermediate numerators of polynomial bit length.
Fix the identities of the $K$ positive classes and allow their capacities to vary.
Choose a deterministic implementation of the augmentation algorithm. It has a polynomial bound
$$
T=\operatorname{poly}(m,K)
$$
on its arithmetic operations and comparisons.
Along any particular execution branch, every intermediate numerical quantity is an affine function of the capacities, with rational coefficients. This follows inductively:
Every condition defining that branch is therefore a rational linear equality or inequality. The output allocation is affine on the branch. Moreover, the coefficients have bit length polynomial in $m,K,L$: each addition or subtraction increases coefficient bit length by at most a constant, after using a common denominator for the fixed rational constants.
Thus, for fixed class identities, the DA map has a finite description by rational linear branches.
Let $A_w(x)$ denote the candidate assignment mass of receiving type $w$ at partner $x$, where $x$ ranges over $M\cup\{\bot\}$. Let $b_w$ be its total mass.
Suppose some $w\in D$ receives positive candidate mass at a partner strictly below $\bot$.
Select positive mass from that old partner category and let it report the empty list. Its new class rejects every proposer, so all selected mass becomes unmatched. Every selected member strictly improves. This contradicts the strong promise.
Hence, in a promised strong profile, manipulable mass receives only truly acceptable partners or $\bot$.
Proposition. If a manipulable type has at least two old partners with positive mass, the candidate is not super-strong.
Proof. Let $p$ be the worst partner with positive mass for such a type $w$, and select its entire old mass
$$
c=A_w(p)>0.
$$
Have that selected mass retain the candidate report. The aggregate profile and DA allocation remain unchanged. Identical classes merge, and proportional sharing gives the selected mass the new assignment measure
$$
t(x)=\frac{c}{b_w}A_w(x).
$$
Its old assignment is entirely $p$. Every partner in the support of $t$ is weakly preferred to $p$, and
$$
\sum_{x\succ_w p}t(x)
=
\frac{c}{b_w}\sum_{x\succ_w p}A_w(x)>0.
$$
Pairing the old partner $p$ with this new distribution is a profitable weak improvement coupling. This uses the task’s express permission to select by old partner and retain an existing report. $\square$
Accordingly, the remaining case has a unique old partner $p_w$ for every $w\in D$.
For a post-deviation class $c=(w,r)$, define its assignment measure by
$$
Z_c(i)=X_{ic}\quad(i\in M),
\qquad
Z_c(\bot)=q_c-\sum_iX_{ic}.
$$
Call $c$ safe if
$$
Z_c(x)=0
\qquad\text{for every }x\prec_w p_w.
$$
Define its strictly improving mass by
$$
g_c=\sum_{x\succ_w p_w}Z_c(x).
$$
These conditions and quantities are linear in $q$ and $X$.
Because the selected old assignment of type $w$ is entirely $p_w$, a weak improvement coupling exists exactly when its new measure gives zero mass to partners below $p_w$. Such a coupling has positive strictly improving mass exactly when its new measure gives positive mass to partners above $p_w$.
Let $r_w^0$ be the candidate report.
Lemma. Any profitable weak deviation can be replaced, without changing its aggregate profile, by one in which the coalition contains:
Every included class is safe.
Proof. Every changed-report class consists entirely of coalition mass: mass outside the coalition must retain its report.
Suppose positive coalition mass shares the original-report class. Its share of that class’s assignment measure is a positive scalar multiple of $Z_c$, by proportional sharing. Weak improvement is therefore possible only if $c$ is safe.
Enlarge the coalition to include the whole capacity of each such original-report class. This does not change any report or class capacity. The additionally selected old mass also had partner $p_w$, so safety guarantees weak improvement for it. Enlarging the coalition cannot remove any strictly improving mass.
Selection is feasible: without the original-report class, the selected mass of type $w$ is the total changed-report capacity; with it, the selected mass is $b_w$. Purity permits either selection from the old assignment. $\square$
Compute its DA allocation using Section 2.
If any changed-report class is unsafe, that aggregate profile cannot be realized by a weakly improving coalition.
Otherwise, include every changed-report class and every safe original-report class. A profitable weak coalition realizes the profile exactly when
$$
\sum_{\substack{w\in D,\ r\neq r_w^0}}g_{(w,r)}
+
\sum_{\substack{w\in D:\\(w,r_w^0)\text{ is present and safe}}}
g_{(w,r_w^0)}
>0.
$$
Necessity follows from the lemma. For sufficiency, select precisely those whole classes; all their mass weakly improves, and the displayed inequality supplies positive strictly improving mass.
This test takes polynomial time in $m,K$ and the supplied rational profile’s encoding length. Unlike the conditional test in the notes, it computes and authenticates the DA allocation itself.
Theorem. Suppose every manipulable type’s old assignment is pure. If a profitable weak deviation uses $K$ positive classes with arbitrary real capacities, there is a profitable weak deviation using the same positive classes whose capacities, allocation, and coalition masses have encoding length polynomial in $m,K,L$.
Proof.
Fix the class identities used by the real deviation. Apply the preceding lemma, and fix which original-report classes are included in its coalition.
Also fix the execution branch of the deterministic DA algorithm at the real capacity vector. Section 2 supplies:
Impose the following additional conditions:
$$ \sum_{c:\,\operatorname{type}(c)=w}q_c=b_w. $$
After substituting $X(q)$, all these conditions are rational linear equalities, weak inequalities, or strict inequalities. Their number and coefficient bit lengths are polynomial in $m,K,L$. The original real vector satisfies them.
It remains to prove that this linear system has a small rational solution.
Write every strict inequality as
$$
\ell_j(q)>0.
$$
Introduce a variable $\varepsilon$ and replace those inequalities by
$$
\ell_j(q)\geq\varepsilon,
\qquad
0\leq\varepsilon\leq1.
$$
Retain all equalities and weak inequalities, and maximize $\varepsilon$.
At the original real solution, all finitely many strict margins are positive. Choosing $\varepsilon$ smaller than their minimum gives a feasible point with $\varepsilon>0$. Thus the optimum is positive.
The feasible region is compact: capacities are nonnegative and their typewise totals are fixed, so every capacity lies in $[0,1]$; also $\varepsilon\in[0,1]$. A positive optimum is attained at a rational vertex.
For completeness, its encoding length is polynomial. If there are $d$ variables and coefficients have bit length at most $B$, clear denominators in a set of $d$ independent active constraints. The resulting integer coefficients have bit length polynomial in $d,B$. Cramer’s rule and
$$
|\det H|\leq d!\bigl(\max_{u,v}|H_{uv}|\bigr)^d
$$
then bound every vertex numerator and denominator by polynomial bit length in $d,B$.
The resulting rational capacities remain on the fixed branch, remain positive, and satisfy safety and positive gain. Their affine DA allocation also has polynomial bit length. Selecting the prescribed whole classes gives rational coalition masses. Since each type’s old partner is pure, coupling that partner to the rational new measure directly supplies the required coupling. $\square$
Mixed old assignments already have rational witnesses by Section 3: the candidate allocation is rational, and the no-report-change construction uses rational selected masses.
Therefore arbitrary real masses do not enlarge the existence question beyond rational deviations. Crucially, the encoding bound is polynomial in the number $K$ of reports used, which has not been bounded polynomially in the original input.
Let $p=|M|$. The number of possible reports is
$$
R_p=\sum_{\ell=0}^{p}\frac{p!}{(p-\ell)!}.
$$
Thus the total number of possible receiving classes is at most
$$
K_{\max}=|W|R_p.
$$
The following algorithm is exact:
Strict feasibility is decided by the $\varepsilon$ construction.
If the algorithm finds a feasible system, its solution supplies an actual profitable deviation. Conversely, every profitable real deviation has a support, a whole-class coalition choice, and an execution branch represented in the enumeration. Its corresponding system is feasible.
Because $K_{\max}$ depends only on $m$, and the arithmetic branch bound is polynomial in $m,K_{\max}$, this gives running time
$$
f(m)\operatorname{poly}(L)
$$
for a computable function $f$. In particular, the problem is polynomial-time decidable when $m$ is fixed.
This is not polynomial time in $m,\tau,L$. The enumeration includes a factorial report universe and many arithmetic branches.
Theorem. If every type in $D$ reports the empty list in the candidate, then a promised strong candidate is super-strong.
Proof.
Every manipulable type is initially unmatched. Suppose a profitable weak deviation exists.
For every changed-report class $c=(w,r)$ with $w\in D$, let
$$
T_c=\sum_iX_{ic}
$$
be its final matched mass. Since the old partner is $\bot$, weak improvement implies that every matched partner in such a class is truly acceptable. Profitability implies
$$
\sum_cT_c>0.
$$
Replace each changed-report capacity $q_c$ by $T_c$, removing the class if $T_c=0$. Return the removed capacity to that true type’s empty-report class.
We verify that the matched allocation $X$ is preserved.
If $T_c<q_c$, class $c$ is vacant at termination. A class’s total held mass never decreases: it accepts incoming mass until full, and thereafter replaces rejected mass while remaining full. Therefore $c$ was never full during the original execution. It never rejected a proposer listed in its report.
All listed proposing mass it received remained held, and its cumulative amount was exactly $T_c$. Reducing its capacity to $T_c$ consequently causes no additional rejection at any point of that execution. Classes with $T_c=q_c$ are unchanged.
The enlarged empty-report classes accept no proposer. Their insertion or enlargement adds only futile proposals. By replaying the original batch execution, and using proposal-order independence from Section 2, the new profile has the same matched allocation $X$.
Now select, from the old unmatched mass of each manipulable type, exactly the capacities $T_c$, and assign them to their respective changed reports. Each selected class is completely matched, and every partner it receives is strictly above $\bot$. Thus almost all selected mass strictly improves. The selected coalition has positive mass because $\sum_cT_c>0$.
This contradicts the strong promise. Hence no profitable weak deviation exists. $\square$
The new results remove two obstacles: actual DA outcomes can be computed directly from binary rational capacities, and arbitrary-real profitability has rational witnesses.
They leave the central combinatorial obstacle unresolved. A witness’s size is polynomial in its number of report classes, but that number may range over a factorial report universe. No polynomial bound on necessary report support, polynomial search procedure, or promise-preserving hardness reduction is proved here.
⟨structured verdict parsed — rendered above⟩
Result: partial. The output establishes substantive intermediate results, but it does not answer whether the promised equilibrium test is polynomial-time solvable or NP-hard. It accurately acknowledges this limitation. I found no false central mathematical step; the main issue is the unresolved target, with one minor omission in the application of the stable-allocation theorem.
The requested classification concerns running time polynomial in $m,\tau,L$, or an NP-hardness result satisfying the strong-profile promise.
The output establishes neither. Its running-time bound
$$ f(m)\operatorname{poly}(L) $$
permits superpolynomial dependence on $m$. Its rational-witness bound is polynomial in the number $K$ of receiving classes, which is not bounded polynomially in the original input.
Major issue — unresolved target. Sections 1 and 8 expressly leave the required classification open. This is an acknowledged scope limitation, rather than a misleading claim of completeness.
Required additional work: Establish one of the requested complexity conclusions. A polynomial bound on $K$ alone would not finish the polynomial-time direction; an efficient search or decision procedure would still be necessary.
The edge condition correctly encodes mutual reported acceptability: the proposer must truly accept the receiving type, and the receiving report must list the proposer.
Deleting classes that immediately reject a proposer does not alter successful assignments. The incident preference orders are strict because identical receiving classes are merged and the task specifies a strict lexicographic order among distinct reports.
The definitions
$$ P_{ic}(X)=a_i-\sum_{d:\,d\succeq_i c}X_{id}, \qquad Q_{ic}(X)=q_c-\sum_{j:\,j\succeq_c i}X_{jc} $$
correctly measure inferior allocations together with unassigned mass or vacant capacity. Feasibility makes both quantities nonnegative.
Their simultaneous positivity is exactly the condition for a mutually improving positive increase on the edge. The introduced edge bound $\min(a_i,q_c)$ causes no discrepancy: simultaneous positivity implies
$$ X_{ic}<a_i \quad\text{and}\quad X_{ic}<q_c, $$
so that bound cannot prevent the increase.
Thus the stated stability disjunction is correct.
The citation supports the substantive theorem invoked. Lemma 1 gives proposal-order independence and the unique proposer-optimal allocation, including real data. Lemma 5 identifies the augmentation algorithm’s output with that allocation. Section 3 also supports a polynomial implementation without dynamic trees using the arithmetic operations needed here. See [Dean and Munshi, *Faster Algorithms for Stable Allocation Problems*](https://people.computing.clemson.edu/~bcdean/stable_alloc.pdf).
Minor issue — incomplete dummy specification. The cited formulation fills vertex quotas through dummy elements. The output mentions a dummy proposer and receiver ranked last by real vertices, but does not specify their quotas, incident edge capacities, or their own strict preference orders.
Minimum clarification: Specify this augmentation sufficiently to verify the cited theorem’s feasibility hypotheses and explain that its restriction to real edges preserves the intended DA allocation. This is a routine modeling clarification.
The serialization argument is sound. Sequential retention of the best available mass gives the same holding as simultaneous retention, and newly rejected mass can be delayed until the next round.
The rejection monotonicity used here is valid: after positive rejection of proposer type $i$, the class remains full with mass ranked at least as highly as $i$. Its total holding of types strictly above $i$ cannot decrease. Later proposals of $i$ cannot produce a net increase.
Skipping these futile proposals therefore preserves the aggregate trajectory. The cited proposal-order independence then identifies the output with the specified mechanism.
The rational arithmetic argument is valid. A common denominator has polynomial bit length; the stated operations preserve it, and polynomially many operations produce numerators of polynomial bit length.
For fixed class identities, fixing all comparison outcomes and minimum choices makes every numerical quantity affine in the capacities. This includes the initial edge-capacity minima. Branch conditions are rational linear conditions, and their coefficient lengths remain polynomial.
No substantive gap appears in these conclusions, subject to the dummy specification above.
This argument is correct. Selecting positive mass assigned strictly below $\bot$ and moving it to an empty report makes that selected mass unmatched. Every selected member strictly improves, contradicting the strong promise.
The conclusion concerns manipulable types only, as stated.
The proposition is correct under the task’s explicit selection and proportional-sharing rules.
Selecting the old mass at the worst positive-mass partner and retaining the candidate report leaves the aggregate profile unchanged. The selected mass then receives
$$ t(x)=\frac{A_w(p)}{b_w}A_w(x). $$
This measure has no partner worse than $p$ and has positive mass strictly above $p$. The selected coalition therefore has the required profitable weak coupling.
The argument covers mixed assignments involving $\bot$ as well as assignments involving only proposer types. It does not assert a strict improvement coupling for all selected mass.
When the old assignment of each manipulable type is concentrated at $p_w$, the coupling criterion is correctly reduced to absence of new mass below $p_w$, with positive mass above $p_w$ for profitability.
The normal-form lemma is valid:
Purity of the old assignment justifies the enlarged selection.
The supplied-profile test consequently has correct necessity and sufficiency in the pure-old-assignment case. Positive gain ensures that the selected coalition has positive mass. The polynomial-time bound is appropriately measured against the supplied profile’s size, including $K$.
This does not itself provide a polynomial-time search over deviations.
The rational-replacement proof is sound.
Fixing the real deviation’s support, coalition choice, and algorithm branch yields rational linear constraints. Safety is linear after substituting the affine allocation, and profitability is a strict linear inequality.
The $\varepsilon$ construction correctly handles all strict inequalities simultaneously. Finitely many positive margins admit a common positive $\varepsilon$. The capacity totals and nonnegativity bound every capacity in $[0,1]$, making the resulting feasible region compact.
A positive optimum can therefore be attained at a rational vertex. The active-constraint and determinant argument supplies polynomial encoding length in the stated parameters. The allocation and whole-class coalition masses inherit that bound.
The mixed-assignment construction also has rational data, because the candidate’s rational DA allocation supplies its selected mass and new measure.
The important limitation is correctly stated: the bound depends polynomially on $K$, not necessarily on the original input size.
The report count
$$ R_p=\sum_{\ell=0}^{p}\frac{p!}{(p-\ell)!} $$
is correct for strict ordered lists of subsets, including the empty list. Hence $K_{\max}=|W|R_p$ is a valid upper bound.
The enumeration covers every possible profitable deviation: its positive support, normal-form coalition choice, and deterministic algorithm branch all occur among the enumerated choices.
Conversely, a feasible enumerated system specifies actual capacities on that branch, safe coalition classes, and positive gain. Thus it certifies a profitable deviation.
The bound $f(m)\operatorname{poly}(L)$ is justified: the support universe and branch-operation bound depend only on $m$, while the rational linear feasibility problems have polynomial dependence on coefficient encoding length.
This establishes an exact algorithm and polynomial-time decidability for fixed $m$. It does not establish the requested uniform polynomial-time bound.
The special-case proof is sound.
Initially all manipulable mass is unmatched. Every changed-report class consists entirely of coalition mass, so weak improvement excludes truly unacceptable matched partners.
A class with final holding $T_c<q_c$ was never full: total held mass cannot decrease. It therefore never rejected a listed proposer, and its cumulative accepted mass never exceeded $T_c$. Shrinking its capacity to $T_c$ creates no additional rejection during the replay.
Returning removed capacity to empty-report classes adds only rejecting classes. The same matched allocation can consequently be replayed under batch DA, and proposal-order independence identifies the resulting outcome.
Selecting precisely the remaining changed-report capacities yields positive coalition mass that is completely matched to partners strictly above $\bot$. This contradicts the strong promise.
The case $D=\varnothing$ is also covered: no profitable deviation exists.
The structural observations, rational-replacement result, finite search, and empty-report special case constitute genuine progress. Their conclusions are narrower than the requested complexity classification, and the prover states that limitation accurately.
The write-up needs a routine clarification of its dummy augmentation. Beyond that, resolving the target requires substantive new work rather than an expositional repair.
⟨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.