序数图分割关系的非普适性障碍
A Nonuniversality Obstruction to an Ordinal Graph Partition Relation
研究概述
Erdős 第597题询问，序数平方 ω₁² 的两色染色必然包含哪些图。本文将 Shelah 已有的非普适性定理应用于 Erdős 所报告的 Baumgartner 负分割关系，对不限制为有限目标图的断言给出反例。目标恰有 ℵ₁ 个顶点，是连通二部图，直径至多为三，并且不含可数无限完全二部图。本文给出显式的双团秩证明及连通目标构造，同时明确归属 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.
数学审核
机器检查的推导以公开列明的引用定理为输入；这些定理的证明尚未纳入当前代码包。完整形式化还需包含这些引用结果的已检查证明。
审核标准