Pith. sign in

REVIEW 4 major objections 3 minor 1 cited by

Separations above TFNP from Sherali-Adams Lower Bounds

T0 review · 4 major / 3 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper establishes that the Linear Ordering Principle, a natural TFΣ2 search problem, has no efficient black-box reduction to Strong Avoid, making it the first TFΣ2 problem known to lie outside the Strong-Avoid-reducible class.

desk verdict A genuinely new separation—LOP outside StrongAvoid^dt—but the current manuscript encodes the wrong totality axiom for LOP, so the main theorem needs a one-line fix before it is literally true. read the letter →

arxiv 2602.16810 v2 pith:M5MVXKW2 submitted 2026-02-18 cs.CC

Noah Fleming , Anna Gal , Deniz Imrek , Christophe Marciot This is my paper · ORCID
classification cs.CC MSC 03F2068Q1568Q17
keywords TFΣ2StrongAvoidLinearOrderingPrincipleSherali-Adamsproofsystempseudo-expectationblack-boxreductionscomplexitypermutationcovering
topics P versus NP
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper establishes that the Linear Ordering Principle (LOP) is not solvable by an efficient black-box reduction to Strong Avoid, placing LOP outside the class of TFΣ2 problems reducible to Strong Avoid for the first time. The proof translates the search problem into a propositional formula and shows that no low-degree proof of it exists in a Σ2 variant of the Sherali–Adams proof system. To do this, the authors extend pseudo-expectations to the Σ2 setting and construct one of degree n/300 for LOP, reducing the task to a combinatorial covering problem about permutations. If correct, the result gives the first TFΣ2 separation obtained via proof complexity, and a criterion separating LOP from any problem with a low-degree Sherali–Adams refutation.

What carries the argument

A degree-d Σ2-pseudo-expectation is a family of linear functionals, one for each Σ2-weakening of the constraint set, each behaving like the uniform distribution over total orders when evaluated on low-degree polynomial tests. Lemma 3.4 says such a family exists exactly when there is no degree-d Σ2-unary-Sherali-Adams proof. The construction for LOP at d=n/300 runs through normalization lemmas that turn arbitrary weakenings and juntas into canonical permutation terms of the form [[S]]_π, followed by a counting argument over hitting triples in a 0/1 array showing that multiply-accepted orders outweigh rejected orders. This counting is exactly the covering problem about permutations stated in t

What would settle it

Find a polylog(n)-degree Σ2-unary-Sherali-Adams refutation of the propositional encoding of LOP, or an explicit black-box decision-tree reduction from LOP to Strong Avoid; either would overturn Theorem 1.1. Equivalently, for some d ≤ n/100, construct a cover of the orders that do not start with 1 using fewer than d! collections C_{S,σ}, contradicting the covering lemma behind Theorem 4.1.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1.1: LOP is not in StrongAvoid^dt, meaning there is no polylog-complexity decision-tree reduction from the Linear Ordering Principle to Strong Avoid. The technical engine is Theorem 4.1: a degree n/300 Σ2-pseudo-expectation exists for the LOP axioms. By Lemma 3.4, such a pseudo-expectation precludes any degree-n/300 Σ2-unary-Sherali-Adams refutation; by the characterization theorem from the authors' companion paper, reducibility to Strong Avoid is equivalent to the existence of a polylog-degree Σ2-unary-Sherali-Adams proof, so the pseudo-expectation rules out the reduction. The same construction yields Corollary 5.1, that LOP is not reducible to any TFΣ2 problem

Load-bearing premise

The separation rests on the characterization from the authors' companion paper — that efficient black-box reductions to Strong Avoid coincide with polylog-degree Σ2-unary-Sherali-Adams proofs — which is cited but not re-proved here; if that bridge fails, the pseudo-expectation lower bound no longer implies LOP ∉ StrongAvoid^dt.

Editorial extensions

