{"id":"f7383f2e-f958-47d4-8038-2f890aa0bc0d","arxiv_id":"2602.16810","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"LOP is separated from Strong Avoid and Least Number in the black-box TFΣ2 setting, via Σ2-variant Sherali-Adams pseudo-expectations.","lead":"The authors prove that the Linear Ordering Principle (LOP) does not reduce to Strong Avoid by efficient black-box reductions in the second level of the total-function polynomial hierarchy, providing the first TFΣ2 problem outside the Strong-Avoid-reducible class. The proof builds a degree-Ω(n) pseudo-expectation over total orders using a combinatorial covering argument about permutations.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"LOP encoding in §4 uses a tautological totality axiom; as printed the formula does not encode the stated problem.","rationale":"The paper's central claim is LOP ∉ StrongAvoid^dt, obtained by ruling out low-degree Σ2-uSA proofs via a Σ2-pseudo-expectation for the propositional encoding of LOP. The main technical construction, the uniform pseudo-expectation over total orders, appears structurally sound: Lemmas 4.4–4.12 are reasonable normalizations, and Theorem 4.13's counting argument, despite minor presentational slips, supplies the needed over-counting lower bound. The final inequality in Theorem 4.13, although printed in a compressed form, can be justified by splitting the fraction; it is not a fatal gap. The more immediate correctness issue is the printed totality axiom O_{i,j} = x_{i,j} ∨ ¬x_{i,j}, which is a tautology. Under the paper's own LOP definition, the totality condition is x_{i,j} ∨ x_{j,i} (otherwise incomparability is a violation). With the tautological O, the formula does not encode the stated LOP, and the equivalence between -M_i and 'i is not minimal' breaks. This is almost certainly a typo, and the pseudo-expectation proof is insensitive to the correction, so the right disposition is conditional acceptance after fixing the formula. The FIM25 bridge theorem is a published dependency and not re-proved here; it remains a secondary concern, but the totality axiom is a concrete, checkable issue that should be resolved first.","tokens_in":22135,"tokens_out":58198,"duration_ms":489559,"concrete_test":"Correct O_{i,j} to x_{i,j} ∨ x_{j,i} in Section 4 and re-verify: (1) the conjunction of axioms is unsatisfiable exactly under the Section 1 LOP definition; (2) the step in §4 that every weakening of a non-M axiom is true on all total orders still works, since x_{i,j} ∨ x_{j,i} is true on every total order; (3) no other use of O assumes the tautological form. If the proof survives, the typo is benign; if not, Theorem 1.1 is not proved for the stated LOP.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 4 lists the totality axiom as O_{i,j}: x_{i,j} ∨ ¬x_{i,j}, a tautology, rather than the required x_{i,j} ∨ x_{j,i}. The LOP definition in Section 1 makes incomparability a violation (condition ii), so totality is part of the search problem. The non-minimality axioms -M_i: ∨_{j≠i} x_{j,i} say 'i has a predecessor'; this is equivalent to 'i is not minimal' only under totality. As printed, the formula F_LOP therefore encodes the Ordering Principle for partial orders, not the LOP defined earlier, and Theorem 4.1's pseudo-expectation is constructed for the wrong formula unless O is corrected. This is likely a typo: the pseudo-expectation proof treats O as a non-M axiom true on all total orders, which also holds for x_{i,j} ∨ x_{j,i}. But the central separation is stated for the LOP of Section 1, so the formula must be corrected before Theorem 1.1 is established as written.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":22380,"tokens_out":22895,"duration_ms":197766,"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":[{"comment":"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.","section":"§4, axiom block before Definition 4.2"},{"comment":"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.","section":"§4.1.3, final estimate in Theorem 4.13"},{"comment":"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.","section":"§5, Definition 5.7 and Proposition 5.8"},{"comment":"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.","section":"§3, proof of Lemma 3.4"}],"minor_comments":[{"comment":"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.","section":"§5.2, proof of Theorem 1.2"},{"comment":"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.","section":"§3, Theorem 3.2"},{"comment":"The reference [GZSD25] has typographical problems: 'In Submission, 20225' and the author name appears as 'Ghenntiyala' while the text uses 'Ghentiyala'. Please correct.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The paper is promising and the main idea is sound, but the written version has several sign/encoding errors in the central technical sections. None appears to be unfixable: the LOP totality axiom should be x_{i,j}\\lor x_{j,i}, the numerical bound in Theorem 4.13 needs a corrected estimate, and the reduced-problem axiom in Proposition 5.8 should use \\overline{G}_{b,y}. Once these are corrected, I expect the main separations to go through. I recommend major revision rather than rejection, and I would ask the authors to re-verify the algebra in Proposition 5.8 carefully."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should know: this is the first TFΣ2 problem shown outside StrongAvoid^dt in the black-box model, and the core mechanism—extending pseudo-expectations to Σ2 weakenings and turning a permutation-covering problem into a degree lower bound—is a substantial new technique. It deserves a serious referee. But don't accept the current version as is. Section 4's LOP encoding uses O_{i,j}: x_{i,j} ∨ ¬x_{i,j}, which is a tautology, not the totality axiom x_{i,j} ∨ x_{j,i}. The paper's own Section 1 defines LOP with incomparability as a violation, so the formula in Section 4 encodes the Ordering Principle for partial orders, not LOP. The pseudo-expectation proof is insensitive to the difference (the intended totality axiom is also true on every total order), so the fix is straightforward, but Theorem 1.1 is not established by the manuscript as written.\n\nWhat is genuinely new: the separation itself, complementing KP24's reverse direction; the Σ2 pseudo-expectation criterion (Lemma 3.4) and the covering lower bound; and the factorization of reductions into weakenings plus counter-example reductions, yielding a reusable non-reducibility criterion (Corollary 5.1). The LEASTNUMBER separation is a nice application. No fitted parameters, no invented entities, no post-hoc selection. The proof is detailed and the combinatorial core looks plausible.\n\nSoft spots, in proportion: the final estimate in Theorem 4.13 is not literally correct as printed—with ℓ+g ≤ n/100 you get (99n/100)^2(99n/100−1), not (99n/100)^3, so the displayed inequality overstates the constant. It is easily fixed and the margin still works, but it should be corrected. Also, the definitions of AVOID and STRONG AVOID in Section 1 are printed identically—a plain typo that obscures the statement. And the load-bearing bridge is Theorem 3.2 from FIM25, by three of the four authors, not re-derived here. That is a legitimate published dependency, and I do not see circularity, but the paper should flag it more prominently and the referee should verify the statement matches.\n\nWho this is for: people working on TFΣ2, range avoidance, proof complexity, and query complexity. It answers a specific question of KKMP21 and provides a template for future separations. I would bring it to a reading group and cite it once the typos are fixed.\n\nRecommendation: send to peer review, but insist on fixing the totality axiom typo before publication. The core result is very likely right; the manuscript just needs a careful proofreading pass.","headline":"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.","tokens_in":22856,"tokens_out":2952,"would_cite":true,"duration_ms":26504,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F20","68Q15","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["TFΣ2","Strong Avoid","Linear Ordering Principle","Sherali-Adams proof system","pseudo-expectation","black-box reductions","proof complexity","permutation covering"],"falsifier":"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.","tokens_in":22023,"feed_emoji":"🔀","tokens_out":6337,"duration_ms":58597,"temperature":0.7,"pith_summary":"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.","feed_headline":"Linear Ordering Principle evades Strong Avoid in black-box setting","feed_subtitle":"First TFΣ2 problem outside the class of problems reducible to Strong Avoid, via Σ2 Sherali–Adams pseudo-expectations.","key_machinery":"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","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["LOP escapes Strong Avoid in black-box reductions","New separation: LOP not reducible to Strong Avoid","Sherali-Adams bound yields LOP vs Strong Avoid gap","First TFΣ2 problem beyond Strong Avoid class","Black-box: LOP beats Strong Avoid via SA lower bound"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["LOP escapes Strong Avoid in black-box reductions","New separation: LOP not reducible to Strong Avoid","Sherali-Adams bound yields LOP vs Strong Avoid gap","First TFΣ2 problem beyond Strong Avoid class","Black-box: LOP beats Strong Avoid via SA lower bound"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000148,"raw_usage":{"total_tokens":1085,"prompt_tokens":865,"completion_tokens":220,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":609,"completion_tokens_details":{"reasoning_tokens":154}},"tokens_in":609,"tokens_out":220,"duration_ms":2609,"temperature":1.0,"reasoning_tokens":154,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T22:26:59.704062+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}