The four-colour Rado number of 5(x-y) = 3z is 625

Identifier: F:rado-r4-a5-b3
Proof route: search-certificate
External status: open
Axiom footprint: rado.encoder-faithfulness, rado.drat-checker-check_drat_backward, rado.certificate-not-re-checked-per-commit

Recorded description

R_4(5(x-y)=3z) = 625. The lower bound is the a-adic valuation colouring of Chang-De Loera-Wesley's Lemma 4.1 (R_k >= a^k), replayed and verified three ways; the upper bound is a refutation at n = 625 with a self-checked DRAT certificate.

Formal statement

(assert (forall-colourings 625 4 (exists-mono-solution (= (* 5 (- x y)) (* 3 z)))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

claim-rado-r4-a5-b3

Kind: claim-ref
Status: checked

Supports: R_4(5(x-y)=3z) = 625, both bounds, with pinned deciding instance and regeneration recipe

Checker command

python3 scripts/validate-claims.py

Evidence notes

The claim carries the pinned CNF, the replayable lower-bound colouring, and the DRAT regeneration recipe.

lower-bound-replay

Kind: witness-replay
Status: checked

Supports: R_4(5(x-y)=3z) > 624

Checker command

cargo run --release -q -p axeyum-search --example akb2_frontier -- verify 5 3 4 artifacts/claims/rado/rado-r4-a5-b3/witness.txt

Evidence notes

Cheap and real: re-verifies the colouring three ways from the stored file in ~0.1s.

deciding-instance-regeneration

Kind: instance-pin
Status: checked

Supports: the refutation's verdict names this exact formula

Checker command

test "$(cargo run --release -q -p axeyum-search --example rado_dump_cnf -- a=5 b=3 k=4 n=625 out=/tmp/rb3.cnf >/dev/null 2>&1; sha256sum /tmp/rb3.cnf | cut -d' ' -f1)" = "$(sha256sum artifacts/claims/rado/rado-r4-a5-b3/F_625.cnf | cut -d' ' -f1)"

Evidence notes

Regeneration, not storage comparison: the bytes must come back out of the same encoder.

Provenance

{
  "date": "2026-08-14",
  "established_by": "axeyum native proof-producing CDCL (no external solver or checker, ADR-0002) on host s4, checked in-process by check_drat_backward",
  "source": "blank cell of Chang-De Loera-Wesley Table 10; inside the a >= b+2, gcd(a,b)=1 hypotheses",
  "prior_art": [
    {
      "citation": "campaign lane agent-c, 2026-08-14",
      "establishes": "solve killed mid-run at 3h11m with 15.51 GB of proof, because the check needed ~102 GiB against a 123 GiB maximum. At the 1.5x checking ratio landed later the same day it needs ~23 GiB and is reachable."
    },
    {
      "citation": "coordinator, 2026-08-14",
      "establishes": "closed: 220,077,720 steps, 19,877,980,843 bytes of DRAT, solve 8,762.2 s, check 14,499.6 s. Checking cost MORE than searching. The earlier estimate above was right that the 1.5x checking ratio made it reachable."
    }
  ]
}