pith. sign in

arxiv: 2605.23517 · v1 · pith:56FRVO77new · submitted 2026-05-22 · 💻 cs.CC

Probabilistically checkable proofs for the Existential Theory of the Reals

Jack Stade This is my paper

Pith reviewed 2026-05-25 02:34 UTC · model grok-4.3

classification 💻 cs.CC
keywords existential theory of the realsPCP theoreminapproximabilityMAX-ETR-INVapproximation algorithmscomplexity theoryreal variables
0
0 comments X

The pith

MAX-ETR-INV is ∃R-hard to approximate better than a factor of 1-ε for some ε>0.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes a probabilistically checkable proof theorem for the existential theory of the reals. This is used to prove that the problem MAX-ETR-INV, which maximizes the number of satisfied constraints of the forms x=1, xy=1 or x+y=z with variables bounded in [1/2, 2], is hard to approximate to within 1-ε. The hardness applies even to nondeterministic polynomial-time algorithms unless the complexity class ∃R equals NP. Sympathetic readers care because this limits the approximability of a problem that many geometric decision problems reduce to.

Core claim

We prove a PCP theorem for the existential theory of the reals, showing that MAX-ETR-INV is ∃R-hard to approximate to within some constant factor. We also give a polynomial-time 8-factor approximation algorithm and a non-deterministic-polynomial-time 2-factor approximation algorithm for MAX-ETR-INV.

What carries the argument

A gap-producing reduction from ETR-INV to MAX-ETR-INV based on a PCP construction for ETR instances.

If this is right

  • MAX-ETR-INV has no 1-ε approximation algorithm in nondeterministic polynomial time unless ∃R equals NP.
  • There exists a polynomial-time algorithm that approximates MAX-ETR-INV to within a factor of 8.
  • There exists a nondeterministic polynomial-time algorithm that approximates MAX-ETR-INV to within a factor of 2.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This hardness may extend to other optimization versions of ∃R-complete geometric problems.
  • The specific value of ε could potentially be improved with tighter PCP parameters.
  • Similar techniques might apply to other real-number constraint satisfaction problems.

Load-bearing premise

The problem ETR-INV with constraints x=1, xy=1, x+y=z and variables in [1/2,2] is ∃R-complete.

What would settle it

A nondeterministic polynomial-time algorithm that approximates MAX-ETR-INV within a factor of 1-ε/2 on all instances would falsify the inapproximability claim.

read the original abstract

We prove a PCP theorem for the existential theory of the reals, showing that MAX-ETR-INV is $\exists\mathbb{R}$-hard to approximate to within some constant factor. The existential theory of the reals (ETR) is a decision problem asking if there exists a set of real-valued variables satisfying some constraints involving polynomials and inequalities, and $\exists\mathbb{R}$ is the complexity class of problems polynomial-time reducible to ETR. Many important geometric problems are known to be $\exists\mathbb{R}$-complete. $\exists\mathbb{R}$-hardness results frequently work by a reduction from the $\exists\mathbb{R}$-complete problem ETR-INV, which asks if there is a an assignment of real variables each in the interval $[\frac12, 2]$ satisfying some constraints of form $x=1$, $xy=1$ and $x+y=z$. MAX-ETR-INV is a related optimization problem that asks, given a set of constraints of form $x=1$, $xy=1$, and $x+y=z$, for a feasible (that is, satisfiable with variables in $[\frac12, 2]$) subset of those constraints of the largest possible size. We show that there is some constant $\epsilon>0$ such that it is $\exists\mathbb{R}$-hard to approximate MAX-ETR-INV better than a $1-\epsilon$ factor. This means that even a non-deterministic polynomial-time algorithm can't approximate MAX-ETR-INV better than this factor unless $\exists\mathbb{R}=\text{NP}$. We also give a polynomial-time $8$-factor approximation algorithm and a non-deterministic-polynomial-time $2$-factor approximation algorithm for MAX-ETR-INV.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript proves a PCP theorem for the existential theory of the reals by establishing that MAX-ETR-INV (maximizing the number of satisfied constraints of types x=1, xy=1, x+y=z with all variables in [1/2,2]) is ∃R-hard to approximate within a factor 1-ε for some constant ε>0. Hardness is obtained via a gap-producing reduction from the decision problem ETR-INV. The paper also supplies an 8-factor polynomial-time approximation algorithm and a 2-factor non-deterministic polynomial-time approximation algorithm.