If this is right

  • StrongAvoid^dt does not contain all of TFΣ2: LOP is a natural TFΣ2 problem outside the class of problems reducible to Strong Avoid, answering a question of Kleinberg et al. in the black-box setting.
  • LOP is also not reducible to Least Number, and more generally Corollary 5.1 separates LOP from every TFΣ2 problem with a polylog-degree Sherali–Adams refutation.
  • The Σ2 pseudo-expectation method is a viable route to TFΣ2 degree lower bounds, so future separations can be pursued by constructing such pseudo-expectations rather than by direct query-complexity adversaries.
  • The covering problem is settled negatively for d ≤ n/100: one cannot cover the set of total orders that do not start with 1 using fewer than d! collections of the form C_{S,σ}, and this bound is tight up to constant factors.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the companion-paper bridge between reducibility and Σ2-unary-Sherali-Adams proofs is robust, the same pseudo-expectation construction may separate LOP from other TFΣ2 problems that currently resist direct query lower bounds; the bottleneck will be constructing pseudo-expectations for each candidate target.
  • The covering formulation isolates a purely combinatorial question — the minimum number of permutation cylinders needed to cover all orders not starting with 1 — so progress on this covering problem can feed directly into proof-complexity separations without requiring a new reduction argument.
  • The n/300 constant is not optimized; counting hitting k-tuples for larger k could raise the degree lower bound and potentially separate LOP from problems whose Sherali–Adams refutations have slightly larger degree.
  • A natural next target, flagged but not answered in the paper, is separating Least Number from Strong Avoid; since Least Number has an exponential-size but low-degree refutation, doing so would require a size-based lower-bound method rather than the degree-based pseudo-expectation used here.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 3 minor

Summary. The paper claims that the Linear Ordering Principle (LOP) is not in StrongAvoid^dt, the class of TF\Sigma_2 problems reducible in the black-box setting to Strong Avoid, and likewise that LOP is not reducible to Least Number. The proof route is proof complexity: using the characterization from [FIM25] that reductions to Strong Avoid are equivalent to polylog-complexity \Sigma_2-unary-Sherali-Adams proofs, the authors reduce the separation to a degree lower bound for LOP. The technical core is a degree n/300 \Sigma_2-pseudo-expectation for the LOP axioms, built from the uniform distribution over all total orders and a combinatorial covering argument about permutations. A further criterion (Corollary 5.1) converts the LOP pseudo-expectation into a non-reducibility statement against any problem with a low-degree SA proof, yielding the Least Number separation.

Significance. If the argument is correct after the fixes below, this is a significant result: it answers, in the black-box setting, the question of whether natural TF\Sigma_2 problems all reduce to Strong Avoid, and it demonstrates that the proof-complexity bridge of [FIM25] can prove separations in TF\Sigma_2^dt. The pseudo-expectation is explicit, parameter-free, and the covering formulation is concrete and falsifiable. The paper also gives a useful decomposition of arbitrary reductions into weakenings plus counter-example reductions. These are genuine strengths. However, the written manuscript contains several sign/axiom errors in load-bearing places, and the numerical estimate at the end of Theorem 4.13 needs correction; these require revision before the claims are established as stated.

major comments (4)
  1. [§4, axiom block before Definition 4.2] The totality axiom is printed as O_{i,j}: x_{i,j} \lor \neg x_{i,j}, which is a tautology and does not encode the LOP totality condition (condition (ii) in Section 1). As printed, Theorem 4.1 and hence Theorem 1.1 are about a formula without totality, i.e. a partial-order version, not the stated LOP. The intended axiom is evidently x_{i,j} \lor x_{j,i}; the pseudo-expectation over total orders is compatible with that axiom, so the proof can be repaired, but the formula must be corrected before the main separation is established.
  2. [§4.1.3, final estimate in Theorem 4.13] The displayed lower bound writes the first term as 6(99n/100)^3/n^3. Substituting the available bound gives factors (99n/100)^2(99n/100-1), not (99n/100)^3, since the last factor is n-l-g-1 and only n-l-g is bounded below by 99n/100. The displayed substitution is therefore not literally valid. The conclusion survives: a more careful estimate shows the corresponding scalar is still > 1 for n sufficiently large. Please replace the displayed calculation with the correct bound.
  3. [§5, Definition 5.7 and Proposition 5.8] There is a sign error concerning G_{b,y}. The correctness condition for the reduced problem is \overline{G_{b,y}}(x) \lor \bigvee_c R_{s(n),b,c}(f(x)), i.e. the DNF polynomial should be (1-G_{b,y}) + \sum_c R_{s(n),b,c}\circ f - 1. With the printed G_{b,y}+\sum_c R-1, multiplying by G_{b,y} and summing over y yields \sum_c R\circ f, not \sum_c R\circ f - 1, so the asserted final refutation identity is false. With the corrected axiom, the intended composition argument works: multiplying (1-G)+S-1 by G gives GS-G, and summing over y gives S-1. This is a load-bearing step for Corollary 5.1 and must be fixed.
  4. [§3, proof of Lemma 3.4] The last paragraph of the proof is garbled: 'Consider G= S G G' and the switch from the weakening G to a union over all weakenings is not written coherently. The statement is clear, but the proof needs a clean notation for the union formula and for the pseudo-expectation indexed by it.
