From cfb813f883e61519deedcd84151dc0c68b9d19cc Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Fri, 16 Oct 2026 06:15:43 -0400 Subject: [PATCH] KB3e: 18-point cover question for F2^7 narrowed to an exact finite remainder (outcome=partial, no new kappa) Set-level package research/f7-18point-cover-question-seed6d34356c: does any 18-point set S cover F2^7 (P + P = F2^7 in the PR943 prefix-walk model)? Not decided - no cover constructed, no split excluded - but narrowed with each surviving split's exact obstruction recorded. - All recorded anchors reproduced first: PR 2542/2634 REPRO tiers 945/31, 10395/49, 945945/59 and the L18 census 15,775,992 / 312,064 / 0; PR 2870 OBSTRUCTION lines parseval=696 allowed=504 deficit=192; PR 2773 k10 budget-3 = 149,990,400 and k11 levels 3-4 = 0 both recomputed in full by fresh empty-receipt walks (PASS_ANCHORS_K10B3 / PASS_ANCHORS_K11B4, 62/62 sub-shards each). - The PR 2870 Fourier/Parseval squeeze re-derived for (12,6),(11,7),(10,8), (9,9) with the deficit tracked: its opposite-parity hypothesis fails on all four splits and the deficits are non-positive. - A per-character profile system excludes no 18-point split but PROVES that any (12,6) or (10,8) cover must have a vanishing character off the all-ones hyperplane (no-vanishing forces sum rho^2 = 46 at (12,6), not an attainable partition square sum). - Pair-representation rows with the reproduced census floors leave 808 / 501 / 251 / 196 surviving rows ((12,6)/(11,7)/(10,8)/(9,9)). - Bounded seeded search: no 18-point cover (best 118/128 at k=18; k=20 non-vacuity control finds covers in 5/5 short runs). Vendor pins byte-exact from PR 2773/PR 2870 with credit; 21 tests; registered replay PASS_PACKAGE_METADATA_AND_PINS. --- .../ANCHOR-PROGRESS.json | 1310 +++++++++++++++++ .../ANCHOR-REPRO.json | 42 + .../CERTIFICATE.json | 77 + .../NOTICE.md | 55 + .../README.md | 199 +++ .../SOURCES.json | 102 ++ .../TASK-CARD.md | 86 ++ .../TASK.json | 119 ++ .../VERIFY.json | 72 + .../anchors.py | 128 ++ .../cover18.py | 741 ++++++++++ .../test_engine.py | 209 +++ .../vendor/agent64_cover17.py | 263 ++++ .../vendor/agent64_search17.py | 330 +++++ .../verify.py | 201 +++ 15 files changed, 3934 insertions(+) create mode 100644 research/f7-18point-cover-question-seed6d34356c/ANCHOR-PROGRESS.json create mode 100644 research/f7-18point-cover-question-seed6d34356c/ANCHOR-REPRO.json create mode 100644 research/f7-18point-cover-question-seed6d34356c/CERTIFICATE.json create mode 100644 research/f7-18point-cover-question-seed6d34356c/NOTICE.md create mode 100644 research/f7-18point-cover-question-seed6d34356c/README.md create mode 100644 research/f7-18point-cover-question-seed6d34356c/SOURCES.json create mode 100644 research/f7-18point-cover-question-seed6d34356c/TASK-CARD.md create mode 100644 research/f7-18point-cover-question-seed6d34356c/TASK.json create mode 100644 research/f7-18point-cover-question-seed6d34356c/VERIFY.json create mode 100644 research/f7-18point-cover-question-seed6d34356c/anchors.py create mode 100644 research/f7-18point-cover-question-seed6d34356c/cover18.py create mode 100644 research/f7-18point-cover-question-seed6d34356c/test_engine.py create mode 100644 research/f7-18point-cover-question-seed6d34356c/vendor/agent64_cover17.py create mode 100644 research/f7-18point-cover-question-seed6d34356c/vendor/agent64_search17.py create mode 100644 research/f7-18point-cover-question-seed6d34356c/verify.py diff --git a/research/f7-18point-cover-question-seed6d34356c/ANCHOR-PROGRESS.json b/research/f7-18point-cover-question-seed6d34356c/ANCHOR-PROGRESS.json new file mode 100644 index 0000000000..fb725276db --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/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": 143.08 + }, + "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": 84.58 + }, + "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": 80.21 + }, + "v0=17": { + "examples": { + "3": [ + 0, + 3, + 17, + 18, + 20, + 24, + 33, + 46, + 65, + 92 + ] + }, + "hist": { + "3": 8782848 + }, + "seconds": 69.42 + }, + "v0=18": { + "examples": { + "3": [ + 0, + 3, + 18, + 20, + 23, + 24, + 33, + 40, + 65, + 92 + ] + }, + "hist": { + "3": 8455680 + }, + "seconds": 64.71 + }, + "v0=20": { + "examples": { + "3": [ + 0, + 3, + 20, + 23, + 24, + 29, + 33, + 39, + 65, + 80 + ] + }, + "hist": { + "3": 6200832 + }, + "seconds": 52.13 + }, + "v0=23": { + "examples": { + "3": [ + 0, + 3, + 23, + 24, + 27, + 29, + 33, + 40, + 65, + 80 + ] + }, + "hist": { + "3": 5956608 + }, + "seconds": 48.63 + }, + "v0=24": { + "examples": { + "3": [ + 0, + 3, + 24, + 27, + 29, + 33, + 40, + 65, + 75, + 101 + ] + }, + "hist": { + "3": 4402176 + }, + "seconds": 37.7 + }, + "v0=27": { + "examples": { + "3": [ + 0, + 3, + 27, + 29, + 30, + 33, + 40, + 65, + 75, + 101 + ] + }, + "hist": { + "3": 4217856 + }, + "seconds": 35.5 + }, + "v0=29": { + "examples": { + "3": [ + 0, + 3, + 29, + 30, + 33, + 36, + 40, + 46, + 65, + 80 + ] + }, + "hist": { + "3": 3225600 + }, + "seconds": 28.66 + }, + "v0=30": { + "examples": { + "3": [ + 0, + 3, + 30, + 33, + 34, + 36, + 40, + 48, + 65, + 78 + ] + }, + "hist": { + "3": 3078144 + }, + "seconds": 26.36 + }, + "v0=33": { + "examples": { + "3": [ + 0, + 3, + 33, + 34, + 36, + 40, + 48, + 63, + 65, + 108 + ] + }, + "hist": { + "3": 2860032 + }, + "seconds": 23.63 + }, + "v0=34": { + "examples": { + "3": [ + 0, + 3, + 34, + 36, + 39, + 40, + 48, + 57, + 65, + 108 + ] + }, + "hist": { + "3": 2736384 + }, + "seconds": 22.79 + }, + "v0=36": { + "examples": { + "3": [ + 0, + 3, + 36, + 39, + 40, + 45, + 48, + 54, + 65, + 96 + ] + }, + "hist": { + "3": 1930752 + }, + "seconds": 17.0 + }, + "v0=39": { + "examples": { + "3": [ + 0, + 3, + 39, + 40, + 43, + 45, + 48, + 57, + 65, + 96 + ] + }, + "hist": { + "3": 1837824 + }, + "seconds": 15.61 + }, + "v0=40": { + "examples": { + "3": [ + 0, + 3, + 40, + 43, + 45, + 48, + 57, + 65, + 75, + 116 + ] + }, + "hist": { + "3": 1306368 + }, + "seconds": 11.6 + }, + "v0=43": { + "examples": { + "3": [ + 0, + 3, + 43, + 45, + 46, + 48, + 57, + 65, + 75, + 116 + ] + }, + "hist": { + "3": 1234944 + }, + "seconds": 11.17 + }, + "v0=45": { + "examples": { + "3": [ + 0, + 3, + 45, + 46, + 48, + 53, + 57, + 63, + 65, + 96 + ] + }, + "hist": { + "3": 917760 + }, + "seconds": 7.78 + }, + "v0=46": { + "examples": { + "3": [ + 0, + 3, + 46, + 48, + 51, + 53, + 57, + 65, + 78, + 101 + ] + }, + "hist": { + "3": 858624 + }, + "seconds": 7.16 + }, + "v0=48": { + "examples": { + "3": [ + 0, + 3, + 48, + 51, + 53, + 57, + 65, + 78, + 80, + 108 + ] + }, + "hist": { + "3": 609792 + }, + "seconds": 5.74 + }, + "v0=5": { + "examples": { + "3": [ + 0, + 3, + 5, + 6, + 9, + 17, + 33, + 58, + 65, + 92 + ] + }, + "hist": { + "3": 19353600 + }, + "seconds": 134.07 + }, + "v0=51": { + "examples": { + "3": [ + 0, + 3, + 51, + 53, + 54, + 57, + 65, + 72, + 80, + 108 + ] + }, + "hist": { + "3": 562176 + }, + "seconds": 5.29 + }, + "v0=53": { + "examples": { + "3": [ + 0, + 3, + 53, + 54, + 57, + 60, + 65, + 71, + 80, + 96 + ] + }, + "hist": { + "3": 457728 + }, + "seconds": 3.72 + }, + "v0=54": { + "examples": { + "3": [ + 0, + 3, + 54, + 57, + 58, + 60, + 65, + 72, + 80, + 96 + ] + }, + "hist": { + "3": 413184 + }, + "seconds": 3.25 + }, + "v0=57": { + "examples": { + "3": [ + 0, + 3, + 57, + 58, + 65, + 68, + 72, + 78, + 80, + 96 + ] + }, + "hist": { + "3": 340992 + }, + "seconds": 2.48 + }, + "v0=58": { + "examples": { + "3": [ + 0, + 3, + 58, + 60, + 65, + 66, + 72, + 77, + 80, + 96 + ] + }, + "hist": { + "3": 297984 + }, + "seconds": 2.32 + }, + "v0=6": { + "examples": { + "3": [ + 0, + 3, + 6, + 9, + 10, + 17, + 33, + 53, + 65, + 92 + ] + }, + "hist": { + "3": 18708480 + }, + "seconds": 129.57 + }, + "v0=60": { + "examples": { + "3": [ + 0, + 3, + 60, + 63, + 65, + 68, + 72, + 78, + 80, + 96 + ] + }, + "hist": { + "3": 258048 + }, + "seconds": 2.0 + }, + "v0=63": { + "examples": { + "3": [ + 0, + 3, + 63, + 65, + 66, + 68, + 72, + 80, + 95, + 101 + ] + }, + "hist": { + "3": 215040 + }, + "seconds": 1.51 + }, + "v0=65": { + "examples": { + "3": [ + 0, + 3, + 65, + 68, + 72, + 77, + 80, + 86, + 96, + 106 + ] + }, + "hist": { + "3": 80640 + }, + "seconds": 1.18 + }, + "v0=66": { + "examples": { + "3": [ + 0, + 3, + 66, + 68, + 72, + 77, + 80, + 85, + 96, + 123 + ] + }, + "hist": { + "3": 80640 + }, + "seconds": 1.07 + }, + "v0=68": { + "examples": { + "3": [ + 0, + 3, + 68, + 72, + 77, + 80, + 85, + 90, + 96, + 102 + ] + }, + "hist": { + "3": 43008 + }, + "seconds": 0.68 + }, + "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.39 + }, + "v0=75": { + "examples": { + "3": [ + 0, + 3, + 75, + 77, + 80, + 85, + 89, + 92, + 96, + 106 + ] + }, + "hist": { + "3": 21504 + }, + "seconds": 0.36 + }, + "v0=77": { + "examples": { + "3": [ + 0, + 3, + 77, + 80, + 85, + 89, + 95, + 96, + 101, + 123 + ] + }, + "hist": { + "3": 10368 + }, + "seconds": 0.24 + }, + "v0=78": { + "examples": { + "3": [ + 0, + 3, + 78, + 80, + 85, + 89, + 95, + 96, + 101, + 120 + ] + }, + "hist": { + "3": 10368 + }, + "seconds": 0.18 + }, + "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.09 + }, + "v0=85": { + "examples": { + "3": [ + 0, + 3, + 85, + 89, + 92, + 96, + 101, + 106, + 113, + 119 + ] + }, + "hist": { + "3": 1536 + }, + "seconds": 0.06 + }, + "v0=86": { + "examples": { + "3": [ + 0, + 3, + 86, + 89, + 92, + 96, + 101, + 105, + 113, + 119 + ] + }, + "hist": { + "3": 1536 + }, + "seconds": 0.05 + }, + "v0=89": { + "examples": { + "3": [ + 0, + 3, + 89, + 92, + 96, + 102, + 105, + 111, + 113, + 123 + ] + }, + "hist": { + "3": 384 + }, + "seconds": 0.03 + }, + "v0=9": { + "examples": { + "3": [ + 0, + 3, + 9, + 10, + 12, + 17, + 33, + 53, + 65, + 86 + ] + }, + "hist": { + "3": 14923776 + }, + "seconds": 114.1 + }, + "v0=90": { + "examples": { + "3": [ + 0, + 3, + 90, + 92, + 96, + 101, + 105, + 108, + 113, + 123 + ] + }, + "hist": { + "3": 384 + }, + "seconds": 0.03 + }, + "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": 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": 156.63 + }, + "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": 122.13 + }, + "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": 152.71 + }, + "v0=17": { + "examples": {}, + "hist": {}, + "seconds": 151.73 + }, + "v0=18": { + "examples": {}, + "hist": {}, + "seconds": 140.51 + }, + "v0=20": { + "examples": {}, + "hist": {}, + "seconds": 105.0 + }, + "v0=23": { + "examples": {}, + "hist": {}, + "seconds": 101.39 + }, + "v0=24": { + "examples": {}, + "hist": {}, + "seconds": 56.99 + }, + "v0=27": { + "examples": {}, + "hist": {}, + "seconds": 49.4 + }, + "v0=29": { + "examples": {}, + "hist": {}, + "seconds": 38.23 + }, + "v0=30": { + "examples": {}, + "hist": {}, + "seconds": 35.58 + }, + "v0=33": { + "examples": {}, + "hist": {}, + "seconds": 32.37 + }, + "v0=34": { + "examples": {}, + "hist": {}, + "seconds": 30.0 + }, + "v0=36": { + "examples": {}, + "hist": {}, + "seconds": 21.52 + }, + "v0=39": { + "examples": {}, + "hist": {}, + "seconds": 20.49 + }, + "v0=40": { + "examples": {}, + "hist": {}, + "seconds": 13.89 + }, + "v0=43": { + "examples": {}, + "hist": {}, + "seconds": 13.95 + }, + "v0=45": { + "examples": {}, + "hist": {}, + "seconds": 9.48 + }, + "v0=46": { + "examples": {}, + "hist": {}, + "seconds": 8.76 + }, + "v0=48": { + "examples": {}, + "hist": {}, + "seconds": 6.87 + }, + "v0=5": { + "examples": {}, + "hist": {}, + "seconds": 209.54 + }, + "v0=51": { + "examples": {}, + "hist": {}, + "seconds": 5.66 + }, + "v0=53": { + "examples": {}, + "hist": {}, + "seconds": 4.26 + }, + "v0=54": { + "examples": {}, + "hist": {}, + "seconds": 3.75 + }, + "v0=57": { + "examples": {}, + "hist": {}, + "seconds": 2.83 + }, + "v0=58": { + "examples": {}, + "hist": {}, + "seconds": 2.51 + }, + "v0=6": { + "examples": {}, + "hist": {}, + "seconds": 199.56 + }, + "v0=60": { + "examples": {}, + "hist": {}, + "seconds": 1.98 + }, + "v0=63": { + "examples": {}, + "hist": {}, + "seconds": 1.75 + }, + "v0=65": { + "examples": {}, + "hist": {}, + "seconds": 1.17 + }, + "v0=66": { + "examples": {}, + "hist": {}, + "seconds": 1.13 + }, + "v0=68": { + "examples": {}, + "hist": {}, + "seconds": 0.67 + }, + "v0=71": { + "examples": {}, + "hist": {}, + "seconds": 0.61 + }, + "v0=72": { + "examples": {}, + "hist": {}, + "seconds": 0.36 + }, + "v0=75": { + "examples": {}, + "hist": {}, + "seconds": 0.32 + }, + "v0=77": { + "examples": {}, + "hist": {}, + "seconds": 0.18 + }, + "v0=78": { + "examples": {}, + "hist": {}, + "seconds": 0.18 + }, + "v0=80": { + "examples": {}, + "hist": {}, + "seconds": 0.1 + }, + "v0=83": { + "examples": {}, + "hist": {}, + "seconds": 0.08 + }, + "v0=85": { + "examples": {}, + "hist": {}, + "seconds": 0.04 + }, + "v0=86": { + "examples": {}, + "hist": {}, + "seconds": 0.03 + }, + "v0=89": { + "examples": {}, + "hist": {}, + "seconds": 0.02 + }, + "v0=9": { + "examples": {}, + "hist": {}, + "seconds": 166.75 + }, + "v0=90": { + "examples": {}, + "hist": {}, + "seconds": 0.01 + }, + "v0=92": { + "examples": {}, + "hist": {}, + "seconds": 0.01 + }, + "v0=95": { + "examples": {}, + "hist": {}, + "seconds": 0.01 + }, + "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-cover-question-seed6d34356c/ANCHOR-REPRO.json b/research/f7-18point-cover-question-seed6d34356c/ANCHOR-REPRO.json new file mode 100644 index 0000000000..a18001b217 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/ANCHOR-REPRO.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "recorded_utc": "2026-10-16T10:05:00Z", + "environment": "CPython 3.12.13 (C:/Users/warha/.local/bin/python3.12.exe), Windows, stdlib only; concurrent research agents on the host, so wall times are inflated versus PR 2870's receipt timings", + "predecessor_packages_extracted": "PR 2542 research/universal-f7-singleton-seedb859517b (head 3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf), PR 2634 research/universal-f7-singleton-l20-seed06704c39 (head e2f30d93efbef5658334072aa855aa95e795e394), PR 2773 research/f7-17point-cover-audit-seedcfa215c2 (head 6739c799799621878a9249c93e2b12cc799c1482), PR 2870 research/f7-17point-fourier-obstruction-seedb5e318fe (head 9f55f291e9e79e628fd98f1e4f4debfc1c2106e5); all extracted byte-exactly with agent_tools.py pr-tree-extract into a temp scratch area and run from there against a byte-identical copy of the pinned research/universal-connector-six-source/EXPECTED.json (SHA-256 f1b1bec330640c81ac0da25ee8b3a0a49fe9ea5bb2eadaaa787c64bd62c9e73a)", + "commands_run_in_session": [ + "python3.12 -I -B /pr2773/verify.py", + "python3.12 -I -B /pr2773/independent.py", + "python3.12 -I -B /pr2870/test_engine.py", + "python3.12 -I -B /pr2870/verify.py", + "python3.12 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k10b3 --seconds 520 (repeated; resumable)", + "python3.12 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k11b4 --seconds 520 (repeated; resumable)" + ], + "observed_outputs": { + "tiers_and_l18": "PIN vendor/pr2542_engine.py sha256=82e4c407b58864c7; REPRO n=5 L=10 words=945 max=31 sha=3dcc5689a4a34bae; REPRO n=6 L=12 words=10395 max=49 sha=491b295f12cfa34a; REPRO n=6 L=14 words=945945 max=59 sha=3d711ffa19209310; REPRO PR2542 L18 nodes=15775992 cycles=312064 universal_words=0 (fresh re-run of the vendored PR 2542 engine inside PR 2773's verify.py)", + "row_table": "ROWS17 11_6/6_11 rows_after_min_excess=2 (the (5,1),(6,0) remainder); 10_7/7_10 rows_after_min_excess=0; 9_8/8_9 sharp_feasible=false", + "controls": "CONTROL n5 k=9 covers=0 max=29 k=10 covers=99200 max=32; RECEIPT zeros=['k10_budget0','k10_budget1','k10_budget2','k11_budget2'] k9=17776640 (receipt validation of the PR 2773 SIDON-RECEIPT.json values)", + "predecessor_tests": "Ran 13 tests in 0.077s ... OK (PR 2870 test_engine.py)", + "parseval_obstruction": "OBSTRUCTION (11, 6) odd_excess=2 bounded=B parseval=696 allowed=504 deficit=192 contradiction=True; OBSTRUCTION (6, 11) odd_excess=2 bounded=A parseval=696 allowed=504 deficit=192 contradiction=True; REPRO rows remainder (5,1),(6,0) shared=1 c=1", + "predecessor_independent": "PASS_17POINT_INDEPENDENT (receipt_consistency k10_budget3 count=149990400 first_valid=true; k11_raw_budget4 complete=true level3=0 level4=0 sub_shards=62; rows agree on all six splits; small_group_budget_agreement 420/840/168)" + }, + "heavy_anchor_recomputation": { + "method": "The established PR 2773 raw-domain walk on the byte-vendored PR 2773 engine (vendor/agent64_search17.py, SHA-256 9eb1bf79...), complete GL(6,2)-transitive domain through {0, 3}, sub-shards by the smallest free element, per-sub-shard receipts in ANCHOR-PROGRESS.json (one section per mode), blocking foreground invocations with PYTHONUNBUFFERED=1.", + "correction_note": "An earlier in-session PASS_ANCHORS_* print from the extracted PR 2870 package was receipt validation only: PR 2870's committed ANCHOR-PROGRESS.json already contained all 62 sub-shards, so its anchors.py resumed instantly and re-added the recorded totals. The runs recorded here are the genuine fresh re-walk in this package's own ANCHOR-PROGRESS.json, started empty.", + "k10_budget3": "PASS_ANCHORS_K10B3 count=149990400 total_hist={'3': 149990400} shards=62 -- full fresh re-walk (62/62 sub-shards, started from an empty receipt); matches the recorded anchor 149,990,400 exactly and every leaf is at exact pair-sum excess 3.", + "k11_levels34": "PASS_ANCHORS_K11B4 count=0 total_hist={} shards=62 -- full fresh re-walk (62/62 sub-shards); zero 11-sets of pair-sum excess <= 4 through {0,3}, so k=11 levels 3 and 4 are both 0 (min pair-sum excess of 11-sets in F2^6 is >= 5).", + "fresh_floor_walks": "FRESH_WALK k=10 budget=2 count=0 (165.1 s) and k=11 budget=2 count=0 (140.4 s), each a complete count_sets(EVEN, k, 2, fixed=(0,3)) walk; combined with the excess-3 examples in the k10b3 receipts this fresh-proves floor(10) = 3 and floor(11) >= 3." + }, + "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], + "parseval_obstruction_11_6": {"parseval_remainder": 696, "max_allowed": 504, "deficit": 192} + }, + "status": "ANCHOR STATUS: every recorded predecessor anchor named in the assignment is reproduced in this session. RECOMPUTED from scratch: the PR 2542/2634 REPRO tiers (945/31, 10395/49, 945945/59 with records SHA-256) and the PR 2542 length-18 census (15,775,992 nodes, 312,064 cycles, zero universal) via PR 2773's verify.py on the byte-exact vendored engine; the PR 2870 OBSTRUCTION lines (parseval=696 allowed=504 deficit=192, both parity orders) via PR 2870's own verify.py/test_engine.py and again in this package's squeeze_numbers; the row table and n=5 set controls; and BOTH heavy census anchors in full by fresh empty-receipt walks (PASS_ANCHORS_K10B3 count=149990400, PASS_ANCHORS_K11B4 count=0, 62/62 sub-shards each, receipts in this package's ANCHOR-PROGRESS.json). VALIDATED (not re-walked): the four zero shards k10 budgets 0/1/2 and k11 budget 2 against the PR 2773 receipt arithmetic (verify.py --full, ~17 min on PR 2870's machine, not re-run here); the fresh k10/k11 budget-2 walks independently confirm the two load-bearing zero facts." +} diff --git a/research/f7-18point-cover-question-seed6d34356c/CERTIFICATE.json b/research/f7-18point-cover-question-seed6d34356c/CERTIFICATE.json new file mode 100644 index 0000000000..dd73ebf6e3 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/CERTIFICATE.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "result": "KB3e set-level verdict (outcome=partial): the 18-point cover question for F2^7 is NOT decided -- no 18-point cover was constructed and no split was excluded -- but it is narrowed to an exact finite remainder. All four counting-feasible splits (12,6),(11,7),(10,8),(9,9) survive the extended odd-coverage Fourier/Parseval layer (deficits non-positive; the PR 2870 squeeze hypothesis fails because 18 is even, so both sides have equal character parity), survive the extended pair-representation rows after the reproduced census floors (808 / 501 / 251 / 196 surviving rows respectively), and survive a bounded seeded construction search (best coverage 118/128 at k=18 against 10/10 instant k=20 covers as non-vacuity control). Exact new obstructions: (12,6) and (10,8) covers must have at least one vanishing character off the all-ones hyperplane. No kappa, supplier or selected-frontier change; the gap 20 <= f(7) <= 24 is unchanged.", + "labels": [ + { + "statement": "Reduction lemma: for S = A u B with A in the even coset E and B in the odd coset O of F2^n, and D = p + B (p any odd mask, D subset E), S covers F2^n iff (i) A + D = E and (ii) (A + A) u (D + D) = E. Every parity split (s, t) is therefore a two-set covering problem in the even group E =~ F2^6.", + "label": "PROVEN", + "evidence": "Direct from coset arithmetic (A + B = O iff A + D = p + O = E, and B + B = D + D); machine-checked exhaustively over all 256 subsets of F2^3 in test_engine.py (test_reduction_equivalence_exhaustive_n3) and on the real F2^5 cover." + }, + { + "statement": "Every 18-point cover of split (12,6) -- and of split (10,8) -- must have at least one character u not in {0, all-ones} with f_hat(u) = 0 or g_hat(u) = 0 (a vanishing character). Equivalently the no-vanishing sub-case of the profile system is infeasible for both splits.", + "label": "PROVEN", + "evidence": "Exact integer enumeration (cover18.fourier_profile_feasibility with nonzero_both=True) over every attainable rho square sum: for (12,6) the no-vanishing spectral shape is forced to n22=24, n24=8, n42=31 on the 126 characters off {0,1}, giving sum rho^2 = 46, which is not an attainable sum of squares of integer rho >= 0 with sum rho = 8 (the attainable set is {8,10,12,14,16,18,20,22,24,26,28,30,32,34,38,40,50,64}); for (10,8) the two Parseval equations force a non-integer shape count. The constraint set (character parity, |rho_hat| <= E_o with rho_hat == E_o (mod 2), the even-half bound f_hat^2 + g_hat^2 <= s + t + 2P - 2^n, and Parseval) is validated against every real cover of F2^3 and F2^4 (exhaustive) and of F2^5 (sample) in test_engine.py." + }, + { + "statement": "The PR 2870 odd-coverage Fourier/Parseval squeeze does not reach any 18-point split: 18 is even, so s and t always have equal character parity, and the tracked deficits are non-positive on every split.", + "label": "PROVEN", + "evidence": "Exact bookkeeping (cover18.squeeze_numbers): (12,6) E_o=8, remainders A=1248, B=696, no uniform character bound (vanishing possible); (11,7) E_o=13, remainders 1166 and 798 vs allowed 126*169 = 21294 each (deficits -20128, -20496); (10,8) E_o=16, remainders 540, 448, no uniform bound; (9,9) E_o=17, remainders 990, 990 vs allowed 126*289 = 36414 (deficit -35424). PR 2870's own obstruction() reports the same status ('equal character parities: no side is squeezed')." + }, + { + "statement": "Every recorded predecessor anchor is reproduced before any new number: PR 2542/2634 REPRO tiers 945/31, 10395/49, 945945/59 and the L18 census 15,775,992 nodes / 312,064 cycles / 0 universal; PR 2870 OBSTRUCTION lines parseval=696 allowed=504 deficit=192 both parity orders; PR 2773 k10 budget-3 = 149,990,400 and k11 levels 3-4 = 0 both recomputed IN FULL by fresh empty-receipt walks (PASS_ANCHORS_K10B3 count=149990400 shards=62, PASS_ANCHORS_K11B4 count=0 shards=62); row table (5,1),(6,0) remainder and the n=5 set controls.", + "label": "CHECKED", + "evidence": "ANCHOR-REPRO.json records commands and observed outputs; the fresh walks live in this package's ANCHOR-PROGRESS.json (one section per mode, per-sub-shard receipts). Correction recorded there: an earlier PASS print from the extracted PR 2870 package was receipt validation (its committed receipt pre-filled all shards), not a re-walk; the anchors.py runs recorded here started from an empty receipt." + }, + { + "statement": "The pair-representation rows of the four 18-point splits after the reproduced census floors (floor(6..9)=0, floor(10)=3, floor(11)=5, floor(12)=3 counting): (12,6) 808 surviving rows over 120 distinct (e_ex, b_ex) pairs, (11,7) 501 rows / 36 pairs, (10,8) 251 rows / 28 pairs, (9,9) 196 rows / 45 pairs. Each row is exact (attainable c computed by contingency-table pairing sums, validated equal to the vendored PR 2773 _pairing_sums wherever the vendored O(m!) loop terminates).", + "label": "CHECKED", + "evidence": "cover18.sharp_rows_fast; verify.py rows mode asserts the four row counts and reproduces the 17-point control remainder (5,1),(6,0) and the empty (10,7) table after the floor; full row lists in the verify output." + }, + { + "statement": "The per-character profile system does not exclude any 18-point split: (12,6), (11,7), (10,8), (9,9) all admit consistent profiles (feasible S value lists recorded; (9,9) partially undecided where the solver step cap was reached, which is never treated as a proof).", + "label": "CHECKED", + "evidence": "cover18.fourier_profile_feasibility; the same system reproduces the known exclusions ((11,6) infeasible -- PR 2870's result; (10,7) infeasible -- consistent with PR 2773's census exclusion) and accepts every split realized by a real cover (exhaustive F2^3/F2^4 cover batteries)." + }, + { + "statement": "No 18-point cover exists in the searched domain (scoped search failure, not an exclusion): direct local search at k=18 with 200 seeded restarts tops out at 118 of 128 covered masks; the structured (A, D) searches per split (60 restarts each) top out at 118 / 118 / 118 / 117 of 128; a k=19 probe is similar. Non-vacuity: the identical machinery finds 20-point covers in 10/10 short runs, matching PR 2634's recorded abundance of 20-point covers and its own failure to find 19-point covers in 200 restarts (max 124/128).", + "label": "CHECKED", + "evidence": "cover18.search_direct / cover18.search_split, fixed seeds 20261016+; verify.py search mode; the search never asserts nonexistence." + }, + { + "statement": "The direct extension of PR 2870's squeeze to 18-point splits as an exclusion mechanism is DEMOTED: its hypothesis (opposite character parity) fails on every 18-point split and the tracked deficits are non-positive.", + "label": "DEMOTED", + "evidence": "See the PROVEN bookkeeping statement; PR 2870 itself predicted this route does not reach the 18/19-point splits (E_o >= 8 there)." + }, + { + "statement": "The expectation that the pair-representation rows collapse to a small remainder (as at 17 points, where two rows survived) is DEMOTED at 18 points: the remainders are large (808 / 501 / 251 / 196 rows) and the census floors at 18 points are weaker (floor(12) = 3 is only the counting floor).", + "label": "DEMOTED", + "evidence": "cover18.sharp_rows_fast output; the floors used are exactly the reproduced ones (floor(10) = 3 fresh-proven by the k10-budget-2 = 0 walk plus excess-3 examples; floor(11) = 5 from the reproduced k11b4 = 0 walk)." + } + ], + "obstruction_numbers": { + "n": 7, + "split_order_notes": "(s, t) = (points in the even coset, points in the odd coset); mirrors are identical by odd translation", + "splits": { + "12_6": {"odd_excess": 8, "squeeze": "none (equal parity)", "remainders": [1248, 696], "uniform_bound": null, "profile_system": "feasible (16 S values)", "no_vanishing": "infeasible -> PROVEN vanishing character required", "rows_after_floors": 808, "search_best_of_128": 118}, + "11_7": {"odd_excess": 13, "squeeze": "none (equal parity)", "remainders": [1166, 798], "allowed_per_side": 21294, "deficits": [-20128, -20496], "profile_system": "feasible (22 S values)", "no_vanishing": "automatic (odd characters never vanish)", "rows_after_floors": 501, "search_best_of_128": 118}, + "10_8": {"odd_excess": 16, "squeeze": "none (equal parity)", "remainders": [1080, 896], "uniform_bound": null, "profile_system": "feasible (50 S values)", "no_vanishing": "infeasible -> PROVEN vanishing character required", "rows_after_floors": 251, "search_best_of_128": 118}, + "9_9": {"odd_excess": 17, "squeeze": "none (equal parity)", "remainders": [990, 990], "allowed_per_side": 36414, "deficits": [-35424, -35424], "profile_system": "feasible (31 S values; some S undecided at the solver step cap)", "no_vanishing": "automatic (odd characters never vanish)", "rows_after_floors": 196, "search_best_of_128": 117} + }, + "controls": { + "11_6": "profile system infeasible -- reproduces PR 2870's exclusion (squeeze parseval=696 allowed=504 deficit=192)", + "10_7": "profile system infeasible -- consistent with PR 2773's census exclusion", + "n5_real_cover": "split (4,6) of the real 10-point cover of F2^5 passes every check (positive control)" + } + }, + "reproduce": [ + "python3 -I -B research/f7-18point-cover-question-seed6d34356c/test_engine.py", + "python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py quick", + "python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py fourier", + "python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py rows", + "python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py search", + "python3 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k10b3 (resumable, ~35 min cold)", + "python3 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k11b4 (resumable, ~35 min cold)" + ], + "kappa_change": null, + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" +} diff --git a/research/f7-18point-cover-question-seed6d34356c/NOTICE.md b/research/f7-18point-cover-question-seed6d34356c/NOTICE.md new file mode 100644 index 0000000000..1f70b443c2 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/NOTICE.md @@ -0,0 +1,55 @@ +# 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 +tests in `test_engine.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, the claim "No 17-point set + covers `F2^7`" and the pair-representation identity this package's row + machinery extends. +- [PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634) by + Aaron Wang (navinor) — the recorded KB3b state (REPRO tiers, `L = 20` + campaign) and the Set-ILS precedent (20-point covers abundant; no 19-point + cover in 200 restarts) that the bounded search here is compared against. +- [PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773) by + Aaron Wang (navinor) — the split-by-split audit, the sharp row machinery, + the Sidon/pair-sum budget enumeration (`cover17.py` / `search17.py`, + vendored here byte-exact as `vendor/agent64_cover17.py` / + `vendor/agent64_search17.py`) and the census floors. +- [PR 2870](https://github.com/CrocSwap/integer-mult-bounds/pull/2870) by + Aaron Wang (navinor) — the odd-coverage Fourier/Parseval identity (the + deficit bookkeeping re-derived and extended here), the hash-pinned vendor + copies this package extracts byte-exactly, and the resumable anchor driver + `anchors.py` (vendored byte-exact). +- [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 tests): + +| Local path | Source | SHA-256 (prefix) | +|---|---|---| +| `vendor/agent64_cover17.py` | PR 2773 `cover17.py` (via PR 2870's pinned vendor/) | `082bc838134cba97...` | +| `vendor/agent64_search17.py` | PR 2773 `search17.py` (via PR 2870's pinned vendor/) | `9eb1bf79ffb99b0e...` | +| `anchors.py` | PR 2870 `anchors.py` | `73d73a9b94539403...` | + +Predecessor packages were read byte-exactly from their PR heads with +`agent_tools.py pr-tree-extract` / `pr-file-bytes` and were never imported at +runtime. diff --git a/research/f7-18point-cover-question-seed6d34356c/README.md b/research/f7-18point-cover-question-seed6d34356c/README.md new file mode 100644 index 0000000000..be908c5665 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/README.md @@ -0,0 +1,199 @@ +# KB3e — the 18-point cover question for `F2^7`: narrowed to an exact finite remainder (outcome=partial) + +**Set-level finite result, no words enumerated. Question NOT decided: no +18-point cover of `F2^7` was constructed and no parity split was excluded. +Every counting-feasible split `(12,6)`, `(11,7)`, `(10,8)`, `(9,9)` survives +each exact layer this package builds, and each is recorded below with its +exact obstruction status. Two new PROVEN structural constraints: any +`(12,6)` or `(10,8)` cover must have a vanishing character off the all-ones +hyperplane. No new kappa; 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` — every mask of `F2^7` is a pair-sum `a + b` of +two elements of the set (self-pairs `a + a` cover mask `0`; the sumset is +translation-invariant, so WLOG `0 in S`). [PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542) +by Aaron Wang (navinor) excludes length 18 and claims "No 17-point set covers +`F2^7`"; [PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773) +by Aaron Wang audits it split-by-split; [PR 2870](https://github.com/CrocSwap/integer-mult-bounds/pull/2870) +by Aaron Wang closes the recorded remainder rows `(5,1),(6,0)` with an exact +odd-coverage Fourier/Parseval identity (`696 > 504`, deficit `192`), so all +six counting-feasible 17-point splits are excluded. + +This package asks the immediate successor (PR 2870's open question 1): **does +any 18-point set cover `F2^7`?** With 17-point covers excluded, `|P| = 18` is +the set-level frontier for universal words at `L = 20/22`; an 18-point cover +would keep the `L = 22` route alive and supply its needed prefix set, while +excluding 18-point covers would kill `L = 22` outright. A parity split +`S = A u B` has `A` in the even coset `E` (s points) and `B` in the odd coset +`O` (t points), `s + t = 18`; the counting-feasible splits are `(12,6)`, +`(11,7)`, `(10,8)`, `(9,9)` and their mirrors (identical by odd translation). +**Every 18-point split has `s` and `t` of equal parity — exactly the case the +PR 2870 squeeze does not reach.** + +## Verdict per split (exact integers throughout) + +| Split | `E_o` | PR 2870 squeeze | Parseval remainders (A, B) | Allowed per side | Deficit | Profile system | Rows after floors | Search best /128 | +|---|---:|---|---:|---:|---:|---|---:|---:| +| `(12,6)` | 8 | none (equal parity) | 1248, 696 | none (vanishing possible) | non-positive | feasible (16 `S`) | 808 | 118 | +| `(11,7)` | 13 | none (equal parity) | 1166, 798 | 21294 | -20128, -20496 | feasible (22 `S`) | 501 | 118 | +| `(10,8)` | 16 | none (equal parity) | 1080, 896 | none (vanishing possible) | non-positive | feasible (50 `S`) | 251 | 118 | +| `(9,9)` | 17 | none (equal parity) | 990, 990 | 36414 | -35424, -35424 | feasible (31 `S`, partly undecided) | 196 | 117 | + +Controls: the same profile system reports `(11,6)` infeasible (reproducing PR +2870's exclusion, whose squeeze numbers `696/504/192` this package's +`squeeze_numbers` reproduces exactly) and `(10,7)` infeasible (consistent with +PR 2773's census exclusion), and accepts the split `(4,6)` of a real 10-point +cover of `F2^5` with no false contradiction. + +## The four layers + +**1. Reduction lemma (PROVEN).** 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`. Checked exhaustively over all 256 subsets of +`F2^3` and on the real `F2^5` cover. Every split `(s, t)` becomes a two-set +covering problem in the even group `E =~ F2^6`. + +**2. Fourier/Parseval re-derivation with tracked deficit (PROVEN bookkeeping; +no exclusion).** PR 2870's odd-coverage identity squeezes the even-cardinality +side's characters to `{0, ±2, ...}` only when `s, t` have opposite parity. At +18 points they never do, and the tracked deficits are non-positive on every +split (table above). The identity is DEMOTED as an 18-point exclusion +mechanism; PR 2870 predicted this (`E_o >= 8` there). + +**3. Per-character profile system (CHECKED; two PROVEN consequences).** A +second exact layer: character parities; the odd-half identity +`f_hat(u) g_hat(u) = rho_hat(u)` with `|rho_hat(u)| <= E_o` and +`rho_hat(u) == E_o (mod 2)`; the even-half bound +`f_hat(u)^2 + g_hat(u)^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` (partition square sums). Its constraints hold on every real cover of +`F2^3`/`F2^4` (exhaustive witness battery) and `F2^5`. It excludes no +18-point split, but the **no-vanishing sub-case is infeasible for `(12,6)` and +`(10,8)`** (PROVEN): e.g. for `(12,6)` a no-vanishing spectrum is forced to +24 / 8 / 31 characters of shapes `(2,2) / (2,4) / (4,2)`, giving +`sum rho^2 = 46`, which no integer `rho >= 0` of total 8 attains (attainable: +`8, 10, 12, ..., 40, 50, 64`). So any `(12,6)` or `(10,8)` cover must have at +least one character `u` off `{0, all-ones}` with `f_hat(u) = 0` or +`g_hat(u) = 0`. + +**4. Pair-representation rows with census floors (CHECKED).** PR 2773's rows +`(e_ex, b_ex, c)` extended to the four splits (its byte-vendored shape/draw +primitives with a contingency-table pairing-sums replacement — the vendored +`O(m!)` pairing loop cannot run at 18-point row sizes; the replacement is +validated equal to it wherever it terminates). Floors: `floor(6..9) = 0` +(Sidon k-sets exist; PR 2773 receipts `k7 = 34,122,816`, `k9 = 17,776,640`), +`floor(10) = 3` (fresh-proven here: `k10 budget-2 = 0` walk plus excess-3 +examples), `floor(11) = 5` (reproduced `k11 budget-4 = 0` walk), `floor(12) = 3` +(counting: `C(12,2) = 66 > 63`). Remainders: `(12,6)` 808 rows over 120 +distinct `(e_ex, b_ex)` pairs; `(11,7)` 501/36; `(10,8)` 251/28; `(9,9)` +196/45. At 17 points two rows survived; at 18 the remainder is large — the +"small finite remainder" expectation is DEMOTED, and the exact row lists are +the finite remainder. + +**5. Bounded construction search (CHECKED; scoped search failure).** The +smallest falsifying instance for "no 18-point cover exists" is one covering +set; it was searched first. Direct seeded local search at `k = 18` (200 +restarts) tops out at 118/128 covered masks; the structured `(A, D)` searches +per split (60 restarts each, the one bounded pivot after the direct search +failed) top out at 118/118/118/117; a `k = 19` probe is similar. Non-vacuity: +the identical machinery finds 20-point covers in 10/10 short runs — matching +[PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634)'s +recorded abundance of 20-point covers and its own failure to find 19-point +covers in 200 restarts (max 124/128). 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-cover-question-seed6d34356c/test_engine.py +python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py quick +python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py fourier +python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py rows +python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py search +``` + +Expected markers: `Ran 21 tests ... OK`, `PASS_F7_18POINT_QUICK`, +`PASS_F7_18POINT_FOURIER`, `PASS_F7_18POINT_ROWS`, `PASS_F7_18POINT_SEARCH`. +The heavy census anchors are recomputed by the byte-vendored PR 2870 driver +(resumable, per-sub-shard receipts in `ANCHOR-PROGRESS.json`, one section per +mode): + +```sh +python3 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k10b3 +python3 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k11b4 +``` + +Observed 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` (about 35 minutes each cold on this host). + +## 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/test_engine.py; again in `squeeze_numbers`) | +| PR 2773 row table | `(11,6)/(6,11)` remainder `(5,1),(6,0)` | recomputed | +| n=5 set controls | `0` nine-point covers (max 29/32), `99,200` ten-point covers | recomputed | +| PR 2773 `k10 budget-3` | `149,990,400` (every leaf at exact excess 3) | recomputed in full (fresh empty-receipt walk, 62/62 sub-shards) | +| PR 2773 `k11` levels 3-4 | `0`, `0` | recomputed in full (fresh empty-receipt walk, 62/62 sub-shards) | + +`ANCHOR-REPRO.json` records commands, observed outputs and one correction: an +earlier `PASS_ANCHORS_*` print from the extracted PR 2870 package was receipt +validation (its committed receipt pre-filled all sub-shards), not a re-walk; +the anchors recorded here started from an empty receipt. The four zero shards +(`k10` budgets 0/1/2, `k11` budget 2) are receipt-validated, not re-walked; +the fresh `k10 budget-2 = 0` and `k11 budget-2 = 0` walks independently +confirm the two load-bearing zero facts. + +## Scope and limitations + +Set-level only inside PR943's abstract interface. Not checked: everything +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), +whose splits `(10,9)/(10,8),(9,9)` are WORD objects; this package's row +tables cover the `(10,8)/(9,9)` set-level part and `(10,9)` is a 19-point +object untouched here), the 19-point cover question, walk-realizability of any +cover, and any kappa, supplier, tariff or selected-frontier implication. The +profile system is a source of necessary conditions: its feasibility is never +a construction, and its step cap (reached for some `(9,9)` spectra) is +recorded as undecided, never as a proof. The gap `20 <= f(7) <= 24` is +unchanged. + +## Open next questions + +1. **Do 18-point covers of `F2^7` exist (is `r((C2)^7) = 20`)?** Why it + matters: it is the deciding set-level object for the `L = 22` route (a + cover keeps `L = 22` alive; exclusion kills it). First step: attack one + split through the `(A, D)` reduction in `F2^6` under the forced character + vanishings — for `(12,6)`, enumerate 6-sets `D` and solve the + translate-hitting problem `A + D = F2^6` (`|A| = 12`) jointly with + `(A + A) u (D + D) = F2^6`. Blocked by: the joint `(A, B)` tree growth and + the absence of stabilizer canonical forms (PR 2773's recorded blocker). +2. **Does combining the forced vanishings with the even-half multiplicities + exclude `(12,6)` outright?** Why it matters: it would settle a quarter of + the question by exact integers alone. First step: add the even-half + multiplicity constraints (`tau = A_x + B_x - 1` on `E \ {0}`) as a second + layer to the profile system and enumerate the joint profiles. Blocked by: + nothing structural; the solver step cap must be lifted or the lattice + solved directly. +3. **Handoff to the concurrent `L = 20` word claim** (Nicholas Stone): the + set-level splits `(10,8),(9,9)` of the claim admit the row remainders + recorded here (251 and 196 rows), so neither is excluded at the set level; + the 19-point split `(10,9)` is untouched. Blocked by: nothing; a handoff + note. + +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-cover-question-seed6d34356c/SOURCES.json b/research/f7-18point-cover-question-seed6d34356c/SOURCES.json new file mode 100644 index 0000000000..6609e29779 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/SOURCES.json @@ -0,0 +1,102 @@ +{ + "base_commit": "ffbd90dd90dbe0055464f3a1411b25a3a4fdc6b8", + "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" + }, + { + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "path": "research/universal-connector-boundary/README.md", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476", + "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, enumerates no words, and its row tables cover the (10,8)/(9,9) set-level part. Agent-72 works the F-star family gap (KB5g); untouched here.", + "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 and recorded 20-point covers exist (r((C2)^7) <= 20) with no 19-point cover in 200 ILS restarts; PR 2773 (Aaron Wang) audited the claim split-by-split and left the (5,1),(6,0) rows; PR 2870 (Aaron Wang) closed those rows with the odd-coverage Fourier/Parseval identity. This package is the successor question (PR 2870 open question 1) at 18 points.", + "question": "KB3e: does any 18-point set cover F2^7 (P + P = F2^7 in the PR943 prefix-walk model)? Outcome=partial: not decided, narrowed to an exact row remainder per split with new structural constraints (vanishing characters forced for the (12,6) and (10,8) splits)." + }, + "references": [ + { + "head": "6739c799799621878a9249c93e2b12cc799c1482", + "local_path": "vendor/agent64_cover17.py", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from PR 2870's hash-pinned vendor/, never imported), credit Aaron Wang (navinor), PR 2773. Pair-representation rows (sharp_rows), shapes/draws primitives and the small-group controls use it. The live drift check pins base-commit blobs only, so this head-pinned vendor copy is enforced by test_engine.py's byte-pin test.", + "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 (GL(6,2)-transitive domain through {0,3}, smallest-free-element sub-shards) used by anchors.py for both heavy census anchors. Enforced by test_engine.py's byte-pin test.", + "pr": 2773, + "sha256": "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674", + "source_path": "research/f7-17point-cover-audit-seedcfa215c2/search17.py" + }, + { + "head": "9f55f291e9e79e628fd98f1e4f4debfc1c2106e5", + "local_path": "anchors.py", + "note": "Vendored byte-exact via agent_tools.py pr-file-bytes, 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 test_engine.py's byte-pin test.", + "pr": 2870, + "sha256": "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7", + "source_path": "research/f7-17point-fourier-obstruction-seedb5e318fe/anchors.py" + }, + { + "head": "9f55f291e9e79e628fd98f1e4f4debfc1c2106e5", + "local_path": null, + "note": "Aaron Wang (navinor): the odd-coverage Fourier/Parseval identity re-derived and extended here; its OBSTRUCTION numbers (696/504/192) are reproduced by this package's squeeze_numbers and by its own verify.py in-session. Read byte-exactly from the PR head, not vendored.", + "pr": 2870, + "source_path": "research/f7-17point-fourier-obstruction-seedb5e318fe/{fourier17.py,verify.py,README.md}" + }, + { + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "local_path": null, + "note": "Aaron Wang (navinor): the audited claim 'no 17-point set covers F2^7', the pair-representation identity and 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, including the Set-ILS precedent (20-point covers found; no 19-point cover in 200 restarts, max 124/128) that this package's bounded search is 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 record f(5) = 12, f(6) = 16, 20 <= f(7) <= 24 and the frozen tier EXPECTED.json reproduced here.", + "pr": 1185, + "source_path": "research/universal-connector-six-source/" + } + ], + "schema_version": 1 +} diff --git a/research/f7-18point-cover-question-seed6d34356c/TASK-CARD.md b/research/f7-18point-cover-question-seed6d34356c/TASK-CARD.md new file mode 100644 index 0000000000..ce4e7b1052 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/TASK-CARD.md @@ -0,0 +1,86 @@ +# Local task card — KB3e: the 18-point cover question for F2^7 + +Task ID / proposed scope key: `f7-18point-cover-question` (scope key drawn +`eee4a5467dd91c47ef45` etc. not used; see scope change). + +Base commit; exact predecessor and dependency heads: +- Base commit: `ffbd90dd90dbe0055464f3a1411b25a3a4fdc6b8` (origin/main at draw). +- Predecessor PR 2542 (Aaron Wang) head `3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf`, + package `research/universal-f7-singleton-seedb859517b`. +- Predecessor PR 2634 (Aaron Wang) head `e2f30d93efbef5658334072aa855aa95e795e394`, + package `research/universal-f7-singleton-l20-seed06704c39`. +- Predecessor PR 2773 (Aaron Wang) head `6739c799799621878a9249c93e2b12cc799c1482`, + package `research/f7-17point-cover-audit-seedcfa215c2`. +- Predecessor PR 2870 (Aaron Wang) heads `88426cc42` + `9f55f291e9e79e628fd98f1e4f4debfc1c2106e5`, + package `research/f7-17point-fourier-obstruction-seedb5e318fe`. +- PR 2691 (Nicholas Stone) recorded state only (the (10,10) word census). + +Concrete object and question: +In the PR943 prefix-walk model, a prefix set `P` covers `F2^7` when +`P + P = F2^7` (pair-sums `a + b` of elements of the set, self-pairs covering +mask 0; every mask of F2^7 is a pair-sum or a self-sum). Question: does any +**18-point** set `S` cover `F2^7`? Parity splits `(|A|, |B|)` with `A` in the +even coset `E` and `B` in the odd coset `O`, `|A| + |B| = 18`: (12,6), (11,7), +(10,8), (9,9) and the mirror orders (6,12), (7,11), (8,10). + +Scope status: **changed** — authorized explicit open request (kappa-blocker +KB3e), recorded in TASK.json. Reason: the drawn card (chooser OS nonce +`6d34356c3c96fdb981b4f20ddfa06b07`, track `adversarial-audit`, cards +`selected-stock-envelope` / `supplier-boundary-audit` / `uniform-transfer-audit`) +is saturated / off-object; the assignment is the immediate successor of the +now-complete 17-point question (KB3b/KB3c/KB3d chain, PR 2542 + PR 2634 + +PR 2773 + PR 2870) and the deciding set-level object for the f(7) L=22 route. + +Existing restriction being changed (or exact claim being audited): +PR 2870's open question 1 ("Do 18-point or 19-point covers of F2^7 exist?"), +and PR 2773's open question 3 (tabulate the odd-coverage Fourier obstruction +over the counting-feasible splits). + +Method; explicit parameter ranges/candidate alphabet: +1. Reproduce every recorded anchor before new numbers (PR 2870 OBSTRUCTION + parseval=696 allowed=504 deficit=192; PR 2773 k10 budget-3 = 149,990,400 and + k11 levels 3-4 = 0; PR 2542/2634 REPRO tiers 945/31, 10395/49, 945945/59 and + the L18 census 15,775,992 / 312,064 / 0). +2. Re-derive the odd-coverage Fourier/Parseval identity for the four + counting-feasible 18-point splits (12,6), (11,7), (10,8), (9,9) and track the + deficit exactly (remainder vs allowed character squares per split). +3. Extend PR 2773's pair-representation row machinery (`sharp_rows`) to the + four splits and demote rows with the reproduced census floors + (floor(10) = 3, floor(11) = 5; counting floor(12) = 3; Sidon floors 6-9 = 0). +4. Smallest falsifying instance first: a bounded construction search for an + 18-point cover (search falsifying "no 18-point cover exists"), using the + exact (A,D) reduction of each split to F2^6 and the vendored enumeration + primitives; exact verification of any candidate; one bounded pivot maximum. +All arithmetic exact integers. Alphabet: F2^7 masks 0..127, sets up to +translation (WLOG 0 in S). + +Nearest overlapping PRs and why this adds something: +PR 2542/2634/2773/2870 (Aaron Wang) close the 17-point question; none treats +18-point sets. PR 2691 (Nicholas Stone) is the word-level L=20 repeated-state +census with splits (10,9)/(10,8),(9,9) — his WORD object; this card stays on +the SET-level question (pair-collision check 2026-10-16 07:10 UTC: no CLAIM on +the 18-point set object in discussions 1317/1166). + +Declared milestone: audit / scoped obstruction (set level; no words enumerated). + +Optimistic full cost budget; required observable improvement: +Reproduction ~70 min of single-core census (sharded, resumable); new +computation bounded. Required observable: a decided split (excluded or +constructed) or a finite row remainder per split with exact obstructions. + +Unresolved consumer/restoration costs; family expansion decision if continuing: +none at this level (set-level abstraction inside PR943's interface; word-level +walk realizability and L=22 consequences are separate obligations). + +Success evidence; falsification test; time/compute cap: +Success = PROVEN exclusion of at least one 18-point split, or an explicit +verified 18-point cover, or outcome=partial with every surviving split's exact +obstruction recorded. Falsification of any new claim = the smallest exact +counterexample (a covering set for a claimed-impossible split). Cap: one +session; heavy anchors sharded to <=600 s blocking jobs with receipts. + +Predecessor authors; intended artifact and reproduction command: +Predecessors PR 2542/2634/2773/2870 by Aaron Wang (navinor); PR 943 by Ross +Richardson (prefix-walk model); PR 1185 by Doug Colkitt (pinned f(5)=12, +f(6)=16 record). Artifact: `research/f7-18point-cover-question-seed6d34356c/` +with `verify.py` replay markers. diff --git a/research/f7-18point-cover-question-seed6d34356c/TASK.json b/research/f7-18point-cover-question-seed6d34356c/TASK.json new file mode 100644 index 0000000000..47794c14c5 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/TASK.json @@ -0,0 +1,119 @@ +{ + "actual_scope": "Kappa-blocker KB3e (set level, no words): decide whether any 18-point set covers F2^7 (PR943 covering condition P + P = F2^7; every mask of F2^7 a pair-sum a + b of elements of the set). Delivered outcome=partial: the question is not decided (neither excluded nor constructed) but narrowed to an exact finite remainder. (1) The PR 2870 odd-coverage Fourier/Parseval squeeze is re-derived for the four counting-feasible splits (12,6),(11,7),(10,8),(9,9) with the deficit tracked per split: its opposite-parity hypothesis fails on all of them (18 is even) and the deficits are non-positive (e.g. (11,7) remainders 1166/798 vs allowed 21294; (9,9) 990/990 vs 36414). (2) A per-character profile system (parity, |rho_hat| <= E_o with rho_hat == E_o (mod 2), the even-half bound f_hat^2 + g_hat^2 <= s + t + 2P - 2^n, Parseval, exact attainable sums of squares of rho) excludes no 18-point split but PROVES that any (12,6) or (10,8) cover must have a vanishing character off the all-ones hyperplane (the no-vanishing sub-case is infeasible; for (12,6) it would force sum rho^2 = 46, unattainable). The same system reproduces PR 2870's (11,6) exclusion and PR 2773's (10,7) exclusion. (3) PR 2773's pair-representation rows extended to the four splits with the reproduced census floors leave 808 / 501 / 251 / 196 surviving rows ((e_ex, b_ex, c) lists exact; contingency-table pairing sums validated against the vendored engine). (4) Bounded seeded construction search: no 18-point cover found (direct k=18, 200 restarts, best 118/128; per-split structured searches best 118/118/118/117), with a k=20 non-vacuity control finding covers in 10/10 short runs. Every recorded predecessor anchor was reproduced before any new number (see ANCHOR-REPRO.json; both heavy census anchors recomputed in full by fresh empty-receipt walks). No word enumeration (the L=20 repeated-state word census is Nicholas Stone's concurrent claim); no kappa, supplier or selected-frontier change; 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": "ffbd90dd90dbe0055464f3a1411b25a3a4fdc6b8", + "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 this package narrows the 18-point frontier to an exact row remainder with new structural constraints, feeding the word-level L=20/L=22 censuses their 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-18968355", + "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 extension of their identities.", + "evidence": "CERTIFICATE.json labels every statement PROVEN / CHECKED / DEMOTED with its exact numbers. cover18.py holds the exact-arithmetic engine (coverage, the (A, D) reduction, the profile system and its no-vanishing sub-case, squeeze/deficit bookkeeping, contingency-table pairing sums, sharp rows, bounded searches). test_engine.py holds 21 tests including the vendored byte pins (vendor/agent64_cover17.py 082bc838..., vendor/agent64_search17.py 9eb1bf79..., anchors.py 73d73a9b...), exhaustive reduction equivalence at n=3, the exhaustive witness-constraint battery over all real covers of F2^3 and F2^4, the (11,6) and (10,7) exclusion controls, row-table agreement with the vendored engine wherever it terminates, and the real F2^5 cover as positive control. verify.py replays four modes (quick / fourier / rows / search) with markers PASS_F7_18POINT_{QUICK,FOURIER,ROWS,SEARCH}. anchors.py (byte-vendored from PR 2870) recomputed both heavy PR 2773 census anchors in full from empty receipts: PASS_ANCHORS_K10B3 count=149990400 and PASS_ANCHORS_K11B4 count=0 (62/62 sub-shards each; ANCHOR-PROGRESS.json). ANCHOR-REPRO.json records the reproduction commands and observed outputs. No kappa claim.", + "object_synonyms_used_in_overlap": [ + "18-point", + "18point", + "18-set", + "18 point set", + "cover F2^7", + "covers F2^7", + "pair-sum", + "pair-sum excess", + "Parseval", + "Parseval obstruction", + "Sidon", + "near-Sidon", + "universal word", + "L=22", + "prefix", + "18 distinct prefixes", + "r((C2)^7)", + "P + P", + "17-point", + "f(7)" + ], + "open_questions": [ + { + "blocked_by": "The joint (A, B) tree growth (~3.1e8 Sidon 6/7-sets on one side; no stabilizer canonical forms implemented) and the absence of any 18-point-specific identity beyond the layers recorded here.", + "first_step": "Attack one split at a time through the (A, D) reduction in F2^6 with the vanishing-character constraint: for (12,6), enumerate 6-sets D and solve the translate-hitting problem A + D = F2^6 (|A| = 12) together with (A + A) u (D + D) = F2^6 under the forced character vanishings; stabilizer canonical forms for the pair (A, D) are the recorded PR 2773 blocker.", + "question": "Do 18-point covers of F2^7 exist (is r((C2)^7) = 20)? The four splits (12,6),(11,7),(10,8),(9,9) survive this package's exact layers as an enumerated row remainder (808/501/251/196 rows).", + "why_it_matters": "It is the deciding set-level object for the f(7) L=22 route: an 18-point cover keeps L=22 alive and supplies its needed prefix set, while excluding 18-point covers kills L=22 outright (f(7) in {20, 24})." + }, + { + "blocked_by": "Nothing structural; a bounded exact enumeration (the solver step cap must be lifted or the lattice solved directly).", + "first_step": "Add the even-half multiplicity constraints (tau = A_x + B_x - 1 on E \\ {0}) to the per-character profile system as a second exact layer and enumerate the joint profiles for (12,6).", + "question": "Does the profile-system route extend to a complete exclusion of the (12,6) split by combining the forced character vanishings with the even half (A + A) u (D + D) = F2^6 multiplicities?", + "why_it_matters": "The no-vanishing sub-case is already impossible for (12,6)/(10,8); quantifying the vanishings against the even-half multiplicity profile is the only exact-integer route this package left open, and would settle a full quarter of the 18-point question." + }, + { + "blocked_by": "Nothing; a handoff note, not an obligation of this package.", + "first_step": "Handoff note: the 18-point splits (10,8),(9,9) of the word claim admit set-level remainders (251 and 196 rows here), so neither is excluded at the set level; the 19-point split (10,9) is untouched (this package's identity stops at 18 points).", + "question": "For the concurrent repeated-state L=20 word claim (Nicholas Stone, discussion 1166 comment 18954844): do its remaining splits (10,9),(10,8),(9,9) survive at the set level as well?", + "why_it_matters": "It is the last word-level family at length 20 and feeds the f(7) gap 20 <= f(7) <= 24; this package's row tables cover the (10,8)/(9,9) set-level part of those splits (18-point) but not (10,9) (19-point)." + } + ], + "original_card": { + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "first_experiment": "Choose one of the fourteen recorded stages, pin its producer, and derive the parent reserve and depth coefficient. Stop with a precise source-level missing lemma if that coefficient cannot yet be bounded; do not rerun the already checked headroom arithmetic as a new result.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #1956/#1965/#1990 in the batch review and the stock-audit source boundary. Its actual selected coefficient remains uncomputed.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "id": "selected-stock-envelope", + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990" + ], + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption." + ], + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md" + ] + }, + "outcome": "partial", + "pair_collision_check": { + "checked_utc": "2026-10-16T07:10:00Z and 07:41:00Z (entry and refined overlap passes, before computation), 2026-10-16T09:16:00Z (post-interruption re-check before completing the heavy anchors)", + "result": "No claim on the 18-point set object at any check. Overlap matches were the predecessor lineage (PR 2542/2634/2691/2773/2870 and their board comments) plus unrelated pair-sum/Fourier/cover objects. Nicholas Stone's claim 18954844 is the repeated-state L=20 WORD census (splits (10,9)/(10,8),(9,9) at the word level) and is explicitly a different object; agent-72's KB5g claim (2026-10-16T09:13Z, F-star family gap) is a different object. This package's own CLAIM (comment 18968355) was posted 2026-10-16T09:20Z after the re-check.", + "threads_scanned": [ + "discussion 1317 since 2026-10-15T00:00:00Z (silent throughout; CLAIM scan incl. nested replies)", + "discussion 1166 since 2026-10-15T17:00:00Z with grep CLAIM|18-point|cover|pair-sum|Parseval|Sidon|L=22|prefix (no claim on the set-level 18-point object)" + ], + "tool": "agent_tools.py disc-comments --grep (with nested replies) + scripts/find_overlap.py --refresh" + }, + "priced_budget_breakdown": "25 min entry overlap, pair-collision checks and the task card; 20 min predecessor extraction, attribution checks and light anchor reproductions; 45 min new machinery (TDD: 21 tests, profile system, pairing-sums acceleration, rows); 50 min anchor recomputation jobs (both heavy walks, resumable sub-shards, plus the interruption recovery); 20 min bounded searches and controls; 50 min package metadata, registration, gates and submission.", + "priced_budget_minutes": 210, + "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 6d34356c3c96fdb981b4f20ddfa06b07, track adversarial-audit) drew the saturated cards selected-stock-envelope / supplier-boundary-audit / uniform-transfer-audit; the assignment (kappa-blocker KB3e) is the immediate successor of the now-complete 17-point question (PR 2542 + PR 2634 + PR 2773 + PR 2870) and explicitly authorizes taking this open request (PR 2870 open question 1) instead of the drawn card. Pair-collision checks (discussions 1317 and 1166 with nested replies via agent_tools.py disc-comments --grep, plus scripts/find_overlap.py --refresh with the object's proper names) found no claim on the 18-point set 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": "eee4a5467dd91c47ef45", + "scope_status": "changed", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "session_seed": "6d34356c3c96fdb981b4f20ddfa06b07", + "smallest_falsifying_instance_first": "The falsifying instance for 'no 18-point cover exists' is one 18-point set S with S + S = F2^7; it was searched first (the bounded seeded construction search, with the identical machinery finding 20-point covers instantly as non-vacuity). Before any new number the recorded predecessor state was reproduced byte-exactly (ANCHOR-REPRO.json): the PR 2542/2634 REPRO tiers (945/31, 10395/49, 945945/59 with records SHA-256), the PR 2542 length-18 census (15,775,992 nodes, 312,064 cycles, zero universal), the PR 2870 OBSTRUCTION lines (parseval=696 allowed=504 deficit=192 both parity orders), the row table and n=5 set controls, and both heavy census anchors recomputed in full (PASS_ANCHORS_K10B3 count=149990400, PASS_ANCHORS_K11B4 count=0). The smallest instances the new layers touch are the forced odd-coverage profiles rho of the 18-point splits (E_o = 8/13/16/17); their exact status (feasible systems, non-positive deficits, forced vanishings for (12,6)/(10,8)) is recorded and machine-checked.", + "stop_rule": "Stop at the first of: (a) an explicit 18-point covering set (outcome (b) of the assignment), (b) an exact exclusion of all four splits (outcome (a)), or (c) the priced budget expiring with each surviving split's exact obstruction recorded (outcome (c), labelled partial). Outcome (c): the row remainder per split, the deficit table and the vanishing-character constraints are recorded; one bounded pivot (the structured (A, D) search after the direct search failed) was used and failed to find a cover; no second pivot.", + "task_id": "selected-stock-envelope", + "track": "adversarial-audit (drawn); scope changed to the assigned explicit open request kappa-blocker KB3e (the 18-point cover question for F2^7, immediate successor of the closed 17-point question)" +} diff --git a/research/f7-18point-cover-question-seed6d34356c/VERIFY.json b/research/f7-18point-cover-question-seed6d34356c/VERIFY.json new file mode 100644 index 0000000000..62b07e0167 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/VERIFY.json @@ -0,0 +1,72 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-cover-question-seed6d34356c/test_engine.py" + ], + "checks": "21 tests: vendored byte pins (vendor/agent64_cover17.py 082bc838..., vendor/agent64_search17.py 9eb1bf79..., anchors.py 73d73a9b...), coverage agreement with the vendored engine, the (A, D) reduction equivalence exhaustively over all subsets of F2^3, the rho square-sum set (46 excluded), character-shape parity/bound checks on all six splits, the (11,6)/(6,11) infeasibility controls reproducing PR 2870, the (10,7) infeasibility control consistent with PR 2773, the real F2^5 cover positive control, fast pairing sums against the vendored O(m!) loop on random draws, sharp-row agreement with the vendored rows on the 17-point splits, the recorded 17-point remainder (5,1),(6,0), and the exhaustive witness-constraint battery over every real cover of F2^3 and F2^4.", + "timeout_seconds": 60 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-cover-question-seed6d34356c/verify.py", + "quick" + ], + "checks": "Vendored byte pins; reduction and witness soundness controls; the squeeze/deficit bookkeeping for all six splits (asserting PR 2870's 696/504/192 reproduction); the rho square-sum control; and the anchor receipts in ANCHOR-PROGRESS.json (both heavy walks complete: k10b3 count=149990400, k11b4 count=0, 62/62 sub-shards each). Marker PASS_F7_18POINT_QUICK.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-cover-question-seed6d34356c/verify.py", + "fourier" + ], + "checks": "The per-character profile system on the four 18-point splits and the two controls (asserting feasibility exactly where the Fourier layer does not exclude, and infeasibility of (11,6) and (10,7)), plus the no-vanishing sub-case (asserting infeasibility for (12,6) and (10,8) -- the PROVEN vanishing-character constraints). Marker PASS_F7_18POINT_FOURIER.", + "timeout_seconds": 600 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-cover-question-seed6d34356c/verify.py", + "rows" + ], + "checks": "The pair-representation rows of the four 18-point splits after the census floors (asserting 808/501/251/196 rows, all exact), and the 17-point controls ((5,1),(6,0) remainder; (10,7) empty after the floor). Marker PASS_F7_18POINT_ROWS.", + "timeout_seconds": 60 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-cover-question-seed6d34356c/verify.py", + "search" + ], + "checks": "The bounded seeded construction search (direct k=18 and the structured (A, D) searches per split; a found cover is printed loudly and never asserted against), a k=19 probe, and the k=20 non-vacuity control (asserting the machinery finds the known-abundant 20-point covers). Marker PASS_F7_18POINT_SEARCH.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "research/f7-18point-cover-question-seed6d34356c/cover18.py", + "research/f7-18point-cover-question-seed6d34356c/test_engine.py", + "research/f7-18point-cover-question-seed6d34356c/verify.py", + "research/f7-18point-cover-question-seed6d34356c/anchors.py", + "research/f7-18point-cover-question-seed6d34356c/ANCHOR-PROGRESS.json", + "research/f7-18point-cover-question-seed6d34356c/ANCHOR-REPRO.json", + "research/f7-18point-cover-question-seed6d34356c/vendor/agent64_cover17.py", + "research/f7-18point-cover-question-seed6d34356c/vendor/agent64_search17.py" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/f7-18point-cover-question-seed6d34356c/anchors.py b/research/f7-18point-cover-question-seed6d34356c/anchors.py new file mode 100644 index 0000000000..d07fa31100 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/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-cover-question-seed6d34356c/cover18.py b/research/f7-18point-cover-question-seed6d34356c/cover18.py new file mode 100644 index 0000000000..3faa640d79 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/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-cover-question-seed6d34356c/test_engine.py b/research/f7-18point-cover-question-seed6d34356c/test_engine.py new file mode 100644 index 0000000000..205476d1d4 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/test_engine.py @@ -0,0 +1,209 @@ +"""Tests for the KB3e engine (18-point cover question for F2^7). + +Test-first: these were written and run (RED) before cover18.py existed, then +made GREEN. Controls deliberately include the known 17-point outcomes so the +new machinery cannot silently disagree with PR 2870/PR 2773: + + * the (11,6)/(6,11) split must come out impossible (PR 2870, deficit 192); + * the (10,7) split must NOT show a Fourier contradiction (PR 2870 table); + * a real 10-point cover of F2^5 must pass every check (positive control); + * the fast pairing-sums and row tables must agree with the vendored PR 2773 + engine wherever the vendored engine terminates. +""" + +import itertools +import random +import sys +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +sys.path.insert(0, str(HERE / "vendor")) + +import cover18 as c18 # noqa: E402 +import agent64_cover17 as c17 # noqa: E402 + + +class TestCoverageAndReduction(unittest.TestCase): + def test_coverage_matches_vendored_engine(self): + rng = random.Random(20261016) + for _ in range(200): + k = rng.randint(1, 10) + pts = rng.sample(range(128), k) + self.assertEqual(c18.coverage_mask(pts), c17.coverage_mask(pts)) + self.assertEqual(c18.covers(pts), c17.coverage_mask(pts) == (1 << 128) - 1) + + def test_split_of_parity(self): + self.assertEqual(c18.split_of([0, 3, 5, 7]), (3, 1)) + + def test_reduction_equivalence_exhaustive_n3(self): + # Every subset of F2^3: S covers iff the (A, D) reduction holds. + for r in range(9): + for pts in itertools.combinations(range(8), r): + A = [p for p in pts if not (p.bit_count() % 2)] + B = [p for p in pts if p.bit_count() % 2] + direct = c18.covers(pts, n=3) + odd_ok, even_ok = c18.reduction_conditions(A, B, n=3) + self.assertEqual(direct, odd_ok and even_ok, (pts, odd_ok, even_ok)) + + def test_positive_control_n5_cover(self): + # A real 10-point cover of F2^5 (PR 2870's positive control). + S = [0, 1, 2, 3, 4, 5, 6, 8, 16, 31] + self.assertTrue(c18.covers(S, n=5)) + A = [p for p in S if not (p.bit_count() % 2)] + B = [p for p in S if p.bit_count() % 2] + odd_ok, even_ok = c18.reduction_conditions(A, B, n=5) + self.assertTrue(odd_ok and even_ok) + + +class TestRhoSquares(unittest.TestCase): + def test_rho_square_values_exact(self): + # sum rho = 8 over integer rho >= 0: attainable sums of squares. + got = set(c18.rho_square_values(8)) + want = {8, 10, 12, 14, 16, 18, 20, 22, 24, 26, 28, 30, 32, 34, 38, 40, 50, 64} + self.assertEqual(got, want) + self.assertNotIn(46, got) # the (12,6) no-vanishing contradiction value + + def test_rho_square_values_two(self): + self.assertEqual(set(c18.rho_square_values(2)), {2, 4}) + + +class TestFourierSystem(unittest.TestCase): + def test_116_control_infeasible(self): + # PR 2870: (11,6) is impossible. The profile system must be + # infeasible and its squeeze numbers must reproduce 696/504/192. + rec = c18.fourier_profile_feasibility(7, 11, 6) + self.assertFalse(rec["feasible"]) + squeeze = c18.squeeze_numbers(7, 11, 6) + self.assertEqual(squeeze["parseval_remainder"], 696) + self.assertEqual(squeeze["max_allowed"], 504) + self.assertEqual(squeeze["deficit"], 192) + self.assertTrue(squeeze["contradiction"]) + + def test_611_mirror_control_infeasible(self): + rec = c18.fourier_profile_feasibility(7, 6, 11) + self.assertFalse(rec["feasible"]) + + def test_107_control_infeasible_consistent_with_pr2773(self): + # PR 2870's pure squeeze found no contradiction for (10,7), but the + # split is excluded (PR 2773's census route). The profile system adds + # the even-half bound and must find it infeasible -- consistent with + # the known truth, and a control that the system can detect this split. + rec = c18.fourier_profile_feasibility(7, 10, 7) + self.assertFalse(rec["feasible"]) + + def test_small_n_covers_never_excluded(self): + # Soundness: every split realized by a REAL cover of F2^3 or F2^4 must + # be feasible for the profile system (no false exclusions), and the + # actual character values of the cover must satisfy every constraint. + for n in (3, 4): + N = 1 << n + seen = set() + for r in range(1, N + 1): + for pts in itertools.combinations(range(N), r): + if not c18.covers(pts, n=n): + continue + A = [p for p in pts if not (p.bit_count() % 2)] + B = [p for p in pts if p.bit_count() % 2] + key = (n, len(A), len(B)) + self.assertTrue( + c18.witness_constraints_ok(A, B, n), (n, pts) + ) + if key not in seen: + seen.add(key) + if len(A) * len(B) - (1 << (n - 1)) > 12: + continue # solver battery is bounded; witnesses above cover all + rec = c18.fourier_profile_feasibility(n, len(A), len(B)) + if rec["feasible"] is None: + continue # E_o beyond the enumeration budget + self.assertTrue(rec["feasible"], (key, rec["reason"])) + + def test_positive_control_n5_system_feasible(self): + # The real F2^5 cover has split (4,6); the system must allow it. + rec = c18.fourier_profile_feasibility(5, 4, 6) + self.assertTrue(rec["feasible"]) + S = [0, 1, 2, 3, 4, 5, 6, 8, 16, 31] + A = [p for p in S if not (p.bit_count() % 2)] + B = [p for p in S if p.bit_count() % 2] + self.assertTrue(c18.witness_constraints_ok(A, B, 5)) + + def test_shapes_respect_parity_and_bounds(self): + for (s, t) in ((11, 6), (10, 7), (12, 6), (11, 7), (10, 8), (9, 9)): + rec = c18.shapes_fourier(7, s, t) + eo = s * t - 64 + for (f2, g2, p2) in rec: + a = int(f2 ** 0.5) + b = int(g2 ** 0.5) + self.assertEqual(a % 2, s % 2) + self.assertEqual(b % 2, t % 2) + self.assertLessEqual(a * b, eo) + self.assertEqual((a * b) % 2, eo % 2) + + +class TestPairingSums(unittest.TestCase): + def test_fast_pairing_agrees_with_vendored(self): + rng = random.Random(7) + for _ in range(300): + m = rng.randint(1, 6) + da = tuple(sorted(rng.randint(1, 4) for _ in range(m))) + db = tuple(sorted(rng.randint(1, 4) for _ in range(m))) + fast = c18.pairing_sums(da, db) + slow = set(c17._pairing_sums(da, db)) + self.assertEqual(fast, slow, (da, db)) + + def test_pairing_sums_single(self): + self.assertEqual(c18.pairing_sums((1,), (5,)), {5}) + + +class TestRows(unittest.TestCase): + def test_sharp_rows_fast_agrees_with_vendored_17point(self): + for (s, t) in ((11, 6), (10, 7), (9, 8)): + fast = c18.sharp_rows_fast(7, s, t) + slow = c17.sharp_rows(7, s, t) + self.assertEqual( + [(r["e_ex"], r["b_ex"], r["c"]) for r in fast["rows"]], + [(r["e_ex"], r["b_ex"], r["c"]) for r in slow["rows"]], + (s, t), + ) + self.assertEqual(fast["best"], slow["best"]) + + def test_row_table_17point_remainder(self): + # With the census floors the 17-point (11,6) remainder is (5,1),(6,0). + rows = c18.surviving_rows_fast(7, 11, 6, min_e_ex=5, min_b_ex=0) + got = sorted((r["e_ex"], r["b_ex"]) for r in rows["rows"]) + self.assertEqual(got, [(5, 1), (6, 0)]) + + def test_row_table_107_after_floor_empty(self): + rows = c18.surviving_rows_fast(7, 10, 7, min_e_ex=3, min_b_ex=0) + self.assertEqual(rows["rows"], []) + + +class TestSearchSmoke(unittest.TestCase): + def test_coverage_best_on_known_cover(self): + S = [0, 1, 2, 3, 4, 5, 6, 8, 16, 31] + self.assertEqual(c18.coverage_mask(S).bit_count(), 32) + + +class TestVendoredPins(unittest.TestCase): + def _sha(self, rel): + import hashlib + + return hashlib.sha256((HERE / rel).read_bytes()).hexdigest() + + def test_agent64_cover17_byte_pin(self): + self.assertEqual(self._sha("vendor/agent64_cover17.py"), c18.VENDOR_PIN_COVER17) + + def test_agent64_search17_byte_pin(self): + self.assertEqual(self._sha("vendor/agent64_search17.py"), c18.VENDOR_PIN_SEARCH17) + + def test_pr2870_anchors_byte_pin(self): + # byte-vendored from PR 2870 head 9f55f291e9e79e628fd98f1e4f4debfc1c2106e5 + self.assertEqual( + self._sha("anchors.py"), + "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7", + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/f7-18point-cover-question-seed6d34356c/vendor/agent64_cover17.py b/research/f7-18point-cover-question-seed6d34356c/vendor/agent64_cover17.py new file mode 100644 index 0000000000..5add3747a3 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/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-cover-question-seed6d34356c/vendor/agent64_search17.py b/research/f7-18point-cover-question-seed6d34356c/vendor/agent64_search17.py new file mode 100644 index 0000000000..ef17635967 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/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-cover-question-seed6d34356c/verify.py b/research/f7-18point-cover-question-seed6d34356c/verify.py new file mode 100644 index 0000000000..c4ecbb7994 --- /dev/null +++ b/research/f7-18point-cover-question-seed6d34356c/verify.py @@ -0,0 +1,201 @@ +"""Registered replay for the KB3e package (18-point cover question, F2^7). + +Modes (each bounded; see VERIFY.json): + + quick vendored byte pins, reduction and witness soundness controls, + the squeeze/deficit bookkeeping for all six splits, and the + recorded anchor receipts. marker PASS_F7_18POINT_QUICK + fourier the per-character profile system and its no-vanishing sub-case. + marker PASS_F7_18POINT_FOURIER + rows the pair-representation rows after the census floors. + marker PASS_F7_18POINT_ROWS + search the bounded seeded construction search (a found cover is printed + loudly; the search never asserts nonexistence). + marker PASS_F7_18POINT_SEARCH + +Everything is exact integer arithmetic (no floats). The heavy PR 2773 census +anchors are recomputed by anchors.py (byte-vendored from PR 2870; resumable, +per-sub-shard receipts in ANCHOR-PROGRESS.json) and were recomputed in full +in-session -- see ANCHOR-REPRO.json. +""" + +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 cover18 as c18 # noqa: E402 + +SPLITS = [(12, 6), (11, 7), (10, 8), (9, 9)] +CONTROLS = [(11, 6), (10, 7)] +# Census floors: min pair-sum excess of k-sets in F2^6 (= E). floor(6..9)=0 +# (Sidon k-sets exist; PR 2773 receipts k7_budget0=34,122,816 and +# k9_budget0=17,776,640), floor(10)=3 and floor(11)=5 (the two heavy anchors +# reproduced here), floor(12)=3 (counting: C(12,2)=66 > 63). +FLOORS = {6: 0, 7: 0, 8: 0, 9: 0, 10: 3, 11: 5, 12: 3} +VENDOR_PINS = { + "vendor/agent64_cover17.py": c18.VENDOR_PIN_COVER17, + "vendor/agent64_search17.py": c18.VENDOR_PIN_SEARCH17, + "anchors.py": "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7", +} + + +def check_pins(): + import hashlib + + for rel, want in VENDOR_PINS.items(): + got = hashlib.sha256((HERE / rel).read_bytes()).hexdigest() + assert got == want, (rel, got, want) + print("PIN %s sha256=%s" % (rel, got[:16]), flush=True) + + +def mode_quick(): + t0 = time.time() + check_pins() + # reduction + witness soundness (exhaustive at n = 3, sampled at n = 4/5) + import itertools + + n3 = 0 + for r in range(9): + for pts in itertools.combinations(range(8), r): + A = [p for p in pts if not (p.bit_count() % 2)] + B = [p for p in pts if p.bit_count() % 2] + direct = c18.covers(pts, n=3) + assert direct == all(c18.reduction_conditions(A, B, n=3)), pts + n3 += 1 + print("CONTROL reduction exhaustive n=3 subsets=%d ok=true" % n3, flush=True) + S = [0, 1, 2, 3, 4, 5, 6, 8, 16, 31] + A = [p for p in S if not (p.bit_count() % 2)] + B = [p for p in S if p.bit_count() % 2] + assert c18.covers(S, n=5) and c18.witness_constraints_ok(A, B, 5) + print("CONTROL n5 real cover split=(4,6) witness_ok=true", flush=True) + assert 46 not in c18.rho_square_values(8) + print("CONTROL rho_square_values(8) excludes 46 (the (12,6) no-vanishing value)", flush=True) + # squeeze / deficit bookkeeping for every split + for (s, t) in SPLITS + CONTROLS: + rec = c18.squeeze_numbers(7, s, t) + sides = rec["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, rec["odd_excess"], rec["opposite_parity"], rec["contradiction"], line), + flush=True, + ) + rec = c18.squeeze_numbers(7, 11, 6) + assert rec["parseval_remainder"] == 696 and rec["max_allowed"] == 504 and rec["deficit"] == 192 + print("CONTROL PR2870 obstruction reproduced: parseval=696 allowed=504 deficit=192", flush=True) + # recorded anchor receipts (recomputed in full in-session; see ANCHOR-REPRO.json) + prog = json.loads((HERE / "ANCHOR-PROGRESS.json").read_text(encoding="utf-8")) + k10 = prog["modes"]["k10b3"] + k11 = prog["modes"]["k11b4"] + assert k10.get("complete") and k10["total_hist"] == {"3": 149990400} + assert k11.get("complete") and k11["total_hist"] == {} + print("ANCHORS receipts k10b3 count=149990400 total_hist={'3': 149990400} shards=%d" % len(k10["shards"]), flush=True) + print("ANCHORS receipts k11b4 count=0 total_hist={} shards=%d" % len(k11["shards"]), flush=True) + print("PASS_F7_18POINT_QUICK seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_fourier(): + t0 = time.time() + expect = {(12, 6): True, (11, 7): True, (10, 8): True, (9, 9): True, (11, 6): False, (10, 7): False} + for (s, t) in SPLITS + CONTROLS: + rec = c18.fourier_profile_feasibility(7, s, t) + print( + "PROFILE18 (%d, %d) eo=%d feasible=%s capped=%s S_count=%d rem=(%d, %d)" + % ( + s, + t, + rec["odd_excess"], + rec["feasible"], + rec.get("capped"), + len(rec["feasible_S"]), + rec["parseval_remainders"][0], + rec["parseval_remainders"][1], + ), + flush=True, + ) + assert rec["feasible"] is expect[(s, t)], (s, t, rec["reason"]) + for (s, t) in SPLITS: + rec = c18.fourier_profile_feasibility(7, s, t, nonzero_both=True) + tag = "PROVEN every (s,t) cover has a vanishing character off {0,1}" if not rec["feasible"] else "no constraint" + print("NOVANISH (%d, %d) feasible=%s capped=%s -> %s" % (s, t, rec["feasible"], rec.get("capped"), tag), flush=True) + if (s, t) in ((12, 6), (10, 8)): + assert not rec["feasible"] + print("PASS_F7_18POINT_FOURIER seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_rows(): + t0 = time.time() + want = {(12, 6): 808, (11, 7): 501, (10, 8): 251, (9, 9): 196} + for (s, t) in SPLITS: + rows = c18.sharp_rows_fast(7, s, t, min_e_ex=FLOORS[s], min_b_ex=FLOORS[t]) + eb = sorted({(r["e_ex"], r["b_ex"]) for r in rows["rows"]}) + print( + "ROWS18 (%d, %d) rows=%d distinct_eb=%d best=%d need=%d c_vals=%d floors=(e>=%d, b>=%d)" + % (s, t, len(rows["rows"]), len(eb), rows["best"], rows["need"], len(rows["c_vals"]), FLOORS[s], FLOORS[t]), + flush=True, + ) + assert len(rows["rows"]) == want[(s, t)], (s, t, len(rows["rows"])) + assert all(r["status"] == "sharp" for r in rows["rows"]) + # 17-point control: the recorded remainder (5,1),(6,0) must reappear + rows = c18.surviving_rows_fast(7, 11, 6, min_e_ex=5, min_b_ex=0) + got = sorted((r["e_ex"], r["b_ex"]) for r in rows["rows"]) + assert got == [(5, 1), (6, 0)], got + rows = c18.surviving_rows_fast(7, 10, 7, min_e_ex=3, min_b_ex=0) + assert rows["rows"] == [] + print("CONTROL 17-point rows reproduce: (11,6) remainder (5,1),(6,0); (10,7) empty after floor", flush=True) + print("PASS_F7_18POINT_ROWS seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_search(): + t0 = time.time() + res = c18.search_direct(k=18, restarts=200, seed=20261016, seconds=60.0) + print( + "SEARCH18 direct k=18 found=%s score=%s restarts=%s seconds=%s" + % (res["found"], res["score"], res.get("restarts"), res["seconds"]), + flush=True, + ) + if res["found"]: + print("SEARCH18 FOUND COVER S=%s" % res["S"], flush=True) + for (s, t) in SPLITS: + res = c18.search_split(s, t, restarts=60, seed=20261016 + s, seconds=25.0) + print( + "SEARCH18 (%d, %d) found=%s score=%s moves=%s seconds=%s" + % (s, t, res["found"], res["score"], res.get("moves"), res["seconds"]), + flush=True, + ) + if res["found"]: + print("SEARCH18 FOUND PAIR A=%s D=%s" % (res["A"], res["D"]), flush=True) + res = c18.search_direct(k=19, restarts=60, seed=1919, seconds=15.0) + print("SEARCH18 probe k=19 found=%s score=%s" % (res["found"], res["score"]), flush=True) + found = 0 + for seed in range(5): + res = c18.search_direct(k=20, restarts=3, seed=1000 + seed, seconds=8.0) + found += 1 if res["found"] else 0 + print("CONTROL SEARCH k=20 covers found in %d/5 runs (non-vacuity)" % found, flush=True) + assert found >= 1, "search machinery must find known-abundant 20-point covers" + print("PASS_F7_18POINT_SEARCH seconds=%.1f" % (time.time() - t0), flush=True) + + +def main(): + sys.stdout.reconfigure(encoding="utf-8") + mode = sys.argv[1] if len(sys.argv) > 1 else "quick" + fn = { + "quick": mode_quick, + "fourier": mode_fourier, + "rows": mode_rows, + "search": mode_search, + }[mode] + fn() + + +if __name__ == "__main__": + main()