Significance. If the reduction preserves the exact three constraint forms and [1/2,2] bounds, the result would be the first constant-factor inapproximability result for an ∃R-complete problem and would constitute a PCP theorem for ∃R with direct implications for geometric problems. The two approximation algorithms are concrete positive contributions that bound the approximability gap from above. The work ships explicit approximation ratios and a non-deterministic 2-approximation, which are verifiable strengths.

major comments (2)
  1. [Abstract] Abstract (paragraph on ETR-INV completeness): the ∃R-completeness of ETR-INV is invoked to transfer hardness to MAX-ETR-INV, yet the manuscript does not exhibit or cite a reference establishing that completeness holds exactly when variables are restricted to [1/2,2] and only the three listed constraint types are permitted. If any step of the standard reduction requires an auxiliary variable outside [1/2,2] or an additional constraint form, the gap-producing instance for MAX-ETR-INV lies outside the stated language and the 1-ε inapproximability claim does not follow.
  2. [Hardness section (reduction from ETR-INV)] The gap-producing reduction (implicit in the hardness proof) must map feasible ETR-INV instances to MAX-ETR-INV instances while preserving both satisfiability and the restricted constraint vocabulary; without an explicit verification that the known ETR-INV completeness reduction stays inside these syntactic restrictions, the central hardness claim rests on an unverified assumption.
minor comments (2)
  1. [Abstract] The abstract states the 8-factor and 2-factor approximation ratios but does not indicate whether the algorithms are analyzed in the main body or deferred to an appendix; a pointer would improve readability.
  2. [Introduction / preliminaries] Notation for the optimization objective (size of largest feasible subset) should be defined once with a displayed equation rather than described only in prose.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the need to make the completeness of ETR-INV under the stated syntactic restrictions fully explicit. We address both major comments below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [Abstract] Abstract (paragraph on ETR-INV completeness): the ∃R-completeness of ETR-INV is invoked to transfer hardness to MAX-ETR-INV, yet the manuscript does not exhibit or cite a reference establishing that completeness holds exactly when variables are restricted to [1/2,2] and only the three listed constraint types are permitted. If any step of the standard reduction requires an auxiliary variable outside [1/2,2] or an additional constraint form, the gap-producing instance for MAX-ETR-INV lies outside the stated language and the 1-ε inapproximability claim does not follow.

    Authors: The ETR-INV problem is introduced in the literature precisely with variables restricted to [1/2,2] and using only the three constraint types x=1, xy=1, x+y=z; its ∃R-completeness under these restrictions is a standard result obtained via reductions that preserve the interval bounds and constraint vocabulary (by scaling and choice of auxiliary values that remain inside [1/2,2]). We will add an explicit citation to the relevant reference establishing this completeness, together with a short clarifying sentence in the abstract and introduction, so that the transfer of hardness to MAX-ETR-INV is fully grounded. revision: yes

  2. Referee: [Hardness section (reduction from ETR-INV)] The gap-producing reduction (implicit in the hardness proof) must map feasible ETR-INV instances to MAX-ETR-INV instances while preserving both satisfiability and the restricted constraint vocabulary; without an explicit verification that the known ETR-INV completeness reduction stays inside these syntactic restrictions, the central hardness claim rests on an unverified assumption.

    Authors: The gap-producing reduction we employ is from the decision version of ETR-INV (already restricted to the three constraint forms and [1/2,2]) to MAX-ETR-INV; it is constructed to use only the allowed constraints and to keep all variables inside the interval. The completeness of the source problem under these restrictions is the standard result cited above. We will add the same explicit reference and a brief verification paragraph in the hardness section to remove any ambiguity. revision: yes

