Define

with \(R(r,k)=\infty\) if there is no such \(N\). Then the live problem is equivalent to

(a)

Proof: if all these thresholds are finite, restrict an arbitrary \(r\)-colouring of \(\mathbb N\) to \([R(r,k)]\) for each \(k\). Conversely, if avoiding colourings of every \(\mathcal H_{N,k}\) exist for some fixed \(r,k\), arrange them in the finitely branching tree whose parent map is restriction from \([N+1]\) to \([N]\). Every level is nonempty, so König's lemma gives an infinite \(r\)-colouring with no \(k\)-element witness. Finally, witnesses of unbounded size are equivalent to witnesses of every exact size because every subset of a witness is a witness. (a)

This isolates the remaining task exactly: prove a finite obstruction for every \((r,k)\), or construct one infinite avoiding branch. (a)

3. Verified finite results

With the convention above, the computation proves

The first equality is elementary; the other equality and the lower bound are computational-only. (a)/(d)

3.1 The pair case is ordinary graph colouring

When \(k=2\), every hyperedge is the pair \(\{x+y,xy\}\). Let \(G_N\) be the ordinary graph on \([N]\) with those pairs as edges for distinct \(x,y\) and with both values at most \(N\). Thus \(R(r,2)\) is the first \(N\) with \(\chi(G_N)>r\). (a)

For \(N=7\), \(G_7\) is the path

plus isolated vertex \(1\), so it is two-colourable. At \(N=8\), vertices \(6,7,8\) form a triangle: its edges arise respectively from

Hence \(R(2,2)=8\). (a)

For three colours, the checker constructs \(G_{99}\) with 230 edges and validates this explicit colouring of vertices \(2,\ldots,99\):

10101201021202120101021012010121021202120101212102120212010120121202021201010121012101010101021202

It constructs \(G_{100}\) with 234 edges and exhaustively proves that no three-colouring exists. The new vertex has neighbourhood

with witnesses \((5,20),(4,25),(2,50),(1,99)\). The independent standard-library DSATUR search uses saturation degree, ordinary degree, and a fixed vertex tie-break; it explores unused colours only up to permutation. It finds the \(G_{99}\) colouring in 152 recursive calls and exhausts \(G_{100}\) in 148 calls. Thus \(R(3,2)=100\). This upper certificate is exact but computer-assisted, not a hand proof. (d)

3.2 An explicit two-colouring through 5000 avoiding every triple

For \(a \[ \Phi(\{a,b,c\})\subseteq[N]\quad\Longleftrightarrow\quad bc\leq N. \tag{3.2} \]

The number of triples to check is therefore

At \(N=5000\), this is exactly \(210{,}497\). (a)

The file erdos172_wave5l_reverify.py embeds an explicit 5000-bit colouring, compressed losslessly as a base85/zlib constant. Its uncompressed SHA-256 is

a8599f44248a5ff52c954f4ee2e7b0687dd73eafed89545ecb40081d170b682b

It has 3,980 zeros and 1,020 ones. Direct enumeration confirms that every one of the 210,497 footprints contains both colours; 209,919 footprints have six distinct values and 578 have five. Consequently \(R(2,3)>5000\). (d)

The model was discovered from the exact not-all-equal CNF. If \(z_v\) is the colour bit of \(v\), each footprint \(E\) contributes

The discovery instance had 5,000 variables and 420,994 clauses. The recorded model was found in 44.6 seconds on this VM. The essential generator was:

clauses = []
for b in range(2, N + 1):
    for c in range(b + 1, N // b + 1):
        for a in range(1, b):
            edge = sorted({
                a + b, a + c, b + c,
                a * b, a * c, b * c,
            })
            clauses.append(edge)
            clauses.append([-v for v in edge])

SAT is used only for discovery. The run used PySAT 1.9.dev7 with its cadical195 backend (CaDiCaL 1.9.5). The final verifier contains no SAT library and checks the decoded colouring against all triples from scratch. (d)

4. Independent reproduction

Run:

$ python runs/erdos172_wave5l_reverify.py --sources
Triple certificate passed: N=5000, triples=210497, footprint sizes={5: 578, 6: 209919}, 0/1 counts=3980/1020.
Pair thresholds passed: R(2,2)=8 (G7/G8 edges 5/7; UNSAT calls 6); R(3,2)=100 (G99/G100 edges 230/234; SAT/UNSAT calls 152/148).
ALL MATHEMATICAL CHECKS PASSED
Primary-source TeX/metadata checks passed.
ALL SOURCE CHECKS PASSED

The mathematical run takes under one second here. Source mode re-downloads six arXiv source archives and Hindman's Crossref record; it does not attempt to bypass Cloudflare or silently substitute a cached Erdős Problems page. (d)

5. Exact wall and next computation

The rational theorem does not transfer by simply clearing denominators. If \(q_i\in\mathbb Q\) and \(Dq_i\in\mathbb Z\), then for \(b_i=Dq_i\),

Thus sums and products land in two different dilation scales. Alweiss's rational colouring theorem supplies no compatibility between an arbitrary natural-number colouring at the \(D\) and \(D^2\) scales. A sufficient missing ingredient would be a denominator-synchronisation lemma that produces the rational configuration and a common \(D\) while forcing the original colouring to agree on all these linearly and quadratically scaled values. No such lemma was found. (a)/(c)

The two-variable Moreira/Bowen machinery likewise controls selected sums and products, not the simultaneous complete graph of \(\binom{k}{2}\) pairs. The exact missing combinatorial statement is already the first unsettled finite target \(R(2,3)<\infty\). Our certificate only pushes its lower bound past 5000; it gives no infinite colouring and no evidence that the threshold is infinite. (a)/(c)/(d)

For scale, \(N=7500\) has 393,628 hyperedges and 787,256 clauses; a CaDiCaL decision run was stopped unresolved after about 75 seconds. At \(N=100{,}000\), (3.3) gives 20,424,017 hyperedges, 40,848,034 clauses, and up to about 245 million literal occurrences. That is roughly 0.91 GiB for raw 32-bit literals alone and several times more with solver/Python overhead. A modest next portfolio of 16 cores for two hours would cost 32 core-hours, about US$1.60–$3.20 at US$0.05–$0.10 per vCPU-hour, but has no guaranteed outcome; an UNSAT certificate could be much more expensive. I did not run that heavier search here. (d)/(c)

The finite pair thresholds do not address unbounded \(|A|\), and the \(N=5000\) colouring is not a counterexample on \(\mathbb N\). The live problem remains open. (a)/(d)

PARTIAL: Reduced the problem exactly to finite weak hypergraph colouring, proved R(2,2)=8, computationally certified R(3,2)=100, and supplied a solver-free-verified 2-colouring of [5000] showing R(2,3)>5000; no uniform or infinite conclusion.