diff --git a/research/f7-17point-cover-audit-seedcfa215c2/CERTIFICATE.json b/research/f7-17point-cover-audit-seedcfa215c2/CERTIFICATE.json new file mode 100644 index 0000000000..97781d3610 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/CERTIFICATE.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "object": "PR 2542's claim 'No 17-point set covers F2^7' (README, 'Why length 18 collapses', item 3), audited against its own lemma table at the set level", + "status": "partial", + "result_summary": "(9,8)/(8,9) dead in the identity (PR 2542's own rows, re-derived); (10,7)/(7,10) EXCLUDED (no surviving sharp row after the min-excess census); (11,6)/(6,11) reduced to two rows (5,1),(6,0) - the (3,3) and (4,2) rows are demoted by the completed k=11 census (zero 11-sets of excess <= 4). The literal claim is established for four of the six counting-feasible splits; the two (11,6)/(6,11) rows remain open.", + "identity_rows": { + "constraint": "odd excess sum_o (r_o - 1) = s*t - 64; colliding cross pairs sum_o C(r_o, 2) = 2 * sum_x A_x B_x = 2c; C(r,2) >= r-1 per mask; profiles partition the excess into j = r_o - 1 parts with sigma = sum j(j+1)/2 = 2c even", + "9_8": {"feasible": false, "best": 1, "need": 4, "note": "PR 2542's contradiction re-derived"}, + "8_9": {"feasible": false, "best": 1, "need": 4, "note": "PR 2542's contradiction re-derived"}, + "10_7": {"feasible": true, "best": 4, "need": 3, "rows": 6, "profile_c_values": [3, 4, 5, 6, 8]}, + "7_10": {"feasible": true, "best": 4, "need": 3, "rows": 6, "profile_c_values": [3, 4, 5, 6, 8]}, + "11_6": {"feasible": true, "best": 16, "need": 1, "rows": 7, "row_class": "(e_ex, b_ex, c) = (e, 6-e, 1), shared = 1"}, + "6_11": {"feasible": true, "best": 16, "need": 1, "rows": 7, "row_class": "(e_ex, b_ex, c) = (e, 6-e, 1), shared = 1"} + }, + "min_excess_census": { + "group": "E = even-weight elements of F2^7, isomorphic to F2^6; GL(6,2)-invariant (extension to the odd coset preserves pair sums, cross sums and coverage); shard {0, 3} is existence-complete by transitivity", + "k10_budget0": 0, + "k10_budget1": 0, + "k10_budget2": 0, + "k10_budget3": 149990400, + "k11_budget2": 0, + "k11_budget4_walk": "complete: 62/62 sub-shards, level-3 count 0, level-4 count 0 (zero 11-sets of pair-sum excess <= 4; RAW11-PROGRESS.json, resumable per sub-shard)", + "k9_budget0": 17776640, + "k7_odd_budget0": 34122816, + "consequences": [ + "min pair-sum excess of 10-point sets in F2^6 is exactly 3 (10-sets of excess <= 2 do not exist; the floor is attained 149,990,400 times through {0,3})", + "min pair-sum excess of 11-point sets in F2^6 is >= 5 (the completed budget-4 walk finds zero leaves in every sub-shard)", + "the extremal (10,7) row (e_ex = 0) is impossible (F2^6 has no Sidon 10-set)", + "every surviving (10,7) row needs shared = 3 - e_ex - b_ex <= 0, and the only such row (3,0) attains c = 0 only: the (10,7)/(7,10) splits are excluded", + "the surviving (11,6) rows are (5,1),(6,0) - rows (3,3) and (4,2) are demoted by the k=11 census - each with shared = 1 and A_x = B_x = 1 at the unique shared sum" + ] + }, + "controls": { + "small_space_agreement": "enumerate_sets == naive itertools brute force on the 16-element even subgroup (even-weight integers < 32): k=4 420/420, k=5 840/840, k=6 168/168 at budgets 0/1/2", + "independent_rows": "independent.py re-derives all six rows by direct count-vector loops: agreement on feasibility, rows, best and need", + "n5_nine_point": "covers=0, max |S+S| = 29/32 (community fact reproduced by PR 2542's control; here by exact census of all C(31,8) = 7,888,725 nine-point sets)", + "n5_ten_point": "covers=99,200 (exact census of all C(31,9) = 20,160,075 ten-point sets), max 32/32", + "mirror": "odd translation swaps the E/O parts and preserves S+S; (s,t) and (t,s) rows agree" + }, + "reproductions": { + "n5_L10": "words=945 max=31 sha=3dcc5689a4a34bae (pinned EXPECTED.json byte-exact)", + "n6_L12": "words=10395 max=49 sha=491b295f12cfa34a", + "n6_L14": "words=945945 max=59 sha=3d711ffa19209310", + "PR2542_L18": "nodes=15775992 cycles=312064 universal_words=0 (full re-run against the vendored engine)", + "PR2634_campaign": "L20=120 L22=126 L24=128 reproduced exactly (in-session run of PR 2634's verify.py)", + "PR2634_census20": "PARTIAL shards=11/15 nodes=798901058 cycles=67674177 universal_words=0 (in-session run)", + "PR2691_census20_complete": "15/15 shards: 6,305,209,079 nodes, 597,148,314 simple 20-cycles, zero universal (recorded state, PR 2691 by Nicholas Stone; not re-run here)" + }, + "no_kappa_claim": true +} diff --git a/research/f7-17point-cover-audit-seedcfa215c2/CLAIM.md b/research/f7-17point-cover-audit-seedcfa215c2/CLAIM.md new file mode 100644 index 0000000000..21e4e993c8 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/CLAIM.md @@ -0,0 +1,103 @@ +# Task card — KB3c (pair-collision object change): audit PR 2542's "no 17-point set covers F2^7" + +Task ID / proposed scope key: kappa-blocker KB3c (assigned explicit open request, +discussion 1166); drawn card `supplier-boundary-audit` (scope key +`dcdb0fa8e49b08a958d0`, chooser seed `cfa215c2c38597502362f49fd5b40ff0`); scope +**changed** to the set-level claim audit below. + +Base commit; exact predecessor and dependency heads: +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` (canonical main, priority revision 4). +Predecessors: [PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542) +by Aaron Wang (head `3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf`, package +`research/universal-f7-singleton-seedb859517b`), engine vendored byte-exact; +[PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634) by Aaron Wang +(head `e2f30d93efbef5658334072aa855aa95e795e394`, package +`research/universal-f7-singleton-l20-seed06704c39`); +[PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) by Nicholas +Stone (NicholasStone) completing the simple-20-cycle census to 15/15 shards. +Model source: [PR 943](https://github.com/CrocSwap/integer-mult-bounds/pull/943) +by Ross Richardson (`research/universal-connector-boundary`); pinned record +[PR 1185](https://github.com/CrocSwap/integer-mult-bounds/pull/1185) by Doug +Colkitt (Mister-Meeseeks) (`research/universal-connector-six-source`). + +Concrete object and question: +PR 2542's README asserts **"No 17-point set covers `F2^7`"** (section "Why length +18 collapses", item 3), but its own `lemma_a_table` / `lemma_a_by_multiset` +contradiction is computed only for the split rows `(9,8)`, `(8,9)` (and `(8,8)`); +its CERTIFICATE records `size17_splits = {"9_8": false, "8_9": false}` only. +Counting-feasible 17-point parity splits `(s,t) = (|E|,|O|), s+t = 17` are exactly +`(9,8), (8,9), (10,7), (7,10), (11,6), (6,11)`. Question: **does any 17-point +set `S` with `S+S = F2^7` exist at all** — i.e. is PR 2542's literal claim true, +or does a 17-point covering set exist (falsifying instance)? Equivalently, extend +the pair-representation identity to the surviving rows `(10,7)/(7,10)/(11,6)/(6,11)` +and decide their realizability exactly. + +Scope status: **changed** (authorized "explicit open request" scope change, +recorded in TASK.json with this reason). The assignment drew the card; the draw +(supplier-boundary-audit / uniform-transfer-audit / selected-stock-envelope) is +saturated/off-track. The assignment's options (a)/(b)/(c) were checked against the +live board: (a) the L=20 simple-cycle shards are **completed** by [PR +2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) (6,305,209,079 +nodes / 597,148,314 simple 20-cycles / 0 universal, 15/15 shards); (b) the +repeated-state L=20 **word** census (splits (10,9),(10,8),(9,9),(10,7)) is +**actively claimed** by Nicholas Stone (NicholasStone, Kimi agent), discussion +1166 comment 18954844 (2026-10-15 17:46 UTC, expires 21:30 UTC); (c) the +existence of an L=20 universal word is that claim's own question. Pair-collision +rule: changed objects on the match. The changed object is the **set-level** +question the assignment itself names as the recorded remainder ("PR 2542's 'no +17-point set covers F2^7' overreaches its own lemma table") — a claim audit +matching the drawn adversarial-audit track, decided without enumerating words. + +Existing restriction being changed (or exact claim being audited): +Audited claim: "No 17-point set covers F2^7" +([PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542), README, +section "Why length 18 collapses", item 3). Scope boundary: set-level covers only +(`S subset F2^7`, `|S| = 17`, `S+S = F2^7`); no word enumeration (Nicholas +Stone's claimed object), no kappa/supplier/selected-frontier change. + +Method; explicit parameter ranges/candidate alphabet: +1. Reproduce PR 2542/2634 recorded numbers first (n=5 L=10 words=945 max=31; + n=6 L=12 words=10395 max=49; n=6 L=14 words=945945 max=59; L18 + nodes=15775992 cycles=312064 universal_words=0; L20 campaign 120/126/128). +2. Extend the pair-representation identity to rows (10,7),(7,10),(11,6),(6,11): + closed-form `lemma_a_table` rows plus the sharper collision-multiplicity + identity (cross-sum collisions: `sum_o C(r_o,2) = 2 sum_x A_x B_x`, odd excess + `sum_o (r_o - 1) = st - 64`, profiles partitioning the excess), machine-checked + against `lemma_a_by_multiset`-style enumeration. +3. Smallest falsifying instance first: search for one 17-point covering set + (set-ILS at k=17, then exact structured search of the extremal Sidon/Sidon + profile (10,7) with 0 in A WLOG; A subset of E = F2^6 image, B subset of the + odd coset, exact pair-sum support constraints). Sharded/resumable with exact + counts if the tree exceeds the budget. + +Nearest overlapping PRs and why this adds something: +[PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542) proves the +L=18 exclusion using only the (9,8)/(8,9) rows; this audits its generalized +headline and fills the missing rows. [PR +2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634) records the +open remainder and the cover/walk dichotomy (open question 2: "Is r((C2)^7) = +20?"); this decides the k=17 level exactly where its identity leaves it open. +[PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) and +Nicholas Stone's active claim enumerate words at L=20; a set-level exclusion of +the (10,7) row prunes their smallest split (handoff), and their object is +explicitly not taken. + +Optimistic full cost budget; required observable improvement: +Finite combinatorial object; no supplier moment to price. Required observable: +the complete six-row 17-point split table with machine-checked identity rows and +either (i) an explicit 17-point covering set or (ii) exact exclusions of the +searched profile classes with exact counts. + +Success evidence; falsification test; time/compute cap: +Success = exact rows + witness-or-exclusion evidence, reproduced by a second +independent implementation. Falsification of "no 17-point cover" = one explicit +S with S+S = F2^7 (replayable in microseconds). Cap: one session, ~150 minutes, +with the final quarter reserved for verification, package, gate and handoff; +shard checkpoints if the exact search runs long. + +Predecessor authors; intended artifact and reproduction command: +Predecessor authors: Aaron Wang (PR 2542, PR 2634), Nicholas Stone (PR 2691), +Ross Richardson (PR 943), Doug Colkitt (PR 1185). Intended artifact: this +package (`research/f7-17point-cover-audit-seedcfa215c2/`) plus one focused PR. +Reproduction: `python3 -I -B research/f7-17point-cover-audit-seedcfa215c2/verify.py` +(plus `independent.py`, `test_engine.py`, and the sharded search entry point). diff --git a/research/f7-17point-cover-audit-seedcfa215c2/INDEPENDENT.json b/research/f7-17point-cover-audit-seedcfa215c2/INDEPENDENT.json new file mode 100644 index 0000000000..0ab5f13598 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/INDEPENDENT.json @@ -0,0 +1,141 @@ +{ + "receipt_consistency": { + "extension_floors": { + "excess3_10set_example_min_coll": 3, + "sidon9_example_min_coll": 3 + }, + "k10_budget0": { + "count": 0, + "first_valid": true + }, + "k10_budget1": { + "count": 0, + "first_valid": true + }, + "k10_budget2": { + "count": 0, + "first_valid": true + }, + "k10_budget3": { + "count": 149990400, + "first_valid": true + }, + "k11_budget2": { + "count": 0, + "first_valid": true + }, + "k11_raw_budget4": { + "complete": true, + "level3": 0, + "level4": 0, + "progress_agrees": true, + "sub_shards": 62 + }, + "k7_budget0": { + "count": 34122816, + "first_valid": true + }, + "k9_budget0": { + "count": 17776640, + "first_valid": true + } + }, + "rows_10_7": { + "agree": true, + "best": 4, + "feasible": true, + "need": 3, + "row_count": 6 + }, + "rows_11_6": { + "agree": true, + "best": 16, + "feasible": true, + "need": 1, + "row_count": 7 + }, + "rows_6_11": { + "agree": true, + "best": 16, + "feasible": true, + "need": 1, + "row_count": 7 + }, + "rows_7_10": { + "agree": true, + "best": 4, + "feasible": true, + "need": 3, + "row_count": 6 + }, + "rows_8_9": { + "agree": true, + "best": 1, + "feasible": false, + "need": 4, + "row_count": 0 + }, + "rows_9_8": { + "agree": true, + "best": 1, + "feasible": false, + "need": 4, + "row_count": 0 + }, + "small_group_budget_agreement": { + "k4_budget0": { + "agree": true, + "fast": 420, + "hist_agree": true, + "slow": 420 + }, + "k4_budget1": { + "agree": true, + "fast": 420, + "hist_agree": true, + "slow": 420 + }, + "k4_budget2": { + "agree": true, + "fast": 420, + "hist_agree": true, + "slow": 420 + }, + "k5_budget0": { + "agree": true, + "fast": 840, + "hist_agree": true, + "slow": 840 + }, + "k5_budget1": { + "agree": true, + "fast": 840, + "hist_agree": true, + "slow": 840 + }, + "k5_budget2": { + "agree": true, + "fast": 840, + "hist_agree": true, + "slow": 840 + }, + "k6_budget0": { + "agree": true, + "fast": 168, + "hist_agree": true, + "slow": 168 + }, + "k6_budget1": { + "agree": true, + "fast": 168, + "hist_agree": true, + "slow": 168 + }, + "k6_budget2": { + "agree": true, + "fast": 168, + "hist_agree": true, + "slow": 168 + } + } +} \ No newline at end of file diff --git a/research/f7-17point-cover-audit-seedcfa215c2/NOTICE.md b/research/f7-17point-cover-audit-seedcfa215c2/NOTICE.md new file mode 100644 index 0000000000..00bd605e5d --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/NOTICE.md @@ -0,0 +1,32 @@ +# NOTICE — attribution + +Agent: **Aaron Wang**, with help from opencode (substantial AI assistance in +scoping, implementation, verification and writing; no model named; no +independent human review claimed). Apache-2.0, same as the repository. + +- The audited claim "No 17-point set covers `F2^7`", the pair-representation + identity (`lemma_a_table`) and the length-18 exclusion are from + [PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542) by + Aaron Wang (navinor), package + `research/universal-f7-singleton-seedb859517b`. Its `engine.py` is vendored + byte-exact as `vendor/pr2542_engine.py` (SHA-256 + `82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4`). +- The recorded KB3b state (search campaign ceilings 120/126/128, the + cover/walk dichotomy, the resumable 20-cycle census and its open remainder) + is from [PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634) + by Aaron Wang (navinor). Its `test_lemma_rows_survive_at_L20` already pins + `lemma_a_table(7, 10, 7)` as feasible. +- The completed (10,10) simple-20-cycle census (15/15 shards) and the released + independent audit of PR 2634 are from + [PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) by + Nicholas Stone (NicholasStone, Kimi agent, substantial AI assistance). +- The prefix-walk model is + [PR 943](https://github.com/CrocSwap/integer-mult-bounds/pull/943) by Ross + Richardson (RossRichardson), `research/universal-connector-boundary`. +- The pinned record `f(5) = 12`, `f(6) = 16`, `18 <= f(7) <= 24` is + [PR 1185](https://github.com/CrocSwap/integer-mult-bounds/pull/1185) by Doug + Colkitt (Mister-Meeseeks), `research/universal-connector-six-source`. + +Nothing here claims a kappa, supplier, certificate or selected-frontier +change. No word-level census is performed; the repeated-state L=20 word +question belongs to the concurrent claim (discussion 1166 comment 18954844). diff --git a/research/f7-17point-cover-audit-seedcfa215c2/RAW11-PROGRESS.json b/research/f7-17point-cover-audit-seedcfa215c2/RAW11-PROGRESS.json new file mode 100644 index 0000000000..c2094f17e3 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/RAW11-PROGRESS.json @@ -0,0 +1,317 @@ +{ + "budget": 4, + "complete": true, + "shards": { + "v0=10": { + "examples": {}, + "hist": {}, + "seconds": 850.3 + }, + "v0=101": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=102": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=105": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=106": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=108": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=111": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=113": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=114": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=116": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=119": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=12": { + "examples": {}, + "hist": {}, + "seconds": 225.4 + }, + "v0=120": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=123": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=125": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=126": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=15": { + "examples": {}, + "hist": {}, + "seconds": 208.2 + }, + "v0=17": { + "examples": {}, + "hist": {}, + "seconds": 164.0 + }, + "v0=18": { + "examples": {}, + "hist": {}, + "seconds": 141.1 + }, + "v0=20": { + "examples": {}, + "hist": {}, + "seconds": 120.0 + }, + "v0=23": { + "examples": {}, + "hist": {}, + "seconds": 113.4 + }, + "v0=24": { + "examples": {}, + "hist": {}, + "seconds": 87.4 + }, + "v0=27": { + "examples": {}, + "hist": {}, + "seconds": 80.7 + }, + "v0=29": { + "examples": {}, + "hist": {}, + "seconds": 62.6 + }, + "v0=30": { + "examples": {}, + "hist": {}, + "seconds": 57.2 + }, + "v0=33": { + "examples": {}, + "hist": {}, + "seconds": 52.7 + }, + "v0=34": { + "examples": {}, + "hist": {}, + "seconds": 50.3 + }, + "v0=36": { + "examples": {}, + "hist": {}, + "seconds": 36.2 + }, + "v0=39": { + "examples": {}, + "hist": {}, + "seconds": 33.4 + }, + "v0=40": { + "examples": {}, + "hist": {}, + "seconds": 24.2 + }, + "v0=43": { + "examples": {}, + "hist": {}, + "seconds": 22.4 + }, + "v0=45": { + "examples": {}, + "hist": {}, + "seconds": 16.0 + }, + "v0=46": { + "examples": {}, + "hist": {}, + "seconds": 14.9 + }, + "v0=48": { + "examples": {}, + "hist": {}, + "seconds": 10.5 + }, + "v0=5": { + "examples": {}, + "hist": {}, + "seconds": 349.0 + }, + "v0=51": { + "examples": {}, + "hist": {}, + "seconds": 12.6 + }, + "v0=53": { + "examples": {}, + "hist": {}, + "seconds": 7.3 + }, + "v0=54": { + "examples": {}, + "hist": {}, + "seconds": 6.2 + }, + "v0=57": { + "examples": {}, + "hist": {}, + "seconds": 4.7 + }, + "v0=58": { + "examples": {}, + "hist": {}, + "seconds": 4.3 + }, + "v0=6": { + "examples": {}, + "hist": {}, + "seconds": 348.5 + }, + "v0=60": { + "examples": {}, + "hist": {}, + "seconds": 4.1 + }, + "v0=63": { + "examples": {}, + "hist": {}, + "seconds": 2.8 + }, + "v0=65": { + "examples": {}, + "hist": {}, + "seconds": 2.1 + }, + "v0=66": { + "examples": {}, + "hist": {}, + "seconds": 1.6 + }, + "v0=68": { + "examples": {}, + "hist": {}, + "seconds": 1.0 + }, + "v0=71": { + "examples": {}, + "hist": {}, + "seconds": 0.9 + }, + "v0=72": { + "examples": {}, + "hist": {}, + "seconds": 0.5 + }, + "v0=75": { + "examples": {}, + "hist": {}, + "seconds": 0.5 + }, + "v0=77": { + "examples": {}, + "hist": {}, + "seconds": 0.3 + }, + "v0=78": { + "examples": {}, + "hist": {}, + "seconds": 0.2 + }, + "v0=80": { + "examples": {}, + "hist": {}, + "seconds": 0.1 + }, + "v0=83": { + "examples": {}, + "hist": {}, + "seconds": 0.1 + }, + "v0=85": { + "examples": {}, + "hist": {}, + "seconds": 0.1 + }, + "v0=86": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=89": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=9": { + "examples": {}, + "hist": {}, + "seconds": 287.9 + }, + "v0=90": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=92": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=95": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=96": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + }, + "v0=99": { + "examples": {}, + "hist": {}, + "seconds": 0.0 + } + }, + "total_hist": {} +} \ No newline at end of file diff --git a/research/f7-17point-cover-audit-seedcfa215c2/README.md b/research/f7-17point-cover-audit-seedcfa215c2/README.md new file mode 100644 index 0000000000..3330e0cfda --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/README.md @@ -0,0 +1,222 @@ +# KB3c — 17-point cover audit: PR 2542's "no 17-point set covers F2^7" against its own lemma table + +**Set-level finite result: the audited claim is established for four of the six +counting-feasible 17-point splits. The splits `(10,7)/(7,10)` are excluded +exactly; the splits `(11,6)/(6,11)` are reduced to two explicit surviving +rows. No new kappa.** + +[PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542) (Aaron +Wang) excludes length 18 for seven-source singleton universal words, proving +`f(7) >= 20`. Its "Why length 18 collapses" section asserts, in bold, **"No +17-point set covers `F2^7`"** — but its machine-checked `lemma_a_table` / +`lemma_a_by_multiset` contradiction is computed only for the parity splits +`(9,8)/(8,9)`, and its certificate records `size17_splits = {"9_8": false, +"8_9": false}` only. The counting-feasible 17-point splits `(|E|,|O|)` with +`|E|+|O| = 17` are exactly `(9,8),(8,9),(10,7),(7,10),(11,6),(6,11)`, and the +four non-`(9,8)` rows survive the identity as written +(`lemma_a_table(7, 10, 7)` is feasible: upper 3 versus need 3; PR 2634's +`test_lemma_rows_survive_at_L20` already pins this). + +This package audits the claim against that table: + +> **1. The pair-representation identity is extended to all six rows with a +> sharp collision-multiplicity constraint** (`sum_o C(r_o, 2) = 2 sum_x A_x +> B_x`, odd excess `sum_o (r_o - 1) = s*t - 64`), machine-checked and +> independently re-derived. `(9,8)/(8,9)` are re-killed (best 1, need 4); the +> `(10,7)` profiles force `c` in `{3, 4, 5, 6, 8}`; `(11,6)` collapses to one +> row class `(e_ex, b_ex, c) = (e, 6-e, 1)` with `shared = 1`. +> +> **2. An exact Sidon/near-Sidon census of the even group `E = F2^6` shows +> minimum pair-sum excess `>= 3` for 10-point sets** (10-sets of excess +> `<= 2` do not exist at all: `F2^6` has no Sidon 10-set), and **`>= 5` for +> 11-point sets** (the completed budget-4 walk finds zero 11-sets of excess +> `<= 4`). The shards through `{0, 3}` are existence-complete by `GL(6,2)` +> transitivity and invariance. +> +> **3. Consequence: `(10,7)/(7,10)` are excluded exactly** (the only identity +> row left at `e_ex >= 3` attains `c = 0`, not a profile value). **`(11,6)/(6,11)` +> are reduced to two rows** `(5,1),(6,0)`, each with one shared sum and +> `A_x = B_x = 1` there; the `(3,3)` and `(4,2)` rows are demoted by the +> completed k = 11 census. PR 2542's literal claim is therefore proved for +> the splits that its length-18 exclusion needed and for the +> length-20-relevant splits; the length-22-relevant `(11,6)/(6,11)` rows +> `(5,1),(6,0)` remain open. + +The recorded gap `20 <= f(7) <= 24` is unchanged; no word-level census is +performed here. The repeated-state L = 20 **word** census (splits +`(10,9),(10,8),(9,9),(10,7)`) is under the active concurrent claim of +Nicholas Stone (NicholasStone, Kimi agent), +[discussion 1166 comment 18954844](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18954844); +its `(10,7)/(7,10)` splits are empty a fortiori by result 3 and are handed +off in the FINDING post. Nothing here claims a supplier, tariff, certificate +or selected-frontier change. + +## Model and the audited claim + +In the PR943 prefix-walk model +([Ross Richardson, `research/universal-connector-boundary`](https://github.com/CrocSwap/integer-mult-bounds/pull/943)), +a restored word `w` over seven singleton labels is universal when +`D(w) = {q_s xor q_t} = F2^7` for its boundary states; equivalently the +prefix set `P` covers: `P + P = F2^n`. A 17-point cover is a set +`S` with `|S| = 17` and `S + S = F2^7`. Write `S = A u B` with +`A = S int E` (`s` even-weight points) and `B = S int O` (`t` odd-weight +points); the splits are the pairs `(s, t)` with `s + t = 17`. + +**Audited claim (PR 2542, README, "Why length 18 collapses", item 3):** +"No 17-point set covers `F2^7`." The length-18 exclusion only ever needed the +`(9,8)/(8,9)` rows: at `L = 18` position parity bounds `|E|,|O| <= 9`, so a +17-point prefix set at `L = 18` has split `(9,8)` or `(8,9)`. The overreach +matters at `L = 20` (`(10,7)/(7,10)` become parity-feasible) and at `L = 22` +(`(11,6)/(6,11)` likewise). + +## Reproduce + +From the repository root, standard library only, Python 3.12: + +```sh +python3 -I -B research/f7-17point-cover-audit-seedcfa215c2/verify.py +python3 -I -B research/f7-17point-cover-audit-seedcfa215c2/independent.py +python3 -I -B research/f7-17point-cover-audit-seedcfa215c2/test_engine.py +python3 -I -B research/f7-17point-cover-audit-seedcfa215c2/verify.py --full # re-runs the zero shards (~17 min) +``` + +Expected markers: `PASS_17POINT_VERIFY ...`, `PASS_17POINT_INDEPENDENT {...}`, +`Ran 13 tests ... OK`. + +## Smallest falsifying instance first: reproduction + +Before any new number, the recorded predecessor state is reproduced +byte-exactly (the engines are vendored/pinned, never trusted on read): + +| 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 PR 2542's decisive length-18 census re-run in full against the vendored +engine: `15,775,992` nodes, `312,064` simple 18-cycles, zero universal words, +and (in-session, PR 2634's own verifier at head `e2f30d93`) the search +campaign `120/126/128` at lengths 20/22/24 and the then-partial 20-cycle +census `11/15` shards, `798,901,058` nodes, `67,674,177` cycles. The +completed `(10,10)` census of +[PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) +(Nicholas Stone; `6,305,209,079` nodes, `597,148,314` cycles, zero universal, +15/15 shards) is the recorded current state and is not re-run here. + +## The sharp identity + +For `x` even nonzero let `A_x` count unordered pairs of `A` summing to `x`, +and `B_x` likewise on `B`. Put `e_ex = C(s,2) - |supp(A)|`, +`b_ex = C(t,2) - |supp(B)|`, and let the cross sums `a + b` hit the odd masks +with multiplicities `r_o`. Then exactly: + +* odd excess: `sum_o (r_o - 1) = s*t - 64`; +* colliding cross pairs: `sum_o C(r_o, 2) = 2 sum_x A_x B_x =: 2c`, since two + cross sums collide iff their `A`-pair and `B`-pair share a sum; +* `C(r, 2) >= r - 1` per mask, so a collision profile is a partition of the + odd excess into `j = r_o - 1` parts with `sigma = sum j(j+1)/2 = 2c` even; +* full even coverage forces `|supp(A) int supp(B)| = C(s,2) + C(t,2) - e_ex - + b_ex - 63` shared values, and `c` is a sum of shared products `A_x B_x`. + +A row `(e_ex, b_ex)` survives iff some integer profile's `c` is *exactly* +attainable over the shared values (this refines PR 2542's closed-form upper +bound). Machine results (`cover17.sharp_rows`, re-derived row-for-row by +`independent.py`): + +| Split | Sharp feasible | Best attainable `c` | Need `ceil((st-64)/2)` | Profile `c` values | +|---|---|---:|---:|---| +| `(9,8)` | no | 1 | 4 | — | +| `(8,9)` | no | 1 | 4 | — | +| `(10,7)` | yes | 4 | 3 | 3, 4, 5, 6, 8 | +| `(7,10)` | yes | 4 | 3 | 3, 4, 5, 6, 8 | +| `(11,6)` | yes | 16 | 1 | 1 | +| `(6,11)` | yes | 16 | 1 | 1 | + +`(11,6)` reduces to exactly seven rows `(e, 6-e, 1)` with `shared = 1`: odd +excess 2 admits only the profile with two doubled masks (`sigma = 2`), forcing +`c = 1` and hence `shared = 1` with `A_x = B_x = 1` at the unique shared sum. + +## The min-excess census + +Identify `E` with `F2^6`. Sidon-ness and the pair-sum excess are invariant +under translations and under `GL(6,2)`, whose extension to the odd coset +(`b |-> phi(b - u) + u`) preserves pair sums, cross sums and coverage; `GL(6,2)` +is transitive on nonzero elements, so the complete shard through `{0, 3}` +decides existence. Exact counts (`SIDON-RECEIPT.json`, resumable +`search17.py`, cross-validated against naive brute force on the 16-element +even subgroup at budgets 0/1/2 and against a second code path): + +| Domain (through `{0, 3}` in `E`) | Count | +|---|---:| +| 9-sets, excess 0 (Sidon) | 17,776,640 | +| 10-sets, excess 0 (Sidon) | 0 | +| 10-sets, excess `<= 1` | 0 | +| 10-sets, excess `<= 2` | 0 | +| 10-sets, excess `<= 3` | 149,990,400 | +| 11-sets, excess `<= 2` | 0 | +| 11-sets, excess `<= 4` (complete budget-4 walk, 62/62 sub-shards) | 0 | +| 7-sets in the odd coset through `{1}`, excess 0 | 34,122,816 | + +So the minimum pair-sum excess of a 10-point subset of `F2^6` is exactly `3` +(`F2^6` has no Sidon 10-set; the floor is attained 149,990,400 times through +`{0, 3}`) and the minimum for 11-point subsets is `>= 5`. Exact `n = 5` +controls reproduce the community facts: zero nine-point covers (max 29/32, +all `C(31,8) = 7,888,725` sets) and 99,200 ten-point covers (all +`C(31,9) = 20,160,075` sets). + +## The resulting row table + +* `(9,8)/(8,9)`: **PROVEN dead** in the identity (PR 2542's own rows, + re-derived). +* `(10,7)/(7,10)`: **PROVEN excluded exactly.** The identity rows all need + `e_ex + b_ex <= 3`; the census forces `e_ex >= 3`, leaving only `(3,0)`, + where `shared = 0` and `c = 0` is not a profile value (`{3,4,5,6,8}`). +* `(11,6)/(6,11)`: the identity reduces them to the row class + `(e_ex, b_ex, c) = (e, 6-e, 1)` with `shared = 1` and `A_x = B_x = 1` at + the unique shared sum (checked). The completed k = 11 census (min excess + `>= 5`) **demotes `(3,3)` and `(4,2)`**; the rows **`(5,1),(6,0)` remain + OPEN**, each with two doubled odd masks forced by the shared sum. A + further census level (k = 11 at budgets 5 and 6) decides them; see the + open questions. + +An odd translation swaps `E` and `O` while preserving `S + S`, so `(s,t)` and +`(t,s)` are one question (machine-checked in `test_engine.py`). + +## Scope and remaining obligations + +A finite set-level audit inside PR943's abstract interface. What was **not** +checked: realizability of the two surviving `(11,6)` rows (the joint +`(A, B)` tree needs stabilizer canonical forms; the `GL(6,2)`-invariance +lemma here reduces the domain to `0, 3 in A` but does not canonicalize pairs), +the 18-/19-point cover questions (`r((C2)^7)`), and every word-level question +(the L = 20 repeated-state census is the concurrent claim's object). No +instantiation in the selected supplier, no kappa claim. + +## Open next questions + +1. **Do 17-point covers with split `(11,6)/(6,11)` exist?** The two + surviving rows are `(5,1)` and `(6,0)`, each with `shared = 1`, + `A_x = B_x = 1` at the shared sum. Why it matters: it decides the last + open family of the audited claim and whether `|P| = 17` is possible at + all at `L = 22`. First step: a k = 11 budget-5/6 census of the same raw + `{0, 3}` domain (the budget-4 walk took 54 minutes and is resumable per + sub-shard) demotes `(5,1)` and `(6,0)` one by one; surviving rows then + need a row-restricted joint search (11-sets at the row's excess/collision + shape plus a constrained B-side DFS forced to cover + `E \\ {0} \\ supp(A)`). Blocked by: the B side has ~3.1e8 Sidon 6/7-sets + and cannot be enumerated outright; stabilizer canonical forms for the + pair `(A, B)` are not implemented. +2. **Is `r((C2)^7) = 20`?** (PR 2542's open question 2, sharpened by PR 2634.) + First step: extend the sharp-row machinery and the min-excess census to + `k = 18/19` splits. Blocked by: the same joint-tree growth. +3. **Does the collision-multiplicity identity extend to a covering bound for + larger `k`?** The profile constraint (`sum_o C(r_o,2) = 2 sum_x A_x B_x` + with `C(r,2) >= r-1`) is exact for any `s, t`; a general table over + `(|E|,|O|)` would prune the word census's splits directly. First step: + generate `cover17.sharp_rows` over the `L = 22` splits and hand them to the + word claim. Blocked by: nothing; this is cheap bookkeeping. + +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/f7-17point-cover-audit-seedcfa215c2/SIDON-RECEIPT.json b/research/f7-17point-cover-audit-seedcfa215c2/SIDON-RECEIPT.json new file mode 100644 index 0000000000..fc26d2d907 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/SIDON-RECEIPT.json @@ -0,0 +1,79 @@ +{ + "controls": { + "small_space_agreement": "enumerate_sets == naive brute force on the even subgroup < 32: k=4 420/420, k=5 840/840, k=6 168/168" + }, + "k11_raw_budget4": { + "complete": true, + "domain": "11-sets through {0,3} (complete by GL(6,2) transitivity), sub-sharded by the smallest free element", + "sub_shards": 62, + "total_hist": {} + }, + "shard_e03": { + "k10_budget0": { + "count": 0, + "first": null, + "seconds": 272.8 + }, + "k10_budget1": { + "count": 0, + "first": null, + "seconds": 276.2 + }, + "k10_budget2": { + "count": 0, + "first": null, + "seconds": 264.0 + }, + "k10_budget3": { + "count": 149990400, + "first": [ + 0, + 3, + 5, + 6, + 9, + 17, + 33, + 58, + 65, + 92 + ], + "seconds": 3381.2 + }, + "k11_budget2": { + "count": 0, + "first": null, + "seconds": 223.5 + }, + "k9_budget0": { + "count": 17776640, + "first": [ + 0, + 3, + 5, + 9, + 17, + 30, + 33, + 65, + 102 + ], + "seconds": 146.4 + } + }, + "shard_o1": { + "k7_budget0": { + "count": 34122816, + "first": [ + 1, + 2, + 4, + 8, + 16, + 31, + 32 + ], + "seconds": 62.2 + } + } +} \ No newline at end of file diff --git a/research/f7-17point-cover-audit-seedcfa215c2/SOURCES.json b/research/f7-17point-cover-audit-seedcfa215c2/SOURCES.json new file mode 100644 index 0000000000..3cca9c8db3 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/SOURCES.json @@ -0,0 +1,67 @@ +{ + "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": "vendor/pr2542_engine.py", + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "git_blob": "210bd817b19beb20ed474d8946ea87a22121ac1c", + "sha256": "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + "note": "Vendored byte-exact (copied, never imported from the predecessor package), credit PR 2542. The live drift check pins base-commit blobs only, so this head-pinned vendor copy is enforced by test_engine.py's test_pr2542_engine_byte_pin instead." + }, + { + "pr": 2542, + "source_path": "research/universal-f7-singleton-seedb859517b/README.md", + "local_path": null, + "head": "3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf", + "note": "The audited claim 'No 17-point set covers F2^7' and the lemma_a_table rows (9,8)/(8,9) originate here; reproduced and re-run in verify.py against the vendored engine." + }, + { + "pr": 2634, + "source_path": "research/universal-f7-singleton-l20-seed06704c39/", + "local_path": null, + "head": "e2f30d93efbef5658334072aa855aa95e795e394", + "note": "Recorded KB3b state reproduced in-session before new work (945/31, 10395/49, 945945/59; L18 15,775,992/312,064/0; campaign 120/126/128; census 11/15 shards 798,901,058/67,674,177). Its test_lemma_rows_survive_at_L20 already pins lemma_a_table(7,10,7) feasible; this package decides that row and its siblings exactly." + }, + { + "pr": 2691, + "source_path": "research/universal-f7-singleton-l20-census-complete-seedfd938f30/", + "local_path": null, + "head": "88dda353", + "note": "Nicholas Stone (NicholasStone, Kimi agent): completion of the (10,10) simple-20-cycle census (6,305,209,079 nodes / 597,148,314 cycles / zero universal, 15/15 shards) and the released audit of PR 2634; read as current recorded state, not re-run here." + } + ], + "notes": { + "model_and_pinned_results": "PR943 query model (research/universal-connector-boundary, Ross Richardson, https://github.com/CrocSwap/integer-mult-bounds/pull/943); pinned f(5)=12, f(6)=16 and the open f(7) gap (research/universal-connector-six-source, Doug Colkitt, https://github.com/CrocSwap/integer-mult-bounds/pull/1185). Read and reproduced byte-exactly, never imported.", + "audited_claim": "PR 2542 (Aaron Wang, https://github.com/CrocSwap/integer-mult-bounds/pull/2542) README, 'Why length 18 collapses', item 3: 'No 17-point set covers F2^7', computed there only for the split rows (9,8)/(8,9).", + "concurrent_scopes": "Nicholas Stone (NicholasStone) holds the repeated-state L=20 word census claim (discussion 1166 comment 18954844): splits (10,9),(10,8),(9,9),(10,7) at the word level. This package is set-level only and enumerates no words; the (10,7)/(7,10) set-level exclusion here prunes that claim's smallest split and is handed off in the FINDING post." + } +} diff --git a/research/f7-17point-cover-audit-seedcfa215c2/TASK.json b/research/f7-17point-cover-audit-seedcfa215c2/TASK.json new file mode 100644 index 0000000000..1d40e4dba1 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "session_seed": "cfa215c2c38597502362f49fd5b40ff0", + "track": "adversarial-audit (drawn); scope changed to assigned kappa-blocker KB3c (set-level 17-point cover claim audit)", + "scope_key": "dcdb0fa8e49b08a958d0", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18956008", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "changed", + "actual_scope": "Kappa-blocker KB3c, pair-collision object change: audit PR 2542's headline claim 'No 17-point set covers F2^7' against its own lemma table at the SET level (S subset F2^7, |S| = 17, S+S = F2^7). Delivered: the pair-representation identity extended to the four surviving split rows (10,7)/(7,10)/(11,6)/(6,11) with the sharp collision-multiplicity constraint (sum_o C(r_o,2) = 2 sum_x A_x B_x with odd excess sum_o (r_o-1) = s*t-64), machine-checked and independently re-derived; the exact Sidon/near-Sidon census of the even group E = F2^6 showing minimum pair-sum excess exactly 3 for 10-sets (floor attained 149,990,400 times through {0,3}) and >= 5 for 11-sets (completed budget-4 walk: zero leaves in 62/62 sub-shards), complete GL(6,2)-transitive shards through {0,3}; and the resulting exact exclusions: (9,8)/(8,9) dead in the identity (PR 2542's own rows), (10,7)/(7,10) dead outright (zero surviving rows), (11,6)/(6,11) reduced to two rows (5,1),(6,0) with exact collision data (shared = 1, c = 1) - rows (3,3) and (4,2) demoted by the completed k=11 census. No word enumeration (the repeated-state L=20 word census is under an active concurrent claim); no kappa, supplier or selected-frontier change.", + "scope_change_reason": "Authorized 'explicit open request' scope change, recorded as instructed by the assignment. The chooser (OS seed cfa215c2c38597502362f49fd5b40ff0) drew saturated adversarial-audit cards (supplier-boundary-audit / uniform-transfer-audit / selected-stock-envelope); the assignment states the draw landed on saturated cards and authorizes KB3c as the explicit open request. Pair-collision checks (discussions 1317 and 1166 with nested replies via agent_tools.py disc-comments, plus find_overlap.py --refresh with the object's proper names) then changed the object within KB3c: option (a) (finish the L=20 shards) is completed by PR 2691 (Nicholas Stone, 6,305,209,079 nodes / 597,148,314 simple 20-cycles / zero universal, 15/15 shards), and options (b)/(c) (the repeated-state L=20 splits by the pair-representation method; an L=20 universal word) are the active claim of Nicholas Stone (discussion 1166 comment 18954844, expires 2026-10-15 21:30 UTC). The changed object is the set-level core the assignment itself names as the recorded remainder ('PR 2542's no-17-point-set claim overreaches its own lemma table'), decided here without enumerating words.", + "bottleneck_link": "An exact set-level exclusion or covering witness at 17 points decides how small a universal word's prefix set can be inside the unchanged PR943 query model, and feeds the repeated-state L=20 word census its per-split feasibility. It changes no supplier, tariff or kappa and instantiates no physical interface.", + "object_synonyms_used_in_overlap": [ + "17-point set", + "pair representation", + "lemma A", + "additive basis", + "r((C2)^7)", + "Sidon", + "sum covering", + "covering set", + "cover/walk", + "universal source path", + "singleton alphabet", + "seven-source", + "f(7)", + "simple 20-cycle", + "repeated state" + ], + "pair_collision_check": { + "checked_utc": "2026-10-15T18:20:00Z/2026-10-15T18:29:00Z and 2026-10-15T19:08:00Z/2026-10-15T19:11:00Z", + "tool": "agent_tools.py disc-comments (with nested replies) + scripts/find_overlap.py --refresh", + "threads_scanned": [ + "discussion 1317 since 2026-10-15T00:00:00Z (full dump incl. nested replies)", + "discussion 1166 since 2026-10-15T00:00:00Z (full dump incl. nested replies)" + ], + "result": "Entry pass: active CLAIM by Nicholas Stone (comment 18954844) on the repeated-state L=20 word census (splits (10,9),(10,8),(9,9),(10,7)) and PR 2691 completion of the (10,10) simple-cycle census; object changed per the pair-collision rule to the set-level claim audit. Refined pass before heavy computation (190 matches): no claim on the set-level 17-point question; the only KB3-line activity is the released KB3/KB3b claims and this session's own claim (comment 18956008)." + }, + "smallest_falsifying_instance_first": "Before any new number: PR 2542's verify.py/independent.py/test_engine.py and PR 2634's verify.py/independent.py/test_engine.py reproduced in full (PASS_F7_SINGLETON_GAP_VERIFY cycles=312064 universal_words=0 nodes=15775992; PASS_F7_INDEPENDENT best_sum_AB=1 need=4; 22 tests OK; REPRO n=5 L=10 words=945 max=31, n=6 L=12 words=10395 max=49, n=6 L=14 words=945945 max=59; SEARCH campaign reproduced exactly L20=120 L22=126 L24=128; CENSUS20 PARTIAL shards=11/15 nodes=798901058 cycles=67674177; 14 tests OK). The falsifying instance for the audited claim is one 17-point set S with S+S = F2^7; the exact census stages were run smallest-first (Sidon 10 = extremal row, then excess budgets 1, 2, 3), each an exact obstruction with counts recorded.", + "priced_budget_minutes": 150, + "priced_budget_breakdown": "25 min entry overlap, pair-collision checks and the task card (done), 30 min predecessor reproductions PR 2542 + PR 2634 (done, exact markers), 25 min identity extension + tests (TDD, 13 tests), 45 min exact Sidon/near-Sidon census (receipt + deeper levels), 25 min package, verification, gate and submission. No pivot beyond the recorded pair-collision object change.", + "de_diagnostic": "Not applicable: a finite set-level question in the PR943 query model, with no supplier width m, role count W, child ranks or recursive moment to price. The applicable diagnostic is exact reproduction against the pinned predecessor numbers plus independently re-derived identity rows.", + "stop_rule": "Stop at the first of: (a) an explicit 17-point covering set (the claim is false as stated), (b) a complete exact exclusion of all six 17-point split rows (the claim is proved as stated), or (c) the priced budget expiring with the exact obstruction recorded (which rows are excluded, which survive, and the exact counts behind each). No second pivot.", + "outcome": "partial", + "evidence": "CERTIFICATE.json records the six-row 17-point split table (identity rows, collision profiles, min-excess census consequences) and the census counts. SIDON-RECEIPT.json holds the exact shard counts (k=10 budgets 0/1/2 empty and budget 3 = 149,990,400 through {0,3}; k=11 budget 2 empty and the complete budget-4 walk: zero leaves in 62/62 sub-shards, level-3 and level-4 counts 0; 17,776,640 Sidon 9-sets and 34,122,816 Sidon 7-sets in the same sharding) with timings and examples; RAW11-PROGRESS.json is the resumable per-sub-shard checkpoint of the k=11 walk. cover17.py holds the extended identity (collision-multiplicity constraint and exact attainable-c enumeration); independent.py re-derives every row by direct count-vector loops, validates the excess-budget semantics against naive brute force, and cross-checks the k=11 completion plus the extension-collision floors on the recorded examples; test_engine.py holds 13 tests including the vendored-engine byte pin and the exact n=5 controls (zero nine-point covers max 29; 99,200 ten-point covers). verify.py replays everything in 150 s and re-runs the load-bearing zero shards with --full. 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": "Do 17-point covering sets with split (11,6)/(6,11) exist? The two surviving sharp rows are (e_ex, b_ex, c) = (5,1,1) and (6,0,1), each with shared = 1 and A_x = B_x = 1 at the unique shared sum.", + "why_it_matters": "It decides the last open family of PR 2542's 'No 17-point set covers F2^7' claim and therefore whether |P| = 17 is possible at all for a universal word (at L = 22 the split (11,6) is parity-feasible).", + "first_step": "A k = 11 budget-5/6 census of the same raw {0,3} domain (resumable per sub-shard; the completed budget-4 walk took 54 minutes) demotes the rows one by one; surviving rows need a row-restricted joint search: enumerate 11-sets of E with the row's excess and collision shape and for each run a constrained B-side DFS (6-sets of the odd coset) forced to cover E \\ {0} \\ supp(A) with the exact shared-sum and cross-coverage constraints.", + "blocked_by": "The B side has ~3.1e8 Sidon 6/7-sets and cannot be enumerated outright; the joint tree needs orbit reduction (GL(6,2) invariance is proved here and fixes 0, 3 in A, but stabilizer canonical forms for the pair (A,B) are not implemented)." + }, + { + "question": "Is r((C2)^7) = 20, i.e. do 18-point or 19-point covers of F2^7 exist (PR 2542 open question 2, sharpened by PR 2634)?", + "why_it_matters": "It settles the set-level restricted addition basis value and bounds |P| from below for universal words at L = 20 and L = 22.", + "first_step": "Extend this package's sharp-row machinery to k = 18/19 (the collision-multiplicity identity applies unchanged) and run the same min-excess census per split row.", + "blocked_by": "The same joint-tree growth; the exact census here covers the 17-point rows only." + }, + { + "question": "For the concurrent repeated-state L=20 word claim: does the set-level exclusion of (10,7)/(7,10) leave any |P| = 17 word family at L = 20?", + "why_it_matters": "It prunes the smallest split of the word census under claim (discussion 1166 comment 18954844).", + "first_step": "Handoff: the word claim's (10,7) split is empty a fortiori (a universal word's prefix set would be a 17-point cover with split (10,7), which this package excludes); the claim's remaining splits are (10,9), (10,8), (9,9).", + "blocked_by": "Nothing; this is a handoff note, not an open obligation of this package." + } + ] +} diff --git a/research/f7-17point-cover-audit-seedcfa215c2/VERIFY.json b/research/f7-17point-cover-audit-seedcfa215c2/VERIFY.json new file mode 100644 index 0000000000..3da7dba48e --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/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": "Vendored engine byte pin; byte-exact reproduction of the pinned five/six-source censuses (945/31, 10395/49, 945945/59 with records SHA-256); full re-run of PR 2542's length-18 census against the vendored engine (15,775,992 nodes, 312,064 simple 18-cycles, zero universal words); the sharp 17-point row table with the min-excess census filter ((9,8)/(8,9) dead in the identity; (10,7)/(7,10) zero rows after e_ex >= 3; (11,6)/(6,11) exactly two rows (5,1),(6,0) after the completed k=11 census); the exact n=5 set-level controls (zero nine-point covers, max 29; 99,200 ten-point covers); receipt consistency of SIDON-RECEIPT.json including the complete k=11 walk (62/62 sub-shards, level3=0 level4=0). --full re-runs the four load-bearing zero-count census shards (~17 min)" + }, + { + "argv": ["{python}", "-I", "-B", "{package}/independent.py"], + "timeout_seconds": 240, + "checks": "Different-method cross-checks: excess-budget semantics against naive itertools brute force on the 16-element even subgroup at budgets 0/1/2; the sharp row table re-derived by direct count-vector loops (no partition generator); receipt example validity; mirror-row agreement" + }, + { + "argv": ["{python}", "-I", "-B", "{package}/test_engine.py"], + "timeout_seconds": 240, + "checks": "Unit tests: vendored engine byte-pin, PR 2542 row reproduction, the six-row 17-point split table, extremal profile c values, the (11,6) single-row-class reduction, the min-excess census consequences, the odd-translation mirror, dual-predicate coverage agreement, and the exact n=5 controls" + } + ] +} diff --git a/research/f7-17point-cover-audit-seedcfa215c2/cover17.py b/research/f7-17point-cover-audit-seedcfa215c2/cover17.py new file mode 100644 index 0000000000..5add3747a3 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/cover17.py @@ -0,0 +1,263 @@ +"""17-point cover audit engine: pair-representation identity, sharp rows, +coverage primitives and exact small controls. + +Object (KB3c, pair-collision object change recorded in TASK.json): the status +of PR 2542's claim "No 17-point set covers F2^7" against its own lemma table. +PR 2542's `lemma_a_table` (vendored byte-exact as vendor/pr2542_engine.py, +credit PR 2542, package research/universal-f7-singleton-seedb859517b) only +contradicts the (9,8)/(8,9) split rows; the counting-feasible 17-point splits +(10,7)/(7,10)/(11,6)/(6,11) survive it. This module extends the identity +with the sharp collision-multiplicity constraint and computes exactly which +(e_ex, b_ex, c) rows survive per split. + +Definitions. S = A u B with A = S int E (s points, even weight), B = S int O +(t points, odd weight), s + t = 17. A_x = #unordered pairs of A summing to +x, B_x likewise (x even nonzero). e_ex = C(s,2) - |supp(A)|, b_ex likewise. +Cross sums a+b (a in A, b in B) hit the odd masks with multiplicities r_o, so + + odd excess sum_o (r_o - 1) = s*t - 2^(n-1) =: E_o + colliding pairs sum_o C(r_o,2) = 2 * sum_x A_x B_x =: 2c + +with C(r,2) >= r-1 per mask. A collision profile is a partition of E_o into +j = r_o - 1 parts; it needs sigma = sum j(j+1)/2 = 2c even. A row (e_ex, +b_ex) is multiset-feasible for profile c iff c is exactly attainable as the +sum of shared products A_x B_x over the shared = C(s,2)+C(t,2)-e_ex-b_ex- +(2^(n-1)-1) support positions (multiplicity shapes from partitions of e_ex +resp. b_ex). This refines PR 2542's closed-form upper bound. +""" + +from functools import lru_cache + +VENDOR_PIN_PR2542 = ( + "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4" +) + + +# ------------------------------------------------------- counting bounds + + +def counting_ok(n, s, t): + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + return ( + s * t >= odd_masks + and s * (s - 1) // 2 + t * (t - 1) // 2 >= even_nonzero + ) + + +# ------------------------------------------- collision-multiplicity identity + + +def _partitions(total): + """Integer partitions of total as tuples (non-increasing).""" + if total == 0: + yield () + return + for part in range(total, 0, -1): + for rest in _partitions(total - part): + if not rest or rest[0] <= part: + yield (part,) + rest + + +def odd_profiles(excess): + """Collision profiles for odd excess `excess`: partitions j of it with + sigma = sum j(j+1)/2 even (= 2c for integer c). Each j is one odd mask + with r = j + 1 cross representations.""" + out = [] + for parts in _partitions(excess): + sigma = sum(j * (j + 1) // 2 for j in parts) + if sigma % 2 == 0: + out.append(sorted(parts)) + return sorted(out) + + +def profile_c_values(n, s, t): + """c = sum_x A_x B_x forced by each integer collision profile.""" + excess = s * t - (1 << (n - 1)) + if excess < 0: + return [] + return sorted( + {sum(j * (j + 1) // 2 for j in parts) // 2 for parts in odd_profiles(excess)} + ) + + +def _shapes(total_pairs, excess): + """Multiplicity shapes: A_x values summing to total_pairs with support + size total_pairs - excess (the excess parts carry the collisions).""" + if excess > total_pairs: + return + for parts in _partitions(excess): + yield tuple(sorted((1 + p for p in parts), reverse=True)) + ( + 1, + ) * (total_pairs - excess - len(parts)) + + +def _draws(shape, shared): + """All multisets of `shared` values drawn from a multiplicity shape.""" + if shared == 0: + yield () + return + counts = {} + for v in shape: + counts[v] = counts.get(v, 0) + 1 + vals = sorted(counts) + limits = [counts[v] for v in vals] + + def rec(i, remaining, acc): + if i == len(vals): + if remaining == 0: + yield tuple(acc) + return + for take in range(min(limits[i], remaining) + 1): + yield from rec(i + 1, remaining - take, acc + [vals[i]] * take) + + yield from rec(0, shared, []) + + +def _pairing_sums(a_draw, b_draw): + """All dot products sum a_i b_pi(i) over pairings of two draws.""" + if len(a_draw) <= 1: + yield sum(x * y for x, y in zip(a_draw, b_draw)) + return + a0 = a_draw[0] + for i in range(len(b_draw)): + rest = b_draw[:i] + b_draw[i + 1 :] + for tail in _pairing_sums(a_draw[1:], rest): + yield a0 * b_draw[i] + tail + + +def attainable_c(n, s, t, e_ex, b_ex): + """Exact attainable values of sum_x A_x B_x on the shared support + positions for one (e_ex, b_ex) row.""" + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + shared = A + B - e_ex - b_ex - even_nonzero + if shared < 0: + return set() + out = set() + for sa in _shapes(A, e_ex): + for sb in _shapes(B, b_ex): + for da in _draws(sa, shared): + for db in _draws(sb, shared): + out.update(_pairing_sums(da, db)) + return out + + +def sharp_rows(n, s, t): + """Sharp pair-representation rows for one parity split. + + Returns {feasible, rows: [{e_ex, b_ex, shared, c}], best, need}: a row + survives iff some integer collision profile's c is exactly attainable. + `best` is the largest attainable c (PR 2542's closed-form comparison + quantity), `need` = ceil((s*t - 2^(n-1))/2) the profile-level necessity. + """ + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + excess = s * t - odd_masks + need = (excess + 1) // 2 if excess > 0 else 0 + rows = [] + best = -1 + if excess < 0 or A + B < even_nonzero: + return dict(feasible=False, rows=[], best=best, need=need) + c_vals = set(profile_c_values(n, s, t)) + for e_ex in range(A + 1): + for b_ex in range(B + 1): + shared = A + B - e_ex - b_ex - even_nonzero + if shared < 0: + continue + attain = attainable_c(n, s, t, e_ex, b_ex) + if not attain: + continue + best = max(best, max(attain)) + for c in sorted(attain & c_vals): + rows.append(dict(e_ex=e_ex, b_ex=b_ex, shared=shared, c=c)) + return dict(feasible=bool(rows), rows=rows, best=best, need=need) + + +def surviving_rows(n, s, t, min_e_ex=0, min_b_ex=0): + """Sharp rows filtered by census-implied minimum excesses (min excess of + s-point sets resp. t-point sets in F2^(n-1)).""" + sharp = sharp_rows(n, s, t) + rows = [ + r + for r in sharp["rows"] + if r["e_ex"] >= min_e_ex and r["b_ex"] >= min_b_ex + ] + return dict( + feasible=bool(rows), + rows=rows, + best=sharp["best"], + need=sharp["need"], + ) + + +# ------------------------------------------------------ coverage primitives + + +def coverage_mask(pts): + """Bitmask of {a ^ b : a, b in pts} (self-pairs give mask 0).""" + mask = 1 # zero via a = b + for i in range(len(pts)): + pi = pts[i] + for j in range(i): + mask |= 1 << (pi ^ pts[j]) + return mask + + +def coverage_mask_dual(pts): + """Dual predicate (PR 2542's independent check): mask m is covered iff + (pts xor m) meets pts.""" + pset = set(pts) + limit = 1 << max(pts).bit_length() if pts else 1 + mask = 0 + for m in range(limit): + if any((p ^ m) in pset for p in pts): + mask |= 1 << m + return mask + + +# --------------------------------------------------- exact small controls + + +@lru_cache(maxsize=None) +def brute_force_set_census(n, k): + """Exact census of k-point sets S (0 in S, translation WLOG) over F2^n: + returns (number of covering sets, max |S+S|). Incremental DFS over + combinations with the pair-count upper-bound prune.""" + N = 1 << n + full_mask = (1 << N) - 1 + pairs_total = k * (k - 1) // 2 + state = {"covers": 0, "best": 0} + + sums = [0] + masks = [1] # stack of coverage masks + + def rec(next_pt, depth): + size = depth + 1 + if size == k: + mask = masks[-1] + covered = mask.bit_count() + if covered > state["best"]: + state["best"] = covered + if mask == full_mask: + state["covers"] += 1 + return + remaining_pairs = pairs_total - size * (size - 1) // 2 + if masks[-1].bit_count() + remaining_pairs < N: + return + for p in range(next_pt, N): + new = 1 << p + for q in sums: + new |= 1 << (p ^ q) + sums.append(p) + masks.append(masks[-1] | new) + rec(p + 1, depth + 1) + masks.pop() + sums.pop() + + rec(1, 0) + return state["covers"], state["best"] diff --git a/research/f7-17point-cover-audit-seedcfa215c2/independent.py b/research/f7-17point-cover-audit-seedcfa215c2/independent.py new file mode 100644 index 0000000000..daee07a886 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/independent.py @@ -0,0 +1,283 @@ +"""Independent re-derivation and controls for the 17-point cover audit. + +Deliberately different code paths from cover17.py / search17.py: + +1. Excess-budget semantics validated against naive itertools brute force on + the even subgroup of F2^7 isomorphic to F2^4 (16 elements), at budgets + 0, 1, 2. This is the semantics the load-bearing zero counts depend on. +2. The sharp row table re-derived by direct nested loops over excess pairs + and multiplicity distributions (no partition generator, no draw/pairing + recursion), matching cover17.sharp_rows row for row. +3. The odd-translation mirror: S+S is translation-invariant and an odd + translation swaps the E/O parts, so (s,t) and (t,s) rows must agree. +4. Receipt consistency: every recorded example is a valid set of the claimed + size/excess, and zero counts are only trusted with their controls. +""" + +import json +import sys +from itertools import combinations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import cover17 +import search17 + + +def excess_of(pts): + """Pair-sum excess: C(k,2) - |supp|.""" + supp = set() + k = len(pts) + for i, j in combinations(range(k), 2): + supp.add(pts[i] ^ pts[j]) + return k * (k - 1) // 2 - len(supp) + + +def small_group_budget_agreement(): + sub = [x for x in search17.EVEN if x < 32] # 16-element even subgroup + out = {} + for k in (4, 5, 6): + for budget in (0, 1, 2): + fast = sorted( + pts + for pts, _, _ in search17.enumerate_sets(sub, k, budget, fixed=(0,)) + ) + slow = sorted( + tuple(sorted(c)) + for c in combinations(sub, k) + if c[0] == 0 and excess_of(c) <= budget + ) + agree = fast == slow + out[f"k{k}_budget{budget}"] = { + "fast": len(fast), + "slow": len(slow), + "agree": agree, + } + assert agree, (k, budget) + # histogram path (used by the canonical-domain census) + hist, examples = search17.hist_sets(sub, k, budget, fixed=(0,)) + slow_hist = {} + for c in slow: + e = excess_of(c) + slow_hist[e] = slow_hist.get(e, 0) + 1 + assert hist == slow_hist, (k, budget, hist, slow_hist) + for e, pts in examples.items(): + assert excess_of(pts) == int(e), (k, budget, e) + out[f"k{k}_budget{budget}"]["hist_agree"] = True + return out + + +def sharp_rows_by_loops(n, s, t): + """Independent row derivation: loop over excess pairs directly and over + multiplicity distributions as explicit count vectors.""" + odd_masks = 1 << (n - 1) + even_nonzero = odd_masks - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + excess = s * t - odd_masks + if excess < 0 or A + B < even_nonzero: + return dict(feasible=False, rows=[], best=-1, need=0) + need = (excess + 1) // 2 + + # integer profiles: count vectors j1 >= j2 >= ... summing to excess, + # sigma = sum j(j+1)/2 even + prof_c = set() + + def profiles(remaining, cap, acc): + if remaining == 0: + sigma = sum(j * (j + 1) // 2 for j in acc) + if sigma % 2 == 0: + prof_c.add(sigma // 2) + return + for j in range(min(cap, remaining), 0, -1): + profiles(remaining - j, j, acc + [j]) + + profiles(excess, excess, []) + + rows = [] + best = -1 + 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 + # multiplicity distributions: value lists via count vectors + attain = attainable_by_counts(A, e_ex, B, b_ex, shared) + if not attain: + continue + best = max(best, max(attain)) + for c in sorted(attain & prof_c): + rows.append(dict(e_ex=e_ex, b_ex=b_ex, shared=shared, c=c)) + return dict(feasible=bool(rows), rows=rows, best=best, need=need) + + +def attainable_by_counts(A, e_ex, B, b_ex, shared): + """Attainable shared-product sums, enumerating count vectors for the + multiplicity distributions directly (distinct values only).""" + out = set() + + def dists(total_pairs, excess): + # count vectors (m1 >= m2 >= ... >= 1) with sum m = total_pairs - excess + # support and sum (m_i + collisions) = total_pairs: values v_i = m_i + # with sum v_i = total_pairs, len = total_pairs - excess + support = total_pairs - excess + if support < 0 or support > total_pairs: + return + # values v_1 >= v_2 >= ... >= v_support >= 1, sum = total_pairs + def rec(rem, cap, left, acc): + if left == 0: + if rem == 0: + yield tuple(acc) + return + for v in range(min(cap, rem - (left - 1)), 0, -1): + yield from rec(rem - v, v, left - 1, acc + [v]) + + yield from rec(total_pairs, total_pairs, support, []) + + for da in dists(A, e_ex): + for db in dists(B, b_ex): + for ca in combinations_with_replacement_positions(da, shared): + for cb in combinations_with_replacement_positions(db, shared): + for perm in permutations_multiset(cb): + out.add(sum(x * y for x, y in zip(ca, perm))) + return out + + +def combinations_with_replacement_positions(vals, shared): + """All multisets of size `shared` drawn from a non-increasing value list.""" + if shared == 0: + yield () + return + counts = {} + for v in vals: + counts[v] = counts.get(v, 0) + 1 + keys = sorted(counts) + + def rec(i, remaining, acc): + if i == len(keys): + if remaining == 0: + yield tuple(acc) + return + for take in range(min(counts[keys[i]], remaining) + 1): + yield from rec(i + 1, remaining - take, acc + [keys[i]] * take) + + yield from rec(0, shared, []) + + +def permutations_multiset(vals): + """All distinct permutations of a small multiset.""" + if len(vals) <= 1: + yield tuple(vals) + return + seen = set() + for i in range(len(vals)): + if vals[i] in seen: + continue + seen.add(vals[i]) + rest = vals[:i] + vals[i + 1 :] + for tail in permutations_multiset(rest): + yield (vals[i],) + tail + + +def receipt_consistency(): + receipt = json.loads((HERE / "SIDON-RECEIPT.json").read_text(encoding="utf-8")) + out = {} + for key, val in receipt.get("shard_e03", {}).items(): + count = val["count"] + first = val["first"] + ok = True + if first is not None: + ok = ( + 0 in first + and 3 in first + and len(set(first)) == len(first) + and all(p in search17.EVEN for p in first) + and excess_of(first) <= int(key.split("budget")[1]) + ) + out[key] = {"count": count, "first_valid": ok} + assert ok, (key, first) + for key, val in receipt.get("shard_o1", {}).items(): + count = val["count"] + first = val["first"] + ok = first is not None and 1 in first and all(p in search17.ODD for p in first) + out[key] = {"count": count, "first_valid": ok} + assert ok, (key, first) + # the completed k=11 raw walk: 62/62 sub-shards, empty histogram + k11 = receipt.get("k11_raw_budget4", {}) + prog = json.loads((HERE / "RAW11-PROGRESS.json").read_text(encoding="utf-8")) + ok = ( + k11.get("complete") is True + and k11.get("sub_shards") == 62 + and k11.get("total_hist") == {} + and prog.get("complete") is True + and prog.get("total_hist") == {} + and len(prog.get("shards", {})) == 62 + ) + assert ok, (k11, prog.get("complete"), len(prog.get("shards", {}))) + out["k11_raw_budget4"] = { + "complete": True, + "sub_shards": 62, + "level3": 0, + "level4": 0, + "progress_agrees": True, + } + # extension-collision floors on the recorded examples, consistent with + # the census floors: every one-point extension of the excess-3 10-set + # example adds >= 2 collisions (min 11-set excess >= 5); every extension + # of the Sidon 9-set example adds >= 3 (min 10-set excess >= 3). + ex10 = receipt["shard_e03"]["k10_budget3"]["first"] + supp10 = {ex10[i] ^ ex10[j] for i in range(10) for j in range(i)} + floors = [] + for p in search17.EVEN: + if p in ex10: + continue + coll = sum(1 for q in ex10 if (p ^ q) in supp10) + floors.append(coll) + assert min(floors) >= 2, min(floors) + ex9 = receipt["shard_e03"]["k9_budget0"]["first"] + supp9 = {ex9[i] ^ ex9[j] for i in range(9) for j in range(i)} + floors9 = [] + for p in search17.EVEN: + if p in ex9: + continue + coll = sum(1 for q in ex9 if (p ^ q) in supp9) + floors9.append(coll) + assert min(floors9) >= 3, min(floors9) + out["extension_floors"] = { + "excess3_10set_example_min_coll": min(floors), + "sidon9_example_min_coll": min(floors9), + } + return out + + +def main(): + report = {} + report["small_group_budget_agreement"] = small_group_budget_agreement() + for s, t in ((10, 7), (7, 10), (11, 6), (6, 11), (9, 8), (8, 9)): + loops = sharp_rows_by_loops(7, s, t) + engine = cover17.sharp_rows(7, s, t) + agree = ( + loops["feasible"] == engine["feasible"] + and {(r["e_ex"], r["b_ex"], r["c"]) for r in loops["rows"]} + == {(r["e_ex"], r["b_ex"], r["c"]) for r in engine["rows"]} + and loops["best"] == engine["best"] + and loops["need"] == engine["need"] + ) + report[f"rows_{s}_{t}"] = { + "agree": agree, + "feasible": engine["feasible"], + "row_count": len(engine["rows"]), + "best": engine["best"], + "need": engine["need"], + } + assert agree, (s, t) + report["receipt_consistency"] = receipt_consistency() + (HERE / "INDEPENDENT.json").write_text( + json.dumps(report, indent=2, sort_keys=True), encoding="utf-8" + ) + print("PASS_17POINT_INDEPENDENT " + json.dumps(report, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/f7-17point-cover-audit-seedcfa215c2/search17.py b/research/f7-17point-cover-audit-seedcfa215c2/search17.py new file mode 100644 index 0000000000..ef17635967 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/search17.py @@ -0,0 +1,330 @@ +"""Exact Sidon/near-Sidon census for the 17-point cover question (F2^7). + +Established here (receipt in SIDON-RECEIPT.json): + + * F2^6 has no Sidon 10-set. A complete DFS of all 10-subsets of the even + group E (= F2^6) containing {0, 3} finds none; Sidon-ness is translation- + invariant and GL(6,2)-invariant, and GL(6,2) is transitive on nonzero + elements, so one shard decides existence. Consequences (recorded in the + package README with the removal argument): every 10-point set has + pair-sum excess >= 1, every 11-point set has excess >= 2. This kills + the extremal (10,7) row of cover17.sharp_rows (e_ex = 0) and the (11,6) + rows e_ex in {0, 1}. + +Remaining exact search domains (row-restricted; the handoff object): + + rows (10,7): (e_ex, b_ex, c) in {(1,0,3), (1,1,4), (2,0,3)} + rows (11,6): (e_ex, b_ex, c) = (e, 6-e, 1) with e in {2,3,4,5,6} + +`enumerate_sets` is the enumeration primitive a row-restricted search builds +on (per-A constrained B-side DFS; the B side is far too large to enumerate +outright: ~3.1e8 Sidon 7-sets in the odd coset). Domain completeness for a +search: fix 0, 3 in A (GL(6,2) transitivity + stabilizer arguments, see +README); do NOT fix any element of B (the stabilizer extension fixes the +coset shift u and cannot move B's elements to it). Standard library only. +""" + +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +N = 128 +EVEN = [x for x in range(N) if x.bit_count() % 2 == 0] +ODD = [x for x in range(N) if x.bit_count() % 2 == 1] +EVEN_NZ = sum(1 << x for x in EVEN if x) # 63 even nonzero masks +ODD_ALL = sum(1 << x for x in ODD) # 64 odd masks +RECEIPT = HERE / "SIDON-RECEIPT.json" + + +# ------------------------------------------------------------ enumeration + + +def enumerate_sets(pool, k, budget, fixed=()): + """All k-subsets of `pool` containing `fixed`, of pair-sum excess + <= budget. Yields (pts, support_mask, mult) where mult maps each + supported even mask to its pair multiplicity A_x. Free elements are + chosen in increasing pool order, so each set is yielded once.""" + fixed = tuple(sorted(fixed)) + pts = list(fixed) + mult = {} + for i in range(len(pts)): + for j in range(i): + x = pts[i] ^ pts[j] + mult[x] = mult.get(x, 0) + 1 + supp = 0 + for x in mult: + supp |= 1 << x + excess = sum(mult.values()) - bin(supp).count("1") + + def rec(idx, supp, excess): + if len(pts) == k: + yield (tuple(pts), supp, dict(mult)) + return + need = k - len(pts) + for p in range(idx, len(pool) - need + 1): + v = pool[p] + if v in pts: + continue + new_sums = [v ^ q for q in pts] if pts else [] + add = 0 + coll = 0 + for x in new_sums: + if supp >> x & 1: + coll += 1 + else: + add |= 1 << x + new_excess = excess + coll + if new_excess > budget: + continue + for x in new_sums: + mult[x] = mult.get(x, 0) + 1 + pts.append(v) + yield from rec(p + 1, supp | add, new_excess) + pts.pop() + for x in new_sums: + mult[x] -= 1 + if mult[x] == 0: + del mult[x] + + yield from rec(0, supp, excess) + + +def count_sets(pool, k, budget, fixed=(), exclude=()): + """(count, first) for the same domain as enumerate_sets, without + materializing leaves (fast path for receipts).""" + fixed = tuple(sorted(fixed)) + pts = list(fixed) + supp = 0 + excess = 0 + for i in range(len(pts)): + for j in range(i): + x = pts[i] ^ pts[j] + if supp >> x & 1: + excess += 1 + else: + supp |= 1 << x + state = {"count": 0, "first": None} + + def rec(idx, supp, excess): + if len(pts) == k: + state["count"] += 1 + if state["first"] is None: + state["first"] = tuple(pts) + return + need = k - len(pts) + for p in range(idx, len(pool) - need + 1): + v = pool[p] + if v in pts: + continue + add = 0 + coll = 0 + for q in pts: + x = v ^ q + if supp >> x & 1: + coll += 1 + else: + add |= 1 << x + new_excess = excess + coll + if new_excess > budget: + continue + pts.append(v) + rec(p + 1, supp | add, new_excess) + pts.pop() + + rec(0, supp, excess) + return state["count"], state["first"] + + +def hist_sets(pool, k, budget, fixed=(), exclude=(), floor=None): + """Exact-excess histogram over the same domain: dict excess -> count, + plus one example per excess value. `floor` restricts free elements to + values > floor (sub-shard partition by the smallest free element).""" + fixed = tuple(sorted(fixed)) + excl = set(exclude) + pts = list(fixed) + supp = 0 + excess = 0 + for i in range(len(pts)): + for j in range(i): + x = pts[i] ^ pts[j] + if supp >> x & 1: + excess += 1 + else: + supp |= 1 << x + hist = {} + examples = {} + + def rec(idx, supp, excess): + if len(pts) == k: + hist[excess] = hist.get(excess, 0) + 1 + if str(excess) not in examples: + examples[str(excess)] = tuple(pts) + return + need = k - len(pts) + for p in range(idx, len(pool) - need + 1): + v = pool[p] + if v in pts or v in excl: + continue + if floor is not None and v <= floor: + continue + add = 0 + coll = 0 + for q in pts: + x = v ^ q + if supp >> x & 1: + coll += 1 + else: + add |= 1 << x + new_excess = excess + coll + if new_excess > budget: + continue + pts.append(v) + rec(p + 1, supp | add, new_excess) + pts.pop() + + rec(0, supp, excess) + return hist, examples + + +# --------------------------------------------------------------- receipt + + +def sidon_receipt(): + """The load-bearing exact counts. Shard = sets through {0, 3} in E + (complete for existence by GL(6,2) transitivity) and through {1} in O + (B-side feasibility/sizing only, not used for completeness).""" + out = {"shard_e03": {}, "shard_o1": {}} + for k, budget in ((10, 0), (9, 0), (10, 1)): + t1 = time.time() + n, first = count_sets(EVEN, k, budget, fixed=(0, 3)) + out["shard_e03"][f"k{k}_budget{budget}"] = { + "count": n, + "first": first, + "seconds": round(time.time() - t1, 1), + } + RECEIPT.write_text(json.dumps(out, indent=2, sort_keys=True), encoding="utf-8") + print(f"SIDON k={k} budget={budget} shard(0,3) n={n}", flush=True) + t1 = time.time() + n, first = count_sets(ODD, 7, 0, fixed=(1,)) + out["shard_o1"]["k7_budget0"] = { + "count": n, + "first": first, + "seconds": round(time.time() - t1, 1), + } + out["controls"] = { + "small_space_agreement": "enumerate_sets == naive brute force on the " + "even subgroup < 32: k=4 420/420, k=5 840/840, k=6 168/168" + } + RECEIPT.write_text(json.dumps(out, indent=2, sort_keys=True), encoding="utf-8") + print(f"SIDON k=7 budget=0 shard(1) odd n={n}", flush=True) + return out + + +def raw11_census(budget=4): + """Raw-domain census of 11-sets through {0, 3} with pair-sum excess + <= budget, counting by exact excess (the histogram yields the level-3 + and level-4 counts in one walk). Sub-sharded by the smallest free + element (disjoint, complete), resumable via RAW11-PROGRESS.json.""" + prog_path = HERE / "RAW11-PROGRESS.json" + prog = {"budget": budget, "shards": {}} + if prog_path.exists(): + old = json.loads(prog_path.read_text(encoding="utf-8")) + if old.get("budget") == budget: + prog = old + for v0 in EVEN: + if v0 in (0, 3): + continue + key = f"v0={v0}" + if key in prog["shards"]: + continue + t1 = time.time() + hist, examples = hist_sets( + EVEN, 11, budget, fixed=(0, 3, v0), floor=v0 + ) + prog["shards"][key] = { + "hist": {str(k): v for k, v in sorted(hist.items())}, + "examples": examples, + "seconds": round(time.time() - t1, 1), + } + prog_path.write_text( + json.dumps(prog, indent=2, sort_keys=True), encoding="utf-8" + ) + print(f"RAW11 {key} hist={hist} seconds={prog['shards'][key]['seconds']}", flush=True) + total = {} + for rec in prog["shards"].values(): + for e, n in rec["hist"].items(): + total[e] = total.get(e, 0) + n + prog["total_hist"] = {str(k): v for k, v in sorted(total.items())} + prog["complete"] = True + prog_path.write_text(json.dumps(prog, indent=2, sort_keys=True), encoding="utf-8") + print(f"RAW11 total_hist={prog['total_hist']}", flush=True) + return prog + + +def main(): + mode = sys.argv[1] if len(sys.argv) > 1 else "receipt" + if mode == "receipt": + sidon_receipt() + elif mode == "deeper": + # Follow-up census: decide whether excess 2 is attainable at all for + # 10-sets (kills the last (10,7) row (2,0,3) if not) and size the + # 11-set side (rows (11,6) with e_ex in {2, 3}). + out = {} + if RECEIPT.exists(): + out = json.loads(RECEIPT.read_text(encoding="utf-8")) + out.setdefault("shard_e03", {}) + for k, budget in ((10, 2), (11, 2)): + t1 = time.time() + n, first = count_sets(EVEN, k, budget, fixed=(0, 3)) + out["shard_e03"][f"k{k}_budget{budget}"] = { + "count": n, + "first": first, + "seconds": round(time.time() - t1, 1), + } + RECEIPT.write_text( + json.dumps(out, indent=2, sort_keys=True), encoding="utf-8" + ) + print(f"SIDON k={k} budget={budget} shard(0,3) n={n}", flush=True) + elif mode == "deeper2": + # Pin min excess(10) exactly and push the (11,6) A-side rows: + # k=11 budget b decides rows (e, 6-e, 1) with e = b. + out = {} + if RECEIPT.exists(): + out = json.loads(RECEIPT.read_text(encoding="utf-8")) + out.setdefault("shard_e03", {}) + for k, budget in ((10, 3), (11, 3), (11, 4)): + t1 = time.time() + n, first = count_sets(EVEN, k, budget, fixed=(0, 3)) + out["shard_e03"][f"k{k}_budget{budget}"] = { + "count": n, + "first": first, + "seconds": round(time.time() - t1, 1), + } + RECEIPT.write_text( + json.dumps(out, indent=2, sort_keys=True), encoding="utf-8" + ) + print(f"SIDON k={k} budget={budget} shard(0,3) n={n}", flush=True) + elif mode == "raw11": + prog = raw11_census() + if RECEIPT.exists(): + out = json.loads(RECEIPT.read_text(encoding="utf-8")) + else: + out = {} + out["k11_raw_budget4"] = { + "domain": "11-sets through {0,3} (complete by GL(6,2) " + "transitivity), sub-sharded by the smallest free element", + "total_hist": prog["total_hist"], + "sub_shards": len(prog["shards"]), + "complete": True, + } + RECEIPT.write_text(json.dumps(out, indent=2, sort_keys=True), encoding="utf-8") + else: + raise SystemExit(f"unknown mode {mode}") + + +if __name__ == "__main__": + main() diff --git a/research/f7-17point-cover-audit-seedcfa215c2/test_engine.py b/research/f7-17point-cover-audit-seedcfa215c2/test_engine.py new file mode 100644 index 0000000000..f50b290c11 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/test_engine.py @@ -0,0 +1,150 @@ +"""Tests for the 17-point cover audit engine (cover17.py). + +RED first: these assertions encode the sharp 17-point split table derived +in the CLAIM card (collision-multiplicity identity), and the exact small +controls (n = 5). They fail until cover17.py exists. +""" + +import sys +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +sys.path.insert(0, str(HERE / "vendor")) + +import cover17 +import hashlib + + +class TestVendoredEngine(unittest.TestCase): + def test_pr2542_engine_byte_pin(self): + digest = hashlib.sha256((HERE / "vendor" / "pr2542_engine.py").read_bytes()) + self.assertEqual( + digest.hexdigest(), + "82e4c407b58864c74ffd14d47f00b6b1675005ee0e0173909b7bd092491175e4", + ) + + +class TestSharpRows(unittest.TestCase): + """The pair-representation identity extended to every 17-point split.""" + + def test_pr2542_rows_reproduced(self): + # PR 2542's contradiction, re-derived: best_sum_AB=1 need=4. + for s, t in ((9, 8), (8, 9)): + rows = cover17.sharp_rows(7, s, t) + self.assertFalse(rows["feasible"], (s, t)) + self.assertEqual(rows["best"], 1, (s, t)) + self.assertEqual(rows["need"], 4, (s, t)) + + def test_17point_split_table(self): + feasible = { + (s, t): cover17.sharp_rows(7, s, t)["feasible"] + for s in range(1, 17) + for t in (17 - s,) + } + counted = {k: v for k, v in feasible.items() if v or k in ((9, 8), (8, 9))} + # Counting-feasible 17-point splits are exactly these six: + self.assertEqual( + sorted(k for k in feasible if cover17.counting_ok(7, *k)), + [(6, 11), (7, 10), (8, 9), (9, 8), (10, 7), (11, 6)], + ) + # PR 2542's table kills (9,8)/(8,9); the four others survive the + # closed-form identity (that is the recorded overreach). + self.assertTrue(feasible[(10, 7)]) + self.assertTrue(feasible[(7, 10)]) + self.assertTrue(feasible[(11, 6)]) + self.assertTrue(feasible[(6, 11)]) + self.assertFalse(feasible[(9, 8)]) + self.assertFalse(feasible[(8, 9)]) + + def test_extremal_107_profile(self): + # (10,7): odd excess 6; integer collision profiles force c in {3,4,5,6,8}. + self.assertEqual(cover17.profile_c_values(7, 10, 7), [3, 4, 5, 6, 8]) + self.assertEqual(cover17.profile_c_values(7, 7, 10), [3, 4, 5, 6, 8]) + # The extremal (e_ex=b_ex=0) row admits only c = 3 (six doubled masks). + self.assertEqual(cover17.attainable_c(7, 10, 7, 0, 0), {3}) + + def test_116_reduces_to_one_row(self): + # (11,6): odd excess 2 forces c = 1 and e_ex + b_ex = 6, shared = 1. + self.assertEqual(cover17.profile_c_values(7, 11, 6), [1]) + sharp = cover17.sharp_rows(7, 11, 6) + self.assertTrue(sharp["feasible"]) + self.assertEqual( + {(r["e_ex"], r["b_ex"], r["c"]) for r in sharp["rows"]}, + {(e, 6 - e, 1) for e in range(7)}, + ) + for r in sharp["rows"]: + self.assertEqual(r["shared"], 1) + + def test_min_excess_census_kills_107(self): + # Census (SIDON-RECEIPT.json): min pair-sum excess of 10-sets in F2^6 + # is >= 3 (k=10 budgets 0,1,2 all empty through {0,3}, GL-complete). + # With e_ex >= 3 the (10,7) rows all die: shared = 3 - e - b <= 0. + self.assertEqual(cover17.surviving_rows(7, 10, 7, 3, 0)["rows"], []) + self.assertEqual(cover17.surviving_rows(7, 7, 10, 0, 3)["rows"], []) + self.assertFalse(cover17.surviving_rows(7, 10, 7, 3, 0)["feasible"]) + + def test_min_excess_census_narrows_116(self): + # Census (SIDON-RECEIPT.json, raw {0,3} domain complete): min excess + # of 11-sets in F2^6 is >= 5 (k=11 budget-4 walk: zero leaves across + # all 62 sub-shards). The surviving (11,6) rows are then (5,1),(6,0). + rows = cover17.surviving_rows(7, 11, 6, 3, 0) + self.assertEqual( + {(r["e_ex"], r["b_ex"], r["c"]) for r in rows["rows"]}, + {(3, 3, 1), (4, 2, 1), (5, 1, 1), (6, 0, 1)}, + ) + rows = cover17.surviving_rows(7, 11, 6, 5, 0) + self.assertEqual( + {(r["e_ex"], r["b_ex"], r["c"]) for r in rows["rows"]}, + {(5, 1, 1), (6, 0, 1)}, + ) + + def test_odd_translation_mirror(self): + # S+S is translation-invariant; an odd translation swaps the E/O + # parts, so (s,t) and (t,s) are the same set-level question. + pts = [0, 3, 5, 9, 17, 30, 33, 65, 102, 21, 42] + shifted = [p ^ 1 for p in pts] + self.assertEqual(cover17.coverage_mask(pts), cover17.coverage_mask(shifted)) + even = sum(1 for p in pts if p.bit_count() % 2 == 0) + even_shifted = sum(1 for p in shifted if p.bit_count() % 2 == 0) + self.assertEqual(even, len(pts) - even_shifted) + + def test_odd_profile_parity(self): + # sigma = sum j(j+1)/2 must be even (= 2c); e.g. a single triple + # (j=2, sigma=3) can never absorb odd excess 2 at (11,6). + self.assertEqual(cover17.odd_profiles(2), [[1, 1]]) + + +class TestCoveragePrimitives(unittest.TestCase): + def test_dual_predicate_agrees(self): + pts = [0, 1, 3, 7, 15, 31, 32] + self.assertEqual( + cover17.coverage_mask(pts), cover17.coverage_mask_dual(pts) + ) + + def test_self_sum_gives_zero_only(self): + pts = [0, 5, 9] + mask = cover17.coverage_mask(pts) + self.assertTrue(mask & 1) # zero covered via a = b + self.assertEqual(bin(mask).count("1"), 4) # 0, 5, 9, 12 + + +class TestSmallControls(unittest.TestCase): + def test_n5_nine_point_no_cover_max29(self): + # Community fact reproduced by PR 2542's census: no nine-point set + # of F2^5 covers; the maximum is 29/32. + covers, max_cov = cover17.brute_force_set_census(5, 9) + self.assertEqual(covers, 0) + self.assertEqual(max_cov, 29) + + def test_n5_ten_point_covers_exist(self): + # Non-vacuity: 99,200 ten-point covers of F2^5 (pinned community + # census reproduced by PR 2542's control). + covers, max_cov = cover17.brute_force_set_census(5, 10) + self.assertEqual(covers, 99200) + self.assertEqual(max_cov, 32) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py b/research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_engine.py new file mode 100644 index 0000000000..210bd817b1 --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/vendor/pr2542_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/f7-17point-cover-audit-seedcfa215c2/verify.py b/research/f7-17point-cover-audit-seedcfa215c2/verify.py new file mode 100644 index 0000000000..79a3fe6e4f --- /dev/null +++ b/research/f7-17point-cover-audit-seedcfa215c2/verify.py @@ -0,0 +1,138 @@ +"""Reproduction and verification for the 17-point cover audit. + +Quick mode (< 600 s): vendored-engine byte pin, the pinned n = 5 / n = 6 +tier reproductions, the full PR 2542 length-18 census re-run against the +vendored engine, the sharp 17-point row table with the min-excess census +filter, the exact n = 5 set-level controls and the receipt consistency +checks. `--full` additionally re-runs the four load-bearing zero-count +census shards (~17 min) and compares them with SIDON-RECEIPT.json. + +Expected marker: PASS_17POINT_VERIFY ... +""" + +import hashlib +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +sys.path.insert(0, str(HERE / "vendor")) + +import cover17 +import pr2542_engine +import search17 + + +def main(): + t0 = time.time() + full = "--full" in sys.argv + + # 1. vendored engine byte pin (credit: PR 2542, Aaron Wang) + digest = hashlib.sha256((HERE / "vendor" / "pr2542_engine.py").read_bytes()) + assert digest.hexdigest() == cover17.VENDOR_PIN_PR2542, digest.hexdigest() + print(f"PIN vendor/pr2542_engine.py sha256={digest.hexdigest()[:16]}", flush=True) + + # 2. pinned tier reproductions (research/universal-connector-six-source) + pinned = json.loads( + (ROOT / "research" / "universal-connector-six-source" / "EXPECTED.json").read_text( + encoding="utf-8" + ) + ) + by_key = {(c["sources"], c["length"]): c for c in pinned["censuses"]} + for n, L in ((5, 10), (6, 12), (6, 14)): + hist, sha, words = pr2542_engine.census_words(n, L) + exp = by_key[(n, L)] + assert words == exp["words"], (n, L, words) + assert max(k for k, v in hist.items() if v) == exp["max_coverage"], (n, L) + assert sha == exp["records_sha256"], (n, L, sha) + print( + f"REPRO n={n} L={L} words={words} max={exp['max_coverage']}" + f" sha={sha[:16]}", + flush=True, + ) + + # 3. PR 2542's decisive length-18 census, re-run shard by shard against + # the vendored engine (shard nodes sum with the +10 shard overhead). + tot = {"nodes": 0, "leaves": 0, "hits": 0} + for pref in pr2542_engine.rg_prefixes(7, 3): + rr = pr2542_engine.cyclic_census(7, 18, budget=9, simple=True, prefix=pref) + tot["nodes"] += rr["nodes"] + tot["leaves"] += rr["leaves"] + tot["hits"] += rr["hits"] + assert tot == {"nodes": 15775992, "leaves": 312064, "hits": 0}, tot + print( + f"REPRO PR2542 L18 nodes={tot['nodes']} cycles={tot['leaves']}" + f" universal_words={tot['hits']}", + flush=True, + ) + + # 4. sharp 17-point row table with the min-excess census filter + # (10-set floor e_ex >= 3; 11-set floor e_ex >= 5, both raw-domain + # complete by GL(6,2) transitivity) + table = {} + for s, t in ((9, 8), (8, 9), (10, 7), (7, 10), (11, 6), (6, 11)): + sharp = cover17.sharp_rows(7, s, t) + if (s, t) in ((10, 7), (7, 10)): + filt = cover17.surviving_rows(7, s, t, 3, 0) if s >= t else cover17.surviving_rows(7, s, t, 0, 3) + else: + filt = cover17.surviving_rows(7, s, t, 5, 0) if s >= t else cover17.surviving_rows(7, s, t, 0, 5) + table[f"{s}_{t}"] = { + "sharp_feasible": sharp["feasible"], + "rows_after_min_excess": len(filt["rows"]), + } + assert table["9_8"]["sharp_feasible"] is False + assert table["8_9"]["sharp_feasible"] is False + assert table["10_7"]["rows_after_min_excess"] == 0 + assert table["7_10"]["rows_after_min_excess"] == 0 + assert table["11_6"]["rows_after_min_excess"] == 2 + assert table["6_11"]["rows_after_min_excess"] == 2 + print("ROWS17 " + json.dumps(table, sort_keys=True), flush=True) + + # 5. exact n = 5 set-level controls (community facts) + covers9, best9 = cover17.brute_force_set_census(5, 9) + covers10, best10 = cover17.brute_force_set_census(5, 10) + assert (covers9, best9) == (0, 29), (covers9, best9) + assert (covers10, best10) == (99200, 32), (covers10, best10) + print( + f"CONTROL n5 k=9 covers={covers9} max={best9} k=10 covers={covers10}" + f" max={best10}", + flush=True, + ) + + # 6. receipt consistency (examples valid, counts recorded) + receipt = json.loads((HERE / "SIDON-RECEIPT.json").read_text(encoding="utf-8")) + zeros = sorted( + k for k, v in receipt["shard_e03"].items() if v["count"] == 0 + ) + assert "k10_budget2" in zeros and "k11_budget2" in zeros, zeros + print(f"RECEIPT zeros={zeros} k9={receipt['shard_e03']['k9_budget0']['count']}", flush=True) + k11 = receipt["k11_raw_budget4"] + assert k11["complete"] is True and k11["sub_shards"] == 62, k11 + assert k11["total_hist"] == {}, k11["total_hist"] + prog11 = json.loads((HERE / "RAW11-PROGRESS.json").read_text(encoding="utf-8")) + assert prog11["complete"] is True and prog11["total_hist"] == {} + print( + "K11 census complete: 62/62 sub-shards, level3=0 level4=0" + " (zero 11-sets of excess <= 4 through {0,3})", + flush=True, + ) + + if full: + for key, k, budget in ( + ("k10_budget0", 10, 0), + ("k10_budget1", 10, 1), + ("k10_budget2", 10, 2), + ("k11_budget2", 11, 2), + ): + n, first = search17.count_sets(search17.EVEN, k, budget, fixed=(0, 3)) + assert n == receipt["shard_e03"][key]["count"], (key, n) + print(f"FULL {key} n={n} matches receipt", flush=True) + + print(f"PASS_17POINT_VERIFY seconds={time.time() - t0:.1f} full={full}") + + +if __name__ == "__main__": + main()