Erdoes #592 - working report - Erdős Problem a Day

Erdős problem #592 — wave w000

Date: 2026-07-28 (UTC)

0. Mandatory live-page gate

I fetched the live page through the Bright Data browser route, not by direct datacenter curl. I also fetched the linked discussion page.

Live URL: <https://www.erdosproblems.com/592>

The exact current problem statement, verbatim, is:

Determine which countable ordinals β have the property that, if α = ω^β, then in any red/blue colouring of the edges of K_α there is either a red K_α or a blue K_3.

The live snapshot showed:

OPEN — $1000;
0 claimed proofs;
Currently working: None;
Interested in collaborating: None;
one comment, posted by onetwothreefour on 24 July 2026 with an AI

disclosure, whose entire mathematical content is only the typo report “‘this is holds’ should be ‘this holds’”;

Likes: LawrenceHollom; all other participation markers were empty;
last edited 23 January 2026.

Thus neither stop condition is present and this run is eligible to proceed. The tracker tags and the supplied YAML were not used as a mathematical statement.

The live page lists these known results:

In arrow notation the property is

$\alpha\to(\alpha,3)^2$, and such $\alpha$ are called partition ordinals.

Specker proved the case $\beta=2$, but the property fails for

$3\leq\beta<\omega$.

Chang proved the case $\beta=\omega$.
Galvin and Larson proved that if $\beta\geq3$ has the property, then

$\beta$ is additively indecomposable, hence $\beta=\omega^\gamma$.

Schipperus proved the property when

$\gamma$ is a countable sum of one or two indecomposable ordinals, and proved failure when it is a sum of four or more.

The unresolved boundary is exactly the case in which $\gamma$ is a sum

of three indecomposable ordinals.

No claimed proof or substantive mathematical comment was hidden in the discussion page.

1. Claim labels and notation

The requested claim labels are used as follows:

(a) elementary-rigorous — fully proved here from the definitions;
(b) rigorous-modulo-named-theorem — the implication is complete once

the explicitly named published theorem is accepted;

(c) plausible/structural-unverified — diagnostic or literature-search

conclusion, not used as a theorem;

(d) computational-only — exhaustive only for the stated finite model

and range.

For a 2-colouring $\chi:[\alpha]^2\to\{0,1\}$,

\alpha\to(\alpha,3)^2

means that there is either a colour-0 subset of order type $\alpha$, or a three-element colour-1 set.

To avoid the live page's $\beta$ conflicting with Schipperus's parameter, write

\beta=\omega^\gamma,\qquad \alpha=\omega^\beta=\omega^{\omega^\gamma}.

An indecomposable summand is an additively indecomposable ordinal $\omega^\delta$. “Three summands” counts repetitions, so the least residual parameter is

\gamma=3=1+1+1,\qquad \beta=\omega^3,\qquad \alpha=\omega^{\omega^3}.

Boundary classification (b). Combining the live page's cited theorems, all nontrivial uncertainty is the family

\gamma=\rho_0+\rho_1+\rho_2 \quad (\rho_i\text{ additively indecomposable}).

Hajnal--Larson's Handbook chapter states this same boundary and records $\omega^{\omega^3}\to(\omega^{\omega^3},3)^2?$ as Question 10.2. This does not say that solving the first case automatically settles every three-summand $\gamma$.

2. Primary-source and current-state audit

2.1 Sources actually checked

Schipperus. I checked the complete archived TeX/PostScript,

not only an abstract: [R. Schipperus, Countable Partition Ordinals][schipperus-source]. The journal version is Annals of Pure and Applied Logic 161 (2010), 1195–1215, DOI [10.1016/j.apal.2009.12.007][schipperus-doi]. Its abstract and Theorem 1 give the one/two-summand positive result. The archived full text contains:

Theorem 37, the Ramsey game dichotomy;
Theorem 41, the large colour-0 set in the Builder branch;
Lemma 47, simultaneous play of three games in the indecomposable case;
Theorem 51, the one/two-summand positive theorem;
Theorem 52, the negative relations for two, three, and at least four

summands.

