序数图分割关系的非普适性障碍
A Nonuniversality Obstruction to an Ordinal Graph Partition Relation
研究概述
Erdős 第597题询问，序数平方 ω₁² 的两色染色是否必然包含某些目标图。本文使用 Erdős 所报告的 Baumgartner 负分割关系，对不限制为有限目标图的断言给出反例：目标恰有 ℵ₁ 个顶点，连通且为二部图，直径至多为三，并且不含可数无限完全二部图。论证使用刻画有限双团的良基树，并明确引用 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.
数学审核
这些结论仍以公开清单中的外部定理前提为条件。这是中间版本；最终形式化还必须为每项此前提提供检查过的证明。
审核标准