{"id":"fe2de090-ea4e-403b-9927-424fe62058b3","arxiv_id":"2502.00680","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"This paper proves oracle, logical, and Ladner-type structural theorems for the complexity class ∃R, some conditional on ∃R being different from NP.","lead":"Researchers proved that several structural results long known for the complexity class NP also hold for the real-number class ∃R, including oracle separations and a logical description. The results answer open questions from the community's standard reference on the existential theory of the reals.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Theorem 2's oracle separation is an artifact of allowing BSS machines exact real-valued oracle queries, not a BGS-style relativizational separation; a symmetric oracle model may collapse it.","rationale":"The reader's CONDITIONAL verdict is fair. The main theorems other than the oracle result—descriptive complexity (§3) and Ladner (§4)—are supported by known techniques ([11], [2], [15]), and the presentation gaps (parity reversal in Lemma 2, garbled exponential-gap notation) are repairable typos. The oracle model, however, is not a typo; it is a definitional choice that changes the meaning of the theorem. In classical relativization, P^A ⊆ NP^A holds for every A because the machine model is fixed; here the paper intentionally allows the base machine to differ, so the 'separation' NP^Z ⊊ ∃R^Z is not evidence about the relationship between NP and ∃R in any fixed model. Because the paper's stated goal is to answer the compendium's open structural questions, this concern is load-bearing. It does not invalidate the paper as a mathematical contribution under its own definitions, and the authors are transparent about the subtlety, so no verdict change is needed beyond the reader's existing conditional. The concrete test above would settle whether the separation survives a symmetric oracle model.","tokens_in":14411,"tokens_out":28392,"duration_ms":303267,"concrete_test":"Re-run Theorem 2(b) after modifying Definition 3 so that a BSS machine may only query the oracle with elements of {0,1}* (non-Boolean queries receive answer 0), and encode Z as the set of binary representations of integers. If, as expected, ∃R^Z collapses to ∃R and NP^Z to NP, then the separation in Theorem 2(b) is an artifact of exact real oracle queries rather than a relativizational separation in the BGS sense.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Definition 3's oracle model for ∃R^A is the load-bearing weakness. It allows a constant-free BSS machine to submit arbitrary real vectors as oracle queries, whereas NP^A and PSPACE^A are defined by Turing machines querying a Boolean oracle. The integer-oracle separation in Theorem 2(b) depends entirely on this asymmetry: the BSS machine can guess a real vector x, query Z about each coordinate, and thereby decide Hilbert's Tenth Problem, which is undecidable for Turing machines. Hence NP=NP^Z ⊊ ∃R^Z is not a BGS-style separation of two relativized versions of the same base model; it separates a Turing-machine class with a decidable oracle from a BSS class with exact real membership tests. The paper explicitly acknowledges the different machine models, but this means Theorem 2 does not answer the compendium's open question unless one accepts this nonstandard relativization as the intended one. A symmetric oracle model (e.g., Boolean-only queries) would restore NP^A ⊆ ∃R^A for all A and likely collapse the separation.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proves structural complexity results for the class ∃R. It establishes oracle results relative to a BSS-based oracle model, showing oracles that collapse or separate the relevant classes; a descriptive-complexity characterization of ∃R by existential second-order logic over discrete R-structures; and a Ladner-style theorem giving, under the assumption ∃R ≠ NP, a problem in ∃R \\ NP that is not ∃R-complete. The main technical tool is the characterization ∃R = BP(NP_R^0) and the countability of constant-free BSS machines.","tokens_in":14570,"tokens_out":8640,"duration_ms":82566,"significance":"If correct, the results would answer several open structural questions from the compendium of Schaefer, Cardinal, and Miltzow and would provide useful BSS-based analogues of classical theorems. The paper is clearly structured and the high-level proof strategies are plausible and mostly follow known techniques. However, the oracle relativization is nonstandard and asymmetric, and the proofs of the main theorems are partly sketches with deferred details or contain parity/indexing errors. The paper is not yet ready for publication in its current form, but the underlying ideas are promising and likely repairable.","major_comments":[{"comment":"The oracle model is asymmetric: ∃R^A is defined by constant-free BSS machines that may query arbitrary real vectors, while NP^A and PSPACE^A are defined by Turing machines with a Boolean oracle. The separation NP = NP^Z ⊊ ∃R^Z in Theorem 2(b) depends essentially on this asymmetry, since a BSS machine can guess a real vector and query membership of each coordinate in Z, thereby deciding Hilbert's tenth problem. The paper acknowledges the different machine models in Section 2, but this means the result is not a BGS-style relativization of a single base model. The paper should either prove the separation under a symmetric oracle model or explicitly state that it solves a different, nonstandard question.","section":"Section 2, Definition 3"},{"comment":"The proof that ∃R^QBF = PSPACE enumerates query strings over the alphabet {0,1,*} and treats * as denoting a non-binary component. But a BSS machine can compute arbitrary real-valued queries, and the actual real values influence the subsequent computation. The simulation must existentially quantify the real-valued queries inside the first-order sentence, rather than only enumerate bit patterns. As written, the argument does not cover all possible oracle queries and is therefore incomplete.","section":"Section 2, proof of Theorem 2(a)"},{"comment":"The appendix proofs of Theorems 3 and 4 are only sketches. Theorem 3's proof states that the FO_R^0 formula is 'constructed precisely as in [11]', and Theorem 4's proof says the details 'can be found in [11] and can be transferred almost literally'. Since the main contribution of Section 3 is the transfer to the constant-free, discrete setting, the key step—that the constructed formulas lie in ∃SO_R^0 and FFP_R^0—should be shown in detail or via a precise transfer lemma. As written, the central descriptive-complexity claims are not fully verified in the manuscript.","section":"Section 3, Theorems 3 and 4"},{"comment":"The parity cases in Lemma 2 are inverted. Definition 10 defines L(a) to equal QPS0 exactly on intervals [a_{2i-1}, a_{2i}-1], which start at odd indices. Lemma 2's proof, however, says that if the maximal j with a_j ≤ n is even, then n ∈ {a_{2j'}, ..., a_{2j'+1}-1} and L(a) ∩ {0,1}^n equals QPS0; this is the opposite of Definition 10. This parity error makes the reduction in Lemma 2 incorrect as written, and the lemma is load-bearing for the claim that L(a) and L(b) belong to ∃R.","section":"Section 4, Lemma 2"},{"comment":"The proof outline for the Ladner-type theorem is incomplete in several places. In Lemma 1, for an input x with n ∈ [b_{2i-1}, b_{2i}-1], the second case states 'n < b_{2i-1}', which is false, and the proof does not justify why a polynomial-time reduction cannot map positive instances into later L(a)-intervals; the exponential gap is not used carefully enough. In Theorem 6, the sequence construction is described algorithmically, but there is no proof that for every i a suitable n(i) exists, nor a complexity bound for computing the sequences, despite condition ii) requiring efficient computability. These are nontrivial gaps in the diagonalization argument.","section":"Section 4, Lemma 1 and Theorem 6"}],"minor_comments":[{"comment":"There is a typo in the abstract: 'separating NP form ∃R' should read 'separating NP from ∃R'.","section":"Abstract"},{"comment":"The sentence 'Since in this sine-model one can decide in constant time whether a number is integral, it follows can P_R^Z can be decided by a sine-machine' contains duplicated words and should be rephrased.","section":"Section 2, proof of Theorem 2(c)"},{"comment":"Reference [20] appears to have 'Preprint, arXiv:2407.18006, 2024' appended to the 1994 Michaux paper; this arXiv identifier already belongs to reference [23], so the reference list needs correction.","section":"References"},{"comment":"The definition of L(a) uses a set-builder-like notation but the closing brace is missing; the displayed definition should be cleaned up for readability.","section":"Section 4, Definition 10"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nMeer-Wurm gives plausible answers to three compendium questions about ∃R: oracle separations, a descriptive-complexity characterization, and a conditional Ladner theorem. The descriptive part is the strongest; the oracle part is the most fragile.\n\nWhat's new: Theorem 2a (QBF oracle collapses P^A=NP^A=∃R^A=PSPACE^A) is convincing. Theorem 2b (NP=NP^Z ⊊ ∃R^Z for integer oracle Z) works, but it depends on ∃R^A allowing BSS machines to query real vectors, while NP^A and PSPACE^A are Turing machines with Boolean oracles. The paper admits this asymmetry, so it is not a hidden flaw, but it is not a BGS-style separation of the same base model. The stress-test note is right. If the compendium question wanted a true BGS analogue, this doesn't fully answer it.\n\nThe descriptive complexity section (Theorem 3) looks solid: discrete R-structures and constant-free BSS machines are well chosen, and the proof sketch follows the expected Grädel-Meer transfer. Details deferred to [11], but the strategy is sound.\n\nThe Ladner part (Theorem 5) is a genuine result if the construction works, but the presentation is thin. Section 4 is an outline; Lemma 2 has a parity reversal; Definition 10's gaps are garbled. The idea is plausible (quantifier elimination to diagonalize against NP-machines), but a referee will have work to do.\n\nCitations are fine. Self-citations are prior independent results.\n\nThis is for the ∃R community. It deserves a serious referee, though I'd want the authors to fill in the Ladner proof and reframe the oracle claims more carefully. My recommendation: send to review, expect revision.","headline":"Plausible structural results for ∃R, with a candid but significant caveat about the oracle model.","tokens_in":15139,"tokens_out":3773,"would_cite":true,"duration_ms":38733,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q15","03C13","03B25"],"pacs":[],"model":"deepseek-v4-flash","headline":"Three classical NP structural results are proven for the existential theory of the reals (∃R).","keywords":["existential theory of the reals","complexity classes","relativization","oracle separation","descriptive complexity","Ladner's theorem","Blum-Shub-Smale model","real computation"],"falsifier":"Restrict the oracle access in ∃R^A to Boolean strings (as for NP^A) and check whether the integer-oracle separation NP = NP^Z ⊊ ∃R^Z still holds; if it collapses, the claimed relativization depends essentially on the asymmetric oracle model.","tokens_in":14173,"feed_emoji":"🔢","tokens_out":6445,"duration_ms":56811,"temperature":0.7,"pith_summary":"The paper proves that three classical structural results for the class NP also hold for ∃R, the complexity class of decision problems reducible to deciding whether a system of polynomial equations with rational coefficients has a real solution. It constructs oracles that both collapse and separate ∃R with NP and PSPACE, following the Baker–Gill–Solovay pattern. It gives a descriptive complexity characterization of ∃R via existential second-order logic over finite structures with real-valued functions. Finally, it shows that if ∃R differs from NP, then there are problems in the difference that are not ∃R-complete, a Ladner-style intermediate result. These answer open questions from the standard compendium on ∃R and establish structural tools for further study.","feed_headline":"Oracle, logic, and hierarchy results for the existential reals","feed_subtitle":"Answers open questions on relativization, descriptive complexity, and intermediate ∃R problems.","key_machinery":"The paper's proofs rest on the characterization of ∃R as BP($NP^{0}$_R), which yields a countable set of machine models, and on the ability (via quantifier-elimination results for the reals) to express both Turing-machine and $NP^{0}$_R-machine computations as existential first-order formulas over the reals with rational coefficients. For the oracle results, the crucial mechanism is the asymmetry between real-valued oracle queries for ∃R and Boolean queries for NP; for the descriptive complexity result, it is the notion of a 'discrete R-structure' and the capture of algebraic unit-cost computation by existential second-order logic; for the Ladner theorem, it is the construction of two sequences of input-dimension intervals with exponential gaps so that any polynomial-time reduction would force a polynomial-time decision of a PSPACE-hard problem.","core_discovery":"The central discovery is that the structural theory of NP transfers to ∃R when the right machine model is used. The key identification is ∃R = BP($NP^{0}$_R), the Boolean part of nondeterministic Blum–Shub–Smale machines that use only rational constants and accept real witnesses. From this, the paper derives three main theorems. First, relative to a QBF oracle, P^A = NP^A = ∃R^A = PSPACE^A, while relative to the integer oracle Z, NP = NP^Z but ∃R^Z contains undecidable problems such as Hilbert's tenth problem, so the two classes separate. Second, ∃R is exactly the class of problems definable by existential second-order sentences over discrete R-structures, i.e., finite ordered structures augmented with the real field and rational constants. Third, assuming ∃R ≠ NP, there exists a language in ∃R \\ NP that is not ∃R-complete, constructed by diagonalization with exponentially spaced input-dimension intervals.","pith_inferences":["The oracle asymmetry suggests that any proof separating NP from ∃R must inherently use the real-valued witness structure, not just Boolean computation; a fully relativizing proof would be impossible if the oracle definitions were symmetric.","The discrete R-structure framework may allow importing finite-model-theory techniques, such as games or locality, to attack problems in ∃R.","The integer oracle separation can be seen as evidence that the boundary between discrete and continuous computation is real, and may inform the search for natural problems in ∃R \\ NP.","One could test whether the Ladner construction works for other classes sandwiched between NP and PSPACE that share the countable-machine property."],"forward_implications":["The compendium's open questions on relativization and descriptive complexity for ∃R are settled.","The integer oracle shows that relativization for ∃R is sensitive to the machine model; standard Boolean-relativization arguments do not capture the real-number witness behavior.","The descriptive characterization gives a logical handle on ∃R that may support inexpressibility-based lower bounds.","The Ladner-style result implies that if ∃R ≠ NP, the structure between them is nontrivial, with intermediate degrees.","The methods may extend to other real-number classes defined by countable constant-free BSS machines."],"supporting_citations":[{"why":"The compendium that lists the open structural questions this paper answers.","marker":"[23]"},{"why":"Establishes NP_R-completeness of polynomial systems, which underlies the characterization ∃R = BP(NP^0_R).","marker":"[4]"},{"why":"Provides the PSPACE algorithm for the existential theory of the reals used in the oracle and reduction arguments.","marker":"[5]"},{"why":"Fagin's theorem, the classical descriptive complexity result for NP that the paper adapts to ∃R.","marker":"[8]"},{"why":"Gives the real-number descriptive complexity framework on which the discrete R-structure logic is built.","marker":"[11]"},{"why":"Ladner's theorem, the classical intermediate-problem result that the paper re-proves for ∃R.","marker":"[14]"},{"why":"Provides the exponential-gap construction for non-complete problems over the complex numbers, adapted here.","marker":"[15]"},{"why":"Shows how quantifier elimination helps construct intermediate problems in real-number classes, a key ingredient for Theorem 5.","marker":"[2]"},{"why":"Matiyasevich's undecidability of Hilbert's tenth problem, used to show ∃R^Z contains undecidable problems.","marker":"[16]"},{"why":"Gives the sine-model lower bound used to prove the separation in the full BSS model.","marker":"[17]"}],"fun_headline_variants":["Oracles split NP from existential reals","Ladner's theorem arrives for ∃R","Descriptive complexity captures ∃R","New oracle worlds for NP and ∃R","Hierarchy and separations for real machines"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is the asymmetry in the definitions of the relativized classes: a machine in ∃R^A may ask the oracle arbitrary real-vector questions, while machines in NP^A and PSPACE^A may only ask Boolean questions; the integer-oracle separation NP = NP^Z ⊊ ∃R^Z relies on this asymmetry.","fun_headline_variants_meta":{"raw":{"variants":["Oracles split NP from existential reals","Ladner's theorem arrives for ∃R","Descriptive complexity captures ∃R","New oracle worlds for NP and ∃R","Hierarchy and separations for real machines"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000343,"raw_usage":{"total_tokens":1869,"prompt_tokens":909,"completion_tokens":960,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":525,"completion_tokens_details":{"reasoning_tokens":894}},"tokens_in":525,"tokens_out":960,"duration_ms":9052,"temperature":1.0,"reasoning_tokens":894,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T18:08:54.475608+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Restrict the oracle access in ∃R^A to Boolean strings (as for NP^A) and check whether the integer-oracle separation NP = NP^Z ⊊ ∃R^Z still holds; if it collapses, the claimed relativization depends essentially on the asymmetric oracle model.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Establishes NP_R-completeness of polynomial systems, which underlies the characterization ∃R = BP(NP^0_R)."},{"cited_title":"Canny, Some algebraic and geometric computations in PSPACE","cited_arxiv_id":null,"evidence_quote":"Provides the PSPACE algorithm for the existential theory of the reals used in the oracle and reduction arguments."},{"cited_title":"Fagin, Generalized first-order spectra and polynomial-time recognizable sets, Pro- ceedings SIAM-AMS 7, 43–73, 1974","cited_arxiv_id":null,"evidence_quote":"Fagin's theorem, the classical descriptive complexity result for NP that the paper adapts to ∃R."},{"cited_title":"Gr¨ adel, K","cited_arxiv_id":null,"evidence_quote":"Gives the real-number descriptive complexity framework on which the discrete R-structure logic is built."},{"cited_title":"Ladner, On the structure of polynomial time reducibility , Journal of the ACM 22, 155–171, 1975","cited_arxiv_id":null,"evidence_quote":"Ladner's theorem, the classical intermediate-problem result that the paper re-proves for ∃R."},{"cited_title":"Malajovich, K","cited_arxiv_id":null,"evidence_quote":"Provides the exponential-gap construction for non-complete problems over the complex numbers, adapted here."},{"cited_title":"Ben-David, K","cited_arxiv_id":null,"evidence_quote":"Shows how quantifier elimination helps construct intermediate problems in real-number classes, a key ingredient for Theorem 5."},{"cited_title":"Matiyasevich, Enumerable sets are Diophantine , Soviet Mathematics","cited_arxiv_id":null,"evidence_quote":"Matiyasevich's undecidability of Hilbert's tenth problem, used to show ∃R^Z contains undecidable problems."},{"cited_title":"Meer, Real Number Models under Various Sets of Operations , J","cited_arxiv_id":null,"evidence_quote":"Gives the sine-model lower bound used to prove the separation in the full BSS model."}],"review_version":1}