# Conway-checkers / k-nacci realm — open problem survey

Generated 2026-05-25 in the idea-factory autonomous swing. Sources cited inline.

## Genuinely-open problems (gap-of-1 or larger)

From [George I. Bell, "George's Peg Solitaire Army Page"](https://www.gibell.net/pegsolitaire/army/index.html) (auth. reference, last modified 2025-04-27, last full survey is Bell-Hirschberg-Guerrero 2007), the minimum army size to reach row `n` in each variant:

| Variant | Row | Pagoda LB | Best UB | Open gap |
|---|---|---|---|---|
| Conway orthogonal | 4 | 19 | 20 | 1 (OEIS A014225) |
| Conway orthogonal | 5 | impossible | — | resolved (Conway 1961) |
| Conway orthogonal | 6 | 43 | 46 | 3 |
| Conway orthogonal | 7 | impossible | — | resolved if ≤ 5 → 7 follows |
| Skew (diagonal-only) | 5 | 18 | 19 | 1 |
| Skew | 6 | 51 | 53 | 2 |
| Hexagonal | 6 | 35 | 36 | 1 |
| Hexagonal | 7 | 140 ≤ N ≤ 145 | 145 | ≥ 5 |
| Fully diagonal | 4 | 7 | 8 | 1 (OEIS A125730) |
| Fully diagonal | 5 | 13 | 13 | resolved |
| Fully diagonal | 6 | 23 | 23 | resolved |
| Fully diagonal | 7 | 45 | 46 | 1 |
| Fully diagonal | 8 | 122 | 123 | 1 |
| Fully diagonal | 9 | impossible | — | resolved (Aigner 1997) |

Beyond Bell's table, from the Bruda-Cooper 2025 paper `bruda-cooper-2025-knacci.txt` §4.5–§4.6:
- **(m, k, d) projection failure set characterization** for k ≥ 3: completely open (their argument only treats k = 2 explicitly).
- **Achievability density `lim_{m→∞} #(S ∩ [1,m])/m`**: known to be 0 (Theorem 4.9), but the explicit characterization for d ≥ 3 is open.
- **The empirical L(32) claim**: under the actual predicate (4.41), the L(2k) family is **vacuously not in S**, so either their paragraph has a Fibonacci/Lucas swap (the substantive set is `S = {F(2k+1):k≥1}` per our `CORRECTION-2026-05-25.md`), or there is a separate algorithm in their text that doesn't match (4.41). Worth an erratum email to authors.

## Lean tractability assessment

| Target | Lean cost | Known status | Lean-novel? |
|---|---|---|---|
| Exact size 20 for Conway row 4 | 25+ year open | open | would be world-first |
| Exact 8 for fully-diagonal row 4 | open | open | would be world-first |
| `nM ≤ 3d - 1` for general d | feasible (weeks) | known (Eriksson-Lindström 1995) | yes |
| Bruda-Cooper Thm 4.3 d=1 (1D upper bound) | feasible (hours-days) | known (2025) | yes |
| Constructive row 4 reach (20 pegs) | feasible (tedious) | known | yes |
| Constructive row 8 reach in fully diagonal (123 pegs) | feasible (tedious) | known | yes |
| 1D specialization `nM = ⌊log_φ(m·φ)⌋` | feasible (hours) | known (folklore + Bruda-Cooper) | yes |
| (m,k,1) k≥3 upper bound | feasible (extends infrastructure) | known (Bruda-Cooper Thm 4.3 generalizes) | yes |

## Decision

Honest reality check: "prove an unsolved-but-known problem via Lean" cannot be completed in a session — these problems have been open for 25+ years. The achievable analogue is **Lean-novel mechanization of known results in this realm that advance toward the open problems**.

Chosen target: **Mechanize Bruda-Cooper Theorem 4.3 for d=1, k=2** — the 1D upper bound `nM ≤ ⌊log_φ(m·φ)⌋` for the (m, 2, 1)-game.

Rationale:
- Recent paper (2025), no Lean mechanization exists.
- Generalizes existing row-5 infrastructure to per-cell multiplicity `m`.
- Provides building block for future attacks on open problems in the realm.
- Self-contained, tractable in remaining session time.
- Concrete and falsifiable: theorem either compiles sorry-free in Lean or it doesn't.

NOT claiming to solve an open problem. Claiming: Lean-novel, paper-known, infrastructure-contributing.