KB3i: the 18-point cover remainder for F2^7 - parity shortcut DEMOTED, m=5 obstruction localized (outcome=partial, no new kappa)

research/f7-18point-remainder-kb3i-a1/CERTIFICATE.json

@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "object": "the 18-point cover question for F2^7 (P + P = F2^7 in the PR 943 prefix-walk model); the recorded remainder of PR 3023: splits (12,6) A-vanish (4,2)/(3,3) and the both-odd splits (11,7)/(9,9)",
+  "outcome": "partial (narrowed remainder; no class decided; no false kill)",
+  "labels": {
+    "PROVEN": "established by complete exact enumeration or a validated identity; a zero count over a complete enumeration proves emptiness",
+    "CHECKED": "reproduced against pinned predecessor numbers or a bounded complete census",
+    "DEMOTED": "a proposed route/hypothesis refuted or shown not to lift; a negative about the method, not about the object"
+  },
+  "claims": [
+    {
+      "id": "anchors-reproduced",
+      "label": "CHECKED",
+      "statement": "All recorded anchors reproduce before any new number.",
+      "evidence": {
+        "PR2870_OBSTRUCTION": "parseval=696 allowed=504 deficit=192 (recomputed live)",
+        "PR2911_ROWS18": "808/501/251/196 (recomputed live)",
+        "PR2911_NOVANISH": "(12,6),(10,8) infeasible (recomputed live)",
+        "PR2933_CLASSIFY": "tight-equality Sidon m=3 cases=6720 ok=true; 32=32 TIGHT count=2 (recomputed live)",
+        "PR2961_FOURIER_71": "need=175 lower=239 contradiction=True (recomputed live)",
+        "PR2961_CLASS82": "checked=28815360 covering=0 (read back from PR 3023 receipts)",
+        "PR2961_CLASS60": "d_checked=169911 d_with_transversals=0 (read back from PR 3023 receipts)",
+        "PR3023_AV51": "u_checked=169911 uv_pairs=3049492320 covering_configs=0 (read back from PR 3023 receipts)"
+      }
+    },
+    {
+      "id": "parity-shortcut-demoted",
+      "label": "PROVEN (negative on the method)",
+      "statement": "The hypothesis 'a covering reduced pair (A,B) of F2^m must have |A|,|B| both even' is FALSE; both-odd reduced covers exist. Therefore no dimension-free parity rule can exclude the both-odd splits (11,7)/(9,9).",
+      "evidence": "Complete m=3 reduced-covering census (all 2^8 x 2^8 subset pairs): both-odd splits (3,5),(3,7),(5,3),(5,5),(5,7),(7,3),(7,5),(7,7) all admit covers; (5,5) has 3136 covers, (7,7) has 64. Only (3,3) among small both-odd splits is empty.",
+      "scope": "Negative about the parity-kill METHOD, not about (11,7)/(9,9) themselves (which remain undecided/unexcluded)."
+    },
+    {
+      "id": "m5-ground-truth",
+      "label": "CHECKED (complete census)",
+      "statement": "The m=5 ground truth (reduced problem in F2^4 with |A|+|B|=10) has covers only in the both-even splits (2,8),(4,6),(6,4),(8,2); the both-odd sum-10 splits (1,9),(3,7),(5,5) are empty.",
+      "evidence": "Complete m=4 sum-10 split censuses: (2,8) covers=15360, (4,6) covers=143360, (1,9) covers=0, (3,7) covers=0, (5,5) covers=0.",
+      "obstruction_localization": {
+        "(1,9)": "counting: st = 9 < 16 = |F2^4|, so A+B never covers (cross_covering=0; self covers for all 183040 pairs)",
+        "(3,7)": "cross never covers: st = 21 >= 16 but A+B != F2^4 for every pair (cross_covering=0)",
+        "(5,5)": "self never covers when cross covers: 4085760 cross-covering pairs, self_covering_when_cross=0, |A+A|,|B+B| in {8,11}, max self-union 15/16"
+      }
+    },
+    {
+      "id": "m5-obstruction-not-lifted",
+      "label": "DEMOTED",
+      "statement": "The m=5 even-only obstruction does not lift as a parity or self-sum-size rule to (11,7)/(9,9) at m=6.",
+      "evidence": "Both-odd covers exist at m=3 (parity-shortcut-demoted) and the (5,5) self-sum bound (|A+A| <= 11) is scale-dependent (both-odd (5,5) covers at m=3). No valid invariant forbidding a both-odd self cover at m=6 is established; (11,7)/(9,9) remain unexcluded.",
+      "scope": "Negative about the LIFT, not about (11,7)/(9,9)."
+    },
+    {
+      "id": "frontier-pinned",
+      "label": "CHECKED",
+      "statement": "The exact rho^2/identity frontier for (11,7)/(9,9) is reproduced and pinned.",
+      "evidence": {
+        "(11,7)": "odd excess E_o = 11*7 - 64 = 13; even_half_max = 42; partition min sum rho^2 = 13; effective min 17 after PR 2961 excludes the all-ones and (2,1^11) patterns; PR 2870 squeeze opposite-parity hypothesis inapplicable (s+t even)",
+        "(9,9)": "odd excess E_o = 9*9 - 64 = 17; even_half_max = 34; partition min sum rho^2 = 17; effective min 19 after the all-ones pattern is excluded; squeeze inapplicable"
+      }
+    },
+    {
+      "id": "construction-search-failure",
+      "label": "CHECKED (scoped search failure, not an exclusion)",
+      "statement": "Bounded seeded construction search finds no covering 18-set; the search ceiling is unchanged.",
+      "evidence": "search_direct k=18 on F2^7 (3 seeds): best 118/128 (record ceiling 119/128, PR 2634). Reduced split searches: (12,6),(11,7),(10,8) reach 118/128, (9,9) 117/128. No cover reached."
+    },
+    {
+      "id": "classes-undecided",
+      "label": "NOT DECIDED (recorded, honest partial)",
+      "statement": "(4,2), (3,3), (11,7), (9,9) are all undecided here; nothing in this package excludes any of them.",
+      "evidence": "(4,2): exact reduction D1={0,1} under GL(5,2), budgets 20/20/24 (PR 3023 classification, reproduced), walk strictly larger than (5,1)'s 3,049,492,320-pair walk and too large for the session. (3,3): four L3 lines direct, all budgets slack (line IV 36+9 vs 32), no forced structure. (11,7)/(9,9): parity shortcut DEMOTED, remain at the rho^2/identity frontier."
+    }
+  ],
+  "arithmetic": "Exact Python integer arithmetic (int bitmasks); no floats anywhere. Census counts are complete enumerations. Search results are bounded/seeded and never claimed as exclusions.",
+  "reproduce": "python3 -I -B research/f7-18point-remainder-kb3i-a1/verify.py quick|full|search"
+}