minor comments (3)
  1. [§5.2, proof of Theorem 1.2] The DNF for the least-number axioms is printed as x_i \lor \bigvee_{j<i} x_j, but the displayed polynomial and the refutation use -x_i + \sum_{j<i} x_j, which is the polynomial for \neg x_i \lor \bigvee_{j<i} x_j. Correct the displayed DNF to match the intended axiom.
  2. [§3, Theorem 3.2] The main separation is conditional on the [FIM25] characterization that reductions to Strong Avoid are equivalent to polylog-complexity \Sigma_2-uSA proofs. This is a published result by three of the four authors, and reliance on it is legitimate, but the dependence should be stated even more prominently in the introduction and in the proof of Theorem 1.1.
  3. [References] The reference [GZSD25] has typographical problems: 'In Submission, 20225' and the author name appears as 'Ghenntiyala' while the text uses 'Ghentiyala'. Please correct.

Circularity Check

1 steps flagged · score 3.0 of 10

Self-cited FIM25 characterization is load-bearing for the separation; the pseudo-expectation core is explicit and non-circular. The printed totality axiom is a tautology (correctness issue, not circularity).

  1. self citation load bearing [Theorem 3.2 (Section 3) and Proof of Theorem 1.1 (Section 4)]
    "Theorem 3.2 ([FIM25]). For any R∈TFΣ^dt_2 there exists a polylog(n)-complexity Σ2-uSA proof of R iff R∈StrongAvoiddt. ... By Theorem 3.2 LOP∈StrongAvoiddt iff there exists a polylog(n)-complexity Σ2-uSA proof of the propositional encoding of LOP given by Lemma 2.4."

    This is the bridge that converts the paper's new lower bound (no polylog-degree Σ2-uSA proof of LOP) into the advertised separation LOP∉StrongAvoiddt. The theorem is not proved here; it is imported from [FIM25], a prior paper by three of the four authors. The central separation therefore inherits its correctness from this self-cited characterization rather than from a derivation contained in the present paper. This is a load-bearing self-citation dependency, not an equivalence-by-construction: the pseudo-expectation in Theorem 4.1 is explicit and independently constructed.

full rationale

The technical engine of the paper is not circular. Theorem 4.1 constructs an explicit degree n/300 Σ2-pseudo-expectation as a uniform distribution over total orders, with no fitted parameters and no back-solving; Lemma 3.4 is proved in the text; and the combinatorial covering argument over permutations is genuine new content. The skeptical issue about the totality axiom is a correctness/typo defect, not a circularity: Section 4 lists O_{i,j}: x_{i,j} ∨ ¬x_{i,j}, which is a tautology, whereas the LOP definition requires x_{i,j}∨x_{j,i}. As printed, Theorem 4.1 concerns the Ordering Principle for partial orders. This does not make the derivation circular, and the intended fix preserves the argument because x_{i,j}∨x_{j,i} is also true for every total order. The only load-bearing imported ingredient is Theorem 3.2 (and Lemma 2.4) from [FIM25], a published, peer-reviewed paper by three of the four authors; it is not re-derived here. This creates a self-citation dependency for the black-box separation claim, but the present paper's own lower-bound construction is independent and explicit. Hence the circularity score is modest.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The proof introduces no empirical parameters or new physical entities. The constants n/300, n/100 are proof-theoretic thresholds. The main external load is the self-cited FIM25 characterization.

