KB3d: (11,6)/(6,11) remainder rows (5,1),(6,0) of the 17-point cover question impossible by an exact Fourier/Parseval identity (no new kappa)

research/f7-17point-fourier-obstruction-seedb5e318fe/ANCHOR-REPRO.json

@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "recorded_utc": "2026-10-16T00:40:00Z",
+  "environment": "CPython 3.12.13 (C:/Users/warha/.local/bin/python3.12.exe), Windows, stdlib only",
+  "predecessor_package": "research/f7-17point-cover-audit-seedcfa215c2 (PR 2773, head 6739c799799621878a9249c93e2b12cc799c1482 at extraction), extracted byte-exactly with agent_tools.py pr-tree-extract",
+  "commands_run_in_session": [
+    "python3.12 -I -B research/f7-17point-cover-audit-seedcfa215c2/verify.py",
+    "python3.12 -I -B research/f7-17point-cover-audit-seedcfa215c2/verify.py --full",
+    "python3.12 -I -B research/f7-17point-cover-audit-seedcfa215c2/test_engine.py",
+    "python3.12 -I -B research/f7-17point-cover-audit-seedcfa215c2/independent.py",
+    "python3.12 -I -B research/f7-17point-fourier-obstruction-seedb5e318fe/anchors.py k10b3 --seconds 900",
+    "python3.12 -I -B research/f7-17point-fourier-obstruction-seedb5e318fe/anchors.py k11b4 --seconds 900"
+  ],
+  "observed_outputs": {
+    "tiers_and_l18": "REPRO n=5 L=10 words=945 max=31 sha=3dcc5689a4a34bae; REPRO n=6 L=12 words=10395 max=49 sha=491b295f12cfa34a; REPRO n=6 L=14 words=945945 max=59 sha=3d711ffa19209310; REPRO PR2542 L18 nodes=15775992 cycles=312064 universal_words=0",
+    "row_table": "ROWS17 11_6 and 6_11 rows_after_min_excess=2 (the (5,1),(6,0) remainder); 10_7/7_10 rows_after_min_excess=0; 9_8/8_9 sharp_feasible=false",
+    "controls": "CONTROL n5 k=9 covers=0 max=29 k=10 covers=99200 max=32",
+    "receipt_consistency": "RECEIPT zeros=['k10_budget0','k10_budget1','k10_budget2','k11_budget2'] k9=17776640; K11 census complete: 62/62 sub-shards, level3=0 level4=0 (zero 11-sets of excess <= 4 through {0,3})",
+    "full_zero_shards": "FULL k10_budget0 n=0 matches receipt; FULL k10_budget1 n=0 matches receipt; FULL k10_budget2 n=0 matches receipt; FULL k11_budget2 n=0 matches receipt; PASS_17POINT_VERIFY seconds=909.6 full=True",
+    "predecessor_tests": "Ran 13 tests in 27.410s ... OK",
+    "predecessor_independent": "PASS_17POINT_INDEPENDENT {receipt_consistency: k10_budget3 count=149990400 first_valid=true, k11_raw_budget4 complete=true level3=0 level4=0 progress_agrees=true sub_shards=62, k9_budget0=17776640 first_valid=true, ...; rows agree on all six splits; small_group_budget_agreement 420/840/168 agree}"
+  },
+  "anchor_recomputation": {
+    "method": "Established PR 2773 raw-domain walk on the vendored engine (vendor/agent64_search17.py, byte-pinned): complete GL(6,2)-transitive domain through {0,3}, sub-shards by the smallest free element, per-sub-shard receipts in ANCHOR-PROGRESS.json, blocking foreground invocations with PYTHONUNBUFFERED=1 (anchors.py, CPython 3.12).",
+    "k10_budget3": "PASS_ANCHORS_K10B3 count=149990400 total_hist={'3': 149990400} shards=62 -- matches the recorded anchor 149,990,400 exactly; every leaf is at exact pair-sum excess 3.",
+    "k11_levels34": "PASS_ANCHORS_K11B4 count=0 total_hist={} shards=62 -- zero 11-sets of pair-sum excess <= 4 through {0,3}; recorded levels 3 and 4 both reproduced as 0."
+  },
+  "recorded_anchor_values": {
+    "k10_budget3": 149990400,
+    "k11_level3": 0,
+    "k11_level4": 0,
+    "l18_nodes": 15775992,
+    "l18_cycles": 312064,
+    "l18_universal": 0,
+    "tier_n5_l10": [945, 31],
+    "tier_n6_l12": [10395, 49],
+    "tier_n6_l14": [945945, 59]
+  },
+  "status": "ANCHOR STATUS: ALL recorded predecessor anchors were reproduced in this session. RECOMPUTED byte-exactly against the vendored engines: the PR 2542/2634 REPRO tiers (945/31, 10395/49, 945945/59 with records SHA-256), the PR 2542 length-18 census (15,775,992 nodes, 312,064 cycles, zero universal), the row table and the n=5 set controls; the four load-bearing zero shards (k10 budgets 0/1/2, k11 budget 2) recomputed by verify.py --full and matching the PR 2773 receipt. RECOMPUTED IN FULL by the resumable sub-shard walk (anchors.py, per-shard receipts in ANCHOR-PROGRESS.json): the k=10 budget-3 count (PASS_ANCHORS_K10B3 count=149990400, 62/62 sub-shards) and the k=11 excess <= 4 walk (PASS_ANCHORS_K11B4 count=0, 62/62 sub-shards; levels 3 and 4 both 0). None of these anchors is load-bearing for the KB3d verdict: the (5,1),(6,0) rows are excluded by the exact Fourier/Parseval identity in fourier17.py, which uses only exact integer arithmetic and is reproduced by test_engine.py and independent.py."
+}

