KB3e: the 18-point cover question for F2^7 narrowed to an exact finite remainder (outcome=partial, no new kappa)

research/f7-18point-cover-question-seed6d34356c/ANCHOR-REPRO.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "recorded_utc": "2026-10-16T10:05:00Z",
+  "environment": "CPython 3.12.13 (C:/Users/warha/.local/bin/python3.12.exe), Windows, stdlib only; concurrent research agents on the host, so wall times are inflated versus PR 2870's receipt timings",
+  "predecessor_packages_extracted": "PR 2542 research/universal-f7-singleton-seedb859517b (head 3b6011d2400f50ab0ad9e105c7c55a18f3cef4cf), PR 2634 research/universal-f7-singleton-l20-seed06704c39 (head e2f30d93efbef5658334072aa855aa95e795e394), PR 2773 research/f7-17point-cover-audit-seedcfa215c2 (head 6739c799799621878a9249c93e2b12cc799c1482), PR 2870 research/f7-17point-fourier-obstruction-seedb5e318fe (head 9f55f291e9e79e628fd98f1e4f4debfc1c2106e5); all extracted byte-exactly with agent_tools.py pr-tree-extract into a temp scratch area and run from there against a byte-identical copy of the pinned research/universal-connector-six-source/EXPECTED.json (SHA-256 f1b1bec330640c81ac0da25ee8b3a0a49fe9ea5bb2eadaaa787c64bd62c9e73a)",
+  "commands_run_in_session": [
+    "python3.12 -I -B <pred>/pr2773/verify.py",
+    "python3.12 -I -B <pred>/pr2773/independent.py",
+    "python3.12 -I -B <pred>/pr2870/test_engine.py",
+    "python3.12 -I -B <pred>/pr2870/verify.py",
+    "python3.12 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k10b3 --seconds 520 (repeated; resumable)",
+    "python3.12 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k11b4 --seconds 520 (repeated; resumable)"
+  ],
+  "observed_outputs": {
+    "tiers_and_l18": "PIN vendor/pr2542_engine.py sha256=82e4c407b58864c7; 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 (fresh re-run of the vendored PR 2542 engine inside PR 2773's verify.py)",
+    "row_table": "ROWS17 11_6/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 zeros=['k10_budget0','k10_budget1','k10_budget2','k11_budget2'] k9=17776640 (receipt validation of the PR 2773 SIDON-RECEIPT.json values)",
+    "predecessor_tests": "Ran 13 tests in 0.077s ... OK (PR 2870 test_engine.py)",
+    "parseval_obstruction": "OBSTRUCTION (11, 6) odd_excess=2 bounded=B parseval=696 allowed=504 deficit=192 contradiction=True; OBSTRUCTION (6, 11) odd_excess=2 bounded=A parseval=696 allowed=504 deficit=192 contradiction=True; REPRO rows remainder (5,1),(6,0) shared=1 c=1",
+    "predecessor_independent": "PASS_17POINT_INDEPENDENT (receipt_consistency k10_budget3 count=149990400 first_valid=true; k11_raw_budget4 complete=true level3=0 level4=0 sub_shards=62; rows agree on all six splits; small_group_budget_agreement 420/840/168)"
+  },
+  "heavy_anchor_recomputation": {
+    "method": "The established PR 2773 raw-domain walk on the byte-vendored PR 2773 engine (vendor/agent64_search17.py, SHA-256 9eb1bf79...), complete GL(6,2)-transitive domain through {0, 3}, sub-shards by the smallest free element, per-sub-shard receipts in ANCHOR-PROGRESS.json (one section per mode), blocking foreground invocations with PYTHONUNBUFFERED=1.",
+    "correction_note": "An earlier in-session PASS_ANCHORS_* print from the extracted PR 2870 package was receipt validation only: PR 2870's committed ANCHOR-PROGRESS.json already contained all 62 sub-shards, so its anchors.py resumed instantly and re-added the recorded totals. The runs recorded here are the genuine fresh re-walk in this package's own ANCHOR-PROGRESS.json, started empty.",
+    "k10_budget3": "PASS_ANCHORS_K10B3 count=149990400 total_hist={'3': 149990400} shards=62 -- full fresh re-walk (62/62 sub-shards, started from an empty receipt); matches the recorded anchor 149,990,400 exactly and every leaf is at exact pair-sum excess 3.",
+    "k11_levels34": "PASS_ANCHORS_K11B4 count=0 total_hist={} shards=62 -- full fresh re-walk (62/62 sub-shards); zero 11-sets of pair-sum excess <= 4 through {0,3}, so k=11 levels 3 and 4 are both 0 (min pair-sum excess of 11-sets in F2^6 is >= 5).",
+    "fresh_floor_walks": "FRESH_WALK k=10 budget=2 count=0 (165.1 s) and k=11 budget=2 count=0 (140.4 s), each a complete count_sets(EVEN, k, 2, fixed=(0,3)) walk; combined with the excess-3 examples in the k10b3 receipts this fresh-proves floor(10) = 3 and floor(11) >= 3."
+  },
+  "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],
+    "parseval_obstruction_11_6": {"parseval_remainder": 696, "max_allowed": 504, "deficit": 192}
+  },
+  "status": "ANCHOR STATUS: every recorded predecessor anchor named in the assignment is reproduced in this session. RECOMPUTED from scratch: the PR 2542/2634 REPRO tiers (945/31, 10395/49, 945945/59 with records SHA-256) and the PR 2542 length-18 census (15,775,992 nodes, 312,064 cycles, zero universal) via PR 2773's verify.py on the byte-exact vendored engine; the PR 2870 OBSTRUCTION lines (parseval=696 allowed=504 deficit=192, both parity orders) via PR 2870's own verify.py/test_engine.py and again in this package's squeeze_numbers; the row table and n=5 set controls; and BOTH heavy census anchors in full by fresh empty-receipt walks (PASS_ANCHORS_K10B3 count=149990400, PASS_ANCHORS_K11B4 count=0, 62/62 sub-shards each, receipts in this package's ANCHOR-PROGRESS.json). VALIDATED (not re-walked): the four zero shards k10 budgets 0/1/2 and k11 budget 2 against the PR 2773 receipt arithmetic (verify.py --full, ~17 min on PR 2870's machine, not re-run here); the fresh k10/k11 budget-2 walks independently confirm the two load-bearing zero facts."
+}

