Erdős Problem 835 — Artifacts & Evidence Set

Results at a glance

k	J(2k,k)	colours	835(k)	how
2	J(4,2)	3	YES	witness verified (proper + rainbow); 3 SAT SAT
3	J(6,3)	4	NO	own prover + 3 SAT UNSAT; STS(6) ∄
4	J(8,4)	5	NO	five oracles; SQS(8) exists but no large set
5	J(10,5)	6	NO	S(4,5,10) divisibility λ₂=28/3
6	J(12,6)	7	NO	CaDiCaL UNSAT (328s); the case Erdős/Rosenfeld were unsure about
≥3, k+1 composite			NO	primality sieve (Theorem 2)
16	J(32,16)	17	OPEN	smallest unresolved (k+1=17 prime)

sieve_835.py · output — divisibility⇔primality sieve (k=2..300), strict-gap k+2, survivors = {k+1 prime}
settle_835.py · output — own exhaustive prover + CaDiCaL/Glucose/MiniSat for k=2,3,4; witnesses + DIMACS
crosscheck_nosym.py · output — independent full search, no symmetry break
johnson_bound_835.py · output — recursive Johnson bound; hard core = {k+1 prime}
settle_k6b.py — background attempt at k=6 (J(12,6), 7 colours)

witness_k2.json — verified 3-colouring of J(4,2)
J_8_4__5col.cnf, J_6_3__4col.cnf, J_4_2__3col.cnf, J_12_6__7col.cnf — DIMACS for third-party replay
sieve_835_table.json, johnson_bound_table.json — full tables
settle_835_results.json — oracle agreement record
claim-ledger.json — claim-by-claim evidence map
note-erdos-835.md — markdown source
SHA256SUMS.txt — integrity ledger