KB3c: 17-point cover audit - PR 2542's 'no 17-point set covers F2^7' against its own lemma table (no new kappa)

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
+}

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).

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
+    }
+  }
+}

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).