assumptions (3)
  • domain assumption Theorem 3.2 of [FIM25]: R∈TFΣ2^dt is reducible to StrongAvoid^dt iff the encoding of R has a polylog(n)-complexity Σ2-unary-Sherali-Adams proof.
    Section 3, Theorem 3.2; this self-cited, peer-reviewed theorem is the bridge converting the separation into a proof-complexity lower bound. It is not reproved here.
  • domain assumption Lemma 2.4 of [FIM25]: every TFΣ2^dt problem is equivalent to a false-formula search problem for an unsatisfiable DNF formula of polylog width.
    Section 2, Lemma 2.4; used to encode LOP as a propositional formula over LOP axioms.
  • standard math Standard facts about total orders and DNF polynomial encodings, including replacing negated literals x_{i,j} by x_{j,i} for total orders and the equivalence of DNF satisfaction and polynomial non-negativity.
    Used throughout Section 4 in the normalization and pseudo-expectation arguments.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Separations above TFNP from Sherali-Adams Lower Bounds." pith.science (2026). https://pith.science/paper/M5MVXKW2

@misc{pith2026260216810,
  author       = {Pith},
  title        = {Pith review of: Separations above TFNP from Sherali-Adams Lower Bounds},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/M5MVXKW2}},
  note         = {Machine review of arXiv:2602.16810}
}
abstract

Unlike in TFNP, for which there is an abundance of problems capturing natural existence principles which are incomparable (in the black-box setting), Kleinberg et al. [KKMP21] observed that many of the natural problems considered so far in the second level of the total function polynomial hierarchy (TF$\Sigma_2$) reduce to the Strong Avoid problem. In this work, we prove that the Linear Ordering Principle does not reduce to Strong Avoid in the black-box setting, exhibiting the first TF$\Sigma_2$ problem that lies outside of the class of problems reducible to Strong Avoid. The proof of our separation exploits a connection between total search problems in the polynomial hierarchy and proof complexity, recently developed by Fleming, Imrek, and Marciot [FIM25]. In particular, this implies that to show our separation, it suffices to show that there is no small proof of the Linear Ordering Principle in a $\Sigma_2$-variant of the Sherali-Adams proof system. To do so, we extend the classical pseudo-expectation method to the $\Sigma_2$ setting, showing that the existence of a $\Sigma_2$ pseudo-expectation precludes a $\Sigma_2$ Sherali-Adams proof. The main technical challenge is in proving the existence of such a pseudo-expectation, we manage to do so by solving a combinatorial covering problem about permutations. We also show that the extended pseudo-expectation bound implies that the Linear Ordering Principle cannot be reduced to any problem admitting a low-degree Sherali-Adams refutation.

Figures

Figures reproduced from arXiv: 2602.16810 by the authors.

Figure 1
Figure 1. Relationships of some TFΣ dt 2 classes. A black arrow from a class A to a class B means that A ⊆ B ([KKMP21]). A dashed or dotted arrow from a class A to a class B means that A ̸⊆ B. The dashed separations are proved in this paper. [KP24] proves that STRONGAVOID does not reduce to AVOID and LOP. [FGJ+26] proves that AVOIDdt does not contain all of TFNPdt. This implies that none of the other problems in the diagram r… view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Provable Reductions in TFNP

    cs.CC 2026-06 unverdicted novelty 8.0 of 10

    New <EF, R> proof systems are introduced; <EF, Iter> is shown polynomially equivalent to G1 and [EF, Resolution], yielding the first characterization of an implicit proof system by a classical one beyond prior work.

Reference graph

Works this paper leans on