Circularity Check

0 steps flagged

No circularity: hardness flows from external completeness of ETR-INV

full rationale

The paper's central claim is obtained by a gap-producing reduction from the decision problem ETR-INV, which is invoked as a known ∃R-complete problem under the exact constraint forms (x=1, xy=1, x+y=z) and variable bounds [1/2,2] stated in the abstract. No equation, definition, or self-citation in the provided text reduces the inapproximability factor 1-ε to a fitted quantity, a renamed input, or a load-bearing self-citation chain whose own justification collapses. The completeness result is treated as prior external knowledge, and the new contribution (PCP-style inapproximability plus approximation algorithms) is independent of any self-referential construction. This satisfies the default expectation of a self-contained derivation against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on the standard definition of ∃R-completeness for ETR-INV and the standard PCP framework; no free parameters, ad-hoc axioms, or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption ETR-INV is ∃R-complete under the given constraint forms and variable interval [1/2, 2]
    Invoked to transfer hardness from ETR-INV to MAX-ETR-INV
  • standard math Standard definitions of PCP and approximation hardness apply to the optimization version MAX-ETR-INV
    Background framework used throughout the result

pith-pipeline@v0.9.0 · 5850 in / 1389 out tokens · 21082 ms · 2026-05-25T02:34:59.940346+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    2007 , issue_date =

    Dinur, Irit , title =. 2007 , issue_date =. doi:10.1145/1236457.1236459 , journal =

    work page doi:10.1145/1236457.1236459 2007

  2. [2]

    2006 , isbn =

    Radhakrishnan, Jaikumar , title =. 2006 , isbn =. doi:10.1007/11786986_10 , booktitle =

    work page doi:10.1007/11786986_10 2006

  3. [3]

    1991 , issn =

    Optimization, approximation, and complexity classes , journal =. 1991 , issn =. doi:https://doi.org/10.1016/0022-0000(91)90023-X , url =

    work page doi:10.1016/0022-0000(91)90023-x 1991

  4. [4]

    Entropy Waves, the Zig-Zag Graph Product, and New Constant-Degree Expanders , urldate =

    Omer Reingold and Salil Vadhan and Avi Wigderson , journal =. Entropy Waves, the Zig-Zag Graph Product, and New Constant-Degree Expanders , urldate =

    work page

  5. [5]

    Framework for ER-Completeness of Two-Dimensional Packing Problems , year=

    Abrahamsen, Mikkel and Miltzow, Tillmann and Seiferth, Nadja , booktitle=. Framework for ER-Completeness of Two-Dimensional Packing Problems , year=

    work page

  6. [6]

    2024 , eprint=

    The Existential Theory of the Reals as a Complexity Class: A Compendium , author=. 2024 , eprint=

    work page 2024

  7. [7]

    1988 , isbn =

    Canny, John , title =. 1988 , isbn =. doi:10.1145/62212.62257 , booktitle =

    work page doi:10.1145/62212.62257 1988

  8. [8]

    Proceedings of the 37th International Conference on Neural Information Processing Systems , articleno =

    Bertschinger, Daniel and Hertrich, Christoph and Jungeblut, Paul and Miltzow, Tillmann and Weber, Simon , title =. Proceedings of the 37th International Conference on Neural Information Processing Systems , articleno =. 2023 , publisher =

    work page 2023

  9. [9]

    Training Neural Networks is ER-complete , url =

    Abrahamsen, Mikkel and Kleist, Linda and Miltzow, Tillmann , booktitle =. Training Neural Networks is ER-complete , url =

    work page

  10. [10]

    41st International Symposium on Computational Geometry (SoCG 2025) , pages =

    Stade, Jack , title =. 41st International Symposium on Computational Geometry (SoCG 2025) , pages =. 2025 , volume =. doi:10.4230/LIPIcs.SoCG.2025.74 , annote =

    work page doi:10.4230/lipics.socg.2025.74 2025

  11. [11]

    Journal of the ACM , author=

    The art gallery problem is. Journal of the ACM , author=. 2021 , pages=. doi:10.1145/3486220 , number=

    work page doi:10.1145/3486220 2021

  12. [12]

    and Khot, S

    Guruswami, V. and Khot, S. , booktitle=. Hardness of Max 3SAT with no mixed clauses , year=

    work page

  13. [13]

    Explicit Expanders of Every Degree and Size , url =

    Alon, Noga , date =. Explicit Expanders of Every Degree and Size , url =. Combinatorica , number =. 2021 , bdsk-url-1 =. doi:10.1007/s00493-020-4429-x , id =

    work page doi:10.1007/s00493-020-4429-x 2021

  14. [14]

    On Radhakrishnan’s Proof of PCP Gap Amplification , author=

    work page

  15. [15]

    SIAM Journal on Computing , volume =

    Dinur, Irit and Reingold, Omer , title =. SIAM Journal on Computing , volume =. 2006 , doi =

    work page 2006

  16. [16]

    and Zwick, U

    Karloff, H. and Zwick, U. , booktitle=. A 7/8-approximation algorithm for MAX 3SAT? , year=

    work page

  17. [17]

    2011 , isbn =

    Barak, Boaz and Dvir, Zeev and Yehudayoff, Amir and Wigderson, Avi , title =. 2011 , isbn =. doi:10.1145/1993636.1993705 , booktitle =

    work page doi:10.1145/1993636.1993705 2011

  18. [18]

    Improved rank bounds for design matrices and a new proof of Kelly's theorem , volume=

    DVIR, ZEEV and SARAF, SHUBHANGI and WIGDERSON, AVI , year=. Improved rank bounds for design matrices and a new proof of Kelly's theorem , volume=. doi:10.1017/fms.2014.2 , journal=

    work page doi:10.1017/fms.2014.2 2014

  19. [19]

    Theory of Computing , volume =

    Dvir, Zeev and Saraf, Shubhangi and Wigderson, Avi , title =. Theory of Computing , volume =. 2017 , pages =. doi:10.4086/toc.2017.v013a011 , publisher =

    work page doi:10.4086/toc.2017.v013a011 2017

  20. [20]

    Proceedings of the 56th Annual ACM Symposium on Theory of Computing (STOC) , pages =

    Amireddy, Prashanth and Behera, Amik Raj and Paraashar, Manaswi and Srinivasan, Srikanth and Sudan, Madhu , title =. 2024 , isbn =. doi:10.1145/3618260.3649746 , booktitle =

    work page doi:10.1145/3618260.3649746 2024

  21. [21]

    Proceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA) , chapter =

    Prashanth Amireddy and Amik Raj Behera and Manaswi Paraashar and Srikanth Srinivasan and Madhu Sudan , title =. Proceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA) , chapter =. 2025 , pages =. doi:10.1137/1.9781611978322.187 , URL =

    work page doi:10.1137/1.9781611978322.187 2025

  22. [22]

    Demillo and Richard J

    Richard A. Demillo and Richard J. Lipton , keywords =. A probabilistic remark on algebraic program testing , journal =. 1978 , issn =. doi:https://doi.org/10.1016/0020-0190(78)90067-4 , url =

    work page doi:10.1016/0020-0190(78)90067-4 1978

  23. [23]

    Schwartz, J. T. , title =. 1980 , issue_date =. doi:10.1145/322217.322225 , journal =

    work page doi:10.1145/322217.322225 1980

  24. [24]

    Probabilistic algorithms for sparse polynomials

    Zippel, Richard. Probabilistic algorithms for sparse polynomials. Symbolic and Algebraic Computation. 1979

    work page 1979

  25. [25]

    1998 , issue_date =

    Arora, Sanjeev and Lund, Carsten and Motwani, Rajeev and Sudan, Madhu and Szegedy, Mario , title =. 1998 , issue_date =. doi:10.1145/278298.278306 , journal =

    work page doi:10.1145/278298.278306 1998

  26. [26]

    Short Locally Testable Codes and Proofs: A Survey in Two Parts

    Goldreich, Oded. Short Locally Testable Codes and Proofs: A Survey in Two Parts. Property Testing: Current Research and Surveys. 2010. doi:10.1007/978-3-642-16367-8_6

    work page doi:10.1007/978-3-642-16367-8_6 2010

  27. [27]

    2012 , issue_date =

    Yekhanin, Sergey , title =. 2012 , issue_date =. doi:10.1561/0400000030 , journal =

    work page doi:10.1561/0400000030 2012

  28. [28]

    2022 , isbn =

    Dinur, Irit and Evra, Shai and Livne, Ron and Lubotzky, Alexander and Mozes, Shahar , title =. 2022 , isbn =. doi:10.1145/3519935.3520024 , booktitle =

    work page doi:10.1145/3519935.3520024 2022

  29. [29]

    Random Structures & Algorithms , volume =

    Bafna, Mitali and Srinivasan, Srikanth and Sudan, Madhu , title =. Random Structures & Algorithms , volume =. doi:https://doi.org/10.1002/rsa.20933 , url =. https://onlinelibrary.wiley.com/doi/pdf/10.1002/rsa.20933 , year =

    work page doi:10.1002/rsa.20933

  30. [30]

    Edward J Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Liang Wang, Weizhu Chen, et al

    Expander graphs and their applications , volume=. Bulletin of the American Mathematical Society , author=. 2006 , month=. doi:10.1090/s0273-0979-06-01126-8 , number=

    work page doi:10.1090/s0273-0979-06-01126-8 2006

  31. [31]

    1997 , isbn =

    Raz, Ran and Safra, Shmuel , title =. 1997 , isbn =. doi:10.1145/258533.258641 , booktitle =

    work page doi:10.1145/258533.258641 1997

  32. [32]

    and Fortnow, L

    Babai, L. and Fortnow, L. and Lund, C. , booktitle=. Nondeterministic exponential time has two-prover interactive protocols , year=

    work page

  33. [33]

    Checking computations in polylogarithmic time , year =

    Babai, L\'. Checking computations in polylogarithmic time , year =. doi:10.1145/103418.103428 , booktitle =

    work page doi:10.1145/103418.103428

  34. [34]

    and Goldwasser, S

    Feige, U. and Goldwasser, S. and Lovasz, L. and Safra, S. and Szegedy, M. , booktitle=. Approximating clique is almost NP-complete , year=

    work page

  35. [35]

    Interactive proofs and the hardness of approximating cliques , year =

    Feige, Uriel and Goldwasser, Shafi and Lov\'. Interactive proofs and the hardness of approximating cliques , year =. doi:10.1145/226643.226652 , journal =

    work page doi:10.1145/226643.226652

  36. [36]

    Theory of Computing , volume =

    Zuckerman, David , title =. Theory of Computing , volume =. 2007 , pages =. doi:10.4086/toc.2007.v003a006 , publisher =

    work page doi:10.4086/toc.2007.v003a006 2007

  37. [37]

    1995 , issn =

    The complexity and approximability of finding maximum feasible subsystems of linear relations , journal =. 1995 , issn =. doi:https://doi.org/10.1016/0304-3975(94)00254-G , url =

    work page doi:10.1016/0304-3975(94)00254-g 1995

  38. [38]

    and Pedersen, P

    Mishra, B. and Pedersen, P. , title =. 1990 , isbn =. doi:10.1145/96877.96909 , booktitle =

    work page doi:10.1145/96877.96909 1990