順序数グラフの分割関係に対する非普遍性の障害
A Nonuniversality Obstruction to an Ordinal Graph Partition Relation
研究概要
Erdős 第597問は、順序数の平方 ω₁² の2彩色にどのグラフが必ず現れるかを問う。本稿は Shelah の既知の非普遍性定理を、Erdős が報告した Baumgartner の負の分割関係に適用し、対象を有限グラフに限定しない主張に反例を与える。対象はちょうど ℵ₁ 個の頂点を持つ連結二部グラフで、直径は3以下、可算無限完全二部グラフを含まない。完全二部部分グラフの明示的なランク証明と連結な対象の構成を示し、木の節点の比較可能性を使う先行手法を Shelah に帰属させる。Lean の付随コードは構成と引用した Baumgartner の定理からの導出を検証し、その引用定理の証明自体はコードベースの範囲外にある。Reference-Gated はこの機械検証の境界を表す。有限対象の問いは未解決のままである。
元の公開問題
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 Problem 597 asks 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 identify a nonuniversality obstruction to this assertion: applying Shelah's theorem for graphs omitting the countable biclique to Baumgartner's negative partition relation, as recorded by Erdős, gives 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.
数学の検証
機械検証された導出は、出典を明示した引用定理を入力として用います。その証明は現在のコードパッケージの範囲外です。完全な形式化には、これらの引用結果の検証済み証明も含める必要があります。
検証基準