research/f7-17point-fourier-obstruction-seedb5e318fe/CERTIFICATE.json

@@ -0,0 +1,52 @@
+{
+  "schema_version": 1,
+  "result": "KB3d set-level verdict: the two remaining rows (5,1),(6,0) of the (11,6)/(6,11) family of PR 2542's 17-point cover question are impossible; the whole (11,6)/(6,11) family is excluded, and with PR 2542 and PR 2773 no 17-point set covers F2^7 (set level, no words enumerated).",
+  "labels": [
+    {
+      "statement": "For A in the even coset and B in the odd coset of F2^7 with |A| = 11, |B| = 6 (either order), the 66 cross sums cannot cover all 64 odd masks: with rho = r - 1_O (r = 1_A * 1_B) of total 2, the even-cardinality side's characters are {0, +2, -2} off {0, all-ones}, but Parseval gives a remainder of 696 over 126 squares of at most 4 (696 > 504, deficit 192).",
+      "label": "PROVEN",
+      "evidence": "fourier17.obstruction (exact integer arithmetic), test_engine.py 13 tests, independent.py second path (FWHT + Parseval double counting + exhaustive rho-hat control over all 2,080 total-2 shapes + exhaustive F2^3 identity over 65,536 set pairs)."
+    },
+    {
+      "statement": "Rows (5,1) and (6,0) of the (11,6)/(6,11) family (the whole recorded remainder of PR 2773, pair-sum excess 5 and 6 at 11 points, shared = 1, c = 1) are impossible; hence no 17-point set of split (11,6)/(6,11) covers F2^7 and at L = 22 every universal word needs at least 18 distinct prefixes.",
+      "label": "PROVEN",
+      "evidence": "The obstruction above covers every row of the family (it does not use the even half of the covering condition); the remainder rows themselves are reproduced from the vendored PR 2773 row engine (sharp_rows(7,11,6) filtered by the recorded k=11 floor e_ex >= 5 gives exactly (5,1),(6,0))."
+    },
+    {
+      "statement": "The literal claim 'No 17-point set covers F2^7' is complete at the set level.",
+      "label": "PROVEN",
+      "evidence": "Jointly with PR 2542 ((9,8)/(8,9) dead in the pair-representation identity) and PR 2773 ((10,7)/(7,10) excluded exactly against the census floor; (3,3),(4,2) demoted by the completed k=11 census), plus this package's exclusion of (5,1),(6,0) and therefore of the whole (11,6)/(6,11) family. All six counting-feasible splits are now excluded."
+    },
+    {
+      "statement": "The recorded predecessor anchors of PR 2542/2634/2773 are reproduced (REPRO tiers 945/31, 10395/49, 945945/59; length-18 census 15,775,992 nodes / 312,064 cycles / 0 universal; row table; n=5 set controls; the four zero shards recomputed against the PR 2773 receipt; and the two heavy anchors recomputed in full: PASS_ANCHORS_K10B3 count=149990400, PASS_ANCHORS_K11B4 count=0).",
+      "label": "CHECKED",
+      "evidence": "In-session runs of the predecessor packages' own verify.py / verify.py --full / test_engine.py / independent.py against byte-exact extractions, plus the resumable anchors.py sub-shard walk on the vendored engine (62/62 sub-shards each, per-shard receipts in ANCHOR-PROGRESS.json); commands and observed outputs in ANCHOR-REPRO.json."
+    },
+    {
+      "statement": "The Fourier route alone does not exclude the other four 17-point splits, and it does not reach the 18/19-point splits (E_o >= 8 there).",
+      "label": "CHECKED",
+      "evidence": "obstruction(7,10,7)/(7,7,10)/(7,9,8)/(7,8,9) all report contradiction = false (non-vacuity control in test_engine.py and verify.py); a real 10-point cover of F2^5 passes every check (positive control)."
+    },
+    {
+      "statement": "Constructing an 11-set of pair-sum excess 5 or 6 covering F2^7 is refuted: no such covering set exists in the (11,6)/(6,11) family.",
+      "label": "DEMOTED",
+      "evidence": "Follows from the PROVEN obstruction; the planned row-restricted joint (A,B) fallback search was not needed and is not run."
+    }
+  ],
+  "obstruction_numbers": {
+    "n": 7,
+    "split_orders": [[11, 6], [6, 11]],
+    "odd_excess": 2,
+    "character_values": [-2, 0, 2],
+    "parseval_remainder": 696,
+    "max_allowed": 504,
+    "deficit": 192
+  },
+  "reproduce": [
+    "python3 -I -B research/f7-17point-fourier-obstruction-seedb5e318fe/test_engine.py",
+    "python3 -I -B research/f7-17point-fourier-obstruction-seedb5e318fe/independent.py",
+    "python3 -I -B research/f7-17point-fourier-obstruction-seedb5e318fe/verify.py"
+  ],
+  "kappa_change": null,
+  "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+}

research/f7-17point-fourier-obstruction-seedb5e318fe/NOTICE.md

@@ -0,0 +1,32 @@
+# NOTICE — attribution and licenses
+
+Contributor: **Aaron Wang**, with help from opencode (substantial AI assistance
+in scoping, implementation, verification and writing; no model named; no
+independent human review claimed). Apache-2.0; all source licenses and notices
+are retained.
+
+Predecessor credit (authors verified against current ground truth with
+`gh pr view NNN --json author,title` at writing time):
+
+- [PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542) by Aaron
+  Wang (navinor): the audited claim "No 17-point set covers `F2^7`", the
+  pair-representation identity and the length-18 exclusion.
+- [PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773) by Aaron
+  Wang (navinor): the 17-point cover audit, the sharp collision-multiplicity
+  rows, the Sidon/near-Sidon census floors and the exact remainder rows
+  `(5,1),(6,0)` this package decides. Its `cover17.py` and `search17.py` are
+  vendored byte-exact under `vendor/` (SHA-256 pins enforced by
+  `test_engine.py`), copied with `agent_tools.py pr-tree-extract`, never
+  imported from the predecessor package.
+- [PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634) by Aaron
+  Wang (navinor): the recorded KB3b state (REPRO tiers, L=20 campaign and
+  census) reproduced here before new work.
+- [PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) by
+  Nicholas Stone (NicholasStone, Kimi agent): the completed `(10,10)`
+  simple-20-cycle census (recorded state, not re-run).
+- [PR 943](https://github.com/CrocSwap/integer-mult-bounds/pull/943) by Ross
+  Richardson (RossRichardson): the prefix-walk model (`S + S = F2^n`
+  covering condition).
+- [PR 1185](https://github.com/CrocSwap/integer-mult-bounds/pull/1185) by Doug
+  Colkitt (Mister-Meeseeks): the pinned record `f(5) = 12`, `f(6) = 16` and the
+  `f(7)` gap, plus the frozen tier `EXPECTED.json` reproduced here.