順序数グラフの分割関係に対する非普遍性の障害
A Nonuniversality Obstruction to an Ordinal Graph Partition Relation
研究概要
Erdős 第597問は、順序数の平方 ω₁² の2彩色に特定の対象グラフが必ず現れるかを問う。本論文は、Erdős が報告した Baumgartner の負の分割関係を用い、対象を有限グラフに限定しない主張に反例を与える。対象はちょうど ℵ₁ 個の頂点を持つ連結二部グラフで、直径は3以下であり、可算無限完全二部グラフを含まない。有限の完全二部部分グラフを捉える整礎木を用い、Shelah の非普遍性定理を先行結果として明示する。Lean 形式化が検証するのは、明示された一つの既刊結果を前提とする導出（Reference-Gated）であり、Baumgartner の構成そのものは形式化していない。別途提示された有限対象の問題は未解決のままである。
元の公開問題
Erdős 第597問：有限グラフに限定しない対象についての主張
Paul Erdős: Some problems on finite and infinite graphs (1987) — Printed p.224: the forbidden-K4 and forbidden-countable-biclique graph question, the reported Baumgartner relation, and the separately posed finite-target variant.
Erdős Problems: problem 597 — The result addresses the unrestricted infinite-target assertion; it does not settle the finite-target question or claim endorsement by the problem-list maintainer.
原文要旨（英語）
Erdős asked whether every graph on at most ℵ₁ vertices omitting both a four-vertex clique and a countably infinite complete bipartite graph is forced as a blue subgraph in every colouring of the ordinal square ω₁² with no red homogeneous set of order type ω₁·ω. We apply the nonuniversality of graphs omitting the countable biclique to Baumgartner's negative partition relation, as recorded by Erdős, to obtain a negative answer to this unrestricted assertion. The obstructing target can have exactly ℵ₁ vertices and be connected and bipartite, with diameter at most three. We give an elementary well-founded-tree proof of the required special case of Shelah's nonuniversality theorem. The separate question about finite target graphs remains unresolved by this argument.
数学の検証
これらの結論は、公開された一覧にある外部定理を前提としています。これは中間版であり、最終的な形式化には各前提の検証済み証明も必要です。
検証基準