research/f7-18point-remainder-kb3i-a1/NOTICE.md

@@ -0,0 +1,36 @@
+# NOTICE — third-party and predecessor attribution
+
+This package (`research/f7-18point-remainder-kb3i-a1`) is a set-level research
+contribution by **Aaron Wang**, with help from opencode (substantial AI
+assistance; no model named; no independent human review claimed). Apache-2.0.
+
+## Vendored engines (byte-exact, SHA-256 pinned in `verify.py`)
+
+The six files under `vendor/` are copied byte-for-byte from the predecessor
+research packages and are credited to their authors. They are re-verified by
+`verify.py check_pins` on every run.
+
+| File | sha256 (prefix) | Source PR | Author | Contents |
+|---|---|---|---|---|
+| `vendor/tight.py` | `14670ef2…` | [PR 2961](https://github.com/CrocSwap/integer-mult-bounds/pull/2961) | Aaron Wang (navinor) | bitmask primitives, the (7,1) Fourier identity, rho classification |
+| `vendor/cover18.py` | `24c6a2f4…` | [PR 2961](https://github.com/CrocSwap/integer-mult-bounds/pull/2961) | Aaron Wang (navinor) | reduced (A,D) covering model, Fourier profile system, squeeze numbers, pair-representation rows, bounded search |
+| `vendor/vanish.py` | `6c605c54…` | [PR 2961](https://github.com/CrocSwap/integer-mult-bounds/pull/2961) | Aaron Wang (navinor) | vanishing-character class tables, L7 Sidon tight-equality lemma |
+| `vendor/agent64_cover17.py` | `082bc838…` | [PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773) | Aaron Wang (navinor) | profile_c_values (pair-representation shape primitives) |
+| `vendor/agent64_search17.py` | `9eb1bf79…` | [PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773) | Aaron Wang (navinor) | 17-point search primitives |
+| `vendor/anchors.py` | `73d73a9b…` | [PR 2961](https://github.com/CrocSwap/integer-mult-bounds/pull/2961) | Aaron Wang (navinor) | anchor-reproduction helpers |
+
+The engines were extracted with `agent_tools.py pr-tree-extract` from the
+immediate predecessor [PR 3023](https://github.com/CrocSwap/integer-mult-bounds/pull/3023)
+(Aaron Wang), which itself vendored them from PR 2961/PR 2773 with the same
+pins. This package never imports them from a predecessor tree at run time; the
+copies are local and pinned.
+
+## Model and predecessor credit
+
+- **PR 943** (Ross Richardson): the prefix-walk model (`research/universal-connector-boundary`), in which a restored seven-source singleton word is universal exactly when its prefix set `P` covers `P + P = F2^7`.
+- **PR 1185** (Mister-Meeseeks, per current ground truth): the pinned `f(5) = 12`, `f(6) = 16` record (`research/universal-connector-six-source`).
+- **PR 2542 / 2634 / 2773 / 2870 / 2911 / 2933 / 2961 / 3023** (Aaron Wang): the 17-point exclusion chain, the KB3b search ceilings (`119/128` at `k=18`, `124/128` at `k=19`), the pair-representation rows, the odd-coverage Fourier/Parseval identity, the `(A,D)` reduction and vanishing-character restriction, the class floors, the tight-class decisions, and the `(5,1)` decision whose recorded remainder ((4,2)/(3,3)/(11,7)/(9,9)) this package takes.
+- **PR 2691 / 2973** (Nicholas Stone, NicholasStone) and **PR 3005** (Nick Petalas, petalas): the word-level census line and its false-prune correction (`22 <= f(7) <= 24`, corroborated). PR 2973's scope note explicitly leaves the set-level chain PR 2773-3023 unaffected. This package is set-level only and enumerates no words.
+
+Every cited PR author was verified against current ground truth with
+`gh pr view NNN --json author,title` at writing.