The two-colour Ramsey number R(3,3) is 6, as a kernel theorem

Identifier: F:ramsey-r33-six
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Every graph on at least six vertices contains three pairwise adjacent vertices or three pairwise non-adjacent ones, and some graph on five vertices contains neither -- the five-cycle. So R(3,3) = 6. Both halves are kernel terms with an empty axiom footprint: the upper bound is the textbook pigeonhole argument encoded as a 32-leaf case tree over the five edges at one vertex, and the lower bound is a search certificate that the kernel re-checks by reflection.

Formal statement

theorem Nat.Graph.ramsey_three_three : Nat.Graph.IsRamseyNumber33 6

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

kernel-Nat.Graph.ramsey_three_three

Kind: kernel-term
Status: checked

Supports: R(3,3) = 6, both halves, as one kernel term of type Nat.Graph.IsRamseyNumber33 6

Checker command

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

Evidence notes

`Nat.Graph.ramsey33_arrows_six` (the upper half) is a case tree over the five edges at vertex 0 -- 32 leaves, each one application of `Nat.Graph.triangle_or_indep` or `Nat.Graph.antitriangle_or_indep`, the two four-leaf case analyses proved once. The pigeonhole step is discharged by the enumeration: the builder computes the majority colour class at each leaf and a Rust assertion fires if some leaf has fewer than three on both sides. `Nat.Graph.ramsey33_not_arrows_five` (the lower half) refutes `Arrows33 5` by reflection against `Nat.Graph.ramsey33Witness`: 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`, applied to the witness AND to its complement. The two are joined by `Nat.Graph.isRamseyNumber33_of_succ` at m = 5. ADR-1608.

shape-Nat.Graph.ramsey_three_three

Kind: exhaustive-enumeration
Status: checked

Supports: the declaration exists under this exact name and is a theorem, not a definition or an axiom

Checker command

cargo run --release -q -p axeyum-lean-kernel --example shape_search -- --name Nat.Graph.ramsey_three_three --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. The same query returned ABSENT for every one of graph, edge, vertex, degree, walk, ramsey, clique and independ before this lane, which is the pre-state this row is measured against.

search-lower-bound-r33

Kind: exhaustive-enumeration
Status: checked

Supports: 6 is LEAST: of the 2^10 graphs on five vertices, at least one has neither a triangle nor an independent triple

Checker command

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

Evidence notes

The untrusted half, pinned independently of the kernel term it produced. The test re-derives the no-monochromatic-triple property from the returned edge list rather than trusting the search's own verdict, and carries a negative control -- the empty graph, which the same predicate must reject -- so the check is not vacuous. It also pins that the witness has five edges and is 2-regular, i.e. that it is the five-cycle up to relabelling, which is the unique such graph. Separately, `noClique3B` (the decision the kernel actually runs) is checked `true` on the witness and its complement and `false` on the complete graph on three vertices, so the reflection cannot be vacuously true.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum lane `graph-carrier`, roadmap items W1-6 and W2-11: `nat_prelude/graph.rs` declares the carrier and `nat_prelude/ramsey.rs` the Ramsey family; the lower-bound search in `ramsey.rs` produced the five-vertex certificate and the reconstruction emitted the kernel terms",
  "source": "Ramsey's theorem for two colours at (3,3); classical (Ramsey 1930, and the R(3,3) = 6 value is the standard first example)",
  "prior_art": [
    {
      "citation": "Ramsey, 1930",
      "establishes": "the general finite Ramsey theorem, of which R(3,3) = 6 is the first non-trivial diagonal value"
    }
  ]
}