A source and later-work search performed on 2026-07-28 found no proof or counterexample for the general complement question. Durand, Jones, Makowsky, and More state the problem as open and identify the complexity-theoretic equivalence \[ \mathrm{Spec}=\mathrm{coSpec}\quad\Longleftrightarrow\quad \mathrm{NE}=\mathrm{coNE}. \] Kopczyński and Tan prove that the full question can be reduced to first-order sentences with three variables and one symmetric binary relation, under the semantic restriction that every finite model is an undirected bipartite graph. Their earlier two-variable result gives a boundary on the other side: spectra of two-variable logic with counting are exactly the semilinear sets and are closed under complement.

The fixed finite unary-vocabulary calculation in this packet supplies a complete fragment result and an exact quantifier-rank cost. It leaves the three-variable binary-relation frontier untouched. The unresolved remainder is the full statement: construct a first-order spectrum for every complement, or prove that one complement is outside the class of first-order spectra.

Kopczyński and Tan first reduce the complement question to three-variable sentences over binary relations. Their later graph encoding replaces any collection of binary relations by one symmetric binary relation. For a source sentence \(\Phi\), the construction gives constants \(p,q\) and a sentence \(\Phi'\) with \[ \operatorname{Spec}(\Phi')=\{pn+q:n\in\operatorname{Spec}(\Phi)\}. \] Every model of \(\Phi'\) is an undirected bipartite graph, and the transformation preserves the number of variables when at least three are available. The proof of Corollary 1.2 combines this encoding with the spectrum-machine characterization and a padding argument to obtain the stated equivalence.

Kopczyński and Tan translate the existence of finite models of a \(C^2\) sentence into Presburger conditions on the sizes of vertex classes in regular and biregular graphs. This proves that every \(C^2\) spectrum is semilinear. Their converse construction represents every semilinear set as the spectrum of a \(C^2\) sentence. Semilinear sets are closed under complement, which gives the fragment-level result. Restricting their natural-number convention to the positive cardinalities used by this problem preserves the conclusion.

This theorem permits arbitrary finite relational vocabularies inside \(C^2\) and allows counting quantifiers. The checked variable-hierarchy reduction places the unresolved case at three variables.

Fix integers \(r,q\ge1\). The \(r\) unary predicates determine \(t=2^r\) Boolean 1-types, or colors. Write \(n_i\) for the size of color class \(i\). Two finite structures agree on every sentence of quantifier rank at most \(q\) exactly when the vectors \[ (\min(n_1,q),\ldots,\min(n_t,q)) \] agree. In the \(q\)-round Ehrenfeucht-Fraïssé game, the duplicator matches elements within corresponding colors. A disagreement below \(q\) is exposed by selecting all elements in the smaller class and one more in the larger class. De Rijke states this standard monadic equivalence criterion as Theorem 3.10. The generator collapse and counts below are derived here.

Every truncated vector is definable at rank \(q\). A coordinate \(i<q\) is expressed by requiring exactly \(i\) elements of that color. The coordinate \(q\) requires at least \(q\). Conjunction defines one vector, and disjunction selects any collection of vectors.

Set \(A=t(q-1)\). A vector with every coordinate below \(q\) contributes one exact cardinality, and every singleton size from \(1\) through \(A\) occurs this way. A vector with at least one coordinate equal to \(q\) contributes a tail \(\{n:n\ge s\}\), where \(s\) is the sum of its coordinates. Every tail start \(s\) from \(q\) through \(tq\) occurs. The rank-\(q\) spectra are therefore exactly the unions generated by \[ \{n\}\quad(1\le n\le A), \qquad \{n:n\ge s\}\quad(q\le s\le tq). \]

There are \(2^A\) finite spectra. To count the cofinite spectra, use the largest missing positive integer \(L\), with \(L=0\) for the full set. The cases \(0\le L\le A\) contribute \(2^A\) spectra in total. Each of the \(t-1\) values \(A+1\le L\le tq-1\) permits an arbitrary subset of \(\{1,\ldots,A\}\) and forces every size from \(A+1\) through \(L\) to be absent. Thus there are \(t2^A\) cofinite spectra and \((t+1)2^A\) spectra altogether.

The complement of a finite rank-\(q\) spectrum is an allowed cofinite spectrum. The complement of a cofinite rank-\(q\) spectrum is finite and has no element above \(tq-1\). At rank \(q+1\), exact singleton generators extend through \(tq\), so every such complement occurs. Exactly \((t-1)2^A\) spectra lack a same-rank complement. The bound is sharp: the rank-\(q\) spectrum \[ \{1,\ldots,A\}\cup\{n:n\ge tq\} \] has complement \(\{A+1,\ldots,tq-1\}\), which first becomes available at rank \(q+1\). For one unary predicate this interval is the singleton \(\{2q-1\}\).

This argument covers each fixed finite unary vocabulary. The unrestricted problem allows relations of higher arity and remains open.

Take \[ \varphi=(\exists x\,P(x))\wedge(\exists y\,\neg P(y)). \] It has a model exactly at sizes \(n\ge2\), since the interpretation of \(P\) must be a nonempty proper subset. Its logical negation says that \(P\) is empty or contains the whole universe. At every positive size, one of those interpretations exists. Hence \[ \operatorname{Spec}(\varphi)=\{n:n\ge2\},\qquad \operatorname{Spec}(\neg\varphi)=\mathbb Z_{>0}, \] while \[ \mathbb Z_{>0}\setminus\operatorname{Spec}(\varphi)=\{1\}. \] The failed method is the direct replacement \(\varphi\mapsto\neg\varphi\). A spectrum existentially projects over all interpretations of the relation symbols at each size. Formula negation changes which structures satisfy the sentence and leaves that existential projection in place. Any complement construction must control existence across all structures of a cardinality.

The audit began with the canonical statement, then read the Durand–Jones–Makowsky–More survey, the two finite-variable papers by Kopczyński and Tan, their later one-relation graph reduction, and Reichenberger’s recent historical account. The survey supplies the original formulation and the spectrum-complexity theorem used here. Targeted searches through 2026 found no claimed solution or stronger normal form.

A broad positive fragment checked here is \(C^2\), whose spectra are exactly semilinear. The most restrictive normal form located for the remaining problem is Corollary 1.2 of the 2018 paper: three variables and one symmetric binary relation suffice when all finite models are undirected bipartite graphs. The targeted monadic search found the finite-or-cofinite classification and de Rijke’s explicit bounded-rank equivalence criterion, with no exact generator classification or rank-stratified spectrum count. The search cannot establish novelty for the formulas proved in this packet. TheoremDB orientation resolved the production target exactly and returned zero attached research records. Local fixture and slug searches found no competing packet or duplicate research object.

This was a focused dated search, so silence outside the checked sources has no evidentiary force. The open-status record relies on what the named sources state and on the absence of a located later resolution.

Implement Theorem 1.1 of Kopczyński and Tan as a syntax-directed compiler. Given a first-order sentence \(\Phi\) using at least three variables over binary relations, the artifact should emit the one-relation sentence \(\Phi'\), the constants \(p,q\), and checkable translation data for \[ \operatorname{Spec}(\Phi')=\{pn+q:n\in\operatorname{Spec}(\Phi)\}. \] For \(m\) normalized source relations, the paper's construction gives \(p=m+3\) and \(q=8m+2\). The trace should cover self-loop elimination, padding to \(m\ge3\), the definitions \(F_1,\ldots,F_5\), the constraints \(P_1,\ldots,P_6\), and the forward and reverse model maps. It should retain the source variable bound, prove symmetry of the relation, and derive the bipartition of every model.

