The two-colour Rado number of x - y = z is 5, as a kernel theorem

Identifier: F:rado-r2-schur-two
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Every 2-colouring of {1,...,5} contains a monochromatic solution of x = y + z, and some 2-colouring of {1,...,4} avoids one -- the partition {1,4} / {2,3}. So R_2(x-y=z) = 5. This is the two-colour Schur number in Rado form (a = b = 1), and it is the first Rado number in this repository that is a kernel theorem rather than a search certificate: both halves are reconstructed from search into terms `Kernel::add_declaration` accepted, with an empty axiom footprint.

Formal statement

theorem Nat.Rado.schur_two : Nat.Rado.IsRadoNumber 1 1 2 5

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

kernel-Nat.Rado.schur_two

Kind: kernel-term
Status: checked

Supports: R_2(x-y=z) = 5, both halves, as one kernel term of type Nat.Rado.IsRadoNumber 1 1 2 5

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::rado -- --test-threads=4

Evidence notes

`Nat.Rado.schur_arrows_five` (the upper half) is the `Nat.lt_two_cases` decision tree over the 2^5 colour assignments, with the monochromatic triple the search found at each of the 32 leaves; a leaf with no triple makes the builder return `None` and NOTHING is declared. `Nat.Rado.schur_not_arrows_four` (the lower half) refutes `Arrows 1 1 2 4` by reflection against `Nat.Rado.schurSet` = {2,3}: a Bool triple loop over `Nat.Finset.allBelow` that the kernel's own conversion check reduces to `true`, read back at the three existential witnesses by `allBelow_true_at`. The two are joined by `Nat.Rado.isRadoNumber_of_succ` at m = 4. ADR-1596.

shape-Nat.Rado.schur_two

Kind: exhaustive-enumeration
Status: checked

Supports: the declaration exists under this exact name and states IsRadoNumber, not something weaker

Checker command

cargo run --release -q -p axeyum-lean-kernel --example shape_search -- --name Nat.Rado.schur_two --kind theorem --expect 1

Evidence notes

`shape_search` exits 1 when the count differs and 3 when the query is unanswerable, so a stale index cannot pass for a present declaration.

search-bounds-schur-two

Kind: exhaustive-enumeration
Status: checked

Supports: 5 is LEAST: the 2^4 subsets of [1,4] contain an avoiding colouring and the 2^5 assignments to [1,5] contain none

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::rado_tests::the_search -- --test-threads=4

Evidence notes

The untrusted half, pinned independently of the kernel term it produced. The `None` at n = 5 is the load-bearing assertion; the test also re-checks the returned set with the witness search and requires that adding the excluded member 1 to it CREATES a monochromatic solution, so a set that merely looked avoiding fails.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum lane `rado-in-kernel`, roadmap item W1-1: search in `nat_prelude/rado.rs` produced both certificates and the reconstruction emitted the kernel terms; `Kernel::add_declaration` admitted all 17 declarations on the first attempt",
  "source": "the two-colour Schur number, classical (Schur 1916); a = b = 1 in the Chang-De Loera-Wesley family a(x-y) = bz",
  "prior_art": [
    {
      "citation": "Schur, 1916",
      "establishes": "S(2) = 4 in the sum-free-partition convention, i.e. R_2(x-y=z) = 5"
    }
  ]
}