diff --git a/research/f7-18point-vanishing-seedfc618722/ANCHOR-PROGRESS.json b/research/f7-18point-vanishing-seedfc618722/ANCHOR-PROGRESS.json new file mode 100644 index 0000000000..50cec35c43 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/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": 144.21 + }, + "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": 118.5 + }, + "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": 127.82 + }, + "v0=17": { + "examples": { + "3": [ + 0, + 3, + 17, + 18, + 20, + 24, + 33, + 46, + 65, + 92 + ] + }, + "hist": { + "3": 8782848 + }, + "seconds": 89.68 + }, + "v0=18": { + "examples": { + "3": [ + 0, + 3, + 18, + 20, + 23, + 24, + 33, + 40, + 65, + 92 + ] + }, + "hist": { + "3": 8455680 + }, + "seconds": 65.33 + }, + "v0=20": { + "examples": { + "3": [ + 0, + 3, + 20, + 23, + 24, + 29, + 33, + 39, + 65, + 80 + ] + }, + "hist": { + "3": 6200832 + }, + "seconds": 52.87 + }, + "v0=23": { + "examples": { + "3": [ + 0, + 3, + 23, + 24, + 27, + 29, + 33, + 40, + 65, + 80 + ] + }, + "hist": { + "3": 5956608 + }, + "seconds": 49.23 + }, + "v0=24": { + "examples": { + "3": [ + 0, + 3, + 24, + 27, + 29, + 33, + 40, + 65, + 75, + 101 + ] + }, + "hist": { + "3": 4402176 + }, + "seconds": 38.74 + }, + "v0=27": { + "examples": { + "3": [ + 0, + 3, + 27, + 29, + 30, + 33, + 40, + 65, + 75, + 101 + ] + }, + "hist": { + "3": 4217856 + }, + "seconds": 35.86 + }, + "v0=29": { + "examples": { + "3": [ + 0, + 3, + 29, + 30, + 33, + 36, + 40, + 46, + 65, + 80 + ] + }, + "hist": { + "3": 3225600 + }, + "seconds": 28.79 + }, + "v0=30": { + "examples": { + "3": [ + 0, + 3, + 30, + 33, + 34, + 36, + 40, + 48, + 65, + 78 + ] + }, + "hist": { + "3": 3078144 + }, + "seconds": 27.06 + }, + "v0=33": { + "examples": { + "3": [ + 0, + 3, + 33, + 34, + 36, + 40, + 48, + 63, + 65, + 108 + ] + }, + "hist": { + "3": 2860032 + }, + "seconds": 24.62 + }, + "v0=34": { + "examples": { + "3": [ + 0, + 3, + 34, + 36, + 39, + 40, + 48, + 57, + 65, + 108 + ] + }, + "hist": { + "3": 2736384 + }, + "seconds": 22.38 + }, + "v0=36": { + "examples": { + "3": [ + 0, + 3, + 36, + 39, + 40, + 45, + 48, + 54, + 65, + 96 + ] + }, + "hist": { + "3": 1930752 + }, + "seconds": 17.16 + }, + "v0=39": { + "examples": { + "3": [ + 0, + 3, + 39, + 40, + 43, + 45, + 48, + 57, + 65, + 96 + ] + }, + "hist": { + "3": 1837824 + }, + "seconds": 16.18 + }, + "v0=40": { + "examples": { + "3": [ + 0, + 3, + 40, + 43, + 45, + 48, + 57, + 65, + 75, + 116 + ] + }, + "hist": { + "3": 1306368 + }, + "seconds": 11.85 + }, + "v0=43": { + "examples": { + "3": [ + 0, + 3, + 43, + 45, + 46, + 48, + 57, + 65, + 75, + 116 + ] + }, + "hist": { + "3": 1234944 + }, + "seconds": 10.53 + }, + "v0=45": { + "examples": { + "3": [ + 0, + 3, + 45, + 46, + 48, + 53, + 57, + 63, + 65, + 96 + ] + }, + "hist": { + "3": 917760 + }, + "seconds": 8.75 + }, + "v0=46": { + "examples": { + "3": [ + 0, + 3, + 46, + 48, + 51, + 53, + 57, + 65, + 78, + 101 + ] + }, + "hist": { + "3": 858624 + }, + "seconds": 7.45 + }, + "v0=48": { + "examples": { + "3": [ + 0, + 3, + 48, + 51, + 53, + 57, + 65, + 78, + 80, + 108 + ] + }, + "hist": { + "3": 609792 + }, + "seconds": 5.25 + }, + "v0=5": { + "examples": { + "3": [ + 0, + 3, + 5, + 6, + 9, + 17, + 33, + 58, + 65, + 92 + ] + }, + "hist": { + "3": 19353600 + }, + "seconds": 184.34 + }, + "v0=51": { + "examples": { + "3": [ + 0, + 3, + 51, + 53, + 54, + 57, + 65, + 72, + 80, + 108 + ] + }, + "hist": { + "3": 562176 + }, + "seconds": 4.84 + }, + "v0=53": { + "examples": { + "3": [ + 0, + 3, + 53, + 54, + 57, + 60, + 65, + 71, + 80, + 96 + ] + }, + "hist": { + "3": 457728 + }, + "seconds": 3.64 + }, + "v0=54": { + "examples": { + "3": [ + 0, + 3, + 54, + 57, + 58, + 60, + 65, + 72, + 80, + 96 + ] + }, + "hist": { + "3": 413184 + }, + "seconds": 3.57 + }, + "v0=57": { + "examples": { + "3": [ + 0, + 3, + 57, + 58, + 65, + 68, + 72, + 78, + 80, + 96 + ] + }, + "hist": { + "3": 340992 + }, + "seconds": 2.73 + }, + "v0=58": { + "examples": { + "3": [ + 0, + 3, + 58, + 60, + 65, + 66, + 72, + 77, + 80, + 96 + ] + }, + "hist": { + "3": 297984 + }, + "seconds": 2.39 + }, + "v0=6": { + "examples": { + "3": [ + 0, + 3, + 6, + 9, + 10, + 17, + 33, + 53, + 65, + 92 + ] + }, + "hist": { + "3": 18708480 + }, + "seconds": 209.41 + }, + "v0=60": { + "examples": { + "3": [ + 0, + 3, + 60, + 63, + 65, + 68, + 72, + 78, + 80, + 96 + ] + }, + "hist": { + "3": 258048 + }, + "seconds": 1.9 + }, + "v0=63": { + "examples": { + "3": [ + 0, + 3, + 63, + 65, + 66, + 68, + 72, + 80, + 95, + 101 + ] + }, + "hist": { + "3": 215040 + }, + "seconds": 1.57 + }, + "v0=65": { + "examples": { + "3": [ + 0, + 3, + 65, + 68, + 72, + 77, + 80, + 86, + 96, + 106 + ] + }, + "hist": { + "3": 80640 + }, + "seconds": 1.22 + }, + "v0=66": { + "examples": { + "3": [ + 0, + 3, + 66, + 68, + 72, + 77, + 80, + 85, + 96, + 123 + ] + }, + "hist": { + "3": 80640 + }, + "seconds": 1.08 + }, + "v0=68": { + "examples": { + "3": [ + 0, + 3, + 68, + 72, + 77, + 80, + 85, + 90, + 96, + 102 + ] + }, + "hist": { + "3": 43008 + }, + "seconds": 0.71 + }, + "v0=71": { + "examples": { + "3": [ + 0, + 3, + 71, + 72, + 77, + 80, + 85, + 89, + 96, + 102 + ] + }, + "hist": { + "3": 43008 + }, + "seconds": 0.63 + }, + "v0=72": { + "examples": { + "3": [ + 0, + 3, + 72, + 77, + 80, + 85, + 89, + 95, + 96, + 123 + ] + }, + "hist": { + "3": 21504 + }, + "seconds": 0.4 + }, + "v0=75": { + "examples": { + "3": [ + 0, + 3, + 75, + 77, + 80, + 85, + 89, + 92, + 96, + 106 + ] + }, + "hist": { + "3": 21504 + }, + "seconds": 0.33 + }, + "v0=77": { + "examples": { + "3": [ + 0, + 3, + 77, + 80, + 85, + 89, + 95, + 96, + 101, + 123 + ] + }, + "hist": { + "3": 10368 + }, + "seconds": 0.23 + }, + "v0=78": { + "examples": { + "3": [ + 0, + 3, + 78, + 80, + 85, + 89, + 95, + 96, + 101, + 120 + ] + }, + "hist": { + "3": 10368 + }, + "seconds": 0.19 + }, + "v0=80": { + "examples": { + "3": [ + 0, + 3, + 80, + 85, + 89, + 92, + 96, + 102, + 113, + 123 + ] + }, + "hist": { + "3": 3840 + }, + "seconds": 0.1 + }, + "v0=83": { + "examples": { + "3": [ + 0, + 3, + 83, + 85, + 89, + 95, + 96, + 101, + 113, + 120 + ] + }, + "hist": { + "3": 3840 + }, + "seconds": 0.07 + }, + "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.03 + }, + "v0=89": { + "examples": { + "3": [ + 0, + 3, + 89, + 92, + 96, + 102, + 105, + 111, + 113, + 123 + ] + }, + "hist": { + "3": 384 + }, + "seconds": 0.02 + }, + "v0=9": { + "examples": { + "3": [ + 0, + 3, + 9, + 10, + 12, + 17, + 33, + 53, + 65, + 86 + ] + }, + "hist": { + "3": 14923776 + }, + "seconds": 157.95 + }, + "v0=90": { + "examples": { + "3": [ + 0, + 3, + 90, + 92, + 96, + 101, + 105, + 108, + 113, + 123 + ] + }, + "hist": { + "3": 384 + }, + "seconds": 0.02 + }, + "v0=92": { + "examples": {}, + "hist": {}, + "seconds": 0.02 + }, + "v0=95": { + "examples": {}, + "hist": {}, + "seconds": 0.01 + }, + "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": 227.85 + }, + "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": 184.11 + }, + "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": 182.35 + }, + "v0=17": { + "examples": {}, + "hist": {}, + "seconds": 138.76 + }, + "v0=18": { + "examples": {}, + "hist": {}, + "seconds": 128.92 + }, + "v0=20": { + "examples": {}, + "hist": {}, + "seconds": 93.67 + }, + "v0=23": { + "examples": {}, + "hist": {}, + "seconds": 80.18 + }, + "v0=24": { + "examples": {}, + "hist": {}, + "seconds": 87.99 + }, + "v0=27": { + "examples": {}, + "hist": {}, + "seconds": 75.39 + }, + "v0=29": { + "examples": {}, + "hist": {}, + "seconds": 39.4 + }, + "v0=30": { + "examples": {}, + "hist": {}, + "seconds": 36.33 + }, + "v0=33": { + "examples": {}, + "hist": {}, + "seconds": 32.09 + }, + "v0=34": { + "examples": {}, + "hist": {}, + "seconds": 47.49 + }, + "v0=36": { + "examples": {}, + "hist": {}, + "seconds": 25.24 + }, + "v0=39": { + "examples": {}, + "hist": {}, + "seconds": 21.02 + }, + "v0=40": { + "examples": {}, + "hist": {}, + "seconds": 13.84 + }, + "v0=43": { + "examples": {}, + "hist": {}, + "seconds": 13.93 + }, + "v0=45": { + "examples": {}, + "hist": {}, + "seconds": 9.65 + }, + "v0=46": { + "examples": {}, + "hist": {}, + "seconds": 8.72 + }, + "v0=48": { + "examples": {}, + "hist": {}, + "seconds": 6.17 + }, + "v0=5": { + "examples": {}, + "hist": {}, + "seconds": 312.21 + }, + "v0=51": { + "examples": {}, + "hist": {}, + "seconds": 6.11 + }, + "v0=53": { + "examples": {}, + "hist": {}, + "seconds": 4.43 + }, + "v0=54": { + "examples": {}, + "hist": {}, + "seconds": 3.69 + }, + "v0=57": { + "examples": {}, + "hist": {}, + "seconds": 2.85 + }, + "v0=58": { + "examples": {}, + "hist": {}, + "seconds": 2.59 + }, + "v0=6": { + "examples": {}, + "hist": {}, + "seconds": 207.78 + }, + "v0=60": { + "examples": {}, + "hist": {}, + "seconds": 1.95 + }, + "v0=63": { + "examples": {}, + "hist": {}, + "seconds": 1.68 + }, + "v0=65": { + "examples": {}, + "hist": {}, + "seconds": 1.05 + }, + "v0=66": { + "examples": {}, + "hist": {}, + "seconds": 0.95 + }, + "v0=68": { + "examples": {}, + "hist": {}, + "seconds": 0.59 + }, + "v0=71": { + "examples": {}, + "hist": {}, + "seconds": 0.59 + }, + "v0=72": { + "examples": {}, + "hist": {}, + "seconds": 0.31 + }, + "v0=75": { + "examples": {}, + "hist": {}, + "seconds": 0.29 + }, + "v0=77": { + "examples": {}, + "hist": {}, + "seconds": 0.16 + }, + "v0=78": { + "examples": {}, + "hist": {}, + "seconds": 0.14 + }, + "v0=80": { + "examples": {}, + "hist": {}, + "seconds": 0.06 + }, + "v0=83": { + "examples": {}, + "hist": {}, + "seconds": 0.05 + }, + "v0=85": { + "examples": {}, + "hist": {}, + "seconds": 0.03 + }, + "v0=86": { + "examples": {}, + "hist": {}, + "seconds": 0.02 + }, + "v0=89": { + "examples": {}, + "hist": {}, + "seconds": 0.02 + }, + "v0=9": { + "examples": {}, + "hist": {}, + "seconds": 171.65 + }, + "v0=90": { + "examples": {}, + "hist": {}, + "seconds": 0.02 + }, + "v0=92": { + "examples": {}, + "hist": {}, + "seconds": 0.02 + }, + "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-vanishing-seedfc618722/ANCHOR-REPRO.json b/research/f7-18point-vanishing-seedfc618722/ANCHOR-REPRO.json new file mode 100644 index 0000000000..b40bc92718 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/ANCHOR-REPRO.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "session": "KB3f vanishing-character classification (research/f7-18point-vanishing-seedfc618722)", + "receipt_validation_correction": "The extracted PR 2911 package's verify.py quick prints 'ANCHORS receipts ... shards=62' from its COMMITTED ANCHOR-PROGRESS.json: that line is receipt validation, not recomputation (its own ANCHOR-REPRO.json records the same correction for PR 2870's package). This package's heavy anchors were re-walked by the byte-vendored anchors.py driver from an EMPTY receipt file (run_anchors_all.py printed 'ANCHORS_RUNNER fresh receipts confirmed'); the committed ANCHOR-PROGRESS.json in this package is the receipt of that walk. A replay against the committed receipt is validation again; deleting ANCHOR-PROGRESS.json and re-invoking anchors.py proves recomputation.", + "recorded_anchor_values": { + "k10_budget3": 149990400, + "k11_level3": 0, + "k11_level4": 0, + "l18_nodes": 15775992, + "l18_cycles": 312064, + "l18_universal": 0, + "tier_n5_l10": [945, 31], + "tier_n6_l12": [10395, 49], + "tier_n6_l14": [945945, 59], + "n5_covers_through_0": 99200 + }, + "reproductions": [ + { + "anchor": "PR 2542/2634 REPRO tiers (945/31, 10395/49, 945945/59, records SHA-256), PR 2542 length-18 census (15,775,992 nodes, 312,064 cycles, 0 universal), PR 2773 row remainder (5,1),(6,0), n=5 set controls (0 nine-point covers max 29, 99,200 ten-point covers), vendored small-group control 420/840/168", + "command": "python3.12 -I -B research/f7-17point-cover-audit-seedcfa215c2/verify.py", + "observed_marker": "PASS_17POINT_VERIFY seconds=99.5 full=False", + "status": "recomputed in full (not receipt validation)" + }, + { + "anchor": "PR 2870 OBSTRUCTION parseval=696 allowed=504 deficit=192 (both parity orders), rows remainder (5,1),(6,0) from the vendored engine", + "command": "python3.12 -I -B research/f7-17point-fourier-obstruction-seedb5e318fe/verify.py", + "observed_marker": "PASS_FOURIER_VERIFY seconds=0.0", + "status": "recomputed in full" + }, + { + "anchor": "PR 2911 SQUEEZE table (12,6) 1248/696, (11,7) 1166/798 vs 21294, (10,8) 1080/896, (9,9) 990/990 vs 36414; PR 2870 obstruction control", + "command": "python3.12 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py quick", + "observed_marker": "PASS_F7_18POINT_QUICK seconds=0.0", + "status": "recomputed (the ANCHORS receipts lines in this run are receipt validation of PR 2911's committed walk, see receipt_validation_correction)" + }, + { + "anchor": "PR 2911 PROFILE18 spectra 16/22/50/31 and NOVANISH lines ((12,6),(10,8) infeasible; vanishing forced)", + "command": "python3.12 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py fourier", + "observed_marker": "PASS_F7_18POINT_FOURIER seconds=571.0", + "status": "recomputed in full" + }, + { + "anchor": "PR 2911 ROWS18 808/501/251/196 and the 17-point row controls", + "command": "python3.12 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py rows", + "observed_marker": "PASS_F7_18POINT_ROWS seconds=0.3", + "status": "recomputed in full" + }, + { + "anchor": "PR 2911 NOVANISH premise, from this package's byte-vendored cover18.py (pin 24c6a2f4...)", + "command": "python3.12 -I -B research/f7-18point-vanishing-seedfc618722/verify.py novanish", + "observed_marker": "PASS_F7_18POINT_NOVANISH seconds=0.2", + "status": "recomputed in full" + }, + { + "anchor": "PR 2773 k10 budget-3 = 149,990,400", + "command": "python3.12 -I -B research/f7-18point-vanishing-seedfc618722/anchors.py k10b3 (repeatedly, via run_anchors_all.py)", + "observed_marker": "PASS_ANCHORS_K10B3 count=149990400 total_hist={'3': 149990400} shards=62", + "status": "re-walked in full from EMPTY receipts (62/62 sub-shards, per-sub-shard receipts in ANCHOR-PROGRESS.json)" + }, + { + "anchor": "PR 2773 k11 levels 3-4 = 0, 0", + "command": "python3.12 -I -B research/f7-18point-vanishing-seedfc618722/anchors.py k11b4 (repeatedly, via run_anchors_all.py)", + "observed_marker": "PASS_ANCHORS_K11B4 count=0 total_hist={} shards=62", + "status": "re-walked in full from EMPTY receipts (62/62 sub-shards)" + }, + { + "anchor": "PR 2773 n5 control: 99,200 ten-point covers of F2^5", + "command": "python3.12 -I -B research/f7-18point-vanishing-seedfc618722/verify.py classify (via run_classify_all.py, empty CENSUS-PROGRESS.json)", + "observed_marker": "CONTROL PR2773 n5 control value reproduced: 99200 ten-point covers through {0} (all translations 317440 = 99200 * 32 / 10); PASS_F7_18POINT_CLASSIFY seconds=329.3", + "status": "recomputed independently: this enumeration walks all C(32,10) = 64,512,240 ten-sets with no fixed element; the {0}-slice (shard 0) is exactly PR 2773's fixed-0 value 99,200 and the un-normalized total is 317,440 = 99,200 * 32 / 10 (translation orbits have length 32 and each cover has 10 points)" + } + ] +} diff --git a/research/f7-18point-vanishing-seedfc618722/CENSUS-PROGRESS.json b/research/f7-18point-vanishing-seedfc618722/CENSUS-PROGRESS.json new file mode 100644 index 0000000000..8c2ced5aa8 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/CENSUS-PROGRESS.json @@ -0,0 +1,2296 @@ +{ + "complete": true, + "shards": { + "0": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 1920 + ], + [ + "4_6 kA=12 kD=0", + 8960 + ], + [ + "4_6 kA=6 kD=6", + 26880 + ], + [ + "6_4 kA=0 kD=12", + 13440 + ], + [ + "6_4 kA=6 kD=6", + 40320 + ], + [ + "8_2 kA=7 kD=8", + 7680 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 960 + ], + [ + "A a=1,1 d=3,5 survives", + 6720 + ], + [ + "A a=1,1 d=5,3 survives", + 6720 + ], + [ + "A a=1,1 d=7,1 survives", + 960 + ], + [ + "A a=2,2 d=2,4 survives", + 134400 + ], + [ + "A a=2,2 d=4,2 survives", + 134400 + ], + [ + "A a=3,3 d=1,3 survives", + 120960 + ], + [ + "A a=3,3 d=3,1 survives", + 120960 + ], + [ + "A a=4,4 d=0,2 survives", + 26880 + ], + [ + "A a=4,4 d=2,0 survives", + 26880 + ], + [ + "D a=1,3 d=3,3 survives", + 40320 + ], + [ + "D a=1,7 d=1,1 survives", + 960 + ], + [ + "D a=2,0 d=4,4 survives", + 13440 + ], + [ + "D a=2,4 d=2,2 survives", + 134400 + ], + [ + "D a=3,1 d=3,3 survives", + 120960 + ], + [ + "D a=3,5 d=1,1 survives", + 20160 + ], + [ + "D a=4,2 d=2,2 survives", + 268800 + ], + [ + "D a=5,3 d=1,1 survives", + 33600 + ], + [ + "D a=7,1 d=1,1 survives", + 6720 + ] + ], + "combos": 20160075, + "covers": [ + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 16, + 31 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 17, + 30 + ], + [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 18, + 29 + ] + ], + "covers_total": 99200 + }, + "1": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 6720 + ], + [ + "4_6 kA=12 kD=0", + 10080 + ], + [ + "4_6 kA=6 kD=6", + 30240 + ], + [ + "6_4 kA=0 kD=12", + 5600 + ], + [ + "6_4 kA=6 kD=6", + 16800 + ], + [ + "8_2 kA=7 kD=8", + 960 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 840 + ], + [ + "A a=1,1 d=3,5 survives", + 17640 + ], + [ + "A a=1,1 d=5,3 survives", + 29400 + ], + [ + "A a=1,1 d=7,1 survives", + 5880 + ], + [ + "A a=2,2 d=2,4 survives", + 100800 + ], + [ + "A a=2,2 d=4,2 survives", + 201600 + ], + [ + "A a=3,3 d=1,3 survives", + 25200 + ], + [ + "A a=3,3 d=3,1 survives", + 75600 + ], + [ + "A a=4,4 d=2,0 survives", + 6720 + ], + [ + "D a=0,2 d=4,4 survives", + 26880 + ], + [ + "D a=1,3 d=3,3 survives", + 105840 + ], + [ + "D a=1,7 d=1,1 survives", + 840 + ], + [ + "D a=2,0 d=4,4 survives", + 20160 + ], + [ + "D a=2,4 d=2,2 survives", + 100800 + ], + [ + "D a=3,1 d=3,3 survives", + 75600 + ], + [ + "D a=3,5 d=1,1 survives", + 4200 + ], + [ + "D a=4,2 d=2,2 survives", + 67200 + ], + [ + "D a=5,3 d=1,1 survives", + 2520 + ], + [ + "D a=7,1 d=1,1 survives", + 120 + ] + ], + "combos": 14307150, + "covers": [ + [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 16, + 24 + ], + [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 17, + 25 + ], + [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 18, + 26 + ] + ], + "covers_total": 70400 + }, + "10": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 32 + ], + [ + "4_6 kA=12 kD=0", + 128 + ], + [ + "4_6 kA=6 kD=6", + 496 + ], + [ + "6_4 kA=0 kD=12", + 256 + ], + [ + "6_4 kA=6 kD=6", + 704 + ], + [ + "8_2 kA=7 kD=8", + 48 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 32 + ], + [ + "A a=1,1 d=3,5 survives", + 128 + ], + [ + "A a=1,1 d=5,3 survives", + 96 + ], + [ + "A a=2,2 d=2,4 survives", + 2672 + ], + [ + "A a=2,2 d=4,2 survives", + 1840 + ], + [ + "A a=3,3 d=1,3 survives", + 2320 + ], + [ + "A a=3,3 d=3,1 survives", + 1904 + ], + [ + "A a=4,4 d=0,2 survives", + 192 + ], + [ + "A a=4,4 d=2,0 survives", + 144 + ], + [ + "D a=0,2 d=4,4 survives", + 128 + ], + [ + "D a=1,3 d=3,3 survives", + 1648 + ], + [ + "D a=1,7 d=1,1 survives", + 48 + ], + [ + "D a=2,0 d=4,4 survives", + 96 + ], + [ + "D a=2,4 d=2,2 survives", + 4368 + ], + [ + "D a=3,1 d=3,3 survives", + 1328 + ], + [ + "D a=3,5 d=1,1 survives", + 192 + ], + [ + "D a=4,2 d=2,2 survives", + 2928 + ], + [ + "D a=5,3 d=1,1 survives", + 144 + ] + ], + "combos": 293930, + "covers": [ + [ + 10, + 11, + 12, + 13, + 16, + 17, + 18, + 22, + 24, + 29 + ], + [ + 10, + 11, + 12, + 13, + 16, + 17, + 18, + 22, + 25, + 28 + ], + [ + 10, + 11, + 12, + 13, + 16, + 17, + 18, + 22, + 26, + 31 + ] + ], + "covers_total": 1664 + }, + "11": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 32 + ], + [ + "4_6 kA=12 kD=0", + 160 + ], + [ + "4_6 kA=6 kD=6", + 368 + ], + [ + "6_4 kA=0 kD=12", + 32 + ], + [ + "6_4 kA=6 kD=6", + 160 + ], + [ + "8_2 kA=7 kD=8", + 16 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 32 + ], + [ + "A a=1,1 d=3,5 survives", + 128 + ], + [ + "A a=1,1 d=5,3 survives", + 96 + ], + [ + "A a=2,2 d=2,4 survives", + 2480 + ], + [ + "A a=2,2 d=4,2 survives", + 1648 + ], + [ + "A a=3,3 d=1,3 survives", + 528 + ], + [ + "A a=3,3 d=3,1 survives", + 432 + ], + [ + "A a=4,4 d=0,2 survives", + 64 + ], + [ + "A a=4,4 d=2,0 survives", + 48 + ], + [ + "D a=0,2 d=4,4 survives", + 128 + ], + [ + "D a=1,3 d=3,3 survives", + 1200 + ], + [ + "D a=1,7 d=1,1 survives", + 16 + ], + [ + "D a=2,0 d=4,4 survives", + 96 + ], + [ + "D a=2,4 d=2,2 survives", + 784 + ], + [ + "D a=3,1 d=3,3 survives", + 1008 + ], + [ + "D a=3,5 d=1,1 survives", + 64 + ], + [ + "D a=4,2 d=2,2 survives", + 560 + ], + [ + "D a=5,3 d=1,1 survives", + 48 + ] + ], + "combos": 167960, + "covers": [ + [ + 11, + 12, + 13, + 14, + 16, + 17, + 18, + 19, + 24, + 28 + ], + [ + 11, + 12, + 13, + 14, + 16, + 17, + 18, + 19, + 25, + 29 + ], + [ + 11, + 12, + 13, + 14, + 16, + 17, + 18, + 19, + 26, + 30 + ] + ], + "covers_total": 768 + }, + "12": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 16 + ], + [ + "4_6 kA=12 kD=0", + 32 + ], + [ + "4_6 kA=6 kD=6", + 208 + ], + [ + "6_4 kA=0 kD=12", + 96 + ], + [ + "6_4 kA=6 kD=6", + 272 + ], + [ + "8_2 kA=7 kD=8", + 16 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 16 + ], + [ + "A a=1,1 d=3,5 survives", + 64 + ], + [ + "A a=1,1 d=5,3 survives", + 48 + ], + [ + "A a=2,2 d=2,4 survives", + 960 + ], + [ + "A a=2,2 d=4,2 survives", + 672 + ], + [ + "A a=3,3 d=1,3 survives", + 896 + ], + [ + "A a=3,3 d=3,1 survives", + 736 + ], + [ + "A a=4,4 d=0,2 survives", + 64 + ], + [ + "A a=4,4 d=2,0 survives", + 48 + ], + [ + "D a=0,2 d=4,4 survives", + 64 + ], + [ + "D a=1,3 d=3,3 survives", + 704 + ], + [ + "D a=1,7 d=1,1 survives", + 16 + ], + [ + "D a=2,0 d=4,4 survives", + 48 + ], + [ + "D a=2,4 d=2,2 survives", + 1664 + ], + [ + "D a=3,1 d=3,3 survives", + 544 + ], + [ + "D a=3,5 d=1,1 survives", + 64 + ], + [ + "D a=4,2 d=2,2 survives", + 1120 + ], + [ + "D a=5,3 d=1,1 survives", + 48 + ] + ], + "combos": 92378, + "covers": [ + [ + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 20, + 24, + 31 + ], + [ + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 20, + 25, + 30 + ], + [ + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 20, + 26, + 29 + ] + ], + "covers_total": 640 + }, + "13": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 8 + ], + [ + "4_6 kA=12 kD=0", + 64 + ], + [ + "4_6 kA=6 kD=6", + 120 + ], + [ + "6_4 kA=6 kD=6", + 56 + ], + [ + "8_2 kA=7 kD=8", + 8 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 8 + ], + [ + "A a=1,1 d=3,5 survives", + 32 + ], + [ + "A a=1,1 d=5,3 survives", + 24 + ], + [ + "A a=2,2 d=2,4 survives", + 896 + ], + [ + "A a=2,2 d=4,2 survives", + 592 + ], + [ + "A a=3,3 d=1,3 survives", + 192 + ], + [ + "A a=3,3 d=3,1 survives", + 144 + ], + [ + "A a=4,4 d=0,2 survives", + 32 + ], + [ + "A a=4,4 d=2,0 survives", + 24 + ], + [ + "D a=0,2 d=4,4 survives", + 32 + ], + [ + "D a=1,3 d=3,3 survives", + 384 + ], + [ + "D a=1,7 d=1,1 survives", + 8 + ], + [ + "D a=2,0 d=4,4 survives", + 24 + ], + [ + "D a=2,4 d=2,2 survives", + 192 + ], + [ + "D a=3,1 d=3,3 survives", + 336 + ], + [ + "D a=3,5 d=1,1 survives", + 32 + ], + [ + "D a=4,2 d=2,2 survives", + 144 + ], + [ + "D a=5,3 d=1,1 survives", + 24 + ] + ], + "combos": 48620, + "covers": [ + [ + 13, + 14, + 16, + 17, + 20, + 21, + 24, + 25, + 28, + 30 + ], + [ + 13, + 14, + 16, + 17, + 20, + 21, + 24, + 25, + 29, + 31 + ], + [ + 13, + 14, + 16, + 17, + 20, + 21, + 24, + 26, + 28, + 29 + ] + ], + "covers_total": 256 + }, + "14": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 8 + ], + [ + "4_6 kA=6 kD=6", + 56 + ], + [ + "6_4 kA=6 kD=6", + 56 + ], + [ + "8_2 kA=7 kD=8", + 8 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 8 + ], + [ + "A a=1,1 d=3,5 survives", + 32 + ], + [ + "A a=1,1 d=5,3 survives", + 24 + ], + [ + "A a=2,2 d=2,4 survives", + 192 + ], + [ + "A a=2,2 d=4,2 survives", + 144 + ], + [ + "A a=3,3 d=1,3 survives", + 192 + ], + [ + "A a=3,3 d=3,1 survives", + 144 + ], + [ + "A a=4,4 d=0,2 survives", + 32 + ], + [ + "A a=4,4 d=2,0 survives", + 24 + ], + [ + "D a=0,2 d=4,4 survives", + 32 + ], + [ + "D a=1,3 d=3,3 survives", + 192 + ], + [ + "D a=1,7 d=1,1 survives", + 8 + ], + [ + "D a=2,0 d=4,4 survives", + 24 + ], + [ + "D a=2,4 d=2,2 survives", + 192 + ], + [ + "D a=3,1 d=3,3 survives", + 144 + ], + [ + "D a=3,5 d=1,1 survives", + 32 + ], + [ + "D a=4,2 d=2,2 survives", + 144 + ], + [ + "D a=5,3 d=1,1 survives", + 24 + ] + ], + "combos": 24310, + "covers": [ + [ + 14, + 15, + 16, + 18, + 20, + 22, + 24, + 26, + 28, + 31 + ], + [ + 14, + 15, + 16, + 18, + 20, + 22, + 24, + 26, + 29, + 30 + ], + [ + 14, + 15, + 16, + 18, + 20, + 22, + 24, + 27, + 28, + 30 + ] + ], + "covers_total": 128 + }, + "15": { + "agg": [], + "class_agg": [], + "combos": 11440, + "covers": [], + "covers_total": 0 + }, + "16": { + "agg": [], + "class_agg": [], + "combos": 5005, + "covers": [], + "covers_total": 0 + }, + "17": { + "agg": [], + "class_agg": [], + "combos": 2002, + "covers": [], + "covers_total": 0 + }, + "18": { + "agg": [], + "class_agg": [], + "combos": 715, + "covers": [], + "covers_total": 0 + }, + "19": { + "agg": [], + "class_agg": [], + "combos": 220, + "covers": [], + "covers_total": 0 + }, + "2": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 3584 + ], + [ + "4_6 kA=12 kD=0", + 6720 + ], + [ + "4_6 kA=6 kD=6", + 20160 + ], + [ + "6_4 kA=0 kD=12", + 4480 + ], + [ + "6_4 kA=6 kD=6", + 13440 + ], + [ + "8_2 kA=7 kD=8", + 896 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 3136 + ], + [ + "A a=1,1 d=3,5 survives", + 15680 + ], + [ + "A a=1,1 d=5,3 survives", + 9408 + ], + [ + "A a=1,1 d=7,1 survives", + 448 + ], + [ + "A a=2,2 d=2,4 survives", + 120960 + ], + [ + "A a=2,2 d=4,2 survives", + 80640 + ], + [ + "A a=3,3 d=1,3 survives", + 47040 + ], + [ + "A a=3,3 d=3,1 survives", + 33600 + ], + [ + "A a=4,4 d=0,2 survives", + 3584 + ], + [ + "A a=4,4 d=2,0 survives", + 2688 + ], + [ + "D a=0,2 d=4,4 survives", + 14336 + ], + [ + "D a=1,3 d=3,3 survives", + 70560 + ], + [ + "D a=1,7 d=1,1 survives", + 784 + ], + [ + "D a=2,0 d=4,4 survives", + 10752 + ], + [ + "D a=2,4 d=2,2 survives", + 80640 + ], + [ + "D a=3,1 d=3,3 survives", + 50400 + ], + [ + "D a=3,5 d=1,1 survives", + 3920 + ], + [ + "D a=4,2 d=2,2 survives", + 53760 + ], + [ + "D a=5,3 d=1,1 survives", + 2352 + ], + [ + "D a=7,1 d=1,1 survives", + 112 + ] + ], + "combos": 10015005, + "covers": [ + [ + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 14, + 16, + 25 + ], + [ + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 14, + 17, + 24 + ], + [ + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 14, + 18, + 27 + ] + ], + "covers_total": 49280 + }, + "20": { + "agg": [], + "class_agg": [], + "combos": 55, + "covers": [], + "covers_total": 0 + }, + "21": { + "agg": [], + "class_agg": [], + "combos": 10, + "covers": [], + "covers_total": 0 + }, + "22": { + "agg": [], + "class_agg": [], + "combos": 1, + "covers": [], + "covers_total": 0 + }, + "23": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "24": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "25": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "26": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "27": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "28": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "29": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "3": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 448 + ], + [ + "4_6 kA=12 kD=0", + 2688 + ], + [ + "4_6 kA=6 kD=6", + 8064 + ], + [ + "6_4 kA=0 kD=12", + 4928 + ], + [ + "6_4 kA=6 kD=6", + 14784 + ], + [ + "8_2 kA=7 kD=8", + 3136 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 392 + ], + [ + "A a=1,1 d=3,5 survives", + 1960 + ], + [ + "A a=1,1 d=5,3 survives", + 1176 + ], + [ + "A a=1,1 d=7,1 survives", + 56 + ], + [ + "A a=2,2 d=2,4 survives", + 48384 + ], + [ + "A a=2,2 d=4,2 survives", + 32256 + ], + [ + "A a=3,3 d=1,3 survives", + 52080 + ], + [ + "A a=3,3 d=3,1 survives", + 36624 + ], + [ + "A a=4,4 d=0,2 survives", + 12544 + ], + [ + "A a=4,4 d=2,0 survives", + 9408 + ], + [ + "D a=0,2 d=4,4 survives", + 1792 + ], + [ + "D a=1,3 d=3,3 survives", + 28560 + ], + [ + "D a=1,7 d=1,1 survives", + 2744 + ], + [ + "D a=2,0 d=4,4 survives", + 1344 + ], + [ + "D a=2,4 d=2,2 survives", + 88704 + ], + [ + "D a=3,1 d=3,3 survives", + 19824 + ], + [ + "D a=3,5 d=1,1 survives", + 13720 + ], + [ + "D a=4,2 d=2,2 survives", + 59136 + ], + [ + "D a=5,3 d=1,1 survives", + 8232 + ], + [ + "D a=7,1 d=1,1 survives", + 392 + ] + ], + "combos": 6906900, + "covers": [ + [ + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 16, + 24 + ], + [ + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 17, + 25 + ], + [ + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 18, + 26 + ] + ], + "covers_total": 34048 + }, + "30": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "31": { + "agg": [], + "class_agg": [], + "combos": 0, + "covers": [], + "covers_total": 0 + }, + "4": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 1536 + ], + [ + "4_6 kA=12 kD=0", + 3168 + ], + [ + "4_6 kA=6 kD=6", + 9504 + ], + [ + "6_4 kA=0 kD=12", + 2112 + ], + [ + "6_4 kA=6 kD=6", + 6336 + ], + [ + "8_2 kA=7 kD=8", + 384 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 1344 + ], + [ + "A a=1,1 d=3,5 survives", + 6720 + ], + [ + "A a=1,1 d=5,3 survives", + 4032 + ], + [ + "A a=1,1 d=7,1 survives", + 192 + ], + [ + "A a=2,2 d=2,4 survives", + 57024 + ], + [ + "A a=2,2 d=4,2 survives", + 38016 + ], + [ + "A a=3,3 d=1,3 survives", + 22080 + ], + [ + "A a=3,3 d=3,1 survives", + 15936 + ], + [ + "A a=4,4 d=0,2 survives", + 1536 + ], + [ + "A a=4,4 d=2,0 survives", + 1152 + ], + [ + "D a=0,2 d=4,4 survives", + 6144 + ], + [ + "D a=1,3 d=3,3 survives", + 33120 + ], + [ + "D a=1,7 d=1,1 survives", + 336 + ], + [ + "D a=2,0 d=4,4 survives", + 4608 + ], + [ + "D a=2,4 d=2,2 survives", + 38016 + ], + [ + "D a=3,1 d=3,3 survives", + 23904 + ], + [ + "D a=3,5 d=1,1 survives", + 1680 + ], + [ + "D a=4,2 d=2,2 survives", + 25344 + ], + [ + "D a=5,3 d=1,1 survives", + 1008 + ], + [ + "D a=7,1 d=1,1 survives", + 48 + ] + ], + "combos": 4686825, + "covers": [ + [ + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 12, + 16, + 23 + ], + [ + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 12, + 17, + 22 + ], + [ + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 12, + 18, + 21 + ] + ], + "covers_total": 23040 + }, + "5": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 192 + ], + [ + "4_6 kA=12 kD=0", + 1200 + ], + [ + "4_6 kA=6 kD=6", + 3600 + ], + [ + "6_4 kA=0 kD=12", + 2256 + ], + [ + "6_4 kA=6 kD=6", + 6768 + ], + [ + "8_2 kA=7 kD=8", + 1344 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 168 + ], + [ + "A a=1,1 d=3,5 survives", + 840 + ], + [ + "A a=1,1 d=5,3 survives", + 504 + ], + [ + "A a=1,1 d=7,1 survives", + 24 + ], + [ + "A a=2,2 d=2,4 survives", + 21600 + ], + [ + "A a=2,2 d=4,2 survives", + 14400 + ], + [ + "A a=3,3 d=1,3 survives", + 23760 + ], + [ + "A a=3,3 d=3,1 survives", + 16848 + ], + [ + "A a=4,4 d=0,2 survives", + 5376 + ], + [ + "A a=4,4 d=2,0 survives", + 4032 + ], + [ + "D a=0,2 d=4,4 survives", + 768 + ], + [ + "D a=1,3 d=3,3 survives", + 12720 + ], + [ + "D a=1,7 d=1,1 survives", + 1176 + ], + [ + "D a=2,0 d=4,4 survives", + 576 + ], + [ + "D a=2,4 d=2,2 survives", + 40608 + ], + [ + "D a=3,1 d=3,3 survives", + 8880 + ], + [ + "D a=3,5 d=1,1 survives", + 5880 + ], + [ + "D a=4,2 d=2,2 survives", + 27072 + ], + [ + "D a=5,3 d=1,1 survives", + 3528 + ], + [ + "D a=7,1 d=1,1 survives", + 168 + ] + ], + "combos": 3124550, + "covers": [ + [ + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 16, + 24 + ], + [ + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 17, + 25 + ], + [ + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 18, + 26 + ] + ], + "covers_total": 15360 + }, + "6": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 192 + ], + [ + "4_6 kA=12 kD=0", + 864 + ], + [ + "4_6 kA=6 kD=6", + 2736 + ], + [ + "6_4 kA=0 kD=12", + 1488 + ], + [ + "6_4 kA=6 kD=6", + 4032 + ], + [ + "8_2 kA=7 kD=8", + 480 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 168 + ], + [ + "A a=1,1 d=3,5 survives", + 840 + ], + [ + "A a=1,1 d=5,3 survives", + 504 + ], + [ + "A a=1,1 d=7,1 survives", + 24 + ], + [ + "A a=2,2 d=2,4 survives", + 16080 + ], + [ + "A a=2,2 d=4,2 survives", + 10704 + ], + [ + "A a=3,3 d=1,3 survives", + 14352 + ], + [ + "A a=3,3 d=3,1 survives", + 9840 + ], + [ + "A a=4,4 d=0,2 survives", + 1920 + ], + [ + "A a=4,4 d=2,0 survives", + 1440 + ], + [ + "D a=0,2 d=4,4 survives", + 768 + ], + [ + "D a=1,3 d=3,3 survives", + 9840 + ], + [ + "D a=1,7 d=1,1 survives", + 360 + ], + [ + "D a=2,0 d=4,4 survives", + 576 + ], + [ + "D a=2,4 d=2,2 survives", + 25488 + ], + [ + "D a=3,1 d=3,3 survives", + 6576 + ], + [ + "D a=3,5 d=1,1 survives", + 2280 + ], + [ + "D a=4,2 d=2,2 survives", + 16560 + ], + [ + "D a=5,3 d=1,1 survives", + 1080 + ], + [ + "D a=7,1 d=1,1 survives", + 120 + ] + ], + "combos": 2042975, + "covers": [ + [ + 6, + 7, + 8, + 9, + 10, + 12, + 16, + 17, + 24, + 31 + ], + [ + 6, + 7, + 8, + 9, + 10, + 12, + 16, + 17, + 25, + 30 + ], + [ + 6, + 7, + 8, + 9, + 10, + 12, + 16, + 23, + 24, + 25 + ] + ], + "covers_total": 9792 + }, + "7": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 384 + ], + [ + "4_6 kA=12 kD=0", + 1008 + ], + [ + "4_6 kA=6 kD=6", + 2496 + ], + [ + "6_4 kA=0 kD=12", + 384 + ], + [ + "6_4 kA=6 kD=6", + 1200 + ], + [ + "8_2 kA=7 kD=8", + 96 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 288 + ], + [ + "A a=1,1 d=3,5 survives", + 1824 + ], + [ + "A a=1,1 d=5,3 survives", + 864 + ], + [ + "A a=1,1 d=7,1 survives", + 96 + ], + [ + "A a=2,2 d=2,4 survives", + 16464 + ], + [ + "A a=2,2 d=4,2 survives", + 10608 + ], + [ + "A a=3,3 d=1,3 survives", + 4416 + ], + [ + "A a=3,3 d=3,1 survives", + 2784 + ], + [ + "A a=4,4 d=0,2 survives", + 384 + ], + [ + "A a=4,4 d=2,0 survives", + 288 + ], + [ + "D a=0,2 d=4,4 survives", + 1536 + ], + [ + "D a=1,3 d=3,3 survives", + 8928 + ], + [ + "D a=1,7 d=1,1 survives", + 96 + ], + [ + "D a=2,0 d=4,4 survives", + 1152 + ], + [ + "D a=2,4 d=2,2 survives", + 7056 + ], + [ + "D a=3,1 d=3,3 survives", + 6048 + ], + [ + "D a=3,5 d=1,1 survives", + 384 + ], + [ + "D a=4,2 d=2,2 survives", + 4752 + ], + [ + "D a=5,3 d=1,1 survives", + 288 + ] + ], + "combos": 1307504, + "covers": [ + [ + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 16, + 24 + ], + [ + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 17, + 25 + ], + [ + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 18, + 26 + ] + ], + "covers_total": 5568 + }, + "8": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 256 + ], + [ + "4_6 kA=12 kD=0", + 576 + ], + [ + "4_6 kA=6 kD=6", + 1920 + ], + [ + "6_4 kA=0 kD=12", + 384 + ], + [ + "6_4 kA=6 kD=6", + 1280 + ], + [ + "8_2 kA=7 kD=8", + 64 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 256 + ], + [ + "A a=1,1 d=3,5 survives", + 1024 + ], + [ + "A a=1,1 d=5,3 survives", + 768 + ], + [ + "A a=2,2 d=2,4 survives", + 10944 + ], + [ + "A a=2,2 d=4,2 survives", + 7488 + ], + [ + "A a=3,3 d=1,3 survives", + 4224 + ], + [ + "A a=3,3 d=3,1 survives", + 3456 + ], + [ + "A a=4,4 d=0,2 survives", + 256 + ], + [ + "A a=4,4 d=2,0 survives", + 192 + ], + [ + "D a=0,2 d=4,4 survives", + 1024 + ], + [ + "D a=1,3 d=3,3 survives", + 6336 + ], + [ + "D a=1,7 d=1,1 survives", + 64 + ], + [ + "D a=2,0 d=4,4 survives", + 768 + ], + [ + "D a=2,4 d=2,2 survives", + 7296 + ], + [ + "D a=3,1 d=3,3 survives", + 5184 + ], + [ + "D a=3,5 d=1,1 survives", + 256 + ], + [ + "D a=4,2 d=2,2 survives", + 4992 + ], + [ + "D a=5,3 d=1,1 survives", + 192 + ] + ], + "combos": 817190, + "covers": [ + [ + 8, + 9, + 10, + 11, + 16, + 17, + 18, + 20, + 24, + 31 + ], + [ + 8, + 9, + 10, + 11, + 16, + 17, + 18, + 20, + 25, + 30 + ], + [ + 8, + 9, + 10, + 11, + 16, + 17, + 18, + 20, + 26, + 29 + ] + ], + "covers_total": 4480 + }, + "9": { + "agg": [ + [ + "2_8 kA=8 kD=7", + 32 + ], + [ + "4_6 kA=12 kD=0", + 192 + ], + [ + "4_6 kA=6 kD=6", + 672 + ], + [ + "6_4 kA=0 kD=12", + 384 + ], + [ + "6_4 kA=6 kD=6", + 1312 + ], + [ + "8_2 kA=7 kD=8", + 224 + ] + ], + "class_agg": [ + [ + "A a=1,1 d=1,7 survives", + 32 + ], + [ + "A a=1,1 d=3,5 survives", + 128 + ], + [ + "A a=1,1 d=5,3 survives", + 96 + ], + [ + "A a=2,2 d=2,4 survives", + 3744 + ], + [ + "A a=2,2 d=4,2 survives", + 2592 + ], + [ + "A a=3,3 d=1,3 survives", + 4320 + ], + [ + "A a=3,3 d=3,1 survives", + 3552 + ], + [ + "A a=4,4 d=0,2 survives", + 896 + ], + [ + "A a=4,4 d=2,0 survives", + 672 + ], + [ + "D a=0,2 d=4,4 survives", + 128 + ], + [ + "D a=1,3 d=3,3 survives", + 2208 + ], + [ + "D a=1,7 d=1,1 survives", + 224 + ], + [ + "D a=2,0 d=4,4 survives", + 96 + ], + [ + "D a=2,4 d=2,2 survives", + 7392 + ], + [ + "D a=3,1 d=3,3 survives", + 1824 + ], + [ + "D a=3,5 d=1,1 survives", + 896 + ], + [ + "D a=4,2 d=2,2 survives", + 5088 + ], + [ + "D a=5,3 d=1,1 survives", + 672 + ] + ], + "combos": 497420, + "covers": [ + [ + 9, + 10, + 11, + 12, + 16, + 17, + 18, + 19, + 24, + 28 + ], + [ + 9, + 10, + 11, + 12, + 16, + 17, + 18, + 19, + 25, + 29 + ], + [ + 9, + 10, + 11, + 12, + 16, + 17, + 18, + 19, + 26, + 30 + ] + ], + "covers_total": 2816 + } + }, + "total_combos": 64512240, + "total_covers": 317440 +} \ No newline at end of file diff --git a/research/f7-18point-vanishing-seedfc618722/CERTIFICATE.json b/research/f7-18point-vanishing-seedfc618722/CERTIFICATE.json new file mode 100644 index 0000000000..091668229a --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/CERTIFICATE.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "result": "KB3f set-level verdict (outcome=partial): the vanishing-character restriction of PR 2911, pressed against the four surviving 18-point splits of the F2^7 cover question, classifies the vanishing configurations exactly and excludes six of their classes, but excludes no split outright and constructs no cover. (12,6): a forced vanishing character must split A 6/6 across its kernel; every such class with D-split (6,0),(5,1),(4,2),(3,3) survives the exact floors, while a D-vanishing forces D 3/3 and kills A-splits (12,0),(11,1),(10,2) outright. (10,8): A-vanishing (5/5) kills D-split (8,0) and pins (7,1) to a tight Sidon class; D-vanishing (4/4) kills A-splits (10,0),(9,1) and pins (8,2) tight. (11,7)/(9,9): both sides odd, so NO character can vanish and the restriction is vacuous exactly there. Ground truth at the smallest instances (complete F2^4 and F2^5 cover censuses, 358,781 covers classified) shows real covers are rich in vanishing characters and never hit a dead class. Bounded class-restricted search finds no 18-point cover (best 115..119 of 128 across 16 classes) while the identical machinery finds F2^5 covers instantly. No kappa, supplier or selected-frontier change; the gap 20 <= f(7) <= 24 is unchanged.", + "labels": [ + { + "statement": "L2 (halving): char_sum(A, psi) = 0 iff A splits |A|/2 + |A|/2 across ker(psi). Hence A-vanishing needs s even and forces (s/2, s/2), D-vanishing needs t even and forces (t/2, t/2); at (11,7) and (9,9) both sides are odd so NO character of either side can vanish and PR 2911's restriction is vacuous exactly on those two splits.", + "label": "PROVEN", + "evidence": "Immediate from char_sum(A, psi) = |A0| - |A1| with |A0| + |A1| = |A|; machine-checked exhaustively for every subset of F2^3 and every character in test_engine.py (test_lemma_exhaustive_f2_3, test_11_7_and_9_9_no_vanishing)." + }, + { + "statement": "L3 (half-decomposition): with H = ker(psi), H' = E \\ H and the induced splits A = A0 u A1, D = D0 u D1, the pair (A, D) covers iff (A0+D0) u (A1+D1) = H, (A0+D1) u (A1+D0) = H', (A0+A0) u (A1+A1) u (D0+D0) u (D1+D1) = H and (A0+A1) u (D0+D1) = H'.", + "label": "PROVEN", + "evidence": "Coset arithmetic (sums of two elements of a common side land in H, cross-side sums in H'); checked exhaustively over all 256 x 256 pairs (A, D) of F2^3 and 4,000 random pairs of F2^5 (test_lemma_exhaustive_f2_3, test_lemma_samples_f2_5; check_half_decomposition)." + }, + { + "statement": "L4 (class floors): the H' even line forces a0*a1 + d0*d1 >= 2^(m-1) = 32 (and the sibling floors F2 (H even line), F3/F4 (odd lines)). In character language F1 is f_hat^2 + g_hat^2 <= s + t + 2P - 2^n and F3+F4 is |f_hat*g_hat| <= E_o: the floors re-derive PR 2911's two profile bounds in split language, and the class verdicts are their forced-split consequences. Six vanishing classes are PROVEN impossible: (12,6) D-vanish with A-split (12,0),(11,1),(10,2); (10,8) A-vanish with D-split (8,0); (10,8) D-vanish with A-split (10,0),(9,1).", + "label": "PROVEN", + "evidence": "Union-size bounds on L3's H' line (|A0+A1| <= a0*a1, |D0+D1| <= d0*d1, union = 32 points); the complete class tables with each floor value are computed by vanish.class_table and asserted in test_engine (test_floor_values_12_6, test_floor_values_10_8, test_dead_classes_have_witness)." + }, + { + "statement": "L5 (multi-vanishing structure): if A vanishes at two distinct characters psi1, psi2, its counts across the four parts of the (ker(psi1), ker(psi2)) grid are (x, y, y, x) with x + y = |A|/2.", + "label": "PROVEN", + "evidence": "From the two equations |A0| = |A1| on each kernel: adding and subtracting gives n00 = n11 and n01 = n10; checked exhaustively over every subset of F2^3 and every vanishing pair (check_multi_vanishing, test_multi_vanishing_structure_exhaustive_f2_3)." + }, + { + "statement": "L7 (equality analysis): whenever a0*a1 + d0*d1 = 32 and the pair covers, |A0+A1| = a0*a1 and |D0+D1| = d0*d1 (both Sidon: all cross sums distinct) and the two cross sumsets are disjoint with union the whole odd half. This pins the tight classes (10,8) A-vanish (7,1) and D-vanish (8,2) to exact forced Sidon structure; the (12,6) class A-vanish (6,0) forces |A0+A1| = 32 (the whole odd half, 36 pairs, excess 4) together with A0 + D = H and A1 + D = H' full.", + "label": "PROVEN", + "evidence": "Equality chain |A0+A1| + |D0+D1| - |intersection| = 32 <= a0*a1 + d0*d1; checked exhaustively over all covering (A, D) pairs of F2^3 and all characters at floor equality (check_tight_equality, test_tight_equality_exhaustive_f2_3). The (6,0) forced structure follows from D1 = empty in L3." + }, + { + "statement": "Every recorded predecessor anchor was reproduced before any new number: PR 2542/2634 REPRO tiers 945/31, 10395/49, 945945/59 (records SHA-256 match) and the L18 census 15,775,992 nodes / 312,064 cycles / 0 universal; PR 2870 OBSTRUCTION parseval=696 allowed=504 deficit=192 both parity orders; PR 2911 SQUEEZE table, PROFILE18 spectra 16/22/50/31, NOVANISH lines and ROWS18 808/501/251/196; the n=5 set controls; and both heavy PR 2773 census 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 this package's ANCHOR-PROGRESS.json (one section per mode, per-sub-shard receipts), started from a missing receipt file (run_anchors_all.py printed 'fresh receipts confirmed'). Receipt-validation trap recorded there: the extracted PR 2911 package's own quick mode prints ANCHORS receipt lines from its committed receipts; those lines validate receipts, they do not re-walk. The NOVANISH premise is additionally recomputed from this package's byte-vendored cover18.py (pin 24c6a2f4...) in verify.py novanish." + }, + { + "statement": "Ground-truth census of the smallest cover-bearing instances, classified by vanishing class: F2^4 has 41,341 covers among all 65,536 subsets; F2^5 has 317,440 ten-point covers among all C(32,10) = 64,512,240 ten-sets, of which exactly 99,200 pass through {0} (reproducing PR 2773's recorded n5 control value; 99,200 * 32 / 10 = 317,440). Exact split support of the F2^5 ten-covers: (2,8) 15,360, (4,6) 143,360, (6,4) 143,360, (8,2) 15,360 -- no (5,5),(3,7),(7,3),(1,9) cover exists -- and every cover has vanishing characters on at least one side (types (k_A,k_D) = (8,7),(12,0),(6,6),(0,12),(7,8) at character level).", + "label": "CHECKED", + "evidence": "vanish.census_f4 / census_f5 (independent enumeration route: every subset resp. every ten-set, not the predecessor's fixed-0 engine); verify.py classify walks all 32 shards from empty CENSUS-PROGRESS.json receipts (PASS_F7_18POINT_CLASSIFY) and asserts both the {0}-slice value 99,200 and the translation identity." + }, + { + "statement": "Soundness of the class floors on every real cover: across all 358,781 covers of the F2^4 and F2^5 censuses, no cover realizes a vanishing class whose forced splits violate a floor (dead_classes_hit is empty in every shard).", + "label": "CHECKED", + "evidence": "Per-shard assertions in verify.py classify (each shard asserts dead_classes_hit == [] before its receipt is written) and the census aggregates in CENSUS-PROGRESS.json; test_engine's census tests." + }, + { + "statement": "No 18-point cover exists in the searched classes (scoped search failure, never an exclusion): seeded first-improvement local search restricted to each of the 16 surviving vanishing classes (bit-0 psi, WLOG under GL(6,2); 30 restarts each) finds no covering pair (A, D); best scores 115..119 of 128 per class.", + "label": "CHECKED", + "evidence": "vanish.search_class, fixed seeds 7000+idx; verify.py search mode. Non-vacuity: the identical machinery finds real F2^5 (4,6) covers instantly both free (A=[9,12,13,14], D=[3,5,8,9,10,11], score 32/32) and inside the census-nonempty class A-vanish (2,4). The search never asserts nonexistence; the results are consistent with PR 2911's unrestricted best 118/128." + }, + { + "statement": "The vanishing-character restriction as an exclusion mechanism for (11,7) and (9,9) is DEMOTED to vacuous: by L2 no character can vanish there, so the restriction cannot press on those two splits at all (their PR 2911 row remainders 501 and 196 are untouched by this package).", + "label": "DEMOTED", + "evidence": "L2 (PROVEN above); test_11_7_and_9_9_no_vanishing asserts the empty class tables." + }, + { + "statement": "The expectation that the vanishing restriction alone excludes (12,6) and/or (10,8) is DEMOTED: eight (12,6) classes and eight (10,8) classes survive the exact floors (four of them pinned to tight forced Sidon or full-sumset structure), and bounded class-restricted search finds no contradiction-adjacent configuration to exploit further within budget.", + "label": "DEMOTED", + "evidence": "The class tables (PROVEN floors) and the class searches (CHECKED); a full exclusion needs either the tight classes' exact decision or the multi-vanishing joint layer (open questions 1-2 of the README)." + } + ], + "obstruction_numbers": { + "n": 7, + "m": 6, + "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": { + "forced_vanishing": "yes (PR 2911 NOVANISH, reproduced)", + "A_vanish": {"forced_split": [6, 6], "classes_surviving": [[6, 0], [5, 1], [4, 2], [3, 3]], "classes_dead": [], "forced_structure": "(6,0): |A0+A1| = 32 (whole odd half, excess 4), A0 + D = H and A1 + D = H' full"}, + "D_vanish": {"forced_split": [3, 3], "classes_surviving": [[9, 3], [8, 4], [7, 5], [6, 6]], "classes_dead": [[12, 0], [11, 1], [10, 2]]}, + "search_best_of_128": 119, + "verdict": "narrowed (3 classes PROVEN impossible), not excluded" + }, + "11_7": { + "forced_vanishing": "impossible (L2: both sides odd)", + "classes": "none exist", + "verdict": "the restriction does not press; PR 2911 row remainder 501 untouched" + }, + "10_8": { + "forced_vanishing": "yes (PR 2911 NOVANISH, reproduced)", + "A_vanish": {"forced_split": [5, 5], "classes_surviving": [[7, 1], [6, 2], [5, 3], [4, 4]], "classes_dead": [[8, 0]], "forced_structure": "(7,1): tight -- |A0+A1| = 25 Sidon, |D0+D1| = 7 (translate of D0), disjoint, union 32"}, + "D_vanish": {"forced_split": [4, 4], "classes_surviving": [[8, 2], [7, 3], [6, 4], [5, 5]], "classes_dead": [[10, 0], [9, 1]], "forced_structure": "(8,2): tight -- |A0+A1| = 16 (A0 misses its delta-translate), |D0+D1| = 16 (4x4 Sidon pair), disjoint, union 32"}, + "search_best_of_128": 119, + "verdict": "narrowed (3 classes PROVEN impossible, 2 pinned tight), not excluded" + }, + "9_9": { + "forced_vanishing": "impossible (L2: both sides odd)", + "classes": "none exist", + "verdict": "the restriction does not press; PR 2911 row remainder 196 untouched" + } + }, + "census_ground_truth": { + "f2_4_covers": 41341, + "f2_5_covers_total": 317440, + "f2_5_covers_through_0": 99200, + "f2_5_split_support": {"2_8": 15360, "4_6": 143360, "6_4": 143360, "8_2": 15360}, + "dead_classes_hit": 0 + }, + "controls": { + "n3_exhaustive": "L2/L3 checked on all 65,536 (A, D) pairs of F2^3; L5 and L7 exhaustive at F2^3", + "n5_real_cover": "the recorded 10-point cover [0,1,2,3,4,5,6,8,16,31] of F2^5 classifies as split (4,6), k_A = 12, k_D = 0, no dead classes (test_f2_5_subspace_example_classified)", + "n4_n5_census_soundness": "no cover of either census hits a dead class" + } + }, + "reproduce": [ + "python3 -I -B research/f7-18point-vanishing-seedfc618722/test_engine.py", + "python3 -I -B research/f7-18point-vanishing-seedfc618722/verify.py quick", + "python3 -I -B research/f7-18point-vanishing-seedfc618722/verify.py novanish", + "python3 -I -B research/f7-18point-vanishing-seedfc618722/verify.py classify", + "python3 -I -B research/f7-18point-vanishing-seedfc618722/verify.py search", + "python3 -I -B research/f7-18point-vanishing-seedfc618722/anchors.py k10b3", + "python3 -I -B research/f7-18point-vanishing-seedfc618722/anchors.py k11b4" + ] +} diff --git a/research/f7-18point-vanishing-seedfc618722/NOTICE.md b/research/f7-18point-vanishing-seedfc618722/NOTICE.md new file mode 100644 index 0000000000..903d224f1f --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/NOTICE.md @@ -0,0 +1,63 @@ +# 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 `test_engine.py` / `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 whole 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` + reproduced as an anchor. +- [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`"; its REPRO tiers and length-18 census are reproduced + here as anchors. +- [PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634) by + Aaron Wang (navinor) - the recorded KB3b state and the bounded-search + precedent (20-point covers abundant; no 19-point cover in 200 restarts, + max `124/128`) that this package's class-restricted searches 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` this package's independent + `C(32,10)` census reproduces. +- [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 from empty receipts). +- [PR 2911](https://github.com/CrocSwap/integer-mult-bounds/pull/2911) by + Aaron Wang (navinor) - the immediate predecessor: the `(A, D)` reduction + lemma, the squeeze/deficit bookkeeping, the per-character profile system + and its no-vanishing sub-case (the vanishing-character restriction this + package presses), the row remainder `808/501/251/196` and the open + questions 1-2 that name this step. Its engine `cover18.py` is vendored + byte-exact as `vendor/cover18.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) is a different (word-level) object and is untouched. + +Vendored files (byte-exact, enforced by byte-pin checks): + +| Local path | Source | SHA-256 (prefix) | +|---|---|---| +| `vendor/agent64_cover17.py` | PR 2773 `cover17.py` (via PR 2870/2911's pinned vendor/) | `082bc838134cba97...` | +| `vendor/agent64_search17.py` | PR 2773 `search17.py` (via PR 2870/2911's pinned vendor/) | `9eb1bf79ffb99b0e...` | +| `vendor/cover18.py` | PR 2911 `cover18.py` | `24c6a2f4911dc2d5...` | +| `anchors.py` | PR 2870 `anchors.py` | `73d73a9b94539403...` | + +Predecessor packages were read byte-exactly from their PR heads with +`agent_tools.py pr-tree-extract` and were never imported at runtime. diff --git a/research/f7-18point-vanishing-seedfc618722/README.md b/research/f7-18point-vanishing-seedfc618722/README.md new file mode 100644 index 0000000000..5c60050eed --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/README.md @@ -0,0 +1,199 @@ +# KB3f - the vanishing-character restriction pressed against the four surviving 18-point splits + +**Set-level finite result, no words enumerated. Outcome=partial: the +18-point cover question for `F2^7` is narrowed, not decided.** PR 2911 +(Aaron Wang) proved that any `(12,6)` or `(10,8)` cover must have a vanishing +character off the all-ones hyperplane. This package classifies those +vanishing configurations exactly and tests each class against coverage of the +remaining masks: **six classes are PROVEN impossible**, the two tight classes +are pinned to exact forced Sidon structure, and for `(11,7)/(9,9)` the +restriction provably cannot press at all (no character can vanish there). +No 18-point cover was constructed and no split was excluded outright; 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), `B` in the odd coset `O` (t points), `s + t = 18`; +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) 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. + +## Verdict per split (exact integers throughout) + +| Split | Forced vanishing (PR 2911, reproduced here) | Vanishing classes after the floors | Verdict | +|---|---|---|---| +| `(12,6)` | yes | `A`-vanish `(6,0)(5,1)(4,2)(3,3)` survive; `D`-vanish `(12,0)(11,1)(10,2)` **PROVEN impossible**; `D`-vanish `(9,3)(8,4)(7,5)(6,6)` survive | narrowed, not excluded | +| `(11,7)` | no vanishing exists (L2) | none | restriction does not press | +| `(10,8)` | yes | `A`-vanish `(8,0)` **PROVEN impossible**; `(7,1)` tight; `(6,2)(5,3)(4,4)` survive; `D`-vanish `(10,0)(9,1)` **PROVEN impossible**; `(8,2)` tight; `(7,3)(6,4)(5,5)` survive | narrowed, not excluded | +| `(9,9)` | no vanishing exists (L2) | none | restriction does not press | + +A class is (vanishing side, forced split of that side, split of the other +side) across `ker(psi)` for one nontrivial character `psi` of `E = F2^6`; +mirrors `(6,12)/(7,11)/(8,10)/(9,9)` are identical by odd translation. + +## The classification (PROVEN lemmas, machine-checked) + +**L2 (halving).** `char_sum(A, psi) = 0` iff `A` splits `|A|/2 + |A|/2` +across `ker(psi)`. So `A`-vanishing needs `s` even and forces `(s/2, s/2)`, +`D`-vanishing needs `t` even and forces `(t/2, t/2)`. At `(11,7)` and +`(9,9)` both sides are odd: **no character can vanish**, so PR 2911's +restriction is vacuous exactly on those two splits. + +**L3 (half-decomposition).** With `H = ker(psi)`, `H' = E \ H` and the +induced splits `A = A0 u A1`, `D = D0 u D1`, 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'`. +Checked exhaustively over all `256 x 256` pairs of `F2^3` and 4,000 random +pairs of `F2^5`. + +**L4 (class floors).** Exact union-size bounds on L3's `H'` even line: +`a0*a1 + d0*d1 >= 2^(m-1) = 32` (and the three sibling floors `F2/F3/F4` +of the `H` even and both odd lines). In character language `F1` is +`f_hat^2 + g_hat^2 <= s + t + 2*P - 2^n` and `F3+F4` is +`|f_hat*g_hat| <= E_o` - i.e. the floors re-derive PR 2911's two profile +bounds in split language; the class verdicts are their forced-split +consequences. A class whose forced splits violate a floor is impossible: +no cover realizes it. Six classes die this way (table above). At the two +tight classes (`(10,8)` `A`-vanish `(7,1)` and `D`-vanish `(8,2)`) the floor +holds with equality. + +**L5 (multi-vanishing structure).** If `A` vanishes at two distinct +characters `psi1, psi2`, its counts across the four parts of the +`(ker(psi1), ker(psi2))` grid are `(x, y, y, x)` with `x + y = |A|/2`. +Exhaustive at `F2^3`. + +**L7 (equality analysis).** Whenever `a0*a1 + d0*d1 = 32` and the pair +covers, `|A0+A1| = a0*a1` and `|D0+D1| = d0*d1` (both Sidon: all cross sums +distinct) and the two cross sumsets are disjoint with union the whole odd +half. Exhaustive at `F2^3`. So the tight classes are pinned to exact +forced Sidon structure, e.g. `(10,8)` `D`-vanish `(8,2)`: `A1` is a pair +whose two translates of `A0` are disjoint (`A0 n (A0 + delta) = 0`), and +`D0, D1` are 4-sets forming a Sidon pair with `|D0+D1| = 16`. +The `(12,6)` `A`-vanish `(6,0)` class forces `|A0+A1| = 32` (the whole odd +half; 36 pairs, excess 4) together with `A0 + D = H` and `A1 + D = H'` full. + +## Ground-truth census: which classes actually occur + +Complete enumeration at the two smallest cover-bearing instances (all exact +integers; independent enumeration route - every subset resp. every 10-set, +not the predecessor's fixed-0 engine): + +- **`F2^4`**: all 65,536 subsets scanned; **41,341 covers** `S + S = F2^4`; + classified by split and vanishing type (full table in the replay log). +- **`F2^5`**: all `C(32,10) = 64,512,240` ten-sets scanned; + **317,440 covers** total. The covers through `{0}` number exactly + **99,200**, reproducing PR 2773's recorded n5 control value (its engine + fixes `0`; `99,200 * 32 / 10 = 317,440` is the un-normalized count, and + shard 0 of this enumeration is the `{0}` slice). + Exact split support: `(2,8)` 15,360; `(4,6)` 143,360 = 35,840 type + `(k_A,k_D) = (12,0)` + 107,520 type `(6,6)`; `(6,4)` 143,360 (mirrored); + `(8,2)` 15,360. **No 10-cover of `F2^5` has split `(5,5),(3,7),(7,3)` or + `(1,9)`**, and every cover has vanishing characters on at least one side. +- **Soundness**: across all 358,781 covers of both censuses **no cover hits + a dead class** - the floors reject no real configuration. + +## Bounded class-restricted search (CHECKED; scoped search failure) + +Smallest falsifying instance first: one covering pair `(A, D)` in a surviving +class. Seeded first-improvement local search restricted to each surviving +class (bit-0 `psi`, WLOG under `GL(6,2)`), 30 restarts each, all 16 classes: +**no cover found**; best scores `115..119` of 128 (per-class exact numbers +in the replay log), consistent with PR 2911's unrestricted best `118/128`. +Non-vacuity: the identical machinery finds `F2^5` `(4,6)` covers instantly +both free (`A=[9,12,13,14], D=[3,5,8,9,10,11]`) and inside the +census-nonempty class `A`-vanish `(2,4)`. A failed bounded search is +evidence about the searched domain, never an exclusion. + +## Reproduce + +Standard library only, CPython 3.12, from the repository root: + +```sh +python3 -I -B research/f7-18point-vanishing-seedfc618722/test_engine.py +python3 -I -B research/f7-18point-vanishing-seedfc618722/verify.py quick +python3 -I -B research/f7-18point-vanishing-seedfc618722/verify.py novanish +python3 -I -B research/f7-18point-vanishing-seedfc618722/verify.py classify +python3 -I -B research/f7-18point-vanishing-seedfc618722/verify.py search +``` + +Expected markers: `Ran 14 tests ... OK`, `PASS_F7_18POINT_QUICK`, +`PASS_F7_18POINT_NOVANISH`, `PASS_F7_18POINT_CLASSIFY`, +`PASS_F7_18POINT_SEARCH`. The heavy PR 2773 census anchors are re-walked +from empty receipts by the byte-vendored driver (per-sub-shard receipts in +`ANCHOR-PROGRESS.json`, one section per mode): + +```sh +python3 -I -B research/f7-18point-vanishing-seedfc618722/anchors.py k10b3 +python3 -I -B research/f7-18point-vanishing-seedfc618722/anchors.py k11b4 +``` + +Re-invoke to continue a partial walk; `run_anchors_all.py` loops both modes +to completion. Recorded in-session from empty receipts: `PASS_ANCHORS_K10B3 +count=149990400 total_hist={'3': 149990400} shards=62` and +`PASS_ANCHORS_K11B4 count=0 total_hist={} shards=62` (see ANCHOR-REPRO.json). + +## Recorded anchors (reproduced before any new number) + +| Anchor | Value | Status here | +|---|---|---| +| PR 2542/2634 REPRO tiers | `945/31`, `10395/49`, `945945/59` (records SHA-256 match) | recomputed (PR 2773 verify.py on the byte-exact vendored engine) | +| PR 2542 length-18 census | `15,775,992` nodes, `312,064` cycles, `0` universal | recomputed (same run) | +| PR 2870 OBSTRUCTION | `parseval=696 allowed=504 deficit=192`, both parity orders | recomputed (PR 2870 verify.py; again in this package's `squeeze_numbers`) | +| PR 2911 SQUEEZE table | `(12,6)` `1248/696`; `(11,7)` `1166/798` vs `21294`; `(10,8)` `1080/896`; `(9,9)` `990/990` vs `36414` | recomputed (vendored `cover18.squeeze_numbers`) | +| PR 2911 NOVANISH lines | `(12,6)`,`(10,8)` infeasible: vanishing forced | recomputed (vendored `cover18.fourier_profile_feasibility`, `verify.py novanish`) | +| PR 2911 ROWS18 | `808/501/251/196` | recomputed (PR 2911 `verify.py rows`) | +| PR 2773 n5 set controls | `0` nine-point covers (max 29), `99,200` ten-point covers through `{0}` | recomputed twice (PR 2773 verify.py; independent full `C(32,10)` census here) | +| PR 2773 `k10 budget-3` | `149,990,400` | re-walked in full (fresh empty receipts, 62/62 sub-shards) | +| PR 2773 `k11` levels 3-4 | `0`, `0` | re-walked in full (fresh empty receipts, 62/62 sub-shards) | + +## 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 are not proved +nonempty or empty: the class floors and the Sidon pinning are necessary +conditions, and the class-restricted search failures are bounded search +failures. The tight classes' exact decision (enumerate the forced Sidon +pairs jointly with the odd-half multiplicities) is the open step. The gap +`20 <= f(7) <= 24` is unchanged. + +## Open next questions + +1. **Decide the two tight classes exactly** (`(10,8)` `A`-vanish `(7,1)` and + `D`-vanish `(8,2)`, and the full-sumset class `(12,6)` `A`-vanish + `(6,0)`). First step: enumerate Sidon pairs `D0, D1` of 4-sets in + `F2^5` (`|D0+D1| = 16`) and solve the disjointness/translation conditions + of L7 against the odd-half `A + D = E` multiplicities. Blocked by: the + joint pair enumeration size; no structural blocker known. +2. **Combine several vanishings (L5's grid) with the floors at their product + characters.** First step: enumerate the four-part counts `(x, y, y, x)` + of surviving classes at two characters and intersect the three floor + systems. Blocked by: nothing structural. +3. **A different identity for `(11,7)/(9,9)`.** The vanishing route is + provably vacuous there (L2); the row remainders `501/196` of PR 2911 are + untouched by this package. Cross-sum multiplicities or the even half in + PR 2870's language remain the named candidates. + +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 anchor +reproductions. diff --git a/research/f7-18point-vanishing-seedfc618722/SOURCES.json b/research/f7-18point-vanishing-seedfc618722/SOURCES.json new file mode 100644 index 0000000000..db00591622 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/SOURCES.json @@ -0,0 +1,118 @@ +{ + "base_commit": "f646a7fb75f7d854a881e07fefb13fdfe7631c86", + "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 before submission (discussions 1317 and 1166 via agent_tools.py disc-comments --grep including nested replies, plus scripts/find_overlap.py --refresh with the object's proper names) found no claim on the 18-point set object or the vanishing-character classification.", + "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; PR 2870 (Aaron Wang) closed the (5,1),(6,0) rows with the odd-coverage Fourier/Parseval identity; PR 2911 (Aaron Wang) narrowed the 18-point question to four splits and PROVED the vanishing-character restriction on (12,6)/(10,8). This package presses that restriction (PR 2911 open questions 1-2).", + "question": "KB3f: classify the vanishing-character configurations of the four surviving 18-point splits and test each class against coverage. Outcome=partial: six classes PROVEN impossible, tight classes pinned to forced Sidon structure, (11,7)/(9,9) provably unreachable by this restriction, no split excluded outright." + }, + "references": [ + { + "head": "6739c799799621878a9249c93e2b12cc799c1482", + "local_path": "vendor/agent64_cover17.py", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from PR 2911's hash-pinned vendor/, never imported), credit Aaron Wang (navinor), PR 2773. Used by the vendored cover18.py. The live drift check pins base-commit blobs only, so this head-pinned vendor copy is enforced by test_engine.py and verify.py 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 (agent_tools.py pr-tree-extract of PR 2911's package), credit Aaron Wang (navinor), PR 2911: the exact-arithmetic KB3e engine (squeeze/deficit bookkeeping, per-character profile system). Reproduces the SQUEEZE table and the load-bearing NOVANISH premise in verify.py quick/novanish. 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 and PR 2911'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": "cfb813f883e61519deedcd84151dc0c68b9d19cc", + "local_path": null, + "note": "Aaron Wang (navinor): the immediate predecessor. The (A, D) reduction lemma, the odd-coverage Fourier/Parseval squeeze with tracked deficit, the per-character profile system and its no-vanishing sub-case (the vanishing restriction this package presses), the row remainder 808/501/251/196 and the bounded search precedent (best 118/128) were read and reproduced byte-exactly, never re-derived as new results.", + "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; its open questions 1-2 name this package's step.", + "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, n5 controls) are re-walked/recomputed here.", + "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', the length-18 exclusion (REPRO tiers and L18 census reproduced in-session).", + "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) that this package's bounded class searches 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 used by the REPRO tier anchors.", + "pr": 1185, + "source_path": "research/universal-connector-six-source/" + } + ], + "schema_version": 1 +} diff --git a/research/f7-18point-vanishing-seedfc618722/TASK-CARD.md b/research/f7-18point-vanishing-seedfc618722/TASK-CARD.md new file mode 100644 index 0000000000..82eb26b261 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/TASK-CARD.md @@ -0,0 +1,103 @@ +# Task card - KB3f: press the vanishing-character restriction against the four surviving 18-point splits + +```text +Task ID / proposed scope key: kappa-blocker KB3f / scope key 4e44f2900cd2a6a3003d + (deterministic: sha256("fc618722a84313d16975dd03a0d68449:kb3f-vanishing")[:20]; + chooser OS nonce fc618722a84313d16975dd03a0d68449, track recursive-interfaces) + +Base commit; exact predecessor and dependency heads (verified with `gh pr view +NNN --json author,title` against current ground truth at entry, 2026-10-16): + base commit f646a7fb75f7d854a881e07fefb13fdfe7631c86 + PR 2542 (Aaron Wang) head 3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf + PR 2634 (Aaron Wang) head e2f30d93efbef5658334072aa855aa95e795e394 + PR 2773 (Aaron Wang) head 6739c799799621878a9249c93e2b12cc799c1482 + PR 2870 (Aaron Wang) head 9f55f291e9e79e628fd98f1e4f4debfc1c2106e5 (MERGED) + PR 2911 (Aaron Wang) head cfb813f883e61519deedcd84151dc0c68b9d19cc + PR 2691 (Nicholas Stone) head 88dda3534071442773106e9c0b941b9d39a3cea8 + (recorded state only; concurrent L=20 WORD census, different object) + +Concrete object and question: + The set-level 18-point cover question for F2^7 (PR943 prefix-walk model: + P + P = F2^7). PR 2911 narrowed it to four surviving parity splits + (12,6), (11,7), (10,8), (9,9) (+ mirrors) and PROVED: any (12,6) or (10,8) + cover must have a vanishing character off the all-ones hyperplane (the + no-vanishing sub-case forces sum rho^2 = 46 at (12,6), unattainable; at + (10,8) the parity/integrality fails). Question here: PRESS THAT RESTRICTION - + classify the vanishing-character configurations (which characters can + vanish, what half-decomposition structure that forces on A and B in the + (A, D) reduction in E = F2^6, and whether coverage of the remaining masks + survives), and try one exact contradiction per class to exclude (12,6) and + (10,8); then, if those hold, extend the classification to (11,7)/(9,9) + (where no character can vanish at all - both sides odd - so those splits + need a different identity). Outcome sought: settle or further narrow the + four splits; a covering 18-set in any split is a complete result. + +Scope status: changed (authorized "explicit open request" scope change). + Reason: the assignment takes the explicit open request from discussion 1166 + (PR 2911's open questions 1 and 2 - the vanishing-character route) instead + of the drawn card. The chooser (seed fc618722a84313d16975dd03a0d68449, + track recursive-interfaces) drew the card centre-path-sharing (scope key + a55534776f5479f1686c) plus two neighbors (coverage-law-change, + connector-alphabet-change); all three are saturated cards for this object + (they target the selected word's centre path / coverage identity / connector + alphabet, not the F2^7 cover question), which the assignment records as the + reason for taking the assigned request. + +Existing restriction being changed (or exact claim being audited): + PR 2911's PROVEN vanishing-character restriction on (12,6)/(10,8) is being + exploited, not changed; PR 2911's own open question 2 ("does combining the + forced vanishings with the even-half multiplicities exclude (12,6) outright?") + is the target. PR 2911's profile system's step cap and its feasible profile + counts (16/22/50/31 spectra) are reproduced first. + +Method; explicit parameter ranges/candidate alphabet: + Exact integer arithmetic only (no floats). (1) Reproduce every recorded + anchor before any new number (PR 2542/2634 REPRO tiers; PR 2542 L=18 census; + PR 2870 OBSTRUCTION parseval=696 allowed=504 deficit=192; PR 2911 ROWS18 + 808/501/251/196 and NOVANISH lines; PR 2773 k10 budget-3 = 149,990,400 and + k11 levels 3-4 = 0/0 re-walked from EMPTY receipts in resumable sharded + jobs). (2) Vanishing-classification layer: for splits (12,6)/(10,8) in the + (A, D) reduction (A, D subsets of E = F2^6, |A| = s, |D| = t, A + D = E, + (A+A) u (D+D) = E), classify configurations with a vanishing character psi + (A-halves of size s/2 across ker(psi); D-halves d0/d1), derive the exact + half-decomposition constraints per class (odd half excess 4+4 at (12,6), + even half E1 coverage (A0+A1) u (D0+D1) = E1), and decide each class by + exact enumeration where the class space is finite and small (halved + F2^5 subproblems, profile shapes with zero columns plus the even-half + multiplicity layer). Ground truth at the smallest instances: exhaustive + classification of all covers of F2^4 and of the 99,200 recorded F2^5 + ten-point covers by vanishing type. (3) One bounded pivot max: structured + seeded search restricted to one vanishing class ((12,6), A-split 6/6 across + a fixed hyperplane) - the smallest falsifying instance for a class + contradiction is a covering pair (A, D) in that class. + +Nearest overlapping PRs and why this adds something: + PR 2911 (Aaron Wang) - the immediate predecessor; narrows the question, + proves the vanishing restriction; its open questions 1-2 name exactly this + next step ("add the even-half multiplicity constraints as a second layer and + enumerate the joint profiles"; "blocked by: nothing structural"). This + package executes that named step and classifies the vanishings; it does not + re-run PR 2911's search or row machinery as new results. + PR 2870 (Aaron Wang) - the odd-coverage Fourier/Parseval identity (vendored + byte-exact with SHA-256 pins, credited). + PR 2773 (Aaron Wang) - pair-representation rows and the census floors whose + anchors are re-walked here. + PR 2691 (Nicholas Stone) - the (10,10) L=20 WORD census (recorded state + only; different object - this package stays strictly on the SET level). + +Declared milestone: local module (a scoped set-level obstruction or narrowed + remainder; no supplier, tariff, certificate or selected-frontier change). + +Optimistic full cost budget; required observable improvement: + Budget ~210 minutes total; the required observable is a labelled + split-by-split verdict (PROVEN / CHECKED / DEMOTED) with exact integers and + machine-checked classification counts, i.e. either class contradictions + excluding (12,6) and/or (10,8), or the exact surviving vanishing classes + recorded as the narrowed remainder. + +Unresolved consumer/restoration costs; family expansion decision if continuing: + Not applicable: a finite set-level question in the PR943 query model; no + consumer, restoration or physical interface is priced and no family + expansion is claimed. The f(7) gap 20 <= f(7) <= 24 is unchanged unless an + 18-point cover is constructed (which keeps L = 22 alive) or all splits are + excluded (which kills L = 22). diff --git a/research/f7-18point-vanishing-seedfc618722/TASK.json b/research/f7-18point-vanishing-seedfc618722/TASK.json new file mode 100644 index 0000000000..7ed37db55c --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/TASK.json @@ -0,0 +1,119 @@ +{ + "actual_scope": "Kappa-blocker KB3f (set level, no words): press the vanishing-character restriction of PR 2911 against the four surviving splits of the 18-point cover question for F2^7. Delivered outcome=partial: an exact classification of the vanishing configurations and a per-class verdict. (1) L2 PROVEN: a vanishing character forces the vanishing side to split equally across its kernel, so at (11,7)/(9,9) both sides odd NO character can vanish and the restriction is vacuous exactly on those two splits. (2) L3 PROVEN (exhaustive m=3, 256x256 pairs): the exact half-decomposition of both covering lines across ker(psi). (3) L4 (class floors): exact union-size bounds on the half lines (in character language they re-derive PR 2911's even-half and odd-half bounds); the forced-split consequences PROVE six vanishing classes impossible: (12,6) D-vanish (12,0),(11,1),(10,2) and (10,8) A-vanish (8,0), D-vanish (10,0),(9,1). (4) L5 PROVEN (exhaustive m=3): two simultaneous vanishings force the balanced grid (x,y,y,x). (5) L7 PROVEN (exhaustive m=3): floor equality plus coverage forces Sidon cross sums (|A0+A1| = a0*a1, |D0+D1| = d0*d1, disjoint, union the whole odd half), pinning the two tight classes (10,8) A-vanish (7,1) and D-vanish (8,2) and the full-sumset class (12,6) A-vanish (6,0) to exact forced structure. (6) Ground-truth census: all covers of F2^4 (41,341 of 65,536 subsets) and of F2^5 (all C(32,10) = 64,512,240 ten-sets, 317,440 covers of which 99,200 through {0} reproducing PR 2773's n5 control exactly) classified by split and vanishing type: F2^5 ten-covers exist only in splits (2,8)/(4,6)/(6,4)/(8,2), every cover has vanishing characters, and no cover hits a dead class (soundness of the floors on 358,781 real covers). (7) Bounded class-restricted seeded search over all 16 surviving classes (30 restarts each) finds no 18-point cover (best 115..119 of 128) while the identical machinery instantly finds F2^5 covers free and in-class (non-vacuity). No split excluded outright; 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": "f646a7fb75f7d854a881e07fefb13fdfe7631c86", + "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 PR 2911 narrowed the 18-point frontier to four splits with a forced vanishing character on (12,6)/(10,8). This package converts that restriction into an exact class table (six classes impossible, two pinned to forced Sidon structure) and ground-truth census, feeding the word-level L=22 route its per-split feasibility. It changes no supplier, tariff or kappa and instantiates no physical interface.", + "catalog_sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18973161", + "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 classification lemmas with exhaustive machine checks.", + "evidence": "CERTIFICATE.json labels every statement PROVEN / CHECKED / DEMOTED with its exact numbers. vanish.py holds the exact-arithmetic classification engine (character sums, halving, half-decomposition, multi-vanishing grid, class tables with the four floors, tight-class Sidon pinning, the F2^4/F2^5 cover censuses and the class-restricted search). test_engine.py holds 14 tests: exhaustive L2/L3 at m=3 (256x256 pairs), exhaustive L5 and L7 at m=3, the hand-derived class tables for (12,6)/(10,8), the L2 no-vanishing result for (11,7)/(9,9), census soundness and the recorded F2^5 witness classification. verify.py replays four modes (quick / novanish / classify / search) with markers PASS_F7_18POINT_{QUICK,NOVANISH,CLASSIFY,SEARCH}. Vendored byte pins: vendor/agent64_cover17.py 082bc838..., vendor/agent64_search17.py 9eb1bf79..., vendor/cover18.py 24c6a2f4..., 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). No kappa claim.", + "object_synonyms_used_in_overlap": [ + "18-point", + "18point", + "18-set", + "18 point set", + "cover F2^7", + "covers F2^7", + "pair-sum", + "Parseval", + "vanishing character", + "character vanishing", + "hyperplane", + "all-ones hyperplane", + "P + P", + "P+P cover", + "universal word", + "L=22", + "prefix", + "F2^7", + "f(7)", + "Sidon" + ], + "open_questions": [ + { + "blocked_by": "The joint Sidon-pair enumeration size; no structural blocker known.", + "first_step": "Enumerate Sidon pairs D0, D1 of 4-sets in F2^5 with |D0+D1| = 16 and solve the disjointness/translation conditions of L7 against the odd-half A + D = E multiplicities; likewise the full-sumset class (12,6) A-vanish (6,0) (6-set pairs with |X+Y| = 32 in F2^5).", + "question": "Decide the tight classes exactly: are the (10,8) classes A-vanish (7,1) and D-vanish (8,2), and the (12,6) class A-vanish (6,0), realizable by a cover at all?", + "why_it_matters": "Each decided class removes a further slice of the (10,8) resp. (12,6) remainder; a realization would construct an 18-point cover and keep L = 22 alive." + }, + { + "blocked_by": "Nothing structural; a bounded exact enumeration.", + "first_step": "Enumerate the four-part counts (x, y, y, x) of L5 at two characters in surviving classes and intersect the three floor systems with the odd-half multiplicities.", + "question": "Do several simultaneous vanishings (L5's balanced grid) contradict coverage where single vanishings do not?", + "why_it_matters": "The joint vanishing structure is the only exact layer beyond the per-character floors this package pressed." + }, + { + "blocked_by": "Nothing structural; a different identity is needed (the vanishing route is vacuous there by L2).", + "first_step": "Extend the even-half multiplicities or the cross-sum multiplicities of PR 2870's odd-half identity to the (11,7)/(9,9) row remainders (501 and 196 rows of PR 2911).", + "question": "What identity cuts the (11,7)/(9,9) row remainders, where no character can vanish?", + "why_it_matters": "These two splits are untouched by the vanishing restriction and carry the other half of the 18-point question." + } + ], + "original_card": { + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "id": "centre-path-sharing", + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ], + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ] + }, + "outcome": "partial", + "pair_collision_check": { + "checked_utc": "2026-10-16T11:05Z (entry, before computation), 2026-10-16T12:20Z (refined re-run with the object's proper names) and 2026-10-16T12:22Z (pre-submission CLAIM re-check incl. NicholasStone)", + "result": "No claim on the 18-point set object or the vanishing-character classification at any check. Discussion 1317 is silent on this object (bit-mechanism word-model claims only). Discussion 1166's only 18-point posts are the predecessor lineage (KB3c/KB3d/KB3e, all released) and this package's own CLAIM (comment 18973161). Nicholas Stone's claim 18954844 (repeated-state L=20 WORD census) expired 2026-10-15 21:30Z, has no successor claim in the checked window, is a different word-level object, and was re-checked at 12:22Z; this package stays strictly on the SET level. Other recent board activity (petalas PR2925/PR2927 etc.) is on different objects.", + "threads_scanned": [ + "discussion 1317 full thread scan with grep CLAIM|FINDING|HANDOFF|DONE and object terms (18-point|18-set|vanishing|F2|Parseval|pair-sum|L=22|universal word) incl. nested replies; nothing on this object since 2026-10-14", + "discussion 1166 since 2026-10-15T12:00Z with grep CLAIM|FINDING|HANDOFF|DONE, since 2026-10-16T09:00Z and again since 11:00Z with grep CLAIM|NicholasStone (incl. nested replies)" + ], + "tool": "agent_tools.py disc-comments --grep (with nested replies) + scripts/find_overlap.py --refresh with the object's proper names" + }, + "priced_budget_breakdown": "25 min entry overlap, pair-collision checks and the task card; 20 min predecessor extraction, attribution checks and light anchor reproductions; 60 min new machinery (TDD: 14 tests, classification lemmas, class tables, censuses, class-restricted search); 90 min anchor/census walk jobs (both heavy anchors re-walked from empty receipts plus two full C(32,10) census walks, resumable with receipts); 40 min package metadata, registration, gates and submission.", + "priced_budget_minutes": 235, + "priority_revision": 5, + "schema_version": 1, + "scope_change_reason": "Authorized 'explicit open request' scope change, recorded as instructed by the assignment. The chooser (OS nonce fc618722a84313d16975dd03a0d68449, track recursive-interfaces) drew the saturated cards centre-path-sharing / coverage-law-change / connector-alphabet-change (all targeting the selected word's centre path, coverage identity or connector alphabet, not the F2^7 cover question); the assignment (kappa-blocker KB3f) explicitly authorizes taking discussion 1166's open request - PR 2911's open questions 1-2, the vanishing-character route - instead of the drawn card. Pair-collision checks found no claim on this object; Nicholas Stone's concurrent claim (discussion 1166 comment 18954844) is the repeated-state L=20 WORD census and this task stays strictly on the SET-level object.", + "scope_key": "4e44f2900cd2a6a3003d", + "scope_status": "changed", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "session_seed": "fc618722a84313d16975dd03a0d68449", + "smallest_falsifying_instance_first": "The falsifying instance for 'no (12,6)/(10,8) cover exists with a vanishing character' is one covering pair (A, D) in a surviving vanishing class; the class-restricted bounded search attacked exactly those first (16 classes, 30 seeded restarts each, best 115..119 of 128) with non-vacuity controls finding F2^5 covers instantly. Before any new number the recorded predecessor state was reproduced byte-exactly (ANCHOR-REPRO.json): PR 2542/2634 REPRO tiers and L18 census, PR 2870 OBSTRUCTION 696/504/192, PR 2911 SQUEEZE/PROFILE18/NOVANISH/ROWS18 lines, the n5 set controls, and both heavy census anchors re-walked in full from empty receipts. The smallest instances the classification touches are the halved F2^3 problems (checked exhaustively over all 65,536 (A, D) pairs) and the F2^4/F2^5 cover censuses (ground truth for which classes occur).", + "stop_rule": "Stop at the first of: (a) an explicit 18-point covering set in any split (outcome (c) of the assignment), (b) a complete class contradiction excluding (12,6) and/or (10,8) (outcome (a)), or (c) the priced budget expiring with each surviving split's exact obstruction recorded (outcome (c), labelled partial). Outcome (c): the class table (six classes PROVEN impossible, two pinned to forced Sidon structure), the L2 no-vanishing result for (11,7)/(9,9), the ground-truth census and the bounded class-search failures are recorded; no second pivot beyond the class-restricted search was taken.", + "task_id": "centre-path-sharing", + "track": "recursive-interfaces (drawn); scope changed to the assigned explicit open request kappa-blocker KB3f (the vanishing-character classification of the 18-point cover question for F2^7, PR 2911 open questions 1-2)" +} diff --git a/research/f7-18point-vanishing-seedfc618722/VERIFY.json b/research/f7-18point-vanishing-seedfc618722/VERIFY.json new file mode 100644 index 0000000000..4587d23cc3 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/VERIFY.json @@ -0,0 +1,74 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-vanishing-seedfc618722/test_engine.py" + ], + "checks": "14 tests: character sums and halving on the recorded F2^5 subspace witness; L2/L3 exhaustive at m=3 (all 256 x 256 (A, D) pairs) and 4,000 random pairs at m=5; L5 (multi-vanishing balanced grid) and L7 (tight-class Sidon pinning) exhaustive at m=3; the hand-derived class tables for (12,6) and (10,8) including the tight flags; the L2 no-vanishing result for (11,7)/(9,9); dead-class witnesses on every class entry; census consistency (every recorded F2^4 cover covers, no dead-class hits); the recorded F2^5 witness classification (split (4,6), k_A=12, k_D=0, no dead classes); a census shard smoke run; and a class-search smoke run that validates any found pair against the reduction conditions and the forced vanishing split.", + "timeout_seconds": 60 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-vanishing-seedfc618722/verify.py", + "quick" + ], + "checks": "Vendored byte pins (vendor/agent64_cover17.py 082bc838..., vendor/agent64_search17.py 9eb1bf79..., anchors.py 73d73a9b..., vendor/cover18.py 24c6a2f4...); the L2/L3/L5/L7 machine checks; the complete class tables of all four splits (with dead/tight verdicts and the NO-VANISHING line for (11,7)/(9,9)); the F2^4 census soundness; the PR 2911 SQUEEZE table reproduction and the PR 2870 obstruction control (696/504/192); and the heavy-anchor receipt totals (k10b3 149,990,400, k11b4 0, both re-walked from empty receipts). Marker PASS_F7_18POINT_QUICK.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-vanishing-seedfc618722/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_F7_18POINT_NOVANISH.", + "timeout_seconds": 60 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-vanishing-seedfc618722/verify.py", + "classify" + ], + "checks": "The complete ground-truth vanishing census: all 65,536 subsets of F2^4 and all C(32,10) = 64,512,240 ten-sets of F2^5 classified by split and vanishing class (resumable per shard in CENSUS-PROGRESS.json; a replay against the committed receipts validates them, delete the receipt to re-walk). Asserts no cover hits a dead class in any shard, the {0}-slice value 99,200 (PR 2773 n5 control) and the translation identity 317,440 = 99,200 * 32 / 10. Marker PASS_F7_18POINT_CLASSIFY.", + "timeout_seconds": 600 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-vanishing-seedfc618722/verify.py", + "search" + ], + "checks": "The class-restricted bounded searches over all 16 surviving vanishing classes of (12,6)/(10,8) (30 seeded restarts each; a found pair is printed loudly and validated, never asserted against) plus two non-vacuity controls: the free (4,6) search finds a real F2^5 cover and the class search finds one in the census-nonempty class A-vanish (2,4). Marker PASS_F7_18POINT_SEARCH.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "research/f7-18point-vanishing-seedfc618722/vanish.py", + "research/f7-18point-vanishing-seedfc618722/test_engine.py", + "research/f7-18point-vanishing-seedfc618722/verify.py", + "research/f7-18point-vanishing-seedfc618722/anchors.py", + "research/f7-18point-vanishing-seedfc618722/ANCHOR-PROGRESS.json", + "research/f7-18point-vanishing-seedfc618722/CENSUS-PROGRESS.json", + "research/f7-18point-vanishing-seedfc618722/ANCHOR-REPRO.json", + "research/f7-18point-vanishing-seedfc618722/vendor/agent64_cover17.py", + "research/f7-18point-vanishing-seedfc618722/vendor/agent64_search17.py", + "research/f7-18point-vanishing-seedfc618722/vendor/cover18.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/f7-18point-vanishing-seedfc618722/anchors.py b/research/f7-18point-vanishing-seedfc618722/anchors.py new file mode 100644 index 0000000000..d07fa31100 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/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-vanishing-seedfc618722/run_anchors_all.py b/research/f7-18point-vanishing-seedfc618722/run_anchors_all.py new file mode 100644 index 0000000000..8a0384116c --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/run_anchors_all.py @@ -0,0 +1,68 @@ +"""Runner: re-walk both heavy anchors from EMPTY receipts, resumably. + +Repeatedly invokes the byte-vendored anchors.py (per-sub-shard receipts in +ANCHOR-PROGRESS.json) until each mode prints PASS_ANCHORS_. The receipt +file must not exist beforehand: a walk against a committed receipt is receipt +validation, not recomputation (PR 2911's recorded correction). Modes run +sequentially because both write the same receipt file. + +Usage: python3 -I -B run_anchors_all.py [k10b3|k11b4] [--seconds S] +""" + +import subprocess +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PY = sys.executable + +MODES_ALL = ["k10b3", "k11b4"] + + +def run_mode(mode, seconds): + rounds = 0 + while True: + rounds += 1 + t0 = time.time() + proc = subprocess.run( + [PY, "-I", "-B", str(HERE / "anchors.py"), mode, "--seconds", str(seconds)], + capture_output=True, + text=True, + encoding="utf-8", + ) + out = (proc.stdout or "") + (proc.stderr or "") + sys.stdout.write(out) + sys.stdout.flush() + if proc.returncode != 0: + print("ANCHOR_RUNNER %s exit=%d round=%d" % (mode, proc.returncode, rounds)) + return False + if "PASS_ANCHORS_" in out: + print("ANCHOR_RUNNER %s complete rounds=%d" % (mode, rounds), flush=True) + return True + print( + "ANCHOR_RUNNER %s checkpoint round=%d wall=%.1fs" % (mode, rounds, time.time() - t0), + flush=True, + ) + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + args = [a for a in sys.argv[1:] if not a.startswith("--")] + seconds = "540" + if "--seconds" in sys.argv: + seconds = sys.argv[sys.argv.index("--seconds") + 1] + modes = args if args else MODES_ALL + progress = HERE / "ANCHOR-PROGRESS.json" + if not progress.exists(): + print("ANCHOR_RUNNER fresh receipts confirmed (no ANCHOR-PROGRESS.json)", flush=True) + else: + print("ANCHOR_RUNNER WARNING receipts already exist", flush=True) + for mode in modes: + if not run_mode(mode, seconds): + raise SystemExit("anchor mode failed: %s" % mode) + print("ANCHOR_RUNNER ALL COMPLETE", flush=True) + + +if __name__ == "__main__": + main() diff --git a/research/f7-18point-vanishing-seedfc618722/run_classify_all.py b/research/f7-18point-vanishing-seedfc618722/run_classify_all.py new file mode 100644 index 0000000000..c52ce2dd03 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/run_classify_all.py @@ -0,0 +1,55 @@ +"""Runner: complete the F2^5 vanishing census (verify.py classify) resumably. + +Repeatedly invokes verify.py classify (per-shard receipts in +CENSUS-PROGRESS.json) until the PASS_F7_18POINT_CLASSIFY marker appears. +The receipt file must not exist beforehand for a full recomputation. + +Usage: python3 -I -B run_classify_all.py [--seconds S] +""" + +import subprocess +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PY = sys.executable + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + seconds = "540" + if "--seconds" in sys.argv: + seconds = sys.argv[sys.argv.index("--seconds") + 1] + progress = HERE / "CENSUS-PROGRESS.json" + if not progress.exists(): + print("CLASSIFY_RUNNER fresh receipts confirmed (no CENSUS-PROGRESS.json)", flush=True) + else: + print("CLASSIFY_RUNNER WARNING receipts already exist", flush=True) + rounds = 0 + while True: + rounds += 1 + t0 = time.time() + proc = subprocess.run( + [PY, "-I", "-B", str(HERE / "verify.py"), "classify", "--seconds", seconds], + capture_output=True, + text=True, + encoding="utf-8", + ) + out = (proc.stdout or "") + (proc.stderr or "") + sys.stdout.write(out) + sys.stdout.flush() + if proc.returncode != 0: + print("CLASSIFY_RUNNER exit=%d round=%d" % (proc.returncode, rounds)) + raise SystemExit(proc.returncode) + if "PASS_F7_18POINT_CLASSIFY" in out: + print("CLASSIFY_RUNNER complete rounds=%d" % rounds, flush=True) + return + print( + "CLASSIFY_RUNNER checkpoint round=%d wall=%.1fs" % (rounds, time.time() - t0), + flush=True, + ) + + +if __name__ == "__main__": + main() diff --git a/research/f7-18point-vanishing-seedfc618722/test_engine.py b/research/f7-18point-vanishing-seedfc618722/test_engine.py new file mode 100644 index 0000000000..a79e057254 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/test_engine.py @@ -0,0 +1,192 @@ +"""Tests for the KB3f vanishing-character classification engine. + +All exact integer arithmetic. The class-floor table asserted here was derived +by hand from the half-decomposition of the covering conditions (see vanish.py +module docstring); the tests are the machine check. Conventions: E = even +coset of F2^n, isomorphic to F2^(n-1); a "character" is a nontrivial +character of E, represented by its F2^n index v in {1..2^n-2}, paired v ~ +v + (2^n - 1) (both indices restrict to the same character of E); class +counts are at the character (pair) level unless a name says u-level. + +Run: python3 -I -B test_engine.py (expected: Ran N tests ... OK) +""" + +import sys +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +import vanish + + +class TestCharBasics(unittest.TestCase): + def test_char_sum_and_split(self): + # A = span{3, 5} = {0, 3, 5, 6} inside E = F2^5 (even-weight view). + A = [0, 3, 5, 6] + self.assertEqual(vanish.char_sum(A, 0), 4) + # annihilator of A inside F2^5: v with base 7 and free bits 3, 4 + ann = {0, 7, 8, 15, 16, 23, 24, 31} + for v in range(1, 32): + cs = vanish.char_sum(A, v) + if v in ann: + self.assertEqual(cs, 4, v) + else: + self.assertEqual(cs, 0, v) + van_u = vanish.vanishing_set_u(A, 5) + self.assertEqual(len(van_u), 24) # 30 u's off {0, 31} minus 6 annihilators + self.assertEqual(van_u, {v for v in range(1, 31) if v not in ann}) + van_e = vanish.vanishing_set(A, 5) + self.assertEqual(len(van_e), 12) # character (pair) level + + def test_split_sizes(self): + A = [0, 3, 5, 6] + # v = 1 (bit 0): dots 1 on {3, 5}, 0 on {0, 6} + self.assertEqual(vanish.split_sizes(A, 1, 5), (2, 2)) + self.assertEqual(vanish.split_sizes(A, 8, 5), (4, 0)) + + +class TestHalfDecomposition(unittest.TestCase): + def test_lemma_exhaustive_f2_3(self): + """L2 (halving) and L3 (half-decomposition of coverage) hold for + every (A, D) pair inside E = F2^3 (256 x 256 pairs).""" + res = vanish.check_half_decomposition(3, exhaustive=True) + self.assertTrue(res["ok"]) + self.assertEqual(res["pairs"], 256 * 256) + + def test_lemma_samples_f2_5(self): + res = vanish.check_half_decomposition(5, exhaustive=False, samples=4000, seed=7) + self.assertTrue(res["ok"]) + self.assertEqual(res["pairs"], 4000) + + def test_multi_vanishing_structure_exhaustive_f2_3(self): + """L5: two simultaneous vanishings force the balanced grid.""" + res = vanish.check_multi_vanishing(3) + self.assertTrue(res["ok"]) + self.assertGreater(res["checked"], 0) + + def test_tight_equality_exhaustive_f2_3(self): + """L7: floor equality plus coverage forces Sidon cross sums.""" + res = vanish.check_tight_equality(3) + self.assertTrue(res["ok"]) + self.assertGreater(res["checked"], 0) + + +class TestClassFloors(unittest.TestCase): + """Exact class table: a vanishing character psi forces the vanishing + side to split equally across ker(psi); even-mask coverage of the odd + side of ker(psi) inside E forces a0*a1 + d0*d1 >= 2^(m-1) (m = 6 here: + the 18-point problem's E = F2^6).""" + + def test_floor_values_12_6(self): + tab = vanish.class_table(12, 6, m=6) + surv = {(c["other_split"][0], c["other_split"][1]): c["verdict"] for c in tab["A_vanish"]} + self.assertEqual( + surv, + {(6, 0): "survives", (5, 1): "survives", (4, 2): "survives", (3, 3): "survives"}, + ) + surv = {(c["other_split"][0], c["other_split"][1]): c["verdict"] for c in tab["D_vanish"]} + self.assertEqual( + surv, + { + (12, 0): "dead", + (11, 1): "dead", + (10, 2): "dead", + (9, 3): "survives", + (8, 4): "survives", + (7, 5): "survives", + (6, 6): "survives", + }, + ) + + def test_floor_values_10_8(self): + tab = vanish.class_table(10, 8, m=6) + surv = {(c["other_split"][0], c["other_split"][1]): c["verdict"] for c in tab["A_vanish"]} + self.assertEqual( + surv, + {(8, 0): "dead", (7, 1): "survives", (6, 2): "survives", (5, 3): "survives", (4, 4): "survives"}, + ) + surv = {(c["other_split"][0], c["other_split"][1]): c["verdict"] for c in tab["D_vanish"]} + self.assertEqual( + surv, + { + (10, 0): "dead", + (9, 1): "dead", + (8, 2): "survives", + (7, 3): "survives", + (6, 4): "survives", + (5, 5): "survives", + }, + ) + tight = sorted( + [c["other_split"] for c in tab["A_vanish"] + tab["D_vanish"] if c["tight"]] + ) + self.assertEqual(tight, [(7, 1), (8, 2)]) + + def test_dead_classes_have_witness(self): + for (s, t) in ((12, 6), (10, 8)): + for side in ("A_vanish", "D_vanish"): + for c in vanish.class_table(s, t, m=6)[side]: + if c["verdict"] == "dead": + self.assertLess(c["floor_value"], c["floor_need"], c) + else: + self.assertGreaterEqual(c["floor_value"], c["floor_need"], c) + + def test_11_7_and_9_9_no_vanishing(self): + for (s, t) in ((11, 7), (9, 9)): + tab = vanish.class_table(s, t, m=6) + self.assertEqual(tab["A_vanish"], []) + self.assertEqual(tab["D_vanish"], []) + self.assertFalse(tab["vanishing_possible"]) + + +class TestFloorsSoundOnRealCovers(unittest.TestCase): + def test_f2_4_census_consistent(self): + rec = vanish.census_f4() + for cov in rec["covers"]: + self.assertTrue(vanish.covers_f2n(cov, 4)) + self.assertGreater(rec["covers_total"], 0) + self.assertEqual(rec["dead_classes_hit"], []) + + def test_f2_5_subspace_example_classified(self): + # recorded real 10-point cover of F2^5 (PR 2773 n5 control witness): + # split (4, 6); A = span{3, 5} is a subspace, so A vanishes on every + # character outside its annihilator; D = 1 + B vanishes on none. + S = [0, 1, 2, 3, 4, 5, 6, 8, 16, 31] + rec = vanish.classify_cover(S, 5) + self.assertEqual(rec["split"], (4, 6)) + self.assertEqual(rec["k_A"], 12) # character level: 15 - 3 annihilator pairs + self.assertEqual(rec["k_D"], 0) + self.assertEqual(rec["dead_classes_hit"], []) + # at every A-vanishing character L2 forces the A split (2, 2); the + # D split must pass the class floor of F2^4 (need 8). + self.assertEqual(len(rec["vanish_rows"]), 12) + for (psi, side, a_sp, d_sp, verdict) in rec["vanish_rows"]: + self.assertEqual(side, "A") + self.assertEqual(a_sp, (2, 2)) + self.assertEqual(verdict, "survives") + + +class TestCensusF5(unittest.TestCase): + def test_census_shard_smoke(self): + rec = vanish.census_f5(shard=0, shards=16, keep_covers=5, max_combos=100000) + self.assertIn(rec["status"], ("complete", "partial")) + self.assertGreater(rec["combos"], 0) + for cov in rec["covers"]: + self.assertTrue(vanish.covers_f2n(cov, 5)) + self.assertEqual(rec["dead_classes_hit"], []) + + +class TestClassSearch(unittest.TestCase): + def test_class_search_smoke(self): + res = vanish.search_class(12, 6, side="A_vanish", other_split=(3, 3), restarts=2, seed=3, seconds=3.0) + self.assertIn("found", res) + if res["found"]: + A, D = res["A"], res["D"] + ok1, ok2 = vanish.cover_conditions(A, D, 6) + self.assertTrue(ok1 and ok2) + self.assertEqual(vanish.split_sizes(A, 1, 6), (6, 6)) # forced vanishing side + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/f7-18point-vanishing-seedfc618722/vanish.py b/research/f7-18point-vanishing-seedfc618722/vanish.py new file mode 100644 index 0000000000..2dca0053f3 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/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-vanishing-seedfc618722/vendor/agent64_cover17.py b/research/f7-18point-vanishing-seedfc618722/vendor/agent64_cover17.py new file mode 100644 index 0000000000..5add3747a3 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/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-vanishing-seedfc618722/vendor/agent64_search17.py b/research/f7-18point-vanishing-seedfc618722/vendor/agent64_search17.py new file mode 100644 index 0000000000..ef17635967 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/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-vanishing-seedfc618722/vendor/cover18.py b/research/f7-18point-vanishing-seedfc618722/vendor/cover18.py new file mode 100644 index 0000000000..3faa640d79 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/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-vanishing-seedfc618722/verify.py b/research/f7-18point-vanishing-seedfc618722/verify.py new file mode 100644 index 0000000000..61b53bbcd2 --- /dev/null +++ b/research/f7-18point-vanishing-seedfc618722/verify.py @@ -0,0 +1,310 @@ +"""Registered replay for the KB3f package (vanishing-character classification +for the 18-point cover question, F2^7). + +Modes (each bounded; see VERIFY.json): + + quick vendored byte pins, the half-decomposition lemma exhaustive at + n = 3, the class tables for all four splits, the F2^4 census + soundness, the SQUEEZE reproduction of the PR 2911 split table, + and the heavy-anchor receipt totals. + marker PASS_F7_18POINT_QUICK + novanish reproduction of the load-bearing PR 2911 NOVANISH premise + (any (12,6) or (10,8) cover has a vanishing character off the + all-ones hyperplane) from the byte-vendored PR 2911 engine. + marker PASS_F7_18POINT_NOVANISH + classify the ground-truth vanishing census: all covers of F2^4 (complete) + and all 10-point covers of F2^5 (complete C(32,10) enumeration, + resumable per shard in CENSUS-PROGRESS.json; one invocation runs + shards until its time budget, re-invoke to continue). + marker PASS_F7_18POINT_CLASSIFY + search the class-restricted bounded searches (a found pair is printed + loudly; a failed bounded search is never an exclusion) plus a + non-vacuity control on F2^5. + marker PASS_F7_18POINT_SEARCH + +Everything is exact integer arithmetic (no floats). +""" + +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 vanish # noqa: E402 + +VENDOR_PINS = { + "vendor/agent64_cover17.py": ( + "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654" + ), + "vendor/agent64_search17.py": ( + "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674" + ), + "anchors.py": "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7", + "vendor/cover18.py": ( + "24c6a2f4911dc2d5de76972eb5ae93dc4e66d8fa1e904443de6d0638e70c0a04" + ), +} + +SPLITS = [(12, 6), (11, 7), (10, 8), (9, 9)] + + +def check_pins(): + for rel, want in VENDOR_PINS.items(): + got = vanish.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() + res = vanish.check_half_decomposition(3, exhaustive=True) + assert res["ok"], res + print("LEMMA half-decomposition exhaustive m=3 pairs=%d ok=true" % res["pairs"], flush=True) + res5 = vanish.check_multi_vanishing(3) + assert res5["ok"], res5 + print("LEMMA multi-vanishing grid exhaustive m=3 pairs=%d ok=true" % res5["checked"], 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) + 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 floors=%s value=%d need=%d -> %s%s" + % ( + s, + t, + side, + c["vanishing_split"], + c["other_split"], + c["floors"], + 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, + ) + rec = vanish.census_f4() + assert rec["dead_classes_hit"] == [], rec["dead_classes_hit"] + print( + "CENSUS f2^4 covers=%d (dead classes hit: none) agg=%s" + % (rec["covers_total"], rec["agg"]), + flush=True, + ) + # SQUEEZE reproduction of the PR 2911 split table (byte-vendored engine). + import cover18 as c18 + + for (s, t) in SPLITS + [(11, 6)]: + sq = c18.squeeze_numbers(7, s, t) + sides = sq["sides"] + line = " ".join( + "%s rem=%s max_char=%s allowed=%s deficit=%s" + % ( + x["side"], + x["parseval_remainder"], + x["max_char"], + x["max_allowed"], + x["deficit"], + ) + for x in sides + ) + print( + "SQUEEZE (%d, %d) eo=%d opposite_parity=%s contradiction=%s | %s" + % (s, t, sq["odd_excess"], sq["opposite_parity"], sq["contradiction"], line), + flush=True, + ) + 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 (this package's own fresh-receipt re-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 (re-walked from empty receipts)" + % (mode, sum(mrec["total_hist"].values()), mrec["total_hist"], len(mrec["shards"])), + flush=True, + ) + print("PASS_F7_18POINT_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_F7_18POINT_NOVANISH seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_classify(budget=540.0): + t0 = time.time() + rec4 = vanish.census_f4() + assert rec4["dead_classes_hit"] == [] + print( + "CENSUS f2^4 covers=%d agg=%s class_agg=%s" + % (rec4["covers_total"], rec4["agg"], rec4["class_agg"]), + flush=True, + ) + prog_path = HERE / "CENSUS-PROGRESS.json" + prog = {"shards": {}} + if prog_path.exists(): + prog = json.loads(prog_path.read_text(encoding="utf-8")) + shards = 32 + for shard in range(shards): + key = str(shard) + if key in prog["shards"]: + continue + sres = vanish.census_f5(shard=shard, shards=shards, keep_covers=3) + assert sres["dead_classes_hit"] == [], (shard, sres["dead_classes_hit"][:3]) + prog["shards"][key] = { + "combos": sres["combos"], + "covers_total": sres["covers_total"], + "agg": sres["agg"], + "class_agg": sres["class_agg"], + "covers": sres["covers"], + } + prog_path.write_text(json.dumps(prog, indent=2, sort_keys=True), encoding="utf-8") + print( + "CENSUS f2^5 shard=%d/%d combos=%d covers=%d" + % (shard, shards, sres["combos"], sres["covers_total"]), + flush=True, + ) + if time.time() - t0 > budget: + print( + "RECEIPT classify checkpoint shards=%d/%d" % (len(prog["shards"]), shards), + flush=True, + ) + return + # full aggregation over all shards + total_covers = sum(r["covers_total"] for r in prog["shards"].values()) + total_combos = sum(r["combos"] for r in prog["shards"].values()) + agg = {} + class_agg = {} + for r in prog["shards"].values(): + for item, cnt in r["agg"]: + agg[item] = agg.get(item, 0) + cnt + for item, cnt in r["class_agg"]: + class_agg[item] = class_agg.get(item, 0) + cnt + prog["complete"] = True + prog["total_combos"] = total_combos + prog["total_covers"] = total_covers + prog_path.write_text(json.dumps(prog, indent=2, sort_keys=True), encoding="utf-8") + print("CENSUS f2^5 combos=%d covers=%d" % (total_combos, total_covers), flush=True) + for item in sorted(agg): + print("CENSUS-SPLIT %s count=%d" % (item, agg[item]), flush=True) + for item in sorted(class_agg): + print("CENSUS-CLASS %s count=%d" % (item, class_agg[item]), flush=True) + # PR 2773's n5 control counts covers through {0} (its engine fixes 0 in + # every draw); shard 0 of this un-normalized enumeration is exactly the + # 0-containing slice, and 99,200 * 32 / 10 = 317,440 is the full count. + covers_through_0 = prog["shards"]["0"]["covers_total"] + assert covers_through_0 == 99200, covers_through_0 + assert total_covers * 10 == covers_through_0 * 32, (total_covers, covers_through_0) + print( + "CONTROL PR2773 n5 control value reproduced: %d ten-point covers through {0}" + " (all translations %d = %d * 32 / 10)" + % (covers_through_0, total_covers, covers_through_0), + flush=True, + ) + print("PASS_F7_18POINT_CLASSIFY seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_search(): + t0 = time.time() + jobs = [] + for (s, t) in SPLITS: + tab = vanish.class_table(s, t, m=6) + for c in tab["A_vanish"]: + if c["verdict"] == "dead": + continue + jobs.append((s, t, "A_vanish", c["other_split"])) + for c in tab["D_vanish"]: + if c["verdict"] == "dead": + continue + jobs.append((s, t, "D_vanish", c["other_split"])) + found_any = False + for idx, (s, t, side, other) in enumerate(jobs): + res = vanish.search_class( + s, t, side=side, other_split=other, restarts=30, seed=7000 + idx, seconds=25.0 + ) + print( + "SEARCH-CLASS (%d,%d) %s other=%s found=%s score=%s/%d moves=%s" + % (s, t, side, other, res["found"], res["score"], 128, res.get("moves")), + flush=True, + ) + if res["found"]: + found_any = True + print("SEARCH-CLASS FOUND A=%s D=%s" % (res["A"], res["D"]), flush=True) + # non-vacuity: the same machinery finds a real (4,6) cover of F2^4 = E of + # F2^5 fast (the (A, D) reduction of an F2^n cover lives in E = F2^(n-1)) + res = vanish.search_free(4, 6, restarts=40, seed=5, seconds=20.0, m=4) + print( + "CONTROL search_free m=4 (4,6) found=%s score=%s/%d (non-vacuity)" + % (res["found"], res["score"], 32), + flush=True, + ) + if res["found"]: + print("CONTROL search_free cover A=%s D=%s" % (res["A"], res["D"]), flush=True) + assert res["found"], "class machinery must find known 10-point covers of F2^5" + # class-restricted non-vacuity: the census proves this class nonempty + res = vanish.search_class(4, 6, side="A_vanish", other_split=(2, 4), restarts=40, seed=6, seconds=20.0, m=4) + print( + "CONTROL search_class m=4 (4,6) A_vanish other=(2,4) found=%s score=%s/%d" + % (res["found"], res["score"], 32), + flush=True, + ) + assert res["found"], "class search must find a cover in a census-nonempty class" + print("PASS_F7_18POINT_SEARCH seconds=%.1f found_18=%s" % (time.time() - t0, found_any), 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 == "classify": + budget = 540.0 + if "--seconds" in sys.argv: + budget = float(sys.argv[sys.argv.index("--seconds") + 1]) + mode_classify(budget) + elif mode == "search": + mode_search() + else: + raise SystemExit("usage: verify.py quick|novanish|classify|search [--seconds S]") + + +if __name__ == "__main__": + main()