The first milestone accepts three-variable sentences over one source relation with quantifier rank at most three. Its test manifest fixes 64 canonical normalized sentences of at most twelve abstract-syntax nodes, chosen to exercise every compiler clause and their main interactions. For each sentence it enumerates every source relation through cardinality four, builds the forward target model, and checks the translated sentence and size equation. Reverse correctness comes from the emitted clause-by-clause proof trace. Generated target models and single-edge mutations supply bounded regression coverage. Self-loop elimination introduces a second relation, then dummy padding brings the normalized count to three, so the affine constants are \(p=6\) and \(q=26\). Stop after eight active implementation hours or after every compiler clause and size equation has a checked lemma. A successful artifact would reproduce an established reduction. The remaining complement construction would stay visible as a separate obligation.

A spectrum signature records membership through cardinality 34 and a separate eventual-tail bit. With \(r\) unary predicates, the program enumerates all \((q+1)^{2^r}-1\) positive-domain truncated count vectors for \(1\le r,q\le3\). It converts every vector to an exact singleton or a tail and checks that the distinct contributions are precisely the generators in asser-claim-monadic-rank-classification. It then forms every union of those generators. The largest census covers 65,535 truncated vectors and 589,824 distinct spectra at \(r=q=3\).

For each bounded pair \((r,q)\), the replay verifies the formulas for finite, cofinite, and total spectra. It complements every enumerated signature, checks the same-rank failure count, and tests membership at rank \(q+1\) without assuming the enumerated family. It also constructs the sharp interval witness. The deeper one-unary run enumerates ranks one through nine, reports ranks one through eight, checks every subset of q-types through rank three, and reconstructs all q-types from labelled unary structures through rank four. A separate recursive solver plays 16,470 bounded Ehrenfeucht-Fraïssé games for one and two unary predicates and matches every result against the truncated-count criterion.

Spectrum operations use finite integer bitsets. The game solver uses finite tuples and recursion. A supervisor enforces the wall-clock limit and polls the two-process resident set every 0.02 seconds. The worker enforces the CPU limit and requests an address-space limit where the platform supports it. The replay uses no network access or random choice.