15 extracted references · 2 linked inside Pith · cited by 1 Pith paper

  1. [6]

    Total search problems in ZPP

    [FGJ+26] Noah Fleming, Stefan Grosser, Siddhartha Jain, Jiawei Li, Hanlin Ren, Morgan Shirley, and Weiqiang Yuan. Total search problems in ZPP. In Shubhangi Saraf, editor,17th Innovations in Theoretical Com- puter Science Conference, ITCS 2026, Bocconi University, Milan, Italy, January 27-30, 2026, volume 362 ofLIPIcs, pages 60:1–60:26. Schloss Dagstuhl -...

    2026

  2. [8]

    Provably Total Functions in the Polynomial Hier- archy

    [FIM25] Noah Fleming, Deniz Imrek, and Christophe Marciot. Provably Total Functions in the Polynomial Hier- archy. In Srikanth Srinivasan, editor,40th Computational Complexity Conference (CCC 2025), volume 339 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 28:1–28:40, Dagstuhl, Germany,

    2025

  3. [13]

    Strong vs

    [KP24] Oliver Korten and Toniann Pitassi. Strong vs. weak range avoidance and the linear ordering principle. In65th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2024, Chicago, IL, USA, October 27-30, 2024, pages 1388–1407. IEEE,

    2024

  4. [14]

    Symmetric exponential time requires near-maximum circuit size: Simplified, truly uniform

    [Li24] Zeyong Li. Symmetric exponential time requires near-maximum circuit size: Simplified, truly uniform. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors,Proceedings of the 56th Annual ACM Sympo- sium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 2000–2007. ACM,

    2024

  5. [1998]

    TFNP characterizations of proof systems and mono- tone circuits

    [BFI23] Sam Buss, Noah Fleming, and Russell Impagliazzo. TFNP characterizations of proof systems and mono- tone circuits. In Yael Tauman Kalai, editor,14th Innovations in Theoretical Computer Science Confer- ence, ITCS 2023, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, volume 251 ofLIPIcs, pages 30:1–30:40. Schloss Dagstuhl - Leibniz-Zentrum f...

    2023

  6. [2004]

    Symmetric exponential time requires near-maximum circuit size

    [CHR24] Lijie Chen, Shuichi Hirahara, and Hanlin Ren. Symmetric exponential time requires near-maximum circuit size. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors,Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 1990–1999. ACM,

    2024

  7. [2009]

    de Rezende, Aaron Potechin, and Kilian Risse

    [dRPR23] Susanna F. de Rezende, Aaron Potechin, and Kilian Risse. Clique is hard on average for unary sherali- adams. In64th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2023, Santa Cruz, CA, USA, November 6-9, 2023, pages 12–25. IEEE,

    2023

  8. [2012]

    How to fit large complexity classes into TFNP.arXiv:2412.09984 [cs.CC],

    [Tha24] Neil Thapen. How to fit large complexity classes into TFNP.arXiv:2412.09984 [cs.CC],

    arXiv

Show all 15 references
  1. [2019]

    Separations in proof complexity and TFNP.CoRR, abs/2205.02168,

    [GHJ+22] Mika G ¨o¨os, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP.CoRR, abs/2205.02168,

    arXiv

  2. [2021]

    The hardest explicit construction

    [Kor21] Oliver Korten. The hardest explicit construction. In62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 433–444. IEEE,

    2021

  3. [2022]

    Adventures in monotone complex- ity and TFNP

    [GKRS19] Mika G ¨o¨os, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in monotone complex- ity and TFNP. In Avrim Blum, editor,10th Innovations in Theoretical Computer Science Conference, ITCS 2019, January 10-12, 2019, San Diego, California, USA, volume 124 ofL...

    2019

  4. [2023]

    Relativized NP search problems and propositional proof systems

    16 [BM04] Josh Buresh-Oppenheim and Tsuyoshi Morioka. Relativized NP search problems and propositional proof systems. In19th Annual IEEE Conference on Computational Complexity (CCC 2004), 21-24 June 2004, Amherst, MA, USA, pages 54–67. IEEE Computer Society,

    2004

  5. [2024]

    Dantchev, Barnaby Martin, and Mark Nicholas Charles Rhodes

    [DMR09] Stefan S. Dantchev, Barnaby Martin, and Mark Nicholas Charles Rhodes. Tight rank lower bounds for the sherali-adams proof system.Theor. Comput. Sci., 410(21-23):2054–2063,

  6. [2025]

    Ghenntiyala, L

    [GZSD25] S. Ghenntiyala, L. Zeyong, and N. Stephens-Davidowitz. Range avoidance, arthur-merlin, and tfnp.In Submission, 20225. [KKMP21] Robert Kleinberg, Oliver Korten, Daniel Mitropolsky, and Christos H. Papadimitriou. Total functions in the polynomial hierarchy. In James R. ...

    2021

  7. [2026]

    Black-box PPP is not turing-closed

    [FGPR24] Noah Fleming, Stefan Grosser, Toniann Pitassi, and Robert Robere. Black-box PPP is not turing-closed. In Bojan Mohar, Igor Shinkar, and Ryan O’Donnell, editors,Proceedings of the 56th Annual ACM Sympo- sium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, Jun...

    2024

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.