{"id":"f99274cf-ce1a-407b-9446-d7e0e3618b80","arxiv_id":"2411.16844","paper_version":5,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":9.0,"correctness_risk":"low","formal_verification":"partial","parameter_count":0,"one_line_summary":"A countable poset with no infinite antichain is constructed that has no 'spine', disproving the Aharoni-Korman (fishbone) conjecture of 1992.","lead":"A 32-year-old conjecture about infinite partially ordered sets is false. The paper constructs a countable poset that has no infinite antichain yet cannot be partitioned into antichains met by a single chain, and it proves the conjecture still holds for a broad class of such posets.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified: the P5 construction and the no-spine proof appear sound.","rationale":"The reader flagged Observation 5.8(iv) as the weakest assumption, but this observation is a standard grid-path fact inside the product-order level Ln, and Ln is an interval of P5, so the chain exists in P5. The deeper parts of Lemma 5.11 also check out: the claim that B_ℓ is comparable to the rest of C follows because B_ℓ lies in the convex hull of a segment of the chain C∩Ln+1, and any element of C in Ln or Ln−1 is comparable to all of that convex hull by transitivity. I searched for other soft spots: the definition of P5 is a genuine partial order (transitivity is trivial across levels with index gap at least 2), P5 is countable and has no infinite antichain by a standard argument, and the final contradiction using the chain F and the antichain-partition function f is valid. The only issue found is a small edge case in the written proof: Lemma 5.10 supplies n with |Ln∩C| finite, not necessarily nonempty, so 'max(C∩Ln)' can be undefined. The intended set R is 'elements above all of C∩Ln', which is well-defined even when C∩Ln is empty, and the subsequent proof works verbatim with R=Ln in that case. This is a presentational gap that can be fixed without changing the argument; it does not affect the central claim.","tokens_in":45532,"tokens_out":37520,"duration_ms":337917,"concrete_test":"Re-run the proof of Proposition 5.7 with the empty case C∩Ln=∅ made explicit: set R=Ln and verify that the definitions of S, Lemma 5.11, and the final chain-length contradiction (F of length 2a+1 vs longest chain in T of length 2a) go through unchanged; alternatively, check the Lean formalization at the cited repository under a pinned mathlib commit.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I attempted to find a flaw in the counterexample proof and could not. Observation 5.8(iv) is correct: in the product order on Ln, a maximal chain from (x,y) to (w,z) through (u,v) has exactly w+z+1−x−y elements, and Ln is an interval of P5. The use of strong maximality of a spine is justified: if a chain D improves on a spine C by replacing a finite segment with a longer chain, then mapping each element of D\\C to the unique spine element in its antichain gives an injection into C\\D. Lemma 5.11's bijection argument is supported by the fact that the interval B_ℓ is contained in the convex hull of C∩Ln+1 and is therefore comparable to the rest of C. The only blemish is that Lemma 5.10 may return n with C∩Ln empty, making 'max(C∩Ln)' in the definition of R formally undefined; the intended meaning ('above every element of C∩Ln') is vacuously satisfied and the subsequent argument adapts, so this is a presentational issue, not a threat to the claim.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper claims to resolve the 1992 Aharoni-Korman conjecture. It develops a substantial apparatus around chain extensions, reduction orders, and strongly maximal chains, and states two main theorems: Theorem 1.15, that every countable FAC poset has a strongly maximal chain, and Theorem 1.18, that every countable vacillating FAC poset has a spine. The central result is Theorem 1.2, proved as Proposition 5.7: the explicitly defined countable poset P5 on N x N x N is scattered and has no infinite antichain, yet it admits no chain C that meets every member of some partition into antichains. The no-spine proof fixes an arbitrary chain C, uses Lemma 5.10 to find a level Ln with finite intersection with C, and then shows that no antichain partition function f can be defined on C union Ln union Ln+1, by forcing f to act bijectively on finite intervals of Ln+1 and then deriving a counting contradiction on a lower-level chain.","tokens_in":1275,"tokens_out":1882,"duration_ms":140727,"significance":"If correct, the paper settles a 1992 conjecture that has been open for over thirty years, and it does so in the negative. The counterexample is the core contribution: it is constructed explicitly, the proof of Proposition 5.7 is largely self-contained, and the paper reports that the proposition has been formally verified in Lean by Bhavik Mehta, with code available at reference [19]. That machine-checked artifact considerably strengthens confidence in the central claim. The positive theorem for countable vacillating FAC posets is also significant because it shows that the counterexample is in a precise sense at the boundary of the class of posets for which the conjecture can still hold. I read the central no-spine argument as sound; the remaining issues I found are local and presentational.","major_comments":[],"minor_comments":[{"comment":"The paper says 'Recall that a poset is vacillating if there is no contiguous chain C in P such that either C or C* has every proper interval wellfounded, but is not itself wellfounded.' This is not equivalent to Definition 1.17. Under the Section 4 formulation, a copy of omega would fail to be vacillating, while Definition 1.17 explicitly permits wellfounded and co-wellfounded posets as vacillating. Please reconcile the two statements.","section":"Section 4, opening paragraph"},{"comment":"The set R is defined as {x in Ln : x > max(C intersect Ln)}, but Lemma 5.10 only guarantees that C intersect Ln is finite, not that it is nonempty. If C intersect Ln is empty, the maximum is undefined. Please state the convention max(empty) = -infinity or redefine R as Ln in that case; the intended argument is clear and adapts, but the formal definition should be repaired.","section":"Section 5.2, proof of Proposition 5.7"},{"comment":"The displayed line 'm_{n+1} <= min{x,y} + 1 <= min{u,v} = m_n. Therefore m_{n+1} < m_n' is not a logically valid inference as written. The intended point is that comparability through the second level condition forces min{x,y} + 1 <= m_n, hence min{x,y} < m_n, and therefore m_{n+1} <= min{x,y} < m_n. Please correct the display.","section":"Section 5.2, Lemma 5.10"},{"comment":"The set T is written as {q in L_{n-1} : q is not >= (3a, a, b)}. The third coordinate is presumably n, not b, and it would help to add a sentence explaining why this set is exactly { (u,v,n-1) : u+v <= 2a-1 }.","section":"Section 5.2, final paragraph of Proposition 5.7"},{"comment":"The notation 'C intersect L_{n+1} is reduced above D0 or D1' uses the reduction symbol from Section 2.3 for objects that are not explicitly identified as nonprincipal chains. Please clarify that the intended relation is 'cofinally above' or first embed the relevant chains in N(P).","section":"Section 5.2, Lemma 5.11"},{"comment":"Item (v) asserts that P5 is scattered and not vacillating without proof. Scatterability is not used heavily in the no-spine proof, but a one-sentence justification for both claims would make the observation self-contained.","section":"Section 5.2, Observation 5.8"},{"comment":"Reference [19] cites a GitHub repository without a commit hash or version identifier. Since the formal verification is advertised as evidence for Proposition 5.7, please pin the exact version of the formalization for reproducibility.","section":"References"}],"recommendation":"minor_revision","confidential_remarks":"For the editor: the counterexample is the publishable core of the paper, and the Lean formalization is a significant strength. I found no reason to doubt the novelty or the attribution of the counterexample. The positive results in Sections 3 and 4 are long and I did not verify every step in the same detail, but their failure would not affect the central counterexample. The vacillation-definition mismatch and the small edge-case gaps in Section 5.2 should be fixed before publication."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line: this is a genuine resolution of a conjecture open since 1992. The counterexample P5 is built from scratch, with no parameter tuned to a target conclusion. The proof that P5 is a scattered FAC poset with no spine is laid out in detail, and the crucial Proposition 5.7 has been formally verified in Lean by Bhavik Mehta, with code linked in the paper. That is real evidence, not window dressing. The paper also proves the conjecture holds for countable vacillating FAC posets, which gives the counterexample context and reorients the field: failure requires a specific kind of non-vacillating interval.\n\nThe positive side is genuinely new, too. The SMC results and the replacement machinery are interesting in their own right, though they are secondary. The counterexample section is largely self-contained, so readers skeptical of the heavier machinery can jump straight to Section 5.\n\nSoft spots are minor. The Lean code has no commit hash, so the formalization is not pinned to a specific version; that is worth fixing but not disqualifying. There is also a small presentational issue in Lemma 5.10: the argument can return an n with C∩Ln empty, making 'max(C∩Ln)' formally undefined. The intended reading—'above every element of C∩Ln'—is vacuously satisfied and the proof adapts, so this is cosmetic rather than substantive. The main text is long and the positive theorem's proof is dense; referees will need patience, but I found no gap in the no-spine argument after checking the stress-test points.\n\nCitation pattern looks honest. The paper uses Duffus–Goddard and Zaguia as black boxes, which are prior independent results, and flags the hypergraph disproof of van der Zypen as related but not sufficient. No self-citation padding.\n\nWho should read this: anyone working on infinite posets, matchings, or the fishbone conjecture. It deserves a serious referee. I would recommend acceptance after minor revisions, mainly for clarity and pinning the formalization.","headline":"This paper refutes the Aharoni–Korman conjecture with a carefully constructed counterexample and a Lean-verified core proof; the positive theorem for vacillating posets keeps the conjecture's spirit alive.","tokens_in":46269,"tokens_out":2204,"would_cite":true,"duration_ms":21381,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["06A07","06A06"],"pacs":[],"model":"deepseek-v4-flash","headline":"The Aharoni–Korman (fishbone) conjecture is false: a countable poset satisfies the finite antichain condition but has no chain meeting every antichain of any partition.","keywords":["Aharoni-Korman conjecture","finite antichain condition","poset spine","strongly maximal chain","scattered poset","vacillating poset","chain replacement","counterexample"],"falsifier":"Find three points $(x,y,n) \\leq (u,v,n) \\leq (w,z,n)$ in $P_5$ such that every chain inside the interval $[(x,y,n),(w,z,n)]$ containing $(u,v,n)$ has length strictly less than $w+z+1-x-y$; that would break the chain-length observation on which Lemma 5.11 depends. Alternatively, exhibit a chain $C \\subseteq P_5$ that meets every antichain in some partition of $P_5$ into antichains, directly contradicting Proposition 5.7.","tokens_in":45304,"feed_emoji":"🐟","tokens_out":9548,"duration_ms":76173,"temperature":0.7,"pith_summary":"The paper claims to settle the Aharoni–Korman conjecture, a 1992 problem asserting that every poset with no infinite antichain (an FAC poset) has a chain that meets every antichain in some partition into antichains. The paper constructs a specific countable poset, $P_5$, and proves it is an FAC scattered poset with no such chain, so the conjecture is false in full generality. At the same time, it proves the conjecture is true for all countable 'vacillating' FAC posets, a class that forbids a particular wellfounded-over-co-wellfounded interval structure. If correct, the work closes the conjecture while showing why counterexamples must be complicated.","feed_headline":"Fishbone conjecture fails: a countable poset has no spine","feed_subtitle":"The 1992 conjecture is false, yet every countable vacillating poset still gets a spine.","key_machinery":"The central object carrying the negative result is the poset $P_5$, and the load-bearing mechanism is the chain-length observation inside each level: any interval between comparable points contains chains of a stated maximal length through a middle point, and Lemma 5.11 uses it to force a hypothetical partition function $f$ to act bijectively on finite intervals of $L_{n+1}$, producing the contradiction. For the positive side, the machinery is a family of 'replacement' partial orders on chains — $\\eta$-replacements, alternating replacements, and reductions — used with Zorn's lemma to construct maximal chains, together with the chain extension $H(P)$ and the reduction order $\\unrhd$; from a reduced chain one builds a strong thick chain, and a known theorem converts a thick chain into a spine.","core_discovery":"The central discovery is a countable poset $P_5$ — defined on levels $L_n = \\omega \\times \\omega \\times \\{n\\}$ with cross-level comparability rules — that satisfies the finite antichain condition yet admits no spine: no chain $C$ can meet every antichain of any partition into antichains. The order places $(x,y,n)$ below $(u,v,m)$ when the levels are far apart ($n \\geq m+2$), within the same level by the product order, and across adjacent levels by two comparison rules that force a precise, chain-rich geometry between $L_n$ and $L_{n+1}$. The proof fixes an arbitrary chain $C$, shows that some level meeting $C$ is finite, then shows that any hypothetical antichain partition with spine would be witnessed by a function $f$ whose level-wise behaviour contradicts the chain-length structure inside each $L_n$. The same paper proves a compensating positive theorem: every countable vacillating FAC poset has a spine.","pith_inferences":["The stability of the counterexample under changing the constant 2 to any α > 1 (noted in the paper) suggests the failure mechanism is structural rather than numerical; one could test whether the same contradiction survives for all α > 1.","Because P5 has width ℵ0, the paper's open question of whether finite-width posets all have spines is not answered by this construction; a finite-width counterexample, if one exists, would need a different mechanism than the one used here.","The replacement-order technique used to find strongly maximal chains might transfer to the hypergraph problems that motivated the conjecture, where a similar maximality-versus-partition tension appears."],"forward_implications":["The Aharoni–Korman conjecture, in full generality, is false; any future positive result must restrict the class of posets or weaken the conclusion.","For countable posets, the vacillating condition marks a sharp boundary: every countable vacillating FAC poset has a spine, while the non-vacillating poset P5 does not.","Every countable FAC poset has a strongly maximal chain, a structural guarantee weaker than a spine but now unconditional in the countable case.","Since a spine must be strongly maximal, counterexamples must be posets whose strongly maximal chains fail to extend to antichain partitions; P5 is such a poset.","The formal verification of the counterexample's key proposition means that the core of the negative result is machine-checked, not merely argued."],"supporting_citations":[{"why":"states the conjecture being disproved and supplies the width-2 base case.","marker":"[9]"},{"why":"provides a formal verification of the counterexample's key proposition.","marker":"[19]"},{"why":"supplies the theorem that turns a thick chain into a spine, used in the positive direction.","marker":"[22]"},{"why":"proves the conjecture for FAC posets with no infinite intervals, used to build strongly maximal chains.","marker":"[13]"},{"why":"classifies scattered linear orders, used to construct atomic increasing chains.","marker":"[17]"}],"fun_headline_variants":["Aharoni–Korman conjecture false: countable poset has no spine","Counterexample kills 1992 poset conjecture","Spine-free countable poset disproves Aharoni–Korman","FAC poset with no spine: conjecture false","Conjecture false, but vacillating posets still have spines"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The counterexample rests on the chain-length fact that inside each level $L_n$ of $P_5$, any interval between two comparable points has a chain of the full claimed length $w+z+1-x-y$ through any specified middle point; if this fact fails, the contradiction that rules out a spine collapses.","fun_headline_variants_meta":{"raw":{"variants":["Aharoni–Korman conjecture false: countable poset has no spine","Counterexample kills 1992 poset conjecture","Spine-free countable poset disproves Aharoni–Korman","FAC poset with no spine: conjecture false","Conjecture false, but vacillating posets still have spines"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000927,"raw_usage":{"total_tokens":3914,"prompt_tokens":832,"completion_tokens":3082,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":448,"completion_tokens_details":{"reasoning_tokens":2994}},"tokens_in":448,"tokens_out":3082,"duration_ms":17681,"temperature":1.0,"reasoning_tokens":2994,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T12:48:07.123203+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find three points $(x,y,n) \\leq (u,v,n) \\leq (w,z,n)$ in $P_5$ such that every chain inside the interval $[(x,y,n),(w,z,n)]$ containing $(u,v,n)$ has length strictly less than $w+z+1-x-y$; that would break the chain-length observation on which Lemma 5.11 depends. Alternatively, exhibit a chain $C \\subseteq P_5$ that meets every antichain in some partition of $P_5$ into antichains, directly contradicting Proposition 5.7.","supporting_citations":[{"cited_title":"Grundz¨ uge einer Theorie der geordneten Mengen.Mathema- tische Annalen 65 , 4 (1908), 435–505","cited_arxiv_id":null,"evidence_quote":"classifies scattered linear orders, used to construct atomic increasing chains."},{"cited_title":"Greene-Kleitman’s theorem for infinite posets","cited_arxiv_id":null,"evidence_quote":"states the conjecture being disproved and supplies the width-2 base case."},{"cited_title":"Disproof of the Aharoni-Korman conjecture","cited_arxiv_id":null,"evidence_quote":"provides a formal verification of the counterexample's key proposition."},{"cited_title":"Some progress on the Aharoni–Korman conjecture","cited_arxiv_id":null,"evidence_quote":"supplies the theorem that turns a thick chain into a spine, used in the positive direction."},{"cited_title":"Some progress on the Aharoni–Korman conjecture","cited_arxiv_id":null,"evidence_quote":"proves the conjecture for FAC posets with no infinite intervals, used to build strongly maximal chains."}],"review_version":1}