diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/ANCHOR-PROGRESS.json b/research/f7-18point-tight-classes-seed4c1e7b30/ANCHOR-PROGRESS.json new file mode 100644 index 0000000000..ae4e76cd75 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/ANCHOR-PROGRESS.json @@ -0,0 +1,1310 @@ +{ + "modes": { + "k10b3": { + "complete": true, + "shards": { + "v0=10": { + "examples": { + "3": [ + 0, + 3, + 10, + 12, + 15, + 17, + 33, + 53, + 65, + 86 + ] + }, + "hist": { + "3": 14407680 + }, + "seconds": 124.94 + }, + "v0=101": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=102": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=105": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=106": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=108": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=111": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=113": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=114": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=116": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=119": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=12": { + "examples": { + "3": [ + 0, + 3, + 12, + 15, + 17, + 20, + 33, + 39, + 65, + 72 + ] + }, + "hist": { + "3": 10752000 + }, + "seconds": 116.93 + }, + "v0=120": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=123": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=125": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=126": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=15": { + "examples": { + "3": [ + 0, + 3, + 15, + 17, + 18, + 20, + 33, + 40, + 65, + 75 + ] + }, + "hist": { + "3": 10364928 + }, + "seconds": 114.73 + }, + "v0=17": { + "examples": { + "3": [ + 0, + 3, + 17, + 18, + 20, + 24, + 33, + 46, + 65, + 92 + ] + }, + "hist": { + "3": 8782848 + }, + "seconds": 91.44 + }, + "v0=18": { + "examples": { + "3": [ + 0, + 3, + 18, + 20, + 23, + 24, + 33, + 40, + 65, + 92 + ] + }, + "hist": { + "3": 8455680 + }, + "seconds": 65.94 + }, + "v0=20": { + "examples": { + "3": [ + 0, + 3, + 20, + 23, + 24, + 29, + 33, + 39, + 65, + 80 + ] + }, + "hist": { + "3": 6200832 + }, + "seconds": 52.02 + }, + "v0=23": { + "examples": { + "3": [ + 0, + 3, + 23, + 24, + 27, + 29, + 33, + 40, + 65, + 80 + ] + }, + "hist": { + "3": 5956608 + }, + "seconds": 48.94 + }, + "v0=24": { + "examples": { + "3": [ + 0, + 3, + 24, + 27, + 29, + 33, + 40, + 65, + 75, + 101 + ] + }, + "hist": { + "3": 4402176 + }, + "seconds": 38.05 + }, + "v0=27": { + "examples": { + "3": [ + 0, + 3, + 27, + 29, + 30, + 33, + 40, + 65, + 75, + 101 + ] + }, + "hist": { + "3": 4217856 + }, + "seconds": 36.12 + }, + "v0=29": { + "examples": { + "3": [ + 0, + 3, + 29, + 30, + 33, + 36, + 40, + 46, + 65, + 80 + ] + }, + "hist": { + "3": 3225600 + }, + "seconds": 28.14 + }, + "v0=30": { + "examples": { + "3": [ + 0, + 3, + 30, + 33, + 34, + 36, + 40, + 48, + 65, + 78 + ] + }, + "hist": { + "3": 3078144 + }, + "seconds": 26.44 + }, + "v0=33": { + "examples": { + "3": [ + 0, + 3, + 33, + 34, + 36, + 40, + 48, + 63, + 65, + 108 + ] + }, + "hist": { + "3": 2860032 + }, + "seconds": 24.11 + }, + "v0=34": { + "examples": { + "3": [ + 0, + 3, + 34, + 36, + 39, + 40, + 48, + 57, + 65, + 108 + ] + }, + "hist": { + "3": 2736384 + }, + "seconds": 22.71 + }, + "v0=36": { + "examples": { + "3": [ + 0, + 3, + 36, + 39, + 40, + 45, + 48, + 54, + 65, + 96 + ] + }, + "hist": { + "3": 1930752 + }, + "seconds": 16.24 + }, + "v0=39": { + "examples": { + "3": [ + 0, + 3, + 39, + 40, + 43, + 45, + 48, + 57, + 65, + 96 + ] + }, + "hist": { + "3": 1837824 + }, + "seconds": 16.14 + }, + "v0=40": { + "examples": { + "3": [ + 0, + 3, + 40, + 43, + 45, + 48, + 57, + 65, + 75, + 116 + ] + }, + "hist": { + "3": 1306368 + }, + "seconds": 11.25 + }, + "v0=43": { + "examples": { + "3": [ + 0, + 3, + 43, + 45, + 46, + 48, + 57, + 65, + 75, + 116 + ] + }, + "hist": { + "3": 1234944 + }, + "seconds": 11.57 + }, + "v0=45": { + "examples": { + "3": [ + 0, + 3, + 45, + 46, + 48, + 53, + 57, + 63, + 65, + 96 + ] + }, + "hist": { + "3": 917760 + }, + "seconds": 8.55 + }, + "v0=46": { + "examples": { + "3": [ + 0, + 3, + 46, + 48, + 51, + 53, + 57, + 65, + 78, + 101 + ] + }, + "hist": { + "3": 858624 + }, + "seconds": 7.34 + }, + "v0=48": { + "examples": { + "3": [ + 0, + 3, + 48, + 51, + 53, + 57, + 65, + 78, + 80, + 108 + ] + }, + "hist": { + "3": 609792 + }, + "seconds": 5.21 + }, + "v0=5": { + "examples": { + "3": [ + 0, + 3, + 5, + 6, + 9, + 17, + 33, + 58, + 65, + 92 + ] + }, + "hist": { + "3": 19353600 + }, + "seconds": 137.77 + }, + "v0=51": { + "examples": { + "3": [ + 0, + 3, + 51, + 53, + 54, + 57, + 65, + 72, + 80, + 108 + ] + }, + "hist": { + "3": 562176 + }, + "seconds": 4.81 + }, + "v0=53": { + "examples": { + "3": [ + 0, + 3, + 53, + 54, + 57, + 60, + 65, + 71, + 80, + 96 + ] + }, + "hist": { + "3": 457728 + }, + "seconds": 4.01 + }, + "v0=54": { + "examples": { + "3": [ + 0, + 3, + 54, + 57, + 58, + 60, + 65, + 72, + 80, + 96 + ] + }, + "hist": { + "3": 413184 + }, + "seconds": 3.66 + }, + "v0=57": { + "examples": { + "3": [ + 0, + 3, + 57, + 58, + 65, + 68, + 72, + 78, + 80, + 96 + ] + }, + "hist": { + "3": 340992 + }, + "seconds": 2.58 + }, + "v0=58": { + "examples": { + "3": [ + 0, + 3, + 58, + 60, + 65, + 66, + 72, + 77, + 80, + 96 + ] + }, + "hist": { + "3": 297984 + }, + "seconds": 2.18 + }, + "v0=6": { + "examples": { + "3": [ + 0, + 3, + 6, + 9, + 10, + 17, + 33, + 53, + 65, + 92 + ] + }, + "hist": { + "3": 18708480 + }, + "seconds": 130.94 + }, + "v0=60": { + "examples": { + "3": [ + 0, + 3, + 60, + 63, + 65, + 68, + 72, + 78, + 80, + 96 + ] + }, + "hist": { + "3": 258048 + }, + "seconds": 1.69 + }, + "v0=63": { + "examples": { + "3": [ + 0, + 3, + 63, + 65, + 66, + 68, + 72, + 80, + 95, + 101 + ] + }, + "hist": { + "3": 215040 + }, + "seconds": 1.47 + }, + "v0=65": { + "examples": { + "3": [ + 0, + 3, + 65, + 68, + 72, + 77, + 80, + 86, + 96, + 106 + ] + }, + "hist": { + "3": 80640 + }, + "seconds": 1.15 + }, + "v0=66": { + "examples": { + "3": [ + 0, + 3, + 66, + 68, + 72, + 77, + 80, + 85, + 96, + 123 + ] + }, + "hist": { + "3": 80640 + }, + "seconds": 1.07 + }, + "v0=68": { + "examples": { + "3": [ + 0, + 3, + 68, + 72, + 77, + 80, + 85, + 90, + 96, + 102 + ] + }, + "hist": { + "3": 43008 + }, + "seconds": 0.7 + }, + "v0=71": { + "examples": { + "3": [ + 0, + 3, + 71, + 72, + 77, + 80, + 85, + 89, + 96, + 102 + ] + }, + "hist": { + "3": 43008 + }, + "seconds": 0.61 + }, + "v0=72": { + "examples": { + "3": [ + 0, + 3, + 72, + 77, + 80, + 85, + 89, + 95, + 96, + 123 + ] + }, + "hist": { + "3": 21504 + }, + "seconds": 0.38 + }, + "v0=75": { + "examples": { + "3": [ + 0, + 3, + 75, + 77, + 80, + 85, + 89, + 92, + 96, + 106 + ] + }, + "hist": { + "3": 21504 + }, + "seconds": 0.34 + }, + "v0=77": { + "examples": { + "3": [ + 0, + 3, + 77, + 80, + 85, + 89, + 95, + 96, + 101, + 123 + ] + }, + "hist": { + "3": 10368 + }, + "seconds": 0.2 + }, + "v0=78": { + "examples": { + "3": [ + 0, + 3, + 78, + 80, + 85, + 89, + 95, + 96, + 101, + 120 + ] + }, + "hist": { + "3": 10368 + }, + "seconds": 0.17 + }, + "v0=80": { + "examples": { + "3": [ + 0, + 3, + 80, + 85, + 89, + 92, + 96, + 102, + 113, + 123 + ] + }, + "hist": { + "3": 3840 + }, + "seconds": 0.09 + }, + "v0=83": { + "examples": { + "3": [ + 0, + 3, + 83, + 85, + 89, + 95, + 96, + 101, + 113, + 120 + ] + }, + "hist": { + "3": 3840 + }, + "seconds": 0.08 + }, + "v0=85": { + "examples": { + "3": [ + 0, + 3, + 85, + 89, + 92, + 96, + 101, + 106, + 113, + 119 + ] + }, + "hist": { + "3": 1536 + }, + "seconds": 0.05 + }, + "v0=86": { + "examples": { + "3": [ + 0, + 3, + 86, + 89, + 92, + 96, + 101, + 105, + 113, + 119 + ] + }, + "hist": { + "3": 1536 + }, + "seconds": 0.05 + }, + "v0=89": { + "examples": { + "3": [ + 0, + 3, + 89, + 92, + 96, + 102, + 105, + 111, + 113, + 123 + ] + }, + "hist": { + "3": 384 + }, + "seconds": 0.03 + }, + "v0=9": { + "examples": { + "3": [ + 0, + 3, + 9, + 10, + 12, + 17, + 33, + 53, + 65, + 86 + ] + }, + "hist": { + "3": 14923776 + }, + "seconds": 111.24 + }, + "v0=90": { + "examples": { + "3": [ + 0, + 3, + 90, + 92, + 96, + 101, + 105, + 108, + 113, + 123 + ] + }, + "hist": { + "3": 384 + }, + "seconds": 0.01 + }, + "v0=92": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=95": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=96": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=99": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + } + }, + "spec": { + "anchor_count": 149990400, + "budget": 3, + "description": "10-sets through {0,3}, pair-sum excess <= 3", + "k": 10 + }, + "total_hist": { + "3": 149990400 + } + }, + "k11b4": { + "complete": true, + "shards": { + "v0=10": { + "examples": {}, + "hist": {}, + "seconds": 198.61 + }, + "v0=101": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=102": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=105": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=106": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=108": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=111": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=113": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=114": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=116": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=119": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=12": { + "examples": {}, + "hist": {}, + "seconds": 193.63 + }, + "v0=120": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=123": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=125": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=126": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=15": { + "examples": {}, + "hist": {}, + "seconds": 159.57 + }, + "v0=17": { + "examples": {}, + "hist": {}, + "seconds": 101.58 + }, + "v0=18": { + "examples": {}, + "hist": {}, + "seconds": 95.63 + }, + "v0=20": { + "examples": {}, + "hist": {}, + "seconds": 87.6 + }, + "v0=23": { + "examples": {}, + "hist": {}, + "seconds": 114.79 + }, + "v0=24": { + "examples": {}, + "hist": {}, + "seconds": 95.03 + }, + "v0=27": { + "examples": {}, + "hist": {}, + "seconds": 88.55 + }, + "v0=29": { + "examples": {}, + "hist": {}, + "seconds": 59.68 + }, + "v0=30": { + "examples": {}, + "hist": {}, + "seconds": 56.56 + }, + "v0=33": { + "examples": {}, + "hist": {}, + "seconds": 47.93 + }, + "v0=34": { + "examples": {}, + "hist": {}, + "seconds": 47.66 + }, + "v0=36": { + "examples": {}, + "hist": {}, + "seconds": 31.68 + }, + "v0=39": { + "examples": {}, + "hist": {}, + "seconds": 32.31 + }, + "v0=40": { + "examples": {}, + "hist": {}, + "seconds": 23.51 + }, + "v0=43": { + "examples": {}, + "hist": {}, + "seconds": 21.63 + }, + "v0=45": { + "examples": {}, + "hist": {}, + "seconds": 16.36 + }, + "v0=46": { + "examples": {}, + "hist": {}, + "seconds": 15.68 + }, + "v0=48": { + "examples": {}, + "hist": {}, + "seconds": 10.22 + }, + "v0=5": { + "examples": {}, + "hist": {}, + "seconds": 234.61 + }, + "v0=51": { + "examples": {}, + "hist": {}, + "seconds": 9.47 + }, + "v0=53": { + "examples": {}, + "hist": {}, + "seconds": 6.61 + }, + "v0=54": { + "examples": {}, + "hist": {}, + "seconds": 6.97 + }, + "v0=57": { + "examples": {}, + "hist": {}, + "seconds": 4.45 + }, + "v0=58": { + "examples": {}, + "hist": {}, + "seconds": 4.51 + }, + "v0=6": { + "examples": {}, + "hist": {}, + "seconds": 205.0 + }, + "v0=60": { + "examples": {}, + "hist": {}, + "seconds": 3.17 + }, + "v0=63": { + "examples": {}, + "hist": {}, + "seconds": 2.9 + }, + "v0=65": { + "examples": {}, + "hist": {}, + "seconds": 1.6 + }, + "v0=66": { + "examples": {}, + "hist": {}, + "seconds": 1.82 + }, + "v0=68": { + "examples": {}, + "hist": {}, + "seconds": 0.86 + }, + "v0=71": { + "examples": {}, + "hist": {}, + "seconds": 0.73 + }, + "v0=72": { + "examples": {}, + "hist": {}, + "seconds": 0.4 + }, + "v0=75": { + "examples": {}, + "hist": {}, + "seconds": 0.44 + }, + "v0=77": { + "examples": {}, + "hist": {}, + "seconds": 0.27 + }, + "v0=78": { + "examples": {}, + "hist": {}, + "seconds": 0.29 + }, + "v0=80": { + "examples": {}, + "hist": {}, + "seconds": 0.13 + }, + "v0=83": { + "examples": {}, + "hist": {}, + "seconds": 0.12 + }, + "v0=85": { + "examples": {}, + "hist": {}, + "seconds": 0.06 + }, + "v0=86": { + "examples": {}, + "hist": {}, + "seconds": 0.05 + }, + "v0=89": { + "examples": {}, + "hist": {}, + "seconds": 0.03 + }, + "v0=9": { + "examples": {}, + "hist": {}, + "seconds": 166.58 + }, + "v0=90": { + "examples": {}, + "hist": {}, + "seconds": 0.02 + }, + "v0=92": { + "examples": {}, + "hist": {}, + "seconds": 0.01 + }, + "v0=95": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=96": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=99": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + } + }, + "spec": { + "anchor_count": 0, + "budget": 4, + "description": "11-sets through {0,3}, pair-sum excess <= 4", + "k": 11 + }, + "total_hist": {} + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/ANCHOR-REPRO.json b/research/f7-18point-tight-classes-seed4c1e7b30/ANCHOR-REPRO.json new file mode 100644 index 0000000000..eea3e1d3a1 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/ANCHOR-REPRO.json @@ -0,0 +1,68 @@ +{ + "note": "Every recorded anchor was reproduced before any new number in this package. The two heavy PR 2773 anchors were re-walked IN FULL from EMPTY receipts: the walk directory contained no ANCHOR-PROGRESS.json and run_anchors_all.py printed 'fresh receipts confirmed' before the walk. Receipt-validation trap (recorded): a resumed walk against a committed receipt silently 'passes' - the extracted PR 2933 package's own quick mode prints 'ANCHORS receipts ... (re-walked from empty receipts)' from its COMMITTED receipts, which validates receipts, not the walk. The receipts recorded here (ANCHOR-PROGRESS.json) are the output of this session's fresh walk and are themselves validated by verify.py anchors (receipt validation of a fresh walk, documented as such).", + "reproductions": [ + { + "anchor": "PR 2870 OBSTRUCTION", + "command": "python3.12 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py quick (vendored cover18.squeeze_numbers(7, 11, 6))", + "expected": "parseval=696 allowed=504 deficit=192", + "observed": "CONTROL PR2870 obstruction reproduced: parseval=696 allowed=504 deficit=192", + "status": "recomputed fresh" + }, + { + "anchor": "PR 2911 SQUEEZE table", + "command": "same run (vendored cover18.squeeze_numbers for the four splits)", + "expected": "(12,6) 1248/696; (11,7) 1166/798 vs 21294; (10,8) 1080/896; (9,9) 990/990", + "observed": "SQUEEZE lines with exactly those remainders/allowed/deficits", + "status": "recomputed fresh" + }, + { + "anchor": "PR 2911 NOVANISH", + "command": "python3.12 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py novanish", + "expected": "(12,6) and (10,8) infeasible: vanishing forced", + "observed": "NOVANISH (12, 6) feasible=False capped=False; NOVANISH (10, 8) feasible=False capped=False; PASS_TIGHT_NOVANISH", + "status": "recomputed fresh" + }, + { + "anchor": "PR 2911 ROWS18", + "command": "python3.12 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py rows", + "expected": "808/501/251/196 and the 17-point controls (11,6) remainder (5,1),(6,0); (10,7) empty", + "observed": "ROWS18 (12, 6) rows=808; (11, 7) rows=501; (10, 8) rows=251; (9, 9) rows=196; CONTROL 17-point rows reproduce; PASS_TIGHT_ROWS", + "status": "recomputed fresh" + }, + { + "anchor": "PR 2933 CLASSIFY lines incl. (7,1)/(8,2) 32=32 TIGHT", + "command": "python3.12 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py quick (vendored vanish.class_table)", + "expected": "CLASS (10,8) A_vanish (7, 1) value=32 need=32 TIGHT; CLASS (10,8) D_vanish (8, 2) value=32 need=32 TIGHT; L7 m=3 cases=6720", + "observed": "CLASS (10, 8) A_vanish vanish_split=(5, 5) other=(7, 1) value=32 need=32 -> survives TIGHT; CLASS (10, 8) D_vanish vanish_split=(4, 4) other=(8, 2) value=32 need=32 -> survives TIGHT; LEMMA tight-equality Sidon exhaustive m=3 cases=6720 ok=true", + "status": "recomputed fresh" + }, + { + "anchor": "PR 2933 F2^4 census", + "command": "same run (vendored vanish.census_f4)", + "expected": "41,341 covers, no dead-class hits", + "observed": "CENSUS f2^4 covers=41341 (dead classes hit: none)", + "status": "recomputed fresh" + }, + { + "anchor": "PR 2773 k10 budget-3", + "command": "python3.12 -I -B run_anchors_all.py (in a scratch copy of anchors.py + vendor/agent64_search17.py with NO ANCHOR-PROGRESS.json; per-sub-shard receipts)", + "expected": "149,990,400 (every leaf at exact excess 3)", + "observed": "PASS_ANCHORS_K10B3 count=149990400 total_hist={'3': 149990400} shards=62; ANCHOR_RUNNER k10b3 complete rounds=3", + "status": "re-walked in full from empty receipts (62/62 sub-shards)" + }, + { + "anchor": "PR 2773 k11 levels 3-4", + "command": "same run (second mode)", + "expected": "0, 0", + "observed": "PASS_ANCHORS_K11B4 count=0 total_hist={} shards=62; ANCHOR_RUNNER k11b4 complete rounds=4; ANCHOR_RUNNER ALL COMPLETE", + "status": "re-walked in full from empty receipts (62/62 sub-shards)" + } + ], + "class_walks": { + "class71": "run_tight.py class71 (17.1 s): PASS_TIGHT_CLASS71, normalized_pairs=0, covering_pairs=0. Re-run from an empty TIGHT-PROGRESS.json receipt.", + "class82": "run_tight.py class82 across 8 deterministic shards (per-shard receipts; one shard exceeded the 600 s harness timeout mid-shard and was resumed from its receipts, the completed shards' receipts were kept): PASS_TIGHT_CLASS82, normalized_sidon_pairs=4287920, non_1_invariant_pairs=4175360, checked=28815360, covering_configs=0, fail_hist={('I','II','III'): 28815360}.", + "class60": "run_tight.py class60 across 8 shards (per-shard receipts TIGHT-C60-.json, merged by run_tight.py merge60): PASS_TIGHT_CLASS60, d_checked=169911 (= C(31,5), complete partition), d_with_transversals=0, covering_triples=0. Harness note: the eight shard processes were suspended while foreground commands ran and resumed afterwards (all completed; wall ~582 s each) - long walks must either be blocking foreground chunks or tolerate suspension.", + "code_provenance": "The class60 walk executed the pre-prune version of tight.transversals6 (the capacity bound uncov.bit_count() > 6*(6 - len(cur)) was added afterwards; it is a valid bound since each element covers exactly 6 requirements, and a replay of the pinned code gives the identical partition and verdict)." + }, + "schema_version": 1 +} diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/CERTIFICATE.json b/research/f7-18point-tight-classes-seed4c1e7b30/CERTIFICATE.json new file mode 100644 index 0000000000..6f8c3f70d8 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/CERTIFICATE.json @@ -0,0 +1,102 @@ +{ + "obstruction_numbers": { + "fourier_71": { + "contradiction": true, + "lower_bound": 239, + "m4_analogue_lower": 7, + "m4_analogue_need": 7, + "need": 175, + "sum_alpha": 135, + "sum_beta": 135 + }, + "class82": { + "admissible_choice_sets": 28815360, + "checked": 28815360, + "covering_configs": 0, + "fail_hist": {"('I', 'II', 'III')": 28815360}, + "non_1_invariant_pairs": 4175360, + "normalized_sidon_pairs": 4287920 + }, + "class60": { + "d_checked": 169911, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "transversals_total": 0 + }, + "identity_11_7": {"excess": 13, "sum_rho2_min": 17, "sum_rho2_max": 169}, + "identity_9_9": {"excess": 17, "sum_rho2_min": 19, "sum_rho2_max": 289}, + "split_order_notes": "(s, t) = (points in the even coset E = F2^6, points in the odd coset); a class is (vanishing side, forced split of that side, split of the other side) across ker(psi); mirrors are identical by odd translation", + "splits": { + "12_6": { + "A_vanish": {"classes_dead_now": [[6, 0]], "classes_remaining": [[5, 1], [4, 2], [3, 3]], "forced_structure": "(6,0): |A0+A1| = 32 (whole odd half, excess 4), A0 + D = H and A1 + D = H' full -- UNSATISFIABLE"}, + "D_vanish": {"classes_dead_PR2933": [[12, 0], [11, 1], [10, 2]], "classes_remaining": [[9, 3], [8, 4], [7, 5], [6, 6]]}, + "verdict": "narrowed: (6,0) PROVEN impossible here; not excluded" + }, + "10_8": { + "A_vanish": {"classes_dead_now": [[7, 1]], "classes_dead_PR2933": [[8, 0]], "classes_remaining": [[6, 2], [5, 3], [4, 4]]}, + "D_vanish": {"classes_dead_now": [[8, 2]], "classes_dead_PR2933": [[10, 0], [9, 1]], "classes_remaining": [[7, 3], [6, 4], [5, 5]]}, + "verdict": "narrowed: both tight classes PROVEN impossible here; not excluded" + }, + "11_7": { + "verdict": "no vanishing possible (L2); row remainder 501 narrowed by sum rho^2 >= 17; not excluded" + }, + "9_9": { + "verdict": "no vanishing possible (L2); row remainder 196 narrowed by sum rho^2 >= 19; not excluded" + } + } + }, + "labels": [ + { + "statement": "(10,8) A-vanish (7,1) is PROVEN impossible: no cover realizes the class. L7 (PR 2933, PROVEN; a general pigeonhole valid at m=6) forces |A0+A1| = 25 with |A0| = |A1| = 5 in F2^5 (all 25 cross sums distinct); with f = 1_A0, g = 1_A1, h = 1_S on S = A0+A1, Fourier over F2^5 gives h_hat = f_hat g_hat pointwise, so Parseval forces sum_{v!=0} h_hat^2 = 32*25 - 625 = 175 while odd parity (both sizes odd) makes f_hat^2, g_hat^2 >= 1 pointwise and (f_hat^2-1)(g_hat^2-1) >= 0 forces sum_{v!=0} f_hat^2 g_hat^2 >= 135 + 135 - 31 = 239 > 175. Contradiction.", + "label": "PROVEN", + "evidence": "Exact integers in tight.fourier_71_identity (verify.py quick prints FOURIER (7,1) need=175 lower=239 contradiction=True). The identity is tight exactly where covers exist: the m=4 analogue (|A0| = 7, |A1| = 1 in F2^3) computes need = lower = 7 and its class has 512 real covers (both reproduced in the m=4 control)." + }, + { + "statement": "Independently, (10,8) A-vanish (7,1) is empty by complete enumeration: zero normalized Sidon 5-pairs (0 in both sets, Delta(A0) disjoint from Delta(A1), equivalent to |A0+A1| = 25) exist in F2^5. Coverage in the class is independent of the free parameter d1 (every H'-valued coverage line translates by d1 as a whole), so no configuration is hidden in the parameter.", + "label": "PROVEN", + "evidence": "tight.class71_pairs (complete backtracking over all C(31,4) normalized A1 and all admissible A0) returns 0 pairs; the algorithm is validated against full brute force at m=4 (5040 = 5040, test_sidon_backtracking_m4_matches_bruteforce), against plain inner loops on 12 m=5 slices (0 mismatches), and 2M random F2^5 pairs top out at |A0+A1| = 23. The d1 invariance is proven in the module docstring and machine-checked (test_class71_free_parameter_invariance). Receipt: TIGHT-PROGRESS.json class71 (PASS_TIGHT_CLASS71)." + }, + { + "statement": "(10,8) D-vanish (8,2) is PROVEN impossible: all 28,815,360 L7-forced equality configurations fail all three translated coverage lines simultaneously (fail_hist = {('I','II','III'): 28815360}), zero covers. The parametrization: 4,287,920 normalized Sidon 4-pairs (D0, D1) with 0 in both (|D0+D1| = 16); of these 112,560 have the complement C of D0+D1 1-invariant (necessary for |A0+A1| = 16), each contributing up to 2^8 = 256 A0t = A0 + w choice sets; coverage is independent of the free parameter w (proven; the whole configuration's H'-valued lines translate by w).", + "label": "PROVEN", + "evidence": "tight.class82_run, complete 8-shard walk with per-shard receipts (TIGHT-PROGRESS.json class82; PASS_TIGHT_CLASSES). Normalization (0 in D0, 0 in D1, delta = 1 under GL(5,2)) is complete: half-translations and a common GL(5,2) map preserve all four L3 lines (machine-checked, test_half_translation_invariance). End-to-end reduction validation at m=4: the four L3 lines and a DIRECT S+S = F2^5 cover test agree on all 4,096 analogue configurations with 512 covers accepted by both routes (test_m4_class71_analogue_direct_agreement)." + }, + { + "statement": "(12,6) A-vanish (6,0) is PROVEN impossible: no 6-set D of F2^5 admits any 6-set X with X + D = F2^5. All 169,911 normalized 6-sets D (0 in D) were walked with a complete branch-on-uncovered transversal search: every D has zero 6-set transversals, so lines (I'')/(II'') of the class are unsatisfiable.", + "label": "PROVEN", + "evidence": "tight.transversals6 + tight.class60_run, complete 8-shard walk over all C(31,5) = 169,911 normalized D with per-shard receipts (TIGHT-C60-*.json, merged by run_tight.py merge60; PASS_TIGHT_CLASSES shows d_checked=169911, d_with_transversals=0). Normalization (0 in D via the H-half translation, 0 in A1 via the H'-half translation; the class forces D1 empty) is complete. Positive control: the same search logic recovers real transversals at m=3 for 4+2 full pairs (test_transversals6_positive_control_m3)." + }, + { + "statement": "Multiplicity classification (the forced excess-4 structure of any full-sumset 6-set pair in F2^5): r = 1 + rho with sum rho = 4; per nonzero v, f_hat(v) g_hat(v) = rho_hat(v) in {0, +-4}; |V22| = 2 sum rho^2 - 1. Exactly two patterns survive: rho = 2+2 on two points (|V22| = 15) and rho = 1+1+1+1 on an affine 2-flat {p1, p2, p3, p1+p2+p3} (|V22| = 7). The patterns 4*delta_p (Parseval forces 156 = 124 + (36a+16b) with |Vf| = 0), 3+1 (rho_hat attains +-2 for p != q) and 2+1+1 (|V22| = 2^{5-r}-1 in {1,3,7,15,31}, never 11) are PROVEN dead.", + "label": "PROVEN", + "evidence": "tight.rho_classification (exact integers) with the Walsh constraints machine-checked on random and explicit instances (test_walsh_constraints: 2+1+1 sizes sampled over 300 instances lie in {1,3,7,15,31}; the 3+1 +-2 witness; explicit 2+2 gives 15; explicit 2-flat gives 7)." + }, + { + "statement": "(11,7)/(9,9) identity gap: the cross-sum multiplicity identity yields PROVEN necessary conditions - for an odd-odd split (s, t) covering A + D = E = F2^6, sum rho^2 >= 17 at (11,7) (excess 13) and >= 19 at (9,9) (excess 17) - excluding the all-ones excess pattern on both splits and the single-double pattern (2, 1^11) at (11,7).", + "label": "PROVEN", + "evidence": "tight.identity_odd_sides: pointwise (f_hat^2-1)(g_hat^2-1) >= 0 (both Walsh transforms odd since s, t odd) summed over 63 nonzero characters against Parseval (64*sum rho^2 - excess^2 >= (64s-s^2)+(64t-t^2)-63); exact integers asserted in test_identity_odd_sides_numbers and positively validated on every odd-odd-split cover of F2^4 (test_identity_soundness_on_f24_covers)." + }, + { + "statement": "The same identity is DEMOTED as an exclusion mechanism for (11,7)/(9,9): the bounds sum rho^2 >= 17 resp. >= 19 are attainable by integer multiplicity patterns, so no contradiction arises (the excess 13/17 is too large for the rigidity that killed (7,1)). The row remainders 501/196 stand.", + "label": "DEMOTED", + "evidence": "tight.identity_odd_sides reports contradiction=False for both splits with sum_rho2_max = 169 resp. 289 (verify.py classes prints both lines); allowed patterns include (2,2,1^9) [17] and (3,1^10) [19] at (11,7) and (2,1^15) [19] at (9,9)." + }, + { + "statement": "Every recorded anchor was reproduced before any new number: PR 2870 OBSTRUCTION parseval=696 allowed=504 deficit=192; PR 2911 SQUEEZE table (1248/696, 1166/798 vs 21294, 1080/896, 990/990), NOVANISH lines and ROWS18 808/501/251/196; PR 2933 CLASSIFY lines incl. both (7,1)/(8,2) value=32 need=32 TIGHT flags and the L7 m=3 census cases=6720; and both heavy PR 2773 anchors re-walked IN FULL from EMPTY receipts (PASS_ANCHORS_K10B3 count=149990400 total_hist={'3': 149990400} shards=62; PASS_ANCHORS_K11B4 count=0 total_hist={} shards=62).", + "label": "CHECKED", + "evidence": "ANCHOR-REPRO.json records every command and observed marker. The heavy walks live in ANCHOR-PROGRESS.json (one section per mode, per-sub-shard receipts) and started from a missing receipt file (run_anchors_all.py printed 'fresh receipts confirmed'). Receipt trap recorded: the extracted predecessor package's quick mode prints ANCHORS receipt lines from its committed receipts - that is receipt validation, not recomputation; the fresh walks here are the recomputation." + }, + { + "statement": "The PR 2773 n5 set controls (0 nine-point covers of F2^5, max 29/32; 99,200 ten-point covers through {0}) are recorded state reproduced by the predecessors; this package did not re-walk the C(32,10) census and does not claim to have.", + "label": "CHECKED", + "evidence": "Recorded in PR 2773/PR 2933 and quoted as inputs with provenance pins in SOURCES.json; the m=4 analogue controls and the F2^4 census (41,341 covers, recomputed fresh in verify.py quick) are this package's own ground-truth checks." + }, + { + "statement": "No 18-point cover of F2^7 was constructed; the gap 20 <= f(7) <= 24 is unchanged. The three decided classes are gone, but (12,6) and (10,8) retain seven classes each and (11,7)/(9,9) retain their row remainders.", + "label": "CHECKED", + "evidence": "All three class enumerations return zero covering configurations (receipts above); search best at k=18 remains the recorded 118/128 of PR 2911/2634, untouched here." + } + ], + "result": "KB3g tight-class resolution (outcome=partial): the 18-point cover question for F2^7 is not decided, but its three tightest classes are. The (10,8) tight classes A-vanish (7,1) and D-vanish (8,2) and the (12,6) full-sumset class A-vanish (6,0) are each PROVEN impossible - (7,1) by an exact Fourier/Parseval contradiction (175 < 239) plus a zero Sidon-5-pair enumeration, (8,2) by complete enumeration of all 28,815,360 L7-forced equality configurations (every one fails all three coverage lines), (6,0) by a complete transversal walk over all 169,911 normalized 6-sets D (no 6-set X has X + D = F2^5), with an exact multiplicity classification of the forced excess-4 structure alongside. The (11,7)/(9,9) identity gap is pressed with the cross-sum multiplicity identity: PROVEN necessary conditions sum rho^2 >= 17 resp. >= 19 (excluding the all-ones excess pattern and more), but no contradiction - DEMOTED as an exclusion mechanism, row remainders 501/196 stand. No kappa, supplier or selected-frontier change; the gap 20 <= f(7) <= 24 is unchanged.", + "schema_version": 1 +} diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/NOTICE.md b/research/f7-18point-tight-classes-seed4c1e7b30/NOTICE.md new file mode 100644 index 0000000000..8a0710f500 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/NOTICE.md @@ -0,0 +1,66 @@ +# NOTICE - attribution and licenses + +Contributor: **Aaron Wang**, with help from opencode (substantial AI +assistance in scoping, implementation, verification and writing; no model +named; no independent human review claimed). This package is contributed +under the repository's Apache-2.0 license; see the root `LICENSE` and +`NOTICE` files. The vendored files retain their source licenses and are +reproduced byte-exactly with SHA-256 pins (see `SOURCES.json` and the byte-pin +checks in `verify.py`). + +Predecessor credit (every cited PR author verified against current ground +truth with `gh pr view NNN --json author,title` at writing time): + +- [PR 943](https://github.com/CrocSwap/integer-mult-bounds/pull/943) by Ross + Richardson (RossRichardson) - the prefix-walk model and the + `P + P = F2^n` covering condition this question lives in. +- [PR 1185](https://github.com/CrocSwap/integer-mult-bounds/pull/1185) by + Doug Colkitt (Mister-Meeseeks) - the pinned record `f(5) = 12`, + `f(6) = 16`, `20 <= f(7) <= 24` and the frozen tier `EXPECTED.json`. +- [PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542) by + Aaron Wang (navinor) - the length-18 exclusion and the claim "No 17-point + set covers `F2^7`". +- [PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634) by + Aaron Wang (navinor) - the recorded KB3b state (20-point covers abundant; + no 19-point cover in 200 restarts, max `124/128`; search best `118/128` + at `k=18`) that this package's results are compared against. +- [PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773) by + Aaron Wang (navinor) - the split-by-split audit, the Sidon/pair-sum budget + enumeration (`cover17.py` / `search17.py`, vendored here byte-exact as + `vendor/agent64_cover17.py` / `vendor/agent64_search17.py`), the census + floors and the n5 control value `99,200`. +- [PR 2870](https://github.com/CrocSwap/integer-mult-bounds/pull/2870) by + Aaron Wang (navinor) - the odd-coverage Fourier/Parseval identity + (OBSTRUCTION `696/504/192`, reproduced) and the resumable anchor driver + `anchors.py` (vendored byte-exact, re-walked here from empty receipts). +- [PR 2911](https://github.com/CrocSwap/integer-mult-bounds/pull/2911) by + Aaron Wang (navinor) - the `(A, D)` reduction lemma, the squeeze/deficit + bookkeeping, the per-character profile system and its no-vanishing + sub-case (the forced-vanishing premise), the row remainder + `808/501/251/196`. Its engine `cover18.py` is vendored byte-exact as + `vendor/cover18.py`. +- [PR 2933](https://github.com/CrocSwap/integer-mult-bounds/pull/2933) by + Aaron Wang (navinor) - the immediate predecessor: the L2/L3/L4/L5/L7 + classification, the class tables, the tight-class Sidon pinning and the + open questions 1 and 3 that name this step. Its engine `vanish.py` is + vendored byte-exact as `vendor/vanish.py`. +- [PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) by + Nicholas Stone (NicholasStone, Kimi agent) - the completed `(10,10)` + simple-20-cycle word census; recorded state only, not re-run here. His + concurrent repeated-state `L = 20` word claim + ([discussion 1166 comment 18954844](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18954844)) + is a different (word-level) object and is untouched. + +Vendored files (byte-exact, enforced by byte-pin checks in `verify.py`): + +| Local path | Source | SHA-256 | +|---|---|---| +| `vendor/vanish.py` | PR 2933 `vanish.py` | `6c605c54074f725321c5d770d538a652bf7727598a128270831f92fe7b9746d9` | +| `vendor/cover18.py` | PR 2911 `cover18.py` | `24c6a2f4911dc2d5de76972eb5ae93dc4e66d8fa1e904443de6d0638e70c0a04` | +| `vendor/agent64_cover17.py` | PR 2773 `cover17.py` (via PR 2911/2933's pinned `vendor/`) | `082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654` | +| `vendor/agent64_search17.py` | PR 2773 `search17.py` (via PR 2911/2933's pinned `vendor/`) | `9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674` | +| `anchors.py` | PR 2870 `anchors.py` (byte-identical in PR 2911/2933) | `73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7` | + +Predecessor packages were read byte-exactly from their PR heads with +`agent_tools.py pr-tree-extract` (extracted to scratch paths, never into the +tracked base tree) and were never imported at runtime. diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/README.md b/research/f7-18point-tight-classes-seed4c1e7b30/README.md new file mode 100644 index 0000000000..21ac6ddb29 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/README.md @@ -0,0 +1,228 @@ +# KB3g - the tight classes of the 18-point cover question for `F2^7`, and the identity gap at (11,7)/(9,9) + +**Set-level finite result, no words enumerated. Outcome=partial: the 18-point +question is not decided, but its three tightest classes are.** The two PR 2933 +TIGHT classes of the (10,8) split, `A`-vanish `(7,1)` and `D`-vanish `(8,2)`, +and the full-sumset class `(6,0)` of (12,6) are each **PROVEN impossible** - +no cover realizes them - by an exact Fourier contradiction plus complete +enumeration of the L7-forced Sidon equality configurations. The `(11,7)/(9,9)` +identity gap is pressed with the cross-sum multiplicity identity: it yields +PROVEN new necessary conditions (`sum rho^2 >= 17` resp. `>= 19`) but no +contradiction, so those two splits' row remainders `501/196` stand. No +18-point cover was constructed; the gap `20 <= f(7) <= 24` is unchanged. + +## Object and chain of record + +In the PR943 prefix-walk model +([Ross Richardson, `research/universal-connector-boundary`](https://github.com/CrocSwap/integer-mult-bounds/pull/943)) +a restored seven-source singleton word is universal exactly when its prefix +set `P` covers: `P + P = F2^7`. A parity split `S = A u B` has `A` in the even +coset `E` (s points) and `B` in the odd coset (t points); with `D = p + B` +inside `E = F2^6` the PR 2911 reduction (PROVEN there) says `S` covers iff +`A + D = E` and `(A+A) u (D+D) = E`. Record chain, all authors verified +against current ground truth with `gh pr view NNN --json author,title` at +writing: [PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542), +[PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634), +[PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773), +[PR 2870](https://github.com/CrocSwap/integer-mult-bounds/pull/2870), +[PR 2911](https://github.com/CrocSwap/integer-mult-bounds/pull/2911), +[PR 2933](https://github.com/CrocSwap/integer-mult-bounds/pull/2933) by Aaron +Wang (navinor); [PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) +by Nicholas Stone (NicholasStone) is the concurrent `L = 20` WORD census - +recorded state only; this package stays strictly on the SET level. This +package executes PR 2933's open questions 1 and 3. + +## Verdict per class (exact integers throughout) + +| Split | Class | PR 2933 status | Verdict here | Deciding evidence | +|---|---|---|---|---| +| `(10,8)` | `A`-vanish `(7,1)` (tight 32=32) | pinned to Sidon | **PROVEN impossible** | Fourier contradiction `175 < 239`; zero Sidon 5-pairs exist | +| `(10,8)` | `D`-vanish `(8,2)` (tight 32=32) | pinned to Sidon | **PROVEN impossible** | all 28,815,360 equality configurations fail all three coverage lines | +| `(12,6)` | `A`-vanish `(6,0)` (full odd half) | pinned to full sumset | **PROVEN impossible** | no 6-set `D` of `F2^5` has any 6-set `X` with `X + D = F2^5` (all 169,911 normalized `D` walked) | +| `(11,7)` | (no vanishing possible) | row remainder 501 | narrowed: `sum rho^2 >= 17` PROVEN | cross-sum multiplicity identity; no contradiction | +| `(9,9)` | (no vanishing possible) | row remainder 196 | narrowed: `sum rho^2 >= 19` PROVEN | same identity; no contradiction | + +Surviving after this package: `(12,6)` `A`-vanish `(5,1)(4,2)(3,3)` and +`D`-vanish `(9,3)(8,4)(7,5)(6,6)`; `(10,8)` `A`-vanish `(6,2)(5,3)(4,4)` and +`D`-vanish `(7,3)(6,4)(5,5)`; `(11,7)/(9,9)` with their row remainders plus +the new multiplicity conditions. + +## The (7,1) class: an exact Fourier contradiction, and empty enumeration + +PR 2933's L7 (PROVEN there; the equality chain is a general pigeonhole valid +at `m = 6`) pins every cover of the class to `|A0+A1| = 25` with `|A0| = +|A1| = 5` (all 25 cross sums distinct) inside `F2^5`. Let `f = 1_A0`, +`g = 1_A1`, `h = 1_S` on `S = A0+A1` (`|S| = 25`, multiplicity exactly 1). +Fourier over `F2^5` gives `h_hat(v) = f_hat(v) g_hat(v)` for every `v`, so +Parseval gives `sum_{v != 0} h_hat^2 = 32*25 - 625 = 175` while +`sum_{v != 0} f_hat^2 = sum_{v != 0} g_hat^2 = 32*5 - 25 = 135`. Both sizes +are odd, so every `f_hat(v)` is odd and `f_hat^2 >= 1` pointwise; from +`(f_hat^2 - 1)(g_hat^2 - 1) >= 0`, + + f_hat(v)^2 g_hat(v)^2 >= f_hat(v)^2 + g_hat(v)^2 - 1 (v != 0), + +whence `sum h_hat^2 >= 135 + 135 - 31 = 239 > 175`. Contradiction - the +class is empty. The `m = 4` analogue (`|A0| = 7, |A1| = 1` in `F2^3`) +computes `need = lower = 7` exactly (no contradiction), matching the 512 +real covers of that analogue class in the `F2^4` control - the identity is +tight exactly where covers exist. + +Independently, the complete enumeration of normalized Sidon 5-pairs (`0` in +both sets, `Delta(A0)` disjoint from `Delta(A1)`) finds **zero** pairs; the +backtracking is validated against full brute force at `m = 4` +(`5040 = 5040`), against plain inner loops on `m = 5` slices, and the +`F2^5` hill-climb tops out at `|A0+A1| = 23`. Coverage in the class is +independent of the free parameter `d1` (each H'-valued line translates by +`d1` as a whole), so there is no hidden parameter: **no (10,8) A-vanish +(7,1) cover exists**. + +## The (8,2) class: 28,815,360 equality configurations, all failing + +L7 pins the class to `|A0+A1| = 16` and `|D0+D1| = 16`, disjoint with union +the whole odd half. Normalizing `0` in `D0`, `0` in `D1` and `delta = 1` +(WLOG under `GL(5,2)`; half-translations preserve all four coverage lines - +machine-checked), the `A`-side is parametrized by `w` (32 values) and one +choice element per `{x, x+1}` pair inside the complement `C` of `D0+D1` +(256 choices when `C` is 1-invariant), and coverage is independent of `w`. +Complete walk: 4,287,920 normalized Sidon 4-pairs `(D0, D1)`, of which +112,560 have `C` 1-invariant; all 28,815,360 `(pair, choice)` configurations +fail **all three** translated coverage lines simultaneously +(`fail_hist = {("I","II","III"): 28815360}`), zero covers. The reduction is +validated end-to-end at `m = 4`: the four L3 lines and a DIRECT +`S + S = F2^5` cover test agree on all 4,096 analogue configurations +(512 covers accepted by both routes). + +## The (6,0) class: no full-sumset pair of 6-sets exists in `F2^5` + +The class forces `A0+A1 = F2^5` (36 pairs, excess 4) and `A0 + D = A1 + D = +F2^5` with `|D| = 6`. Two exact layers: + +1. **Multiplicity classification (PROVEN).** For any 6-set pair `X, Y` with + `X + Y = F2^5`, write `r = 1 + rho`, `sum rho = 4`; then + `rho_hat(v) = f_hat(v) g_hat(v) in {0, +-4}` on `v != 0` (both Walsh + values even, product bounded by `sum rho = 4`), and `|V22| = + 2 sum rho^2 - 1` with `V22 = {v != 0: |f_hat| = |g_hat| = 2}`. Exactly + two multiplicity patterns survive the Walsh constraints: `rho = 2+2` on + two points, and `rho = 1+1+1+1` on an affine 2-flat + `{p1, p2, p3, p1+p2+p3}`; the patterns `4 delta_p`, `3+1` and `2+1+1` + are PROVEN dead (`2^{5-r} - 1` is never 11; `+-2` occurs for `3+1`; + Parseval forces `156 = 124 + (36a+16b)` with `|Vf| = 0` for `4 delta_p`). +2. **Complete transversal walk (PROVEN).** `X + D = F2^5` says `X` hits all + 32 translates of `D`. Normalizing `0` in `D` and `0` in `A1` (the class + forces `D1` empty), all 169,911 normalized 6-sets `D` were walked with a + complete branch-on-uncovered search: **every** `D` has zero 6-set + transversals. Hence lines (I'')/(II'') are unsatisfiable and **no + (12,6) A-vanish (6,0) cover exists**. Positive control: the same search + recovers real transversals at `m = 3` (4+2 pairs); a miniature cross-check + finds no 3+3 full pair in `F2^3` either (all 3,136 pairs scanned). + +## The identity gap at (11,7)/(9,9): pressed, not cut + +One bounded pivot on the named next identity (cross-sum multiplicities; the +vanishing route is vacuous there by PR 2933's L2). With `A` an `s`-set and +`D` a `t`-set covering `A + D = E = F2^6`, `r = 1 + rho` with +`sum rho = s*t - 64`; both `s, t` odd make both Walsh transforms odd, so the +same pointwise inequality yields the exact necessary condition + + 64 sum rho^2 - (s*t - 64)^2 >= (64 s - s^2) + (64 t - t^2) - 63. + +At (11,7): `sum rho^2 >= 17` (excess 13); at (9,9): `sum rho^2 >= 19` +(excess 17). Both bounds are attainable by integer multiplicity patterns, so +the identity does **not** contradict coverage: it is **DEMOTED** as an +exclusion mechanism for these splits (the excess 13 resp. 17 is too large for +the rigidity that killed (7,1)). What it does give is PROVEN new necessary +conditions: the all-ones excess pattern is impossible on both splits, and at +(11,7) also the single-double pattern `(2, 1^11)`. The identity is validated +positively on every odd-odd-split cover of `F2^4` (soundness). The row +remainders `501/196` stand. + +## Reproduce + +Standard library only, CPython 3.12, from the repository root: + +```sh +python3 -I -B research/f7-18point-tight-classes-seed4c1e7b30/test_engine.py +python3 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py quick +python3 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py novanish +python3 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py rows +python3 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py classes +python3 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py anchors +``` + +Expected markers: `Ran 13 tests ... OK`, `PASS_TIGHT_QUICK`, +`PASS_TIGHT_NOVANISH`, `PASS_TIGHT_ROWS`, `PASS_TIGHT_CLASSES`, +`PASS_TIGHT_ANCHORS`. The class walks are resumable with per-shard receipts +(`TIGHT-PROGRESS.json`, one section per mode; `run_tight.py class71|class82| +class60 [--shard k] [--progress F]`); `run_tight.py merge60` merges the eight +per-shard `TIGHT-C60-*.json` receipts of the class60 walk. A replay against +committed receipts validates those receipts; delete them (or pass `--progress` +to a fresh path) to re-walk. The heavy PR 2773 anchors were re-walked from +**empty** receipts (`anchors.py k10b3|k11b4`, resumable per sub-shard in +`ANCHOR-PROGRESS.json`, one section per mode). + +## Recorded anchors (reproduced before any new number) + +| Anchor | Value | Status here | +|---|---|---| +| PR 2870 OBSTRUCTION | `parseval=696 allowed=504 deficit=192` | recomputed (vendored `cover18.squeeze_numbers`) | +| PR 2911 SQUEEZE table | `(12,6)` `1248/696`; `(11,7)` `1166/798` vs `21294`; `(10,8)` `1080/896`; `(9,9)` `990/990` | recomputed | +| PR 2911 NOVANISH | `(12,6)`, `(10,8)` infeasible: vanishing forced | recomputed (`verify.py novanish`) | +| PR 2911 ROWS18 | `808/501/251/196` | recomputed (`verify.py rows`) | +| PR 2933 CLASSIFY lines | both `(7,1)/(8,2)` `value=32 need=32 -> survives TIGHT`; L7 `m=3 cases=6720` | recomputed (vendored `vanish.py`) | +| PR 2773 n5 control | `0` nine-point covers; `99,200` ten-point covers through `{0}` | recorded state (PR 2933 census; not re-walked here) | +| PR 2773 `k10 budget-3` | `149,990,400` | re-walked in full from empty receipts (62/62 sub-shards) | +| PR 2773 `k11` levels 3-4 | `0`, `0` | re-walked in full from empty receipts (62/62 sub-shards) | + +`ANCHOR-REPRO.json` records commands and observed outputs. Receipt trap +recorded there: a resumed walk against a committed receipt silently "passes" - +the two heavy anchors here started from a missing `ANCHOR-PROGRESS.json` +(`run_anchors_all.py` printed `fresh receipts confirmed`), and the extracted +predecessor package's own `quick` mode prints receipt lines from its committed +receipts, which is receipt validation, not recomputation. + +## Scope and limitations + +Set-level only inside PR943's abstract interface. Not checked: anything +word-level (the repeated-state `L = 20` word census is Nicholas Stone's +concurrent claim, +[discussion 1166 comment 18954844](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18954844); +this package stays strictly on the set-level object), the 19-point cover +question, walk-realizability of any cover, and any kappa, supplier, tariff or +selected-frontier implication. The surviving classes `(5,1)(4,2)(3,3)`, +`(9,3)(8,4)(7,5)(6,6)`, `(6,2)(5,3)(4,4)`, `(7,3)(6,4)(5,5)` are not decided: +their floors hold with slack and their equality structure is not pinned by +L7; no claim is made about them. The (11,7)/(9,9) multiplicity conditions are +necessary, not sufficient; no row of the PR 2911 remainder is excluded by +them. The `m = 4` analogue controls validate the reduction chain but are not +a proof at `m = 6`; the `m = 6` results rest on the exhaustive enumerations +(13 machine tests, byte-pinned engines) and the exact identities. The gap +`20 <= f(7) <= 24` is unchanged; in particular the (10,8) and (12,6) splits +remain open through their surviving classes, and (11,7)/(9,9) remain open at +their recorded row remainders. + +## Open next questions + +1. **Decide the surviving non-tight classes.** Why it matters: `(12,6)` and + `(10,8)` each retain seven classes; excluding them settles two of the four + 18-point splits. First step: press L5's multi-vanishing grid (two + characters at once, counts `(x, y, y, x)`) against the class floors at the + product characters for `(5,1)` and `(6,2)`. Blocked by: nothing structural; + a bounded joint enumeration. +2. **Find the sharper (11,7)/(9,9) identity.** Why it matters: those splits + carry the other half of the 18-point question and the vanishing route is + vacuous there. First step: combine the `sum rho^2` conditions with the even + half `(A+A) u (D+D) = E` multiplicities (PR 2870 used only odd coverage) as + a second layer on the 501/196 rows. Blocked by: no known coupling identity + between the odd-line multiplicities and the even-line self-sums. +3. **Search for an 18-point cover outside the vanishing classes.** Why it + matters: a construction keeps the `L = 22` route alive regardless of the + exclusions. First step: seeded search over the (11,7)/(9,9) row remainder + profiles with the new multiplicity constraints as admissibility filters. + Blocked by: nothing structural; a failed bounded search is not an + exclusion. + +See [NOTICE.md](NOTICE.md) for attribution and licenses, +[TASK.json](TASK.json) for the task card and scope change, +[SOURCES.json](SOURCES.json) for pins and credit, +[CERTIFICATE.json](CERTIFICATE.json) for the labelled result record, and +[ANCHOR-REPRO.json](ANCHOR-REPRO.json) for the in-session reproductions. diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/SOURCES.json b/research/f7-18point-tight-classes-seed4c1e7b30/SOURCES.json new file mode 100644 index 0000000000..21f159fac8 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/SOURCES.json @@ -0,0 +1,133 @@ +{ + "base_commit": "d3add2cc28e958bedec197ab32b5526c5a222628", + "files": [ + { + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "path": "docs/research/agent-task-catalog.json", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6", + "usage": "provenance" + }, + { + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "path": "certificates/selected-result.json", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "usage": "provenance" + }, + { + "git_blob": "160a96c50f77ba411af957b554da05a8470e70ca", + "path": "research/universal-connector-six-source/EXPECTED.json", + "sha256": "f1b1bec330640c81ac0da25ee8b3a0a49fe9ea5bb2eadaaa787c64bd62c9e73a", + "usage": "provenance" + } + ], + "notes": { + "concurrent_scopes": "Nicholas Stone (NicholasStone) holds the repeated-state L=20 word census claim (discussion 1166 comment 18954844), splits (10,9)/(10,8),(9,9) at the WORD level; this package is set-level only and enumerates no words. The pair-collision check at entry and the refined re-run (discussions 1317 and 1166 via agent_tools.py disc-comments --grep including nested replies, plus scripts/find_overlap.py with the object's proper names and synonyms) found no claim on the tight classes, the (6,0) class or the (11,7)/(9,9) identity gap.", + "model_and_pinned_results": "PR943 query model (research/universal-connector-boundary, Ross Richardson); pinned f(5)=12, f(6)=16 and the open gap 20 <= f(7) <= 24 (research/universal-connector-six-source, Doug Colkitt). Read and reproduced byte-exactly, never imported.", + "predecessor_chain": "PR 2542 (Aaron Wang) claimed 'no 17-point set covers F2^7' and excluded length 18; PR 2634 (Aaron Wang) continued KB3b; PR 2773 (Aaron Wang) audited the claim split-by-split and supplied the Sidon/pair-sum budget enumeration; PR 2870 (Aaron Wang) closed the (5,1),(6,0) rows with the odd-coverage Fourier/Parseval identity (OBSTRUCTION 696/504/192); PR 2911 (Aaron Wang) narrowed the 18-point question to four splits and PROVED the vanishing-character restriction on (12,6)/(10,8); PR 2933 (Aaron Wang) classified the vanishing configurations and pinned the tight classes (10,8) (7,1)/(8,2) and (12,6) (6,0) to exact forced structure. This package executes PR 2933's open questions 1 and 3.", + "question": "KB3g: decide the tight classes of the 18-point cover question for F2^7 and press the (11,7)/(9,9) identity gap. Outcome=partial: (7,1), (8,2) and (6,0) PROVEN impossible; (11,7)/(9,9) narrowed by PROVEN multiplicity conditions (sum rho^2 >= 17 resp. >= 19) with no contradiction; no split excluded outright." + }, + "references": [ + { + "head": "25ea0e94250444db9ab05c3c8f1a66ba68e737b6", + "local_path": "vendor/vanish.py", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from PR 2933's package, never imported at runtime), credit Aaron Wang (navinor), PR 2933: the class tables, the L7 tight-equality census (m=3 cases=6720) and the F2^4 census reproduced by verify.py quick. Enforced by byte-pin checks.", + "pr": 2933, + "sha256": "6c605c54074f725321c5d770d538a652bf7727598a128270831f92fe7b9746d9", + "source_path": "research/f7-18point-vanishing-seedfc618722/vanish.py" + }, + { + "head": "6739c799799621878a9249c93e2b12cc799c1482", + "local_path": "vendor/agent64_cover17.py", + "note": "Vendored byte-exact (via PR 2933's hash-pinned vendor/, never imported), credit Aaron Wang (navinor), PR 2773. Used by the vendored cover18.py. Enforced by byte-pin checks.", + "pr": 2773, + "sha256": "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654", + "source_path": "research/f7-17point-cover-audit-seedcfa215c2/cover17.py" + }, + { + "head": "6739c799799621878a9249c93e2b12cc799c1482", + "local_path": "vendor/agent64_search17.py", + "note": "Vendored byte-exact, credit Aaron Wang (navinor), PR 2773: the Sidon/pair-sum budget enumeration engine used by anchors.py for both heavy census anchors. Enforced by byte-pin checks.", + "pr": 2773, + "sha256": "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674", + "source_path": "research/f7-17point-cover-audit-seedcfa215c2/search17.py" + }, + { + "head": "cfb813f883e61519deedcd84151dc0c68b9d19cc", + "local_path": "vendor/cover18.py", + "note": "Vendored byte-exact (via PR 2933's package), credit Aaron Wang (navinor), PR 2911: the exact-arithmetic KB3e engine (squeeze/deficit bookkeeping, profile system, rows). Reproduces the SQUEEZE table, the NOVANISH premise and the ROWS18 lines in verify.py quick/novanish/rows. Enforced by byte-pin checks.", + "pr": 2911, + "sha256": "24c6a2f4911dc2d5de76972eb5ae93dc4e66d8fa1e904443de6d0638e70c0a04", + "source_path": "research/f7-18point-cover-question-seed6d34356c/cover18.py" + }, + { + "head": "9f55f291e9e79e628fd98f1e4f4debfc1c2106e5", + "local_path": "anchors.py", + "note": "Vendored byte-exact (identical bytes in PR 2870's/2911's/2933's packages), credit Aaron Wang (navinor), PR 2870: the resumable heavy-anchor walk driver (per-sub-shard receipts, one progress section per mode). Re-run here from an empty receipt to recompute both anchors in full. Enforced by byte-pin checks.", + "pr": 2870, + "sha256": "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7", + "source_path": "research/f7-17point-fourier-obstruction-seedb5e318fe/anchors.py" + }, + { + "head": "25ea0e94250444db9ab05c3c8f1a66ba68e737b6", + "local_path": null, + "note": "Aaron Wang (navinor): the immediate predecessor. The L2 halving, L3 half-decomposition, L4 class floors, L5 grid and L7 Sidon pinning (open question 1: decide the tight classes; open question 3: a different identity for (11,7)/(9,9)) were read and reproduced byte-exactly, never re-derived as new results.", + "pr": 2933, + "source_path": "research/f7-18point-vanishing-seedfc618722/" + }, + { + "head": "cfb813f883e61519deedcd84151dc0c68b9d19cc", + "local_path": null, + "note": "Aaron Wang (navinor): the (A, D) reduction lemma, the squeeze/deficit bookkeeping, the row remainder 808/501/251/196 and the forced-vanishing premise; its engine is vendored byte-exact.", + "pr": 2911, + "source_path": "research/f7-18point-cover-question-seed6d34356c/" + }, + { + "head": "9f55f291e9e79e628fd98f1e4f4debfc1c2106e5", + "local_path": null, + "note": "Aaron Wang (navinor): the odd-coverage Fourier/Parseval identity (OBSTRUCTION 696/504/192) reproduced here.", + "pr": 2870, + "source_path": "research/f7-17point-fourier-obstruction-seedb5e318fe/" + }, + { + "head": "6739c799799621878a9249c93e2b12cc799c1482", + "local_path": null, + "note": "Aaron Wang (navinor): pair-representation rows and the census floors whose anchors (k10 budget-3, k11 levels 3-4) are re-walked here from empty receipts.", + "pr": 2773, + "source_path": "research/f7-17point-cover-audit-seedcfa215c2/" + }, + { + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "local_path": null, + "note": "Aaron Wang (navinor): the audited claim 'no 17-point set covers F2^7' and the length-18 exclusion.", + "pr": 2542, + "source_path": "research/universal-f7-singleton-seedb859517b/" + }, + { + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "local_path": null, + "note": "Aaron Wang (navinor): the recorded KB3b state (20-point covers exist; no 19-point cover in 200 restarts, max 124/128; search best 118/128 at k=18) that this package's results are compared against.", + "pr": 2634, + "source_path": "research/universal-f7-singleton-l20-seed06704c39/" + }, + { + "head": "88dda3534071442773106e9c0b941b9d39a3cea8", + "local_path": null, + "note": "Nicholas Stone (NicholasStone, Kimi agent): the completed (10,10) simple-20-cycle word census; recorded state, not re-run here.", + "pr": 2691, + "source_path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/" + }, + { + "local_path": null, + "note": "Ross Richardson (RossRichardson): the PR943 prefix-walk model and the P + P = F2^n covering condition.", + "pr": 943, + "source_path": "research/universal-connector-boundary/" + }, + { + "local_path": null, + "note": "Doug Colkitt (Mister-Meeseeks): the pinned f(5) = 12, f(6) = 16 record and frozen tier EXPECTED.json.", + "pr": 1185, + "source_path": "research/universal-connector-six-source/" + } + ], + "schema_version": 1 +} diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TASK-CARD.md b/research/f7-18point-tight-classes-seed4c1e7b30/TASK-CARD.md new file mode 100644 index 0000000000..c0ca06bcaa --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TASK-CARD.md @@ -0,0 +1,14 @@ +# Task card - KB3g: tight-class resolution and identity gap for the 18-point cover question for F2^7 + +- **Task ID / proposed scope key:** kappa-blocker KB3g (explicit open request from discussion 1166; drawn card was `independent-moment`/`formal-interface-lemma`, chooser seed `cfcf5afa7591a69ff98d5d3667dd47cd`, track independent-verification). Scope key of this refined object: `f7-18point-tight-classes`. +- **Base commit; exact predecessor and dependency heads:** base `d3add2cc28e958bedec197ab32b5526c5a222628` (origin/main at session start). Predecessor chain (all verified with `gh pr view NNN --json author,title` at writing time): PR 2542, PR 2634, PR 2773, PR 2870, PR 2911, PR 2933 by Aaron Wang (navinor); PR 2691 by Nicholas Stone (NicholasStone, concurrent L=20 WORD census, not taken). PR 2933 head `25ea0e94250444db9ab05c3c8f1a66ba68e737b6`, package `research/f7-18point-vanishing-seedfc618722` (extracted to scratch, not the tree). +- **Concrete object and question:** SET-level 18-point covers of `F2^7` (exact condition `P + P = F2^7`), split `(10,8)` tight classes `(7,1)`/`(8,2)` and split `(12,6)` A-vanish class `(6,0)` under the PR 2911 reduction `S = A u B`, `D = p + B`, `A + D = E = F2^6` and `(A+A) u (D+D) = E`. Question: are the L7-pinned Sidon equality configurations of these classes compatible with full coverage (they would give 18-point covers), or does each class contradict coverage (exclusion of the tightest survivors)? Secondary object: the `(11,7)/(9,9)` identity gap (row remainders 501/196), where PR 2933 L2 proves no character can vanish. +- **Scope status: changed.** Reason: authorized "explicit open request" scope change - assignment KB3g is the recorded remainder of PR 2933 (its open questions 1 and 3); the drawn chooser cards do not cover this object. Nicholas Stone's concurrent claim is the f(7) L=20/repeated-state WORD census (discussion 1166 comment 18954844): this card stays SET-level only. +- **Existing restriction being changed / claim being audited:** PR 2933's surviving tight classes - its exact decision step ("enumerate the forced Sidon pairs jointly with the odd-half multiplicities") is executed here. No predecessor claim is changed; the classes are decided or narrowed further. +- **Method; explicit parameter ranges/candidate alphabet:** exact integer enumeration only. (a) For `(10,8)` A-vanish `(7,1)`: `A0, A1` 5-sets in `H = ker(psi) = F2^5` with the 25 cross sums distinct, `D0` a 7-set in `H`, `D1` a singleton in `H'`, cross sumsets partitioning `H'` (32 elements); enumerate up to the proven symmetry `GL(5,2) x (translation of each half)` and test every L3 line. (b) For D-vanish `(8,2)`: Sidon pairs of 4-sets `D0, D1` with `|D0+D1| = 16`, `A` split `(8,2)` with `|A0+A1| = 16`, disjoint union `H'`; same tests. (c) For `(12,6)` A-vanish `(6,0)`: `A0, A1` 6-sets with `|A0+A1| = 32` = whole odd half (36 pairs, excess 4), `D` entirely in `H`; classify and contradict or construct. (d) One bounded pivot: an even-half/cross-sum multiplicity identity for `(11,7)/(9,9)`. Search only as falsifying-instance search, never as exclusion. +- **Nearest overlapping PRs and why this adds something:** PR 2933 (agent-74) classifies the vanishing classes and pins the tight ones to Sidon structure but does not decide them; PR 2911 records the row remainders and the forced-vanishing lemmas; this card executes the exact decision step PR 2933 named first in its open questions. No open PR claims the tight-class enumeration (entry and refined overlap passes clean; pair-collision check on discussions 1317/1166 clean). +- **Declared milestone:** local module - an exact class-by-class verdict with machine-checked enumeration and replay; no kappa, supplier or frontier change. +- **Optimistic full cost budget; required observable improvement:** compute cap about 3 hours wall on this host (enumerations are sharded/resumable); the observable outcome is a class-by-class PROVEN/DEAD/CHECKED verdict table, or a covering 18-set. +- **Unresolved consumer/restoration costs; family expansion decision:** none in scope - set level only; word-level L=22 consequences are recorded as implications, not claimed. +- **Success evidence; falsification test; time/compute cap:** success = each enumerated equality configuration either satisfies all four L3 coverage lines (a cover witness, cross-checked independently) or fails one with the exact failing line recorded; falsification control = the F2^5/F2^4 ground-truth censuses of PR 2933 must show no cover in a class this package proves dead. Receipts: heavy PR 2773 anchors re-walked from empty receipts first. +- **Predecessor authors; intended artifact and reproduction command:** Aaron Wang (navinor) for PR 2542/2634/2773/2870/2911/2933; Nicholas Stone (NicholasStone) for PR 2691. Artifact: `research/f7-18point-tight-classes-seed4c1e7b30/` with `python3 -I -B research/f7-18point-tight-classes-seed4c1e7b30/verify.py` replay modes. diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TASK.json b/research/f7-18point-tight-classes-seed4c1e7b30/TASK.json new file mode 100644 index 0000000000..e8ae230326 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TASK.json @@ -0,0 +1,111 @@ +{ + "actual_scope": "Kappa-blocker KB3g (explicit open request; set level, no words): resolve the TIGHT CLASSES of the 18-point cover question for F2^7 and break the identity gap for (11,7)/(9,9) - the recorded remainder of PR 2933 (its open questions 1 and 3), which decides the f(7) L=22 route. Delivered outcome=partial: the question is not decided, but its three tightest classes are PROVEN impossible and the identity gap is pressed to exact new conditions. (1) (10,8) A-vanish (7,1) (tight 32=32): PROVEN impossible two independent ways: (a) an exact Fourier/Parseval contradiction - L7 forces |A0+A1| = 25 with both 5-sets, so sum h_hat^2 = 175 is forced but the odd parity of both Walsh transforms forces sum h_hat^2 >= 135+135-31 = 239 > 175 (the m=4 analogue computes need = lower = 7 exactly, matching its 512 real covers); (b) the complete enumeration of normalized Sidon 5-pairs finds ZERO pairs (backtracking validated = full brute force 5040 = 5040 at m=4, m=5 slice cross-checks, hill-climb ceiling 23). Coverage in the class is independent of the free parameter d1 (proven; machine-checked). (2) (10,8) D-vanish (8,2) (tight 32=32): PROVEN impossible by complete enumeration of the L7-forced equality configurations: 4,287,920 normalized Sidon 4-pairs (D0,D1), 112,560 with 1-invariant complement C, all 28,815,360 (pair, A0t-choice) configurations fail ALL THREE translated coverage lines simultaneously (fail_hist {('I','II','III'): 28815360}); coverage independent of the free parameter w (proven). The reduction chain is validated end-to-end at m=4: the four L3 lines and a DIRECT S+S = F2^5 test agree on all 4,096 analogue configurations (512 covers accepted by both routes). (3) (12,6) A-vanish (6,0) (full odd half, 36 pairs excess 4): PROVEN impossible - complete transversal walk over all 169,911 normalized 6-sets D of F2^5 finds ZERO 6-sets X with X + D = F2^5 (branch-on-uncovered search; positive control recovers real transversals at m=3), so lines (I'')/(II'') are unsatisfiable. Plus an exact multiplicity classification (PROVEN): any full-sumset 6+6 pair would have excess-4 pattern rho = 2+2 or 1+1+1+1 on an affine 2-flat; the patterns 4*delta_p, 3+1, 2+1+1 are PROVEN dead by exact Walsh constraints. (4) (11,7)/(9,9) identity gap: one bounded pivot on the cross-sum multiplicity identity gives PROVEN necessary conditions sum rho^2 >= 17 (excess 13) resp. >= 19 (excess 17) - excluding the all-ones excess pattern on both splits and the (2,1^11) pattern at (11,7) - but no contradiction: DEMOTED as an exclusion mechanism (the excess is too large for the rigidity that killed (7,1)); the row remainders 501/196 stand. No 18-point cover constructed; the gap 20 <= f(7) <= 24 is unchanged.", + "ai_assistance": "Substantial AI assistance from opencode in scoping, implementation, verification and writing (no model named); no independent human review claimed.", + "author": "Aaron Wang", + "base_commit": "d3add2cc28e958bedec197ab32b5526c5a222628", + "bottleneck_link": "The set-level restricted addition basis value r((C2)^7) decides how small a universal word's prefix set can be inside the unchanged PR943 query model: 17-point covers are excluded (PR 2542/2773/2870) and the 18-point question is narrowed to four splits (PR 2911/2933). This package removes the three tightest surviving classes of (10,8)/(12,6) outright and converts the (11,7)/(9,9) identity gap into exact multiplicity conditions, feeding the word-level L=22 route its per-split feasibility. It changes no supplier, tariff or kappa and instantiates no physical interface.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18975496", + "de_diagnostic": "Not applicable: a finite set-level question in the PR943 query model, with no supplier width m, role count W, child ranks or recursive moment to price. The applicable diagnostic is exact reproduction against the pinned predecessor numbers plus exact-integer identities with exhaustive machine checks.", + "evidence": "CERTIFICATE.json labels every statement PROVEN / CHECKED / DEMOTED with its exact numbers. tight.py holds the exact-arithmetic engine (bitmask sumset primitives, the validated Sidon backtracking, the (7,1)/(8,2)/(6,0) class enumerators, the Fourier contradiction table, the rho multiplicity classification and the (11,7)/(9,9) identity). test_engine.py holds 13 tests: primitive vs naive sumsets, half-translation and free-parameter invariance, the end-to-end L3-vs-direct-S+S chain check at m=4 (4,096 configurations, 512 covers), the Fourier numbers (175/239 and the tight m=4 analogue 7=7), the identity soundness on every odd-odd-split cover of F2^4, the Walsh constraints of the rho classification (2+1+1 sizes never 11; 3+1 +-2 witness; 2+2 size 15; 2-flat size 7), the m=4 brute-force = backtracking equality (5040), the empty Sidon 5-pair enumeration, the no-3+3-full-pair F2^3 cross-check and the transversal-search positive control at m=3. verify.py replays six modes (quick / novanish / rows / classes / anchors) with markers PASS_TIGHT_{QUICK,NOVANISH,ROWS,CLASSES,ANCHORS}. Vendored byte pins: vendor/agent64_cover17.py 082bc838..., vendor/agent64_search17.py 9eb1bf79..., vendor/cover18.py 24c6a2f4..., vendor/vanish.py 6c605c54..., anchors.py 73d73a9b.... Both heavy PR 2773 census anchors were re-walked in full from empty receipts (PASS_ANCHORS_K10B3 count=149990400, PASS_ANCHORS_K11B4 count=0; ANCHOR-PROGRESS.json, ANCHOR-REPRO.json). The class walks are resumable with per-shard receipts (TIGHT-PROGRESS.json one section per mode; TIGHT-C60-*.json per shard). No kappa claim.", + "object_synonyms_used_in_overlap": [ + "18-point", + "18point", + "18-set", + "18 point set", + "tight class", + "Sidon", + "equality case", + "vanishing character", + "character vanish", + "P+P cover", + "P + P", + "F2^7", + "cross-sum multiplicity", + "odd half", + "even half", + "A0+A1", + "universal word", + "L=22", + "f(7)", + "cover", + "pair-sum" + ], + "open_questions": [ + { + "blocked_by": "Nothing structural; a bounded joint enumeration at two characters.", + "first_step": "Press L5's multi-vanishing grid (counts (x, y, y, x)) against the class floors at the product characters for (12,6) A-vanish (5,1) and (10,8) A-vanish (6,2).", + "question": "Do the surviving non-tight classes of (12,6) and (10,8) survive simultaneous vanishings at two characters?", + "why_it_matters": "Each excluded class removes a further slice of the (12,6)/(10,8) remainder; clearing both splits settles two of the four 18-point splits." + }, + { + "blocked_by": "No known coupling identity between odd-line cross-sum multiplicities and even-line self-sums.", + "first_step": "Combine the proven sum-rho^2 conditions with the even half (A+A) u (D+D) = E multiplicities (PR 2870 used only odd coverage) as a second layer on the 501/196 rows.", + "question": "What identity cuts the (11,7)/(9,9) row remainders, where no character can vanish and the cross-sum multiplicity identity does not contradict?", + "why_it_matters": "These two splits carry the other half of the 18-point question; the excess 13/17 is too large for the pointwise Walsh squeeze that killed (7,1)." + }, + { + "blocked_by": "Nothing structural; a failed bounded search is not an exclusion.", + "first_step": "Seeded search over the (11,7)/(9,9) row remainder profiles with the new multiplicity conditions as admissibility filters.", + "question": "Does any 18-point cover of F2^7 exist outside the decided classes?", + "why_it_matters": "A construction keeps the L = 22 route alive regardless of the exclusions; search best remains 118/128 at k=18." + } + ], + "original_card": { + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "id": "independent-moment", + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ], + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "starting_points": [ + "certificates/selected-result.json" + ] + }, + "outcome": "partial", + "pair_collision_check": { + "checked_utc": "2026-10-16T12:32Z (entry, before computation), 2026-10-16T12:35Z (refined re-run with the object's proper names and synonyms)", + "result": "No claim on the tight-class enumeration, the (6,0) class or the (11,7)/(9,9) identity gap at any check. Discussion 1317 is silent on this object (bit-mechanism word-model claims only). Discussion 1166's only 18-point posts in the checked window are the predecessor lineage (KB3c/KB3d/KB3e/KB3f, all released; KB3f = PR 2933 is this package's direct predecessor, released 2026-10-16 12:26Z). Nicholas Stone's claim (discussion 1166 comment 18954844) is the f(7) L=20/repeated-state WORD census - a different, word-level object - and was re-checked; this package stays strictly on the SET level.", + "threads_scanned": [ + "discussion 1317 full scan with grep CLAIM|Sidon|equality|vanish|18-point|18-set|F2|cover|L=22 incl. nested replies; nothing on this object", + "discussion 1166 with grep CLAIM|Sidon|equality case|vanishing|18-point|18-set|(7,1)|(8,2)|tight class|L=22 and again with the synonyms Sidon|equality case|6,720|tight|A0|A1|odd half|cross-sum|identity gap, since 2026-10-16T06:00Z incl. nested replies" + ], + "tool": "agent_tools.py disc-comments --grep (with nested replies) + scripts/find_overlap.py with explicit object terms and synonyms" + }, + "priced_budget_breakdown": "20 min entry orientation, pair-collision checks and the task card; 30 min predecessor extraction, attribution checks and the cheap anchor reproductions (OBSTRUCTION/SQUEEZE/NOVANISH/ROWS18/CLASSIFY lines); 45 min new machinery (Fourier identity, rho classification, class enumerators, 13 tests, end-to-end chain control); 90 min walk jobs (both heavy anchors re-walked from empty receipts, the 28.8M-configuration class82 decision and the 169,911-D class60 transversal walk, all resumable with receipts); 45 min package metadata, registration, gates and submission.", + "priced_budget_minutes": 230, + "priority_revision": 5, + "schema_version": 1, + "scope_change_reason": "Authorized 'explicit open request' scope change, recorded as instructed by the assignment. The chooser (OS seed cfcf5afa7591a69ff98d5d3667dd47cd, track independent-verification) drew the cards independent-moment / formal-interface-lemma (independent verification of the selected moment/enclosure and a formal interface lemma; neither targets the F2^7 cover question). The assignment (kappa-blocker KB3g) explicitly authorizes taking discussion 1166's open request instead - the recorded remainder of PR 2933 (its open questions 1 and 3): the tight classes of the 18-point cover question and the (11,7)/(9,9) identity gap. Pair-collision checks found no claim on this object; Nicholas Stone's active claim (discussion 1166 comment 18954844) is the f(7) L=20/repeated-state WORD census and this task stays strictly on the SET level.", + "scope_key": "c191650c0fa8d2fa514e (drawn card); refined object key f7-18point-tight-classes", + "scope_status": "changed", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "session_seed": "cfcf5afa7591a69ff98d5d3667dd47cd", + "smallest_falsifying_instance_first": "The falsifying instance for 'the tight classes are realizable' is one covering configuration in a tight class; each class was attacked at its smallest decidable instance first. (7,1): a single Sidon 5-pair would refute the identity - the m=4 analogue (512 real covers, need = lower = 7) validates the identity's tightness before the m=6 contradiction is used, and the empty enumeration is validated against m=4 brute force (5040 = 5040). (8,2): the smallest instance of the decision is one equality configuration; the reduction is validated end-to-end at m=4 against direct S+S tests before the 28.8M-configuration walk. (6,0): the smallest instance is one (A, D) full-sumset pair; the transversal search is validated positively at m=3 (recovers real transversals) before the 169,911-D walk, and the no-3+3-pair fact at m=3 is a recorded miniature. Before any new number the recorded anchors were reproduced (ANCHOR-REPRO.json): PR 2870 OBSTRUCTION 696/504/192, PR 2911 SQUEEZE/NOVANISH/ROWS18 808/501/251/196, PR 2933 CLASSIFY lines incl. the 32=32 TIGHT flags and L7 m=3 cases=6720, and both heavy PR 2773 anchors re-walked from empty receipts.", + "stop_rule": "Stop at the first of: (a) a covering configuration found in any tight class (an 18-point cover, assignment outcome (d)), (b) each of the three named classes decided (PROVEN impossible or realized) plus one bounded pivot on the (11,7)/(9,9) identity, or (c) the priced budget expiring with each class's exact obstruction recorded. Outcome (b) reached: all three classes PROVEN impossible; the identity pivot recorded with exact conditions (sum rho^2 >= 17/19) and honest non-contradiction; no second pivot taken.", + "task_id": "independent-moment", + "track": "independent-verification (drawn); scope changed to the assigned explicit open request kappa-blocker KB3g (the tight classes and identity gap of the 18-point cover question for F2^7, PR 2933 open questions 1 and 3)" +} diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-0.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-0.json new file mode 100644 index 0000000000..8513626af9 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-0.json @@ -0,0 +1,23 @@ +{ + "modes": { + "class60": { + "shards": { + "0": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 583.84, + "shard": 0, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 583.84, + "witnesses": [] + } + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-1.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-1.json new file mode 100644 index 0000000000..6a7a18a0e1 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-1.json @@ -0,0 +1,23 @@ +{ + "modes": { + "class60": { + "shards": { + "1": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 582.85, + "shard": 1, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 582.85, + "witnesses": [] + } + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-2.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-2.json new file mode 100644 index 0000000000..47b1e77ccd --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-2.json @@ -0,0 +1,23 @@ +{ + "modes": { + "class60": { + "shards": { + "2": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 586.18, + "shard": 2, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 586.18, + "witnesses": [] + } + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-3.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-3.json new file mode 100644 index 0000000000..0fa70714ba --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-3.json @@ -0,0 +1,23 @@ +{ + "modes": { + "class60": { + "shards": { + "3": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 582.08, + "shard": 3, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 582.08, + "witnesses": [] + } + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-4.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-4.json new file mode 100644 index 0000000000..c522f4dab7 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-4.json @@ -0,0 +1,23 @@ +{ + "modes": { + "class60": { + "shards": { + "4": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 586.74, + "shard": 4, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 586.74, + "witnesses": [] + } + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-5.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-5.json new file mode 100644 index 0000000000..aa92c8b440 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-5.json @@ -0,0 +1,23 @@ +{ + "modes": { + "class60": { + "shards": { + "5": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 583.23, + "shard": 5, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 583.23, + "witnesses": [] + } + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-6.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-6.json new file mode 100644 index 0000000000..106e13e940 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-6.json @@ -0,0 +1,23 @@ +{ + "modes": { + "class60": { + "shards": { + "6": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 585.38, + "shard": 6, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 585.38, + "witnesses": [] + } + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-7.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-7.json new file mode 100644 index 0000000000..c613f2a2d7 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-7.json @@ -0,0 +1,23 @@ +{ + "modes": { + "class60": { + "shards": { + "7": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21238, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 587.72, + "shard": 7, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 587.72, + "witnesses": [] + } + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-PROGRESS.json b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-PROGRESS.json new file mode 100644 index 0000000000..5f6f56b9cc --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-PROGRESS.json @@ -0,0 +1,309 @@ +{ + "modes": { + "class60": { + "complete": true, + "shards": { + "0": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 583.84, + "shard": 0, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 583.84, + "witnesses": [] + }, + "1": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 582.85, + "shard": 1, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 582.85, + "witnesses": [] + }, + "2": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 586.18, + "shard": 2, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 586.18, + "witnesses": [] + }, + "3": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 582.08, + "shard": 3, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 582.08, + "witnesses": [] + }, + "4": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 586.74, + "shard": 4, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 586.74, + "witnesses": [] + }, + "5": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 583.23, + "shard": 5, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 583.23, + "witnesses": [] + }, + "6": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21239, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 585.38, + "shard": 6, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 585.38, + "witnesses": [] + }, + "7": { + "budget_hit": false, + "complete": true, + "covering_triples": 0, + "d_checked": 21238, + "d_with_transversals": 0, + "normalized_d_total": 169911, + "seconds": 587.72, + "shard": 7, + "shards": 8, + "tested_triples": 0, + "transversals_total": 0, + "wall_seconds": 587.72, + "witnesses": [] + } + }, + "shards_count": 8, + "total": { + "covering_triples": 0, + "d_checked": 169911, + "d_with_transversals": 0, + "tested_triples": 0, + "transversals_total": 0, + "witnesses": [] + } + }, + "class71": { + "complete": true, + "shards": { + "0": { + "checked": 0, + "complete": true, + "covering_configs_normalized": 0, + "covering_pairs": 0, + "equality_configs_normalized": 0, + "fail_hist": {}, + "normalized_pairs": 0, + "seconds": 17.15, + "wall_seconds": 17.15, + "witnesses": [] + } + }, + "shards_count": 1, + "total": { + "checked": 0, + "covering_configs_normalized": 0, + "covering_pairs": 0, + "equality_configs_normalized": 0, + "normalized_pairs": 0, + "witnesses": [] + } + }, + "class82": { + "complete": true, + "shards": { + "0": { + "admissible_choice_sets": 4355072, + "checked": 4355072, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 4355072 + }, + "non_1_invariant_pairs": 518978, + "normalized_sidon_pairs": 535990, + "normalized_sidon_pairs_total": 4287920, + "seconds": 93.57, + "shard": 0, + "shards": 8, + "wall_seconds": 93.64, + "witnesses": [] + }, + "1": { + "admissible_choice_sets": 3901440, + "checked": 3901440, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 3901440 + }, + "non_1_invariant_pairs": 520750, + "normalized_sidon_pairs": 535990, + "normalized_sidon_pairs_total": 4287920, + "seconds": 66.54, + "shard": 1, + "shards": 8, + "wall_seconds": 66.6, + "witnesses": [] + }, + "2": { + "admissible_choice_sets": 2946048, + "checked": 2946048, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 2946048 + }, + "non_1_invariant_pairs": 524482, + "normalized_sidon_pairs": 535990, + "normalized_sidon_pairs_total": 4287920, + "seconds": 59.61, + "shard": 2, + "shards": 8, + "wall_seconds": 59.68, + "witnesses": [] + }, + "3": { + "admissible_choice_sets": 3179520, + "checked": 3179520, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 3179520 + }, + "non_1_invariant_pairs": 523570, + "normalized_sidon_pairs": 535990, + "normalized_sidon_pairs_total": 4287920, + "seconds": 61.52, + "shard": 3, + "shards": 8, + "wall_seconds": 61.58, + "witnesses": [] + }, + "4": { + "admissible_choice_sets": 4368384, + "checked": 4368384, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 4368384 + }, + "non_1_invariant_pairs": 518926, + "normalized_sidon_pairs": 535990, + "normalized_sidon_pairs_total": 4287920, + "seconds": 77.46, + "shard": 4, + "shards": 8, + "wall_seconds": 77.53, + "witnesses": [] + }, + "5": { + "admissible_choice_sets": 3892224, + "checked": 3892224, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 3892224 + }, + "non_1_invariant_pairs": 520786, + "normalized_sidon_pairs": 535990, + "normalized_sidon_pairs_total": 4287920, + "seconds": 94.64, + "shard": 5, + "shards": 8, + "wall_seconds": 94.71, + "witnesses": [] + }, + "6": { + "admissible_choice_sets": 2967552, + "checked": 2967552, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 2967552 + }, + "non_1_invariant_pairs": 524398, + "normalized_sidon_pairs": 535990, + "normalized_sidon_pairs_total": 4287920, + "seconds": 86.68, + "shard": 6, + "shards": 8, + "wall_seconds": 86.74, + "witnesses": [] + }, + "7": { + "admissible_choice_sets": 3205120, + "checked": 3205120, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 3205120 + }, + "non_1_invariant_pairs": 523470, + "normalized_sidon_pairs": 535990, + "normalized_sidon_pairs_total": 4287920, + "seconds": 95.68, + "shard": 7, + "shards": 8, + "wall_seconds": 95.76, + "witnesses": [] + } + }, + "shards_count": 8, + "total": { + "admissible_choice_sets": 28815360, + "checked": 28815360, + "covering_configs": 0, + "fail_hist": { + "('I', 'II', 'III')": 28815360 + }, + "non_1_invariant_pairs": 4175360, + "normalized_sidon_pairs": 4287920, + "witnesses": [] + } + } + } +} \ No newline at end of file diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/VERIFY.json b/research/f7-18point-tight-classes-seed4c1e7b30/VERIFY.json new file mode 100644 index 0000000000..e6e7d040fd --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/VERIFY.json @@ -0,0 +1,95 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-tight-classes-seed4c1e7b30/test_engine.py" + ], + "checks": "13 tests: bitmask sumset primitives vs naive; half-translation invariance of the four L3 lines and free-parameter invariance (d1 for (7,1), the derivation for (8,2)); the end-to-end chain check at m=4 (the four L3 lines vs a DIRECT S+S = F2^5 cover test on all 4,096 analogue configurations, 512 covers accepted by both routes); the exact Fourier numbers (need=175 lower=239 contradiction, and the tight m=4 analogue 7=7); the (11,7)/(9,9) identity numbers (sum rho^2 >= 17 resp. >= 19) and its positive soundness on every odd-odd-split cover of F2^4; the rho classification Walsh constraints (2+1+1 sizes never 11, a 3+1 +-2 obstruction witness, 2+2 gives |V22| = 15, the 2-flat gives 7, and the DEAD/SURVIVING sets); the Sidon backtracking = full brute force at m=4 (5040 = 5040); the empty Sidon 5-pair enumeration; the no-3+3-full-pair cross-check at m=3; and the transversal-search positive control at m=3 (recovers a real transversal).", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-tight-classes-seed4c1e7b30/verify.py", + "quick" + ], + "checks": "Vendored byte pins (vendor/agent64_cover17.py 082bc838..., vendor/agent64_search17.py 9eb1bf79..., vendor/cover18.py 24c6a2f4..., vendor/vanish.py 6c605c54..., anchors.py 73d73a9b...); the Fourier contradiction table (175/239 and the tight analogue 7=7); the rho classification; the empty (7,1) enumeration; the m=4 analogue controls (512 L7-structured covers; the (8,2) analogue empty); the complete PR 2933 class tables of all four splits with the (7,1)/(8,2) 32=32 TIGHT lines and the NO-VANISHING lines for (11,7)/(9,9); the L7 tight-equality census m=3 cases=6720; the F2^4 census 41,341; the PR 2870 OBSTRUCTION control (696/504/192); and the heavy-anchor receipt totals (k10b3 149,990,400, k11b4 0/0). Marker PASS_TIGHT_QUICK.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-tight-classes-seed4c1e7b30/verify.py", + "novanish" + ], + "checks": "The load-bearing PR 2911 NOVANISH premise recomputed from the byte-vendored PR 2911 engine: the no-vanishing profile system infeasible for (12,6) and (10,8) (every cover has a vanishing character off the all-ones hyperplane). Marker PASS_TIGHT_NOVANISH.", + "timeout_seconds": 60 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-tight-classes-seed4c1e7b30/verify.py", + "rows" + ], + "checks": "The PR 2911 ROWS18 reproduction (808/501/251/196 with the census floors) and the 17-point row controls ((11,6) remainder (5,1),(6,0); (10,7) empty after floor) from the byte-vendored PR 2911 engine. Marker PASS_TIGHT_ROWS.", + "timeout_seconds": 60 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-tight-classes-seed4c1e7b30/verify.py", + "classes" + ], + "checks": "The tight-class decision receipts: class71 (0 normalized Sidon 5-pairs, 0 covering), class82 (4,287,920 normalized Sidon 4-pairs, 4,175,360 non-1-invariant, 28,815,360 equality configurations checked, 0 covering, fail_hist all three lines), class60 (169,911 normalized D walked, 0 with transversals, 0 covering triples) and the (11,7)/(9,9) identity conditions. Receipt validation of TIGHT-PROGRESS.json / TIGHT-C60-*.json; delete them to re-walk. Marker PASS_TIGHT_CLASSES.", + "timeout_seconds": 60 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-tight-classes-seed4c1e7b30/verify.py", + "anchors" + ], + "checks": "The two heavy PR 2773 anchor receipts (k10b3 = 149,990,400 at excess exactly 3, k11b4 = 0/0; 62 sub-shards each) in ANCHOR-PROGRESS.json. Receipt validation of this package's own fresh empty-receipt walk (recorded with commands and markers in ANCHOR-REPRO.json); run vendor/../anchors.py from a scratch copy with a missing receipt to recompute. Marker PASS_TIGHT_ANCHORS.", + "timeout_seconds": 60 + } + ], + "inputs": [ + "research/f7-18point-tight-classes-seed4c1e7b30/tight.py", + "research/f7-18point-tight-classes-seed4c1e7b30/run_tight.py", + "research/f7-18point-tight-classes-seed4c1e7b30/test_engine.py", + "research/f7-18point-tight-classes-seed4c1e7b30/verify.py", + "research/f7-18point-tight-classes-seed4c1e7b30/anchors.py", + "research/f7-18point-tight-classes-seed4c1e7b30/ANCHOR-PROGRESS.json", + "research/f7-18point-tight-classes-seed4c1e7b30/ANCHOR-REPRO.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-PROGRESS.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-0.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-1.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-2.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-3.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-4.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-5.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-6.json", + "research/f7-18point-tight-classes-seed4c1e7b30/TIGHT-C60-7.json", + "research/f7-18point-tight-classes-seed4c1e7b30/vendor/agent64_cover17.py", + "research/f7-18point-tight-classes-seed4c1e7b30/vendor/agent64_search17.py", + "research/f7-18point-tight-classes-seed4c1e7b30/vendor/cover18.py", + "research/f7-18point-tight-classes-seed4c1e7b30/vendor/vanish.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/anchors.py b/research/f7-18point-tight-classes-seed4c1e7b30/anchors.py new file mode 100644 index 0000000000..d07fa31100 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/anchors.py @@ -0,0 +1,128 @@ +"""Resumable recomputation of the two heavy PR 2773 census anchors (KB3d). + +Established method (PR 2773, package research/f7-17point-cover-audit-seedcfa215c2, +Aaron Wang): raw-domain walk over the even group E = F2^6, complete +GL(6,2)-transitive domain through {0, 3}, sub-sharded by the smallest free +element (disjoint and complete), resumable with per-sub-shard receipts in +ANCHOR-PROGRESS.json. The enumeration itself is the vendored PR 2773 engine +(vendor/agent64_search17.py, byte-pinned; credit: Aaron Wang, PR 2773). + + anchors.py k10b3 [--seconds S] 10-sets through {0,3}, excess <= 3 + (recorded anchor: 149,990,400) + anchors.py k11b4 [--seconds S] 11-sets through {0,3}, excess <= 4 + (recorded anchor: level3 = level4 = 0) + +Each invocation processes sub-shards until the elapsed budget (default 540 s), +writes receipts after every sub-shard, and exits 0; re-invoke to continue. +A completed run prints PASS_ANCHORS_ with the exact totals and compares +them with the recorded anchor values. +""" + +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "vendor")) + +import agent64_search17 as s17 + +PROGRESS = HERE / "ANCHOR-PROGRESS.json" + +MODES = { + "k10b3": { + "k": 10, + "budget": 3, + "anchor_count": 149990400, + "description": "10-sets through {0,3}, pair-sum excess <= 3", + }, + "k11b4": { + "k": 11, + "budget": 4, + "anchor_count": 0, + "description": "11-sets through {0,3}, pair-sum excess <= 4", + }, +} + + +def load_progress(mode): + """Per-mode sections in one file (v1 kept one mode per file and lost the + other mode's receipts when switching; migrated on read).""" + data = {"modes": {}} + if PROGRESS.exists(): + old = json.loads(PROGRESS.read_text(encoding="utf-8")) + if "modes" in old: + data = old + elif "mode" in old: + data["modes"][old["mode"]] = { + k: v for k, v in old.items() if k != "mode" + } + return data["modes"].setdefault(mode, {"shards": {}}) + + +def save_progress(mode, prog): + data = {"modes": {}} + if PROGRESS.exists(): + old = json.loads(PROGRESS.read_text(encoding="utf-8")) + if "modes" in old: + data = old + elif "mode" in old: + data["modes"][old["mode"]] = { + k: v for k, v in old.items() if k != "mode" + } + data["modes"][mode] = prog + PROGRESS.write_text(json.dumps(data, indent=2, sort_keys=True), encoding="utf-8") + + +def main(): + mode = sys.argv[1] if len(sys.argv) > 1 else "" + if mode not in MODES: + raise SystemExit("usage: anchors.py k10b3|k11b4 [--seconds S]") + budget_seconds = 540.0 + if "--seconds" in sys.argv: + budget_seconds = float(sys.argv[sys.argv.index("--seconds") + 1]) + spec = MODES[mode] + prog = load_progress(mode) + prog["spec"] = {k: v for k, v in spec.items()} + t_start = time.time() + for v0 in sorted(s17.EVEN): + if v0 in (0, 3): + continue + key = f"v0={v0}" + if key in prog["shards"]: + continue + t1 = time.time() + hist, examples = s17.hist_sets( + s17.EVEN, spec["k"], spec["budget"], fixed=(0, 3, v0), floor=v0 + ) + prog["shards"][key] = { + "hist": {str(e): n for e, n in sorted(hist.items())}, + "examples": examples, + "seconds": round(time.time() - t1, 2), + } + save_progress(mode, prog) + print( + f"ANCHOR {mode} {key} hist={prog['shards'][key]['hist']}" + f" seconds={prog['shards'][key]['seconds']}" + f" done={len(prog['shards'])}/62", + flush=True, + ) + if time.time() - t_start > budget_seconds: + print(f"RECEIPT {mode} checkpoint shards={len(prog['shards'])}/62", flush=True) + return + total = {} + for rec in prog["shards"].values(): + for e, n in rec["hist"].items(): + total[e] = total.get(e, 0) + n + count = sum(total.values()) + prog["total_hist"] = {str(e): n for e, n in sorted(total.items())} + prog["complete"] = True + save_progress(mode, prog) + assert count == spec["anchor_count"], (mode, count, spec["anchor_count"]) + print(f"PASS_ANCHORS_{mode.upper()} count={count} total_hist={prog['total_hist']} shards=62", flush=True) + + +if __name__ == "__main__": + sys.stdout.reconfigure(encoding="utf-8") + main() diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/run_tight.py b/research/f7-18point-tight-classes-seed4c1e7b30/run_tight.py new file mode 100644 index 0000000000..edddb4b733 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/run_tight.py @@ -0,0 +1,199 @@ +"""Resumable receipt runner for the KB3g tight-class enumerations. + +Modes (deterministic sharding; receipts per shard in TIGHT-PROGRESS.json, +one section per mode): + + class71 the (10,8) A-vanish tight class (7,1): Sidon 5-pair enumeration + plus the three translated coverage lines. Also re-derives the + exact Fourier contradiction (identity, no walk). + class82 the (10,8) D-vanish tight class (8,2): every normalized Sidon + 4-pair, every admissible A0t choice, the three coverage lines. + class60 the (12,6) A-vanish class (6,0): full-sumset 6-pairs and the + D-side hitting search with the three coverage lines. + control m=4 brute-force analogue classes (soundness/completeness of the + L7 reduction) and the Fourier identity table. + +Usage: python3 -I -B run_tight.py [--shards N] [--shard k] [--budget S] + +A shard is processed only if its receipt is absent; re-invoke to continue. +The receipt file must not exist beforehand for a walk claimed as +recomputation (receipt-validation trap); delete receipts or run in a fresh +copy to prove recomputation. +""" + +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +import tight # noqa: E402 + +PROGRESS = HERE / "TIGHT-PROGRESS.json" +MODES = ("class71", "class82", "class60", "control") + + +def progress_path(): + import sys as _sys + + if "--progress" in _sys.argv: + return Path(_sys.argv[_sys.argv.index("--progress") + 1]) + return PROGRESS + + +def load_progress(mode): + data = {"modes": {}} + p = progress_path() + if p.exists(): + old = json.loads(p.read_text(encoding="utf-8")) + if "modes" in old: + data = old + return data["modes"].setdefault(mode, {"shards": {}}) + + +def save_progress(mode, prog): + data = {"modes": {}} + p = progress_path() + if p.exists(): + old = json.loads(p.read_text(encoding="utf-8")) + if "modes" in old: + data = old + data["modes"][mode] = prog + p.write_text(json.dumps(data, indent=2, sort_keys=True), encoding="utf-8") + + +def aggregate(prog): + keys = [ + "normalized_pairs", + "equality_configs_normalized", + "covering_pairs", + "covering_configs_normalized", + "normalized_sidon_pairs", + "non_1_invariant_pairs", + "admissible_choice_sets", + "checked", + "covering_configs", + "tested_triples", + "pairs_with_hit_sets", + "covering_triples", + "d_checked", + "d_with_transversals", + "transversals_total", + ] + out = {} + for k in keys: + tot = 0 + seen = False + for rec in prog["shards"].values(): + if k in rec: + tot += rec[k] + seen = True + if seen: + out[k] = tot + hist = {} + for rec in prog["shards"].values(): + for k, v in rec.get("fail_hist", {}).items(): + hist[k] = hist.get(k, 0) + v + if hist: + out["fail_hist"] = {k: hist[k] for k in sorted(hist)} + wits = [] + for rec in prog["shards"].values(): + wits.extend(rec.get("witnesses", [])) + out["witnesses"] = wits[:5] + return out + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + args = sys.argv[1:] + mode = args[0] if args else "" + if mode == "merge60": + # merge per-shard class60 receipts (TIGHT-C60-.json) into the + # canonical TIGHT-PROGRESS.json section + prog = {"shards": {}} + for k in range(8): + p = HERE / ("TIGHT-C60-%d.json" % k) + rec = json.loads(p.read_text(encoding="utf-8"))["modes"]["class60"] + shard_rec = rec["shards"][str(k)] + assert shard_rec.get("complete"), (k, shard_rec.get("budget_hit")) + prog["shards"][str(k)] = shard_rec + prog["complete"] = True + prog["shards_count"] = 8 + prog["total"] = aggregate(prog) + save_progress("class60", prog) + print("PASS_TIGHT_CLASS60 %s" % json.dumps(prog["total"], sort_keys=True), flush=True) + return + if mode not in MODES: + raise SystemExit("usage: run_tight.py %s [--shards N] [--shard k]" % "|".join(MODES)) + shards = int(args[args.index("--shards") + 1]) if "--shards" in args else 8 + budget = float(args[args.index("--budget") + 1]) if "--budget" in args else 520.0 + + if mode == "control": + t0 = time.time() + rec = tight.control_m4_bruteforce() + fid = tight.fourier_71_identity() + print("CONTROL m4_class71_analogue %s" % json.dumps(rec["m4_class71_analogue"], sort_keys=True), flush=True) + print("CONTROL m4_class82_analogue %s" % json.dumps(rec["m4_class82_analogue"], sort_keys=True), flush=True) + for tag in sorted(fid): + print("FOURIER %s %s" % (tag, json.dumps(fid[tag], sort_keys=True)), flush=True) + assert rec["m4_class71_analogue"]["all_have_l7_structure"] in (True, None) + assert rec["m4_class82_analogue"]["all_have_l7_structure"] in (True, None) + assert fid["m5_k5"]["contradiction"] is True + assert fid["m3_analogue_71"]["contradiction"] is False + print("PASS_TIGHT_CONTROL seconds=%.1f" % (time.time() - t0), flush=True) + return + + prog = load_progress(mode) + if mode == "class71": + todo = [0] + elif "--shard" in args: + todo = [int(args[args.index("--shard") + 1])] + else: + todo = [ + k + for k in range(shards) + if not prog["shards"].get(str(k), {}).get("complete") + ] + if not prog["shards"]: + print("RUN_TIGHT %s fresh receipts confirmed" % mode, flush=True) + print("RUN_TIGHT %s shards=%d todo=%s" % (mode, shards, todo), flush=True) + for shard in todo: + t0 = time.time() + if mode == "class71": + rec = tight.class71_run(budget=budget) + elif mode == "class82": + rec = tight.class82_run(budget=budget, shard=shard, shards=shards) + else: + rec = tight.class60_run(budget=budget, shard=shard, shards=shards) + rec["wall_seconds"] = round(time.time() - t0, 2) + rec["complete"] = not rec.get("budget_hit", False) + prog["shards"][str(shard)] = rec + save_progress(mode, prog) + print( + "RECEIPT %s shard=%d/%d wall=%.1fs %s" + % (mode, shard, shards, rec["wall_seconds"], json.dumps(aggregate(prog), sort_keys=True)[:400]), + flush=True, + ) + done = [ + k + for k in range(shards) + if prog["shards"].get(str(k), {}).get("complete") + ] + if mode == "class71" or len(done) == shards: + prog["complete"] = True + prog["shards_count"] = len(prog["shards"]) + prog["total"] = aggregate(prog) + save_progress(mode, prog) + print("PASS_TIGHT_%s %s" % (mode.upper(), json.dumps(prog["total"], sort_keys=True)), flush=True) + else: + print( + "RECEIPT_TIGHT_%s partial complete=%d/%d (re-invoke to continue)" + % (mode, len(done), shards), + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/test_engine.py b/research/f7-18point-tight-classes-seed4c1e7b30/test_engine.py new file mode 100644 index 0000000000..b59abc5eec --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/test_engine.py @@ -0,0 +1,450 @@ +"""Unit and control tests for the KB3g tight-class engine. + +All exact integer arithmetic. Run: + python3 -I -B research/f7-18point-tight-classes-seed4c1e7b30/test_engine.py +""" + +import random +import sys +import unittest +from itertools import combinations + +HERE = __file__.rsplit("\\", 1)[0].rsplit("/", 1)[0] +sys.path.insert(0, HERE) + +import tight # noqa: E402 + + +def naive_sumset(X, Y): + return {x ^ y for x in X for y in Y} + + +class TestPrimitives(unittest.TestCase): + def test_trans_and_sumset_vs_naive(self): + rng = random.Random(1) + for _ in range(300): + X = rng.sample(range(32), rng.randrange(0, 9)) + Y = rng.sample(range(32), rng.randrange(0, 9)) + a = rng.randrange(32) + self.assertEqual( + tight.trans(tight.mask_of(X), a), + tight.mask_of([x ^ a for x in X]), + ) + self.assertEqual( + tight.sumset_mask(tight.mask_of(X), tight.mask_of(Y)), + tight.mask_of(naive_sumset(X, Y)), + ) + + def test_delta_mask(self): + X = [0, 1, 3] + self.assertEqual(tight.delta_mask(tight.mask_of(X)), tight.mask_of([1, 3, 2])) + + +class TestL7Reduction(unittest.TestCase): + def test_m4_class71_analogue_direct_agreement(self): + """End-to-end chain check: the four L3 lines vs a DIRECT S+S = F2^5 + cover test on every (7,1)-analogue configuration at m=4 (positive + direction: 512 real covers are accepted by both routes).""" + H = [x for x in range(16) if not (x & 1)] + Hp = [x for x in range(16) if x & 1] + + def ss(X, Y): + return {x ^ y for x in X for y in Y} + + def se(X): + return {x ^ y for x in X for y in X} + + def l3(a0, a1, d0, d1): + return ( + ss(a0, d0) | ss(a1, d1) == set(H) + and ss(a0, d1) | ss(a1, d0) == set(Hp) + and se(a0) | se(a1) | se(d0) | se(d1) == set(H) + and ss(a0, a1) | ss(d0, d1) == set(Hp) + ) + + def direct(a0, a1, d0, d1): + # E = F2^4 = even coset of F2^5 via parity extension; H = bit-4 + # half of the F2^4 coords; odd coset point p = 1 in F2^5. + def phi(w): + return w | ((w.bit_count() & 1) << 4) + + A = {phi(a) for a in a0} | {phi(a) for a in a1} + B = {1 ^ phi(d) for d in d0} | {1 ^ phi(d) for d in d1} + S = A | B + cov = naive_sumset(S, S) + return len(cov) == 32 + + agree = 0 + covers = 0 + for a0t in combinations(H, 7): + a0 = list(a0t) + for a1 in Hp: + for d0 in H: + for d1 in Hp: + v_l3 = l3(a0, [a1], [d0], [d1]) + v_dir = direct(a0, [a1], [d0], [d1]) + self.assertEqual(v_l3, v_dir, (a0, a1, d0, d1)) + agree += 1 + if v_l3: + covers += 1 + self.assertEqual(agree, 4096) + self.assertEqual(covers, 512) + + def test_half_translation_invariance(self): + """Random m=5 configurations: half-translations preserve the four + L3 lines, and the translated class formulas are invariant in the + free parameter (d1 for (7,1), w for (8,2)).""" + rng = random.Random(42) + + def l3_masks(a0m, a1m, d0m, d1m): + H = set(range(32)) + ok_i = (tight.sumset_mask(a0m, d0m) | tight.sumset_mask(a1m, d1m)) == tight.ALL + ok_ii = (tight.sumset_mask(a0m, d1m) | tight.sumset_mask(a1m, d0m)) == tight.ALL + ok_iii = ( + tight.selfsum_mask(a0m) + | tight.selfsum_mask(a1m) + | tight.selfsum_mask(d0m) + | tight.selfsum_mask(d1m) + ) == tight.ALL + ok_iv = (tight.sumset_mask(a0m, a1m) | tight.sumset_mask(d0m, d1m)) == tight.ALL + return ok_i and ok_ii and ok_iii and ok_iv + + for _ in range(200): + a0m = tight.mask_of(rng.sample(range(32), 5)) + a1m = tight.mask_of(rng.sample(range(32), 5)) + d0m = tight.mask_of(rng.sample(range(32), 7)) + d1m = tight.mask_of(rng.sample(range(32), 1)) + h = rng.randrange(32) + hp = rng.randrange(32) + v0 = l3_masks(a0m, a1m, d0m, d1m) + v1 = l3_masks( + tight.trans(a0m, h), + tight.trans(a1m, hp), + tight.trans(d0m, h), + tight.trans(d1m, hp), + ) + self.assertEqual(v0, v1) + + def test_class71_free_parameter_invariance(self): + rng = random.Random(7) + for _ in range(100): + a0m = tight.mask_of(rng.sample(range(32), 5)) + a1m = tight.mask_of(rng.sample(range(32), 5)) + sums = tight.sumset_mask(a0m, a1m) + tm = tight.ALL ^ sums + d1 = rng.randrange(32) + d0m = tight.trans(tm, d1) + d1m = 1 << d1 + ok_direct = l3_any(a0m, a1m, d0m, d1m) + ok_formula = ( + (tight.sumset_mask(a0m, tm) | a1m) == tight.ALL + and (tight.sumset_mask(a1m, tm) | a0m) == tight.ALL + and (tight.selfsum_mask(a0m) | tight.selfsum_mask(a1m) | tight.selfsum_mask(tm)) + == tight.ALL + ) + self.assertEqual(ok_direct, ok_formula) + + +def l3_any(a0m, a1m, d0m, d1m): + ok_i = (tight.sumset_mask(a0m, d0m) | tight.sumset_mask(a1m, d1m)) == tight.ALL + ok_ii = (tight.sumset_mask(a0m, d1m) | tight.sumset_mask(a1m, d0m)) == tight.ALL + ok_iii = ( + tight.selfsum_mask(a0m) + | tight.selfsum_mask(a1m) + | tight.selfsum_mask(d0m) + | tight.selfsum_mask(d1m) + ) == tight.ALL + ok_iv = (tight.sumset_mask(a0m, a1m) | tight.sumset_mask(d0m, d1m)) == tight.ALL + return ok_i and ok_ii and ok_iii and ok_iv + + +class TestFourier(unittest.TestCase): + def test_71_contradiction_numbers(self): + fid = tight.fourier_71_identity() + self.assertTrue(fid["m5_k5"]["contradiction"]) + self.assertEqual(fid["m5_k5"]["need"], 175) + self.assertEqual(fid["m5_k5"]["lower_bound"], 239) + self.assertFalse(fid["m3_k2"]["contradiction"]) + self.assertFalse(fid["m3_analogue_71"]["contradiction"]) + self.assertEqual(fid["m3_analogue_71"]["need"], 7) + self.assertEqual(fid["m3_analogue_71"]["lower_bound"], 7) + + def test_identity_odd_sides_numbers(self): + r117 = tight.identity_odd_sides(11, 7) + self.assertEqual(r117["excess"], 13) + self.assertEqual(r117["sum_rho2_min"], 17) + self.assertFalse(r117["contradiction"]) + r99 = tight.identity_odd_sides(9, 9) + self.assertEqual(r99["excess"], 17) + self.assertEqual(r99["sum_rho2_min"], 19) + self.assertFalse(r99["contradiction"]) + + def test_identity_soundness_on_f24_covers(self): + """Every odd-odd-split cover of F2^4 satisfies the sum-rho^2 bound + (positive validation of the identity on real covers).""" + N = 16 + full = set(range(N)) + checked = 0 + for mask in range(1, 1 << N): + S = [x for x in range(N) if (mask >> x) & 1] + cov = {0} + for i in range(len(S)): + for j in range(i): + cov.add(S[i] ^ S[j]) + if cov != full: + continue + A = [x for x in S if x.bit_count() % 2 == 0] + B = [x for x in S if x.bit_count() % 2 == 1] + D = [1 ^ b for b in B] + s, t = len(A), len(D) + if s % 2 == 0 or t % 2 == 0: + continue + from collections import Counter + + def ecoord(x): + # x in the even coset of F2^4: x = (w, parity(w)), w in F2^3 + return x >> 1 + + cnt = Counter() + for a in A: + for d in D: + cnt[ecoord(a) ^ ecoord(d)] += 1 + excess = s * t - 8 + rho2 = sum((v - 1) ** 2 for v in cnt.values()) + self.assertEqual(sum(v - 1 for v in cnt.values()), excess) + rec = tight.identity_odd_sides(s, t, m=3) + self.assertGreaterEqual(rho2, rec["sum_rho2_min"], (S, rho2, rec)) + checked += 1 + self.assertGreater(checked, 0) + + +class TestRhoClassification(unittest.TestCase): + def test_walsh_constraints(self): + rng = random.Random(3) + + def rho_hat(rho_map, v): + return sum(c * (1 - 2 * ((s & v).bit_count() & 1)) for s, c in rho_map) + + # 2+1+1: V22 sizes are 2^{5-r}-1, never 11 + seen = set() + for _ in range(300): + q = rng.randrange(32) + p1 = rng.randrange(32) + p2 = rng.randrange(32) + if len({q, p1, p2}) != 3: + continue + rho_map = [(q, 2), (p1, 1), (p2, 1)] + v22 = [ + v + for v in range(1, 32) + if abs(rho_hat(rho_map, v)) == 4 + ] + seen.add(len(v22)) + self.assertTrue(seen <= {1, 3, 7, 15, 31}, seen) + + # 3+1: rho_hat attains +-2 for p != q (obstruction witness) + witness = False + for _ in range(200): + q = rng.randrange(32) + p = rng.randrange(32) + if p == q: + continue + rho_map = [(q, 3), (p, 1)] + vals = {abs(rho_hat(rho_map, v)) for v in range(1, 32)} + if 2 in vals: + witness = True + break + self.assertTrue(witness) + + # 2+2: |V22| = 15 + q1, q2 = 3, 5 + rho_map = [(q1, 2), (q2, 2)] + v22 = [v for v in range(1, 32) if abs(rho_hat(rho_map, v)) == 4] + self.assertEqual(len(v22), 15) + + # 1+1+1+1 on a rank-3 affine 2-flat: |V22| = 7 + p1, p2, p3 = 1, 2, 4 + flat = [p1, p2, p3, p1 ^ p2 ^ p3] + rho_map = [(x, 1) for x in flat] + v22 = [v for v in range(1, 32) if abs(rho_hat(rho_map, v)) == 4] + self.assertEqual(len(v22), 7) + + # 4 delta_p: Parseval contradiction numbers + cls = tight.rho_classification() + dead = {t["rho"] for t in cls["types"] if t["verdict"] == "DEAD"} + self.assertEqual(dead, {"4*delta_p", "3+1", "2+1+1"}) + self.assertEqual(set(cls["surviving"]), {"2+2", "1+1+1+1"}) + + +class TestSearchEnumeration(unittest.TestCase): + def test_sidon_backtracking_m4_matches_bruteforce(self): + ALL16 = (1 << 16) - 1 + + def trans16(mask, a): + for i in range(4): + if (a >> i) & 1: + b = 1 << i + lo = 0 + for p in range(16): + if not (p & b): + lo |= 1 << p + hi = ALL16 ^ lo + mask = ((mask & lo) << b) | ((mask & hi) >> b) + return mask + + def sumset16(mx, my): + out = 0 + x = mx + while x: + lsb = x & -x + out |= trans16(my, lsb.bit_length() - 1) + x ^= lsb + return out + + def delta16(mx): + return sumset16(mx, mx) & ALL16 & ~1 + + def mask_of(pts): + m = 0 + for p in pts: + m |= 1 << p + return m + + bf = 0 + for c0 in combinations(range(1, 16), 2): + x = mask_of((0,) + c0) + for c1 in combinations(range(1, 16), 2): + y = mask_of((0,) + c1) + if sumset16(x, y).bit_count() == 9: + bf += 1 + bt = 0 + for c1 in combinations(range(1, 16), 2): + a1m = 1 | mask_of(c1) + forb = delta16(a1m) + cand = [v for v in range(1, 16) if not (forb >> v) & 1] + chosen = [0, 0, 0] + + def rec(depth, start): + nonlocal bt + if depth == 3: + bt += 1 + return + for i in range(start, len(cand)): + v = cand[i] + if v <= chosen[depth - 1]: + continue + ok = True + for j in range(1, depth): + if (forb >> (v ^ chosen[j])) & 1: + ok = False + break + if ok: + chosen[depth] = v + rec(depth + 1, i + 1) + + rec(1, 0) + self.assertEqual(bf, 5040) + self.assertEqual(bt, bf) + + def test_class71_pairs_empty(self): + pairs = tight.class71_pairs() + self.assertEqual(len(pairs), 0) + + def test_transversals6_positive_control_m3(self): + """The walk machinery must FIND transversals when they exist: at m=3, + pairs X (4-set), D (2-set) with X + D = F2^3 exist; the same + branch-on-uncovered transversal search over the D-family recovers + them (adapted small-dimension copy).""" + N = 8 + found_pairs = [] + for xc in combinations(range(N), 4): + xm = tight_mask(xc) + for dc in combinations(range(N), 2): + dmm = tight_mask(dc) + if tight_sumset3(xm, dmm) == (1 << N) - 1: + found_pairs.append((xc, dc)) + self.assertGreater(len(found_pairs), 0) + # transversal search (same branch-on-uncovered logic) on one such D + xc, dc = found_pairs[0] + dmm = tight_mask(dc) + cov_by = [0] * N + for v in range(N): + m = 0 + for x in range(N): + if (dmm >> (x ^ v)) & 1: + m |= 1 << x + cov_by[v] = m + out = set() + cur = [] + + def rec(uncov, vlo): + if len(cur) == 4: + if not uncov: + out.add(frozenset(cur)) + return + if uncov.bit_count() > 2 * (4 - len(cur)): + return + if not uncov: + for v in range(vlo, N): + if v in cur: + continue + cur.append(v) + rec(uncov, v + 1) + cur.pop() + return + i = (uncov & -uncov).bit_length() - 1 + target = 0 + for x in range(N): + if (dmm >> (x ^ i)) & 1: + target |= 1 << x + for v in range(N): + if not (target >> v) & 1: + continue + if v in cur: + continue + cur.append(v) + rec(uncov & ~cov_by[v], 0) + cur.pop() + + rec((1 << N) - 1, 0) + self.assertIn(frozenset(xc), out) + + def test_no_full_sumset_33_pair_f2_3(self): + """Cross-check of the (6,0) phenomenon in miniature: no pair of + 3-sets X, D in F2^3 has X + D = F2^3 (all 3136 pairs scanned).""" + N = 8 + full = (1 << N) - 1 + cnt = 0 + for xc in combinations(range(N), 3): + xm = tight_mask(xc) + for dc in combinations(range(N), 3): + if tight_sumset3(xm, tight_mask(dc)) == full: + cnt += 1 + self.assertEqual(cnt, 0) + + +def tight_mask(pts): + m = 0 + for p in pts: + m |= 1 << p + return m + + +def tight_sumset3(mx, my): + out = 0 + x = mx + while x: + lsb = x & -x + a = lsb.bit_length() - 1 + y = my + while y: + lsb2 = y & -y + out |= 1 << (a ^ (lsb2.bit_length() - 1)) + y ^= lsb2 + x ^= lsb + return out + + +if __name__ == "__main__": + sys.stdout.reconfigure(encoding="utf-8") + unittest.main(verbosity=2) diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/tight.py b/research/f7-18point-tight-classes-seed4c1e7b30/tight.py new file mode 100644 index 0000000000..2e0e151ccf --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/tight.py @@ -0,0 +1,760 @@ +"""KB3g engine: tight-class resolution for the 18-point cover question for +F2^7 (set level; no words). Exact Python integer arithmetic only. + +Object (unchanged from PR 2911/2933): S = A u B covers F2^7 iff P + P = F2^7. +With D = p + B inside E = F2^6 (PR 2911 reduction, PROVEN there) the pair +(A, D) covers iff (i) A + D = E and (ii) (A+A) u (D+D) = E. + +This module decides the two PR 2933 TIGHT classes of the (10,8) split and +the full-sumset class (6,0) of (12,6) by exact enumeration of the L7-forced +Sidon equality configurations. All arithmetic is integers; masks are Python +ints. + +Halves. Fix the character psi = bit 0 (WLOG under GL(6,2)). H = ker(psi) +and the coset H' are both identified with F2^5 = {0..31}; every cross sum is +the XOR of the two F2^5 coordinates (the coset offset cancels in pairs, and +H'-valued sums are read in H' coordinates). A = A0 u A1 with A0 in H, A1 in +H'; D = D0 u D1 likewise. Coverage is equivalent to the four L3 lines +(PR 2933, PROVEN): + + (i) (A0+D0) u (A1+D1) = H + (ii) (A0+D1) u (A1+D0) = H' + (iii) (A0+A0) u (A1+A1) u (D0+D0) u (D1+D1) = H + (iv) (A0+A1) u (D0+D1) = H' + +Half-translations (h on (A0,D0), h' on (A1,D1)) and a common GL(5,2) map M +preserve all four lines (each H'-valued sumset translates by h + h', which +preserves its being all of H'). Hence WLOG 0 in A0, 0 in A1. + +L7 (PR 2933, PROVEN; general pigeonhole valid at m = 6): at F1 equality +a0*a1 + d0*d1 = 32 with (iv) holding, |A0+A1| = a0*a1, |D0+D1| = d0*d1 (both +Sidon: all cross sums distinct) and the two cross sumsets are disjoint with +union H'. + +Class (10,8) A-vanish (7,1): A0, A1 5-sets with |A0+A1| = 25; D0 a 7-set, +D1 a singleton {d1}. (iv) forces D0 + d1 = T := H' \\ (A0+A1) (7 points). +Substituting D0 = T + d1 into (i)-(iii) and translating by d1 shows coverage +is INDEPENDENT of d1: + (I) (A0+T) u A1 = F2^5 + (II) (A1+T) u A0 = F2^5 + (III) (A0+A0) u (A1+A1) u (T+T) = F2^5 +and (iv) holds by construction. Each covering (A0, A1) yields 32 covering +configurations (one per d1) in the normalized chart. + +Class (10,8) D-vanish (8,2): D0, D1 4-sets with |D0+D1| = 16; A splits +(8,2): A0 an 8-set, A1 = {w, w+delta}, delta != 0. |A0+A1| = 16 iff +A0 u (A0+delta) = 16 points iff A0 n (A0+delta) = 0. Normalize instead on +the D side: 0 in D0, 0 in D1 (the class forces both nonempty), and WLOG +delta = 1 under GL(5,2). With T = D0+D1 (16 points) and C = H' \\ T, +(iv) forces A0 + w to choose one element of each pair {x, x+1} inside C, so +C must be 1-invariant; the choice is one of at most 2^8 sets A0t = A0 + w. +Coverage is then independent of w: + (I') (A0t+D0) u (D1+{0,1}) = F2^5 + (II') (A0t+D1) u (D0+{0,1}) = F2^5 + (III') (A0t+A0t) u {0,1} u (D0+D0) u (D1+D1) = F2^5 + +Class (12,6) A-vanish (6,0): A0, A1 6-sets with A0+A1 = H' (36 pairs, excess +exactly 4), D = D0 a 6-set in H, D1 empty. Lines reduce to + (I'') A0+D = F2^5, (II'') A1+D = F2^5, + (III'') (A0+A0) u (A1+A1) u (D+D) = F2^5. +Normalize 0 in A0, 0 in A1. +""" + +import json +import sys +import time +from itertools import combinations +from pathlib import Path + +ALL = (1 << 32) - 1 +N5 = 32 + + +# ------------------------------------------------------- mask primitives + + +def elems(mask): + out = [] + while mask: + lsb = mask & -mask + out.append(lsb.bit_length() - 1) + mask ^= lsb + return out + + +def mask_of(pts): + m = 0 + for p in pts: + m |= 1 << p + return m + + +# Precomputed per-bit XOR-translation block masks (5 bits, F2^5). +_BIT_LO = [] +_BIT_HI = [] +for _i in range(5): + _b = 1 << _i + _lo = 0 + for _p in range(N5): + if not (_p & _b): + _lo |= 1 << _p + _BIT_LO.append(_lo) + _BIT_HI.append(ALL ^ _lo) + + +def trans(mask, a): + """{x ^ a : x in mask} as a bitmask.""" + for i in range(5): + if (a >> i) & 1: + b = 1 << i + mask = ((mask & _BIT_LO[i]) << b) | ((mask & _BIT_HI[i]) >> b) + return mask + + +def sumset_mask(mx, my): + """{x ^ y : x in mx, y in my}.""" + out = 0 + x = mx + while x: + lsb = x & -x + out |= trans(my, lsb.bit_length() - 1) + x ^= lsb + return out + + +def selfsum_mask(mx): + """{x ^ y : x, y in mx} (includes 0).""" + return sumset_mask(mx, mx) + + +def delta_mask(mx): + """{x ^ y : x != y in mx} = selfsum minus {0}.""" + return selfsum_mask(mx) & ALL & ~1 + + +def sidon_cross(mx, my, px, py): + """|X+Y| = |X|*|Y| with sizes px, py (all cross sums distinct).""" + return sumset_mask(mx, my).bit_count() == px * py + + +# ------------------------------------------- class (7,1) at (10,8) + + +def class71_pairs(): + """All normalized Sidon 5-pairs: 0 in A0, 0 in A1, |A0+A1| = 25. + Backtracks A0 = {0, a1, a2, a3, a4} against the forbidden difference + set of A1 (condition Delta(A0) n Delta(A1) = 0).""" + out = [] + rest = list(range(1, N5)) + + def extend(a1m): + forb = delta_mask(a1m) + cand = [v for v in rest if not (forb >> v) & 1] + chosen = [0, 0, 0, 0, 0] + + def rec(depth, start): + if depth == 5: + out.append((mask_of(chosen), a1m)) + return + for i in range(start, len(cand)): + v = cand[i] + if v <= chosen[depth - 1]: + continue + ok = True + for j in range(1, depth): + if (forb >> (v ^ chosen[j])) & 1: + ok = False + break + if ok: + chosen[depth] = v + rec(depth + 1, i + 1) + + rec(1, 0) + + for bs in combinations(rest, 4): + a1m = 1 | mask_of(bs) + extend(a1m) + return out + + +def class71_check(a0m, a1m): + """The three translated coverage lines (I),(II),(III) for one pair. + Returns (ok, which_lines_fail).""" + sums = sumset_mask(a0m, a1m) + if sums.bit_count() != 25: + return False, ("sidon",) + tm = ALL ^ sums + fails = [] + if (sumset_mask(a0m, tm) | a1m) != ALL: + fails.append("I") + if (sumset_mask(a1m, tm) | a0m) != ALL: + fails.append("II") + if (selfsum_mask(a0m) | selfsum_mask(a1m) | selfsum_mask(tm)) != ALL: + fails.append("III") + return (not fails), tuple(fails) + + +def class71_run(progress=None, budget=None): + """Full decision run for class (7,1). Counts every normalized equality + configuration (A0, A1, d1) and every covering one; records witnesses.""" + t0 = time.time() + pairs = class71_pairs() + total = len(pairs) + checked = 0 + covering = 0 + fail_hist = {} + witnesses = [] + for (a0m, a1m) in pairs: + ok, fails = class71_check(a0m, a1m) + checked += 1 + if ok: + covering += 1 + if len(witnesses) < 5: + witnesses.append((elems(a0m), elems(a1m))) + else: + fail_hist[fails] = fail_hist.get(fails, 0) + 1 + if budget is not None and checked % 5000 == 0 and time.time() - t0 > budget: + break + return dict( + normalized_pairs=total, + checked=checked, + covering_pairs=covering, + equality_configs_normalized=total * 32, + covering_configs_normalized=covering * 32, + fail_hist={str(k): v for k, v in sorted(fail_hist.items())}, + witnesses=witnesses, + seconds=round(time.time() - t0, 2), + ) + + +# ------------------------------------------- class (8,2) at (10,8) + + +def sidon44_pairs_normalized(): + """All Sidon 4-pairs: 0 in D0, 0 in D1, |D0+D1| = 16.""" + out = [] + rest = list(range(1, N5)) + for c0 in combinations(rest, 3): + d0m = 1 | mask_of(c0) + for c1 in combinations(rest, 3): + d1m = 1 | mask_of(c1) + if sumset_mask(d0m, d1m).bit_count() == 16: + out.append((d0m, d1m)) + return out + + +def class82_choices(tm): + """All A0t = choice sets: one element of each {x, x+1} pair inside + C = H' \\ T, where T = D0+D1 must have 1-invariant complement. + Returns (choices, reason): choices empty with reason if impossible.""" + cm = ALL ^ tm + if trans(cm, 1) != cm: + return [], "C_not_1_invariant" + pairs = [] + seen = 0 + x = cm + choices = [0] + while x: + lsb = x & -x + p = lsb.bit_length() - 1 + if (seen >> p) & 1: + x ^= lsb + continue + q = p ^ 1 + if not (cm >> q) & 1: + return [], "C_pair_incomplete" + seen |= (1 << p) | (1 << q) + choices = [c | (1 << p) for c in choices] + [c | (1 << q) for c in choices] + x ^= lsb + return choices, "ok" + + +def class82_check(a0tm, d0m, d1m): + """The three coverage lines (I'),(II'),(III') for one configuration. + Returns (ok, which_lines_fail).""" + fails = [] + if (sumset_mask(a0tm, d0m) | sumset_mask(d1m, 3)) != ALL: + fails.append("I") + if (sumset_mask(a0tm, d1m) | sumset_mask(d0m, 3)) != ALL: + fails.append("II") + if (selfsum_mask(a0tm) | 3 | selfsum_mask(d0m) | selfsum_mask(d1m)) != ALL: + fails.append("III") + return (not fails), tuple(fails) + + +def class82_run(budget=None, shard=0, shards=1): + """Full decision run for class (8,2): every normalized Sidon D-pair, every + admissible A0t choice. Counts equality configurations and coverings. + Per-pair D-side masks are precomputed; (I') and (II') are decided by + OR-chains over the 8 chosen candidate translates, (III') only for + survivors. Deterministic sharding: pairs[shard::shards].""" + import itertools as _it + + t0 = time.time() + pairs = sidon44_pairs_normalized() + n_pairs_total = len(pairs) + pairs = pairs[shard::shards] + n_pairs = len(pairs) + n_choice_sets = 0 + covering = 0 + checked = 0 + fail_hist = {} + witnesses = [] + noninv = 0 + budget_hit = False + for (d0m, d1m) in pairs: + tm = sumset_mask(d0m, d1m) + choices, reason = class82_choices(tm) + if not choices: + noninv += 1 + continue + n_choice_sets += len(choices) + md1_01 = sumset_mask(d1m, 3) + md0_01 = sumset_mask(d0m, 3) + mdd = selfsum_mask(d0m) | selfsum_mask(d1m) + # per {x, x+1} pair inside C: (bit_p, bit_q, d0p, d0q, d1p, d1q) + cand = [] + seen = 0 + x = ALL ^ tm + while x: + lsb = x & -x + p = lsb.bit_length() - 1 + if (seen >> p) & 1: + x ^= lsb + continue + q = p ^ 1 + seen |= (1 << p) | (1 << q) + cand.append( + ( + 1 << p, + 1 << q, + trans(d0m, p), + trans(d0m, q), + trans(d1m, p), + trans(d1m, q), + ) + ) + x ^= lsb + for pick in _it.product((0, 1), repeat=len(cand)): + a0tm = 0 + s0 = 0 + s1 = 0 + for i, which in enumerate(pick): + c = cand[i] + if which == 0: + a0tm |= c[0] + s0 |= c[2] + s1 |= c[4] + else: + a0tm |= c[1] + s0 |= c[3] + s1 |= c[5] + checked += 1 + fails = [] + if (s0 | md1_01) != ALL: + fails.append("I") + if (s1 | md0_01) != ALL: + fails.append("II") + if (selfsum_mask(a0tm) | 3 | mdd) != ALL: + fails.append("III") + if fails: + fail_hist[tuple(fails)] = fail_hist.get(tuple(fails), 0) + 1 + else: + covering += 1 + if len(witnesses) < 5: + witnesses.append((elems(a0tm), elems(d0m), elems(d1m))) + if budget is not None and time.time() - t0 > budget: + budget_hit = True + break + return dict( + shard=shard, + shards=shards, + normalized_sidon_pairs_total=n_pairs_total, + normalized_sidon_pairs=n_pairs, + non_1_invariant_pairs=noninv, + admissible_choice_sets=n_choice_sets, + checked=checked, + covering_configs=covering, + fail_hist={str(k): v for k, v in sorted(fail_hist.items())}, + witnesses=witnesses, + budget_hit=budget_hit, + seconds=round(time.time() - t0, 2), + ) + + +# ------------------------------------------- class (6,0) at (12,6) + + +def transversals6(dm): + """All 6-sets X with X + D = F2^5 (X hits every translate x + D), for + D = dm. Complete branch-on-uncovered-requirement search with a bitmask + of covered requirements; results deduplicated as sets.""" + cov_by = [0] * N5 + for v in range(N5): + m = 0 + for x in range(N5): + if (dm >> (x ^ v)) & 1: + m |= 1 << x + cov_by[v] = m + out = set() + cur = [] + + def rec(uncov, vlo): + if len(cur) == 6: + if not uncov: + out.add(frozenset(cur)) + return + if uncov.bit_count() > 6 * (6 - len(cur)): + return + if not uncov: + for v in range(vlo, N5): + if v in cur: + continue + cur.append(v) + rec(uncov, v + 1) + cur.pop() + return + i = (uncov & -uncov).bit_length() - 1 + target = trans(dm, i) + for v in elems(target): + if v in cur: + continue + cur.append(v) + rec(uncov & ~cov_by[v], 0) + cur.pop() + + rec((1 << N5) - 1, 0) + return out + + +def class60_check(a0m, a1m, dm): + """Lines (I''),(II''),(III'') for one (A0, A1, D) triple.""" + fails = [] + if (sumset_mask(a0m, dm)) != ALL: + fails.append("I") + if (sumset_mask(a1m, dm)) != ALL: + fails.append("II") + if (selfsum_mask(a0m) | selfsum_mask(a1m) | selfsum_mask(dm)) != ALL: + fails.append("III") + return (not fails), tuple(fails) + + +def class60_run(budget=None, shard=0, shards=1): + """Decision run for class (6,0) at (12,6): complete D-side transversal + walk. Normalize 0 in D (H-half translation) and 0 in A1 (H'-half + translation; the class forces D1 = empty). For each normalized 6-set D, + F(D) = {6-sets X : X + D = F2^5} by complete search; then test every + (A0, A1) with A0 in F(D), A1 in F(D) containing 0 against A0+A1 = F2^5 + and line (III''). If F(D) is empty for every D, no (6,0) cover exists + (lines (I'')/(II'') are unsatisfiable). Deterministic sharding over the + C(31,5) normalized D by index.""" + t0 = time.time() + total_d = 169911 + tested_triples = 0 + covering = 0 + witnesses = [] + d_with_transversals = 0 + transversal_total = 0 + d_done = 0 + budget_hit = False + for idx, dc in enumerate(combinations(range(1, N5), 5)): + if idx % shards != shard: + continue + d_done += 1 + dm = 1 | mask_of(dc) + F = transversals6(dm) + if F: + d_with_transversals += 1 + transversal_total += len(F) + f_list = sorted(tuple(sorted(s)) for s in F) + for a1t in f_list: + if 0 not in a1t: + continue + a1m = mask_of(a1t) + for a0t in f_list: + a0m = mask_of(a0t) + if sumset_mask(a0m, a1m) != ALL: + continue + dm_self = selfsum_mask(dm) + if (selfsum_mask(a0m) | selfsum_mask(a1m) | dm_self) != ALL: + continue + tested_triples += 1 + covering += 1 + if len(witnesses) < 5: + witnesses.append((a0t, a1t, tuple(sorted(dc)) + (0,))) + if budget is not None and d_done % 64 == 0 and time.time() - t0 > budget: + budget_hit = True + break + return dict( + shard=shard, + shards=shards, + normalized_d_total=total_d, + d_checked=d_done, + d_with_transversals=d_with_transversals, + transversals_total=transversal_total, + tested_triples=tested_triples, + covering_triples=covering, + witnesses=witnesses, + budget_hit=budget_hit, + seconds=round(time.time() - t0, 2), + ) + + +# ------------------------------------------------- Fourier identity (7,1) + + +def fourier_71_identity(): + """Exact-integer contradiction for the (10,8) A-vanish tight class (7,1). + + L7 forces |A0+A1| = 25 with |A0| = |A1| = 5 (both odd) inside F2^5. + With f = 1_A0, g = 1_A1 and h = 1_S on S = A0+A1 (|S| = 25, all pair + sums distinct), Fourier over F2^5 gives h_hat(v) = f_hat(v) g_hat(v) for + every v (r = 1_S exactly). Parseval: + sum_{v != 0} f_hat^2 = 32*5 - 25 = 135 = sum_{v != 0} g_hat^2, + sum_{v != 0} h_hat^2 = 32*25 - 625 = 175. + Parity: |A0| odd makes every f_hat(v) odd, so f_hat^2 >= 1 pointwise; + hence (f_hat^2 - 1)(g_hat^2 - 1) >= 0 gives f_hat^2 g_hat^2 >= + f_hat^2 + g_hat^2 - 1 pointwise on v != 0 and therefore + sum h_hat^2 >= 135 + 135 - 31 = 239 > 175. Contradiction. + + Returns exact integers; the m=4 analogue (|A0| = 7, |A1| = 1 in F2^3) + computes need = lower = 7 (no contradiction), matching the real covers + of the m=4 analogue class in the PR 2933 F2^5 census.""" + out = {} + for tag, m, kx, ky, s_size in (("m5_k5", 5, 5, 5, 25), ("m3_k2", 3, 2, 2, 4)): + n = 1 << m + need = n * s_size - s_size * s_size + sum_alpha = n * kx - kx * kx + sum_beta = n * ky - ky * ky + odd = (kx % 2 == 1) and (ky % 2 == 1) + lower = sum_alpha + sum_beta - (n - 1) if odd else 0 + out[tag] = dict( + n=n, + kx=kx, + ky=ky, + s_size=s_size, + need=need, + sum_alpha=sum_alpha, + sum_beta=sum_beta, + lower_bound=lower, + parity_odd=odd, + contradiction=bool(odd and lower > need), + ) + n = 8 + out["m3_analogue_71"] = dict( + n=n, + kx=7, + ky=1, + s_size=7, + need=n * 7 - 49, + sum_alpha=n * 7 - 49, + sum_beta=n * 1 - 1, + lower_bound=(n * 7 - 49) + (n * 1 - 1) - (n - 1), + parity_odd=True, + contradiction=(n * 7 - 49) + (n * 1 - 1) - (n - 1) > n * 7 - 49, + ) + return out + + +# ------------------------------------------------- m=4 brute-force control + + +def control_m4_bruteforce(): + """Complete brute force of the two m=4 analogue classes (soundness and + completeness control for the L7 structural reduction). + + Analogue of the (7,1)-tight class: D-vanish (1,1), A split (7,1), + F1 = 7*1 + 1*1 = 8 = need. Analogue of the (8,2)-tight class: + A-vanish (2,2), D split (2,2), F1 = 4 + 4 = 8 = need. + + Direct route: every (A, D) pair with those splits inside E = F2^4 + (H = bit-0-even half, 8 points each coset), tested against the four L3 + lines. Every direct cover must show the L7 equality structure (both + cross sumsets Sidon, disjoint, union the whole odd half).""" + H = [x for x in range(16) if not (x & 1)] + Hp = [x for x in range(16) if x & 1] + + def ss(X, Y): + return {x ^ y for x in X for y in Y} + + def se(X): + return {x ^ y for x in X for y in X} + + def l3_lines(a0, a1, d0, d1): + ok_i = ss(a0, d0) | ss(a1, d1) == set(H) + ok_ii = ss(a0, d1) | ss(a1, d0) == set(Hp) + ok_iii = se(a0) | se(a1) | se(d0) | se(d1) == set(H) + ok_iv = ss(a0, a1) | ss(d0, d1) == set(Hp) + return ok_i and ok_ii and ok_iii and ok_iv + + res = {} + + covers_71 = [] + struct_71 = [] + for a0t in combinations(H, 7): + a0 = list(a0t) + for a1 in Hp: + for d0 in H: + for d1 in Hp: + if l3_lines(a0, [a1], [d0], [d1]): + covers_71.append((a0t, a1, d0, d1)) + sums = ss(a0, [a1]) + tset = set(Hp) - sums + struct_71.append( + len(sums) == 7 + and len(tset) == 1 + and ({d0 ^ d1} == tset) + ) + res["m4_class71_analogue"] = dict( + direct_covers=len(covers_71), + all_have_l7_structure=all(struct_71) if struct_71 else None, + ) + + covers_82 = [] + struct_82 = [] + for a0c in combinations(H, 2): + for a1c in combinations(Hp, 2): + for d0c in combinations(H, 2): + for d1c in combinations(Hp, 2): + a0, a1 = list(a0c), list(a1c) + d0, d1 = list(d0c), list(d1c) + if l3_lines(a0, a1, d0, d1): + covers_82.append((a0c, a1c, d0c, d1c)) + sumsA = ss(a0, a1) + sumsD = ss(d0, d1) + struct_82.append( + len(sumsA) == 4 + and len(sumsD) == 4 + and not (sumsA & sumsD) + and (sumsA | sumsD) == set(Hp) + ) + res["m4_class82_analogue"] = dict( + direct_covers=len(covers_82), + all_have_l7_structure=all(struct_82) if struct_82 else None, + ) + return res + + +def rho_classification(): + """Exact classification of the cross-multiplicity pattern of any + full-sumset pair of 6-sets in F2^5 (the forced structure of the (12,6) + A-vanish class (6,0), and of every (A, D) line (I'')/(II'')). + + Let X, Y be 6-sets with X + Y = F2^5 and r(s) = #{(x,y): x+y = s} = + 1 + rho(s), sum rho = 36 - 32 = 4. Fourier: rho_hat(v) = f_hat(v) + g_hat(v) for v != 0. Every f_hat(v), g_hat(v) is even and + |rho_hat(v)| <= sum rho = 4, so per nonzero v: f_hat(v) g_hat(v) is in + {0, 4, -4}, i.e. (f_hat, g_hat) = (0, *) or (*, 0) or both +-2. + Parseval gives sum_{v != 0} f_hat^2 = 156 and rho-Parseval gives + |V22| = 2 sum rho^2 - 1 where V22 = {v != 0: |f_hat| = |g_hat| = 2}. + + Case table (exact integers; the Walsh constraints are machine-checked in + test_engine.py): + + rho type sum rho^2 |V22| needed Walsh constraint verdict + 4 delta_p 16 31 rho_hat = +-4 always DEAD + 3+1 10 19 +-2 occurs for p != q DEAD + 2+2 8 15 subspace size 15 SURVIVES + 2+1+1 6 11 sizes 2^{5-r}-1 DEAD + 1+1+1+1 4 7 rank-3 flat / rank-2 SURVIVES + + DEAD reasons: (4 delta_p) Parseval 156 = 4*31 + (36a+16b) forces + 32 = 36a+16b with |Vf| = a + b = 0, impossible; (3+1) rho_hat = + 3(-1)^{vq} + (-1)^{vp} lies in {+-2, +-4} and |rho_hat| <= 4 needs + v*(p+q) = 0 for every v != 0, i.e. p = q; (2+1+1) V22 is + {v: v*(p1+p2) = 0 and v*(p1+q) = 0} minus {0}, of size 2^{5-r} - 1 in + {1,3,7,15,31}, never 11. + + Surviving types: + (T1) rho = 1 on an affine 2-flat {p1, p2, p3, p1+p2+p3} and 0 else; + (T2) rho = 2 on two distinct points {q1, q2} and 0 else. + Both sides' spectra are pinned: T1 has |Vf| = |Vg| = 8 all of magnitude + 4 and |V00| = 8; T2 has |Vf| = |Vg| = 6 and |V00| = 4.""" + return { + "types": [ + dict( + rho="4*delta_p", + sum_rho2=16, + v22_needed=31, + verdict="DEAD", + reason="Parseval 156 = 4*31 + (36a+16b) needs 32 = 36a+16b with |Vf| = 0", + ), + dict( + rho="3+1", + sum_rho2=10, + v22_needed=19, + verdict="DEAD", + reason="v*(p+q) = 0 for all v != 0 forces p = q", + ), + dict( + rho="2+2", + sum_rho2=8, + v22_needed=15, + verdict="SURVIVES", + v22=15, + vf=6, + vg=6, + v00=4, + ), + dict( + rho="2+1+1", + sum_rho2=6, + v22_needed=11, + verdict="DEAD", + reason="2^{5-r}-1 in {1,3,7,15,31}, never 11", + ), + dict( + rho="1+1+1+1", + sum_rho2=4, + v22_needed=7, + verdict="SURVIVES", + v22=7, + vf=8, + vg=8, + v00=8, + ), + ], + "surviving": ["2+2", "1+1+1+1"], + } + + +def identity_odd_sides(s, t, m=6): + """Cross-sum multiplicity identity for splits with BOTH sides odd (the + (11,7) and (9,9) splits, where no character can vanish - PR 2933 L2). + + With A an s-set and D a t-set in E = F2^m covering the odd line + A + D = E, the multiplicity is r = 1 + rho with sum rho = s*t - 2^m. + Fourier over E: rho_hat(v) = f_hat(v) g_hat(v) for v != 0, every f_hat + and g_hat is odd (s, t odd), so f_hat^2 g_hat^2 >= f_hat^2 + g_hat^2 - 1 + pointwise. Parseval: sum_{v != 0} f_hat^2 = 2^m s - s^2 and likewise + for g, sum_{v != 0} rho_hat^2 = 2^m sum rho^2 - (sum rho)^2. + + The pointwise inequality yields the EXACT necessary condition + 2^m sum rho^2 - (st - 2^m)^2 >= (2^m s - s^2) + (2^m t - t^2) + - (2^m - 1), + i.e. a lower bound on sum rho^2. For (11,7) and (9,9) at m = 6 the + bound is satisfiable (the excess 13 resp. 17 is too large for the + identity to contradict), so the identity is DEMOTED as an exclusion + mechanism for these splits; the numbers below are exact.""" + n = 1 << m + excess = s * t - n + sum_alpha = n * s - s * s + sum_beta = n * t - t * t + lower = sum_alpha + sum_beta - (n - 1) + # sum rho^2 >= ceil((lower + excess^2) / n) + num = lower + excess * excess + rho2_min = -(-num // n) + parity_odd = (s % 2 == 1) and (t % 2 == 1) + # products f_hat*g_hat must lie within +-excess pointwise + return dict( + split=(s, t), + m=m, + excess=excess, + sum_alpha=sum_alpha, + sum_beta=sum_beta, + pointwise_lower_sum_rho_hat_sq=lower, + sum_rho2_min=rho2_min, + sum_rho2_max=excess * excess, + parity_odd=parity_odd, + contradiction=bool(parity_odd and rho2_min > excess * excess), + ) diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/vendor/agent64_cover17.py b/research/f7-18point-tight-classes-seed4c1e7b30/vendor/agent64_cover17.py new file mode 100644 index 0000000000..5add3747a3 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/vendor/agent64_cover17.py @@ -0,0 +1,263 @@ +"""17-point cover audit engine: pair-representation identity, sharp rows, +coverage primitives and exact small controls. + +Object (KB3c, pair-collision object change recorded in TASK.json): the status +of PR 2542's claim "No 17-point set covers F2^7" against its own lemma table. +PR 2542's `lemma_a_table` (vendored byte-exact as vendor/pr2542_engine.py, +credit PR 2542, package research/universal-f7-singleton-seedb859517b) only +contradicts the (9,8)/(8,9) split rows; the counting-feasible 17-point splits +(10,7)/(7,10)/(11,6)/(6,11) survive it. This module extends the identity +with the sharp collision-multiplicity constraint and computes exactly which +(e_ex, b_ex, c) rows survive per split. + +Definitions. S = A u B with A = S int E (s points, even weight), B = S int O +(t points, odd weight), s + t = 17. A_x = #unordered pairs of A summing to +x, B_x likewise (x even nonzero). e_ex = C(s,2) - |supp(A)|, b_ex likewise. +Cross sums a+b (a in A, b in B) hit the odd masks with multiplicities r_o, so + + odd excess sum_o (r_o - 1) = s*t - 2^(n-1) =: E_o + colliding pairs sum_o C(r_o,2) = 2 * sum_x A_x B_x =: 2c + +with C(r,2) >= r-1 per mask. A collision profile is a partition of E_o into +j = r_o - 1 parts; it needs sigma = sum j(j+1)/2 = 2c even. A row (e_ex, +b_ex) is multiset-feasible for profile c iff c is exactly attainable as the +sum of shared products A_x B_x over the shared = C(s,2)+C(t,2)-e_ex-b_ex- +(2^(n-1)-1) support positions (multiplicity shapes from partitions of e_ex +resp. b_ex). This refines PR 2542's closed-form upper bound. +""" + +from functools import lru_cache + +VENDOR_PIN_PR2542 = ( + "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" +) + + +# ------------------------------------------------------- counting bounds + + +def counting_ok(n, s, t): + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + return ( + s * t >= odd_masks + and s * (s - 1) // 2 + t * (t - 1) // 2 >= even_nonzero + ) + + +# ------------------------------------------- collision-multiplicity identity + + +def _partitions(total): + """Integer partitions of total as tuples (non-increasing).""" + if total == 0: + yield () + return + for part in range(total, 0, -1): + for rest in _partitions(total - part): + if not rest or rest[0] <= part: + yield (part,) + rest + + +def odd_profiles(excess): + """Collision profiles for odd excess `excess`: partitions j of it with + sigma = sum j(j+1)/2 even (= 2c for integer c). Each j is one odd mask + with r = j + 1 cross representations.""" + out = [] + for parts in _partitions(excess): + sigma = sum(j * (j + 1) // 2 for j in parts) + if sigma % 2 == 0: + out.append(sorted(parts)) + return sorted(out) + + +def profile_c_values(n, s, t): + """c = sum_x A_x B_x forced by each integer collision profile.""" + excess = s * t - (1 << (n - 1)) + if excess < 0: + return [] + return sorted( + {sum(j * (j + 1) // 2 for j in parts) // 2 for parts in odd_profiles(excess)} + ) + + +def _shapes(total_pairs, excess): + """Multiplicity shapes: A_x values summing to total_pairs with support + size total_pairs - excess (the excess parts carry the collisions).""" + if excess > total_pairs: + return + for parts in _partitions(excess): + yield tuple(sorted((1 + p for p in parts), reverse=True)) + ( + 1, + ) * (total_pairs - excess - len(parts)) + + +def _draws(shape, shared): + """All multisets of `shared` values drawn from a multiplicity shape.""" + if shared == 0: + yield () + return + counts = {} + for v in shape: + counts[v] = counts.get(v, 0) + 1 + vals = sorted(counts) + limits = [counts[v] for v in vals] + + def rec(i, remaining, acc): + if i == len(vals): + if remaining == 0: + yield tuple(acc) + return + for take in range(min(limits[i], remaining) + 1): + yield from rec(i + 1, remaining - take, acc + [vals[i]] * take) + + yield from rec(0, shared, []) + + +def _pairing_sums(a_draw, b_draw): + """All dot products sum a_i b_pi(i) over pairings of two draws.""" + if len(a_draw) <= 1: + yield sum(x * y for x, y in zip(a_draw, b_draw)) + return + a0 = a_draw[0] + for i in range(len(b_draw)): + rest = b_draw[:i] + b_draw[i + 1 :] + for tail in _pairing_sums(a_draw[1:], rest): + yield a0 * b_draw[i] + tail + + +def attainable_c(n, s, t, e_ex, b_ex): + """Exact attainable values of sum_x A_x B_x on the shared support + positions for one (e_ex, b_ex) row.""" + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + shared = A + B - e_ex - b_ex - even_nonzero + if shared < 0: + return set() + out = set() + for sa in _shapes(A, e_ex): + for sb in _shapes(B, b_ex): + for da in _draws(sa, shared): + for db in _draws(sb, shared): + out.update(_pairing_sums(da, db)) + return out + + +def sharp_rows(n, s, t): + """Sharp pair-representation rows for one parity split. + + Returns {feasible, rows: [{e_ex, b_ex, shared, c}], best, need}: a row + survives iff some integer collision profile's c is exactly attainable. + `best` is the largest attainable c (PR 2542's closed-form comparison + quantity), `need` = ceil((s*t - 2^(n-1))/2) the profile-level necessity. + """ + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + excess = s * t - odd_masks + need = (excess + 1) // 2 if excess > 0 else 0 + rows = [] + best = -1 + if excess < 0 or A + B < even_nonzero: + return dict(feasible=False, rows=[], best=best, need=need) + c_vals = set(profile_c_values(n, s, t)) + for e_ex in range(A + 1): + for b_ex in range(B + 1): + shared = A + B - e_ex - b_ex - even_nonzero + if shared < 0: + continue + attain = attainable_c(n, s, t, e_ex, b_ex) + if not attain: + continue + best = max(best, max(attain)) + for c in sorted(attain & c_vals): + rows.append(dict(e_ex=e_ex, b_ex=b_ex, shared=shared, c=c)) + return dict(feasible=bool(rows), rows=rows, best=best, need=need) + + +def surviving_rows(n, s, t, min_e_ex=0, min_b_ex=0): + """Sharp rows filtered by census-implied minimum excesses (min excess of + s-point sets resp. t-point sets in F2^(n-1)).""" + sharp = sharp_rows(n, s, t) + rows = [ + r + for r in sharp["rows"] + if r["e_ex"] >= min_e_ex and r["b_ex"] >= min_b_ex + ] + return dict( + feasible=bool(rows), + rows=rows, + best=sharp["best"], + need=sharp["need"], + ) + + +# ------------------------------------------------------ coverage primitives + + +def coverage_mask(pts): + """Bitmask of {a ^ b : a, b in pts} (self-pairs give mask 0).""" + mask = 1 # zero via a = b + for i in range(len(pts)): + pi = pts[i] + for j in range(i): + mask |= 1 << (pi ^ pts[j]) + return mask + + +def coverage_mask_dual(pts): + """Dual predicate (PR 2542's independent check): mask m is covered iff + (pts xor m) meets pts.""" + pset = set(pts) + limit = 1 << max(pts).bit_length() if pts else 1 + mask = 0 + for m in range(limit): + if any((p ^ m) in pset for p in pts): + mask |= 1 << m + return mask + + +# --------------------------------------------------- exact small controls + + +@lru_cache(maxsize=None) +def brute_force_set_census(n, k): + """Exact census of k-point sets S (0 in S, translation WLOG) over F2^n: + returns (number of covering sets, max |S+S|). Incremental DFS over + combinations with the pair-count upper-bound prune.""" + N = 1 << n + full_mask = (1 << N) - 1 + pairs_total = k * (k - 1) // 2 + state = {"covers": 0, "best": 0} + + sums = [0] + masks = [1] # stack of coverage masks + + def rec(next_pt, depth): + size = depth + 1 + if size == k: + mask = masks[-1] + covered = mask.bit_count() + if covered > state["best"]: + state["best"] = covered + if mask == full_mask: + state["covers"] += 1 + return + remaining_pairs = pairs_total - size * (size - 1) // 2 + if masks[-1].bit_count() + remaining_pairs < N: + return + for p in range(next_pt, N): + new = 1 << p + for q in sums: + new |= 1 << (p ^ q) + sums.append(p) + masks.append(masks[-1] | new) + rec(p + 1, depth + 1) + masks.pop() + sums.pop() + + rec(1, 0) + return state["covers"], state["best"] diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/vendor/agent64_search17.py b/research/f7-18point-tight-classes-seed4c1e7b30/vendor/agent64_search17.py new file mode 100644 index 0000000000..ef17635967 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/vendor/agent64_search17.py @@ -0,0 +1,330 @@ +"""Exact Sidon/near-Sidon census for the 17-point cover question (F2^7). + +Established here (receipt in SIDON-RECEIPT.json): + + * F2^6 has no Sidon 10-set. A complete DFS of all 10-subsets of the even + group E (= F2^6) containing {0, 3} finds none; Sidon-ness is translation- + invariant and GL(6,2)-invariant, and GL(6,2) is transitive on nonzero + elements, so one shard decides existence. Consequences (recorded in the + package README with the removal argument): every 10-point set has + pair-sum excess >= 1, every 11-point set has excess >= 2. This kills + the extremal (10,7) row of cover17.sharp_rows (e_ex = 0) and the (11,6) + rows e_ex in {0, 1}. + +Remaining exact search domains (row-restricted; the handoff object): + + rows (10,7): (e_ex, b_ex, c) in {(1,0,3), (1,1,4), (2,0,3)} + rows (11,6): (e_ex, b_ex, c) = (e, 6-e, 1) with e in {2,3,4,5,6} + +`enumerate_sets` is the enumeration primitive a row-restricted search builds +on (per-A constrained B-side DFS; the B side is far too large to enumerate +outright: ~3.1e8 Sidon 7-sets in the odd coset). Domain completeness for a +search: fix 0, 3 in A (GL(6,2) transitivity + stabilizer arguments, see +README); do NOT fix any element of B (the stabilizer extension fixes the +coset shift u and cannot move B's elements to it). Standard library only. +""" + +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +N = 128 +EVEN = [x for x in range(N) if x.bit_count() % 2 == 0] +ODD = [x for x in range(N) if x.bit_count() % 2 == 1] +EVEN_NZ = sum(1 << x for x in EVEN if x) # 63 even nonzero masks +ODD_ALL = sum(1 << x for x in ODD) # 64 odd masks +RECEIPT = HERE / "SIDON-RECEIPT.json" + + +# ------------------------------------------------------------ enumeration + + +def enumerate_sets(pool, k, budget, fixed=()): + """All k-subsets of `pool` containing `fixed`, of pair-sum excess + <= budget. Yields (pts, support_mask, mult) where mult maps each + supported even mask to its pair multiplicity A_x. Free elements are + chosen in increasing pool order, so each set is yielded once.""" + fixed = tuple(sorted(fixed)) + pts = list(fixed) + mult = {} + for i in range(len(pts)): + for j in range(i): + x = pts[i] ^ pts[j] + mult[x] = mult.get(x, 0) + 1 + supp = 0 + for x in mult: + supp |= 1 << x + excess = sum(mult.values()) - bin(supp).count("1") + + def rec(idx, supp, excess): + if len(pts) == k: + yield (tuple(pts), supp, dict(mult)) + return + need = k - len(pts) + for p in range(idx, len(pool) - need + 1): + v = pool[p] + if v in pts: + continue + new_sums = [v ^ q for q in pts] if pts else [] + add = 0 + coll = 0 + for x in new_sums: + if supp >> x & 1: + coll += 1 + else: + add |= 1 << x + new_excess = excess + coll + if new_excess > budget: + continue + for x in new_sums: + mult[x] = mult.get(x, 0) + 1 + pts.append(v) + yield from rec(p + 1, supp | add, new_excess) + pts.pop() + for x in new_sums: + mult[x] -= 1 + if mult[x] == 0: + del mult[x] + + yield from rec(0, supp, excess) + + +def count_sets(pool, k, budget, fixed=(), exclude=()): + """(count, first) for the same domain as enumerate_sets, without + materializing leaves (fast path for receipts).""" + fixed = tuple(sorted(fixed)) + pts = list(fixed) + supp = 0 + excess = 0 + for i in range(len(pts)): + for j in range(i): + x = pts[i] ^ pts[j] + if supp >> x & 1: + excess += 1 + else: + supp |= 1 << x + state = {"count": 0, "first": None} + + def rec(idx, supp, excess): + if len(pts) == k: + state["count"] += 1 + if state["first"] is None: + state["first"] = tuple(pts) + return + need = k - len(pts) + for p in range(idx, len(pool) - need + 1): + v = pool[p] + if v in pts: + continue + add = 0 + coll = 0 + for q in pts: + x = v ^ q + if supp >> x & 1: + coll += 1 + else: + add |= 1 << x + new_excess = excess + coll + if new_excess > budget: + continue + pts.append(v) + rec(p + 1, supp | add, new_excess) + pts.pop() + + rec(0, supp, excess) + return state["count"], state["first"] + + +def hist_sets(pool, k, budget, fixed=(), exclude=(), floor=None): + """Exact-excess histogram over the same domain: dict excess -> count, + plus one example per excess value. `floor` restricts free elements to + values > floor (sub-shard partition by the smallest free element).""" + fixed = tuple(sorted(fixed)) + excl = set(exclude) + pts = list(fixed) + supp = 0 + excess = 0 + for i in range(len(pts)): + for j in range(i): + x = pts[i] ^ pts[j] + if supp >> x & 1: + excess += 1 + else: + supp |= 1 << x + hist = {} + examples = {} + + def rec(idx, supp, excess): + if len(pts) == k: + hist[excess] = hist.get(excess, 0) + 1 + if str(excess) not in examples: + examples[str(excess)] = tuple(pts) + return + need = k - len(pts) + for p in range(idx, len(pool) - need + 1): + v = pool[p] + if v in pts or v in excl: + continue + if floor is not None and v <= floor: + continue + add = 0 + coll = 0 + for q in pts: + x = v ^ q + if supp >> x & 1: + coll += 1 + else: + add |= 1 << x + new_excess = excess + coll + if new_excess > budget: + continue + pts.append(v) + rec(p + 1, supp | add, new_excess) + pts.pop() + + rec(0, supp, excess) + return hist, examples + + +# --------------------------------------------------------------- receipt + + +def sidon_receipt(): + """The load-bearing exact counts. Shard = sets through {0, 3} in E + (complete for existence by GL(6,2) transitivity) and through {1} in O + (B-side feasibility/sizing only, not used for completeness).""" + out = {"shard_e03": {}, "shard_o1": {}} + for k, budget in ((10, 0), (9, 0), (10, 1)): + t1 = time.time() + n, first = count_sets(EVEN, k, budget, fixed=(0, 3)) + out["shard_e03"][f"k{k}_budget{budget}"] = { + "count": n, + "first": first, + "seconds": round(time.time() - t1, 1), + } + RECEIPT.write_text(json.dumps(out, indent=2, sort_keys=True), encoding="utf-8") + print(f"SIDON k={k} budget={budget} shard(0,3) n={n}", flush=True) + t1 = time.time() + n, first = count_sets(ODD, 7, 0, fixed=(1,)) + out["shard_o1"]["k7_budget0"] = { + "count": n, + "first": first, + "seconds": round(time.time() - t1, 1), + } + out["controls"] = { + "small_space_agreement": "enumerate_sets == naive brute force on the " + "even subgroup < 32: k=4 420/420, k=5 840/840, k=6 168/168" + } + RECEIPT.write_text(json.dumps(out, indent=2, sort_keys=True), encoding="utf-8") + print(f"SIDON k=7 budget=0 shard(1) odd n={n}", flush=True) + return out + + +def raw11_census(budget=4): + """Raw-domain census of 11-sets through {0, 3} with pair-sum excess + <= budget, counting by exact excess (the histogram yields the level-3 + and level-4 counts in one walk). Sub-sharded by the smallest free + element (disjoint, complete), resumable via RAW11-PROGRESS.json.""" + prog_path = HERE / "RAW11-PROGRESS.json" + prog = {"budget": budget, "shards": {}} + if prog_path.exists(): + old = json.loads(prog_path.read_text(encoding="utf-8")) + if old.get("budget") == budget: + prog = old + for v0 in EVEN: + if v0 in (0, 3): + continue + key = f"v0={v0}" + if key in prog["shards"]: + continue + t1 = time.time() + hist, examples = hist_sets( + EVEN, 11, budget, fixed=(0, 3, v0), floor=v0 + ) + prog["shards"][key] = { + "hist": {str(k): v for k, v in sorted(hist.items())}, + "examples": examples, + "seconds": round(time.time() - t1, 1), + } + prog_path.write_text( + json.dumps(prog, indent=2, sort_keys=True), encoding="utf-8" + ) + print(f"RAW11 {key} hist={hist} seconds={prog['shards'][key]['seconds']}", flush=True) + total = {} + for rec in prog["shards"].values(): + for e, n in rec["hist"].items(): + total[e] = total.get(e, 0) + n + prog["total_hist"] = {str(k): v for k, v in sorted(total.items())} + prog["complete"] = True + prog_path.write_text(json.dumps(prog, indent=2, sort_keys=True), encoding="utf-8") + print(f"RAW11 total_hist={prog['total_hist']}", flush=True) + return prog + + +def main(): + mode = sys.argv[1] if len(sys.argv) > 1 else "receipt" + if mode == "receipt": + sidon_receipt() + elif mode == "deeper": + # Follow-up census: decide whether excess 2 is attainable at all for + # 10-sets (kills the last (10,7) row (2,0,3) if not) and size the + # 11-set side (rows (11,6) with e_ex in {2, 3}). + out = {} + if RECEIPT.exists(): + out = json.loads(RECEIPT.read_text(encoding="utf-8")) + out.setdefault("shard_e03", {}) + for k, budget in ((10, 2), (11, 2)): + t1 = time.time() + n, first = count_sets(EVEN, k, budget, fixed=(0, 3)) + out["shard_e03"][f"k{k}_budget{budget}"] = { + "count": n, + "first": first, + "seconds": round(time.time() - t1, 1), + } + RECEIPT.write_text( + json.dumps(out, indent=2, sort_keys=True), encoding="utf-8" + ) + print(f"SIDON k={k} budget={budget} shard(0,3) n={n}", flush=True) + elif mode == "deeper2": + # Pin min excess(10) exactly and push the (11,6) A-side rows: + # k=11 budget b decides rows (e, 6-e, 1) with e = b. + out = {} + if RECEIPT.exists(): + out = json.loads(RECEIPT.read_text(encoding="utf-8")) + out.setdefault("shard_e03", {}) + for k, budget in ((10, 3), (11, 3), (11, 4)): + t1 = time.time() + n, first = count_sets(EVEN, k, budget, fixed=(0, 3)) + out["shard_e03"][f"k{k}_budget{budget}"] = { + "count": n, + "first": first, + "seconds": round(time.time() - t1, 1), + } + RECEIPT.write_text( + json.dumps(out, indent=2, sort_keys=True), encoding="utf-8" + ) + print(f"SIDON k={k} budget={budget} shard(0,3) n={n}", flush=True) + elif mode == "raw11": + prog = raw11_census() + if RECEIPT.exists(): + out = json.loads(RECEIPT.read_text(encoding="utf-8")) + else: + out = {} + out["k11_raw_budget4"] = { + "domain": "11-sets through {0,3} (complete by GL(6,2) " + "transitivity), sub-sharded by the smallest free element", + "total_hist": prog["total_hist"], + "sub_shards": len(prog["shards"]), + "complete": True, + } + RECEIPT.write_text(json.dumps(out, indent=2, sort_keys=True), encoding="utf-8") + else: + raise SystemExit(f"unknown mode {mode}") + + +if __name__ == "__main__": + main() diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/vendor/cover18.py b/research/f7-18point-tight-classes-seed4c1e7b30/vendor/cover18.py new file mode 100644 index 0000000000..3faa640d79 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/vendor/cover18.py @@ -0,0 +1,741 @@ +"""KB3e engine: the 18-point cover question for F2^7. + +Object. In the PR943 prefix-walk model (Ross Richardson, +`research/universal-connector-boundary`, PR 943) a restored seven-source +singleton word is universal exactly when its prefix set `P` covers: +`P + P = F2^7` (every mask of F2^7 is a pair-sum `a + b` of two elements of the +set; self-pairs `a + a` cover mask 0, and the sumset is translation-invariant +so WLOG `0 in S`). PR 2542 (Aaron Wang) excludes length 18 and asserts "no +17-point set covers F2^7"; PR 2773 (Aaron Wang) audits it split-by-split and +PR 2870 (Aaron Wang) closes the remainder rows (5,1),(6,0) with an exact +odd-coverage Fourier/Parseval identity. This module asks the immediate +successor question: **does any 18-point set cover F2^7?** + +Parity splits. S = A u B with A = S int E (s points, even-weight coset) and +B = S int O (t points, odd-weight coset), s + t = 18. The counting-feasible +splits are (12,6), (11,7), (10,8), (9,9) and their mirrors; every 18-point +split has s and t of EQUAL parity (18 is even), which is exactly the case the +PR 2870 squeeze does not reach (its hypothesis is opposite parity). + +Three layers of evidence are computed here, all exact integer arithmetic: + +1. `fourier_profile_feasibility(n, s, t)` -- a per-character profile system + (necessary conditions for a cover): parity of characters, the odd-half + bound |f_hat g_hat| = |rho_hat| <= E_o with rho_hat == E_o (mod 2), the + even-half bound f_hat^2 + g_hat^2 <= s + t + 2*P - 2^n (P = C(s,2)+C(t,2)), + Parseval on both sides, and the exact attainable sums of squares of rho. + Infeasibility of the system PROVES the split impossible; feasibility only + says the Fourier layer does not exclude it. The system reproduces the + PR 2870 exclusion of (11,6)/(6,11) (control in test_engine.py). +2. `sharp_rows_fast(n, s, t)` -- PR 2773's pair-representation rows + (e_ex, b_ex, c), reusing its byte-vendored shape/draw primitives with a + contingency-table pairing-sums replacement that the vendored O(m!) pairing + loop cannot run at the 18-point row sizes. Census floors (min pair-sum + excess of k-sets in F2^6) demote rows exactly as in PR 2773. +3. `search_split(...)` / `search_direct(...)` -- a bounded, seeded local + search for a covering pair (A, D) resp. an 18-point set. A found cover is + a falsifying instance for "no 18-point cover exists"; a failed bounded + search is recorded as a scoped search failure, never as an exclusion. + +Reduction lemma (checked exhaustively at n = 3 in test_engine.py). Fix an +odd mask p and set D = p + B (a subset of E). Then S = A u B covers F2^n iff +(i) A + D = E and (ii) (A + A) u (D + D) = E. So every split (s, t) is a +two-set covering problem in the even group E =~ F2^6. + +All arithmetic is exact Python integers; no floats are used. +""" + +import random +import time +from collections import Counter +from functools import lru_cache +from itertools import combinations +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "vendor")) + +import agent64_cover17 as c17 # noqa: E402 + +# Byte pins of the vendored PR 2773 engine (credit: Aaron Wang, PR 2773, +# head 6739c799799621878a9249c93e2b12cc799c1482; extracted with +# agent_tools.py pr-tree-extract from PR 2870's hash-pinned vendor/). +VENDOR_PIN_COVER17 = ( + "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654" +) +VENDOR_PIN_SEARCH17 = ( + "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674" +) + + +# ------------------------------------------------------------- coverage + + +def dot(s, x): + return (s & x).bit_count() & 1 + + +def coverage_mask(pts): + """Bitmask of {a ^ b : a, b in pts} (self-pairs give mask 0).""" + mask = 1 + for i in range(len(pts)): + pi = pts[i] + for j in range(i): + mask |= 1 << (pi ^ pts[j]) + return mask + + +def covers(pts, n=7): + return coverage_mask(pts) == (1 << (1 << n)) - 1 + + +def split_of(pts): + e = sum(1 for p in pts if not dot(127, p)) + return (e, len(pts) - e) + + +def even_masks(n=7): + return [x for x in range(1 << n) if not dot((1 << n) - 1, x)] + + +def odd_masks(n=7): + return [x for x in range(1 << n) if dot((1 << n) - 1, x)] + + +def _pair_mask(pts): + """Bitmask over the 128 masks of {a ^ b : a, b in pts} (0 via a = b).""" + return coverage_mask(pts) + + +def _covers_all(mask, universe): + return (mask & universe) == universe + + +def reduction_conditions(A, B, n=7): + """(odd_ok, even_ok) of the (A, D) reduction. D = p + B for an odd p; + A u B covers F2^n iff odd_ok and even_ok both hold.""" + p = 1 + D = [p ^ b for b in B] + ev = even_masks(n) + universe = 0 + for x in ev: + universe |= 1 << x + cross = 0 + for a in A: + for d in D: + cross |= 1 << (a ^ d) + selfs = _pair_mask(A) | _pair_mask(D) + return _covers_all(cross, universe), _covers_all(selfs, universe) + + +# ------------------------------------------------------- rho bookkeeping + + +def _partitions(total): + if total == 0: + yield () + return + for part in range(total, 0, -1): + for rest in _partitions(total - part): + if not rest or rest[0] <= part: + yield (part,) + rest + + +@lru_cache(maxsize=None) +def rho_square_values(excess): + """Attainable sums of squares sum rho_x^2 over integer rho >= 0 with + sum rho_x = excess (partition square sums). Domain guard: excess <= 24 + (all splits this package decides have E_o <= 17); beyond that the + partition enumeration is out of budget and callers must treat the split + as not attempted, never as excluded.""" + if excess > 24: + raise ValueError("rho_square_values: excess %d out of budget" % excess) + return sorted({sum(j * j for j in parts) for parts in _partitions(excess)}) + + +# ------------------------------------------------- Fourier profile system + + +def even_half_max(n, s, t): + """Max of f_hat^2 + g_hat^2 off the all-ones hyperplane, from the even + half of the covering condition: s + t + 2*P - 2^n, P = C(s,2)+C(t,2).""" + P = s * (s - 1) // 2 + t * (t - 1) // 2 + return s + t + 2 * P - (1 << n) + + +def shapes_fourier(n, s, t, nonzero_both=False): + """Admissible per-character shapes (f2, g2, p2) = (f_hat^2, g_hat^2, + (f_hat*g_hat)^2) off {0, 1}: character parities, |rho_hat| <= E_o with + rho_hat == E_o (mod 2), and the even-half bound. nonzero_both restricts + to shapes with both characters nonzero (the no-vanishing sub-case).""" + eo = s * t - (1 << (n - 1)) + if eo < 0: + return [] + bound = even_half_max(n, s, t) + out = [] + for a in range(0, s + 1): + if a % 2 != s % 2: + continue + if nonzero_both and a == 0: + continue + for b in range(0, t + 1): + if b % 2 != t % 2: + continue + if nonzero_both and b == 0: + continue + prod = a * b + if prod > eo or prod % 2 != eo % 2: + continue + if a * a + b * b > bound: + continue + out.append((a * a, b * b, prod * prod)) + return out + + +def _solve_counts(shapes, U, RF, RG, RP, cap=4000000): + """First nonneg integer solution of sum n_i = U, sum n_i f2_i = RF, + sum n_i g2_i = RG, sum n_i p2_i = RP, or None. Returns (solution, nodes) + with nodes = "cap" when the step cap is hit (caller must treat as + undecided, never as infeasible).""" + m = len(shapes) + if m == 0: + if U == 0 and RF == 0 and RG == 0 and RP == 0: + return ([], 0) + return (None, 0) + order = sorted(range(m), key=lambda i: -shapes[i][0]) + shp = [shapes[i] for i in order] + sol = [0] * m + nodes = [0] + + # suffix min/max of each coefficient for bound pruning + smin_f = [0] * (m + 1) + smax_f = [0] * (m + 1) + smin_g = [0] * (m + 1) + smax_g = [0] * (m + 1) + smin_p = [0] * (m + 1) + smax_p = [0] * (m + 1) + for i in range(m - 1, -1, -1): + f2, g2, p2 = shp[i] + smin_f[i] = min(f2, smin_f[i + 1]) + smax_f[i] = max(f2, smax_f[i + 1]) + smin_g[i] = min(g2, smin_g[i + 1]) + smax_g[i] = max(g2, smax_g[i + 1]) + smin_p[i] = min(p2, smin_p[i + 1]) + smax_p[i] = max(p2, smax_p[i + 1]) + + def rec(i, u_rem, rf, rg, rp): + nodes[0] += 1 + if nodes[0] > cap: + return "cap" + if i == m - 1: + f2, g2, p2 = shp[i] + if u_rem >= 0 and rf == u_rem * f2 and rg == u_rem * g2 and rp == u_rem * p2: + sol[i] = u_rem + return True + return False + f2, g2, p2 = shp[i] + hi = u_rem + if f2: + hi = min(hi, rf // f2) + if g2: + hi = min(hi, rg // g2) + if p2: + hi = min(hi, rp // p2) + for k in range(hi, -1, -1): + ru, rff, rgg, rpp = u_rem - k, rf - k * f2, rg - k * g2, rp - k * p2 + if ru < 0 or rff < 0 or rgg < 0 or rpp < 0: + continue + if rff > ru * smax_f[i + 1] or rff < ru * smin_f[i + 1]: + continue + if rgg > ru * smax_g[i + 1] or rgg < ru * smin_g[i + 1]: + continue + if rpp > ru * smax_p[i + 1] or rpp < ru * smin_p[i + 1]: + continue + sol[i] = k + got = rec(i + 1, ru, rff, rgg, rpp) + if got == "cap": + return "cap" + if got: + return True + sol[i] = 0 + return False + + got = rec(0, U, RF, RG, RP) + if got == "cap": + return (None, "cap") + if got: + out = [0] * m + for slot, orig in enumerate(order): + out[orig] = sol[slot] + return (out, nodes[0]) + return (None, nodes[0]) + + +def fourier_profile_feasibility(n, s, t, nonzero_both=False): + """Necessary-condition system for an (s,t) split at F2^n. `feasible` + False PROVES the odd half (hence the cover) impossible; `feasible` True + means only that this Fourier layer does not exclude the split. With + nonzero_both=True the system is restricted to per-characters with both + sides nonzero: infeasibility then PROVES every cover of this split must + have at least one vanishing character off {0, 1}.""" + eo = s * t - (1 << (n - 1)) + res = { + "n": n, + "split": (s, t), + "odd_excess": eo, + "nonzero_both": nonzero_both, + "even_half_max": even_half_max(n, s, t), + } + if eo < 0: + res["feasible"] = False + res["reason"] = "counting: fewer cross pairs than odd masks" + res["feasible_S"] = [] + return res + if eo > 24: + res["feasible"] = None + res["reason"] = "E_o out of the rho-square enumeration budget: not attempted" + res["feasible_S"] = [] + return res + shapes = shapes_fourier(n, s, t, nonzero_both=nonzero_both) + res["shapes"] = shapes + U = (1 << n) - 2 + RF = (1 << n) * s - 2 * s * s + RG = (1 << n) * t - 2 * t * t + res["parseval_remainders"] = (RF, RG) + feasible_S = [] + example = None + capped = False + for S in rho_square_values(eo): + RP = (1 << n) * S - 2 * eo * eo + sol, nodes = _solve_counts(shapes, U, RF, RG, RP) + if nodes == "cap": + capped = True + continue + if sol is not None: + feasible_S.append(S) + if example is None: + example = {"S": S, "counts": sol} + res["feasible_S"] = feasible_S + res["example"] = example + res["capped"] = capped + if capped: + res["feasible"] = True + res["reason"] = ( + "step cap hit for some S values: undecided for those (never a " + "proof of impossibility); S values listed are the feasible ones" + ) + elif feasible_S: + res["feasible"] = True + res["reason"] = ( + "profile system consistent for S in %s; no Fourier contradiction" + % sorted(feasible_S) + ) + else: + res["feasible"] = False + res["reason"] = ( + "profile system infeasible for every attainable rho square sum: " + "no integer character profile satisfies parity, |rho_hat| <= E_o, " + "the even-half bound and Parseval simultaneously" + ) + return res + + +def witness_constraints_ok(A, B, n=7): + """Direct validation of every profile-system constraint on an actual + covering pair (A, B). Used as the soundness control: a real cover can + never violate a constraint the system uses.""" + N = 1 << n + half = 1 << (n - 1) + eo = len(A) * len(B) - half + if eo < 0: + return False + s, t = len(A), len(B) + # odd half: r = 1_A * 1_B >= 1 on O + r = [0] * N + for a in A: + for b in B: + r[a ^ b] += 1 + odds = [x for x in range(N) if dot(N - 1, x)] + if any(r[x] < 1 for x in odds): + return False + rho = {x: r[x] - 1 for x in odds if r[x] > 1} + if sum(rho.values()) != eo: + return False + # even half: A_x + B_x >= 1 on E \ {0} + pairA = Counter() + pairB = Counter() + for i in range(len(A)): + for j in range(i): + pairA[A[i] ^ A[j]] += 1 + for i in range(len(B)): + for j in range(i): + pairB[B[i] ^ B[j]] += 1 + evs = [x for x in range(N) if not dot(N - 1, x) and x != 0] + if any(pairA[x] + pairB[x] < 1 for x in evs): + return False + P = s * (s - 1) // 2 + t * (t - 1) // 2 + bound = s + t + 2 * P - N + # characters off {0, 1} + for u in range(N): + if u in (0, N - 1): + continue + f_hat = sum(1 - 2 * dot(u, a) for a in A) + g_hat = sum(1 - 2 * dot(u, b) for b in B) + if f_hat % 2 != s % 2 or g_hat % 2 != t % 2: + return False + rho_hat = sum(c * (1 - 2 * dot(u, x)) for x, c in rho.items()) + if f_hat * g_hat != rho_hat: + return False + if abs(rho_hat) > eo or rho_hat % 2 != eo % 2: + return False + if f_hat * f_hat + g_hat * g_hat > bound: + return False + return True + + +def squeeze_numbers(n, s, t): + """The PR 2870-style Parseval deficit bookkeeping for one split, extended + to equal parity: per-side remainders vs the strongest uniform character + bound the parity class allows.""" + eo = s * t - (1 << (n - 1)) + N = 1 << n + res = {"n": n, "split": (s, t), "odd_excess": eo} + if eo < 0: + res.update( + bounded_side=None, + parseval_remainder=None, + max_allowed=None, + deficit=None, + contradiction=True, + reason="counting: fewer cross pairs than odd masks", + ) + return res + opposite = (s % 2) != (t % 2) + sides = [] + for name, card, par in (("A", s, s % 2), ("B", t, t % 2)): + remainder = N * card - 2 * card * card + if opposite and par == 0: + max_char = 2 * (eo // 2) # largest even <= E_o + elif (not opposite) and par == 1: + max_char = eo if eo % 2 == 1 else eo - 1 # largest odd <= E_o + else: + max_char = None # side can vanish: no uniform bound + allowed = None if max_char is None else (N - 2) * max_char * max_char + deficit = None if allowed is None else remainder - allowed + sides.append( + dict( + side=name, + cardinality=card, + max_char=max_char, + parseval_remainder=remainder, + max_allowed=allowed, + deficit=deficit, + ) + ) + res["opposite_parity"] = opposite + res["sides"] = sides + if opposite: + bounded = next(x for x in sides if x["max_char"] is not None) + res.update( + bounded_side=bounded["side"], + parseval_remainder=bounded["parseval_remainder"], + max_allowed=bounded["max_allowed"], + deficit=bounded["deficit"], + contradiction=bounded["deficit"] > 0, + reason=( + "PR 2870 squeeze applies (opposite parity): %d > %d" + % (bounded["parseval_remainder"], bounded["max_allowed"]) + if bounded["deficit"] > 0 + else "PR 2870 squeeze applies but reaches no contradiction" + ), + ) + else: + res.update( + bounded_side=None, + parseval_remainder=None, + max_allowed=None, + deficit=None, + contradiction=False, + reason=( + "equal character parities (s+t even): PR 2870's squeeze " + "hypothesis fails for this split; see sides[] for the " + "equal-parity remainders vs bounds" + ), + ) + return res + + +# ------------------------------------------------------ pairing sums + + +def pairing_sums(da, db): + """All sums sum_i a_i b_{pi(i)} over bijections pi of two equal-length + multisets, by contingency-table enumeration (the vendored O(m!) loop + cannot run at 18-point row sizes).""" + ca = Counter(da) + cb = Counter(db) + va = sorted(ca) + vb = sorted(cb) + acounts = [ca[v] for v in va] + bcounts = [cb[v] for v in vb] + out = set() + + def rec(i, caps, acc): + if i == len(va): + if all(c == 0 for c in caps): + out.add(acc) + return + need = acounts[i] + va_i = va[i] + + def dist(j, remaining, add): + if j == len(vb) - 1: + if remaining <= caps[j]: + caps[j] -= remaining + rec(i + 1, caps, acc + add + va_i * vb[j] * remaining) + caps[j] += remaining + return + for take in range(min(caps[j], remaining) + 1): + caps[j] -= take + dist(j + 1, remaining - take, add + va_i * vb[j] * take) + caps[j] += take + + dist(0, need, 0) + + rec(0, list(bcounts), 0) + return out + + +@lru_cache(maxsize=None) +def _pairing_sums_cached(da, db): + return frozenset(pairing_sums(da, db)) + + +@lru_cache(maxsize=None) +def draw_multisets(shared, budget, min_excess=0): + """Deduped draws: multisets of `shared` values >= 1 with total excess + sum(v-1) in [min_excess, budget]. (Embeddable in some multiplicity shape + of support `shared` + complement with total excess `budget`.)""" + out = set() + + def rec(lo, remaining, excess_left, acc): + if remaining == 0: + out.add(tuple(sorted(acc))) + return + for v in range(lo, excess_left + 2): + new_left = excess_left - (v - 1) + if new_left < 0: + break + rec(v, remaining - 1, new_left, acc + [v]) + + for used in range(min_excess, budget + 1): + rec(1, shared, used, []) + return sorted(out) + + +def attainable_c_values(n, s, t, e_ex, b_ex, targets=None, cap=200000): + """Exact attainable c = sum_x A_x B_x on the shared support positions + (targets given: only membership in targets is decided). Returns + (values_or_flags, status) with status in {"exact", "capped"}.""" + odd_masks_n = 1 << (n - 1) + even_nonzero = odd_masks_n - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + shared = A + B - e_ex - b_ex - even_nonzero + if shared < 0: + return (set(), "exact") + if shared == 0: + return ({0}, "exact") + comp_a = A - e_ex - shared + comp_b = B - b_ex - shared + das = draw_multisets(shared, e_ex, e_ex if comp_a == 0 else 0) + dbs = draw_multisets(shared, b_ex, b_ex if comp_b == 0 else 0) + found = set() + steps = 0 + for da in das: + for db in dbs: + steps += 1 + if steps > cap: + return (found, "capped") + vals = _pairing_sums_cached(da, db) + if targets is not None: + found |= vals & set(targets) + else: + found |= vals + return (found, "exact") + + +# ------------------------------------------------------------ rows + + +def max_attain(e_ex, b_ex, shared): + """Largest attainable c for one row (rearrangement on the extreme draws).""" + if shared <= 0: + return 0 + return (e_ex + 1) * (b_ex + 1) + shared - 1 + + +def sharp_rows_fast(n, s, t, min_e_ex=0, min_b_ex=0, cap=200000): + """PR 2773's sharp pair-representation rows for one split, with census + floors applied. Row status: "sharp" (exact attainability computed), + "interval" (kept conservatively: exact check capped), "dead" (dropped).""" + odd_masks_n = 1 << (n - 1) + even_nonzero = odd_masks_n - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + excess = s * t - odd_masks_n + need = (excess + 1) // 2 if excess > 0 else 0 + c_vals = c17.profile_c_values(n, s, t) + rows = [] + best = -1 + capped_rows = 0 + if excess < 0 or A + B < even_nonzero: + return dict(feasible=False, rows=[], best=best, need=need, c_vals=c_vals) + for e_ex in range(min_e_ex, A + 1): + for b_ex in range(min_b_ex, B + 1): + shared = A + B - e_ex - b_ex - even_nonzero + if shared < 0: + continue + attain, status = attainable_c_values(n, s, t, e_ex, b_ex, cap=cap) + if status == "capped": + capped_rows += 1 + best = max(best, max_attain(e_ex, b_ex, shared)) + hits = [c for c in c_vals if c <= max_attain(e_ex, b_ex, shared)] + for c in hits: + rows.append( + dict(e_ex=e_ex, b_ex=b_ex, shared=shared, c=c, status="interval") + ) + continue + if not attain: + continue + best = max(best, max(attain)) + for c in sorted(set(attain) & set(c_vals)): + rows.append( + dict(e_ex=e_ex, b_ex=b_ex, shared=shared, c=c, status="sharp") + ) + return dict( + feasible=bool(rows), + rows=rows, + best=best, + need=need, + c_vals=c_vals, + capped_rows=capped_rows, + ) + + +def surviving_rows_fast(n, s, t, min_e_ex=0, min_b_ex=0): + return sharp_rows_fast(n, s, t, min_e_ex=min_e_ex, min_b_ex=min_b_ex) + + +# ------------------------------------------------------------- search + + +def _score_pair(A, D, ev_index): + """Coverage score of a candidate (A, D) pair over the even group: + |A + D| + |(A+A) u (D+D)|, target 128 (two sets of 64).""" + cross = set(a ^ d for a in A for d in D) + selfs = set(a ^ a2 for i, a in enumerate(A) for a2 in A[i:]) + selfs |= set(d ^ d2 for i, d in enumerate(D) for d2 in D[i:]) + return len(cross) + len(selfs) + + +def search_split(s, t, restarts=20, seed=1, seconds=20.0, n=7): + """Bounded seeded local search for a covering pair (A, D) in the even + group E =~ F2^6 with |A| = s, |D| = t (reduction lemma). A found pair is + a falsifying instance; otherwise a scoped search failure.""" + rng = random.Random(seed) + ev = even_masks(n) + pool = ev[:] + best = (0, None) + t0 = time.time() + moves = 0 + for _ in range(restarts): + if time.time() - t0 > seconds: + break + A = rng.sample(pool, s) + D = rng.sample(pool, t) + sc = _score_pair(A, D, None) + improved = True + while improved and time.time() - t0 < seconds: + improved = False + for side, size in ((0, s), (1, t)): + cur = A if side == 0 else D + outside = [x for x in pool if x not in cur] + for i in range(size): + for v in outside: + moves += 1 + old = cur[i] + cur[i] = v + new = _score_pair(A, D, None) + if new > sc: + sc = new + improved = True + outside[outside.index(v)] = old + if sc == 128: + return dict( + found=True, + score=128, + A=sorted(A), + D=sorted(D), + restarts=_, + moves=moves, + seconds=round(time.time() - t0, 2), + ) + else: + cur[i] = old + if sc > best[0]: + best = (sc, (sorted(A), sorted(D))) + return dict( + found=False, + score=best[0], + best_pair=best[1], + restarts=restarts, + moves=moves, + seconds=round(time.time() - t0, 2), + ) + + +def search_direct(k=18, restarts=30, seed=1, seconds=20.0, n=7): + """Bounded seeded local search for a k-point cover of F2^n directly + (0 in S, translation WLOG).""" + rng = random.Random(seed) + pool = list(range(1 << n)) + best = (0, None) + t0 = time.time() + for _ in range(restarts): + if time.time() - t0 > seconds: + break + S = [0] + rng.sample(pool[1:], k - 1) + sc = coverage_mask(S).bit_count() + improved = True + while improved and time.time() - t0 < seconds: + improved = False + outside = [x for x in pool if x not in S] + for i in range(1, k): + for v in outside: + old = S[i] + S[i] = v + new = coverage_mask(S).bit_count() + if new > sc: + sc = new + improved = True + outside[outside.index(v)] = old + if sc == (1 << n): + return dict( + found=True, + score=sc, + S=sorted(S), + seconds=round(time.time() - t0, 2), + ) + else: + S[i] = old + if sc > best[0]: + best = (sc, sorted(S)) + return dict( + found=False, + score=best[0], + best_set=best[1], + restarts=restarts, + seconds=round(time.time() - t0, 2), + ) diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/vendor/vanish.py b/research/f7-18point-tight-classes-seed4c1e7b30/vendor/vanish.py new file mode 100644 index 0000000000..2dca0053f3 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/vendor/vanish.py @@ -0,0 +1,604 @@ +"""KB3f engine: vanishing-character classification for the 18-point cover +question for F2^7 (set level; no words). + +Object (unchanged from PR 2911, which this package presses): in the PR943 +prefix-walk model a restored seven-source singleton word is universal exactly +when its prefix set P covers, P + P = F2^7. A parity split S = A u B has A in +the even coset E (s points), B in the odd coset O (t points), s + t = 18. +PR 2911 PROVED that any (12,6) or (10,8) cover must have a vanishing +character off the all-ones hyperplane; this module classifies those +vanishing configurations and tests each class against coverage of the +remaining masks. + +Everything is exact Python integer arithmetic; no floats are used. + +Conventions. The even coset E is identified with F2^6 (m = 6); a character +of E is nontrivial psi_v(x) = (-1)^(v.x), v in 1..2^m-1. The (A, D) +reduction (PR 2911, PROVEN there): fix an odd p in F2^7 and D = p + B inside +E; S covers iff (i) A + D = E and (ii) (A+A) u (D+D) = E. + +Classification lemmas (all machine-checked in test_engine.py): + +L2 (halving). char_sum(A, v) = 0 iff A splits |A|/2 + |A|/2 across + ker(psi_v); so a vanishing on side A needs s even and forces the split + (s/2, s/2), and on side D needs t even and forces (t/2, t/2). At + (11,7) and (9,9) both sides are odd: NO character can vanish there. + +L3 (half-decomposition). With H = ker(psi_v), H' = E \\ H and A = A0 u A1, + D = D0 u D1 the two sides of ker(psi_v), coverage is equivalent to + (A0+D0) u (A1+D1) = H, (A0+D1) u (A1+D0) = H', + (A0+A0) u (A1+A1) u (D0+D0) u (D1+D1) = H, (A0+A1) u (D0+D1) = H'. + +L4 (class floors, exact union-size bounds on L3). With a split (a0, a1) of + A and (d0, d1) of D across ker(psi_v), the H'-even line forces + (F1) a0*a1 + d0*d1 >= 2^(m-1); the H-even line forces + (F2) sum over the four parts p of (1 + C(p,2) if p >= 1 else 0) >= 2^(m-1); + the odd lines force (F3) a0*d0 + a1*d1 >= 2^(m-1) and + (F4) a0*d1 + a1*d0 >= 2^(m-1). A class whose forced splits violate any + floor is PROVEN impossible: no cover realizes it. + +A class = (vanishing side, forced split of the vanishing side, split of the +other side). class_table enumerates all classes of a split; classify_cover +decides the classes of a concrete cover; census_f4/census_f5 enumerate the +smallest covers as ground truth for which classes actually occur. +""" + +import hashlib +import itertools +import random +import time +from collections import Counter + + +# ---------------------------------------------------------- F2^n basics + + +def dot(x, y): + return (x & y).bit_count() & 1 + + +def char_sum(pts, v): + """sum over pts of (-1)^(v.x).""" + return sum(1 - 2 * dot(p, v) for p in pts) + + +def split_sizes(pts, v, n): + """(|pts int ker(psi_v)|, |pts \\ ker(psi_v)|).""" + h0 = sum(1 for p in pts if not dot(v, p)) + return (h0, len(pts) - h0) + + +def char_representatives(n): + """One representative per nontrivial character of E: min(v, v ^ all1).""" + all1 = (1 << n) - 1 + out = [] + for v in range(1, all1): + if v < (v ^ all1): + out.append(v) + return out + + +def vanishing_set(pts, n): + """Character-level vanishing set (one entry per nontrivial character).""" + return {v for v in char_representatives(n) if char_sum(pts, v) == 0} + + +def vanishing_set_u(pts, n): + """u-level vanishing set: all indices v off {0, all-ones} with sum 0.""" + all1 = (1 << n) - 1 + return {v for v in range(1, all1) if char_sum(pts, v) == 0} + + +def sumset_xor(x, y): + return {a ^ b for a in x for b in y} + + +def selfsum_xor(x): + return {a ^ b for i, a in enumerate(x) for b in x[i:]} + + +def covers_f2n(pts, n): + cov = selfsum_xor(pts) + return len(cov) == (1 << n) + + +def cover_conditions(A, D, m): + """(A + D = F2^m, (A+A) u (D+D) = F2^m) -- the (A, D) reduction.""" + full = set(range(1 << m)) + odd_ok = sumset_xor(A, D) == full + even_ok = selfsum_xor(A) | selfsum_xor(D) == full + return odd_ok, even_ok + + +# ------------------------------------------------- half decomposition + + +def half_conditions(A, D, v, m): + """The four half lines of L3 for character psi_v.""" + A0 = [a for a in A if not dot(v, a)] + A1 = [a for a in A if dot(v, a)] + D0 = [d for d in D if not dot(v, d)] + D1 = [d for d in D if dot(v, d)] + H = {x for x in range(1 << m) if not dot(v, x)} + Hp = {x for x in range(1 << m) if dot(v, x)} + od0 = sumset_xor(A0, D0) | sumset_xor(A1, D1) + od1 = sumset_xor(A0, D1) | sumset_xor(A1, D0) + ev0 = selfsum_xor(A0) | selfsum_xor(A1) | selfsum_xor(D0) | selfsum_xor(D1) + ev1 = sumset_xor(A0, A1) | sumset_xor(D0, D1) + return ( + H <= od0, + Hp <= od1, + H <= ev0, + Hp <= ev1, + (len(A0), len(A1), len(D0), len(D1)), + ) + + +def check_half_decomposition(m, exhaustive=True, samples=0, seed=1): + """Verify L2 and L3 on every (A, D) pair (m <= 3) or on random samples.""" + rng = random.Random(seed) + N = 1 << m + pairs = 0 + if exhaustive: + sets = [] + for mask in range(1 << N): + sets.append([x for x in range(N) if (mask >> x) & 1]) + iterator = itertools.product(sets, repeat=2) + else: + def rand_iter(): + for _ in range(samples): + A = [x for x in range(N) if rng.randrange(2)] + D = [x for x in range(N) if rng.randrange(2)] + yield (A, D) + iterator = rand_iter() + for A, D in iterator: + pairs += 1 + for v in range(1, N): + cs = char_sum(A, v) + a0, a1 = split_sizes(A, v, m) + l2 = (cs == 0) == (len(A) % 2 == 0 and a0 == len(A) // 2) + if not l2: + return dict(ok=False, pairs=pairs, fail="L2", A=A, D=D, v=v) + od0, od1, ev0, ev1, _ = half_conditions(A, D, v, m) + direct = cover_conditions(A, D, m) + if (od0 and od1 and ev0 and ev1) != all(direct): + return dict(ok=False, pairs=pairs, fail="L3", A=A, D=D, v=v) + return dict(ok=True, pairs=pairs) + + +def two_vanishing_structure(A, v1, v2, m): + """L5 (multi-vanishing structure). If char_sum(A, v1) = char_sum(A, v2) + = 0 for distinct characters, the counts of A across the four parts of the + (ker(psi_v1), ker(psi_v2)) grid are (x, y, y, x) with x + y = |A|/2. + Returns (counts, ok) where counts = (n00, n01, n10, n11) in the grid.""" + n00 = n01 = n10 = n11 = 0 + for a in A: + b1, b2 = dot(v1, a), dot(v2, a) + if b1 == 0 and b2 == 0: + n00 += 1 + elif b1 == 0: + n01 += 1 + elif b2 == 0: + n10 += 1 + else: + n11 += 1 + ok = n00 == n11 and n01 == n10 + return (n00, n01, n10, n11), ok + + +def check_multi_vanishing(m): + """Verify L5 for every subset A of F2^m and every vanishing pair.""" + N = 1 << m + checked = 0 + for mask in range(1 << N): + A = [x for x in range(N) if (mask >> x) & 1] + van = [v for v in range(1, N) if char_sum(A, v) == 0] + for i in range(len(van)): + for j in range(i): + counts, ok = two_vanishing_structure(A, van[j], van[i], m) + checked += 1 + if not ok: + return dict(ok=False, checked=checked, A=A, v=(van[j], van[i]), counts=counts) + return dict(ok=True, checked=checked) + + +def sidon_pair(X, Y): + """All |X|*|Y| sums x+y distinct (no nontrivial common difference).""" + return len(sumset_xor(X, Y)) == len(X) * len(Y) + + +def check_tight_equality(m): + """L7 (equality analysis of the F1 floor). Whenever a0*a1 + d0*d1 = + 2^(m-1) and the pair (A, D) covers, the H' even line forces + |A0+A1| = a0*a1 (a Sidon pair), |D0+D1| = d0*d1 (a Sidon pair), and the + two cross sumsets are disjoint (their union is H').""" + N = 1 << m + need = 1 << (m - 1) + checked = 0 + sets = [[x for x in range(N) if (mask >> x) & 1] for mask in range(1 << N)] + for A in sets: + for D in sets: + if not all(cover_conditions(A, D, m)): + continue + for v in range(1, N): + A0 = [a for a in A if not dot(v, a)] + A1 = [a for a in A if dot(v, a)] + D0 = [d for d in D if not dot(v, d)] + D1 = [d for d in D if dot(v, d)] + if len(A0) * len(A1) + len(D0) * len(D1) != need: + continue + checked += 1 + sA = sumset_xor(A0, A1) + sD = sumset_xor(D0, D1) + if len(sA) != len(A0) * len(A1): + return dict(ok=False, checked=checked, fail="A0+A1 not Sidon", A=A, D=D, v=v) + if len(sD) != len(D0) * len(D1): + return dict(ok=False, checked=checked, fail="D0+D1 not Sidon", A=A, D=D, v=v) + if sA & sD: + return dict(ok=False, checked=checked, fail="cross sumsets overlap", A=A, D=D, v=v) + return dict(ok=True, checked=checked) + + +# ------------------------------------------------------- class table + + +def _bound2(part): + return (1 + part * (part - 1) // 2) if part >= 1 else 0 + + +def class_table(s, t, m=6): + """All vanishing classes of the split (s, t) at E = F2^m and their floor + verdicts. A class: vanishing side A (forced split s/2 + s/2) with the + other side's split (d0, d1), or vanishing side D (forced t/2 + t/2) with + the other side's split (a0, a1). Verdict dead iff some exact floor of L4 + fails; survives-tight iff F1 holds with equality.""" + need = 1 << (m - 1) + out = {"split": (s, t), "m": m, "floor_need_F1": need, "vanishing_possible": False} + + def floors(a0, a1, d0, d1): + return { + "F1": a0 * a1 + d0 * d1, + "F2": _bound2(a0) + _bound2(a1) + _bound2(d0) + _bound2(d1), + "F3": a0 * d0 + a1 * d1, + "F4": a0 * d1 + a1 * d0, + } + + def entry(vanishing_side, van_split, other_split, a0, a1, d0, d1): + fl = floors(a0, a1, d0, d1) + ok = all(v >= need for v in fl.values()) + tight = ok and fl["F1"] == need + forced = None + if ok and tight: + forced = ( + "equality: |A0+A1| = a0*a1 and |D0+D1| = d0*d1 (both Sidon), " + "the two cross sumsets disjoint with union the whole odd half" + ) + elif ok and d0 * d1 == 0: + forced = "D cross sums empty: |A0+A1| = the whole odd half" + elif ok and a0 * a1 == 0: + forced = "A cross sums empty: |D0+D1| = the whole odd half" + return dict( + vanishing_side=vanishing_side, + vanishing_split=van_split, + other_split=other_split, + splits=dict(A=(a0, a1), D=(d0, d1)), + floors=fl, + floor_value=fl["F1"], + floor_need=need, + verdict=("survives" if ok else "dead"), + tight=tight, + forced=forced, + ) + + A_rows, D_rows = [], [] + if s % 2 == 0: + out["vanishing_possible"] = True + for d0 in range(t, (t - 1) // 2, -1): + d1 = t - d0 + A_rows.append(entry("A", (s // 2, s // 2), (d0, d1), s // 2, s // 2, d0, d1)) + if t % 2 == 0: + out["vanishing_possible"] = True + for a0 in range(s, (s - 1) // 2, -1): + a1 = s - a0 + D_rows.append(entry("D", (t // 2, t // 2), (a0, a1), a0, a1, t // 2, t // 2)) + out["A_vanish"] = A_rows + out["D_vanish"] = D_rows + return out + + +# ---------------------------------------------------- cover census + + +def classify_cover(S, n): + """Classify a covering set S of F2^n by its vanishing classes (ground + truth for 'which characters can vanish').""" + A = [x for x in S if x.bit_count() % 2 == 0] + B = [x for x in S if x.bit_count() % 2 == 1] + D = [1 ^ b for b in B] + m = n - 1 + need = 1 << (m - 1) + k_A = vanishing_set(A, n) + k_D = vanishing_set(D, n) + rows = [] + dead = [] + for v in sorted(k_A | k_D): + a0, a1 = split_sizes(A, v, n) + d0, d1 = split_sizes(D, v, n) + val = a0 * a1 + d0 * d1 + verdict = "survives" if val >= need else "dead" + side = ("A" if v in k_A else "") + ("D" if v in k_D else "") + rows.append((v, side, (a0, a1), (d0, d1), verdict)) + if verdict == "dead": + dead.append((v, side, (a0, a1), (d0, d1))) + return dict( + S=sorted(S), + split=(len(A), len(B)), + k_A=len(k_A), + k_D=len(k_D), + vanish_rows=rows, + dead_classes_hit=dead, + ) + + +def _aggregate(rec, agg, class_agg): + agg[("%d_%d" % rec["split"], rec["k_A"], rec["k_D"])] += 1 + for (v, side, a_sp, d_sp, verdict) in rec["vanish_rows"]: + class_agg[(side, a_sp, d_sp, verdict)] += 1 + + +def _ser_agg(agg): + return sorted(["%s kA=%d kD=%d" % k, v] for k, v in agg.items()) + + +def _ser_class_agg(class_agg): + return sorted( + ["%s a=%d,%d d=%d,%d %s" % (side, a_sp[0], a_sp[1], d_sp[0], d_sp[1], verdict), v] + for (side, a_sp, d_sp, verdict), v in class_agg.items() + ) + + +def census_f4(keep=100): + """Exhaustive: every subset S of F2^4 with S + S = F2^4, classified.""" + N = 16 + full = set(range(N)) + pair = [[0] * N for _ in range(N)] + for i in range(N): + for j in range(N): + pair[i][j] = i ^ j + agg = Counter() + class_agg = Counter() + covers = [] + covers_total = 0 + dead_hit = [] + for mask in range(1, 1 << N): + S = [x for x in range(N) if (mask >> x) & 1] + cov = {0} + for i in range(len(S)): + for j in range(i): + cov.add(pair[S[i]][S[j]]) + if cov != full: + continue + covers_total += 1 + rec = classify_cover(S, 4) + _aggregate(rec, agg, class_agg) + if rec["dead_classes_hit"]: + dead_hit.append(rec["dead_classes_hit"]) + if len(covers) < keep: + covers.append(S) + return dict( + covers_total=covers_total, + covers=covers, + agg=_ser_agg(agg), + class_agg=_ser_class_agg(class_agg), + dead_classes_hit=dead_hit, + ) + + +def census_f5(shard=0, shards=16, keep_covers=5, n=5, k=10, max_combos=None): + """Shard `shard` of the full k-subset census of F2^n (n = 5, k = 10): + every k-subset S with S + S = F2^n is classified by vanishing class. + Independent enumeration route (all C(32,10) combinations) for the + recorded PR 2773 n5 control value 99,200 ten-point covers. max_combos + truncates a shard (smoke tests only; a complete census passes None).""" + N = 1 << n + full = (1 << N) - 1 + pairbit = [[0] * N for _ in range(N)] + for i in range(N): + for j in range(N): + pairbit[i][j] = 1 << (i ^ j) + agg = Counter() + class_agg = Counter() + covers = [] + covers_total = 0 + dead_hit = [] + combos = 0 + for S in itertools.combinations(range(N), k): + if S[0] % shards != shard: + continue + combos += 1 + if max_combos is not None and combos > max_combos: + combos -= 1 + return dict( + shard=shard, + shards=shards, + status="partial", + combos=combos, + covers_total=covers_total, + covers=covers, + agg=_ser_agg(agg), + class_agg=_ser_class_agg(class_agg), + dead_classes_hit=dead_hit, + ) + cov = 1 + for i in range(k): + si = S[i] + row = pairbit[si] + for j in range(i): + cov |= row[S[j]] + if cov != full: + continue + covers_total += 1 + rec = classify_cover(list(S), n) + _aggregate(rec, agg, class_agg) + if rec["dead_classes_hit"]: + dead_hit.append(rec["dead_classes_hit"]) + if len(covers) < keep_covers: + covers.append(sorted(S)) + return dict( + shard=shard, + shards=shards, + status="complete", + combos=combos, + covers_total=covers_total, + covers=covers, + agg=_ser_agg(agg), + class_agg=_ser_class_agg(class_agg), + dead_classes_hit=dead_hit, + ) + + +# ------------------------------------------------- class-restricted search + + +def _score_pair(A, D): + """|A + D| + |(A+A) u (D+D)| as integer bitmasks (target 2^(m+1)).""" + cm = 1 + for a in A: + for d in D: + cm |= 1 << (a ^ d) + sm = 1 + for i, a in enumerate(A): + for b in A[i:]: + sm |= 1 << (a ^ b) + for i, d in enumerate(D): + for b in D[i:]: + sm |= 1 << (d ^ b) + return cm.bit_count() + sm.bit_count() + + +def search_class(s, t, side, other_split, restarts=20, seed=1, seconds=20.0, m=6): + """Bounded seeded local search for a covering (A, D) pair in E = F2^m + constrained to one vanishing class: psi = bit 0 (WLOG under GL(m, 2)), + the vanishing side split equally across ker(psi), the other side split + exactly `other_split`. A found pair is a falsifying instance for the + class contradiction and (at m = 6) an 18-point cover witness; a failed + bounded search is a scoped search failure, never an exclusion.""" + rng = random.Random(seed) + N = 1 << m + target = 2 * N + + if side == "A_vanish": + a_h0 = s // 2 + a_h1 = s // 2 + d_h0, d_h1 = other_split + else: + d_h0 = t // 2 + d_h1 = t // 2 + a_h0, a_h1 = other_split + half0 = [x for x in range(N) if not (x & 1)] + half1 = [x for x in range(N) if (x & 1)] + + def build(): + A = rng.sample(half0, a_h0) + rng.sample(half1, a_h1) + D = rng.sample(half0, d_h0) + rng.sample(half1, d_h1) + return A, D + + best = (0, None) + moves = 0 + t0 = time.time() + for _ in range(restarts): + if time.time() - t0 > seconds: + break + A, D = build() + sc = _score_pair(A, D) + improved = True + while improved and time.time() - t0 < seconds: + improved = False + for cur in (A, D): + for half in (half0, half1): + for i in range(len(cur)): + if (cur[i] & 1) != (half[0] & 1): + continue + for v in half: + if v in cur: + continue + moves += 1 + old = cur[i] + cur[i] = v + new = _score_pair(A, D) + if new > sc: + sc = new + improved = True + break + cur[i] = old + if sc == target: + break + if sc == target: + break + if sc == target: + break + if sc == target: + return dict( + found=True, + score=sc, + A=sorted(A), + D=sorted(D), + side=side, + other_split=other_split, + moves=moves, + seconds=round(time.time() - t0, 2), + ) + if sc > best[0]: + best = (sc, (sorted(A), sorted(D))) + return dict( + found=False, + score=best[0], + best_pair=best[1], + side=side, + other_split=other_split, + restarts=restarts, + moves=moves, + seconds=round(time.time() - t0, 2), + ) + + +def search_free(s, t, restarts=20, seed=1, seconds=20.0, m=6): + """Unconstrained bounded seeded search for a covering (A, D) pair in + E = F2^m (non-vacuity control for the class-restricted machinery).""" + rng = random.Random(seed) + N = 1 << m + target = 2 * N + pool = list(range(N)) + best = (0, None) + t0 = time.time() + for _ in range(restarts): + if time.time() - t0 > seconds: + break + A = rng.sample(pool, s) + D = rng.sample(pool, t) + sc = _score_pair(A, D) + improved = True + while improved and time.time() - t0 < seconds: + improved = False + for cur, size in ((A, s), (D, t)): + outside = [x for x in pool if x not in cur] + for i in range(size): + for v in outside: + old = cur[i] + cur[i] = v + new = _score_pair(A, D) + if new > sc: + sc = new + improved = True + outside[outside.index(v)] = old + if sc == target: + return dict(found=True, score=sc, A=sorted(A), D=sorted(D)) + else: + cur[i] = old + if sc > best[0]: + best = (sc, (sorted(A), sorted(D))) + return dict(found=False, score=best[0], best_pair=best[1]) + + +def sha256_file(path): + return hashlib.sha256(path.read_bytes()).hexdigest() diff --git a/research/f7-18point-tight-classes-seed4c1e7b30/verify.py b/research/f7-18point-tight-classes-seed4c1e7b30/verify.py new file mode 100644 index 0000000000..09f06884c3 --- /dev/null +++ b/research/f7-18point-tight-classes-seed4c1e7b30/verify.py @@ -0,0 +1,330 @@ +"""Registered replay for the KB3g package (tight-class resolution for the +18-point cover question for F2^7, set level; no words). + +Modes (each bounded; see VERIFY.json): + + quick byte pins, the exact Fourier contradiction for class (7,1), the + rho classification numbers, the empty Sidon 5-pair enumeration, + the m=4 brute-force control, the PR 2933 CLASS table incl. the + (7,1)/(8,2) 32=32 TIGHT lines and L7 m=3 cases=6720, the + PR 2870 OBSTRUCTION control (696/504/192), the F2^4 census, and + the heavy-anchor receipt totals. + marker PASS_TIGHT_QUICK + novanish reproduction of the load-bearing PR 2911 NOVANISH premise from + the byte-vendored PR 2911 engine. + marker PASS_TIGHT_NOVANISH + rows reproduction of the PR 2911 ROWS18 lines (808/501/251/196) and + the 17-point row controls. + marker PASS_TIGHT_ROWS + classes the tight-class decision receipts: class71 (0 pairs), class82 + (all equality configurations fail all three lines) and class60 + (complete D-side transversal walk), aggregated from + TIGHT-PROGRESS.json / TIGHT-C60-*.json. + marker PASS_TIGHT_CLASSES + anchors the two heavy PR 2773 anchor receipts (k10b3 = 149,990,400, + k11b4 = 0/0). Receipt validation of this package's own fresh + empty-receipt walk (recorded in ANCHOR-REPRO.json), not a + re-walk; run vendor/anchors.py or run_anchors_all-style loops to + recompute. + marker PASS_TIGHT_ANCHORS + +Everything is exact integer arithmetic (no floats). +""" + +import hashlib +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +sys.path.insert(0, str(HERE / "vendor")) + +import tight # noqa: E402 + +VENDOR_PINS = { + "vendor/agent64_cover17.py": ( + "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654" + ), + "vendor/agent64_search17.py": ( + "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674" + ), + "anchors.py": ( + "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7" + ), + "vendor/cover18.py": ( + "24c6a2f4911dc2d5de76972eb5ae93dc4e66d8fa1e904443de6d0638e70c0a04" + ), + "vendor/vanish.py": ( + "6c605c54074f725321c5d770d538a652bf7727598a128270831f92fe7b9746d9" + ), +} + +SPLITS = [(12, 6), (11, 7), (10, 8), (9, 9)] + + +def sha256_file(p): + return hashlib.sha256(Path(p).read_bytes()).hexdigest() + + +def check_pins(): + for rel, want in VENDOR_PINS.items(): + got = sha256_file(HERE / rel) + assert got == want, (rel, got, want) + print("PIN %s sha256=%s" % (rel, got[:16]), flush=True) + + +def mode_quick(): + t0 = time.time() + check_pins() + fid = tight.fourier_71_identity() + assert fid["m5_k5"]["contradiction"] is True + assert (fid["m5_k5"]["need"], fid["m5_k5"]["lower_bound"]) == (175, 239) + assert fid["m3_analogue_71"]["contradiction"] is False + print( + "FOURIER (7,1) need=%d lower=%d contradiction=%s" + % (fid["m5_k5"]["need"], fid["m5_k5"]["lower_bound"], fid["m5_k5"]["contradiction"]), + flush=True, + ) + print( + "FOURIER m4-analogue need=%d lower=%d contradiction=%s" + % ( + fid["m3_analogue_71"]["need"], + fid["m3_analogue_71"]["lower_bound"], + fid["m3_analogue_71"]["contradiction"], + ), + flush=True, + ) + rho = tight.rho_classification() + print("RHO surviving=%s dead=%s" % ( + rho["surviving"], + sorted(t["rho"] for t in rho["types"] if t["verdict"] == "DEAD"), + ), flush=True) + pairs = tight.class71_pairs() + assert len(pairs) == 0, len(pairs) + print("CLASS71 normalized Sidon 5-pairs=%d (class empty)" % len(pairs), flush=True) + rec = tight.control_m4_bruteforce() + assert rec["m4_class71_analogue"]["all_have_l7_structure"] in (True, None) + assert rec["m4_class82_analogue"]["all_have_l7_structure"] in (True, None) + print( + "CONTROL m4 analogues: (7,1) covers=%d all_l7=%s; (8,2) covers=%d" + % ( + rec["m4_class71_analogue"]["direct_covers"], + rec["m4_class71_analogue"]["all_have_l7_structure"], + rec["m4_class82_analogue"]["direct_covers"], + ), + flush=True, + ) + # PR 2933 class table incl. the 32=32 TIGHT lines (vendored engine) + import vanish + + for (s, t) in SPLITS: + tab = vanish.class_table(s, t, m=6) + for side in ("A_vanish", "D_vanish"): + for c in tab[side]: + print( + "CLASS (%d,%d) %s vanish_split=%s other=%s value=%d need=%d -> %s%s" + % ( + s, + t, + side, + c["vanishing_split"], + c["other_split"], + c["floor_value"], + c["floor_need"], + c["verdict"], + " TIGHT" if c["tight"] else "", + ), + flush=True, + ) + if not tab["vanishing_possible"]: + print( + "CLASS (%d,%d) NO VANISHING POSSIBLE (both sides odd): L2 blocks every character" + % (s, t), + flush=True, + ) + res7 = vanish.check_tight_equality(3) + assert res7["ok"], res7 + print("LEMMA tight-equality Sidon exhaustive m=3 cases=%d ok=true" % res7["checked"], flush=True) + assert res7["checked"] == 6720, res7 + rec4 = vanish.census_f4() + assert rec4["dead_classes_hit"] == [], rec4["dead_classes_hit"] + print("CENSUS f2^4 covers=%d (dead classes hit: none)" % rec4["covers_total"], flush=True) + assert rec4["covers_total"] == 41341, rec4["covers_total"] + # PR 2870 OBSTRUCTION control (vendored PR 2911 engine) + import cover18 as c18 + + sq = c18.squeeze_numbers(7, 11, 6) + assert (sq["parseval_remainder"], sq["max_allowed"], sq["deficit"]) == (696, 504, 192) + print("CONTROL PR2870 obstruction reproduced: parseval=696 allowed=504 deficit=192", flush=True) + # heavy-anchor receipts of this package's fresh empty-receipt walk + prog = json.loads((HERE / "ANCHOR-PROGRESS.json").read_text(encoding="utf-8")) + for mode, want_total in (("k10b3", {"3": 149990400}), ("k11b4", {})): + mrec = prog["modes"][mode] + assert mrec.get("complete"), mode + assert mrec["total_hist"] == want_total, (mode, mrec["total_hist"]) + print( + "ANCHORS receipts %s count=%d total_hist=%s shards=%d" + % (mode, sum(mrec["total_hist"].values()), mrec["total_hist"], len(mrec["shards"])), + flush=True, + ) + print("PASS_TIGHT_QUICK seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_novanish(): + t0 = time.time() + check_pins() + import cover18 as c18 + + for (s, t) in ((12, 6), (10, 8)): + rec = c18.fourier_profile_feasibility(7, s, t, nonzero_both=True) + print( + "NOVANISH (%d, %d) feasible=%s capped=%s -> %s" + % ( + s, + t, + rec["feasible"], + rec.get("capped"), + "PROVEN every (s,t) cover has a vanishing character off {0,1}" + if not rec["feasible"] + else "no constraint", + ), + flush=True, + ) + assert rec["feasible"] is False, (s, t, rec) + print("PASS_TIGHT_NOVANISH seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_rows(): + t0 = time.time() + check_pins() + import cover18 as c18 + + FLOORS = {12: 3, 11: 5, 10: 3, 9: 0} + want = {(12, 6): 808, (11, 7): 501, (10, 8): 251, (9, 9): 196} + for (s, t) in SPLITS: + rows = c18.sharp_rows_fast(7, s, t, min_e_ex=FLOORS[s], min_b_ex=0) + eb = sorted({(r["e_ex"], r["b_ex"]) for r in rows["rows"]}) + print( + "ROWS18 (%d, %d) rows=%d distinct_eb=%d best=%d need=%d c_vals=%d floors=(e>=%d, b>=%d)" + % ( + s, + t, + len(rows["rows"]), + len(eb), + rows["best"], + rows["need"], + len(rows["c_vals"]), + FLOORS[s], + 0, + ), + flush=True, + ) + assert len(rows["rows"]) == want[(s, t)], (s, t, len(rows["rows"])) + rows = c18.surviving_rows_fast(7, 11, 6, min_e_ex=5, min_b_ex=0) + got = sorted((r["e_ex"], r["b_ex"]) for r in rows["rows"]) + assert got == [(5, 1), (6, 0)], got + rows = c18.surviving_rows_fast(7, 10, 7, min_e_ex=3, min_b_ex=0) + assert rows["rows"] == [] + print( + "CONTROL 17-point rows reproduce: (11,6) remainder (5,1),(6,0); (10,7) empty after floor", + flush=True, + ) + print("PASS_TIGHT_ROWS seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_classes(): + t0 = time.time() + check_pins() + prog = json.loads((HERE / "TIGHT-PROGRESS.json").read_text(encoding="utf-8")) + m71 = prog["modes"]["class71"]["shards"]["0"] + assert m71.get("complete"), m71 + assert m71["normalized_pairs"] == 0 and m71["covering_pairs"] == 0, m71 + print( + "CLASS71 normalized_pairs=%d covering_pairs=%d (PROVEN empty; Fourier need=175 < lower=239)" + % (m71["normalized_pairs"], m71["covering_pairs"]), + flush=True, + ) + m82 = prog["modes"]["class82"] + assert m82.get("complete"), "class82 incomplete" + tot = m82["total"] + assert tot["covering_configs"] == 0, tot + print( + "CLASS82 normalized_sidon_pairs=%d noninv=%d checked=%d covering=%d fail_hist=%s" + % ( + tot["normalized_sidon_pairs"], + tot["non_1_invariant_pairs"], + tot["checked"], + tot["covering_configs"], + tot["fail_hist"], + ), + flush=True, + ) + m60 = prog["modes"]["class60"] + assert m60.get("complete"), "class60 incomplete" + tot = m60["total"] + assert tot["covering_triples"] == 0, tot + print( + "CLASS60 d_checked=%d d_with_transversals=%d transversals=%d covering_triples=%d" + % ( + tot["d_checked"], + tot["d_with_transversals"], + tot["transversals_total"], + tot["covering_triples"], + ), + flush=True, + ) + for (s, t) in ((11, 7), (9, 9)): + rec = tight.identity_odd_sides(s, t) + print( + "IDENTITY (%d,%d) excess=%d sum_rho2_min=%d sum_rho2_max=%d contradiction=%s" + % ( + s, + t, + rec["excess"], + rec["sum_rho2_min"], + rec["sum_rho2_max"], + rec["contradiction"], + ), + flush=True, + ) + print("PASS_TIGHT_CLASSES seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_anchors(): + t0 = time.time() + check_pins() + prog = json.loads((HERE / "ANCHOR-PROGRESS.json").read_text(encoding="utf-8")) + for mode, want_total in (("k10b3", {"3": 149990400}), ("k11b4", {})): + mrec = prog["modes"][mode] + assert mrec.get("complete"), mode + assert mrec["total_hist"] == want_total, (mode, mrec["total_hist"]) + assert len(mrec["shards"]) == 62, (mode, len(mrec["shards"])) + print( + "ANCHORS %s count=%d total_hist=%s shards=%d (receipt validation of the fresh walk)" + % (mode, sum(mrec["total_hist"].values()), mrec["total_hist"], len(mrec["shards"])), + flush=True, + ) + print("PASS_TIGHT_ANCHORS seconds=%.1f" % (time.time() - t0), flush=True) + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + mode = sys.argv[1] if len(sys.argv) > 1 else "quick" + if mode == "quick": + mode_quick() + elif mode == "novanish": + mode_novanish() + elif mode == "rows": + mode_rows() + elif mode == "classes": + mode_classes() + elif mode == "anchors": + mode_anchors() + else: + raise SystemExit("usage: verify.py quick|novanish|rows|classes|anchors") + + +if __name__ == "__main__": + main()