Section 9 explicitly identifies the simultaneous-game step as the only part sensitive to both the number of indecomposable summands and the finite clique size.

Hajnal--Larson. I checked Section 10 of

[A. Hajnal and J. A. Larson, Partition Relations][handbook], in the Handbook of Set Theory (2010), DOI [10.1007/978-1-4020-5764-9_3][handbook-doi]. Theorem 10.1 gives the one/two-summand result; the text immediately before Question 10.2 says exactly-three summands are what remains; Question 10.2 is the $\omega^{\omega^3}$ case.

Galvin--Larson. The full article and bibliographic record are at

[F. Galvin and J. Larson, “Pinning countable ordinals”][galvin-larson], Fundamenta Mathematicae 82 (1974/75), 357–361.

Chang, Specker, and Darby. I verified that the cited articles exist

with the claimed subjects:

C. C. Chang, “A partition theorem for the complete graph on

$\omega^\omega$,” J. Combinatorial Theory A 12 (1972), 396–452, DOI [10.1016/0097-3165(72)90105-7][chang];

E. Specker, “Teilmengen von Mengen mit Relationen,” *Comment. Math.

Helv.* 31 (1956/57), 302–314, [EuDML record and scan][specker];

C. Darby, “Negative Partition Relations for Ordinals

$\omega^{\omega^\alpha}$,” J. Combinatorial Theory B 76 (1999), 205–222, DOI [10.1006/jctb.1999.1903][darby]. Its primary abstract states the decomposability-dependent $n=4$ or $n=6$ negative theorem.

Later corroboration. Džamonja, Koutsoukou-Argyraki, and Paulson's

[Formalising Ordinal Partition Relations Using Isabelle/HOL][formal], arXiv:2011.13218, was published in Experimental Mathematics 31 (2022), 383–400. It names Schipperus's one/two-summand theorem and calls the remaining positive extension open. Its wording “at least three summands” is looser than Schipperus's known negative theorem for four or more, so I do not use that wording to define the exact boundary.

2.2 Search miss, stated narrowly

Current-search conclusion (c). I searched the exact relation $\omega^{\omega^3}\to(\omega^{\omega^3},3)^2$, the exact title and DOI of Schipperus's paper, later citation records, and the 2025 Komjáth [Erdős--Hajnal problem-list update][komjath]. I found no primary paper claiming a resolution. The 2025 paper exists and cites Schipperus, but its accessible abstract/reference page alone does not establish anything more specific. This is a documented search miss, not a proof that no unpublished work exists. The 2026 live page remains authoritative for status.

3. A clean reduction to the exact missing lemma

Schipperus represents $\omega^{\omega^\gamma}$ by a well-order $(W_\gamma,<)$ of finite labelled trees. A game builds a “good” ordered pair $(T,S)\in[W_\gamma]^2$. Builder supplies increasingly large finite labels; Architect chooses specified structural moves. A complete Builder win is colour 0, while a complete Architect win is colour 1.

For a winning Architect strategy $\sigma$ on an infinite $H\subseteq\omega$, define the strategy-output graph

E_\sigma=\bigl\{\{T,S\}:\text{some legal complete play, with Builder sufficiently large in \(H\) and Architect following \(\sigma\), outputs \((T,S)\)}\bigr\}.

By “winning,” $E_\sigma$ is a subgraph of the colour-1 graph.

Three-strategy-amalgamation lemma (the missing statement)

For every

\gamma=\rho_0+\rho_1+\rho_2

with indecomposable $\rho_i$, every infinite $H$, and every winning Architect strategy $\sigma$ on $H$, the graph $E_\sigma$ contains a triangle.

Equivalently, there must be $T_0<T_1<T_2$ such that each of the three pairs is the output of a legal play against the same strategy. Each shared tree $T_i$ carries two game labellings, one for each incident pair, and the labellings must describe the same underlying tree. In particular their maxima, successor counts, nested $G$-sets, allowed splitting nodes, collapsing ladders, and prefix order must all agree where the game rules require agreement.

