# Erdős Problem 835 and the Middle Johnson Graph
### A Verified Reduction, a Primality Sieve, and Machine-Checked Small Cases
**Nathan Wilbanks and Annie — AGNT Labs — Verification Note, July 23, 2026**

## Statement
835 (Erdős–Rosenfeld): does there exist `k > 2` such that the `k`-subsets of
`{1,…,2k}` can be coloured with `k+1` colours so that every `(k+1)`-subset `A`
sees all `k+1` colours among its `k`-subsets?

Two `k`-subsets share a common `(k+1)`-set iff they differ in one element
(`|S∆T|=2`) — adjacency in the Johnson graph `J(2k,k)`. The `k`-subsets of a
`(k+1)`-set form a `(k+1)`-clique covering every edge, so:

> **835(k) is YES  ⟺  χ(J(2k,k)) = k+1.**   (Always χ ≥ k+1.)

## Exact packing bound (Theorem 1)
A colour class is an independent set in `J(2k,k)` = a binary constant-weight code
(length `2k`, weight `k`, min distance ≥ 4). Distance ≥ 4 ⟺ no `(k−1)`-set lies in
two codewords, so a class has ≤ `binom(2k,k−1)/k = C_k` (Catalan) codewords, with
equality **iff** it is a Steiner system `S(k−1,k,2k)`. Since `(k+1)·C_k = binom(2k,k)`
exactly, a proper `(k+1)`-colouring forces **every** class to meet the bound:

> **835(k) YES ⟺ the middle layer partitions into k+1 Steiner systems S(k−1,k,2k)**
> (a large set `LS[k+1](k−1,k,2k)`).

If no Steiner system exists then `A(2k,4,k) ≤ C_k − 1` and
`χ ≥ ceil(binom(2k,k)/(C_k−1)) = k+2` (verified exactly). One missing codeword
jumps χ from `k+1` to `k+2`.

## Primality sieve (Theorem 2)
`S(k−1,k,2k)` needs `(k−i) | binom(2k−i, k−1−i)` for `0 ≤ i ≤ k−1`. The index
`i=k−2` gives `λ = (k+2)/2` (fails for all odd k). Exact computation, k=2..300:

> **The Steiner divisibility for S(k−1,k,2k) holds ⟺ k+1 is prime.** (0 mismatches.)

So every composite `k+1` has an explicit non-integral design equation ⇒ no Steiner
system ⇒ χ ≥ k+2. This is an independent, elementary certificate of the
**Ma–Tang** theorem (NO for all composite `k+1`). The recursive Johnson bound
`jb(2k,4,k)` equals `C_k` **iff k+1 is prime** as well (k=3..60) — a second,
independent isolation of the same hard core `{k : k+1 prime}`.

## Machine-checked small cases (five oracles: own prover ±symmetry break, CaDiCaL, Glucose, MiniSat)
| k | J(2k,k) | colours | result | note |
|---|---------|---------|--------|------|
| 2 | J(4,2)  | 3 | **YES** | witness = 1-factorization of K4; verified proper + rainbow |
| 3 | J(6,3)  | 4 | **NO**  | S(2,3,6)=STS(6) ∄ (λ₁=5/2); 9 / 257 search nodes; 3 SAT UNSAT |
| 4 | J(8,4)  | 5 | **NO**  | SQS(8) exists but no large set; 136 / 11486 nodes; 3 SAT UNSAT |
| 5 | J(10,5) | 6 | **NO**  | S(4,5,10) ∄ (λ₂=28/3) |
| 6 | J(12,6) | 7 | **NO** | S(5,6,12) exists but no large set; CaDiCaL UNSAT in 328s (independent of Brouwer) |

`k=4` is the smallest **structural** case: the Steiner system exists yet its large
set does not, so it is settled by direct colouring infeasibility, not divisibility.

## Frontier
NO for all composite `k+1` (Theorem 2 / Ma–Tang); for prime `k+1`, NO whenever the
Steiner system is absent or admits no large set (k=4,6). Open cases are exactly
`k = p−1` (p prime) with both unresolved. **Smallest open case: k=16** — YES iff
`A(32,4,16)=C₁₆` with a perfect tiling, i.e. iff `S(15,16,32)` exists and 17 disjoint
copies tile `binom([32],16)`. Belief: NO for all k>2, i.e. `χ(J(2k,k)) ≥ k+2`.

## Reproduce
```
python -m pip install python-sat sympy
python sieve_835.py
python settle_835.py 2 3 4
python crosscheck_nosym.py 2 3 4
python johnson_bound_835.py
```

## Attribution
Reduction to `χ(J(2k,k))`, the `A(2k,4,k)` bound: erdosproblems.com/835 (Bloom),
formal-conjectures, forum (eigensolver, B. Mehta, Q. Tang). Composite-case theorem:
Ma & Tang [MT25]. Cases 3≤k≤8: Brouwer's Johnson tables. This note contributes the
explicit large-set characterization, the machine-verified divisibility⇔primality
sieve, the strict `k+2` gap, and the five-oracle base-case certificates.