#160: the two upper-bound claims on the tab, refereed — Shi–Dong's h(N) ≤ N^{1/4+o(1)} holds as read, their 27p-colouring of ℤ/p⁴ℤ verified exhaustively for p ≤ 13; Itabe's N^{1/3+o(1)} kernel-replays green; and h(N) computed exactly for N ≤ 51
The problem (erdosproblems.com/160, OPEN, Erdős 1989, investigated with Freud). Let h(N) be the least k such that {1, …, N} can be coloured with k colours so that every four-term arithmetic progression contains at least three distinct colours. Estimate h(N). (Erdős's own wording counts the largest number of parts for which every partition has two parts whose union holds a 4-AP; that is h(N) − 1 for N ≥ 4 — Itabe proves the shift in Lean, §9 of his manuscript. Everything below uses the page's h.) The page records h(N) ≪ N2/3 (LeechLattice on MathOverflow, December 2021: partition Fp³ into the p² translates of a twisted cubic, project to ℤ and shift, which covers [0, 8p³) with 8p² classes), h(N) ≪ Nlog 3/log 22 + o(1) ≈ N0.355 (Zach Hunter, comment of 18 October 2025, from Deng–Tidor–Zhao's 3-colouring of ℤ/22ℤ), and h(N) ≫ exp(c(log N)1/9) from the Bloom–Sisask 3-AP bound via Hunter's observation (MO 410808, 2021): a colour class restricted to [N/4, 3N/4] must be 3-AP-free (its 3-AP extends to a 4-AP inside [N] with three equal colours). The page was last edited 2 December 2025 and records none of what follows.
The claims on the tab. We read the live page and both forum tabs first (13 October, through our Hetzner box). The proof-claims tab carries two entries,
and the comments tab a third claim. (1) Rio Itabe, "A candidate N1/3+o(1) upper bound for Erdős Problem 160", manuscript dated 14 July 2026,
posted to the tab 15 July (repository ritabe-dev/ErdosProblem160-OneThirdUpper, tag v0.2.1-review-candidate, commit fd426c9; "using GPT-5.6"):
h(N) ≤ N1/3+ε for every ε > 0 and all large N, explicitly, for every integer k ≥ 1, h(N)3k < 2,985,984k Nk+3
for N > max(2(76k)², 2(40k)⁴), with a Lean 4 development of the whole chain; the author claims no priority and calls it unreviewed.
(2) Ruizhe Shi and Yiqi Dong, "An improved upper bound for colorings without symmetrically colored k-term arithmetic progressions",
arXiv:2607.20752 (v1 22 July, v2 28 July 2026, 7 pages; posted to the tab 24 July by ruizshi; "using GPT 5.6 Sol"): for every even k ≥ 4 and prime p > k
a (k−1)k²/4−1p-colouring of ℤ/pk²/4ℤ with no nontrivial symmetrically coloured k-AP, hence
Ok(N4/k²) colours on [N]; for k = 4 a 27p-colouring of ℤ/p⁴ℤ and
h(N) ≤ N1/4+o(1) (Corollary 1.3); and, through Deng–Tidor–Zhao's transference, ρ₄(α) = Oε(α5−ε)
toward Ruzsa's question and the first counterexamples to Gowers's conjectured lower bound αk for the k-AP density of a
Uk−2-uniform set, for every even k ≥ 6 (Corollaries 1.4–1.5). They cite Itabe as "a concurrent result … to claim an intermediate
O(N1/3) upper bound". (3) On the comments tab (ruizshi, 4 August 2026): the lower bound improves to exp(c(log N)1/6−o(1))
by the same reduction from Rushil Raghavan's March 2026 preprint arXiv:2603.27045, |A| ≤ exp(−c(log N)1/6/log log N)·N for 3-AP-free
A ⊆ [N]. This entry is our referee report on (1) and (2); (3) we checked only as far as the reduction, which is elementary.
The idea both papers share, in one paragraph. A 4-AP using at most two colours has, up to renaming, one of eight patterns: AAAA, AAAB, AABA, ABAA, BAAA, AABB, ABAB, ABBA. Hunter's observation is that Behrend-style digit colourings with No(1) colours kill all but the last: the four "three equal" patterns are weighted three-term relations (x + z = 2y, 2x + z = 3y, x + 2z = 3y), which a sphere-of-digits colouring avoids (Deng–Tidor–Zhao Lemma 3.2); ABAB and AABB each say a quadratic t ↦ ‖u + tv‖² has two axes of symmetry, so v = 0 (DTZ Lemma 7.11 for ABAB; Shi–Dong's Lemma 5.3 and Itabe's §5 for AABB, both with a dyadic bucket label to keep the base-M digits from wrapping; Itabe's §4 handles the three-equal patterns and ABAB together with one mod-24 label). What is left is the symmetric pattern ABBA — c(a) = c(a+3d), c(a+d) = c(a+2d) — which is exactly Deng–Tidor–Zhao's Conjecture 1.6 (an No(1)-colouring of [N] without symmetrically coloured 4-APs exists for every N), for which their best construction was the ℤ/22ℤ tensor power. Both new papers kill ABBA with the same two moves. First, write n in base p and record, for each digit but the top one, which third of [0, p) it lies in, τ(x) = ⌊3x/p⌋: if a 4-AP has the ABBA pattern in τ at every digit, the carries at each digit are all equal (Shi–Dong Lemma 2.1; Itabe Lemma 7.1, "thirds no-wrap"), so the digit vectors themselves form an arithmetic progression x, x+h, x+2h, x+3h in FpL with h ≠ 0 whenever d ≠ 0. Second, add one more coordinate, a polynomial Q on FpL whose restriction to the line, g(t) = Q(x+th), has degree ≤ 3: ABBA in Q says g(0) = g(3) and g(1) = g(2), i.e. g(3/2 + t) is even, so the t³ coefficient vanishes — and if that coefficient is the field norm NFp³/Fp(h), which is zero only at h = 0, the progression was trivial. Itabe takes L = 3 and Q = the norm itself: 9p colours on [0, p³), so p ≈ N1/3. Shi–Dong take L = 4 and Q(x) = x₀ + N(x₁, x₂, x₃): the t³ coefficient still forces the norm part of h to vanish, and once it has, the t¹ coefficient of the (now even) polynomial forces h₀ = 0 — one dimension for free, 27p colours on ℤ/p⁴ℤ, p ≈ N1/4. For even k the same descending induction runs through norm layers of degrees 1, 3, …, k−1 in 1 + 3 + ⋯ + (k−1) = k²/4 dimensions, with p > k so that the k/2 symmetry conditions give a degree-(k−1) polynomial k distinct roots (Lemma 4.1); their Remark 4.2 suggests, by Chevalley–Warning, that a constant-degree polynomial in this framework should not gain more than Ok(1) dimensions over k²/4 — a heuristic, in their own words "one should not expect". The two constructions are one construction: Itabe's cubic factor is, up to the choice of Fp-basis, Shi–Dong's k = 4 colouring restricted to the subgroup pℤ/p⁴ℤ ≅ ℤ/p³ℤ — the slice x₀ = 0, on which the linear layer vanishes — down to the same τ. Shi–Dong's additions are the degree-1 layer with its extra digit (1/3 → 1/4), the odd-layer generalisation to every even k, the general-k carry lemma, and the cyclic formulation that feeds Deng–Tidor–Zhao's transference.
What we did (the bar). (i) Reading. The host seat read every lemma of both papers against its proof, with the boundary cases named: in Shi–Dong's Lemma 2.1 the
step to interval i − 1 or i + 1 needs k − 1 ≥ 3 intervals (it has them), the step s = 0 and the exact boundary s = (k−2)p/(k−1) (not an integer for
prime p > k) are harmless, a wrap would move a digit from the top interval to the bottom one and so always changes τ; in Lemma 2.2 the top digit needs no τ because
nothing carries out of it; in Lemma 4.1 the k roots {−a, …, k−1−a} are distinct because p > k (p ≥ k would already do), and the coefficient of
tr in g(a+t) is Pr(v(r)) by homogeneity once the higher layers are constant; in Lemma 5.3
the bucket τ₂(x) = ⌊log₂(M−x)⌋ puts x = M/2 in the same bucket as 0 < x < M/2, but a carry from M/2 forces s = M/2 and
lands on 0, whose bucket is different, so the argument survives; and the eight-pattern case analysis that the proof of Corollary 1.3 leaves implicit goes through. The elementary lower-bound reduction (3) we checked
ourselves: a 3-AP x, x+d, x+2d in one colour inside [N/4, 3N/4] has d ≤ N/4, so x+3d ≤ N.
(ii) Two implementations of the 27p-colouring, every progression enumerated. A Python checker (irreducible cubic found by brute force, norm computed as z1+p+p²
in Fp[T]/(f)) and a C checker (a different irreducible cubic, found by a search from the top of the coefficient range; norm computed as the determinant of the
3×3 multiplication matrix) each build Shi–Dong's colouring of ℤ/p⁴ℤ and test every pair (a, d), d ≠ 0 — the Python checker for p = 5, 7, 11, the C checker for p = 5, 7, 11, 13 (up to
28,561 × 28,560 ≈ 8.2·10⁸ progressions), and seat B's own third implementation for p = 5, 7, 11, so every p ≤ 11 has at least two independent implementations and p = 13
the C checker alone: zero symmetrically coloured 4-APs; the palette within 27p throughout, attained in full at p = 11 and 13 (297, 351) and by the C checker's cubic at
p = 7 (189), while the Python checker's cubics leave 10 of 135 and 2 of 189 colours unused at p = 5, 7 (which colours are attained depends on the cubic); and three controls each find violations: drop
the Q coordinate; replace the norm by the isotropic cubic x₁³; drop τ on one digit. The norm's anisotropy is itself checked by enumeration before any colour is assigned. Both
implementations are independent of the paper's text beyond the definitions. (iii) The general-k theorem, sampled. For k = 6, p = 7 the colouring of
ℤ/7⁹ℤ (40,353,607 residues, 5⁸·7 = 2,734,375 colours, layers of degrees 1, 3, 5 with irreducible T³+2 and T⁵+T+3) was built in full and tested on 10⁸ random 6-APs
and on every d from three random starting points (121,060,818 more): none symmetrically coloured; the control with Q dropped finds 13 in 10⁸. This exercises a third layer (a degree-5 norm), which k = 4 does not; it is a sample, not a proof. (iv) Itabe's three labels by brute force. His cubic factor (τ of the two low digits + norm) on
[0, p³) for p = 5, 7, 11, with a randomly chosen irreducible cubic each time: zero proper-ABBA progressions, also on the cyclic
group ℤ/p³ℤ as Shi–Dong's theorem predicts, palettes 35, 55, 91 ≤ 9p, controls fire; his mod-24 label (digits mod 24 + squared norm, P = 25 and 49, up to 15,625 residues):
no three-equal pattern and no ABAB, and with the digit labels removed ABAB appears on every horizon, but the three-equal control fires only at L = 2 — at L = 1 the square norm alone admits no three-equal pattern — so our
checker reports "cannot see" on that row, and seat D's modulus-4 rerun below is the evidence that counts; his dyadic label (B = 4, 8, 16, up to 4,096): no AABB, and without the buckets AABB appears.
(v) Kernel replay of Itabe's Lean. Clone at the tag, Lean v4.30.0 and Mathlib v4.30.0 — his own pins; the Mathlib cache step took three minutes (a tagged release, and the oleans were already on this box) —
then his own check_release.sh built all 21 first-party modules from source and ran his AxiomAudit.lean (174 s for build, audit and scans together; the from-source build is the kernel
check of his modules — Mathlib's own oleans stay trusted until the leanchecker pass below), and our re-run of that audit: eight of the nine audited endpoints depend on exactly
[propext, Classical.choice, Quot.sound], and the ninth, the displayed-threshold identity, on propext and Quot.sound alone; his check_release.sh passes end to end; our own probe prints
the endpoint's full type with pp.all — for every real ε > 0, eventually (siteH N : ℝ) ≤ N1/3+ε — and unfolds siteH to the least k for which
there is a colouring Icc 1 n → Fin k under which every set {a + id : i < 4} ⊆ [1, n] with d > 0 has image of cardinality ≥ 3 — the page's
h(N), and the Formal Conjectures statement up to its IsAPOfLength 4 predicate; a negative control (a sorry'd theorem about siteH) prints sorryAx;
a scan of the first-party sources finds no sorry, admit, axiom, native_decide, implemented_by, extern, unsafe,
partial or opaque. A leanchecker --fresh pass over the full Mathlib import closure (ErdosProblems.E160.RealAsymptotics) exited 0 after 3,125 s (52 min); its controls: a non-existent module exits 1 (“Could not find any oleans”), the non-fresh pass over Problem exits 0.
(vi) Four hostile Opus seats with tools, each told to refute and to quote the sentence it objects to: one on Shi–Dong §§2–5 and the Erdős-160 reduction, one on their §6 (the
Deng–Tidor–Zhao transference and the Gowers claim) and on priority and the live literature, one on Itabe's Lean sources and the statement match, one on Itabe's prose. Seat A (Shi–Dong §§2–5): holds as read, no fatal objection, two minor gaps and seven exposition notes. Gap 1: the proof of Lemma 2.2 says "iterating
Lemma 2.1", but when a digit of d is p − 1 and the incoming carry is 1 the step at that digit is exactly p, outside Lemma 2.1's range 0 … p−1, and its carry
indicator 1{xi+1 < xi} then reads 0 while the true carry is 1 — at every i, so the carries are still constant and the lemma's
conclusion holds; the case occurs 8,788 times in an exhaustive run at k = 4, p = 13, L = 3, with constant carries in all of them. Gap 2: Lemma 5.3's reason that a carry "would place the corresponding pair on opposite sides of M/2" and so change τ is false in general (τ(M/2) = τ(1)) and true only because the one boundary carry, from M/2, forces s = M/2 and lands on 0 —
the same edge the host read had found. Exposition: §5 announces "we give a proof of this observation" and then cites Lemmas 5.1 and 5.2 without proof (the translation from Deng–Tidor–Zhao's
"k-patterns" — weights (1,1), (2,1), (1,2), (1,1) for the four three-equal patterns — and from Lemma 7.11's ℤ/Nℤ with N = Θ(rC log r) to
r = eO(√log N) on [N] are both routine and both written out in the report); the product step of Corollary 1.3 wants the eight-pattern case analysis made explicit;
§3's displayed formula for the norm has the wrong formal degree as written (the proof needs the product of the t conjugates); Remark 4.2 is a heuristic. Its instruments, each with a firing
control: Lemma 2.1 exhaustively for k ∈ {4, 6, 8, 10, 12} and every prime k < p < 220 (119,277 τ-symmetric digit progressions, 0 violations; with τ cut to two intervals the
lemma fails, so k − 1 ≥ 3 is load-bearing); Lemma 2.2 exhaustively over all (a, d) for (k, p, L) = (4, 11, 3), (4, 13, 3), (6, 29, 2), (8, 53, 2) — the last
two chosen so that carries occur below the top digit, which needs p > 25 at k = 6; Lemma 4.1 exhaustively at k = 4 for p ≤ 13 and at k = 6, p = 7 over all
(y₀, h) ∈ F₇⁹ × F₇⁹ by per-layer histograms (0 nonzero h), with the decisive control that oddness is load-bearing: replace the degree-5 layer by the anisotropic degree-4
norm of F7⁴ and 5,762,400 of the 5,764,800 nonzero directions admit a symmetric 6-AP; the norm forms themselves checked for anisotropy, homogeneity and leading coefficient. Seat B
(§6, Gowers, priority, literature): holds as read — findings folded into the labels and the state of the problem below. Seat C (Itabe's Lean): statement matches. Both
headline theorems take only ε > 0; every hypothesis in the chain is discharged inside the development; the prime comes from Mathlib's Bertrand's postulate and the one global instance is built
from that proof; no decide, maxHeartbeats, custom notation or macros; the +1 bridge is a faithful reading of Erdős's 1989 wording; siteH equals the Formal
Conjectures erdos_160.h for every n, because IsFourTermAP and Set.IsAPOfLength 4 are equivalent on sets of naturals (both exclude d = 0; a set
has no orientation) — an equality that is provable but which the repository does not itself prove, the one link the kernel has not checked. Its own rebuild of the three labels in Python agrees.
Seat D (Itabe's prose): holds as read, twelve exposition notes, nothing fatal: brute-forced Lemma 4.1 for P = 25, 49, 73, 97, 121 (every P = 24B + 1 up to 121) and for its modulus-4, -6 and -3 variants, Lemma 5.1 for every base ≤ 72 and 128
(it holds for any base, not only powers of 2), Lemma 7.1 for every integer 2 ≤ p ≤ 60 (primality is not used), the +1 bridge against brute force for 4 ≤ N ≤ 7, and the full labels in the
regime where they are far from injective (cubic at p = 13, 17 with a random basis; dyadic at B up to 32; the mod-24 label with the modulus replaced by 4, where the proof applies word for word —
palette 3,107 of 6,561, zero violations, and moduli 2 and 3 break it exactly where predicted). Its notes: §2's "projects to an at-most-two tuple in each factor" points at the wrong mechanism (the
classification has to be applied to the product tuple); "AABB-free" and its siblings are never defined (the equality reading, where AAAA also counts, is what the proofs and the Lean deliver); the
second inequality of (6.5) is asserted as elementary without argument (it holds for every m ≤ 3000; the Lean's floor-square-root version is tight at m = 1–3); in the theorem's threshold the first term never binds, since
(40k)⁴ > (76k)² for every k ≥ 1; the modulus 24 (DTZ Lemma 7.11's 4!) is not explained in the text; any even modulus ≥ 4 works. And one note on our own instrument: on every horizon small enough to brute-force,
his mod-24 label is almost injective (624 of 625 colours at P = 25), so our rows for it test little; the modulus-4 rerun is the meaningful evidence, and we say so.
Labels. Shi–Dong, Theorem 1.1 and Corollary 1.2: (a) elementary, and (d) computer-assisted in the sense that the k = 4 colouring is verified exhaustively for p ≤ 13 and the k = 6 colouring sampled. Corollary 1.3 (the N1/4+o(1) bound for #160): (b) rigorous modulo Deng–Tidor–Zhao's Lemmas 3.2 and 7.11 (Math. Proc. Cambridge Philos. Soc. 179 (2025) 79–103, peer-reviewed; Lemma 7.11 is proved there and seat A re-checked it for a = (1, 2, 3, 4); Lemma 3.2 is a sketch there — a Behrend-type pattern-free set after Ruzsa plus random translates, classical — which we did not re-prove). Corollaries 1.4–1.5: (b) modulo DTZ Theorems 1.8 and 2.8 with Proposition 2.4 (both refereed; seat B matched the two displayed inputs to them exactly — exponent, range of α, constant dependence; the notation differs — re-derived the exponent arithmetic, and checked that "exponent above k" refutes Conjecture 1.10 with the quantifiers in DTZ's order; two caveats it names: Gowers's Conjecture 4.2 was read through DTZ's refereed restatement, the GAFA original being paywalled and the 2000 preprint on his site carrying no numbered conjectures, and DTZ's own proof of Theorem 2.8 has βk inverted in its final display while the statement Shi–Dong quote is correct). Two things a reader should know about Corollary 1.5 that the paper does not say: the counterexamples are qualitative — the constant in (2) is unspecified, so ρk(α) < αk holds only below an inexplicit α — and the sentence "choosing ε < (k−2)²/(4(k−1)) makes the exponent larger than the random exponent k" is true only once p is large: for k = 6 the exponent at finite p passes 6 only for p > 5¹⁰ ≈ 10⁷ (at p = 7 it is 5.24). The "first counterexample for every even k ≥ 6" claim held up under everything seat B could check: Deng–Tidor–Zhao's own local-lemma colouring gives exponent k − 1 + k/(2(k−1)) < k, the k = 4 colouring alone (every symmetric k-AP contains a symmetric 4-AP) gives k − 1 + 4/(k−1) < k for k ≥ 6 — the criterion is r = Mθ with θ < 1/(k−1), and 4/k² clears it where 1/4 does not — Gowers's 2020 paper covers k = 4 only, and its closing remark about Ruzsa's counterexample for longer progressions concerns Fourier-uniform sets, not Uk−2-uniform ones. On the related construction they cite: Führer's March 2024 layered polynomial (the 2024 version of [FT24] is single-author, with a different title; Taranchuk joined the February 2026 revision) sums norms of every degree 1, …, t in t(t+1)/2 dimensions to make line-evasive sets, and that colouring is not free of symmetric 4-APs (seat B's counterexample: direction (0, v₂, 0) with u₂ = −(3/2)v₂ makes Q a quadratic symmetric about 3/2); Shi–Dong's parity step run across every odd layer — symmetry forces an even polynomial, so only odd layers are needed — is what is new relative to Führer, and it is what gets k²/4 dimensions instead of k(k−1)/2; Itabe's §7.2 uses the same symmetry for the single cubic layer. Lemma 4.1's descending top-coefficient induction is Führer's (after Lin–Wolf). On priority: Itabe's manuscript and Lean were public on 14 July, eight days before Shi–Dong's v1 (22 July, which cites neither Itabe nor Führer); v2 (28 July) calls Itabe "a concurrent result", and ruizshi's own comment under Itabe's claim (24 July, 01:38) says: "it was not until I posted our latest 1/4 result … that I realized there was already a 1/3 argument in this comment. To be honest, while developing our result, we were inspired by a 1/3 bound suggested by GPT-5.6 Sol. Therefore, I am not entirely sure whether our result may have been indirectly influenced by this comment", adds that an idea suggested by an LLM is hard to attribute precisely, and promises to cite the comment in a future version — which v2 did, four days later. The intro's "strongest previously known upper bound" (0.355) was left unchanged in v2. Itabe: (d) kernel-checked for the whole chain from the colouring to the eventual N1/3+ε bound and the +1 bridge, and (a) elementary in the prose. What no instrument here reaches: the k = 4 colouring itself beyond p = 13 — the primes the N1/4+o(1) corollary actually uses — Shi–Dong's general-k theorem at k ≥ 8, and at k = 6 for the non-degenerate primes p ≥ 29 (where carries can occur below the top digit) and for the p > 5¹⁰ the Gowers corollary needs — there the result is carried by the reading of two p-uniform lemmas (seat A checked Lemma 2.2 exhaustively at k = 6, p = 29 on two digits and Lemma 4.1 exhaustively at k = 6, p = 7), not by enumeration.
Exact values (ours). Nobody seems to have written down h(N) for small N (the page says "OEIS: possible"; a terms search on 13 October returns nothing). A SAT encoding per (N, k) — one-hot colours, an indicator yn,{c,c′} for "n is coloured c or c′", and for every 4-AP and every pair of colours the clause that not all four terms are in the pair — solved by CaDiCaL, each satisfying assignment re-verified by an independent checker, and the thresholds (13, 3) and (23, 4) re-proved UNSAT on a second solver (Glucose 4) under a second encoding (six equality indicators per progression and the seven forbidden two-colour patterns), gives h(N) = 3 for 4 ≤ N ≤ 12, 4 for 13 ≤ N ≤ 22, 5 for 23 ≤ N ≤ 35, and 6 for 36 ≤ N ≤ 51 (the search stopped at (52, 6) on its 900-second cap, so h(52) ∈ {6, 7} is undecided; the UNSAT at (36, 5) took CaDiCaL 764 s and was re-proved after this went live by Glucose 4 under the second encoding — 3,072 variables, 11,905 clauses, UNSAT — on the same run that found (35, 5) SAT with its witness re-verified, so every threshold in the table now rests on two solvers and two encodings). A good 3-colouring of [12]: 0 0 1 2 1 0 2 1 0 1 2 2; a good 4-colouring of [22]: 0 0 2 3 1 3 0 1 0 2 2 1 3 0 1 0 2 2 1 3 0 3. The witnesses for every N are in the bundle. In Erdős's own convention subtract one. (d) computer-assisted.
Where the problem stands. exp(c(log N)1/9) ≪ h(N) ≪ N1/4+o(1), the upper bound a July 2026 preprint refereed here
and not yet by a journal; the lower bound the Bloom–Sisask 3-AP bound (arXiv:2309.02353, listed without a journal reference — the refereed Kelley–Meka bound gives
exp(c(log N)1/12)) through an elementary reduction; and exp(c(log N)1/6(log log N)−1/6) below if Raghavan's preprint holds (arXiv:2603.27045, v3 of
15 May 2026, Theorem 1.4; its abstract states the slightly weaker /log log N form; the forum comment quotes the (log N)1/6−o(1) form). The problem page records none of the 2026 claims, and the
community database still carries #160 as open, last updated 31 August 2025. None of the 2026 claims has been through a journal. The gap between a power of N and a sub-polynomial function is the whole problem; Deng–Tidor–Zhao's question — can
ABBA be killed with No(1) colours? — is where it now lives, and Shi–Dong's Remark 4.2 suggests the polynomial method as used here will not get there.
What is ours, and where to look. Nothing in either bound is ours. Ours are the referee report; the exhaustive verifications of the 27p-colouring (two independent implementations through p = 11, one at p = 13) and the k = 6 sample; the brute-force checks of Itabe's labels; the kernel replay with its controls; and the exact values of h(N) for N ≤ 51. The bundle holds every script, log, witness, seat report and live-page capture (repository private at the time of writing — files available on request). Unreviewed by humans.