Conditional reduction (b). The three-strategy-amalgamation lemma for a fixed $\gamma$ implies

\omega^{\omega^\gamma}\to (\omega^{\omega^\gamma},3)^2.

Proof. Apply Schipperus Theorem 37 to an arbitrary colouring of $[W_\gamma]^2$. It gives an infinite $H$ and one of two branches.

If every sufficiently large Builder play wins, Theorem 41 constructs

$X\subseteq W_\gamma$ of order type $\omega^{\omega^\gamma}$ with every pair colour 0.

If Architect has a winning strategy $\sigma$, the missing lemma gives

a triangle in $E_\sigma$, hence a colour-1 triangle.

These are exactly the alternatives in the arrow relation. $\square$

This reduction removes the arbitrary colouring from the unresolved branch: the remaining question is a uniform compatibility theorem for output graphs of legal strategies. Schipperus's Lemma 47 proves the required three-game scheduling when $\gamma$ is indecomposable. Its crucial root move explicitly uses the condition $\gamma(0)=0$, available in that case; Theorem 51 then obtains the published one/two-summand range with the Erdős--Milner theorem. The source contains no schedule satisfying all three pairwise prefix constraints at three independent summand scales.

Uniformity warning (a). Producing a triangle for one strategy, one finite truncation, or one prescribed interleaving would not prove the missing lemma. Its quantifiers range over every winning strategy and unbounded finite labels in $H$. A finite search would need an additional finite-basis/compactness theorem connecting all bounded states to the transfinite game.

4. Exact block-word relaxation

The simultaneous-game proof contains two conceptually different layers:

the alternating order in which the two trees' partition blocks occur;
whether those blocks can be realised by the same three nested trees.

I isolated layer 1 as a finite model.

4.1 Definition

A pair pattern is an odd alternating word

P=A_{p_0}B_{p_1}A_{p_2}\cdots B_{p_{2m-1}}A_{p_{2m}}.

A global word consists of events $A_i,B_i,C_i$. For an ordered pair, delete events owned by the third object, encode the smaller object as role $A$ and the larger as role $B$, and compress every maximal same-owner run to its final level label. The word triangle-amalgamates $P$ if all three compressed pair projections equal $P$.

This definition intentionally forgets tree nodes, ancestry, successor counts, and collapsing maps.

4.2 Closed-form triangle

Lemma (a). Every such $P$ satisfying

p_0=p_1,\qquad p_{2m-1}=p_{2m}

has a block-word triangle.

For $m\geq2$, an explicit word is

\begin{aligned} &A_{p_0}B_{p_1}C_{p_1}\\ &\quad\prod_{r=1}^{m-1} \left(A_{p_{2r}}B_{p_{2r}}C_{p_{2r+1}}B_{p_{2r+1}}\right) A_{p_{2m}}. \tag{1} \end{aligned}

For $m=1$, use

A_{p_0}B_{p_1}C_{p_1}B_{p_2}A_{p_2}.

Proof.

The $AB$-projection of (1) consists of the initial

$A_{p_0},B_{p_1}$, then $A_{p_{2r}}$ followed by two consecutive $B$-events whose final label is $p_{2r+1}$, and finally $A_{p_{2m}}$.

Deleting all $B$-events leaves the $AC$-projection exactly equal to

$P$.

In the $BC$-projection, the initial $B$ has the required first role-A

label because $p_1=p_0$. Across adjacent product factors, the last $B$-event of one and first $B$-event of the next coalesce; its final label is the next even-indexed $p_i$. The last $B$-run has the required label because $p_{2m-1}=p_{2m}$.

Thus all three compressed projections are $P$. The $m=1$ check is the same three-line projection, with the two endpoint equalities forcing all three needed labels. $\square$

The endpoint equalities hold in both of Schipperus's relevant negative patterns.

For the three-summand $K_4$-obstruction pattern

\[ P_3=A_3B_3A_1B_3A_2B_3A_1B_3A_3, \]

formula (1) gives the explicit triangle word

\boxed{ A_3B_3C_3A_1B_1C_3B_3A_2B_2C_3B_3A_1B_1C_3B_3A_3}.

