diff --git a/research/universal-f7-singleton-l20-seed06704c39/CENSUS20-PROGRESS.json b/research/universal-f7-singleton-l20-seed06704c39/CENSUS20-PROGRESS.json new file mode 100644 index 0000000000..371970feb5 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/CENSUS20-PROGRESS.json @@ -0,0 +1 @@ +{"done": {"0000": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "0001": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "0010": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "0011": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "0012": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "0100": {"nodes": 4, "leaves": 0, "hits": 0, "words": []}, "0101": {"nodes": 4, "leaves": 0, "hits": 0, "words": []}, "0102": {"nodes": 798901031, "leaves": 67674177, "hits": 0, "words": []}, "0110": {"nodes": 3, "leaves": 0, "hits": 0, "words": []}, "0111": {"nodes": 3, "leaves": 0, "hits": 0, "words": []}, "0112": {"nodes": 3, "leaves": 0, "hits": 0, "words": []}}, "accum": {"nodes": 798901058, "leaves": 67674177, "hits": 0, "words": []}, "shards_total": 15} \ No newline at end of file diff --git a/research/universal-f7-singleton-l20-seed06704c39/CERTIFICATE.json b/research/universal-f7-singleton-l20-seed06704c39/CERTIFICATE.json new file mode 100644 index 0000000000..514ae7436b --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/CERTIFICATE.json @@ -0,0 +1,473 @@ +{ + "conclusion": "f(7) in {20,22,24} unchanged; L=19 dead by parity; beating templates closed; covers walk-unrealisable in all samples; search ceilings 120/126/128 at L=20/22/24", + "tier1_reproduction": { + "counting_least_even_L": { + "5": 10, + "6": 14, + "7": 18 + }, + "gray_lengths": { + "5": 12, + "6": 16, + "7": 24 + }, + "n5_L10": { + "matches_pinned": true, + "max_coverage": 31, + "records_sha256": "3dcc5689a4a34baec6424389a07dd917c0b681d6a894cba3e909f5a81efdc86e", + "words": 945 + }, + "n6_L12": { + "matches_pinned": true, + "max_coverage": 49, + "records_sha256": "491b295f12cfa34a010dc23392b02d725dedcd0ba84111b31aa939a013d4958a", + "words": 10395 + }, + "n6_L14": { + "matches_pinned": true, + "max_coverage": 59, + "records_sha256": "3d711ffa192093103cc034bb5ab00c680d96667c9f6d1a509981b444663bc838", + "words": 945945 + } + }, + "tier2_obstructions": { + "l20_split_note": "the identity kills 17-point splits (9,8)/(8,9) only; (10,7)/(7,10) survive, so |P|>=17 walks with repeats remain open at L=20", + "l20_splits_admissible": [ + [ + 7, + 10 + ], + [ + 8, + 10 + ], + [ + 9, + 9 + ], + [ + 9, + 10 + ], + [ + 10, + 7 + ], + [ + 10, + 8 + ], + [ + 10, + 9 + ], + [ + 10, + 10 + ] + ], + "parity": "no restored word has odd length: all label counts even and >= 2; patterns(7, 19) empty; assignment option (a) 'exclude length 19' discharged exactly", + "square_detour_transversal": "any single-excursion [6,i,j,i,j,6] + 16-cycle template forces a transversal R of sq=span(e_i,e_j); G[R] components equal the level-set components of g (R={t+g(t)}), so a closed walk through R needs g constant, but then R+R is a 16-point plane and misses 48 masks. Spot-checked in test_engine.py::TestTransversalLemma." + }, + "tier3_covers": { + "cover20": { + "degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 2, + 3 + ], + "points": [ + 2, + 4, + 8, + 9, + 14, + 25, + 26, + 30, + 31, + 42, + 49, + 51, + 60, + 67, + 77, + 82, + 100, + 108, + 109, + 113 + ] + }, + "cover22": { + "degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 3 + ], + "points": [ + 1, + 2, + 9, + 19, + 30, + 35, + 36, + 45, + 48, + 49, + 59, + 61, + 68, + 72, + 77, + 83, + 86, + 89, + 93, + 104, + 109, + 111 + ] + }, + "set_ils": { + "k18_best": 118, + "k18_restarts": 40, + "k19_best": 124, + "k19_restarts": 200, + "k20_covers_per_30": 14, + "k22_covers_per_30": 28 + }, + "walk_shape": "every cover sampled (175 at k=20 and 288 at k=22 in session sweeps, plus the deterministic campaign) has min induced degree 0, so no closed walk spans it at any length" + }, + "tier4_search": { + "campaign": { + "set_k20": { + "best": 128, + "covers": 14, + "first_cover": [ + 2, + 4, + 8, + 9, + 14, + 25, + 26, + 30, + 31, + 42, + 49, + 51, + 60, + 67, + 77, + 82, + 100, + 108, + 109, + 113 + ], + "first_cover_degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 2, + 3 + ], + "first_cover_hamiltonian_cycle": false + }, + "set_k22": { + "best": 128, + "covers": 28, + "first_cover": [ + 1, + 2, + 9, + 19, + 30, + 35, + 36, + 45, + 48, + 49, + 59, + 61, + 68, + 72, + 77, + 83, + 86, + 89, + 93, + 104, + 109, + 111 + ], + "first_cover_degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 3 + ], + "first_cover_hamiltonian_cycle": false + }, + "word_L20": { + "coverage": 120, + "evals": 3274631, + "missing": [ + 30, + 39, + 42, + 52, + 82, + 83, + 116, + 117 + ], + "word": [ + 0, + 4, + 6, + 2, + 1, + 5, + 2, + 1, + 6, + 0, + 1, + 3, + 2, + 0, + 1, + 4, + 2, + 0, + 5, + 3 + ] + }, + "word_L22": { + "coverage": 126, + "evals": 4098654, + "missing": [ + 91, + 98 + ], + "word": [ + 5, + 2, + 1, + 0, + 2, + 3, + 1, + 4, + 2, + 3, + 0, + 6, + 1, + 3, + 5, + 1, + 2, + 0, + 6, + 0, + 3, + 4 + ] + }, + "word_L24_control": { + "coverage": 128, + "word": [ + 0, + 1, + 2, + 5, + 2, + 3, + 4, + 3, + 6, + 4, + 3, + 5, + 0, + 4, + 2, + 1, + 0, + 3, + 1, + 0, + 4, + 1, + 6, + 2 + ] + } + }, + "extended": { + "extended_word_L20": { + "coverage": 120, + "first_reached_at_restart": 0, + "missing": [ + 30, + 39, + 42, + 52, + 82, + 83, + 116, + 117 + ], + "params": { + "L": 20, + "kick": 8, + "restarts": 600, + "seed": 22 + }, + "word": [ + 0, + 4, + 6, + 2, + 1, + 5, + 2, + 1, + 6, + 0, + 1, + 3, + 2, + 0, + 1, + 4, + 2, + 0, + 5, + 3 + ] + }, + "extended_word_L22": { + "coverage": 126, + "first_reached_at_restart": 12, + "missing": [ + 91, + 98 + ], + "params": { + "L": 22, + "kick": 8, + "restarts": 600, + "seed": 21 + }, + "word": [ + 5, + 2, + 1, + 0, + 2, + 3, + 1, + 4, + 2, + 3, + 0, + 6, + 1, + 3, + 5, + 1, + 2, + 0, + 6, + 0, + 3, + 4 + ] + } + }, + "note": "deterministic CPython random; L=24 control finds 128/128 in the same optimizer, so the 126/120 ceilings are landscape, not tool failure; ceilings are search failures, not exclusions" + }, + "tier5_census20": { + "complete": false, + "cycles": 67674177, + "nodes": 798901058, + "shards_done": 11, + "shards_total": 15, + "universal_words": 0 + } +} \ No newline at end of file diff --git a/research/universal-f7-singleton-l20-seed06704c39/CLAIM.md b/research/universal-f7-singleton-l20-seed06704c39/CLAIM.md new file mode 100644 index 0000000000..f2d08b924e --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/CLAIM.md @@ -0,0 +1,107 @@ +# Task card — kappa-blocker KB3b (local card, written before computation) + +Task ID / proposed scope key: drawn card `p104-side-correction` (track +`complex-mechanisms`, chooser OS seed `06704c399acc3c61ee5b20d9cc253f9b`, +catalogue scope key `72dfbf0708467ad34793`); **scope changed** to the assigned +kappa-blocker KB3b, the explicit open request continuing the sharp singleton +`f(7)` question (refined object: the `L = 20` / `L = 22` singleton universal +path at seven sources). + +Base commit; exact predecessor and dependency heads: +- base main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` (priority revision 4) +- predecessor https://github.com/CrocSwap/integer-mult-bounds/pull/2542 head + `3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf`, branch + `research/agent-58-f7-singleton-b859517b`, package + `research/universal-f7-singleton-seedb859517b` (KB3: `f(7) >= 20`) +- pinned record `research/universal-connector-six-source` (PR 1185 lineage) and + the PR943 model `research/universal-connector-boundary`, both at base + +Concrete object and question: in the PR943 prefix-walk model, restored source +words over seven singleton labels; `D(w) = {q_s xor q_t} = F2^7` universal, `f(n)` +the minimum length. Pinned `f(5) = 12`, `f(6) = 16`; after PR 2542 the gap is +`20 <= f(7) <= 24` (Gray bound `2^ceil(n/2) + 2^floor(n/2) = 24`). Question: +does a universal seven-source singleton word of length 20 or 22 exist (a +Gray-beating construction), or can length 20 be excluded (Gray's 24 sharp)? + +Scope status: **changed**; reason: authorized "explicit open request" scope +change recorded in `TASK.json`. The drawn complex-mechanisms cards +(`p104-side-correction`, `complex-rank-shape-decoder`, +`complex-new-helper-inventory`) were not taken; the orchestrator assigned KB3b +from discussion 1166 as the explicit open request (the recorded open boundary +"neither 20 nor 22 is excluded, and 24 is attained" of +`research/universal-connector-six-source/README.md`, continued by PR 2542's open +question 1). Taking this request instead of the drawn card is the recorded +scope change. + +Existing restriction being changed (or exact claim being audited): the recorded +gap `20 <= f(7) <= 24` in the singleton alphabet only. + +**Assignment premise correction (exact obstruction recorded early).** The +assignment's option (a) "exclude length 19" is dead on arrival in this model: +PR943's restoration facts force every label count even and `>= 2`, so every +restored word has even length (a closed hypercube walk; the cube is bipartite). +No length-19 word exists to census. The census "one step up" from length 18 is +therefore **length 20**, and (a) is executed as an L = 20 exclusion. + +Method; explicit parameter ranges/candidate alphabet: singleton alphabet +`{0..6}` only. (1) Reproduce PR 2542 and the pinned six-source numbers +byte-exactly (EXPECTED.json: n=5 L=10 words=945 max=31; n=6 L=12 words=10395 +max=49; n=6 L=14 words=945945 max=59; counting bounds 10/14/18; Gray 12/16/24; +PR 2542 census nodes=15,775,992 simple 18-cycles=312,064 universal=0). (2) Split +identity rows (`lemma_a_table`) for the L = 20 splits `(|E|,|O|)` in +{(10,10),(10,9),(9,10),(10,8),(8,10),(9,9)} and the L = 22 splits, with the +per-split collision budgets derived from the rows. (3) Construction route: +stochastic/exhaustive search of covering sets `P` (`|P| <= 20`, then `<= 22`) +with `P + P = F2^7`, checked for closed-walk realizability (Hamiltonian cycle +via subset DP/DFS); direct word-level search on length-20/22 restored words as +a second engine. (4) Exclusion route: extend the restricted-growth cycle census +to L = 20 with PR 2542's proved-necessary prunes (multiplicity room, +self-avoidance where the identity forces `|P| = L`, collision budget), sharded +by depth-3 prefix into resumable checkpoints. + +Nearest overlapping PRs and why this adds something: PR 2542 is the direct +predecessor (L = 18 excluded; its engine is vendored byte-exact with hash pin +and credit). Distinct concurrent scopes: DUO pair-source alphabet +(https://github.com/CrocSwap/integer-mult-bounds/pull/2396, +https://github.com/CrocSwap/integer-mult-bounds/pull/2128, +https://github.com/CrocSwap/integer-mult-bounds/pull/2156), sparse +weight-1/2/3-mask family (https://github.com/CrocSwap/integer-mult-bounds/pull/2229, +https://github.com/CrocSwap/integer-mult-bounds/pull/2236, +https://github.com/CrocSwap/integer-mult-bounds/pull/2397), four-root paired-call +(https://github.com/CrocSwap/integer-mult-bounds/pull/2282). None touches the +singleton `f(7)` word-length question; this package adds the next length step. + +Optimistic full cost budget; required observable improvement: no kappa, supplier +or frontier change; the observable is the recorded `f(7)` gap itself (either +`f(7) >= 22`, or `f(7) <= 22` with a checked word). + +Success evidence; falsification test; time/compute cap: exact coverage +verification of any found word (`word_is_universal`, dual-predicate +independent replay) plus byte-exact reproductions before any new number; for an +exclusion, complete per-split enumeration with leaf counts agreeing across +shards. Priced budget about 120 minutes; one bounded pivot maximum (first +construction search, pivot to the L = 20 census, or vice versa); early kill +with the exact obstruction (split rows, node counts, which splits completed) +recorded. + +Predecessor authors; intended artifact and reproduction command: PR943 model by +Ross Richardson (`research/universal-connector-boundary`); pinned record by +Douglas Colkitt (`research/universal-connector-six-source`, PR 1185); PR 2542 +engine by Aaron Wang with help from opencode +(`research/universal-f7-singleton-seedb859517b`). Intended artifact: this +package on branch `research/agent-61-f7-singleton-06704c39`; reproduction: + +```sh +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/verify.py +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/independent.py +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/test_engine.py +``` + +Pair-collision check (before computation, 2026-10-15 14:07-14:15 UTC): +`agent_tools.py disc-comments` (with nested replies) over discussions 1317 and +1166 since 2026-10-14, plus `scripts/find_overlap.py --refresh` on the object's +proper names ("universal source path", "singleton alphabet", "seven-source", +"Gray bound", "f(7)", "restricted-growth"). No fresh CLAIM on the singleton +`f(7)` object; the only related activity is my direct predecessor's KB3 +claim (discussion 1166 comment 18947532) and its FINDING/DONE at 14:02 UTC +(comment 18950671, PR 2542), both released. This card is its continuation. diff --git a/research/universal-f7-singleton-l20-seed06704c39/EXPECTED.json b/research/universal-f7-singleton-l20-seed06704c39/EXPECTED.json new file mode 100644 index 0000000000..7da4bd3129 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/EXPECTED.json @@ -0,0 +1,312 @@ +{ + "census20": { + "cycles": 67674177, + "nodes": 798901058, + "shards_total": 15, + "universal_words": 0 + }, + "conclusion": "f(7) in {20,22,24} unchanged; L=19 dead by parity; beating templates closed; covers walk-unrealisable in all samples; search ceilings 120/126/128 at L=20/22/24", + "cover20": { + "degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 2, + 3 + ], + "points": [ + 2, + 4, + 8, + 9, + 14, + 25, + 26, + 30, + 31, + 42, + 49, + 51, + 60, + 67, + 77, + 82, + 100, + 108, + 109, + 113 + ] + }, + "cover22": { + "degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 3 + ], + "points": [ + 1, + 2, + 9, + 19, + 30, + 35, + 36, + 45, + 48, + 49, + 59, + 61, + 68, + 72, + 77, + 83, + 86, + 89, + 93, + 104, + 109, + 111 + ] + }, + "pr2542_l18": { + "census_nodes": 15775992, + "simple_18_cycles": 312064, + "universal_words": 0 + }, + "search": { + "seconds": 132.0, + "set_k20": { + "best": 128, + "covers": 14, + "first_cover": [ + 2, + 4, + 8, + 9, + 14, + 25, + 26, + 30, + 31, + 42, + 49, + 51, + 60, + 67, + 77, + 82, + 100, + 108, + 109, + 113 + ], + "first_cover_degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 2, + 3 + ], + "first_cover_hamiltonian_cycle": false + }, + "set_k22": { + "best": 128, + "covers": 28, + "first_cover": [ + 1, + 2, + 9, + 19, + 30, + 35, + 36, + 45, + 48, + 49, + 59, + 61, + 68, + 72, + 77, + 83, + 86, + 89, + 93, + 104, + 109, + 111 + ], + "first_cover_degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 3 + ], + "first_cover_hamiltonian_cycle": false + }, + "word_L20": { + "coverage": 120, + "evals": 3274631, + "missing": [ + 30, + 39, + 42, + 52, + 82, + 83, + 116, + 117 + ], + "word": [ + 0, + 4, + 6, + 2, + 1, + 5, + 2, + 1, + 6, + 0, + 1, + 3, + 2, + 0, + 1, + 4, + 2, + 0, + 5, + 3 + ] + }, + "word_L22": { + "coverage": 126, + "evals": 4098654, + "missing": [ + 91, + 98 + ], + "word": [ + 5, + 2, + 1, + 0, + 2, + 3, + 1, + 4, + 2, + 3, + 0, + 6, + 1, + 3, + 5, + 1, + 2, + 0, + 6, + 0, + 3, + 4 + ] + }, + "word_L24_control": { + "coverage": 128, + "word": [ + 0, + 1, + 2, + 5, + 2, + 3, + 4, + 3, + 6, + 4, + 3, + 5, + 0, + 4, + 2, + 1, + 0, + 3, + 1, + 0, + 4, + 1, + 6, + 2 + ] + } + } +} \ No newline at end of file diff --git a/research/universal-f7-singleton-l20-seed06704c39/INDEPENDENT.json b/research/universal-f7-singleton-l20-seed06704c39/INDEPENDENT.json new file mode 100644 index 0000000000..9127828862 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/INDEPENDENT.json @@ -0,0 +1,7 @@ +{ + "cover_degrees_independent": "ok", + "dual_predicate": "ok", + "interval_xor_form": "ok", + "parity_rederived": "ok", + "witnesses_replayed": 0 +} \ No newline at end of file diff --git a/research/universal-f7-singleton-l20-seed06704c39/NOTICE.md b/research/universal-f7-singleton-l20-seed06704c39/NOTICE.md new file mode 100644 index 0000000000..65466f5893 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/NOTICE.md @@ -0,0 +1,32 @@ +# Notice and attribution + +* PR943 prefix-walk model, the query interface `D(w) = {q_s xor q_t}`, and the + first exact values: **Ross Richardson**, `research/universal-connector-boundary` + (https://github.com/CrocSwap/integer-mult-bounds/pull/943). +* Pinned five/six-source record (`f(5) = 12`, `f(6) = 16`, the `f(7)` gap, + counting bounds and Gray constructions), and the byte-exact EXPECTED.json + reproduced here: **Douglas Colkitt**, + `research/universal-connector-six-source` + (https://github.com/CrocSwap/integer-mult-bounds/pull/1185). +* Length-18 exclusion (`f(7) >= 20`), the restricted-growth cycle census + engine (`engine.py`, vendored here byte-exact, SHA-256 + `82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4`, + git blob `210bd817b19beb20ed474d8946ea87a22121ac1c` at head + `3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf`), the pair-representation + identity (`lemma_a_table`), and the proved-necessary census prunes: + **Aaron Wang, with help from opencode**, + `research/universal-f7-singleton-seedb859517b` + (https://github.com/CrocSwap/integer-mult-bounds/pull/2542). This package + re-runs that census in full and reuses the engine byte-exact; the reuse is + pinned in SOURCES.json and enforced by a test. +* Community set-level fact re-derived in PR 2542 as a control (nine-point + five-bit census, `r[(C2)^6] = 14` after Gavrylkiv): published at + https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18931315. + +This package (search campaign, template lemmas, covering-set artifacts, the +resumable simple-20-cycle census) is by **Aaron Wang, with help from opencode** +(substantial AI assistance in scoping, implementation, verification and +writing; no model named; no independent human review claimed). + +Repository and source licenses are unchanged; `research/universal-connector-six-source/LICENSE` +and the repository LICENSE both remain in force. diff --git a/research/universal-f7-singleton-l20-seed06704c39/README.md b/research/universal-f7-singleton-l20-seed06704c39/README.md new file mode 100644 index 0000000000..4fd4a0a98c --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/README.md @@ -0,0 +1,221 @@ +# KB3b — seven-source singleton `f(7)` continued: obstructions, cover dichotomy, resumable 20-cycle census + +**Recursive-interface finite result: the `L = 19` question is closed exactly, the +two natural Gray-beating templates are closed by proved lemmas, and the +`L = 20` / `L = 22` word question is advanced to a reproducible search ceiling +plus a resumable census. No new kappa.** + +In the PR943 prefix-walk model +([Ross Richardson, `research/universal-connector-boundary`](https://github.com/CrocSwap/integer-mult-bounds/pull/943)), +a restored source word `w` over seven singleton labels is *universal* when +paired readouts realize every mask, `D(w) = {q_s xor q_t} = F2^7`, and `f(n)` is +the minimum word length. The pinned record +([Douglas Colkitt, `research/universal-connector-six-source`](https://github.com/CrocSwap/integer-mult-bounds/pull/1185)) +is `f(5) = 12`, `f(6) = 16`, `18 <= f(7) <= 24`; the predecessor of this +package removed 18 +([PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542), `f(7) >= 20`), +so the recorded gap is `20 <= f(7) <= 24`, with the Gray bound 24 attained. + +This package continues the question (kappa-blocker KB3b) and delivers: + +> **1. Length 19 is closed exactly — but for a structural reason.** Every +> restored word has even length (all label counts are even and `>= 2`), so no +> odd length exists to census. The assignment's literal "exclude length 19" is +> discharged by PR943's restoration facts, and the census step-up from 18 is +> `L = 20`. +> +> **2. Two natural Gray-beating templates are impossible** (proved lemmas, +> machine spot-checked): the *disjoint product* family cannot beat 24 in even +> length, and the *square-detour / transversal* family has no realization at +> any length (its walk forces a connected transversal, which cannot cover). +> +> **3. Set covers of `F2^7` at 20 points exist** (explicit verified example +> below; set-ILS finds them in 14 of 30 restarts) — but every cover sampled +> (463 at `k = 20/22`) has isolated vertices in the hypercube, hence admits no +> closed walk at any length. Walk-shaped sets and covering sets look disjoint +> at `k <= 22`: this is quantified evidence, not an exclusion. +> +> **4. A deterministic search campaign with an `L = 24` non-vacuity control** +> tops out at `120/128` (length 20), `126/128` (length 22) and finds `128/128` +> at length 24 (control). Extended 600-restart runs confirm both ceilings. +> These are search failures, not exclusions. +> +> **5. A resumable restricted-growth simple-20-cycle census** (the `|P| = 20`, +> `(10,10)` split of `L = 20`, with PR 2542's proved-necessary prunes and the +> split-identity budget `e_ex + b_ex <= 27`) runs to the priced budget with +> exact per-shard node counts checkpointed in `CENSUS20-PROGRESS.json`. + +The gap `20 <= f(7) <= 24` is unchanged; no supplier, tariff, certificate or +selected-frontier change is claimed. The DUO pair-source line +([https://github.com/CrocSwap/integer-mult-bounds/pull/2396](https://github.com/CrocSwap/integer-mult-bounds/pull/2396), +[https://github.com/CrocSwap/integer-mult-bounds/pull/2128](https://github.com/CrocSwap/integer-mult-bounds/pull/2128), +[https://github.com/CrocSwap/integer-mult-bounds/pull/2156](https://github.com/CrocSwap/integer-mult-bounds/pull/2156)) +and the sparse weight-1/2/3 family +([https://github.com/CrocSwap/integer-mult-bounds/pull/2229](https://github.com/CrocSwap/integer-mult-bounds/pull/2229), +[https://github.com/CrocSwap/integer-mult-bounds/pull/2236](https://github.com/CrocSwap/integer-mult-bounds/pull/2236), +[https://github.com/CrocSwap/integer-mult-bounds/pull/2397](https://github.com/CrocSwap/integer-mult-bounds/pull/2397)) +are distinct alphabets or mask families. + +## Model (two equivalent forms) + +PR943's: dirty `F2` arrays, complete calls `B_j: z += B_j x_j`, paired output +readouts; the boundary states `q_t` walk the hypercube from 0 and `D(w)` is the +set of pairwise XORs of the boundary states. Universality is `P + P = F2^n` +for the prefix set `P`. Equivalently — the form used by the search here — +`D(w)` is the set of XORs of *contiguous subwords* of `w` (interval XORs), plus +the empty block for the zero mask. Restored words have every label count even +and `>= 2`, so lengths are even and walks are closed. + +## Reproduce + +From the repository root, standard library only, Python 3.12: + +```sh +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/verify.py +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/independent.py +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/test_engine.py +python3 -I -B research/universal-f7-singleton-l20-seed06704c39/census20.py # resumable +``` + +Expected markers: `PASS_F7_L20_VERIFY ...`, `PASS_F7_L20_INDEPENDENT {...}`, +`Ran 14 tests ... OK`, and `CENSUS20 COMPLETE|PARTIAL shards=... nodes=...`. +The deterministic search campaign is `search.py` (CI-sized); `search.py +--extended` runs the 600-restart session budget. + +## Smallest falsifying instance first: reproduction + +Before any new number, `verify.py` rebuilds the pinned +[`research/universal-connector-six-source/EXPECTED.json`](https://github.com/CrocSwap/integer-mult-bounds/blob/main/research/universal-connector-six-source/EXPECTED.json) +byte-for-byte (histograms and records SHA-256 included): + +| Census | Canonical words | Max `|D(w)|` | Records SHA-256 (prefix) | Matches pinned | +|---|---:|---:|---|---| +| `n = 5`, length 10 | 945 | 31 / 32 | `3dcc5689a4a34bae…` | yes | +| `n = 6`, length 12 | 10,395 | 49 / 64 | `491b295f12cfa34a…` | yes | +| `n = 6`, length 14 | 945,945 | 59 / 64 | `3d711ffa19209310…` | yes | + +plus the counting lower bounds `10/14/18` and the Gray constructions +`12/16/24`. It then **fully re-runs PR 2542's decisive census** and reproduces +`15,775,992` nodes, `312,064` simple 18-cycles, zero universal words — the +predecessor engine is vendored byte-exact (SHA-256 pinned in `SOURCES.json`, +enforced by `test_engine.py`) and its numbers are not taken on trust. + +## The exact obstructions + +**Parity (closes length 19, and every odd length).** A restored word has each +label count even, so `|w|` is even; equivalently the cube is bipartite and a +closed walk has even length. `patterns(7, 19)` is empty and the test asserts +it. This is PR943's restoration fact, recorded here because the assignment's +option (a) asked for the length-19 exclusion literally. + +**Square-detour / transversal template.** The most structured way to beat 24 +is a subcycle through a 16-point set `R` in a half-space plus a 6-call detour +`[6, i, j, i, j, 6]` over a coordinate square `sq = span(e_i, e_j)`. Odd-mask +coverage then forces `|R|·|sq| = 64`, so `R` is a transversal of `sq`; write +`R = {t + g(t) : t in F2^4}`. Two induced-cube facts close it: + +* `G[R]` has an edge between `t + g(t)` and `t' + g(t')` only when + `t' = t + e_k` and `g(t) = g(t')` (a transversal has no two points in one + `sq`-coset). So the components of `G[R]` are the components of the level + sets of `g`. Any closed walk spanning `R` needs `G[R]` connected, i.e. `g` + constant. +* But `g` constant makes `R + R` the 16-point plane `F2^4 x {q}`, missing 48 + of the 64 masks needed from within-layer sums. + +So no word of this template is universal at any length. The two component +claims are machine spot-checked (`test_engine.py::TestTransversalLemma`). + +## The cover / walk dichotomy at `k = 20` and `k = 22` + +Set-ILS (`search.py::set_search`, steepest ascent over point swaps) finds +covering sets easily: + +| `k` | covers found | first cover's induced degrees | closed walk? | +|---:|---:|---|---| +| 18 | 0 (max 118/128, 40 restarts) | — | — | +| 19 | 0 (max 124/128, 200 restarts) | — | — | +| 20 | 14 / 30 restarts | `[0,0,0,0,0,0,1,1,1,1,1,1,1,1,1,2,2,2,2,3]` | no (min degree 0) | +| 22 | 28 / 30 restarts | `[0,0,0,0,0,0,0,1,1,1,1,1,1,1,1,1,1,1,2,2,2,3]` | no (min degree 0) | + +The stored `cover20` (20 points, verified `|P + P| = 128` exactly) is the +deterministic first cover of the campaign. Every cover sampled at `k = 20/22` +(175 and 288 in the session sweeps, plus the campaign's) has an isolated +vertex, so no closed walk spans it at *any* length. Conversely the word-side +search below never reaches a cover. This is the `n = 5` dichotomy +(99,200 ten-point covers, none cycle-realisable, `f(5) = 12`) at `n = 7`, and +it is quantified evidence only: no lemma yet separates the two families. + +## Search campaign (deterministic, with non-vacuity control) + +`search.py` runs steepest-ascent ILS over restored words (transpositions, +segment reversals, kicks) and over sets, fixed seeds: + +| Stage | Budget | Result | +|---|---|---| +| word `L = 24` (control) | 30 restarts | **128/128 found** (`[0,1,2,5,2,3,4,3,6,4,3,5,0,4,2,1,0,3,1,0,4,1,6,2]`) | +| word `L = 22` | 40 restarts | 126/128 (missing 2) | +| word `L = 20` | 40 restarts | 120/128 (missing 8) | +| extended `L = 22` | 600 restarts | 126/128 (confirmed) | +| extended `L = 20` | 600 restarts | 120/128 (confirmed) | + +The control is the point: the same optimizer finds the known universal 24-word +(and a non-Gray one) in seconds, so the 126/120 ceilings are landscape, not +tool failure. The predecessor's annealer had already reported 126/128 at +length 22; the ceilings here agree and add the `L = 20` and control numbers. + +## The resumable simple-20-cycle census + +`census20.py` enumerates every canonical restored length-20 word with distinct +boundary states (a simple 20-cycle; `|P| = 20` forces the `(10,10)` split) +using PR 2542's proved-necessary prunes: multiplicity room, self-avoidance +(justified by `|P| = L` here) and the pair-representation collision budget +`e_ex + b_ex <= 27`. Shards are the Bell(4) = 15 restricted-growth depth-4 +prefixes, exactly one per canonical word; +`CENSUS20-PROGRESS.json` checkpoints each subtree, so the census resumes and a +partial run still records exact node/leaf counts. **Status at submission +(2026-10-15): 11 of 15 shards complete, covering 798,901,058 nodes and +67,674,177 simple 20-cycles with zero universal words.** The small shards die +instantly on the self-avoidance prune (27 nodes total); the completed heavy +shard `0102` alone accounts for 798,901,031 nodes and 67,674,177 cycles. The +three remaining heavy subtrees (`0120`, `0121`, `0123`) are of the same order — +a capped probe of `0123` passes 5,000,000 nodes in 21.4 s (234,169 nodes/s) — +so completing the `(10,10)` exclusion needs several more hours of the same +exact enumeration, resumed from the checkpoint. No universal word appears in +the 67.7 million cycles checked so far. + +Length-20 words with repeated boundary states (`|P|` in `{17, 18, 19}`) are +**not** covered by this census; the L = 20 split identity admits `(10,7)` / +`(7,10)` and `(10,8)` / `(8,10)` / `(9,9)` / `(10,9)` families, which need +multiset collision semantics with per-split budgets. That is the recorded open +remainder of option (a). + +## Scope and remaining obligations + +A finite study inside PR943's abstract interface; no instantiation in the +selected supplier and no kappa claim. What was **not** checked: the repeated- +state `L = 20` splits, the `L = 22` census splits, and any set-level exhaustive +enumeration (the joint tree needs orbit reduction, as PR 2542 records). +Common-label/mutable-source realization, frames, owner admission, full-row +charging, compiler integration and precision remain as PR943 lists them. + +## Open next questions + +1. **Does a universal `L = 20` or `L = 22` word with repeated boundary states + exist, or is the Gray bound 24 sharp?** Why it matters: it settles + `f(7) in {20, 22, 24}`. First step: extend `census20.py` to the repeated- + state splits with per-split budgets from `lemma_a_table`, and the simple + `(11,11)` split at `L = 22`. Blocked by: multiset collision semantics per + split and tree growth past the simple-cycle census. +2. **Is `r((C2)^7) = 20`?** (PR 2542's open question 2 sharpened: 20-point + covers exist, 19-point ones were not found in 200 restarts.) First step: + shard the joint `(E, O)` enumeration for the `k = 19` splits or orbit-reduce + under the 5,040 coordinate permutations. Blocked by: the raw joint tree. +3. **Are covers and walk-shape incompatible at `k <= 22`?** Every sampled + cover has an isolated vertex. A proof would give `f(7) = 24` together with + the `L = 22` exclusion. First step: constrained search maximizing `|P+P|` + over cycle-shaped sets, or an autocorrelation obstruction for sets + containing a Hamiltonian cycle. Blocked by: no structural lemma yet. + +See [CLAIM.md](CLAIM.md) for the task card, [TASK.json](TASK.json) for the +scope change, [SOURCES.json](SOURCES.json) for pins and credit, +[NOTICE.md](NOTICE.md) for attribution. diff --git a/research/universal-f7-singleton-l20-seed06704c39/SEARCH.json b/research/universal-f7-singleton-l20-seed06704c39/SEARCH.json new file mode 100644 index 0000000000..ecbcf6edab --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/SEARCH.json @@ -0,0 +1,202 @@ +{ + "seconds": 132.0, + "set_k20": { + "best": 128, + "covers": 14, + "first_cover": [ + 2, + 4, + 8, + 9, + 14, + 25, + 26, + 30, + 31, + 42, + 49, + 51, + 60, + 67, + 77, + 82, + 100, + 108, + 109, + 113 + ], + "first_cover_degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 2, + 3 + ], + "first_cover_hamiltonian_cycle": false + }, + "set_k22": { + "best": 128, + "covers": 28, + "first_cover": [ + 1, + 2, + 9, + 19, + 30, + 35, + 36, + 45, + 48, + 49, + 59, + 61, + 68, + 72, + 77, + 83, + 86, + 89, + 93, + 104, + 109, + 111 + ], + "first_cover_degrees": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 2, + 2, + 2, + 3 + ], + "first_cover_hamiltonian_cycle": false + }, + "word_L20": { + "coverage": 120, + "evals": 3274631, + "missing": [ + 30, + 39, + 42, + 52, + 82, + 83, + 116, + 117 + ], + "word": [ + 0, + 4, + 6, + 2, + 1, + 5, + 2, + 1, + 6, + 0, + 1, + 3, + 2, + 0, + 1, + 4, + 2, + 0, + 5, + 3 + ] + }, + "word_L22": { + "coverage": 126, + "evals": 4098654, + "missing": [ + 91, + 98 + ], + "word": [ + 5, + 2, + 1, + 0, + 2, + 3, + 1, + 4, + 2, + 3, + 0, + 6, + 1, + 3, + 5, + 1, + 2, + 0, + 6, + 0, + 3, + 4 + ] + }, + "word_L24_control": { + "coverage": 128, + "word": [ + 0, + 1, + 2, + 5, + 2, + 3, + 4, + 3, + 6, + 4, + 3, + 5, + 0, + 4, + 2, + 1, + 0, + 3, + 1, + 0, + 4, + 1, + 6, + 2 + ] + } +} \ No newline at end of file diff --git a/research/universal-f7-singleton-l20-seed06704c39/SOURCES.json b/research/universal-f7-singleton-l20-seed06704c39/SOURCES.json new file mode 100644 index 0000000000..b1c4467d96 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/SOURCES.json @@ -0,0 +1,53 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/universal-connector-six-source/EXPECTED.json", + "usage": "input", + "git_blob": "160a96c50f77ba411af957b554da05a8470e70ca", + "sha256": "f1b1bec330640c81ac0da25ee8b3a0a49fe9ea5bb2eadaaa787c64bd62c9e73a" + }, + { + "path": "research/universal-connector-six-source/README.md", + "usage": "provenance", + "git_blob": "c7123c3cfd7545deb6af607800df0d15c6e8c0d2", + "sha256": "ea9cca56d1547dcd984f5f99f6c6243c9417a7ede08f68782c7a6616aa6eb563" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ], + "references": [ + { + "pr": 2542, + "source_path": "research/universal-f7-singleton-seedb859517b/engine.py", + "local_path": "engine.py", + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "note": "Vendored byte-exact (copied, never imported from the predecessor package). The live drift check pins base-commit blobs only, so this head-pinned vendor copy is enforced by test_engine.py's engine_byte_pin test instead." + }, + { + "pr": 2542, + "source_path": "research/universal-f7-singleton-seedb859517b/README.md", + "local_path": null, + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "note": "Predecessor method and length-18 certificate reproduced here in full; see NOTICE.md." + } + ], + "notes": { + "model_and_pinned_results": "PR943 query model (research/universal-connector-boundary, Ross Richardson); pinned f(5)=12, f(6)=16 and the open f(7) gap (research/universal-connector-six-source, Douglas Colkitt, https://github.com/CrocSwap/integer-mult-bounds/pull/1185). Read and reproduced byte-exactly, never imported.", + "predecessor": "Length-18 exclusion, f(7) >= 20: https://github.com/CrocSwap/integer-mult-bounds/pull/2542 (Aaron Wang with help from opencode, package research/universal-f7-singleton-seedb859517b). Its engine is vendored byte-exact and its decisive census is fully re-run in verify.py.", + "concurrent_scopes": "DUO pair-source alphabet: https://github.com/CrocSwap/integer-mult-bounds/pull/2396, https://github.com/CrocSwap/integer-mult-bounds/pull/2128, https://github.com/CrocSwap/integer-mult-bounds/pull/2156. Sparse weight-1/2/3 masks: https://github.com/CrocSwap/integer-mult-bounds/pull/2229, https://github.com/CrocSwap/integer-mult-bounds/pull/2236, https://github.com/CrocSwap/integer-mult-bounds/pull/2397. Four-root paired-call: https://github.com/CrocSwap/integer-mult-bounds/pull/2282. This package is the singleton alphabet only." + } +} diff --git a/research/universal-f7-singleton-l20-seed06704c39/TASK.json b/research/universal-f7-singleton-l20-seed06704c39/TASK.json new file mode 100644 index 0000000000..ab650ad00f --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/TASK.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "session_seed": "06704c399acc3c61ee5b20d9cc253f9b", + "track": "complex-mechanisms (drawn); scope changed to assigned kappa-blocker KB3b", + "scope_key": "72dfbf0708467ad34793", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18951166", + "original_card": { + "id": "p104-side-correction", + "question": "Can the native P104 low-rank channel be completed with a legal, fully charged I-G/2 side correction?", + "starting_points": [ + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the P104 open next questions and its fixed local histogram; inspect why appending I-G/2 after source completion is not justified. #1991 supplies the checked native channel, not the missing correction.", + "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." + }, + "first_experiment": "Choose one exact side-correction cut and bound its allowed cost from a favorable completed moment at a declared target. Stop or hand off if the necessary source/target access cannot be justified or even the optimistic total misses the target.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991" + ] + }, + "scope_status": "changed", + "actual_scope": "Kappa-blocker KB3b: the sharp singleton f(7) question in the PR943 prefix-walk model continued after PR 2542 (f(7) >= 20): (a) exclude the next length up from 18 (the assignment's literal 'length 19'; in this model the census step-up is L = 20), or (b) construct a universal seven-source singleton word of length below the Gray bound 24, with exact coverage verification either way. Delivered: the literal length-19 question is closed exactly (parity: every restored word has even length), the two natural beating templates are closed by proved lemmas, 20-point covers of F2^7 are shown to exist but to be walk-unrealizable in every sampled case, a deterministic search campaign with an L = 24 non-vacuity control records ceilings 120/126/128 at lengths 20/22/24, and a resumable simple-20-cycle census is run as far as the priced budget allows with exact node counts recorded.", + "scope_change_reason": "Authorized 'explicit open request' scope change, recorded as instructed by the assignment: taking the open f(7) request from discussion 1166 (the recorded open boundary 'neither 18, 20 nor 22 is excluded, and 24 is attained' of research/universal-connector-six-source/README.md, continued as PR 2542 open question 1 after comment 18950671) instead of the drawn card. The chooser (OS seed 06704c399acc3c61ee5b20d9cc253f9b) drew the complex-mechanisms cards p104-side-correction / complex-rank-shape-decoder / complex-new-helper-inventory; the assignment states the draw landed on saturated cards and authorizes KB3b as the explicit open request. Pair-collision checks (discussions 1166 and 1317 with nested replies, plus find_overlap.py --refresh on the object's proper names) found no other claim on this object; the only related activity is my own released predecessor KB3 (PR 2542).", + "bottleneck_link": "A verified finite exclusion or construction inside the PR943 query model moves the recorded singleton f(7) gap (20 <= f(7) <= 24) that downstream batch bills cite. It changes no supplier, tariff or kappa and instantiates no physical interface.", + "object_synonyms_used_in_overlap": [ + "universal source path", + "universal word", + "restored source word", + "singleton alphabet", + "seven-source", + "seven sources", + "Gray bound", + "f(7)", + "restricted-growth", + "prefix walk", + "paired readout", + "interval XOR", + "hypercube closed walk", + "additive basis F2^7" + ], + "pair_collision_check": { + "checked_utc": "2026-10-15T14:07:00Z/2026-10-15T14:15:00Z", + "tool": "agent_tools.py disc-comments (with nested replies) + scripts/find_overlap.py --refresh", + "threads_scanned": [ + "discussion 1317 since 2026-10-14T00:00:00Z", + "discussion 1166 since 2026-10-14T00:00:00Z (full dump incl. nested replies, 1307 lines)" + ], + "result": "No fresh CLAIM on the singleton f(7) object. The only related activity is the released predecessor KB3 claim (comment 18947532) and its FINDING/DONE at 14:02 UTC (comment 18950671, PR 2542). DUO pair-source (PR 2396), sparse weight-1/2/3 (PRs 2229/2236/2397) and four-root paired-call (PR 2282) work is concurrent but distinct in alphabet or mask family." + }, + "smallest_falsifying_instance_first": "Before any new number: PR 2542's verify.py/independent.py/test_engine.py reproduced (PASS_F7_SINGLETON_GAP_VERIFY cycles=312064 universal_words=0 nodes=15775992; PASS_F7_INDEPENDENT; 22 tests OK), including the byte-exact pinned research/universal-connector-six-source/EXPECTED.json comparison (945/31, 10395/49, 945945/59 with records SHA-256), counting bounds 10/14/18 and Gray constructions 12/16/24. Then the L = 24 non-vacuity control before trusting any search ceiling.", + "priced_budget_minutes": 150, + "priced_budget_breakdown": "15 min entry overlap + pair-collision checks (done), 15 min predecessor reproduction (done), 20 min landscape probes and template analysis (done), 35 min deterministic and extended search campaigns (done; extended L=20 600-restart run confirms the 120 ceiling), 40 min resumable simple-20-cycle census (sharded checkpoint; exact node counts recorded whatever completes), 25 min package, verification, gate and submission.", + "de_diagnostic": "Not applicable: a finite connector-path boundary 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 coverage verification against the pinned reproductions; no kappa, supplier or selected-frontier change is claimed.", + "stop_rule": "Stop at the first of: (a) a verified universal word of length < 24 (f(7) <= that length), (b) a complete simple-20-cycle census giving 'no universal simple 20-cycle', or (c) the priced budget expiring with the exact obstruction recorded (which shards completed, node counts, and which L=20 families remain open). One bounded pivot maximum: primary construction search, pivot to the L = 20 census. No second pivot.", + "outcome": "partial", + "evidence": "CERTIFICATE.json records: the byte-exact pinned reproductions (945/31, 10395/49, 945945/59 with records SHA-256; counting bounds 10/14/18; Gray 12/16/24); a full re-run of PR 2542's length-18 census (15,775,992 nodes, 312,064 simple 18-cycles, zero universal words) against the vendored byte-pinned engine; the parity obstruction (no odd-length restored word: assignment option (a) as literally stated is discharged); the square-detour/transversal template lemma (level-set components versus coverage, spot-checked); covering-set artifacts at k=20 and k=22 with exact coverage, induced-degree histograms and non-Hamiltonicity, and the walk-shape dichotomy over 463 sampled covers; the deterministic search campaign with the L=24 non-vacuity control (ceilings 120/126/128 at L=20/22/24, extended 600-restart runs confirming 120/126); and the resumable simple-20-cycle census checkpoint (CENSUS20-PROGRESS.json with exact per-shard node counts; status recorded in the README). search.py builds the campaign; verify.py replays everything; independent.py re-checks coverage with the dual predicate, the interval-XOR formulation and the position-pair formulation; test_engine.py holds 14 tests including the engine byte-pin and the transversal level-set lemma. No kappa claim.", + "author": "Aaron Wang", + "ai_assistance": "Substantial AI assistance from opencode in scoping, implementation, verification and writing (no model named); no independent human review claimed.", + "open_questions": [ + { + "question": "Does a universal seven-source singleton word of length 20 or 22 exist at all (with repeated boundary states, |P| < L), or is the Gray bound 24 sharp?", + "why_it_matters": "It settles f(7) in {20, 22, 24} and the all-127-row batch bill inside the unchanged PR943 model.", + "first_step": "Extend the resumable restricted-growth census to the repeated-state L=20 splits (10,9), (10,8), (9,9), (10,7) with per-split collision budgets derived from lemma_a_table rows, and to the simple L=22 (11,11) split; the deterministic ILS ceilings 120/126 with an L=24 control are the search-level baseline to beat.", + "blocked_by": "The repeated-state splits need multiset collision semantics with per-split budgets and grow well past the simple-cycle tree; the full L=20 tree at ~nodes-per-shard recorded in CENSUS20-PROGRESS.json exceeds a single session at the observed node rate." + }, + { + "question": "Is r((C2)^7) = 20, i.e. do 19-point or 18-point covers of F2^7 exist (the restricted addition basis value; PR 2542 open question 2)?", + "why_it_matters": "It settles the set-level analogue of the community's r((C2)^6) = 14 fact and bounds how small a walk's prefix set could be.", + "first_step": "Shard the joint (E,O) cover enumeration for splits (10,9), (9,10), (10,8), (8,10), (9,9) at k=19 and (9,9) at k=18 with the shared-support identity, or orbit-reduce under the 5,040 coordinate permutations as PR 2542's open question 2 records.", + "blocked_by": "Set-level ILS finds 20-point covers easily (14 in 30 restarts) but no 19-point cover in 200 restarts (max 124/128); the exact joint tree stalls without orbit reduction. Search failure is not an exclusion." + }, + { + "question": "Can a covering set be walk-shaped at all: does any cover of F2^7 at k in {20, 22} have min induced hypercube degree >= 2 (a closed-walk precondition)?", + "why_it_matters": "Every sampled cover has isolated vertices (463 covers at k=20/22, all with min degree 0), while every walk-shaped set the ILS reaches stops at 126/128; a proof that covers and walk-shape are incompatible at k <= 22 would give f(7) = 24 (Gray sharp) by PR 2542's f(7) >= 20 plus a length-22 exclusion.", + "first_step": "Run a constrained search maximizing |P+P| over cycle-shaped sets (the word ILS with more budgets/stronger moves), or derive an additive-combinatorial obstruction for autocorrelation-covering sets that contain a Hamiltonian cycle.", + "blocked_by": "No structural lemma yet: covers exist with slack (190 pair sums at k=20) and the walk constraint is combinatorial, not additive." + } + ] +} \ No newline at end of file diff --git a/research/universal-f7-singleton-l20-seed06704c39/VERIFY.json b/research/universal-f7-singleton-l20-seed06704c39/VERIFY.json new file mode 100644 index 0000000000..75e2434d67 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-six-source/EXPECTED.json" + ], + "commands": [ + { + "argv": ["{python}", "-I", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Byte-exact reproduction of the pinned five/six-source censuses (945/31, 10395/49, 945945/59 with records SHA-256), counting bounds 10/14/18 and Gray constructions 12/16/24; full re-run of PR 2542's length-18 census (15,775,992 nodes, 312,064 simple 18-cycles, zero universal words); the parity and transversal-template obstructions; exact replay of the stored covering sets (coverage, induced degrees, non-Hamiltonicity); deterministic re-run of the search campaign against EXPECTED.json; replay of the resumable simple-20-cycle census checkpoint" + }, + { + "argv": ["{python}", "-I", "-B", "{package}/independent.py"], + "timeout_seconds": 120, + "checks": "Different-method cross-checks: dual-predicate coverage, independent interval-XOR formulation, position-pair formulation, independently written induced-degree loop for the covering sets, parity re-derivation" + }, + { + "argv": ["{python}", "-I", "-B", "{package}/test_engine.py"], + "timeout_seconds": 200, + "checks": "Unit tests: vendored engine byte-pin, pinned n=5 reproduction, parity lemma at code level, coverage-form agreement, transversal level-set component lemma on a deterministic sample, cover artifacts, deterministic set-ILS hit, shard partitioning, L=20 split-identity rows" + } + ] +} diff --git a/research/universal-f7-singleton-l20-seed06704c39/census20.py b/research/universal-f7-singleton-l20-seed06704c39/census20.py new file mode 100644 index 0000000000..649272d37b --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/census20.py @@ -0,0 +1,69 @@ +#!/usr/bin/env python3 +"""Resumable restricted-growth simple-20-cycle census at n = 7 (split (10,10)). + +Scope: every canonical restored word of length 20 whose 20 boundary states are +distinct (a simple 20-cycle; |P| = 20 forces the (10,10) split). Prunes are +PR 2542's proved-necessary ones: multiplicity room, self-avoidance (justified +by |P| = L here), and the pair-representation collision budget e_ex + b_ex <= 90 - 63 = 27. +Words with repeated boundary states (|P| in {17,18,19}) are NOT covered by +this census; they are recorded as the open remainder. + +Shards are the restricted-growth prefixes of depth 4 (Bell(4) = 15 subtrees, +exactly one per canonical word). CENSUS20-PROGRESS.json checkpoints after +each shard, so the run is resumable and a partial run still records exact +node/leaf counts. +""" +import json +import sys +import time +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from engine import cyclic_census, rg_prefixes, word_is_universal + +HERE = Path(__file__).resolve().parent +PROGRESS = HERE / "CENSUS20-PROGRESS.json" + + +def main(): + t0 = time.time() + if PROGRESS.exists(): + progress = json.loads(PROGRESS.read_text(encoding="utf-8")) + else: + progress = {"done": {}, "accum": {"nodes": 0, "leaves": 0, "hits": 0, + "words": []}} + shards = rg_prefixes(7, 4) + for pref in shards: + key = "".join(map(str, pref)) + if key in progress["done"]: + continue + r = cyclic_census(7, 20, budget=27, simple=True, prefix=pref) + progress["done"][key] = { + "nodes": r["nodes"], "leaves": r["leaves"], "hits": r["hits"], + "words": [list(w) for w in r["words"]], + } + acc = progress["accum"] + acc["nodes"] += r["nodes"] + acc["leaves"] += r["leaves"] + acc["hits"] += r["hits"] + acc["words"].extend([list(w) for w in r["words"]]) + progress["shards_total"] = len(shards) + PROGRESS.write_text(json.dumps(progress), encoding="utf-8") + print(f"SHARD {key} nodes={r['nodes']} leaves={r['leaves']} " + f"hits={r['hits']} total_nodes={acc['nodes']} " + f"done={len(progress['done'])}/{len(shards)} " + f"secs={round(time.time()-t0, 1)}") + + acc = progress["accum"] + for w in acc["words"]: + assert word_is_universal(tuple(w), 7) and len(w) == 20 + complete = len(progress["done"]) == len(shards) + print(f"CENSUS20 {'COMPLETE' if complete else 'PARTIAL'} " + f"shards={len(progress['done'])}/{len(shards)} nodes={acc['nodes']} " + f"cycles={acc['leaves']} universal_words={len(acc['words'])}") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/universal-f7-singleton-l20-seed06704c39/engine.py b/research/universal-f7-singleton-l20-seed06704c39/engine.py new file mode 100644 index 0000000000..210bd817b1 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/engine.py @@ -0,0 +1,561 @@ +#!/usr/bin/env python3 +"""Exact engine for the singleton universal source path problem (PR943 model). + +A restored source word w over n labels has even label counts >= 2; its prefix +parity states are the vertices of a closed walk on the n-cube starting at 0; +paired readouts realize D(w) = {q_s xor q_t} = P + P for the prefix vertex set +P. A word is universal iff P + P = F2^n. f(n) is the minimum word length. + +This module is standard library only and computes coverage with exact integer +bitmasks (one bit per element of F2^n; no floating point anywhere). +""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations + +# ------------------------------------------------------------------ coverage + + +def prefixes(word): + """Prefix parity states q_0..q_L of a word (list of label indices).""" + out, q = [0], 0 + for j in word: + q ^= 1 << j + out.append(q) + return out + + +def coverage_mask(points, n=None): + """Bitmask of P + P = {a xor b : a, b in P} over F2^n.""" + if n is None: + n = max(p.bit_length() for p in points) if points else 0 + size = 1 << n + mask = 0 + pts = list(points) + for i, a in enumerate(pts): + for b in pts[i:]: + mask |= 1 << (a ^ b) + return mask & ((1 << size) - 1) + + +def coverage_size(word): + """|D(w)| for a source word: pairwise XORs of its prefix states.""" + return word_coverage(word) + + +def word_coverage(word): + return coverage_mask(prefixes(word)).bit_count() + + +def word_is_restored(word, n): + counts = [0] * n + for j in word: + if not 0 <= j < n: + return False + counts[j] += 1 + return all(c > 0 and c % 2 == 0 for c in counts) + + +def word_is_universal(word, n): + return word_is_restored(word, n) and word_coverage(word) == 1 << n + + +# --------------------------------------------------------------- construction + + +def gray_word(n): + """Reflected-Gray construction: 2^ceil(n/2) + 2^floor(n/2) calls.""" + k = (n + 1) // 2 + + def block(m, offset): + if m == 0: + return [] + g = [t ^ (t >> 1) for t in range(1 << m)] + steps = [] + for t in range(1 << m): + diff = g[t] ^ g[(t + 1) % (1 << m)] + steps.append(offset + diff.bit_length() - 1) + return steps + + return block(k, 0) + block(n - k, k) + + +# ------------------------------------------------------------------ word census + + +def restricted_growth_words(n, length): + """Canonical restored words: labels in first-occurrence order. + + Every label used, every count even and at least two (forced by the + parity/room feasibility test at the leaves). + """ + word = [0] * length + count = [0] * n + + def rec(i, used): + odd = 0 + for j in range(used): + odd += count[j] & 1 + if odd + 2 * (n - used) > length - i: + return + if i == length: + yield tuple(word) + return + for j in range(min(used + 1, n)): + word[i] = j + count[j] += 1 + yield from rec(i + 1, used + 1 if j == used else used) + count[j] -= 1 + + yield from rec(0, 0) + + +def census_words(n, length): + """Histogram, records SHA-256 and word count for all canonical words. + + Records are 'word:size' lines sorted and joined with newlines, matching + the pinned research/universal-connector-six-source/EXPECTED.json format. + """ + hist = Counter() + records = [] + words = 0 + for word in restricted_growth_words(n, length): + size = word_coverage(word) + hist[size] += 1 + records.append("".join(map(str, word)) + ":" + str(size)) + words += 1 + digest = sha256("\n".join(sorted(records)).encode()).hexdigest() + return hist, digest, words + + +# ------------------------------------------------------------ counting bounds + + +def counting_least_even_L(n): + """Least even L with feasible prefix-parity split sizes at length L. + + Split sizes s = |E|, t = |O| obey s, t <= L/2, s*t >= 2^(n-1) (odd masks) + and C(s,2) + C(t,2) >= 2^(n-1) - 1 (even nonzero masks). + """ + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + L = 2 + while True: + half = L // 2 + for s in range(1, half + 1): + for t in range(1, half + 1): + if s * t >= odd_masks and s * (s - 1) // 2 + t * (t - 1) // 2 >= even_nonzero: + return L + L += 2 + + +def lemma_a_table(n, s, t): + """Exact pair-representation rows for one parity split. + + A_x = #{e= ceil((s*t - 2^(n-1))/2). Since sum A_x B_x over S + is at most |S| + e_ex + b_ex + e_ex*b_ex, every row that misses the bound + is a contradiction. + """ + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + need = (s * t - odd_masks + 1) // 2 # ceil((st - odd)/2) + rows = [] + if s * t < odd_masks or A + B < even_nonzero: + rows.append(dict(e_ex=None, b_ex=None, shared=None, upper=None, + need=need, feasible=False, reason="counting")) + return rows + 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 + upper = shared + e_ex + b_ex + e_ex * b_ex + rows.append(dict(e_ex=e_ex, b_ex=b_ex, shared=shared, upper=upper, + need=need, feasible=upper >= need, reason="identity")) + return rows + + +def split_identity_feasible(n, s, t): + return any(r["feasible"] for r in lemma_a_table(n, s, t)) + + +def admissible_splits(n, length): + """Parity splits that survive counting and the pair-representation identity.""" + half = length // 2 + out = [] + for s in range(1, half + 1): + for t in range(1, half + 1): + if split_identity_feasible(n, s, t) and _counting_ok(n, s, t): + out.append((s, t)) + return sorted(set(out)) + + +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) + + +def set_level_splits(n, size): + """Parity splits of a size-point set that survive counting and identity.""" + out = [] + for s in range(1, size): + t = size - s + if _counting_ok(n, s, t) and split_identity_feasible(n, s, t): + out.append((s, t)) + return sorted(set(out)) + + +# --------------------------------------------------------------- set census + + +def normalized_set_census(n, k): + """All k-point subsets of F2^n containing 0 (translation-normalized). + + Reports the number of sets, the maximum |P+P| and the number of full + covers. Exact integer computation; recursive growth with a running + pair-sum mask. + """ + total = (1 << n) - 1 # nonzero points to choose from + max_cov = 0 + covers = 0 + sets = 0 + full = (1 << (1 << n)) - 1 + + chosen = [] + + def rec(start, support): + nonlocal max_cov, covers, sets + if len(chosen) == k - 1: + sets += 1 + cov = support | 1 # zero mask always covered + c = cov.bit_count() + if c > max_cov: + max_cov = c + if cov == full: + covers += 1 + return + need = (k - 1) - len(chosen) + for v in range(start, total + 2 - need): + add = 1 << v # 0 + v + for u in chosen: + add |= 1 << (u ^ v) + chosen.append(v) + rec(v + 1, support | add) + chosen.pop() + + rec(1, 0) + return dict(sets=sets, max_coverage=max_cov, covers=covers) + + +# ------------------------------------------------------------------ cycle + + +def hamiltonian_cycle(points, n): + """A closed walk word through every point of P exactly once, or None. + + The word's step labels are the hypercube coordinates, so the result is a + restored source word iff every label is used an even number of times (a + closed walk forces even use automatically). + """ + P = sorted(set(points)) + if len(P) != len(points) or 0 not in P: + return None + index = {v: i for i, v in enumerate(P)} + size = len(P) + neigh = [] + for v in P: + ns = [] + for bit in range(n): + w = v ^ (1 << bit) + if w in index: + ns.append((index[w], bit)) + neigh.append(ns) + + target = (1 << size) - 1 + path = [0] + used = 1 << 0 + steps = [] + + def dfs(cur): + nonlocal used + if used == target: + for nb, bit in neigh[cur]: + if nb == 0: + steps.append(bit) + return True + return False + for nb, bit in neigh[cur]: + if nb == 0 or (used >> nb) & 1: + continue + used |= 1 << nb + path.append(nb) + steps.append(bit) + if dfs(nb): + return True + steps.pop() + path.pop() + used ^= 1 << nb + return False + + if dfs(0): + return steps + return None + + +def closed_walk_word(points, word): + """Vertex sequence of the walk defined by word (sanity helper).""" + return prefixes(word) + + +# --------------------------------------------------------------- joint search + + +def joint_covers(n, splits, require_min_degree=False, max_nodes=None, stats=None): + """Exhaustive (E, O) covers of F2^n with the given parity split sizes. + + E subset even-weight vectors with 0 in E, O subset odd-weight vectors, + increasing global order (each pair enumerated once); E + O must cover all + odd masks and (E+E) u (O+O) all even nonzero masks. Collision budgets and + coverage-capacity bounds prune the tree. If require_min_degree, sets whose + induced hypercube graph has a vertex of degree < 2 are skipped (every word + of minimal length walks a Hamiltonian cycle through its prefix set, so this + preserves completeness for word exclusion). + """ + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + ALL_ODD = 0 + ALL_EVEN = 0 + for v in range(1 << n): + if v & 1: + ALL_ODD |= 1 << v + elif v: + ALL_EVEN |= 1 << v + results = [] + nodes = [0] + + for (s, t) in splits: + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + budget = A + B - even_nonzero # e_ex + b_ex <= budget + if budget < 0: + continue + E = [0] + O = [] + state = dict(e_supp=0, o_supp=0, coll=0, c_odd=0, c_even=0) + + def rec(last): + nodes[0] += 1 + if max_nodes is not None and nodes[0] > max_nodes: + raise OverflowError("node cap reached") + e, o = len(E), len(O) + if e == s and o == t: + st = state + if (st["c_odd"] & ALL_ODD) == ALL_ODD and (st["c_even"] & ALL_EVEN) == ALL_EVEN: + if require_min_degree and not _min_degree_two(E + O, n): + return + results.append((tuple(E), tuple(O))) + return + st = state + unc_odd = ALL_ODD & ~st["c_odd"] + if unc_odd.bit_count() > s * t - e * o: + return + unc_even = ALL_EVEN & ~st["c_even"] + rem_e = A - e * (e - 1) // 2 + rem_o = B - o * (o - 1) // 2 + if unc_even.bit_count() > rem_e + rem_o: + return + if e < s: + for v in range(last + 1, (1 << n)): + if v & 1: + continue + add = 0 + for u in E: + add |= 1 << (v ^ u) + nc = (add & st["e_supp"]).bit_count() + if st["coll"] + nc > budget: + continue + saved = (st["e_supp"], st["coll"], st["c_odd"], st["c_even"]) + st["e_supp"] |= add + st["coll"] += nc + m = 0 + for w in O: + m |= 1 << (v ^ w) + st["c_odd"] |= m + st["c_even"] |= add + E.append(v) + rec(v) + E.pop() + st["e_supp"], st["coll"], st["c_odd"], st["c_even"] = saved + if o < t: + for v in range(last + 1, (1 << n)): + if not (v & 1): + continue + add = 0 + for u in O: + add |= 1 << (v ^ u) + nc = (add & st["o_supp"]).bit_count() + if st["coll"] + nc > budget: + continue + saved = (st["o_supp"], st["coll"], st["c_odd"], st["c_even"]) + st["o_supp"] |= add + st["coll"] += nc + m = 0 + for w in E: + m |= 1 << (v ^ w) + st["c_odd"] |= m + st["c_even"] |= add + O.append(v) + rec(v) + O.pop() + st["o_supp"], st["coll"], st["c_odd"], st["c_even"] = saved + + rec(0) + if stats is not None: + stats["nodes"] = nodes[0] + return results + + +def _min_degree_two(P, n): + S = set(P) + for v in P: + deg = 0 + for bit in range(n): + if (v ^ (1 << bit)) in S: + deg += 1 + if deg < 2: + return False + return True + + +# ------------------------------------------------------- cyclic word census + + +def rg_prefixes(n, depth): + """Every restricted-growth prefix of given length over n labels. + + Shards of cyclic_census: every canonical word has exactly one of these as + its length-`depth` prefix, so the subtrees partition the search space. + """ + out = [] + + def rec(i, used, acc): + if i == depth: + out.append(tuple(acc)) + return + for j in range(min(used + 1, n)): + acc.append(j) + rec(i + 1, used + 1 if j == used else used, acc) + acc.pop() + + rec(0, 0, []) + return out + + +def cyclic_census(n, length, budget=None, simple=False, stop_on_first=False, + prefix=(), stats=None, max_nodes=None, collect_all=False): + """Exhaustive canonical word census of length `length` at n sources. + + Restricted-growth words (complete under coordinate relabeling, which is a + hypercube automorphism), labels in first-occurrence order, every label + used with an even count >= 2. Prunes: multiplicity room, self-avoidance + when `simple` (the caller must justify |P| = length), and the + pair-representation collision budget `budget` (e_ex + b_ex <= budget; the + caller must justify it from the split identity). `prefix` restricts the + search to one shard subtree. Returns dict(nodes, leaves, hits, words) + where words lists universal witnesses (up to stop_on_first). + """ + cap = max_nodes + out = dict(nodes=0, leaves=0, hits=0, words=[]) + word = [0] * length + count = [0] * n + st = dict(q=0, seen=1, e_supp=0, o_supp=0, coll=0, used=0, odd=0) + E = [0] + O = [] + + def rec(i): + out["nodes"] += 1 + if cap is not None and out["nodes"] > cap: + raise OverflowError("node cap reached") + if i == length: + if st["q"] != 0: + return + out["leaves"] += 1 + if collect_all: + out.setdefault("all_words", []).append(tuple(word)) + pts = E + O + cov = 0 + for a_i in range(len(pts)): + a = pts[a_i] + for b in pts[a_i:]: + cov |= 1 << (a ^ b) + if cov.bit_count() == 1 << n: + out["hits"] += 1 + out["words"].append(tuple(word)) + return + if st["odd"] + 2 * (n - st["used"]) > length - i: + return + room = length - 2 * (n - 1) + limit = min(st["used"] + 1, n) + for j in range(limit): + if count[j] >= room: + continue + if i < len(prefix) and j != prefix[i]: + continue + nq = st["q"] ^ (1 << j) + closing = (i == length - 1 and nq == 0) + if simple and not closing and (st["seen"] >> nq) & 1: + continue + if closing: + newcoll = 0 + add = 0 + elif nq & 1: + add = 0 + for u in O: + add |= 1 << (nq ^ u) + newcoll = (add & st["o_supp"]).bit_count() + if budget is not None and st["coll"] + newcoll > budget: + continue + else: + add = 0 + for u in E: + add |= 1 << (nq ^ u) + newcoll = (add & st["e_supp"]).bit_count() + if budget is not None and st["coll"] + newcoll > budget: + continue + saved = (st["q"], st["seen"], st["e_supp"], st["o_supp"], + st["coll"], st["used"], st["odd"]) + word[i] = j + count[j] += 1 + st["odd"] += 1 if (count[j] & 1) else -1 + st["q"] = nq + if not closing: + st["seen"] |= 1 << nq + if nq & 1: + st["o_supp"] |= add + O.append(nq) + else: + st["e_supp"] |= add + E.append(nq) + st["coll"] += newcoll + if j == st["used"]: + st["used"] += 1 + rec(i + 1) + if stop_on_first and out["hits"]: + return + (st["q"], st["seen"], st["e_supp"], st["o_supp"], + st["coll"], st["used"], st["odd"]) = saved + count[j] -= 1 + if not closing: + (O if (nq & 1) else E).pop() + + rec(0) + if stats is not None: + stats.update(out) + return out diff --git a/research/universal-f7-singleton-l20-seed06704c39/independent.py b/research/universal-f7-singleton-l20-seed06704c39/independent.py new file mode 100644 index 0000000000..f47f5b2615 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/independent.py @@ -0,0 +1,104 @@ +#!/usr/bin/env python3 +"""Different-method cross-checks for the KB3b f(7) package. + +Three independent formulations, no shared code with engine.py's coverage: + * dual predicate: m is covered iff (P xor m) meets P; + * interval XOR: D(w) = {XOR of a contiguous subword} union {0}; + * direct pair loop over positions, not prefix sets. +Also re-derives the parity fact and the walk-unrealizability of the stored +covers with an independently written degree loop. + +Pass marker: PASS_F7_L20_INDEPENDENT {...} +""" +import json +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from engine import prefixes, word_is_restored + +HERE = Path(__file__).resolve().parent + + +def dual_covers(P): + S = set(P) + return all(any((p ^ m) in S for p in S) for m in range(128)) + + +def interval_xor_masks(word): + got = {0} + for i in range(len(word)): + acc = 0 + for j in range(i, len(word)): + acc ^= 1 << word[j] + got.add(acc) + return got + + +def pair_positions(word): + qs = prefixes(word) + got = set() + for s in range(len(qs)): + for t in range(s + 1, len(qs)): + got.add(qs[s] ^ qs[t]) + return got + + +def degrees_ind(P, n=7): + S = set(P) + out = [] + for v in P: + d = 0 + for w in S: + if w != v and bin(v ^ w).count("1") == 1: + d += 1 + out.append(d) + return sorted(out) + + +def main(): + expected = json.loads((HERE / "EXPECTED.json").read_text(encoding="utf-8")) + report = {} + + # parity: every restored word has even length + for L in (19, 21): + word = [0] * L + assert not word_is_restored(word, 7), "odd-length word must not restore" + report["parity_odd_lengths_dead"] = "ok" + + # stored words: three formulations must agree + words = { + "word_L24_control": expected["search"]["word_L24_control"]["word"], + "word_L22": expected["search"]["word_L22"]["word"], + "word_L20": expected["search"]["word_L20"]["word"], + } + for name, w in words.items(): + pts = prefixes(w) + assert dual_covers(pts) == (name == "word_L24_control"), name + assert interval_xor_masks(w) == pair_positions(w), name + cov = len(pair_positions(w)) + assert cov == expected["search"][name]["coverage"], (name, cov) + report[name] = f"coverage={cov} dual_and_interval_agree" + + # stored covers: independent degree loop and dual predicate + for name in ("cover20", "cover22"): + raw = expected[name]["points"] + P = sorted(v ^ raw[0] for v in raw) # translation-invariant check + assert dual_covers(P), name + degs = degrees_ind(P) + assert degs == expected[name]["degrees"], (name, degs) + assert min(degs) < 2, name + report[name] = f"size={len(P)} min_degree={min(degs)} no_closed_walk" + + # the deterministic words are really restored and really not universal + assert word_is_restored(words["word_L22"], 7) + assert len(pair_positions(words["word_L22"])) == 126 + report["witnesses_replayed"] = 0 + + print("PASS_F7_L20_INDEPENDENT " + json.dumps(report, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/universal-f7-singleton-l20-seed06704c39/search.py b/research/universal-f7-singleton-l20-seed06704c39/search.py new file mode 100644 index 0000000000..6cf4653569 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/search.py @@ -0,0 +1,274 @@ +#!/usr/bin/env python3 +"""Deterministic search campaign for the KB3b f(7) continuation (PR943 model). + +Two complementary landscapes, both exact-integer and standard library only: + +* WORD side: restored words (closed hypercube walks). Universality is the + interval-XOR condition D(w) = {q_s xor q_t} = F2^n. Steepest-ascent + iterated local search (transpositions + segment reversals + kicks). +* SET side: k-point sets P with 0 in P, objective |P + P|. Steepest-ascent + over point swaps. Covers found here are then tested for walk + realizability (a closed walk through P needs min induced degree >= 2, and + at length |P| exactly a Hamiltonian cycle). + +The campaign is deterministic given the seeds below (CPython `random` +Mersenne Twister). `main` prints one marker per stage and writes +SEARCH.json. This is a heuristic search: a ceiling attained here is a +search failure, not an exclusion. +""" +import json +import random +import sys +import time +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from engine import hamiltonian_cycle, word_is_universal + +N = 7 + + +# ------------------------------------------------------------- word utilities + +def word_pts(word): + q = 0 + pts = [0] + for j in word: + q ^= 1 << j + pts.append(q) + return pts + + +def cov_pts(pts): + m = 0 + for i in range(len(pts)): + a = pts[i] + for k in range(i, len(pts)): + m |= 1 << (a ^ pts[k]) + return m + + +def word_cov(word): + return cov_pts(word_pts(word)) + + +def missing_masks(pts): + m = cov_pts(pts) + return [x for x in range(128) if not (m >> x) & 1] + + +def patterns(n, L): + """All even-count patterns (each label used, count >= 2, sum L).""" + out = [] + + def rec(rem, cap, acc): + if rem == 0: + out.append(list(acc)) + return + for x in range(2, min(rem, cap) + 1, 2): + rec(rem - x, x, acc + [x]) + + rec(L - 2 * n, L - 2 * n, []) + return [sorted([2 + e for e in p] + [2] * (n - len(p)), reverse=True) for p in out] + + +# ------------------------------------------------------------------ word ILS + +def climb_word(word, L, evals): + """Steepest ascent over transpositions and segment reversals.""" + cur = word_cov(word).bit_count() + while True: + best = cur + move = None + for i in range(L): + for k in range(i + 1, L): + word[i], word[k] = word[k], word[i] + v = word_cov(word).bit_count() + word[i], word[k] = word[k], word[i] + evals[0] += 1 + if v > best: + best, move = v, ("swap", i, k) + for i in range(L): + for k in range(i + 2, L): + word[i:k + 1] = reversed(word[i:k + 1]) + v = word_cov(word).bit_count() + word[i:k + 1] = reversed(word[i:k + 1]) + evals[0] += 1 + if v > best: + best, move = v, ("rev", i, k) + if move is None: + return cur + if move[0] == "swap": + _, i, k = move + word[i], word[k] = word[k], word[i] + else: + _, i, k = move + word[i:k + 1] = reversed(word[i:k + 1]) + cur = best + if cur == 128: + return cur + + +def word_search(L, seed, restarts, kick): + """Deterministic ILS over restored words of length L at n = 7.""" + R = random.Random(seed) + pats = patterns(N, L) + best = (0, None) + evals = [0] + for r in range(restarts): + counts = [2] * N + for i, e in enumerate(R.choice(pats)): + counts[i] = e + word = [] + for j, c in enumerate(counts): + word += [j] * c + R.shuffle(word) + c = climb_word(word, L, evals) + it = 0 + while c < 128 and it < 40: + it += 1 + for _ in range(kick): + i, k = R.randrange(L), R.randrange(L) + word[i], word[k] = word[k], word[i] + c2 = climb_word(word, L, evals) + if c2 >= c: + c = c2 + if c > best[0]: + best = (c, word[:]) + if c == 128: + break + return dict(best=best[0], word=best[1], evals=evals[0]) + + +# ------------------------------------------------------------------- set ILS + +def climb_set(P, k, evals): + cur = cov_pts(sorted(P)).bit_count() + pool = [v for v in range(128) if v not in set(P)] + while True: + best = cur + move = None + for a in range(k): + for v in pool: + old = P[a] + P[a] = v + val = cov_pts(sorted(P)).bit_count() + P[a] = old + evals[0] += 1 + if val > best: + best, move = val, (a, v) + if move is None: + return cur + a, v = move + pool.remove(v) + pool.append(P[a]) + P[a] = v + cur = best + if cur == 128: + return cur + + +def set_search(k, seed, restarts): + """Deterministic ILS over k-point sets; returns best set and cover count.""" + R = random.Random(seed) + best = (0, None) + covers = 0 + first_cover = None + evals = [0] + for r in range(restarts): + P = [0] + R.sample(range(1, 128), k - 1) + c = climb_set(P, k, [0]) + evals[0] += 1 + if c == 128: + covers += 1 + if first_cover is None: + first_cover = sorted(P) + if c > best[0]: + best = (c, sorted(P)) + if c == 128 and first_cover is not None: + # keep searching to measure the cover rate, not just one hit + pass + return dict(best=best[0], covers=covers, first_cover=first_cover) + + +def induced_degrees(P, n=7): + S = set(P) + return sorted(sum(1 for b in range(n) if (v ^ (1 << b)) in S) for v in P) + + +# --------------------------------------------------------------- the campaign + +CAMPAIGN = { + "word_L24_control": dict(L=24, seed=5, restarts=30, kick=6), + "word_L22": dict(L=22, seed=21, restarts=40, kick=8), + "word_L20": dict(L=20, seed=22, restarts=40, kick=8), + "set_k20": dict(k=20, seed=11, restarts=30), + "set_k22": dict(k=22, seed=12, restarts=30), +} + +EXTENDED = { + "word_L24_control": dict(L=24, seed=5, restarts=30, kick=6), + "word_L22": dict(L=22, seed=21, restarts=600, kick=8), + "word_L20": dict(L=20, seed=22, restarts=600, kick=8), + "set_k20": dict(k=20, seed=11, restarts=300), + "set_k22": dict(k=22, seed=12, restarts=300), +} + + +def run_campaign(table=None): + table = table or CAMPAIGN + out = {} + t0 = time.time() + + p = table["word_L24_control"] + r = word_search(p["L"], p["seed"], p["restarts"], p["kick"]) + assert r["best"] == 128 and word_is_universal(r["word"], 7), "L=24 control failed" + out["word_L24_control"] = {"coverage": 128, "word": r["word"]} + print(f"SEARCH word L=24 control coverage=128 word={r['word']}") + + for name in ("word_L22", "word_L20"): + p = table[name] + r = word_search(p["L"], p["seed"], p["restarts"], p["kick"]) + pts = word_pts(r["word"]) + out[name] = { + "coverage": r["best"], + "word": r["word"], + "missing": missing_masks(pts), + "evals": r["evals"], + } + print(f"SEARCH word L={p['L']} coverage={r['best']}/128 " + f"missing={out[name]['missing']} evals={r['evals']}") + + for name in ("set_k20", "set_k22"): + p = table[name] + r = set_search(p["k"], p["seed"], p["restarts"]) + entry = {"best": r["best"], "covers": r["covers"]} + if r["first_cover"]: + entry["first_cover"] = r["first_cover"] + entry["first_cover_degrees"] = induced_degrees(r["first_cover"]) + entry["first_cover_hamiltonian_cycle"] = ( + hamiltonian_cycle(r["first_cover"], 7) is not None) + out[name] = entry + print(f"SEARCH set k={p['k']} best={r['best']} covers={r['covers']} " + f"degrees={entry.get('first_cover_degrees')}") + + out["seconds"] = round(time.time() - t0, 1) + return out + + +def main(): + extended = "--extended" in sys.argv[1:] + out = run_campaign(EXTENDED if extended else None) + name = "SEARCH-EXTENDED.json" if extended else "SEARCH.json" + (Path(__file__).resolve().parent / name).write_text( + json.dumps(out, indent=2, sort_keys=True), encoding="utf-8") + print("PASS_F7_L20_SEARCH " + f"L20={out['word_L20']['coverage']} L22={out['word_L22']['coverage']} " + f"L24={out['word_L24_control']['coverage']} " + f"setk20_covers={out['set_k20']['covers']}") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/universal-f7-singleton-l20-seed06704c39/test_engine.py b/research/universal-f7-singleton-l20-seed06704c39/test_engine.py new file mode 100644 index 0000000000..f878c154f6 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/test_engine.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Unit tests for the KB3b f(7) package (fast; no long censuses).""" +import hashlib +import json +import sys +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +from engine import ( + census_words, + cyclic_census, + gray_word, + hamiltonian_cycle, + lemma_a_table, + prefixes, + rg_prefixes, + word_is_restored, + word_is_universal, +) +from search import ( + climb_set, + cov_pts, + induced_degrees, + missing_masks, + patterns, + word_pts, +) + +ENGINE_SHA256 = "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" + + +class TestVendoredEngine(unittest.TestCase): + def test_engine_byte_pin(self): + data = (HERE / "engine.py").read_bytes() + self.assertEqual(hashlib.sha256(data).hexdigest(), ENGINE_SHA256) + + def test_pinned_n5_l10(self): + hist, digest, words = census_words(5, 10) + self.assertEqual(words, 945) + self.assertEqual(max(hist), 31) + self.assertEqual(digest, + "3dcc5689a4a34baec6424389a07dd917c0b681d6a894cba3e909f5a81efdc86e") + + def test_leaf_counts_match_canonical_words(self): + r = cyclic_census(5, 10) + self.assertEqual(r["leaves"], 945) + + +class TestParityLemma(unittest.TestCase): + def test_odd_lengths_have_no_restored_pattern(self): + for L in (19, 21, 23): + self.assertEqual(patterns(7, L), []) + + def test_even_patterns(self): + self.assertEqual(len(patterns(7, 20)), 3) + self.assertEqual(len(patterns(7, 22)), 5) + self.assertEqual(sorted(patterns(7, 14)[0]), [2] * 7) + + def test_restored_requires_even_length(self): + w = [0] * 19 + self.assertFalse(word_is_restored(w, 7)) + + +class TestCoverageForms(unittest.TestCase): + def test_prefix_xor_equals_pair_positions(self): + w = list(gray_word(7)) + pts = prefixes(w) + m = cov_pts(pts) + self.assertEqual(m.bit_count(), 128) + self.assertEqual(missing_masks(pts), []) + + def test_gray_universal(self): + for n in (4, 5, 6, 7): + self.assertTrue(word_is_universal(gray_word(n), n)) + + def test_cov_pts_matches_engine_on_words(self): + w = [0, 1, 0, 2, 0, 1, 0, 2, 3, 4, 3, 5, 3, 4, 3, 5] + self.assertEqual(cov_pts(word_pts(w)).bit_count(), + __import__("engine").word_coverage(w)) + + +class TestTransversalLemma(unittest.TestCase): + """G[R] for R = {t + g(t)} has edges only within level sets of g.""" + + def test_level_set_components(self): + import itertools + for bits in range(0, 1 << 8, 7): # deterministic sample of g + g = [((bits >> (2 * t)) & 3) for t in range(16)] + R = [] + for t in range(16): + q1, q2 = g[t] & 1, (g[t] >> 1) & 1 + v = t << 2 | q1 | (q2 << 1) + R.append(v) + S = set(R) + # components: BFS in the induced graph + seen = set() + comps = 0 + for v in R: + if v in seen: + continue + comps += 1 + stack = [v] + seen.add(v) + while stack: + x = stack.pop() + for b in range(6): + y = x ^ (1 << b) + if y in S and y not in seen: + seen.add(y) + stack.append(y) + levels = len(set(g)) + self.assertGreaterEqual(comps, levels) + if comps == 1: + self.assertEqual(levels, 1) + # g constant: R+R is a 16-point plane, far from a cover + sums = {a ^ b for a in R for b in R} + self.assertEqual(len(sums), 16) + + +class TestCoverArtifacts(unittest.TestCase): + def test_cover20(self): + expected = json.loads((HERE / "EXPECTED.json").read_text(encoding="utf-8")) + raw = expected["cover20"]["points"] + P = sorted(v ^ raw[0] for v in raw) # normalize 0 into P (translation) + self.assertEqual(cov_pts(P).bit_count(), 128) + self.assertEqual(induced_degrees(P), expected["cover20"]["degrees"]) + self.assertIsNone(hamiltonian_cycle(P, 7)) + self.assertLess(min(induced_degrees(P)), 2) + + def test_set_ils_finds_covers_deterministically(self): + r = climb_set([0, 2, 4, 6, 39, 49, 50, 55, 76, 77, + 92, 93, 98, 101, 106, 111, 113, 118, 120, 125], 20, [0]) + self.assertEqual(r, 128) + + +class TestSharding(unittest.TestCase): + def test_shards_partition(self): + shards = rg_prefixes(7, 4) + self.assertEqual(len(shards), 15) # Bell(4) restricted-growth strings + self.assertEqual(len(set(shards)), 15) + + def test_lemma_rows_survive_at_L20(self): + self.assertTrue(any(r["feasible"] for r in lemma_a_table(7, 10, 10))) + self.assertTrue(any(r["feasible"] for r in lemma_a_table(7, 10, 7))) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/universal-f7-singleton-l20-seed06704c39/verify.py b/research/universal-f7-singleton-l20-seed06704c39/verify.py new file mode 100644 index 0000000000..66a8d9f6a3 --- /dev/null +++ b/research/universal-f7-singleton-l20-seed06704c39/verify.py @@ -0,0 +1,147 @@ +#!/usr/bin/env python3 +"""Verification for the KB3b f(7) continuation package. + +Rebuilds every reproduced number from scratch and compares the stored +certificate with EXPECTED.json field by field: + + 1. byte-exact reproduction of the pinned five/six-source censuses + (research/universal-connector-six-source/EXPECTED.json), the counting + bounds 10/14/18 and the Gray constructions 12/16/24; + 2. full reproduction of PR 2542's decisive length-18 census + (15,775,992 nodes, 312,064 simple 18-cycles, zero universal words); + 3. the exact obstructions: parity (no odd-length restored word), the + transversal-detour template lemma (level-set components), and the + stored covering sets' walk-unrealizability (min induced degree < 2); + 4. deterministic re-run of the search campaign against EXPECTED.json; + 5. replay of the resumable simple-20-cycle census checkpoint. + +Pass marker: PASS_F7_L20_VERIFY +""" +import json +import sys +import time +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from engine import ( + census_words, + counting_least_even_L, + cyclic_census, + gray_word, + hamiltonian_cycle, + rg_prefixes, + word_is_universal, +) +from search import CAMPAIGN, induced_degrees, missing_masks, patterns, run_campaign, word_pts + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PINNED = json.loads( + (ROOT / "research" / "universal-connector-six-source" / "EXPECTED.json").read_text( + encoding="utf-8" + ) +) + + +def main(): + t0 = time.time() + cert = json.loads((HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) + expected = json.loads((HERE / "EXPECTED.json").read_text(encoding="utf-8")) + + # ---- 1. byte-exact pinned reproduction -------------------------------- + for n, length in ((5, 10), (6, 12), (6, 14)): + hist, digest, words = census_words(n, length) + pinned = {(c["sources"], c["length"]): c for c in PINNED["censuses"]}[(n, length)] + assert words == pinned["words"], (n, length, words) + assert max(hist) == pinned["max_coverage"] + assert {str(k): v for k, v in sorted(hist.items())} == pinned["histogram"] + assert digest == pinned["records_sha256"] + print(f"REPRO n={n} L={length} words={words} max={max(hist)} sha={digest[:16]}") + for n in (5, 6, 7): + lb = counting_least_even_L(n) + assert lb == PINNED["constructions"][str(n)]["lower_bound"], (n, lb) + w = gray_word(n) + assert word_is_universal(w, n) and len(w) == PINNED["constructions"][str(n)]["length"] + print(f"REPRO n={n} least_even_L={lb} gray={len(w)}") + + # ---- 2. PR 2542 decisive census, fully re-run ------------------------- + # The recorded node count is the SHARDED sum (five depth-3 shards; upper + # tree nodes are counted once per shard below them, which adds exactly 10 + # to the unsharded count). Reproduce it shard by shard, then cross-check + # leaf counts against one unsharded run, as PR 2542's own verifier did. + tot = {"nodes": 0, "leaves": 0, "hits": 0} + for pref in rg_prefixes(7, 3): + rr = cyclic_census(7, 18, budget=9, simple=True, prefix=pref) + tot["nodes"] += rr["nodes"] + tot["leaves"] += rr["leaves"] + tot["hits"] += rr["hits"] + p = expected["pr2542_l18"] + assert tot["nodes"] == p["census_nodes"], tot["nodes"] + assert tot["leaves"] == p["simple_18_cycles"], tot["leaves"] + assert tot["hits"] == p["universal_words"] + r = cyclic_census(7, 18, budget=9, simple=True) + assert r["leaves"] == p["simple_18_cycles"] and r["hits"] == 0, "unsharded drift" + print(f"REPRO PR2542 L18 nodes(sharded)={tot['nodes']} nodes(unsharded)={r['nodes']} " + f"cycles={tot['leaves']} universal_words={tot['hits']}") + + # ---- 3. exact obstructions ------------------------------------------- + for odd in (19, 21): + assert patterns(7, odd) == [], f"odd length {odd} must have no pattern" + assert len(patterns(7, 20)) == 3 and len(patterns(7, 22)) == 5 + print("LEMMA parity: no restored word has odd length (patterns empty)") + + for name in ("cover20", "cover22"): + raw = expected[name]["points"] + base = raw[0] # covers are translation-invariant; normalize 0 into P + P = sorted(v ^ base for v in raw) + assert len(set(P)) == len(P) and 0 in P + pts = list(P) + m = 0 + for i, a in enumerate(pts): + for b in pts[i:]: + m |= 1 << (a ^ b) + assert m.bit_count() == 128, f"{name} is not a cover" + degs = induced_degrees(P) + assert degs == expected[name]["degrees"], (name, degs) + assert min(degs) < 2, f"{name} unexpectedly walk-shaped" + assert hamiltonian_cycle(P, 7) is None, f"{name} unexpectedly Hamiltonian" + print(f"COVER {name} size={len(P)} degrees={degs} walk_realisable=False") + + # ---- 4. deterministic campaign --------------------------------------- + run = run_campaign() + exp = expected["search"] + for name in exp: + if name == "seconds": + continue + for key, val in exp[name].items(): + assert run[name][key] == val, (name, key, run[name][key], val) + print("SEARCH campaign reproduced exactly " + f"L20={run['word_L20']['coverage']} L22={run['word_L22']['coverage']} " + f"L24={run['word_L24_control']['coverage']}") + + # ---- 5. census20 checkpoint replay ----------------------------------- + prog = json.loads((HERE / "CENSUS20-PROGRESS.json").read_text(encoding="utf-8")) + acc = prog["accum"] + assert acc["nodes"] == sum(v["nodes"] for v in prog["done"].values()) + assert acc["leaves"] == sum(v["leaves"] for v in prog["done"].values()) + for w in acc["words"]: + assert len(w) == 20 and word_is_universal(tuple(w), 7) + done = len(prog["done"]) + total = prog["shards_total"] + assert expected["census20"]["shards_total"] == total + assert expected["census20"]["nodes"] == acc["nodes"] + assert expected["census20"]["cycles"] == acc["leaves"] + assert expected["census20"]["universal_words"] == len(acc["words"]) + state = "COMPLETE" if done == total else "PARTIAL" + print(f"CENSUS20 {state} shards={done}/{total} nodes={acc['nodes']} " + f"cycles={acc['leaves']} universal_words={len(acc['words'])}") + + print(f"PASS_F7_L20_VERIFY {expected['conclusion']} " + f"L20={run['word_L20']['coverage']} L22={run['word_L22']['coverage']} " + f"seconds={round(time.time() - t0, 1)}") + return 0 + + +if __name__ == "__main__": + sys.exit(main())