# Rowing meet: covering all 276 pairs with boats of six

## The problem

24 people, 4 boats of exactly 6 seats. Each day everyone is partitioned into the
four boats; the partition may change daily. We must guarantee that **every** one of
the $\binom{24}{2}=276$ pairs of people shares a boat on **at least one** day.

> **What is the minimum number of days?**

**Answer: $\boxed{6}$ days.**

The rest of this document explains how we get there: two lower bounds (the easy one
gives $\ge 5$, a counting identity rules out $5$ and gives $\ge 6$), and an explicit,
machine‑verified 6‑day schedule. We also describe the approaches that *didn't* work.

---

## 1. A useful reformulation

A day is a partition of the 24 people into 4 labelled boats of 6. Over $d$ days,
give each person the vector of boats they occupy:

$$ v_x \in \{0,1,2,3\}^{d}, \qquad v_x(c) = \text{boat of person } x \text{ on day } c. $$

Two people **share a boat on day $c$** iff $v_x(c)=v_y(c)$. So:

- **Goal (coverage):** every pair $x\ne y$ agrees in *at least one* coordinate
  — i.e. no two vectors differ in *all* $d$ coordinates.
- **Constraint (balance):** in every coordinate each of the 4 symbols appears
  exactly 6 times (each boat holds exactly 6).

Let $a_{xy} = \#\{c : v_x(c)=v_y(c)\}$ be the number of days a pair shares a boat.
Coverage $\iff a_{xy}\ge 1$ for all 276 pairs.

Two counts we use repeatedly:

- Each boat covers $\binom{6}{2}=15$ pairs, each day $4\cdot 15 = 60$, so
  $\sum_{x<y} a_{xy} = 60d$ for any balanced schedule.
- Each person shares their boat with $5$ others per day, so meets at most $5d$
  distinct people over $d$ days.

---

## 2. Lower bound: at least 5 days

A single person must meet all $23$ others, but meets at most $5$ per day:

$$ 5d \ge 23 \;\Longrightarrow\; d \ge \lceil 23/5\rceil = 5. $$

With $d=4$ each person meets at most $20 < 23$ people, so 4 days is hopeless.
(Equivalently, $60\cdot 4 = 240 < 276$ pair‑slots.) So $d\ge 5$.

This is also the **Schönheim bound** for the covering number
$C(24,6,2)\ge \lceil \tfrac{24}{6}\lceil\tfrac{23}{5}\rceil\rceil = 20$ blocks,
i.e. $20/4 = 5$ resolvable days. The interesting question is whether 5 is reachable.

---

## 3. Five days is impossible — a counting identity

Suppose 5 balanced partitions covered all 276 pairs. We derive a contradiction by
counting **double‑agreements** two different ways.

### The identity

For a pair of days $c\ne c'$, let

$$ D_{c,c'} = \#\{\text{pairs sharing a boat on both day } c \text{ and day } c'\}. $$

A pair that agrees in a set of $a_{xy}$ coordinates is counted once for each of the
$\binom{a_{xy}}{2}$ day‑pairs inside that set, so

$$ \sum_{c<c'} D_{c,c'} \;=\; \sum_{x<y} \binom{a_{xy}}{2}. \tag{$\star$}$$

### Left side is forced to be large