Interpretation (a+b). Schipperus's Theorem 52 says the actual three-summand tree pattern has no $K_4$, and the four-summand pattern

\begin{split} P_4={}&A_4B_4A_1B_1A_1B_1A_3B_2A_1B_2A_4\\ &B_2A_1B_2A_3B_1A_1B_1A_1B_4A_4 \end{split}

has no triangle. Yet the block-word model gives a triangle for $P_4$ by the lemma, and the exhaustive automaton even gives a $K_4$ for $P_3$. Therefore pairwise block order and level labels alone are provably insufficient. Any valid proof or counterexample must retain the shared trees' prefix/splitting compatibility.

4.3 Independent exhaustive check

The standalone checker performs breadth-first search in the complete finite automaton. A state records, for every pair, its current pattern block and the last label in that block. It independently projects and recompresses every returned certificate.

Computational result (d).

| pattern length | patterns tested | triangle-SAT | maximum BFS states | |---:|---:|---:|---:| | 3 | 1 | 1 | 25 | | 5 | 3 | 3 | 121 | | 7 | 27 | 27 | 394 | | 9 | 243 | 243 | 949 | | 11 | 2187 | 2187 | 1879 |

The sweep contains every alternating three-level pattern of the indicated length for which the first and last occurrence of each role has label 3. Those constraints are exactly $p_0=p_1=p_{2m-1}=p_{2m}=3$. The script checks both the closed formula and an independent BFS for every row.

Negative controls:

$P_3$, three objects: SAT, a shortest returned word has length 16;
$P_3$, four objects: SAT in the relaxation, length 23, 18,244 states

visited, despite the genuine ordinal $K_4$ obstruction;

$P_4$, three objects: SAT in the relaxation, length 36, 6,945 states

visited, despite the genuine ordinal triangle obstruction.

The two negative-control certificates are, respectively,

A3 B3 C3 D3 A1 B1 C1 D3 C3 B3 A2 B2 C2 D3 C3 B3 A1 B1 C1 D3 C3 B3 A3
A4 B4 C4 A1 B1 C1 A1 B1 C1 A3 B3 C2 B2 A1 B1 C2 B2 A4 B4 C2 B2 A1 B1 C2 B2 A3 B3 C1 B1 A1 C1 B1 A1 C4 B4 A4

These controls prevent the finite computation from being mistaken for an ordinal theorem.

5. Why a direct faithful computation stalls

Exact mathematical wall (b). The missing assertion is the three-strategy-amalgamation lemma in Section 3. More concretely, the unknown step is a schedule that synchronises, on each of three shared trees, the two legal game histories incident with that tree while preserving all nested prefix and collapsing-ladder constraints at each of three indecomposable summand scales.

Needed finiteness lemma (c). A useful computational attack would first need a canonical finite quotient of simultaneous legal game positions with:

transitions preserving the two labellings on every shared tree;
a proof that quotient states cover arbitrarily large labels in $H$;
a well-quasi-order, compactness, or finite-obstruction theorem making

bounded UNSAT/SAT conclusions uniform over all strategies.

Without item 3, no depth or branching cutoff can settle the ordinal statement.

To quantify why naive enumeration is inappropriate, define a toy class of ordered rooted shapes by

S_b(0)=1,\qquad S_b(d+1)=\sum_{j=1}^{b} S_b(d)^j.

This is not $W_\gamma$; it merely counts exact-depth shapes with between one and $b$ ordered children at each internal node.

Toy count (a).

| branch cap $b$ | $S_b(0),\ldots,S_b(3)$ | triples $S_b(3)^3$ | equal-size leaf interleavings | |---:|---:|---:|---:| | 2 | $1,2,6,42$ | 74,088 | $24!/(8!)^3=9,465,511,770$ | | 3 | $1,3,39,60,879$ | 225,632,954,531,439 | $81!/(27!)^3\approx4.4902\cdot10^{36}$ | | 4 | $1,4,340,13,402,779,940$ | $2.4076\cdot10^{30}$ | $192!/(64!)^3\approx1.7377\cdot10^{89}$ |

