"""Numerically verify the two lemmas behind 'D=5 is impossible'.

Reformulation: assign each person a vector in {0,1,2,3}^D (boat per day),
each coordinate balanced (each symbol exactly 6x). a_xy = #coords where x,y agree.
Full coverage <=> every a_xy >= 1.

Identity:  sum_{x<y} C(a_xy, 2) = sum_{c<c'} D_{cc'},
where D_{cc'} = # pairs sharing a boat on BOTH day c and day c'.
"""
from itertools import product
from math import comb

# ---- Lemma 1: every pair of days forces D_{cc'} >= 8 ----
# D_{cc'} = sum_{b,b'} C(m_{bb'},2) over 4x4 nonneg integer matrix with all
# row sums = col sums = 6.  Minimize it.
def min_double_agreements():
    best = 10**9
    bestM = None
    # enumerate 4x4 matrices with row sums 6 and col sums 6 (bounded entries 0..6)
    # build row by row; each row is a composition of 6 into 4 parts (0..6)
    rows = [r for r in product(range(7), repeat=4) if sum(r) == 6]
    for r0 in rows:
        for r1 in rows:
            s01 = [r0[j] + r1[j] for j in range(4)]
            if any(s > 6 for s in s01):
                continue
            for r2 in rows:
                s012 = [s01[j] + r2[j] for j in range(4)]
                if any(s > 6 for s in s012):
                    continue
                r3 = tuple(6 - s012[j] for j in range(4))
                if any(v < 0 for v in r3):
                    continue
                M = (r0, r1, r2, r3)
                val = sum(comb(M[i][j], 2) for i in range(4) for j in range(4))
                if val < best:
                    best, bestM = val, M
    return best, bestM


# ---- Lemma 2: max of sum C(a,2) under full-coverage budget for D days ----
# sum a = 60*D, all a>=1 (276 pairs), a<=D. excess E = 60*D - 276 distributed
# as e=a-1 in [0, D-1]. Maximize sum C(1+e,2). Convex -> fill biggest chunks.
def max_sum_binom(D):
    E = 60 * D - 276
    cap = D - 1               # max excess per pair (a<=D)
    npairs = 276
    # greedy: put as much excess as possible into pairs at cap (most C/unit)
    full = E // cap
    rem = E - full * cap
    # value
    total = full * comb(1 + cap, 2)
    if rem > 0:
        total += comb(1 + rem, 2)
    used = full + (1 if rem > 0 else 0)
    assert used <= npairs, "not enough pairs"
    return E, cap, total


if __name__ == "__main__":
    mn, M = min_double_agreements()
    print("Lemma 1: min D_{cc'} over balanced 4x4 tables =", mn)
    print("   attained by matrix:")
    for row in M:
        print("     ", row)

    print()
    for D in (5, 6):
        E, cap, mx = max_sum_binom(D)
        lhs = 8 * comb(D, 2)   # lower bound on sum_{c<c'} D_{cc'}
        print(f"D={D}: excess budget E={E}, per-pair cap a<= {D}")
        print(f"   RHS  max possible sum_x<y C(a,2)            = {mx}")
        print(f"   LHS  forced  sum_c<c' D_cc'  >= 8*C(D,2)    = {lhs}")
        verdict = "CONTRADICTION -> impossible" if lhs > mx else "no contradiction"
        print(f"   => {verdict}\n")