Fix two days. The numbers $m_{b,b'}$ = (people in boat $b$ on day $c$ **and** boat
$b'$ on day $c'$) form a $4\times 4$ table whose every row and column sums to $6$
(boats hold 6 on both days). Then $D_{c,c'} = \sum_{b,b'}\binom{m_{b,b'}}{2}$, and

$$ D_{c,c'} \;=\; \tfrac12\Big(\textstyle\sum m_{b,b'}^2 - 24\Big) \;\ge\; 8, $$

minimised when the table is as flat as possible — eight 2's and eight 1's
(e.g. rows $2,2,1,1$), giving $\sum m^2 = 40$. This holds for **every** pair of days,
so

$$ \sum_{c<c'} D_{c,c'} \;\ge\; \binom{5}{2}\cdot 8 \;=\; 80. $$

### Right side is forced to be small

With 5 days, $a_{xy}\le 5$, and full coverage forces
$\sum_{x<y} a_{xy} = 300$ over the $276$ pairs, each $\ge 1$. The total "excess"
is $\sum (a_{xy}-1) = 300-276 = 24$. The function $\binom{a}{2}$ is convex and
$a\le 5$, so $\sum\binom{a}{2}$ is maximised by piling excess into as few pairs as
possible — six pairs at $a=5$ ($6\times 4 = 24$ excess):

$$ \sum_{x<y}\binom{a_{xy}}{2} \;\le\; 6\cdot\binom{5}{2} \;=\; 60. $$

### Contradiction

By $(\star)$ the two sides are equal, but $80 \le (\star) \le 60$ is impossible.
**Hence 5 days cannot cover all pairs.** Combined with §2, $d\ge 6$.

> **Sharper:** the left bound $\sum_{c<c'}D_{c,c'}\ge 80$ holds for *any* 5 balanced
> partitions, covering or not. Pushing the same algebra (write $a=1+e$, $e\le 4$,
> $\sum e = 300-C$ where $C$ is the number of covered pairs) gives
> $C\le 268$. **So with 5 days at least $276-268 = 8$ pairs are *always* left out** —
> 5 days don't just barely miss, they miss by at least 8.

The lemmas above are checked numerically in [proof_check.py](proof_check.py) and
[bound5.py](bound5.py); local searches over thousands of 5‑day schedules never reach
full coverage, consistent with this bound ([min5.py](min5.py)).

---

## 4. Six days suffices — an explicit schedule

Six days leave plenty of room: each person now has $5\cdot 6 = 30$ meeting slots for
23 partners (slack 7), and the budget version of §3 has no contradiction
($\sum D \ge 8\binom{6}{2}=120 \le 250$, the new RHS cap). A schedule is easy to find
by local search (see §5). Here is one, **verified** to cover all 276 pairs
([verify in lib.py](lib.py), output below). Day 1 is just the four natural bands.

| Day | Boat A | Boat B | Boat C | Boat D |
|----:|--------|--------|--------|--------|
| 1 | 0 1 2 3 4 5 | 6 7 8 9 10 11 | 12 13 14 15 16 17 | 18 19 20 21 22 23 |
| 2 | 1 3 8 9 16 23 | 4 10 14 17 18 20 | 5 11 12 13 19 21 | 0 2 6 7 15 22 |
| 3 | 4 5 7 8 16 22 | 1 6 14 17 19 21 | 0 9 12 13 18 20 | 2 3 10 11 15 23 |
| 4 | 0 8 11 14 17 22 | 1 7 10 12 13 23 | 2 5 6 16 18 20 | 3 4 9 15 19 21 |
| 5 | 1 5 9 10 15 22 | 0 4 6 11 16 23 | 3 7 14 17 18 20 | 2 8 12 13 19 21 |
| 6 | 1 8 11 15 18 20 | 2 5 9 14 17 23 | 3 4 6 12 13 22 | 0 7 10 16 19 21 |

The same data as the requested JSON format (each day = 4 boats of 6, 0‑indexed) is in
**[solution6.json](solution6.json)**:

```json
[[[0,1,2,3,4,5],[6,7,8,9,10,11],[12,13,14,15,16,17],[18,19,20,21,22,23]],
 [[1,3,8,9,16,23],[4,10,14,17,18,20],[5,11,12,13,19,21],[0,2,6,7,15,22]],
 [[4,5,7,8,16,22],[1,6,14,17,19,21],[0,9,12,13,18,20],[2,3,10,11,15,23]],
 [[0,8,11,14,17,22],[1,7,10,12,13,23],[2,5,6,16,18,20],[3,4,9,15,19,21]],
 [[1,5,9,10,15,22],[0,4,6,11,16,23],[3,7,14,17,18,20],[2,8,12,13,19,21]],
 [[1,8,11,15,18,20],[2,5,9,14,17,23],[3,4,6,12,13,22],[0,7,10,16,19,21]]]
```

**Verification (`python3 lib.py` style check):**

```
valid 6-day schedule & full cover: True
days: 6 | covered: 276 /276 | missing: 0
total meetings: 360 | repeat excess: 84
every person meets all 23 others: yes (distinct partners = 23 for all)
pairs meeting k times: {1: 212, 2: 56, 3: 4, 6: 4}
```

Since $d\ge 6$ and 6 is achievable, **the minimum number of days is 6.**

---

## 5. Methods tried (including dead ends)

| Method | Outcome |
|---|---|
| **Per‑person / Schönheim counting** | Clean bound $d\ge 5$. Not tight. |
| **Double‑agreement identity (§3)** | The crux: proves $d\ge 6$ and even "$\ge 8$ pairs missed at $d=5$". |
| **Greedy day‑by‑day** ([build6.py](build6.py)) | Maximising new pairs each day stalls at 12 missing — gets greedy‑stuck. |
| **Algebraic grid / affine boats** | Elegant but gives **7** days, not 6 — see below. A near miss. |
| **Single‑orbit cyclic** ([cyclic6.py](cyclic6.py)) | One base partition + its 6 column‑rotations: best 15 missing. Too rigid. |
| **Local search / annealing** ([anneal6.py](anneal6.py)) | Finds a full 6‑cover in well under a second. This produced the schedule above. |
| **SAT model** ([sat_check.py](sat_check.py)) | Encodes "exists a $d$‑day cover". Fast SAT for $d=6$; the $d=5$ UNSAT search is slow (the §3 proof is the authority). |
| **Local search at $d=5$** ([min5.py](min5.py)) | Never reaches full cover — consistent with the $\ge 8$ uncovered bound. |

### Why the elegant grid construction gives 7, not 6

Put people on a $4\times 6$ grid, person $=(r,c)$, $r\in\mathbb Z_4,\,c\in\mathbb Z_6$.
"Affine" days assign boat label $(r+g_d(c))\bmod 4$ for a function $g_d:\mathbb Z_6\to\mathbb Z_4$;
these are always valid partitions into sextets. Day "rows" ($g\equiv0$) covers all
same‑row pairs. But two people in the **same column** ($c=c'$) share a boat only when
$r-r'\equiv 0$ — never, since $r\ne r'$. So affine days *structurally cannot* cover
same‑column pairs, and to cover every different‑row/different‑column pair one needs,
for each column pair, the three differences $g_d(c')-g_d(c)$ to be a permutation of
$\{1,2,3\}$. Their sum is $6\equiv 2\pmod 4$ for *every* column pair, which is
impossible for $\ge 3$ columns (a telescoping contradiction). The construction needs
a 4th affine day plus 2 column‑repair days $=7$. Pretty, but beaten by search.

---

## 6. Files

- [index.md](index.md) — this document.
- [solution6.json](solution6.json) — the 6‑day construction (the deliverable).
- [lib.py](lib.py) — schedule verifier and counting facts.
- [proof_check.py](proof_check.py) — numeric check of the two §3 lemmas (min $D=8$; max RHS $=60$).
- [bound5.py](bound5.py) — the "$\ge 8$ uncovered at $d=5$" bound.
- [anneal6.py](anneal6.py) — local search that finds the 6‑day cover.
- [build6.py](build6.py), [cyclic6.py](cyclic6.py), [min5.py](min5.py), [sat_check.py](sat_check.py) — the other methods.

### Reproduce

```bash
python3 lib.py                  # counting facts
python3 proof_check.py          # §3 lemmas  -> CONTRADICTION at d=5
python3 bound5.py               # >= 8 pairs uncovered with 5 days
python3 anneal6.py 6            # find & save a verified 6-day cover
python3 -c "import json,lib; print(lib.verify(json.load(open('solution6.json')))[0])"  # True
```