Even ignoring all labelings and interleavings, the $b=3$ shape triples take over 62,675 core-hours at an optimistic one million triples/second (about 7.15 core-years). This estimate is elementary arithmetic, not a claimed lower bound for every possible algorithm. I did not run any such search. A faithful attack needs symmetry reduction and a uniformity theorem before SAT, not more brute force.

6. Reproducibility

Standalone checker:

runs/erdos592_wavew000_verify.py

Run from the repository root:

python runs/erdos592_wavew000_verify.py

Observed on this VM:

Coarse block-word certificates (NOT ordinal certificates):
  P3 triangle: length=16, visited=493, closed-form-length=16
    A3 B3 C3 A1 B1 C3 B3 A2 B2 C3 B3 A1 B1 C3 B3 A3
  P3 K4 negative control: length=23, visited=18244
    A3 B3 C3 D3 A1 B1 C1 D3 C3 B3 A2 B2 C2 D3 C3 B3 A1 B1 C1 D3 C3 B3 A3
  P4 triangle negative control: length=36, visited=6945, closed-form-length=40
    A4 B4 C4 A1 B1 C1 A1 B1 C1 A3 B3 C2 B2 A1 B1 C2 B2 A4 B4 C2 B2 A1 B1 C2 B2 A3 B3 C1 B1 A1 C1 B1 A1 C4 B4 A4
Exhaustive three-level alternating-pattern sweep:
  length  tested  triangle-SAT  max-BFS-states
       3       1             1              25
       5       3             3             121
       7      27            27             394
       9     243           243             949
      11    2187          2187            1879
Toy exact-depth-3 ordered-shape counts:
  b=2: S=(1, 2, 6, 42), leaves=8, S(3)^3=74088, multinomial=9465511770, shape-only-hours@1e6/s=2.058e-05
  b=3: S=(1, 3, 39, 60879), leaves=27, S(3)^3=225632954531439, multinomial=4490186382903298862950669893074864640, shape-only-hours@1e6/s=62675.8
  b=4: S=(1, 4, 340, 13402779940), leaves=64, S(3)^3=2407601808768952985638023784000, multinomial=173769574576495682336776543913345076449313300929448789599626442561155990662132131755196250, shape-only-hours@1e6/s=6.68778e+20
Elapsed seconds: 12.353
ALL CHECKS PASSED

The code uses only the Python standard library. It derives the state graph from the pattern definition; there are no stored SAT answers or external certificates.

7. Claim ledger and conclusion

(a) The block-word construction (1), its projection proof, the endpoint

conditions, and the toy counting arithmetic are from-scratch results.

(b) The exact residual family and the game reduction rely explicitly on

Galvin--Larson and Schipperus Theorems 37, 41, 51, and 52.

(c) The literature miss, proposed finite quotient, and algorithmic

interpretation are not theorems.

(d) The table and BFS certificate lengths apply only to the explicitly

defined block-word relaxation.

[schipperus-source]: https://users.math.cas.cz/~jech/library/schipperus/countable.tex [schipperus-doi]: https://doi.org/10.1016/j.apal.2009.12.007 [handbook]: https://people.clas.ufl.edu/jal/files/jal30g.pdf [handbook-doi]: https://doi.org/10.1007/978-1-4020-5764-9_3 [galvin-larson]: https://eudml.org/doc/214674 [chang]: https://doi.org/10.1016/0097-3165(72)90105-7 [specker]: https://eudml.org/doc/139143 [darby]: https://doi.org/10.1006/jctb.1999.1903 [formal]: https://arxiv.org/abs/2011.13218 [komjath]: https://doi.org/10.1017/bsl.2025.1

PARTIAL: Reduced every unresolved positive instance to uniform three-way amalgamation of Schipperus game strategies, and proved that every endpoint-compatible alternating block pattern triangle-amalgamates (with exhaustive negative controls)—so the exact remaining obstruction is shared-tree prefix/splitting compatibility.

This is the AI working report, labelled by outcome — not an independently verified claim unless marked PROVED. ← ledger