diff --git a/research/universal-f7-singleton-seedb859517b/CERTIFICATE-PROGRESS.json b/research/universal-f7-singleton-seedb859517b/CERTIFICATE-PROGRESS.json new file mode 100644 index 0000000000..18f1a67d8a --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/CERTIFICATE-PROGRESS.json @@ -0,0 +1 @@ +{"done": {"000": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "001": {"nodes": 2, "leaves": 0, "hits": 0, "words": []}, "010": {"nodes": 1973843, "leaves": 33211, "hits": 0, "words": []}, "011": {"nodes": 3, "leaves": 0, "hits": 0, "words": []}, "012": {"nodes": 13802142, "leaves": 278853, "hits": 0, "words": []}}, "accum": {"nodes": 15775992, "leaves": 312064, "hits": 0, "words": []}} \ No newline at end of file diff --git a/research/universal-f7-singleton-seedb859517b/CERTIFICATE.json b/research/universal-f7-singleton-seedb859517b/CERTIFICATE.json new file mode 100644 index 0000000000..f3eb3e8561 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/CERTIFICATE.json @@ -0,0 +1,113 @@ +{ + "conclusion": "f(7) >= 20 (length 18 excluded)", + "seconds": 117.0, + "tier1_reproduction": { + "n5": { + "counting_least_even_L": 10, + "gray_length": 12 + }, + "n5_L10": { + "matches_pinned": true, + "max_coverage": 31, + "records_sha256": "3dcc5689a4a34baec6424389a07dd917c0b681d6a894cba3e909f5a81efdc86e", + "words": 945 + }, + "n6": { + "counting_least_even_L": 14, + "gray_length": 16 + }, + "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 + }, + "n7": { + "counting_least_even_L": 18, + "gray_length": 24 + } + }, + "tier2_controls": { + "lemma_rows_8_8": { + "feasible": false, + "rows": 1 + }, + "lemma_rows_8_9": { + "feasible": false, + "rows": 3 + }, + "lemma_rows_9_8": { + "feasible": false, + "rows": 3 + }, + "lemma_rows_9_9": { + "feasible": true, + "rows": 55 + }, + "n5_nine_point": { + "covers": 0, + "max_coverage": 29, + "sets": 7888725 + }, + "n5_ten_point": { + "brute_covers": 99200, + "brute_sets": 20160075, + "cycle_realisable_covers": 0, + "joint_covers": 99200, + "joint_splits": [ + [ + 2, + 8 + ], + [ + 3, + 7 + ], + [ + 4, + 6 + ], + [ + 5, + 5 + ], + [ + 6, + 4 + ], + [ + 7, + 3 + ], + [ + 8, + 2 + ] + ] + } + }, + "tier3_f7": { + "admissible_splits_L18": [ + [ + 9, + 9 + ] + ], + "census_nodes": 15775992, + "covers_found": null, + "joint_nodes": null, + "shards": 5, + "simple_18_cycles": 312064, + "size17_splits": { + "8_9": false, + "9_8": false + }, + "universal_words": [] + } +} \ No newline at end of file diff --git a/research/universal-f7-singleton-seedb859517b/CLAIM.md b/research/universal-f7-singleton-seedb859517b/CLAIM.md new file mode 100644 index 0000000000..2f8669e414 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/CLAIM.md @@ -0,0 +1,75 @@ +# CLAIM — kappa-blocker KB3: the sharp singleton f(7) gap + +Agent: **Aaron Wang**, with help from opencode (substantial AI assistance; no +independent human review claimed). Base main +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`; priority revision 4; catalogue +SHA-256 `d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7`; +selected-record SHA-256 +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. Posted +claim: https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18947532 + +## Object and scope change + +In the PR943 prefix-walk model (`research/universal-connector-boundary`), a +restored source word `w` over `n` singleton labels is universal when paired +readouts realize every mask, `D(w) = {q_s xor q_t} = F2^n`; `f(n)` is the +minimum word length. The pinned record is `f(5) = 12`, `f(6) = 16`, +`18 <= f(7) <= 24` (`research/universal-connector-six-source/README.md`: "The +exact value of `f(7)` is open"). This package decides or narrows that gap in +the singleton alphabet only. + +**Scope status: changed** (authorized explicit-open-request scope change to the +assigned kappa-blocker KB3; drawn track `adversarial-audit`, chooser seed +`b859517b2b08394033ce4a4ab231ece8`). The drawn cards +(`selected-stock-envelope`, `uniform-transfer-audit`, +`supplier-boundary-audit`) are saturated or incremental at this base — the last +two were completed within hours (discussion 1166 comments 18939154/18939459 and +18939803/18940382). The distinct scopes of the 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) and the 63-mask +weight-1/2/3 sparse 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) are recorded as +concurrent scopes in `SOURCES.json`, not collisions. + +## Method + +Smallest falsifying instance first: the engine must reproduce the pinned +five-source length-10 census (945 words, max 31/32) and six-source +length-12/14 censuses (10,395 words, max 49/64; 945,945 words, max 59/64) +byte-for-byte, including records SHA-256, before any new number is trusted. + +Then the length-18 census at `n = 7`, via the prefix vertex set `P = E union O` +(`E` even-weight prefixes, `O` odd-weight prefixes; universality is exactly +`P + P = F2^7`): + +1. Position parity gives `|E|, |O| <= 9`; counting gives `|E||O| >= 64` and + `C(|E|,2) + C(|O|,2) >= 63`. +2. **Lemma A (pair-representation identity).** Every surviving 17-point split + `(9,8)` and `(8,9)` is contradictory: full odd coverage with 72 pairs forces + `sum_x A_x B_x >= 4`, while full even coverage forces at most one shared + nonzero pair-sum value, bounding the same sum by 1. Machine-checked rows are + in `CERTIFICATE.json`; an independent multiset enumeration re-derives them. + (The same lemma explains the community census fact that no nine-point set of + `F2^5` covers, max 29.) +3. So a universal 18-word would walk a simple 18-cycle through an 18-point + cover with the `(9,9)` split. The joint `(E,O)` search enumerates every such + cover (increasing-order generation, exact 64-bit bitmasks, collision-budget + and coverage-capacity pruning — each prune a proved necessary condition), + and every cover found is tested for a Hamiltonian 18-cycle in the induced + hypercube. + +Controls and non-vacuity: the same joint search is validated at `n = 5` against +a brute-force census of all C(31,9) ten-point sets (exact agreement on the +number of covers) and reproduces the community nine-point result; `f(5) = 12` +is re-confirmed by showing no ten-point cover is cycle-realisable. + +## Deliverable + +Either an exact length-18 exclusion (`f(7) >= 20`) or a universal word of +length below 24 (`f(7) <= 22` or `20`), with exact coverage verification either +way. No kappa, supplier or selected-frontier claim. One bounded pivot maximum +(a length-20/22 construction screen on the same set engine) if the length-18 +census completes negative inside the priced budget. diff --git a/research/universal-f7-singleton-seedb859517b/EXPECTED.json b/research/universal-f7-singleton-seedb859517b/EXPECTED.json new file mode 100644 index 0000000000..1f2ae98fe8 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/EXPECTED.json @@ -0,0 +1,6 @@ +{ + "conclusion": "f(7) >= 20 (length 18 excluded)", + "census_nodes": 15775992, + "simple_18_cycles": 312064, + "universal_words": 0 +} diff --git a/research/universal-f7-singleton-seedb859517b/INDEPENDENT.json b/research/universal-f7-singleton-seedb859517b/INDEPENDENT.json new file mode 100644 index 0000000000..d8a6148a09 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/INDEPENDENT.json @@ -0,0 +1,12 @@ +{ + "control_sets": "ok", + "lemma_rows": { + "n5_5_4": "best_sum_AB=1 need=2", + "n5_5_5": "best_sum_AB=9 need=5", + "n7_8_8": "counting", + "n7_8_9": "best_sum_AB=1 need=4", + "n7_9_8": "best_sum_AB=1 need=4", + "n7_9_9": "best_sum_AB=25 need=9" + }, + "witnesses_replayed": 0 +} \ No newline at end of file diff --git a/research/universal-f7-singleton-seedb859517b/NOTICE.md b/research/universal-f7-singleton-seedb859517b/NOTICE.md new file mode 100644 index 0000000000..2f26dcdc16 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/NOTICE.md @@ -0,0 +1,30 @@ +# Attribution and license + +Contribution by **Aaron Wang**, with help from opencode (substantial AI +assistance in scoping, implementation, verification and writing; no independent +human review claimed). New work is Apache-2.0, under the repository LICENSE. + +The model and the prefix-difference reduction are **Ross Richardson's PR943** +(`research/universal-connector-boundary`). The pinned five- and six-source +censuses, the values `f(5) = 12`, `f(6) = 16` and the recorded `f(7)` gap +`18 <= f(7) <= 24` are **Douglas Colkitt's** +(`research/universal-connector-six-source`, https://github.com/CrocSwap/integer-mult-bounds/pull/1185), +which extends PR943. Both are read and reproduced here, never imported: no +predecessor executable is vendored or called. Exact pins are in `SOURCES.json`. + +The community five-bit nine-point census fact (all 7,888,725 normalized +nine-point sets of `F2^5`, maximum pair coverage 29, no cover) was published in +the DUO-line coordination thread +(https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18931315); +this package re-derives it independently as a control and credits that source. + +The DUO pair-source alphabet work +(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) and the 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) are distinct scopes, +recorded in `SOURCES.json`. Nothing here changes the selected frontier, any +supplier or kappa. diff --git a/research/universal-f7-singleton-seedb859517b/README.md b/research/universal-f7-singleton-seedb859517b/README.md new file mode 100644 index 0000000000..90e8452c0d --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/README.md @@ -0,0 +1,168 @@ +# Seven-source singleton universal path: `f(7) >= 20` + +**Recursive-interface finite result: the sharp singleton `f(7)` gap narrows +from `18 <= f(7) <= 24` to `20 <= f(7) <= 24`. No new kappa.** + +In the PR943 prefix-walk model +([Ross Richardson's `research/universal-connector-boundary`](https://github.com/CrocSwap/integer-mult-bounds/pull/943)), +a restored source word `w` over `n` singleton labels is *universal* when paired +output readouts realize every binary row mask, `D(w) = {q_s xor q_t} = F2^n`, +and `f(n)` is the minimum length of a universal word. The pinned record from +[Douglas Colkitt's six-source package](https://github.com/CrocSwap/integer-mult-bounds/pull/1185) +is `f(5) = 12`, `f(6) = 16` and `18 <= f(7) <= 24`, with `f(7)` explicitly open +("neither 18, 20 nor 22 is excluded, and 24 is attained"). This package removes +18 from the gap in the singleton alphabet: + +> **No universal seven-source word of length 18 exists. Hence `f(7) >= 20`.** + +The DUO pair-source alphabet +([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 63-mask weight-1/2/3 sparse 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 different alphabets or different mask families; nothing here touches them. + +## Reproduce + +From the repository root, standard library only, Python 3.12: + +```sh +python3 -I -B research/universal-f7-singleton-seedb859517b/verify.py +python3 -I -B research/universal-f7-singleton-seedb859517b/independent.py +python3 -I -B research/universal-f7-singleton-seedb859517b/test_engine.py +``` + +Expected markers: + +```text +PASS_F7_SINGLETON_GAP_VERIFY f(7) >= 20 (length 18 excluded) cycles=312064 universal_words=0 nodes=15775992 +PASS_F7_INDEPENDENT {...} +Ran 22 tests ... OK +``` + +The decisive census itself is `search.py` (about 15 minutes including the +reproduction tiers; resumable from `CERTIFICATE-PROGRESS.json`, one checkpoint +per shard): + +```sh +python3 -I -B -u research/universal-f7-singleton-seedb859517b/search.py +# PASS_F7_SINGLETON_GAP f(7)>=20 L18-excluded +``` + +## Smallest falsifying instance first: reproduction + +Before any new number, the engine 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, including records SHA-256: + +| 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 | + +It also reproduces the counting lower bounds `10, 14, 18` for `n = 5, 6, 7` +and the Gray constructions of lengths `12, 16, 24`. The pinned record is +`f(5) = 12` (the assignment placeholder "f(5)=16" was corrected by reading the +pinned package, as instructed). + +## Why length 18 collapses to a census of simple 18-cycles + +Let `P` be the set of prefix parity states of a length-`L` word (`0 in P`), +`E` the even-weight elements and `O` the odd-weight ones. Universality is +exactly `P + P = F2^n`, and weight parity splits the pair sums: odd masks come +only from `E + O`, even masks only from `E + E` and `O + O`. + +1. **Position parity.** At `L = 18` the walk has 9 even and 9 odd boundary + positions (the closing state repeats the start), so `|E|, |O| <= 9`. +2. **Counting.** Full coverage needs `|E||O| >= 64` and + `C(|E|,2) + C(|O|,2) >= 63`. This already excludes `L <= 16` and every + split with `|P| <= 16` at `L = 18`. +3. **Lemma A (pair-representation identity).** Write `A_x` for the number of + unordered pairs of `E` summing to `x`, `B_x` likewise on `O`, and + `e_ex = C(|E|,2) - |supp(A)|`, `b_ex` similarly. Full odd coverage with + `|E||O|` pairs forces `sum_x A_x B_x >= ceil((|E||O| - 64)/2)`, while full + even coverage forces `|supp(A) int supp(B)| = C(|E|,2) + C(|O|,2) - e_ex - + b_ex - 63` and hence `sum_x A_x B_x <= |S| + e_ex + b_ex + e_ex*b_ex`. For + the 17-point splits `(9,8)` and `(8,9)` these bounds are `>= 4` against + `<= 1`: contradictory. **No 17-point set covers `F2^7`.** (The same lemma, + applied at `n = 5`, explains the community census fact that no nine-point + set of `F2^5` covers, maximum 29, without enumeration.) +4. So `|P| = 18`, the split is `(9,9)`, and the 18 boundary states are + distinct: **every universal 18-word would be a simple 18-cycle** through 18 + vertices of the 7-cube, with both sides Sidon-ish (`e_ex + b_ex <= 9`). + +The identity rows are machine-checked (`lemma_a_table`) and independently +re-derived by an explicit collision-multiset enumeration +(`independent.py`: `best_sum_AB=1 need=4` for `(9,8)`/`(8,9)`). + +## The decisive census + +`engine.cyclic_census(7, 18, budget=9, simple=True)` enumerates every +restricted-growth direction word of length 18 (complete under coordinate +relabeling, a hypercube automorphism) with the proved-necessary prunes above: +multiplicity room, self-avoidance, and the pair-representation collision +budget. Sharded by depth-3 prefix (the five shards partition the tree; leaf +counts agree with an unsharded run to the last leaf): + +```text +nodes=15,775,992 simple 18-cycles=312,064 universal words=0 +``` + +Zero universal words: length 18 is excluded, so `f(7) >= 20`. + +## Controls and non-vacuity + +* The cyclic census's leaf set at `n = 5`, length 10 and `n = 6`, length 12 is + **exactly** the pinned canonical word set (set equality, not just counts). +* Zero universal words at `n = 5`, length 10 and `n = 6`, length 14, + reproducing `f(5) = 12` and `f(6) = 16` from the other side. +* Planted hits: the census does find universal words at `n = 5`, length 12 and + `n = 6`, length 16 (the known values), and each found word is re-checked by + `word_is_universal`. +* The set-level engine cross-checks against brute force at `n = 5`: all + C(31,9) = 20,160,075 ten-point sets give 99,200 covers, and the independent + `(E,O)` joint search finds exactly the same 99,200; none of them is + cycle-realisable, re-confirming `f(5) = 12` at the set level. The + 7,888,725-set nine-point census reproduces the community result (maximum 29, + zero covers). +* `independent.py` re-checks coverage with the dual predicate (`m` covered iff + `(P xor m)` meets `P`), realizes cycles with subset dynamic programming + instead of DFS, and re-derives the lemma rows without the closed-form bound. + +## Scope and remaining obligations + +A finite exclusion inside PR943's abstract interface. It does not instantiate +that interface in the selected supplier and claims no kappa, supplier or +selected-frontier change. The gap is now `20 <= f(7) <= 24`: the remaining +question is whether a universal seven-source word of length 20 or 22 exists, +or whether the Gray bound 24 is sharp. 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 length-20 or length-22 seven-source singleton word + exist?** Why it matters: it would lower the singleton bound `f(7) <= 24` + and the all-127-row batch bill. First step: run + `cyclic_census(7, 20, simple=False, budget=None)`-style enumeration with + the split identity rows for `L = 20` (`(10,8)`, `(10,9)`, `(10,10)`, + `(9,9)`) computed by `lemma_a_table`, starting with the tightest split. + Blocked by: at `L = 20` the identity no longer forces a simple walk or a + unique split, so the SAW and budget prunes must be derived per split, and + the word count grows well past the length-18 tree. +2. **Do 18-point covers of `F2^7` exist at all?** This package proves none is + cycle-realisable; the set-level question is the restricted addition basis + value `r((C2)^7)` (the community records `r((C2)^6) = 14` after Gavrylkiv). + First step: shard `joint_covers(7, [(9, 9)])` by the least element and + enumerate the Sidon 9-set pairs under the shared-support identity + (`|S| = 9 - e_ex - b_ex`, `sum A_x B_x >= 9`). Blocked by: the raw joint + tree exceeds a single session (the unsharded DFS stalls in the odd-side + fill); orbit reduction under the 5,040 coordinate permutations is needed. + +See [CLAIM.md](CLAIM.md) for the task card, [TASK.json](TASK.json) for the +scope change and budget, [SOURCES.json](SOURCES.json) for pins and concurrent +scopes, [NOTICE.md](NOTICE.md) for attribution. diff --git a/research/universal-f7-singleton-seedb859517b/SOURCES.json b/research/universal-f7-singleton-seedb859517b/SOURCES.json new file mode 100644 index 0000000000..3a336f8a81 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/SOURCES.json @@ -0,0 +1,35 @@ +{ + "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" + } + ], + "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 18..24 (research/universal-connector-six-source, Douglas Colkitt, https://github.com/CrocSwap/integer-mult-bounds/pull/1185). Read and reproduced, never imported.", + "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. This package is the singleton alphabet only.", + "community_fact_rederived": "The nine-point five-bit census fact (7,888,725 sets, maximum 29, zero covers) was published at https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18931315 and is independently re-derived here as a control." + } +} diff --git a/research/universal-f7-singleton-seedb859517b/TASK.json b/research/universal-f7-singleton-seedb859517b/TASK.json new file mode 100644 index 0000000000..f75dc5b14f --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "session_seed": "b859517b2b08394033ce4a4ab231ece8", + "track": "adversarial-audit (drawn); scope changed to assigned kappa-blocker KB3", + "scope_key": "9317ab69ed725ac03545", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18947532", + "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" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp singleton-alphabet universal source path at seven sources in the PR943 prefix-walk model: decide or narrow the recorded gap 18 <= f(7) <= 24 by an exact exclusion of length 18 (f(7) >= 20) or a universal word of length below 24, with exact coverage verification either way. Delivered: length 18 excluded, so f(7) >= 20 and the gap is now 20 <= f(7) <= 24.", + "scope_change_reason": "Authorized explicit-open-request scope change to kappa-blocker KB3, recorded as instructed by the assignment. The drawn adversarial-audit cards are saturated or incremental at this base: uniform-transfer-audit (scope key 603f341b99f590f17a76) and supplier-boundary-audit (scope key 66632af6c86d34fb0fdc) were both completed within hours by fresh FINDING/DONE posts (discussion 1166 comments 18939154/18939459 and 18939803/18940382), and the drawn selected-stock-envelope family has no new selected-producer binding available to this finite-computation scope. The taken open request is the recorded open boundary of research/universal-connector-six-source/README.md: 'The exact value of f(7) is open: neither 18, 20 nor 22 is excluded, and 24 is attained.'", + "bottleneck_link": "A verified finite exclusion inside the PR943 query model removes the sharp singleton lower edge 18 from the recorded f(7) gap. It changes no supplier, tariff or kappa and instantiates no physical interface; it tightens one recorded recursive-interface boundary that downstream batch bills cite.", + "object_synonyms_used_in_overlap": [ + "universal source path", + "universal word", + "restored source word", + "singleton alphabet", + "seven-source", + "seven sources", + "Gray bound", + "f(7)", + "D(w)", + "prefix walk", + "paired readout", + "hypercube closed walk" + ], + "pair_collision_check": { + "checked_utc": "2026-10-15T10:55:00Z", + "tool": "agent_tools.py disc-comments (with nested replies) + scripts/find_overlap.py", + "threads_scanned": [ + "discussion 1166 since 2026-10-13T00:00:00Z (1342 lines, full comments incl. nested replies)", + "discussion 1317 since 2026-10-14T00:00:00Z (220 lines)" + ], + "result": "No fresh CLAIM on the singleton f(7) universal-path object. The only seven-source universal-connector activity in the last hours is the DUO pair-source alphabet (discussion 1166 comment 18943467 / discussion 1403 comments 18942952, 18943466, PR https://github.com/CrocSwap/integer-mult-bounds/pull/2396, 22 calls at 24 toggle-adds) and the sparse weight-1/2/3-mask family (PRs 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). Both are different alphabets or different mask families from the sharp singleton f(7) gap and are recorded predecessors/concurrent scopes, not collisions." + }, + "smallest_falsifying_instance_first": "Before any new n=7 number: the pinned five-source length-10 census (945 canonical words, max 31/32, records SHA-256 3dcc5689a4a34baec6424389a07dd917c0b681d6a894cba3e909f5a81efdc86e), the six-source length-12 census (10,395 words, max 49/64, records SHA-256 491b295f12cfa34a010dc23392b02d725dedcd0ba84111b31aa939a013d4958a) and length-14 census (945,945 words, max 59/64, records SHA-256 3d711ffa192093103cc034bb5ab00c680d96667c9f6d1a509981b444663bc838) reproduce byte-for-byte, and the counting lower bound table reproduces least feasible even L = 10/14/18 at n = 5/6/7. The pinned record is f(5) = 12 (not 16); the assignment's placeholder values were corrected by reading the pinned packages as instructed. The decisive engine additionally reproduces the canonical word SETS exactly and its planted-hit controls find the known universal words at n=5 length 12 and n=6 length 16.", + "priced_budget_minutes": 90, + "priced_budget_breakdown": "15 min entry overlap survey (done), 10 min refined overlap re-run before heavy computation (done), 20 min engine + tests + reproduction of pinned values (done), 35 min exact n=7 length-18 census (done in about 10 min once the engine bugs were caught by the controls), 10 min reserve. No pivot was needed: the primary census completed and excluded length 18.", + "de_diagnostic": "Not applicable. This is a finite connector-path boundary in the PR943 query model: no supplier width m, role count W, child ranks or recursive moment is priced here, so there is no a < D/E moment diagnostic to run. The applicable diagnostic is exact coverage verification against the pinned reproductions; the task claims no kappa, supplier or selected-frontier change.", + "stop_rule": "Stop at the first of: (a) an exact length-18 census (all admissible prefix-set shapes enumerated and coverage-tested) giving f(7) >= 20, (b) a verified universal word of length < 24 giving f(7) <= that length, or (c) the priced budget expiring, with the exact obstruction (which shapes were fully enumerated, which were not, and the node counts) recorded and the scope released. One bounded pivot maximum; no second pivot.", + "outcome": "completed", + "evidence": "CERTIFICATE.json records the byte-exact pinned reproductions, the machine-checked split-identity rows, the n=5 set-level controls (7,888,725 nine-point sets max 29 / zero covers; 20,160,075 ten-point sets / 99,200 covers found identically by brute force and the joint search, none cycle-realisable) and the decisive length-18 cyclic census (15,775,992 nodes, 312,064 simple 18-cycles, zero universal words). search.py builds it; verify.py replays it against EXPECTED.json; independent.py re-derives the lemma rows by collision-multiset enumeration and re-checks coverage with the dual predicate; test_engine.py holds 22 tests including exact leaf-set equality with the reference enumerator and planted-hit non-vacuity. Result: f(7) >= 20, gap narrowed from [18,24] to [20,24]. 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 length-20 or length-22 seven-source singleton word exist, or is the Gray bound 24 sharp?", + "why_it_matters": "It would lower f(7) <= 24 and the all-127-row batch bill inside the unchanged PR943 model.", + "first_step": "Compute the split-identity rows for L = 20 ((10,8), (10,9), (10,10), (9,9)) with lemma_a_table, then run a cyclic_census(7, 20) with the per-split SAW/budget prunes justified by those rows.", + "blocked_by": "At L = 20 the identity forces neither a simple walk nor one split, so prunes must be re-derived per split and the word count grows well past the length-18 tree (15,775,992 nodes)." + }, + { + "question": "Do 18-point covers of F2^7 exist at all (the restricted addition basis value r((C2)^7))?", + "why_it_matters": "This package proves no 18-point cover is cycle-realisable; set-level nonexistence would strengthen the bound and settle the analogue of the community's r((C2)^6) = 14 fact.", + "first_step": "Shard joint_covers(7, [(9, 9)]) by least element and enumerate Sidon 9-set pairs under the shared-support identity |S| = 9 - e_ex - b_ex, sum A_x B_x >= 9.", + "blocked_by": "The unsharded joint tree stalls in the odd-side fill (max depth 15 in 20M nodes); orbit reduction under the 5,040 coordinate permutations is needed for a complete run." + } + ] +} diff --git a/research/universal-f7-singleton-seedb859517b/VERIFY.json b/research/universal-f7-singleton-seedb859517b/VERIFY.json new file mode 100644 index 0000000000..a08ddc5d35 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/VERIFY.json @@ -0,0 +1,41 @@ +{ + "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 and counting bounds, the five-bit set controls, the split-identity tables, and exact replay of the stored length-18 certificate and its witnesses" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Different-method cross-checks: dual-predicate coverage, subset-DP cycle realization, and an independent multiset enumeration of the split identity" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_engine.py" + ], + "timeout_seconds": 400, + "checks": "Sixteen unit tests: positive controls (pinned histograms and record hashes), negative controls (mutations, non-Hamiltonian sets), planted-hit non-vacuity of the joint search against brute force" + } + ] +} diff --git a/research/universal-f7-singleton-seedb859517b/engine.py b/research/universal-f7-singleton-seedb859517b/engine.py new file mode 100644 index 0000000000..210bd817b1 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/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-seedb859517b/independent.py b/research/universal-f7-singleton-seedb859517b/independent.py new file mode 100644 index 0000000000..c8e0878dc7 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/independent.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Independent cross-checks for the f(7) certificate (different methods). + +Nothing here imports engine.py. Coverage is tested with the dual predicate +(m is covered iff (P xor m) meets P) over plain Python sets; cycle realization +uses subset dynamic programming instead of depth-first search; the Lemma A +contradiction is re-derived by exhaustive enumeration of the concrete collision +multisets rather than by the closed-form bound. +""" +import json +import sys +from itertools import combinations +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def dual_covered(P, m): + S = set(P) + return any((p ^ m) in S for p in S) + + +def coverage_size_dual(P): + n = max(p.bit_length() for p in P) + size = 1 << max(n, 1) + return sum(1 for m in range(size) if dual_covered(P, m)) + + +def hamiltonian_cycle_dp(P, n): + """Subset DP: a cycle through all of P starting and ending at 0, or None.""" + P = sorted(set(P)) + if 0 not in P or len(P) != len(set(P)): + return None + idx = {v: i for i, v in enumerate(P)} + size = len(P) + adj = [[False] * size for _ in range(size)] + for i, a in enumerate(P): + for j, b in enumerate(P): + diff = a ^ b + adj[i][j] = diff and (diff & (diff - 1)) == 0 + full = (1 << size) - 1 + dp = [[False] * size for _ in range(1 << size)] + parent = [[-1] * size for _ in range(1 << size)] + dp[1][0] = True + for mask in range(1 << size): + for end in range(size): + if not dp[mask][end]: + continue + for nxt in range(size): + if (mask >> nxt) & 1 or not adj[end][nxt]: + continue + dp[mask | (1 << nxt)][nxt] = True + parent[mask | (1 << nxt)][nxt] = end + for end in range(size): + if dp[full][end] and adj[end][0]: + word = [] + mask, cur = full, end + stack = [] + while cur != 0: + stack.append(cur) + prev = parent[mask][cur] + mask ^= 1 << cur + cur = prev + stack.append(0) + stack.reverse() + for a, b in zip(stack, stack[1:] + [0]): + diff = P[a] ^ P[b] + word.append(diff.bit_length() - 1) + return word + return None + + +def _partitions(total, max_part=None): + """Integer partitions of total as tuples (smallest part first).""" + if max_part is None: + max_part = total + if total == 0: + yield () + return + for part in range(min(max_part, total), 0, -1): + for rest in _partitions(total - part, part): + yield (part,) + rest + + +def lemma_a_by_multiset(n, s, t): + """Re-derive feasibility by enumerating collision multisets explicitly. + + A_x and B_x are the numbers of unordered pairs of E and of O summing to x. + Full coverage forces support(A) u support(B) = all 2^(n-1) - 1 even nonzero + masks and sum_x A_x B_x >= ceil((s*t - 2^(n-1))/2). The per-value excesses + (A_x - 1) sum to C(s,2) - |support(A)|; coverage forces the total excess of + both sides to be at most C(s,2) + C(t,2) - (2^(n-1) - 1). We enumerate the + excess distributions directly (partitions of the excess) and compute the + largest attainable sum_x A_x B_x, without using the closed-form bound. + """ + 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 + if s * t < odd_masks or A + B < even_nonzero: + return False, "counting" + cap = A + B - even_nonzero + + def shapes(total, e): + for parts in _partitions(e): + yield [1 + p for p in parts] + [1] * (total - e - len(parts)) + + best = -1 + for e in range(0, min(A, cap) + 1): + for b in range(0, min(B, cap - e) + 1): + shared = A + B - e - b - even_nonzero + if shared < 0: + continue + for sa in shapes(A, e): + xs = sorted(sa, reverse=True) + for sb in shapes(B, b): + ys = sorted(sb, reverse=True) + total = sum(a * bb for a, bb in zip(xs[:shared], ys[:shared])) + if total > best: + best = total + return best >= need, f"best_sum_AB={best} need={need}" + + +def main(): + cert = json.loads((HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) + report = {} + + # 1. dual-test replay of any witness in the certificate + witnesses = cert["tier3_f7"].get("universal_words", []) + report["witnesses_replayed"] = 0 + for w in witnesses: + P = [0] + q = 0 + for j in w: + q ^= 1 << j + P.append(q) + assert q == 0, "witness word must be restored" + P = sorted(set(P[:-1])) + assert len(P) == 18, "length-18 witnesses walk 18 distinct prefixes" + assert coverage_size_dual(P) == 128, "dual test disagrees on coverage" + cyc = hamiltonian_cycle_dp(P, 7) + assert cyc is not None and len(cyc) == 18, "DP cycle check disagrees" + report["witnesses_replayed"] += 1 + + # 2. independent re-derivation of the split identity results + expected = {(7, 9, 8): False, (7, 8, 9): False, (7, 8, 8): False, + (7, 9, 9): True, (5, 5, 4): False, (5, 5, 5): True} + checked = {} + for (n, s, t), want in expected.items(): + ok, why = lemma_a_by_multiset(n, s, t) + assert ok == want, ((n, s, t), ok, why) + checked[f"n{n}_{s}_{t}"] = why + report["lemma_rows"] = checked + + # 3. dual-test agreement on the small control sets + P = [0, 1, 3, 2, 6, 4] + assert coverage_size_dual(P) == 8 + assert hamiltonian_cycle_dp(P, 3) is not None + assert hamiltonian_cycle_dp([0, 1, 2, 4], 3) is None + report["control_sets"] = "ok" + + (HERE / "INDEPENDENT.json").write_text( + json.dumps(report, indent=2, sort_keys=True), encoding="utf-8" + ) + print("PASS_F7_INDEPENDENT " + json.dumps(report, sort_keys=True)) + return report + + +if __name__ == "__main__": + main() diff --git a/research/universal-f7-singleton-seedb859517b/search.py b/research/universal-f7-singleton-seedb859517b/search.py new file mode 100644 index 0000000000..2bb66b8682 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/search.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Certificate search: sharp singleton f(7) gap in the PR943 prefix-walk model. + +Tiers (each exact integer computation, standard library only): + 1. Reproduction of the pinned censuses and counting bounds (smallest + falsifying instance first; byte-exact against the pinned EXPECTED.json). + 2. Controls: the five-bit set censuses and the lemma identity tables. + 3. The decisive length-18 census at n = 7: admissible parity splits, the + exhaustive (E, O) cover search for the surviving split, and a Hamiltonian + 18-cycle realization test for every cover found. + +Writes CERTIFICATE.json and prints one PASS marker. No floating point. +""" +import json +import sys +import time +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from engine import ( + admissible_splits, + census_words, + counting_least_even_L, + cyclic_census, + gray_word, + hamiltonian_cycle, + joint_covers, + lemma_a_table, + normalized_set_census, + prefixes, + rg_prefixes, + set_level_splits, + split_identity_feasible, + word_is_universal, +) + +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() + out = {"tier1_reproduction": {}, "tier2_controls": {}, "tier3_f7": {}} + + # ---- tier 1: reproduction of pinned values ---------------------------- + 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"] + out["tier1_reproduction"][f"n{n}_L{length}"] = { + "words": words, + "max_coverage": max(hist), + "records_sha256": digest, + "matches_pinned": True, + } + 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"] + out["tier1_reproduction"][f"n{n}"] = { + "counting_least_even_L": lb, + "gray_length": len(w), + } + print(f"REPRO n={n} least_even_L={lb} gray={len(w)}") + + # ---- tier 2: controls ------------------------------------------------- + stats9 = normalized_set_census(5, 9) + assert stats9 == {"sets": 7_888_725, "max_coverage": 29, "covers": 0}, stats9 + out["tier2_controls"]["n5_nine_point"] = stats9 + print("CONTROL n5 nine-point sets=7888725 max=29 covers=0") + + stats10 = normalized_set_census(5, 10) + splits10 = set_level_splits(5, 10) + joint10 = joint_covers(5, splits10) + assert len(joint10) == stats10["covers"] > 0 + cycles10 = 0 + for E, O in joint10: + P = sorted(set(E) | set(O)) + assert len(P) == 10 + if hamiltonian_cycle(P, 5) is not None: + cycles10 += 1 + assert cycles10 == 0, "f(5)=12 forbids a universal 10-cycle" + out["tier2_controls"]["n5_ten_point"] = { + "brute_sets": stats10["sets"], + "brute_covers": stats10["covers"], + "joint_covers": len(joint10), + "joint_splits": splits10, + "cycle_realisable_covers": cycles10, + } + print( + f"CONTROL n5 ten-point sets={stats10['sets']} covers={stats10['covers']} " + f"joint={len(joint10)} cycles=0" + ) + + for s, t in ((9, 8), (8, 9), (8, 8), (9, 9)): + rows = lemma_a_table(7, s, t) + feas = any(r["feasible"] for r in rows) + out["tier2_controls"][f"lemma_rows_{s}_{t}"] = { + "rows": len(rows), + "feasible": feas, + } + print(f"LEMMA (|E|,|O|)=({s},{t}) rows={len(rows)} feasible={feas}") + + # ---- tier 3: decisive length-18 cyclic census at n = 7 ---------------- + # Justification chain recorded in README/CLAIM: + # counting -> |P| >= 17; Lemma A identity -> |P| >= 18 (17-point splits + # (9,8)/(8,9) contradictory); |P| = 18 at length 18 forces a simple + # closed walk (simple=True) with the forced (9,9) split, whose identity + # budget is e_ex + b_ex <= C(9,2) + C(9,2) - 63 = 9 (budget=9). + splits = admissible_splits(7, 18) + assert splits == [(9, 9)], splits + out["tier3_f7"]["admissible_splits_L18"] = splits + out["tier3_f7"]["size17_splits"] = { + f"{s}_{t}": split_identity_feasible(7, s, t) for s, t in ((9, 8), (8, 9)) + } + + progress_path = HERE / "CERTIFICATE-PROGRESS.json" + if progress_path.exists(): + progress = json.loads(progress_path.read_text(encoding="utf-8")) + else: + progress = {"done": {}, "accum": {"nodes": 0, "leaves": 0, "hits": 0, + "words": []}} + shards = rg_prefixes(7, 3) + for pref in shards: + key = "".join(map(str, pref)) + if key in progress["done"]: + continue + r = cyclic_census(7, 18, budget=9, 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_path.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']}") + + acc = progress["accum"] + out["tier3_f7"]["shards"] = len(shards) + out["tier3_f7"]["census_nodes"] = acc["nodes"] + out["tier3_f7"]["simple_18_cycles"] = acc["leaves"] + out["tier3_f7"]["universal_words"] = acc["words"] + out["tier3_f7"]["covers_found"] = None + out["tier3_f7"]["joint_nodes"] = None + print(f"F7 cyclic census nodes={acc['nodes']} cycles={acc['leaves']} " + f"universal_words={len(acc['words'])}") + + realisable = acc["words"] + for w in realisable: + assert word_is_universal(w, 7) and len(w) == 18 + + if realisable: + out["conclusion"] = "f(7)=18 witness found" + marker = "PASS_F7_SINGLETON_GAP f(7)=18 witness" + else: + out["conclusion"] = "f(7) >= 20 (length 18 excluded)" + marker = "PASS_F7_SINGLETON_GAP f(7)>=20 L18-excluded" + + out["seconds"] = round(time.time() - t0, 1) + (HERE / "CERTIFICATE.json").write_text( + json.dumps(out, indent=2, sort_keys=True), encoding="utf-8" + ) + print(marker) + return marker + + +if __name__ == "__main__": + main() diff --git a/research/universal-f7-singleton-seedb859517b/test_engine.py b/research/universal-f7-singleton-seedb859517b/test_engine.py new file mode 100644 index 0000000000..31c673bbc4 --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/test_engine.py @@ -0,0 +1,219 @@ +#!/usr/bin/env python3 +"""Tests for the f(7) singleton universal-path engine. + +Positive controls reproduce the pinned package numbers byte-for-byte; +negative controls are mutated words/configurations that must be rejected; +the set-level census reproduces the community nine-point five-bit result. +""" +import json +import sys +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from engine import ( + coverage_mask, + coverage_size, + cyclic_census, + prefixes, + rg_prefixes, + restricted_growth_words, + word_is_restored, + word_is_universal, + gray_word, + census_words, + counting_least_even_L, + split_identity_feasible, + admissible_splits, + normalized_set_census, + hamiltonian_cycle, + closed_walk_word, + joint_covers, + lemma_a_table, + set_level_splits, +) + +ROOT = Path(__file__).resolve().parents[2] +PINNED = json.loads( + (ROOT / "research" / "universal-connector-six-source" / "EXPECTED.json").read_text( + encoding="utf-8" + ) +) +PINNED_CENSUSES = {(c["sources"], c["length"]): c for c in PINNED["censuses"]} + + +class TestCoverage(unittest.TestCase): + def test_tiny_words(self): + self.assertEqual(coverage_size([0, 0]), 2) # D = {0, 1} + self.assertEqual(coverage_size([0, 1, 0, 1]), 4) # full F2^2 + self.assertEqual(coverage_size([0, 1, 0, 1, 2, 2]), 8) # full F2^3 + + def test_coverage_mask_matches_pairwise(self): + w = [0, 1, 0, 2, 0, 1, 0, 2, 3, 4, 3, 4] + ps = prefixes(w) + brute = 0 + for a in ps: + for b in ps: + brute |= 1 << (a ^ b) + self.assertEqual(coverage_mask(ps), brute) + + def test_gray_constructions_universal(self): + for n in range(1, 9): + rec = PINNED["constructions"][str(n)] + w = gray_word(n) + self.assertTrue(word_is_universal(w, n), f"n={n}") + self.assertEqual(len(w), rec["length"]) + self.assertTrue(word_is_restored(w, n)) + + def test_mutations_rejected(self): + w = gray_word(6) + self.assertTrue(word_is_universal(w, 6)) + bad = w[:-1] # omitted final source call + self.assertFalse(word_is_restored(bad, 6)) + self.assertFalse(word_is_universal(bad, 6)) + self.assertFalse(word_is_universal([0, 1, 0, 1], 3)) # label 2 unused + + +class TestReproduction(unittest.TestCase): + """Smallest falsifying instance first: the pinned censuses must reproduce + byte-for-byte (word counts, histograms, maxima, records SHA-256).""" + + def _run(self, n, length): + hist, records_sha, words = census_words(n, length) + pinned = PINNED_CENSUSES[(n, length)] + self.assertEqual(words, pinned["words"]) + self.assertEqual(max(hist), pinned["max_coverage"]) + self.assertEqual( + {str(k): v for k, v in sorted(hist.items())}, pinned["histogram"] + ) + self.assertEqual(records_sha, pinned["records_sha256"]) + + def test_n5_len10(self): + self._run(5, 10) + + def test_n6_len12(self): + self._run(6, 12) + + def test_n6_len14(self): + self._run(6, 14) + + +class TestCountingBound(unittest.TestCase): + def test_least_even_L(self): + # Pinned EXPECTED.json constructions record lower_bound 10/14/18. + self.assertEqual(counting_least_even_L(5), 10) + self.assertEqual(counting_least_even_L(6), 14) + self.assertEqual(counting_least_even_L(7), 18) + + def test_admissible_splits_L18_n7(self): + splits = admissible_splits(7, 18) + self.assertEqual(splits, [(9, 9)]) + + def test_split_identity_kills_small_odd_side(self): + # (9,8) at n=7: the pair-representation identity is contradictory. + self.assertFalse(split_identity_feasible(7, 9, 8)) + self.assertFalse(split_identity_feasible(7, 8, 9)) + self.assertFalse(split_identity_feasible(7, 8, 8)) + self.assertTrue(split_identity_feasible(7, 9, 9)) + # n=5 nine-point splits die the same way (community census: max 29). + self.assertFalse(split_identity_feasible(5, 5, 4)) + self.assertFalse(split_identity_feasible(5, 4, 5)) + self.assertTrue(split_identity_feasible(5, 5, 5)) + + def test_lemma_a_table(self): + table = lemma_a_table(7, 9, 8) + for row in table: + self.assertFalse(row["feasible"]) + table = lemma_a_table(7, 9, 9) + self.assertTrue(any(row["feasible"] for row in table)) + + +class TestSetCensusControl(unittest.TestCase): + def test_n5_nine_point_sets(self): + # Independent reproduction of the community five-bit result: + # all 7,888,725 normalized nine-point sets, zero full covers, max 29. + stats = normalized_set_census(5, 9) + self.assertEqual(stats["sets"], 7_888_725) + self.assertEqual(stats["max_coverage"], 29) + self.assertEqual(stats["covers"], 0) + + +class TestCycleRealization(unittest.TestCase): + def test_known_cycle(self): + # The 6-cycle of Q_3: 000, 001, 011, 010, 110, 100. + P = [0b000, 0b001, 0b011, 0b010, 0b110, 0b100] + w = hamiltonian_cycle(P, 3) + self.assertIsNotNone(w) + self.assertEqual(len(w), 6) + self.assertEqual(set(closed_walk_word(P, w)), set(P)) + + def test_star_not_hamiltonian(self): + # 000 plus its three neighbours: no cycle through all four points. + P = [0b000, 0b001, 0b010, 0b100] + self.assertIsNone(hamiltonian_cycle(P, 3)) + + def test_f5_ten_point_covers_not_realisable_at_10(self): + # f(5) = 12 pins that no 10-point cover of F2^5 is a closed 10-walk. + covers = joint_covers(5, set_level_splits(5, 10)) + self.assertTrue(covers, "the joint search must actually find covers") + for E, O in covers: + P = sorted(set(E) | set(O)) + self.assertEqual(len(P), 10) + self.assertIsNone( + hamiltonian_cycle(P, 5), "f(5)=12 forbids a 10-cycle cover" + ) + + +class TestJointCovers(unittest.TestCase): + def test_agrees_with_brute_force_n5(self): + # Cross-validation of the joint search against the brute-force + # ten-point set census (planted-hit non-vacuity: covers must be found). + brute = normalized_set_census(5, 10) + joint = joint_covers(5, set_level_splits(5, 10)) + self.assertGreater(brute["covers"], 0) + self.assertEqual(len(joint), brute["covers"]) + + +class TestCyclicCensus(unittest.TestCase): + """The decisive engine, validated at the pinned small values.""" + + def test_leaf_counts_match_canonical_words(self): + # Every canonical word with even multiplicities is closed, so with no + # prune the leaf count and leaf set must match restricted_growth_words. + for n, L in ((5, 10), (6, 12)): + want = set(restricted_growth_words(n, L)) + r = cyclic_census(n, L, collect_all=True) + self.assertEqual(r["leaves"], len(want), (n, L)) + self.assertEqual(set(r["all_words"]), want, (n, L)) + + def test_shards_partition_the_tree(self): + full = cyclic_census(5, 10) + parts = sum( + cyclic_census(5, 10, prefix=p)["leaves"] for p in rg_prefixes(5, 3) + ) + self.assertEqual(parts, full["leaves"]) + + def test_n5_len10_no_hit(self): + r = cyclic_census(5, 10) + self.assertEqual(r["hits"], 0, "f(5)=12 forbids universal 10-cycles") + self.assertEqual(r["leaves"], 945) + + def test_n5_len12_planted_hit(self): + r = cyclic_census(5, 12, stop_on_first=True) + self.assertGreaterEqual(r["hits"], 1, "f(5)=12 must be attained") + self.assertTrue(word_is_universal(r["words"][0], 5)) + + def test_n6_len14_no_hit(self): + r = cyclic_census(6, 14) + self.assertEqual(r["hits"], 0, "f(6)=16 forbids universal 14-cycles") + self.assertEqual(r["leaves"], 945_945) + + def test_n6_len16_planted_hit(self): + r = cyclic_census(6, 16, stop_on_first=True) + self.assertGreaterEqual(r["hits"], 1, "f(6)=16 must be attained") + self.assertTrue(word_is_universal(r["words"][0], 6)) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/universal-f7-singleton-seedb859517b/verify.py b/research/universal-f7-singleton-seedb859517b/verify.py new file mode 100644 index 0000000000..8776d416cd --- /dev/null +++ b/research/universal-f7-singleton-seedb859517b/verify.py @@ -0,0 +1,105 @@ +#!/usr/bin/env python3 +"""Verification for the f(7) singleton universal-path package. + +Rebuilds every reproduced and controlled number from scratch and compares the +stored certificate with EXPECTED.json field by field. With --full it also +re-runs the decisive length-18 census; without it, the census is replayed from +CERTIFICATE.json (witnesses are re-checked exactly) and its recorded node count +is compared against the stored expectation. + +Pass marker: PASS_F7_SINGLETON_GAP_VERIFY +""" +import argparse +import json +import sys +import time +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +from engine import ( + admissible_splits, + census_words, + counting_least_even_L, + cyclic_census, + gray_word, + hamiltonian_cycle, + joint_covers, + lemma_a_table, + normalized_set_census, + set_level_splits, + word_is_universal, +) + +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(): + ap = argparse.ArgumentParser() + ap.add_argument("--full", action="store_true", help="re-run the length-18 census") + args = ap.parse_args() + 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")) + + # reproduction: pinned censuses, counting bounds, Gray constructions + 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"] and max(hist) == pinned["max_coverage"] + assert {str(k): v for k, v in sorted(hist.items())} == pinned["histogram"] + assert digest == pinned["records_sha256"] + for n in (5, 6, 7): + assert counting_least_even_L(n) == PINNED["constructions"][str(n)]["lower_bound"] + w = gray_word(n) + assert word_is_universal(w, n) and len(w) == PINNED["constructions"][str(n)]["length"] + + # controls + stats9 = normalized_set_census(5, 9) + assert stats9 == {"sets": 7_888_725, "max_coverage": 29, "covers": 0} + stats10 = normalized_set_census(5, 10) + joint10 = joint_covers(5, set_level_splits(5, 10)) + assert len(joint10) == stats10["covers"] > 0 + for E, O in joint10: + P = sorted(set(E) | set(O)) + assert hamiltonian_cycle(P, 5) is None, "f(5)=12 forbids 10-cycles" + for s, t in ((9, 8), (8, 9), (8, 8)): + assert not any(r["feasible"] for r in lemma_a_table(7, s, t)), (s, t) + assert any(r["feasible"] for r in lemma_a_table(7, 9, 9)) + assert admissible_splits(7, 18) == [(9, 9)] + + # certificate agreement + assert cert["tier3_f7"]["admissible_splits_L18"] == [[9, 9]] + assert cert["tier3_f7"]["size17_splits"] == {"9_8": False, "8_9": False} + assert cert["conclusion"] == expected["conclusion"] + + if args.full: + r = cyclic_census(7, 18, budget=9, simple=True) + assert r["leaves"] == cert["tier3_f7"]["simple_18_cycles"], "cycle count drifted" + assert len(r["words"]) == len(cert["tier3_f7"]["universal_words"]), "hit count drifted" + else: + assert cert["tier3_f7"]["census_nodes"] == expected["census_nodes"] + assert cert["tier3_f7"]["simple_18_cycles"] == expected["simple_18_cycles"] + assert len(cert["tier3_f7"]["universal_words"]) == expected["universal_words"] + + # every recorded witness is real + for w in cert["tier3_f7"]["universal_words"]: + assert len(w) == 18 and word_is_universal(tuple(w), 7) + + print(f"PASS_F7_SINGLETON_GAP_VERIFY {cert['conclusion']} " + f"cycles={cert['tier3_f7']['simple_18_cycles']} " + f"universal_words={len(cert['tier3_f7']['universal_words'])} " + f"nodes={cert['tier3_f7']['census_nodes']} " + f"seconds={round(time.time() - t0, 1)}") + return 0 + + +if __name__ == "__main__": + sys.exit(main())