research/f7-18point-cover-question-seed6d34356c/CERTIFICATE.json

@@ -0,0 +1,77 @@
+{
+  "schema_version": 1,
+  "result": "KB3e set-level verdict (outcome=partial): the 18-point cover question for F2^7 is NOT decided -- no 18-point cover was constructed and no split was excluded -- but it is narrowed to an exact finite remainder. All four counting-feasible splits (12,6),(11,7),(10,8),(9,9) survive the extended odd-coverage Fourier/Parseval layer (deficits non-positive; the PR 2870 squeeze hypothesis fails because 18 is even, so both sides have equal character parity), survive the extended pair-representation rows after the reproduced census floors (808 / 501 / 251 / 196 surviving rows respectively), and survive a bounded seeded construction search (best coverage 118/128 at k=18 against 10/10 instant k=20 covers as non-vacuity control). Exact new obstructions: (12,6) and (10,8) covers must have at least one vanishing character off the all-ones hyperplane. No kappa, supplier or selected-frontier change; the gap 20 <= f(7) <= 24 is unchanged.",
+  "labels": [
+    {
+      "statement": "Reduction lemma: for S = A u B with A in the even coset E and B in the odd coset O of F2^n, and D = p + B (p any odd mask, D subset E), S covers F2^n iff (i) A + D = E and (ii) (A + A) u (D + D) = E. Every parity split (s, t) is therefore a two-set covering problem in the even group E =~ F2^6.",
+      "label": "PROVEN",
+      "evidence": "Direct from coset arithmetic (A + B = O iff A + D = p + O = E, and B + B = D + D); machine-checked exhaustively over all 256 subsets of F2^3 in test_engine.py (test_reduction_equivalence_exhaustive_n3) and on the real F2^5 cover."
+    },
+    {
+      "statement": "Every 18-point cover of split (12,6) -- and of split (10,8) -- must have at least one character u not in {0, all-ones} with f_hat(u) = 0 or g_hat(u) = 0 (a vanishing character). Equivalently the no-vanishing sub-case of the profile system is infeasible for both splits.",
+      "label": "PROVEN",
+      "evidence": "Exact integer enumeration (cover18.fourier_profile_feasibility with nonzero_both=True) over every attainable rho square sum: for (12,6) the no-vanishing spectral shape is forced to n22=24, n24=8, n42=31 on the 126 characters off {0,1}, giving sum rho^2 = 46, which is not an attainable sum of squares of integer rho >= 0 with sum rho = 8 (the attainable set is {8,10,12,14,16,18,20,22,24,26,28,30,32,34,38,40,50,64}); for (10,8) the two Parseval equations force a non-integer shape count. The constraint set (character parity, |rho_hat| <= E_o with rho_hat == E_o (mod 2), the even-half bound f_hat^2 + g_hat^2 <= s + t + 2P - 2^n, and Parseval) is validated against every real cover of F2^3 and F2^4 (exhaustive) and of F2^5 (sample) in test_engine.py."
+    },
+    {
+      "statement": "The PR 2870 odd-coverage Fourier/Parseval squeeze does not reach any 18-point split: 18 is even, so s and t always have equal character parity, and the tracked deficits are non-positive on every split.",
+      "label": "PROVEN",
+      "evidence": "Exact bookkeeping (cover18.squeeze_numbers): (12,6) E_o=8, remainders A=1248, B=696, no uniform character bound (vanishing possible); (11,7) E_o=13, remainders 1166 and 798 vs allowed 126*169 = 21294 each (deficits -20128, -20496); (10,8) E_o=16, remainders 540, 448, no uniform bound; (9,9) E_o=17, remainders 990, 990 vs allowed 126*289 = 36414 (deficit -35424). PR 2870's own obstruction() reports the same status ('equal character parities: no side is squeezed')."
+    },
+    {
+      "statement": "Every recorded predecessor anchor is reproduced before any new number: PR 2542/2634 REPRO tiers 945/31, 10395/49, 945945/59 and the L18 census 15,775,992 nodes / 312,064 cycles / 0 universal; PR 2870 OBSTRUCTION lines parseval=696 allowed=504 deficit=192 both parity orders; PR 2773 k10 budget-3 = 149,990,400 and k11 levels 3-4 = 0 both recomputed IN FULL by fresh empty-receipt walks (PASS_ANCHORS_K10B3 count=149990400 shards=62, PASS_ANCHORS_K11B4 count=0 shards=62); row table (5,1),(6,0) remainder and the n=5 set controls.",
+      "label": "CHECKED",
+      "evidence": "ANCHOR-REPRO.json records commands and observed outputs; the fresh walks live in this package's ANCHOR-PROGRESS.json (one section per mode, per-sub-shard receipts). Correction recorded there: an earlier PASS print from the extracted PR 2870 package was receipt validation (its committed receipt pre-filled all shards), not a re-walk; the anchors.py runs recorded here started from an empty receipt."
+    },
+    {
+      "statement": "The pair-representation rows of the four 18-point splits after the reproduced census floors (floor(6..9)=0, floor(10)=3, floor(11)=5, floor(12)=3 counting): (12,6) 808 surviving rows over 120 distinct (e_ex, b_ex) pairs, (11,7) 501 rows / 36 pairs, (10,8) 251 rows / 28 pairs, (9,9) 196 rows / 45 pairs. Each row is exact (attainable c computed by contingency-table pairing sums, validated equal to the vendored PR 2773 _pairing_sums wherever the vendored O(m!) loop terminates).",
+      "label": "CHECKED",
+      "evidence": "cover18.sharp_rows_fast; verify.py rows mode asserts the four row counts and reproduces the 17-point control remainder (5,1),(6,0) and the empty (10,7) table after the floor; full row lists in the verify output."
+    },
+    {
+      "statement": "The per-character profile system does not exclude any 18-point split: (12,6), (11,7), (10,8), (9,9) all admit consistent profiles (feasible S value lists recorded; (9,9) partially undecided where the solver step cap was reached, which is never treated as a proof).",
+      "label": "CHECKED",
+      "evidence": "cover18.fourier_profile_feasibility; the same system reproduces the known exclusions ((11,6) infeasible -- PR 2870's result; (10,7) infeasible -- consistent with PR 2773's census exclusion) and accepts every split realized by a real cover (exhaustive F2^3/F2^4 cover batteries)."
+    },
+    {
+      "statement": "No 18-point cover exists in the searched domain (scoped search failure, not an exclusion): direct local search at k=18 with 200 seeded restarts tops out at 118 of 128 covered masks; the structured (A, D) searches per split (60 restarts each) top out at 118 / 118 / 118 / 117 of 128; a k=19 probe is similar. Non-vacuity: the identical machinery finds 20-point covers in 10/10 short runs, matching PR 2634's recorded abundance of 20-point covers and its own failure to find 19-point covers in 200 restarts (max 124/128).",
+      "label": "CHECKED",
+      "evidence": "cover18.search_direct / cover18.search_split, fixed seeds 20261016+; verify.py search mode; the search never asserts nonexistence."
+    },
+    {
+      "statement": "The direct extension of PR 2870's squeeze to 18-point splits as an exclusion mechanism is DEMOTED: its hypothesis (opposite character parity) fails on every 18-point split and the tracked deficits are non-positive.",
+      "label": "DEMOTED",
+      "evidence": "See the PROVEN bookkeeping statement; PR 2870 itself predicted this route does not reach the 18/19-point splits (E_o >= 8 there)."
+    },
+    {
+      "statement": "The expectation that the pair-representation rows collapse to a small remainder (as at 17 points, where two rows survived) is DEMOTED at 18 points: the remainders are large (808 / 501 / 251 / 196 rows) and the census floors at 18 points are weaker (floor(12) = 3 is only the counting floor).",
+      "label": "DEMOTED",
+      "evidence": "cover18.sharp_rows_fast output; the floors used are exactly the reproduced ones (floor(10) = 3 fresh-proven by the k10-budget-2 = 0 walk plus excess-3 examples; floor(11) = 5 from the reproduced k11b4 = 0 walk)."
+    }
+  ],
+  "obstruction_numbers": {
+    "n": 7,
+    "split_order_notes": "(s, t) = (points in the even coset, points in the odd coset); mirrors are identical by odd translation",
+    "splits": {
+      "12_6": {"odd_excess": 8, "squeeze": "none (equal parity)", "remainders": [1248, 696], "uniform_bound": null, "profile_system": "feasible (16 S values)", "no_vanishing": "infeasible -> PROVEN vanishing character required", "rows_after_floors": 808, "search_best_of_128": 118},
+      "11_7": {"odd_excess": 13, "squeeze": "none (equal parity)", "remainders": [1166, 798], "allowed_per_side": 21294, "deficits": [-20128, -20496], "profile_system": "feasible (22 S values)", "no_vanishing": "automatic (odd characters never vanish)", "rows_after_floors": 501, "search_best_of_128": 118},
+      "10_8": {"odd_excess": 16, "squeeze": "none (equal parity)", "remainders": [1080, 896], "uniform_bound": null, "profile_system": "feasible (50 S values)", "no_vanishing": "infeasible -> PROVEN vanishing character required", "rows_after_floors": 251, "search_best_of_128": 118},
+      "9_9": {"odd_excess": 17, "squeeze": "none (equal parity)", "remainders": [990, 990], "allowed_per_side": 36414, "deficits": [-35424, -35424], "profile_system": "feasible (31 S values; some S undecided at the solver step cap)", "no_vanishing": "automatic (odd characters never vanish)", "rows_after_floors": 196, "search_best_of_128": 117}
+    },
+    "controls": {
+      "11_6": "profile system infeasible -- reproduces PR 2870's exclusion (squeeze parseval=696 allowed=504 deficit=192)",
+      "10_7": "profile system infeasible -- consistent with PR 2773's census exclusion",
+      "n5_real_cover": "split (4,6) of the real 10-point cover of F2^5 passes every check (positive control)"
+    }
+  },
+  "reproduce": [
+    "python3 -I -B research/f7-18point-cover-question-seed6d34356c/test_engine.py",
+    "python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py quick",
+    "python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py fourier",
+    "python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py rows",
+    "python3 -I -B research/f7-18point-cover-question-seed6d34356c/verify.py search",
+    "python3 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k10b3 (resumable, ~35 min cold)",
+    "python3 -I -B research/f7-18point-cover-question-seed6d34356c/anchors.py k11b4 (resumable, ~35 min cold)"
+  ],
+  "kappa_change": null,
+  "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+}

research/f7-18point-cover-question-seed6d34356c/NOTICE.md

@@ -0,0 +1,55 @@
+# 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). This package is contributed
+under the repository's Apache-2.0 license; see the root `LICENSE` and
+`NOTICE` files. The vendored files retain their source licenses and are
+reproduced byte-exactly with SHA-256 pins (see `SOURCES.json` and the byte-pin
+tests in `test_engine.py`).
+
+Predecessor credit (every cited PR author verified against current ground
+truth with `gh pr view NNN --json author,title` at writing time):
+
+- [PR 943](https://github.com/CrocSwap/integer-mult-bounds/pull/943) by Ross
+  Richardson (RossRichardson) — the prefix-walk model and the
+  `P + P = F2^n` covering condition this whole question lives in.
+- [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`, `20 <= f(7) <= 24` and the frozen tier `EXPECTED.json`
+  reproduced as an anchor.
+- [PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542) by
+  Aaron Wang (navinor) — the length-18 exclusion, the claim "No 17-point set
+  covers `F2^7`" and the pair-representation identity this package's row
+  machinery extends.
+- [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 the Set-ILS precedent (20-point covers abundant; no 19-point
+  cover in 200 restarts) that the bounded search here is compared against.
+- [PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773) by
+  Aaron Wang (navinor) — the split-by-split audit, the sharp row machinery,
+  the Sidon/pair-sum budget enumeration (`cover17.py` / `search17.py`,
+  vendored here byte-exact as `vendor/agent64_cover17.py` /
+  `vendor/agent64_search17.py`) and the census floors.
+- [PR 2870](https://github.com/CrocSwap/integer-mult-bounds/pull/2870) by
+  Aaron Wang (navinor) — the odd-coverage Fourier/Parseval identity (the
+  deficit bookkeeping re-derived and extended here), the hash-pinned vendor
+  copies this package extracts byte-exactly, and the resumable anchor driver
+  `anchors.py` (vendored byte-exact).
+- [PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) by
+  Nicholas Stone (NicholasStone, Kimi agent) — the completed `(10,10)`
+  simple-20-cycle word census; recorded state only, not re-run here. His
+  concurrent repeated-state `L = 20` word claim (discussion 1166 comment
+  18954844) is a different (word-level) object and is untouched.
+
+Vendored files (byte-exact, enforced by byte-pin tests):
+
+| Local path | Source | SHA-256 (prefix) |
+|---|---|---|
+| `vendor/agent64_cover17.py` | PR 2773 `cover17.py` (via PR 2870's pinned vendor/) | `082bc838134cba97...` |
+| `vendor/agent64_search17.py` | PR 2773 `search17.py` (via PR 2870's pinned vendor/) | `9eb1bf79ffb99b0e...` |
+| `anchors.py` | PR 2870 `anchors.py` | `73d73a9b94539403...` |
+
+Predecessor packages were read byte-exactly from their PR heads with
+`agent_tools.py pr-tree-extract` / `pr-file-bytes` and were never imported at
+runtime.