From a05791d428f5d06802fb4c96b33732e6347c64eb Mon Sep 17 00:00:00 2001 From: Aaron Wang Date: Fri, 16 Oct 2026 15:35:03 -0400 Subject: [PATCH] KB3i: the 18-point cover remainder for F2^7 - parity shortcut DEMOTED, m=5 obstruction localized (outcome=partial, no new kappa) Set-level result, no words enumerated. The FINAL 18-point remainder of PR 3023: (12,6) A-vanish (4,2)/(3,3) plus the both-odd splits (11,7)/(9,9). No class is decided and no 18-point cover is constructed; the single most tempting shortcut to breaking (11,7)/(9,9) is PROVEN false. - PROVEN (negative on the method): a covering reduced pair (A,B) of F2^m need NOT have |A|,|B| both even. A complete m=3 census (2^8 x 2^8) finds both-odd covers ((5,5): 3136, (7,7): 64), so no dimension-free parity rule can exclude (11,7)/(9,9). - CHECKED (m=5 ground truth, complete m=4 sum-10 censuses): covers only in the both-even splits (2,8)=15360, (4,6)=143360; both-odd (1,9),(3,7),(5,5) empty, obstruction localized per split: (1,9) counting st=9<16, (3,7) cross never covers, (5,5) self never covers when cross covers (4,085,760 cross-covering pairs, self-union <= 15/16). - DEMOTED: the m=5 obstruction does not lift as a parity/self-sum rule to (9,9)/(11,7) (both-odd covers exist at m=3; the (5,5) selfsum bound is scale-dependent). - CHECKED: the (11,7)/(9,9) rho^2/identity frontier pinned (E_o=13/17, even_half_max=42/34, min sum rho^2=17/19, PR 2870 squeeze inapplicable). - CHECKED (route c): bounded construction search finds no covering 18-set; best 118/128 at k=18 (record ceiling 119/128). - NOT DECIDED: (4,2)/(3,3) recorded as walk-ready reduced forms with budgets (PR 3023 classification, reproduced); walks too large for the session. All seven anchors reproduced first (FOURIER/OBSTRUCTION/CLASSIFY/ROWS18/NOVANISH recomputed live; CLASS82/CLASS60/AV51 read back from PR 3023 receipts). Exact integer arithmetic throughout. Vendored engines byte-exact with SHA-256 pins. Attribution: Aaron Wang, with help from opencode. Registered package research/f7-18point-remainder-kb3i-a1 passes --check-only. --- .../CERTIFICATE.json | 75 ++ .../f7-18point-remainder-kb3i-a1/NOTICE.md | 36 + .../f7-18point-remainder-kb3i-a1/README.md | 234 ++++++ .../f7-18point-remainder-kb3i-a1/SOURCES.json | 66 ++ .../f7-18point-remainder-kb3i-a1/TASK.json | 122 +++ .../f7-18point-remainder-kb3i-a1/VERIFY.json | 55 ++ .../f7-18point-remainder-kb3i-a1/_assemble.py | 284 +++++++ .../f7-18point-remainder-kb3i-a1/_card.json | 40 + .../_emit_meta.py | 44 + .../construct_search.py | 45 ++ .../fourier_probe.py | 52 ++ .../parity_census.py | 169 ++++ .../self_obstruction.py | 116 +++ .../split_census.py | 99 +++ .../vendor/agent64_cover17.py | 263 ++++++ .../vendor/agent64_search17.py | 330 ++++++++ .../vendor/anchors.py | 128 +++ .../vendor/cover18.py | 741 +++++++++++++++++ .../vendor/tight.py | 760 ++++++++++++++++++ .../vendor/vanish.py | 604 ++++++++++++++ .../f7-18point-remainder-kb3i-a1/verify.py | 232 ++++++ 21 files changed, 4495 insertions(+) create mode 100644 research/f7-18point-remainder-kb3i-a1/CERTIFICATE.json create mode 100644 research/f7-18point-remainder-kb3i-a1/NOTICE.md create mode 100644 research/f7-18point-remainder-kb3i-a1/README.md create mode 100644 research/f7-18point-remainder-kb3i-a1/SOURCES.json create mode 100644 research/f7-18point-remainder-kb3i-a1/TASK.json create mode 100644 research/f7-18point-remainder-kb3i-a1/VERIFY.json create mode 100644 research/f7-18point-remainder-kb3i-a1/_assemble.py create mode 100644 research/f7-18point-remainder-kb3i-a1/_card.json create mode 100644 research/f7-18point-remainder-kb3i-a1/_emit_meta.py create mode 100644 research/f7-18point-remainder-kb3i-a1/construct_search.py create mode 100644 research/f7-18point-remainder-kb3i-a1/fourier_probe.py create mode 100644 research/f7-18point-remainder-kb3i-a1/parity_census.py create mode 100644 research/f7-18point-remainder-kb3i-a1/self_obstruction.py create mode 100644 research/f7-18point-remainder-kb3i-a1/split_census.py create mode 100644 research/f7-18point-remainder-kb3i-a1/vendor/agent64_cover17.py create mode 100644 research/f7-18point-remainder-kb3i-a1/vendor/agent64_search17.py create mode 100644 research/f7-18point-remainder-kb3i-a1/vendor/anchors.py create mode 100644 research/f7-18point-remainder-kb3i-a1/vendor/cover18.py create mode 100644 research/f7-18point-remainder-kb3i-a1/vendor/tight.py create mode 100644 research/f7-18point-remainder-kb3i-a1/vendor/vanish.py create mode 100644 research/f7-18point-remainder-kb3i-a1/verify.py diff --git a/research/f7-18point-remainder-kb3i-a1/CERTIFICATE.json b/research/f7-18point-remainder-kb3i-a1/CERTIFICATE.json new file mode 100644 index 0000000000..3d6313453f --- /dev/null +++ b/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" +} diff --git a/research/f7-18point-remainder-kb3i-a1/NOTICE.md b/research/f7-18point-remainder-kb3i-a1/NOTICE.md new file mode 100644 index 0000000000..b77f4cb0f6 --- /dev/null +++ b/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. diff --git a/research/f7-18point-remainder-kb3i-a1/README.md b/research/f7-18point-remainder-kb3i-a1/README.md new file mode 100644 index 0000000000..5713cbc1d7 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/README.md @@ -0,0 +1,234 @@ +# KB3i — the 18-point cover remainder for F2^7: (4,2)/(3,3)/(11,7)/(9,9) + +**Set-level finite result, no words enumerated. Outcome = partial (narrowed +remainder). No 18-point cover of `F2^7` is constructed and no surviving split +is excluded outright; no new kappa.** The single most tempting shortcut to +excluding the two both-odd splits `(11,7)`/`(9,9)` — a parity rule forcing +both covering halves even — is **PROVEN false** by a complete census, so it +cannot be used to kill them. The m=5 "even-splits-only" ground truth is +**established and its obstruction localized per split**, and is shown to be +scale/mechanism-specific (it does not lift as a parity rule). The exact +rho²/identity frontier for `(11,7)`/`(9,9)` is reproduced and pinned. + +## Object and chain of record + +In the PR943 prefix-walk model +([Ross Richardson, `research/universal-connector-boundary`](https://github.com/CrocSwap/integer-mult-bounds/pull/943)) +a restored seven-source singleton word is universal exactly when its prefix +set `P` covers: `P + P = F2^7`. The 17-point question is closed +([PR 2542](https://github.com/CrocSwap/integer-mult-bounds/pull/2542), +[PR 2634](https://github.com/CrocSwap/integer-mult-bounds/pull/2634), +[PR 2773](https://github.com/CrocSwap/integer-mult-bounds/pull/2773), +[PR 2870](https://github.com/CrocSwap/integer-mult-bounds/pull/2870)). +[PR 2911](https://github.com/CrocSwap/integer-mult-bounds/pull/2911) narrowed +the 18-point question to the splits `(12,6)`, `(11,7)`, `(10,8)`, `(9,9)` (+ +mirrors) and proved any `(12,6)`/`(10,8)` cover must have a vanishing +character off the all-ones hyperplane. [PR 2933](https://github.com/CrocSwap/integer-mult-bounds/pull/2933) +classified the vanishing configurations and recorded the class floors. +[PR 2961](https://github.com/CrocSwap/integer-mult-bounds/pull/2961) decided +the three tightest classes and fully excluded `(10,8)`. +[PR 3023](https://github.com/CrocSwap/integer-mult-bounds/pull/3023) killed +`(12,6)` A-vanish `(5,1)` and recorded the remainder this package takes: +**(12,6) A-vanish (4,2) and (3,3), plus the both-odd splits (11,7) and (9,9) +which carry no vanishing character.** This package is strictly SET-level. + +With `D = p + B` inside `E = F2^6` (PR 2911's reduction) the pair `(A, D)` +covers iff `A + D = E` and `(A+A) u (D+D) = E`. Both halves of `A`, `D` +identify with `F2^5` and coverage is the four PR 2933 L3 lines. Every split +`(s,t)` of 18 has `s` and `t` of equal parity (18 is even), which is exactly +the case the PR 2870 squeeze does not reach (its hypothesis is opposite +parity). `(12,6)` and `(10,8)` are both-even; `(11,7)` and `(9,9)` are +both-odd, and PR 2933 proved both-odd splits carry no vanishing character — so +the Fourier/odd-coverage route that killed the other splits is closed to them. + +Record chain authors, all verified against current ground truth with +`gh pr view NNN --json author,title` at writing: PR 2542/2634/2773/2870/2911/ +2933/2961/3023 are Aaron Wang (navinor); [PR 2691](https://github.com/CrocSwap/integer-mult-bounds/pull/2691) +and [PR 2973](https://github.com/CrocSwap/integer-mult-bounds/pull/2973) are +Nicholas Stone (NicholasStone); [PR 3005](https://github.com/CrocSwap/integer-mult-bounds/pull/3005) +is Nick Petalas (petalas). PR 2973 (merged) and PR 3005 are the concurrent +WORD-level line (`22 <= f(7) <= 24`, a false-prune correction to the word +census budgets); 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. + +## Verdict per class (exact integers) + +| Split | Class | PR 2933 floor | Status here | Deciding evidence | +|---|---|---|---|---| +| (12,6) | A-vanish (4,2) | 44 >= 32 | NOT decided (walk-ready) | exact reduction D1 = 0,1 under GL(5,2); budgets 20/20/24; walk too large | +| (12,6) | A-vanish (3,3) | 45 >= 32 | NOT decided (walk-ready) | four L3 lines direct; all budgets slack; no forced structure | +| (11,7) | both-odd, no vanishing char | — | NOT excluded; parity shortcut DEMOTED | both-odd covers exist at m=3 (complete census); frontier E_o = 13, min sum rho^2 = 17 | +| (9,9) | both-odd, no vanishing char | — | NOT excluded; parity shortcut DEMOTED | both-odd covers exist at m=3 (complete census); frontier E_o = 17, min sum rho^2 = 19 | + +No class is decided here. The (4,2)/(3,3) reductions and budgets are necessary +conditions and exact finite search domains (PR 3023's classification, +reproduced), not exclusions. + +## Route (b): the parity shortcut is PROVEN false (DEMOTED) + +The cleanest way to break `(11,7)`/`(9,9)` would be a parity rule: *a +covering pair `(A,B)` of `F2^m` (i.e. `A+B = F2^m` and `(A+A) u (B+B) = F2^m`) +must have `|A|` and `|B|` both even.* Then the both-odd splits `(11,7)`/`(9,9)` +would be excluded and the 18-point question would collapse to `(12,6)`/`(10,8)`. + +**This is false.** A complete enumeration of the reduced covering problem in +`F2^3` (all `2^8 x 2^8` subset pairs) finds covering pairs in every both-odd +split `(3,5)`, `(3,7)`, `(5,3)`, `(5,5)`, `(5,7)`, `(7,3)`, `(7,5)`, `(7,7)` +— for example `(5,5)` has 3136 covers and `(7,7)` has 64. So there is **no +dimension-free parity obstruction**, and none can be used to kill `(11,7)`/`(9,9)`. +(The complete m=3 census: `(3,3)` is the only small both-odd split with zero +covers; `(5,5)`, `(7,7)` are non-empty.) This is a PROVEN negative on the +shortcut, not on the splits themselves. + +## The m=5 ground truth and its obstruction (route b, "why at m=5") + +The recorded ground truth — *`F2^5` covers exist only in splits `(2,8)`, `(4,6)`, +`(6,4)`, `(8,2)`* — is a statement about the reduced problem in `F2^4` with +`|A| + |B| = 10`. It is **confirmed** by complete enumeration (see +`verify.py full`), and the both-odd emptiness is localized to three distinct +mechanisms: + +| m=4 split | covers | why empty (both-odd) | +|---|---|---| +| (2,8) | > 0 (even) | — (witness `A=[0,1] B=[0,2,4,6,8,10,12,15]`) | +| (4,6) | > 0 (even) | — (witness `A=[0,1,2,3] B=[0,1,2,4,8,15]`) | +| (1,9) | 0 | counting: `st = 9 < 16`, so `A+B` never covers (self covers for all 183,040 pairs) | +| (3,7) | 0 | cross never covers: `st = 21 >= 16` but `A+B != F2^4` for every pair | +| (5,5) | 0 | self never covers when cross covers: all 4,085,760 cross-covering pairs have `|A+A|,|B+B|` in `{8,11}` and `|(A+A) u (B+B)| <= 15 < 16` | + +So the "even-splits-only" pattern at m=5 is a genuine fact, but its mechanism +is split- and scale-specific (counting / cross / self), **not a parity rule**. +Because both-odd covers exist at m=3 and the `(5,5)` self-sum bound is +scale-dependent, the m=5 obstruction does **not** lift to a valid exclusion of +`(11,7)`/`(9,9)` at m=6. No parity or self-sum-size argument is available +there. (DEMOTED: the lift.) + +## The (11,7)/(9,9) identity frontier (reproduced, quantified) + +Both splits survive the rho²/identity layer; the exact remaining conditions +(PR 2961's, reproduced here) are: + +| Split | odd excess E_o | even-half bound | min sum rho^2 (partition) | effective min (post PR 2961) | squeeze (opposite-parity) | +|---|---|---|---|---|---| +| (11,7) | 13 | 42 | 13 | 17 (all-ones and (2,1^11) excluded) | inapplicable (s+t even) | +| (9,9) | 17 | 34 | 17 | 19 (all-ones excluded) | inapplicable (s+t even) | + +`E_o = s*t - 2^6`; the even-half bound is `max(f_hat^2 + g_hat^2)` off the +all-ones hyperplane from the self-sum half of coverage +(`s + t + 2*P - 2^7`, `P = C(s,2)+C(t,2)`). The PR 2870 Parseval squeeze uses +only odd coverage and requires opposite parity; its hypothesis fails for every +18-point split (all have `s + t = 18` even), so its deficit argument reaches no +contradiction here (`deficit < 0` on both sides). Breaking `(11,7)`/`(9,9)` +requires pushing the **even-half (self-sum) coverage** multiplicities at the +501/196 surviving rows (PR 2911) — the direction PR 2870 did not use. This is +PR 2961's open question 2, untouched by any prior PR and **not** settled here. + +## Route (c): bounded construction search (no cover found) + +A bounded, seeded local search (route c) finds no covering 18-set: + +| search | best coverage | record ceiling | +|---|---|---| +| direct k=18 on F2^7 (3 seeds) | 118 / 128 | 119 / 128 (PR 2634) | +| reduced (12,6), (11,7), (10,8) on F2^6 | 118 / 128 | — | +| reduced (9,9) on F2^6 | 117 / 128 | — | + +Seed-invariant best 118/128; no cover reached. A failed bounded search is a +scoped search failure, never an exclusion. The search ceiling is unchanged. + +## Anchors reproduced before any new number + +| Anchor | Expected | Status here | +|---|---|---| +| PR 2870 OBSTRUCTION | parseval=696 allowed=504 deficit=192 | recomputed fresh | +| PR 2911 ROWS18 | 808/501/251/196 | recomputed fresh | +| PR 2911 NOVANISH | (12,6),(10,8) infeasible | recomputed fresh | +| PR 2933 CLASSIFY | 2 lines value=32 need=32 TIGHT, cases=6720 | recomputed fresh | +| PR 2961 FOURIER (7,1) | need=175 lower=239 | recomputed fresh | +| PR 2961 CLASS82 | checked=28,815,360 covering=0 | read from PR 3023 receipts | +| PR 2961 CLASS60 | d_checked=169,911 d_with_transversals=0 | read from PR 3023 receipts | +| PR 3023 AV51 | u_checked=169,911 uv_pairs=3,049,492,320 covering=0 | read from PR 3023 receipts | + +The light anchors are recomputed live from the byte-vendored engines; the heavy +walk anchors (CLASS82/CLASS60/AV51) are read back from PR 3023's per-shard +receipts (PR 3023 re-walked them from empty receipts; reproduced values match +exactly). + +## Reproduce + +Standard library only, CPython 3.12, from the repository root: + +```sh +python3 -I -B research/f7-18point-remainder-kb3i-a1/verify.py quick +python3 -I -B research/f7-18point-remainder-kb3i-a1/verify.py full +python3 -I -B research/f7-18point-remainder-kb3i-a1/verify.py search +``` + +Expected markers: `PASS_KB3I_QUICK`, `PASS_KB3I_FULL`, `PASS_KB3I_SEARCH`. +`quick` reproduces the anchors, the complete m=3 parity-demotion census and the +(11,7)/(9,9) frontier numbers in well under a second. `full` re-runs the +complete m=4 sum-10 censuses and the (5,5) self-obstruction localization +(minutes). `search` re-runs the bounded construction search. Standalone +probes: `parity_census.py m3|m4`, `split_census.py [stop]`, +`self_obstruction.py `, `fourier_probe.py [--full]`, +`construct_search.py`. + +Registered replay: `python3 scripts/research_package.py --package +research/f7-18point-remainder-kb3i-a1 --check-only` passes +`PASS_PACKAGE_METADATA_AND_PINS`. + +## Scope and limitations + +Set-level only inside PR943's abstract interface. Not checked: anything +word-level (PR 2973/PR 3005's corrected word census and `L = 22` versus +`L = 24` are word-level work, untouched here), walk-realizability of any cover, +and any kappa, supplier, tariff or selected-frontier implication. **(4,2), +(3,3), (11,7), (9,9) are all undecided here**; nothing in this package excludes +any of them, and the parity-shortcut demotion is a negative result about the +*method*, not about the splits. No construction search found a cover (route c +is a scoped search failure, not an exclusion). The recorded set-level search +ceilings stay `118/128` at `k = 18` (this run) / `119/128` (PR 2634 record) and +`124/128` at `k = 19`. The word-level gap is `22 <= f(7) <= 24` (PR 2973/3005); +under it this package's question is a necessary condition for `f(7) = 22`. All +arithmetic is exact Python integers (int bitmasks); no floats are used. Frozen +predecessor packages are unchanged; the six vendored engines are byte-exact +with SHA-256 pins (see `NOTICE.md`/`SOURCES.json`). + +## Open next questions + +1. **Push the even-half (self-sum) coverage identity for (11,7)/(9,9)** (PR + 2961's open question 2): derive the self-sum multiplicities at the 501/196 + surviving rows and check them against every cover of `F2^5` (PR 2933's + census) before lifting to `m = 6`. This is the one direction the PR 2870 + odd-coverage squeeze did not use. Why it matters: these two splits carry the + other half of the 18-point question. +2. **Decide (12,6) A-vanish (4,2)** with PR 3023's recorded reduced form (W + 4-sets, `D1 = 0,1`) and budgets `|U+W| >= 20`, `|V+W| >= 20`, `|U+V| >= 24`: + a complete sharded walk with generous per-shard budgets and per-shard + receipts. Why it matters: clearing (4,2) forces any (12,6) A-vanish cover + into (3,3). Blocked by: nothing structural; a few hours of sharded walk + (strictly larger than (5,1)'s 3,049,492,320-pair walk). +3. **Decide or identify (12,6) A-vanish (3,3)** via the direct normalized walk + or a cross-line multiplicity identity. Blocked by: all four line budgets are + slack and no forced structure exists. +4. **Find a valid lift of the (5,5) self-sum obstruction** to (9,9): the m=4 + mechanism (`|A+A| <= 11` for cross-covering `(5,5)`) is scale-dependent and + fails at m=3; determine the exact `m`/split threshold, if any, at which a + self-sum-size bound forbids a both-odd self cover. + +## Credit + +PR 2542/2634/2773/2870/2911/2933/2961/3023 (Aaron Wang): the 17-point +exclusion chain, the KB3b search ceilings, 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 open question 1 records the (4,2)/(3,3) remainder +this package takes. PR 943 (Ross Richardson): the prefix-walk model. PR 1185 +(Mister-Meeseeks, per current ground truth): the pinned `f(5)=12`, `f(6)=16` +record. PR 2691/2973 (Nicholas +Stone) and PR 3005 (Nick Petalas): the word-level census line and its +correction (recorded state; PR 2973 leaves the set-level chain intact). The +PR 2961/2773 engines (`tight.py`, `cover18.py`, `vanish.py`, +`agent64_cover17.py`, `agent64_search17.py`, `anchors.py`) are vendored +byte-exact with SHA-256 pins and credited in `NOTICE.md`/`SOURCES.json`. diff --git a/research/f7-18point-remainder-kb3i-a1/SOURCES.json b/research/f7-18point-remainder-kb3i-a1/SOURCES.json new file mode 100644 index 0000000000..6bccf3cd85 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "usage": "provenance" + }, + { + "path": "certificates/selected-result.json", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "usage": "provenance" + } + ], + "references": [ + { + "local_path": "vendor/tight.py", + "source_path": "research/f7-18point-tight-classes-seed4c1e7b30/tight.py", + "pr": 2961, + "sha256": "14670ef2d3df9e4ecc9e1db962f4e8cb77545d1c889144352760c1fd14e2273b", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from the immediate predecessor PR 3023's package research/f7-18point-avtail-seed010d26fa, which vendored it from PR 2961), credit Aaron Wang (navinor), PR 2961: bitmask primitives, the (7,1) Fourier identity, rho classification. Enforced by byte-pin checks in verify.py." + }, + { + "local_path": "vendor/cover18.py", + "source_path": "research/f7-18point-tight-classes-seed4c1e7b30/cover18.py", + "pr": 2961, + "sha256": "24c6a2f4911dc2d5de76972eb5ae93dc4e66d8fa1e904443de6d0638e70c0a04", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from the immediate predecessor PR 3023's package research/f7-18point-avtail-seed010d26fa, which vendored it from PR 2961), credit Aaron Wang (navinor), PR 2961: the reduced (A,D) covering model, Fourier profile system, squeeze numbers, pair-representation rows, bounded search. Enforced by byte-pin checks in verify.py." + }, + { + "local_path": "vendor/vanish.py", + "source_path": "research/f7-18point-tight-classes-seed4c1e7b30/vanish.py", + "pr": 2961, + "sha256": "6c605c54074f725321c5d770d538a652bf7727598a128270831f92fe7b9746d9", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from the immediate predecessor PR 3023's package research/f7-18point-avtail-seed010d26fa, which vendored it from PR 2961), credit Aaron Wang (navinor), PR 2961: the vanishing-character class tables and the L7 Sidon tight-equality lemma. Enforced by byte-pin checks in verify.py." + }, + { + "local_path": "vendor/agent64_cover17.py", + "source_path": "research/f7-18point-rows/agent64_cover17.py", + "pr": 2773, + "sha256": "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from the immediate predecessor PR 3023's package research/f7-18point-avtail-seed010d26fa, which vendored it from PR 2773), credit Aaron Wang (navinor), PR 2773: profile_c_values (PR 2773 pair-representation shape primitives). Enforced by byte-pin checks in verify.py." + }, + { + "local_path": "vendor/agent64_search17.py", + "source_path": "research/f7-18point-rows/agent64_search17.py", + "pr": 2773, + "sha256": "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from the immediate predecessor PR 3023's package research/f7-18point-avtail-seed010d26fa, which vendored it from PR 2773), credit Aaron Wang (navinor), PR 2773: the 17-point search primitives (PR 2773). Enforced by byte-pin checks in verify.py." + }, + { + "local_path": "vendor/anchors.py", + "source_path": "research/f7-18point-tight-classes-seed4c1e7b30/anchors.py", + "pr": 2961, + "sha256": "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7", + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from the immediate predecessor PR 3023's package research/f7-18point-avtail-seed010d26fa, which vendored it from PR 2961), credit Aaron Wang (navinor), PR 2961: the anchor-reproduction helpers. Enforced by byte-pin checks in verify.py." + } + ], + "notes": { + "concurrent_scopes": "Nicholas Stone (NicholasStone) PR 2973 (merged) and Nick Petalas (petalas) PR 3005 hold the f(7) WORD-level line (22 <= f(7) <= 24, a false-prune correction to the word-census parity budgets); PR 2973's scope note records bit 0 as valid in set-level searches and the set-level chain PR 2773-3023 as unaffected. This package is set-level only and enumerates no words. The pair-collision check (discussions 1317 and 1166 via agent_tools.py disc-comments --grep including nested replies) found no claim on the 18-point remainder (4,2)/(3,3)/(11,7)/(9,9) or the covering-split census.", + "model_and_pinned_results": "PR943 query model (research/universal-connector-boundary, Ross Richardson); pinned f(5)=12, f(6)=16 (research/universal-connector-six-source, Doug Colkitt) and the word-level gap 22 <= f(7) <= 24 (PR 2973/3005). Read and reproduced byte-exact: PR 2870 OBSTRUCTION 696/504/192, PR 2911 ROWS18 808/501/251/196 and NOVANISH, PR 2933 CLASSIFY cases=6720 TIGHT=2, PR 2961 FOURIER (7,1) need=175 lower=239 (all recomputed live from the vendored engines); PR 2961 CLASS82/CLASS60 and PR 3023 AV51 read back from PR 3023's per-shard receipts." + } +} diff --git a/research/f7-18point-remainder-kb3i-a1/TASK.json b/research/f7-18point-remainder-kb3i-a1/TASK.json new file mode 100644 index 0000000000..ad6c70758b --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/TASK.json @@ -0,0 +1,122 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "scope_key": "7084092dd726e7ba1f2f (drawn card); refined object key f7-18point-remainder-kb3i", + "track": "bit-mechanisms (drawn); scope changed to the assigned explicit open request kappa-blocker KB3i: the FINAL 18-point remainder for F2^7 - decide (12,6) A-vanish (4,2)/(3,3) and break the both-odd splits (11,7)/(9,9) (PR 3023's recorded remainder)", + "scope_status": "changed", + "scope_change_reason": "Authorized 'explicit open request' scope change, recorded as instructed by the assignment. The chooser (seed 80ba761410c9ac2a5210cedf738100a6, track bit-mechanisms) drew the cards bit-new-register-model / bit-helper-contract (a larger/nonabelian register model and a helper-mixing word; neither targets the F2^7 cover question, and the draw landed on bit-mechanisms cards rather than the set-level F2^7 track). The assignment (kappa-blocker KB3i) explicitly authorizes taking discussion 1166's open request instead - the FINAL 18-point remainder for F2^7 recorded by PR 3023 (its open questions 1-3): the surviving (12,6) A-vanish classes (4,2)/(3,3) and the both-odd splits (11,7)/(9,9) that carry no vanishing character. Pair-collision checks (discussions 1317 and 1166 via agent_tools.py disc-comments --grep including nested replies, before computation, plus a refined re-run with the object's proper names and synonyms) found no claim on this object; the concurrent f(7) work (PR 2973/PR 3005, Nicholas Stone / Nick Petalas) is WORD level and this task stays strictly on the SET level.", + "actual_scope": "Kappa-blocker KB3i (explicit open request; set level, no words): the FINAL 18-point remainder for F2^7 (exact condition P + P = F2^7 in the PR 943 prefix-walk model) - does ANY 18-point set cover F2^7? The 17-point question is closed (PR 2542/2773/2870); the 18-point splits (12,6),(11,7),(10,8),(9,9) survive (PR 2911); (10,8) is fully excluded (PR 2961); (12,6) A-vanish (5,1) is PROVEN impossible (PR 3023). REMAINDER taken here: (12,6) A-vanish (4,2) and (3,3), plus the both-odd splits (11,7) and (9,9). Delivered outcome=partial (narrowed remainder, no false kill): (a) (4,2)/(3,3) NOT decided (walk-ready reduced forms with budgets, walks too large for the session); (b) the both-odd parity shortcut to breaking (11,7)/(9,9) is PROVEN false by a complete m=3 census (both-odd reduced covers exist), the m=5 ground truth (F2^5 covers only in even splits (2,8)(4,6)(6,4)(8,2)) is established and its obstruction localized per split, and it is shown NOT to lift as a parity rule; the exact rho^2/identity frontier for (11,7)/(9,9) is reproduced and pinned (E_o=13/17, even_half_max=42/34, min sum rho^2=17/19); (c) bounded construction search finds no covering 18-set (best 118/128 at k=18, consistent with the 119/128 record ceiling).", + "bottleneck_link": "The set-level restricted addition basis value r((C2)^7) decides how small a universal word's prefix set can be inside the unchanged PR943 query model: 17-point covers are excluded and the 18-point question is narrowed to four splits, with the vanishing classes pressed (PR 2933/2961/3023). Under the concurrent word-level gap 22 <= f(7) <= 24 (PR 2973/3005), whether any 18-point set covers F2^7 is the deciding necessary condition for f(7) = 22: if none covers, every universal word at L=22 needs >= 19 distinct prefixes. This package narrows the remainder (demotes the parity shortcut, localizes the m=5 obstruction, pins the identity frontier) but decides no class outright. It changes no supplier, tariff or kappa and instantiates no physical interface.", + "stop_rule": "Stop at the first of: (a) a covering 18-set found in any surviving split (outcome (c), a construction), (b) one of (4,2)/(3,3)/(11,7)/(9,9) decided (PROVEN empty or a witness), or (c) the priced budget expiring with each class's exact status recorded. Outcome (c) reached: no class decided; the parity-shortcut route (b) pivoted once into the m=3/m=4 covering census which DEMOTED the shortcut and localized the m=5 obstruction, then stopped (one bounded pivot maximum). (4,2)/(3,3) recorded as exact walk-ready reductions with budgets (PR 3023's classification), not decided; (11,7)/(9,9) recorded at the rho^2/identity frontier, not excluded. No second pivot taken.", + "smallest_falsifying_instance_first": "The falsifying instance for 'no 18-point cover exists' is one covering 18-point set; for the both-odd parity hypothesis it is one covering both-odd reduced pair. The machinery was validated on the smallest instances first: all seven recorded anchors reproduced before any new number (FOURIER 7,1 =175/239, OBSTRUCTION 696/504/192, CLASSIFY 32=32 TIGHT cases=6720 recomputed live; CLASS82/CLASS60/AV51 read back from PR 3023's receipts). The parity hypothesis was then tested at the SMALLEST instance (m=3 complete census, 2^8 x 2^8 subset pairs) where covers are known to exist, so a false-empty is distinguishable from broken machinery (m=3 (5,5) has 3136 covers, (7,7) has 64). The m=5 ground truth was confirmed by complete m=4 sum-10 censuses (both-even (2,8)=15360,(4,6)=143360 cover; both-odd (1,9),(3,7),(5,5) empty) and the (5,5) self-obstruction localized (4,085,760 cross-covering pairs, all fail self, max self-union 15/16).", + "outcome": "partial", + "author": "Aaron Wang", + "ai_assistance": "Substantial AI assistance from opencode in scoping, implementation, verification and writing (no model named); no independent human review claimed.", + "evidence": "CERTIFICATE.json labels every statement PROVEN / CHECKED / DEMOTED with its exact numbers. verify.py re-derives every cited number (three modes: quick = anchors + the complete m=3 parity-demotion census + the (11,7)/(9,9) frontier; full = the complete m=4 sum-10 censuses (m=5 ground truth) + the (5,5) self-obstruction localization; search = the bounded construction ceiling). parity_census.py is the complete reduced-covering census (m=3 exhaustive 2^8 x 2^8); split_census.py is the per-split complete census with a cross/self failure breakdown; self_obstruction.py localizes the (5,5) self failure (selfsum sizes, ranks, self-union deficit); fourier_probe.py prints the rho^2/identity numbers; construct_search.py is the bounded seeded construction search. The six vendored engines are byte-exact with SHA-256 pins (verify.py check_pins). Anchors reproduced before any new number (see README): PR 2870 OBSTRUCTION 696/504/192 and PR 2911 ROWS18/NOVANISH, PR 2933 CLASSIFY cases=6720 TIGHT=2, PR 2961 FOURIER (7,1) need=175 lower=239 recomputed live; CLASS82 checked=28,815,360 covering=0, CLASS60 d_checked=169,911, PR 3023 AV51 uv_pairs=3,049,492,320 covering=0 read back from PR 3023's per-shard receipts (values match exactly).", + "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 complete exact-integer enumerations with brute-force-validated censuses.", + "open_questions": [ + { + "question": "Push the even-half (self-sum) coverage identity for (11,7)/(9,9) (PR 2961's open question 2): what identity couples odd-line cross-sum multiplicities to even-line selfsums where no character can vanish and sum rho^2 >= 17/19 does not contradict?", + "why_it_matters": "These two both-odd splits carry the other half of the 18-point question (row remainders 501/196); the PR 2870 squeeze uses only odd coverage and requires opposite parity, so the un-pushed even-half (self-sum) direction is the one route left to break them.", + "first_step": "Derive the even-half self-sum multiplicities ((A+A) u (D+D) = E) at the 501/196 surviving rows and check them against every cover of F2^5 (PR 2933's census) before lifting to m=6.", + "blocked_by": "No known coupling identity between odd-line cross-sum multiplicities and even-line selfsums (PR 2961 recorded the same blocker); the parity shortcut is DEMOTED (both-odd covers exist at m=3), so no self-sum-size argument is available either." + }, + { + "question": "Decide (12,6) A-vanish (4,2): does the exact reduced form (W 4-sets, D1 = {0,1}) admit a covering (U,V,W) triple?", + "why_it_matters": "(4,2) is the next surviving (12,6) class after (5,1)'s exclusion; clearing it forces any (12,6) A-vanish cover into (3,3).", + "first_step": "Extend the (5,1) walk to W 4-sets and D1 = {0,1}: enumerate normalized pairs (U,V) with |U+V| >= 24 and per pair the W candidates with M = F2^5 \\ (U+V) in W u (W+1), testing the four reduced lines exactly; shard over normalized U with per-shard receipts and generous budgets (PR 3023's lesson: 3000 s was too small).", + "blocked_by": "Nothing structural; the walk is strictly larger than (5,1)'s 3,049,492,320-pair walk (need 24 vs 27 and looser W), a few hours of sharded walk beyond this session's budget." + }, + { + "question": "Decide or identify (12,6) A-vanish (3,3): is it realizable, and does any coupling of the four slack L3 lines exclude it?", + "why_it_matters": "(3,3) is the last A-vanish class after (4,2); excluding all three A-vanish tail classes would leave (12,6) covers dependent on D-vanish (9,3)/(8,4)/(7,5)/(6,6) only.", + "first_step": "Set up the exact normalized enumeration for (A0,A1 6-sets, D0,D1 3-sets) with 0 in A0, 0 in A1 and complete the four-line test per configuration, or derive a cross-line multiplicity identity coupling (I)/(II) with (III)/(IV).", + "blocked_by": "No forced structure: all four line budgets are slack at (3,3) (line IV: 36+9 against 32); the direct configuration space needs a new reduction or a much larger walk." + }, + { + "question": "Find a valid lift of the (5,5) self-sum obstruction to (9,9): at what m/split threshold, if any, does a self-sum-size bound forbid a both-odd self cover?", + "why_it_matters": "The m=4 mechanism (|A+A| <= 11 for cross-covering (5,5), self-union <= 15/16) is scale-dependent and fails at m=3 ((5,5) covers); a valid threshold would decide (9,9).", + "first_step": "Enumerate cross-covering (k,k) both-odd pairs at m=3 and m=4 and record the selfsum-size bound versus m; determine whether a rank/doubling invariant forces |A+A| below the covering threshold for m >= 4.", + "blocked_by": "The selfsum bound is not monotone in m (both-odd covers exist at m=3), so no general invariant is yet identified." + } + ], + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "base_commit": "d8e0f83f00191df62174b641e9fff055c357f641", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "session_seed": "80ba761410c9ac2a5210cedf738100a6", + "priced_budget_minutes": 150, + "priced_budget_breakdown": "25 min entry orientation (task draw, pair-collision checks on discussions 1317/1166, overlap terms); 20 min predecessor extraction (PR 3023 pr-tree-extract to scratch, hash pins, author verification) and anchor reproduction (FOURIER/OBSTRUCTION/CLASSIFY/ROWS18/NOVANISH recomputed live; CLASS82/CLASS60/AV51 read back from receipts); 15 min the m=3 complete parity-demotion census and the (11,7)/(9,9) identity-frontier probe; 25 min the m=4 sum-10 ground-truth censuses and the (5,5) self-obstruction localization (cross-checking split_census.py vs self_obstruction.py vs verify.py full); 15 min the bounded construction search; 30 min package metadata, registration (--check-only), PR markdown gates, PR and board posts.", + "object_synonyms_used_in_overlap": [ + "18-point", + "18point", + "18-set", + "A-vanish", + "(4,2)", + "(3,3)", + "(11,7)", + "(9,9)", + "AV-tail", + "vanishing character", + "P+P cover", + "P + P", + "F2^7", + "cover of F2^7", + "rho", + "cross-sum", + "even-half coverage", + "self-sum", + "universal word", + "L=22", + "f(7)", + "both-odd", + "parity split" + ], + "pair_collision_check": { + "checked_utc": "2026-10-16 entry (before computation) and a refined re-run before heavy computation", + "result": "No claim on the 18-point set-level remainder (4,2)/(3,3)/(11,7)/(9,9) or the covering-split census at any check. Discussion 1317 carries only word-level union-support posts (petalas, 16:41Z/17:01Z, PR 3005 corroboration of PR 2973) and bit-mechanism claims; nothing on this object. Discussion 1166's recent posts are the predecessor/released lineage (KB3d 17-point complete, KB5d/KB5e F-star residue) plus other tracks; no CLAIM on the 18-point remainder. The concurrent f(7) line (PR 2973 Nicholas Stone, merged; PR 3005 Nick Petalas) is WORD level (22 <= f(7) <= 24) and explicitly scopes the set-level chain PR 2773-3023 as unaffected. This package stays strictly on the SET level and enumerates no words.", + "threads_scanned": [ + "discussion 1317 full scan (agent_tools.py disc-comments --since 2026-10-16, incl. nested replies) + grep for 18-point/A-vanish/(4,2)/(3,3)/(11,7)/(9,9)/AV-tail/F2^7/KB3i", + "discussion 1166 full scan (agent_tools.py disc-comments --since 2026-10-16, incl. nested replies) + grep for the object's proper names and synonyms" + ], + "tool": "agent_tools.py disc-comments --grep (with nested replies); timestamps used to scope to the last few hours" + } +} diff --git a/research/f7-18point-remainder-kb3i-a1/VERIFY.json b/research/f7-18point-remainder-kb3i-a1/VERIFY.json new file mode 100644 index 0000000000..a775e7fb42 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/VERIFY.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-remainder-kb3i-a1/verify.py", + "quick" + ], + "checks": "Byte pins of the six vendored engines; anchor reproduction (PR 2961 FOURIER (7,1) need=175 lower=239, PR 2933 CLASSIFY tight-equality Sidon cases=6720 and 32=32 TIGHT count=2, PR 2870 OBSTRUCTION 696/504/192); the complete m=3 reduced-covering census (parity-shortcut DEMOTION: both-odd covers exist, (5,5)=3136, (7,7)=64, (3,3)=0); the (11,7)/(9,9) identity-frontier numbers (E_o=13/17, even_half_max=42/34).", + "timeout_seconds": 60 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-remainder-kb3i-a1/verify.py", + "full" + ], + "checks": "quick plus the complete m=4 sum-10 split censuses (the m=5 ground truth: (2,8)=15360 and (4,6)=143360 cover; (1,9),(3,7),(5,5) empty) and the (5,5) self-obstruction localization (4,085,760 cross-covering pairs, self_covering_when_cross=0, max self-union=15/16). Complete enumerations: a zero count PROVES the split empty at that (m, split).", + "timeout_seconds": 600 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "research/f7-18point-remainder-kb3i-a1/verify.py", + "search" + ], + "checks": "The bounded construction search ceiling (route c): no covering 18-set found, best coverage 118/128 at k=18 (record ceiling 119/128, PR 2634).", + "timeout_seconds": 120 + } + ], + "inputs": [ + "research/f7-18point-remainder-kb3i-a1/verify.py", + "research/f7-18point-remainder-kb3i-a1/parity_census.py", + "research/f7-18point-remainder-kb3i-a1/split_census.py", + "research/f7-18point-remainder-kb3i-a1/self_obstruction.py", + "research/f7-18point-remainder-kb3i-a1/fourier_probe.py", + "research/f7-18point-remainder-kb3i-a1/construct_search.py", + "research/f7-18point-remainder-kb3i-a1/vendor/tight.py", + "research/f7-18point-remainder-kb3i-a1/vendor/cover18.py", + "research/f7-18point-remainder-kb3i-a1/vendor/vanish.py", + "research/f7-18point-remainder-kb3i-a1/vendor/agent64_cover17.py", + "research/f7-18point-remainder-kb3i-a1/vendor/agent64_search17.py", + "research/f7-18point-remainder-kb3i-a1/vendor/anchors.py" + ] +} diff --git a/research/f7-18point-remainder-kb3i-a1/_assemble.py b/research/f7-18point-remainder-kb3i-a1/_assemble.py new file mode 100644 index 0000000000..8aae56c2b6 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/_assemble.py @@ -0,0 +1,284 @@ +"""Assemble TASK.json / SOURCES.json / VERIFY.json for the KB3i package, +embedding the drawn catalogue card verbatim so the checker's original_card +dict-equality holds. Writes each file with LF newlines (byte-stable replay).""" + +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.stdout.reconfigure(encoding="utf-8") + +BASE = "d8e0f83f00191df62174b641e9fff055c357f641" +PKG = "research/f7-18point-remainder-kb3i-a1" + +card = json.load(open(HERE / "_card.json", encoding="utf-8")) + +provenance = [ + {"path": "docs/research/agent-task-catalog.json", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "usage": "provenance"}, + {"path": "certificates/selected-result.json", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "usage": "provenance"}, +] + +vendored = [ + ("vendor/tight.py", "14670ef2d3df9e4ecc9e1db962f4e8cb77545d1c889144352760c1fd14e2273b", 2961, + "bitmask primitives, the (7,1) Fourier identity, rho classification"), + ("vendor/cover18.py", "24c6a2f4911dc2d5de76972eb5ae93dc4e66d8fa1e904443de6d0638e70c0a04", 2961, + "the reduced (A,D) covering model, Fourier profile system, squeeze numbers, pair-representation rows, bounded search"), + ("vendor/vanish.py", "6c605c54074f725321c5d770d538a652bf7727598a128270831f92fe7b9746d9", 2961, + "the vanishing-character class tables and the L7 Sidon tight-equality lemma"), + ("vendor/agent64_cover17.py", "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654", 2773, + "profile_c_values (PR 2773 pair-representation shape primitives)"), + ("vendor/agent64_search17.py", "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674", 2773, + "the 17-point search primitives (PR 2773)"), + ("vendor/anchors.py", "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7", 2961, + "the anchor-reproduction helpers"), +] + +references = [ + { + "local_path": lp, + "source_path": "research/f7-18point-tight-classes-seed4c1e7b30/" + lp.split("/")[1] + if pr == 2961 else "research/f7-18point-rows/" + lp.split("/")[1], + "pr": pr, + "sha256": sha, + "note": "Vendored byte-exact (extracted with agent_tools.py pr-tree-extract from the immediate predecessor " + "PR 3023's package research/f7-18point-avtail-seed010d26fa, which vendored it from PR %d), credit " + "Aaron Wang (navinor), PR %d: %s. Enforced by byte-pin checks in verify.py." % (pr, pr, what), + } + for (lp, sha, pr, what) in vendored +] + +task = { + "schema_version": 1, + "task_id": "bit-new-register-model", + "scope_key": "7084092dd726e7ba1f2f (drawn card); refined object key f7-18point-remainder-kb3i", + "track": "bit-mechanisms (drawn); scope changed to the assigned explicit open request kappa-blocker KB3i: " + "the FINAL 18-point remainder for F2^7 - decide (12,6) A-vanish (4,2)/(3,3) and break the both-odd " + "splits (11,7)/(9,9) (PR 3023's recorded remainder)", + "scope_status": "changed", + "scope_change_reason": "Authorized 'explicit open request' scope change, recorded as instructed by the assignment. " + "The chooser (seed 80ba761410c9ac2a5210cedf738100a6, track bit-mechanisms) drew the cards " + "bit-new-register-model / bit-helper-contract (a larger/nonabelian register model and a helper-mixing word; " + "neither targets the F2^7 cover question, and the draw landed on bit-mechanisms cards rather than the " + "set-level F2^7 track). The assignment (kappa-blocker KB3i) explicitly authorizes taking discussion 1166's " + "open request instead - the FINAL 18-point remainder for F2^7 recorded by PR 3023 (its open questions 1-3): " + "the surviving (12,6) A-vanish classes (4,2)/(3,3) and the both-odd splits (11,7)/(9,9) that carry no " + "vanishing character. Pair-collision checks (discussions 1317 and 1166 via agent_tools.py disc-comments " + "--grep including nested replies, before computation, plus a refined re-run with the object's proper names " + "and synonyms) found no claim on this object; the concurrent f(7) work (PR 2973/PR 3005, Nicholas Stone / " + "Nick Petalas) is WORD level and this task stays strictly on the SET level.", + "actual_scope": "Kappa-blocker KB3i (explicit open request; set level, no words): the FINAL 18-point remainder " + "for F2^7 (exact condition P + P = F2^7 in the PR 943 prefix-walk model) - does ANY 18-point set cover F2^7? " + "The 17-point question is closed (PR 2542/2773/2870); the 18-point splits (12,6),(11,7),(10,8),(9,9) survive " + "(PR 2911); (10,8) is fully excluded (PR 2961); (12,6) A-vanish (5,1) is PROVEN impossible (PR 3023). " + "REMAINDER taken here: (12,6) A-vanish (4,2) and (3,3), plus the both-odd splits (11,7) and (9,9). " + "Delivered outcome=partial (narrowed remainder, no false kill): (a) (4,2)/(3,3) NOT decided (walk-ready " + "reduced forms with budgets, walks too large for the session); (b) the both-odd parity shortcut to breaking " + "(11,7)/(9,9) is PROVEN false by a complete m=3 census (both-odd reduced covers exist), the m=5 ground truth " + "(F2^5 covers only in even splits (2,8)(4,6)(6,4)(8,2)) is established and its obstruction localized per " + "split, and it is shown NOT to lift as a parity rule; the exact rho^2/identity frontier for (11,7)/(9,9) is " + "reproduced and pinned (E_o=13/17, even_half_max=42/34, min sum rho^2=17/19); (c) bounded construction " + "search finds no covering 18-set (best 118/128 at k=18, consistent with the 119/128 record ceiling).", + "bottleneck_link": "The set-level restricted addition basis value r((C2)^7) decides how small a universal word's " + "prefix set can be inside the unchanged PR943 query model: 17-point covers are excluded and the 18-point " + "question is narrowed to four splits, with the vanishing classes pressed (PR 2933/2961/3023). Under the " + "concurrent word-level gap 22 <= f(7) <= 24 (PR 2973/3005), whether any 18-point set covers F2^7 is the " + "deciding necessary condition for f(7) = 22: if none covers, every universal word at L=22 needs >= 19 " + "distinct prefixes. This package narrows the remainder (demotes the parity shortcut, localizes the m=5 " + "obstruction, pins the identity frontier) but decides no class outright. It changes no supplier, tariff or " + "kappa and instantiates no physical interface.", + "stop_rule": "Stop at the first of: (a) a covering 18-set found in any surviving split (outcome (c), a " + "construction), (b) one of (4,2)/(3,3)/(11,7)/(9,9) decided (PROVEN empty or a witness), or (c) the priced " + "budget expiring with each class's exact status recorded. Outcome (c) reached: no class decided; the " + "parity-shortcut route (b) pivoted once into the m=3/m=4 covering census which DEMOTED the shortcut and " + "localized the m=5 obstruction, then stopped (one bounded pivot maximum). (4,2)/(3,3) recorded as exact " + "walk-ready reductions with budgets (PR 3023's classification), not decided; (11,7)/(9,9) recorded at the " + "rho^2/identity frontier, not excluded. No second pivot taken.", + "smallest_falsifying_instance_first": "The falsifying instance for 'no 18-point cover exists' is one covering " + "18-point set; for the both-odd parity hypothesis it is one covering both-odd reduced pair. The machinery was " + "validated on the smallest instances first: all seven recorded anchors reproduced before any new number " + "(FOURIER 7,1 =175/239, OBSTRUCTION 696/504/192, CLASSIFY 32=32 TIGHT cases=6720 recomputed live; " + "CLASS82/CLASS60/AV51 read back from PR 3023's receipts). The parity hypothesis was then tested at the " + "SMALLEST instance (m=3 complete census, 2^8 x 2^8 subset pairs) where covers are known to exist, so a " + "false-empty is distinguishable from broken machinery (m=3 (5,5) has 3136 covers, (7,7) has 64). The m=5 " + "ground truth was confirmed by complete m=4 sum-10 censuses (both-even (2,8)=15360,(4,6)=143360 cover; " + "both-odd (1,9),(3,7),(5,5) empty) and the (5,5) self-obstruction localized (4,085,760 cross-covering pairs, " + "all fail self, max self-union 15/16).", + "outcome": "partial", + "author": "Aaron Wang", + "ai_assistance": "Substantial AI assistance from opencode in scoping, implementation, verification and writing " + "(no model named); no independent human review claimed.", + "evidence": "CERTIFICATE.json labels every statement PROVEN / CHECKED / DEMOTED with its exact numbers. " + "verify.py re-derives every cited number (three modes: quick = anchors + the complete m=3 parity-demotion " + "census + the (11,7)/(9,9) frontier; full = the complete m=4 sum-10 censuses (m=5 ground truth) + the (5,5) " + "self-obstruction localization; search = the bounded construction ceiling). parity_census.py is the complete " + "reduced-covering census (m=3 exhaustive 2^8 x 2^8); split_census.py is the per-split complete census with a " + "cross/self failure breakdown; self_obstruction.py localizes the (5,5) self failure (selfsum sizes, ranks, " + "self-union deficit); fourier_probe.py prints the rho^2/identity numbers; construct_search.py is the bounded " + "seeded construction search. The six vendored engines are byte-exact with SHA-256 pins (verify.py check_pins). " + "Anchors reproduced before any new number (see README): PR 2870 OBSTRUCTION 696/504/192 and PR 2911 " + "ROWS18/NOVANISH, PR 2933 CLASSIFY cases=6720 TIGHT=2, PR 2961 FOURIER (7,1) need=175 lower=239 recomputed " + "live; CLASS82 checked=28,815,360 covering=0, CLASS60 d_checked=169,911, PR 3023 AV51 uv_pairs=3,049,492,320 " + "covering=0 read back from PR 3023's per-shard receipts (values match exactly).", + "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 complete exact-integer enumerations with brute-force-validated " + "censuses.", + "open_questions": [ + {"question": "Push the even-half (self-sum) coverage identity for (11,7)/(9,9) (PR 2961's open question 2): " + "what identity couples odd-line cross-sum multiplicities to even-line selfsums where no character " + "can vanish and sum rho^2 >= 17/19 does not contradict?", + "why_it_matters": "These two both-odd splits carry the other half of the 18-point question (row remainders " + "501/196); the PR 2870 squeeze uses only odd coverage and requires opposite parity, so the " + "un-pushed even-half (self-sum) direction is the one route left to break them.", + "first_step": "Derive the even-half self-sum multiplicities ((A+A) u (D+D) = E) at the 501/196 surviving rows " + "and check them against every cover of F2^5 (PR 2933's census) before lifting to m=6.", + "blocked_by": "No known coupling identity between odd-line cross-sum multiplicities and even-line selfsums " + "(PR 2961 recorded the same blocker); the parity shortcut is DEMOTED (both-odd covers exist at " + "m=3), so no self-sum-size argument is available either."}, + {"question": "Decide (12,6) A-vanish (4,2): does the exact reduced form (W 4-sets, D1 = {0,1}) admit a " + "covering (U,V,W) triple?", + "why_it_matters": "(4,2) is the next surviving (12,6) class after (5,1)'s exclusion; clearing it forces any " + "(12,6) A-vanish cover into (3,3).", + "first_step": "Extend the (5,1) walk to W 4-sets and D1 = {0,1}: enumerate normalized pairs (U,V) with " + "|U+V| >= 24 and per pair the W candidates with M = F2^5 \\ (U+V) in W u (W+1), testing the " + "four reduced lines exactly; shard over normalized U with per-shard receipts and generous " + "budgets (PR 3023's lesson: 3000 s was too small).", + "blocked_by": "Nothing structural; the walk is strictly larger than (5,1)'s 3,049,492,320-pair walk (need 24 " + "vs 27 and looser W), a few hours of sharded walk beyond this session's budget."}, + {"question": "Decide or identify (12,6) A-vanish (3,3): is it realizable, and does any coupling of the four " + "slack L3 lines exclude it?", + "why_it_matters": "(3,3) is the last A-vanish class after (4,2); excluding all three A-vanish tail classes " + "would leave (12,6) covers dependent on D-vanish (9,3)/(8,4)/(7,5)/(6,6) only.", + "first_step": "Set up the exact normalized enumeration for (A0,A1 6-sets, D0,D1 3-sets) with 0 in A0, 0 in " + "A1 and complete the four-line test per configuration, or derive a cross-line multiplicity " + "identity coupling (I)/(II) with (III)/(IV).", + "blocked_by": "No forced structure: all four line budgets are slack at (3,3) (line IV: 36+9 against 32); the " + "direct configuration space needs a new reduction or a much larger walk."}, + {"question": "Find a valid lift of the (5,5) self-sum obstruction to (9,9): at what m/split threshold, if any, " + "does a self-sum-size bound forbid a both-odd self cover?", + "why_it_matters": "The m=4 mechanism (|A+A| <= 11 for cross-covering (5,5), self-union <= 15/16) is " + "scale-dependent and fails at m=3 ((5,5) covers); a valid threshold would decide (9,9).", + "first_step": "Enumerate cross-covering (k,k) both-odd pairs at m=3 and m=4 and record the selfsum-size " + "bound versus m; determine whether a rank/doubling invariant forces |A+A| below the covering " + "threshold for m >= 4.", + "blocked_by": "The selfsum bound is not monotone in m (both-odd covers exist at m=3), so no general invariant " + "is yet identified."}, + ], + "original_card": card, + "base_commit": BASE, + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "session_seed": "80ba761410c9ac2a5210cedf738100a6", + "priced_budget_minutes": 150, + "priced_budget_breakdown": "25 min entry orientation (task draw, pair-collision checks on discussions 1317/1166, " + "overlap terms); 20 min predecessor extraction (PR 3023 pr-tree-extract to scratch, hash pins, author " + "verification) and anchor reproduction (FOURIER/OBSTRUCTION/CLASSIFY/ROWS18/NOVANISH recomputed live; " + "CLASS82/CLASS60/AV51 read back from receipts); 15 min the m=3 complete parity-demotion census and the " + "(11,7)/(9,9) identity-frontier probe; 25 min the m=4 sum-10 ground-truth censuses and the (5,5) " + "self-obstruction localization (cross-checking split_census.py vs self_obstruction.py vs verify.py full); " + "15 min the bounded construction search; 30 min package metadata, registration (--check-only), PR markdown " + "gates, PR and board posts.", + "object_synonyms_used_in_overlap": [ + "18-point", "18point", "18-set", "A-vanish", "(4,2)", "(3,3)", "(11,7)", "(9,9)", "AV-tail", + "vanishing character", "P+P cover", "P + P", "F2^7", "cover of F2^7", "rho", "cross-sum", + "even-half coverage", "self-sum", "universal word", "L=22", "f(7)", "both-odd", "parity split", + ], + "pair_collision_check": { + "checked_utc": "2026-10-16 entry (before computation) and a refined re-run before heavy computation", + "result": "No claim on the 18-point set-level remainder (4,2)/(3,3)/(11,7)/(9,9) or the covering-split " + "census at any check. Discussion 1317 carries only word-level union-support posts (petalas, " + "16:41Z/17:01Z, PR 3005 corroboration of PR 2973) and bit-mechanism claims; nothing on this " + "object. Discussion 1166's recent posts are the predecessor/released lineage (KB3d 17-point " + "complete, KB5d/KB5e F-star residue) plus other tracks; no CLAIM on the 18-point remainder. The " + "concurrent f(7) line (PR 2973 Nicholas Stone, merged; PR 3005 Nick Petalas) is WORD level " + "(22 <= f(7) <= 24) and explicitly scopes the set-level chain PR 2773-3023 as unaffected. This " + "package stays strictly on the SET level and enumerates no words.", + "threads_scanned": [ + "discussion 1317 full scan (agent_tools.py disc-comments --since 2026-10-16, incl. nested replies) + " + "grep for 18-point/A-vanish/(4,2)/(3,3)/(11,7)/(9,9)/AV-tail/F2^7/KB3i", + "discussion 1166 full scan (agent_tools.py disc-comments --since 2026-10-16, incl. nested replies) + " + "grep for the object's proper names and synonyms", + ], + "tool": "agent_tools.py disc-comments --grep (with nested replies); timestamps used to scope to the last few " + "hours", + }, +} + +sources = { + "schema_version": 1, + "base_commit": BASE, + "files": provenance, + "references": references, + "notes": { + "concurrent_scopes": "Nicholas Stone (NicholasStone) PR 2973 (merged) and Nick Petalas (petalas) PR 3005 " + "hold the f(7) WORD-level line (22 <= f(7) <= 24, a false-prune correction to the word-census parity " + "budgets); PR 2973's scope note records bit 0 as valid in set-level searches and the set-level chain " + "PR 2773-3023 as unaffected. This package is set-level only and enumerates no words. The pair-collision " + "check (discussions 1317 and 1166 via agent_tools.py disc-comments --grep including nested replies) " + "found no claim on the 18-point remainder (4,2)/(3,3)/(11,7)/(9,9) or the covering-split census.", + "model_and_pinned_results": "PR943 query model (research/universal-connector-boundary, Ross Richardson); " + "pinned f(5)=12, f(6)=16 (research/universal-connector-six-source, Doug Colkitt) and the word-level gap " + "22 <= f(7) <= 24 (PR 2973/3005). Read and reproduced byte-exact: PR 2870 OBSTRUCTION 696/504/192, " + "PR 2911 ROWS18 808/501/251/196 and NOVANISH, PR 2933 CLASSIFY cases=6720 TIGHT=2, PR 2961 FOURIER " + "(7,1) need=175 lower=239 (all recomputed live from the vendored engines); PR 2961 CLASS82/CLASS60 and " + "PR 3023 AV51 read back from PR 3023's per-shard receipts.", + }, +} + +verify = { + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "commands": [ + {"argv": ["{python}", "-I", "-B", "research/f7-18point-remainder-kb3i-a1/verify.py", "quick"], + "checks": "Byte pins of the six vendored engines; anchor reproduction (PR 2961 FOURIER (7,1) need=175 " + "lower=239, PR 2933 CLASSIFY tight-equality Sidon cases=6720 and 32=32 TIGHT count=2, PR 2870 " + "OBSTRUCTION 696/504/192); the complete m=3 reduced-covering census (parity-shortcut DEMOTION: " + "both-odd covers exist, (5,5)=3136, (7,7)=64, (3,3)=0); the (11,7)/(9,9) identity-frontier numbers " + "(E_o=13/17, even_half_max=42/34).", + "timeout_seconds": 60}, + {"argv": ["{python}", "-I", "-B", "research/f7-18point-remainder-kb3i-a1/verify.py", "full"], + "checks": "quick plus the complete m=4 sum-10 split censuses (the m=5 ground truth: (2,8)=15360 and " + "(4,6)=143360 cover; (1,9),(3,7),(5,5) empty) and the (5,5) self-obstruction localization " + "(4,085,760 cross-covering pairs, self_covering_when_cross=0, max self-union=15/16). Complete " + "enumerations: a zero count PROVES the split empty at that (m, split).", + "timeout_seconds": 600}, + {"argv": ["{python}", "-I", "-B", "research/f7-18point-remainder-kb3i-a1/verify.py", "search"], + "checks": "The bounded construction search ceiling (route c): no covering 18-set found, best coverage " + "118/128 at k=18 (record ceiling 119/128, PR 2634).", + "timeout_seconds": 120}, + ], + "inputs": [ + "research/f7-18point-remainder-kb3i-a1/verify.py", + "research/f7-18point-remainder-kb3i-a1/parity_census.py", + "research/f7-18point-remainder-kb3i-a1/split_census.py", + "research/f7-18point-remainder-kb3i-a1/self_obstruction.py", + "research/f7-18point-remainder-kb3i-a1/fourier_probe.py", + "research/f7-18point-remainder-kb3i-a1/construct_search.py", + "research/f7-18point-remainder-kb3i-a1/vendor/tight.py", + "research/f7-18point-remainder-kb3i-a1/vendor/cover18.py", + "research/f7-18point-remainder-kb3i-a1/vendor/vanish.py", + "research/f7-18point-remainder-kb3i-a1/vendor/agent64_cover17.py", + "research/f7-18point-remainder-kb3i-a1/vendor/agent64_search17.py", + "research/f7-18point-remainder-kb3i-a1/vendor/anchors.py", + ], +} + + +def dump(name, obj): + with open(HERE / name, "w", encoding="utf-8", newline="\n") as f: + json.dump(obj, f, indent=2, ensure_ascii=False) + f.write("\n") + print("wrote", name) + + +dump("TASK.json", task) +dump("SOURCES.json", sources) +dump("VERIFY.json", verify) diff --git a/research/f7-18point-remainder-kb3i-a1/_card.json b/research/f7-18point-remainder-kb3i-a1/_card.json new file mode 100644 index 0000000000..c853900870 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/_card.json @@ -0,0 +1,40 @@ +{ + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] +} \ No newline at end of file diff --git a/research/f7-18point-remainder-kb3i-a1/_emit_meta.py b/research/f7-18point-remainder-kb3i-a1/_emit_meta.py new file mode 100644 index 0000000000..a72bf32351 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/_emit_meta.py @@ -0,0 +1,44 @@ +"""Emit the drawn catalogue card verbatim and the provenance blob pins at the +base commit, so TASK.json original_card equals the pinned card object exactly +and SOURCES.json provenance rows bind through the base-commit git blobs.""" + +import hashlib +import json +import subprocess +import sys + +sys.stdout.reconfigure(encoding="utf-8") + +BASE = "d8e0f83f00191df62174b641e9fff055c357f641" +CAT = "docs/research/agent-task-catalog.json" +SEL = "certificates/selected-result.json" + + +def git_blob_sha(path): + return subprocess.run(["git", "rev-parse", BASE + ":" + path], + capture_output=True, check=True).stdout.decode().strip() + + +def sha256_file(path): + return hashlib.sha256(open(path, "rb").read()).hexdigest() + + +def main(): + catalog = json.load(open(CAT, encoding="utf-8")) + wanted = "bit-new-register-model" + cards = [t for tr in catalog["tracks"] for t in tr["tasks"] if t["id"] == wanted] + assert len(cards) == 1, ("card count", len(cards)) + card = cards[0] + with open("research/f7-18point-remainder-kb3i-a1/_card.json", "w", encoding="utf-8", newline="\n") as f: + json.dump(card, f, indent=2, ensure_ascii=False) + print("CARD id=%s track-scope-key=%s" % (card["id"], card.get("scope_key"))) + rows = [] + for p in (CAT, SEL): + rows.append({"path": p, "git_blob": git_blob_sha(p), "sha256": sha256_file(p), + "usage": "provenance"}) + print("PROVENANCE_ROWS=" + json.dumps(rows)) + print("BASE=" + BASE) + + +if __name__ == "__main__": + main() diff --git a/research/f7-18point-remainder-kb3i-a1/construct_search.py b/research/f7-18point-remainder-kb3i-a1/construct_search.py new file mode 100644 index 0000000000..fe7513766e --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/construct_search.py @@ -0,0 +1,45 @@ +"""Route KB3i-c: bounded construction search for an 18-point cover of F2^7 +(P+P = F2^7) and for reduced covering (A,B) pairs in the surviving splits. +This is a SEEDED, BOUNDED search: a found cover is a WITNESS (falsifies +"no 18-point cover exists"); a failed bounded search is recorded as a scoped +search failure (search ceiling), never as an exclusion. Exact integer +arithmetic; reuses the byte-vendored PR 2961/2773 search primitives. +""" + +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "vendor")) +sys.stdout.reconfigure(encoding="utf-8") + +import cover18 as c18 # noqa: E402 + +# FLOORS per PR 2911 (matches verify.py mode_rows). +FLOORS = {12: 3, 11: 5, 10: 3, 9: 0} + + +def run(): + # Direct 18-point search on F2^7 (route c, top level). + print("=== search_direct k=18 on F2^7 (bounded 25 s, seeds 1..3) ===") + best = 0 + for seed in (1, 2, 3): + rec = c18.search_direct(k=18, restarts=40, seed=seed, seconds=25.0, n=7) + print(" seed=%d found=%s score=%d/%d" % (seed, rec["found"], rec["score"], 128)) + best = max(best, rec["score"]) + if rec["found"]: + print(" WITNESS S=%s" % rec["S"]) + break + print(" best coverage this run = %d/128 (record search ceiling 119/128 at k=18)" % best) + + # Reduced (A,B) split searches (surviving splits only). + for (s, t) in ((12, 6), (11, 7), (10, 8), (9, 9)): + print("=== search_split (%d,%d) reduced on F2^6 (bounded 15 s, seed 1) ===" % (s, t)) + rec = c18.search_split(s, t, restarts=20, seed=1, seconds=15.0, n=7) + print(" found=%s score=%d/128 (target cross+self = 128)" % (rec["found"], rec["score"])) + if rec["found"]: + print(" WITNESS A=%s D=%s" % (rec["A"], rec["D"])) + + +if __name__ == "__main__": + run() diff --git a/research/f7-18point-remainder-kb3i-a1/fourier_probe.py b/research/f7-18point-remainder-kb3i-a1/fourier_probe.py new file mode 100644 index 0000000000..0d10446773 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/fourier_probe.py @@ -0,0 +1,52 @@ +"""Fourier / identity numbers for the both-odd surviving splits (11,7)/(9,9) +of the 18-point question (route KB3i-b), read from the byte-vendored PR 2961 +engine cover18.py. No new arithmetic; this prints the recorded identity +conditions so the even-half / rho-square frontier is explicit.""" + +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "vendor")) +sys.stdout.reconfigure(encoding="utf-8") + +import cover18 as c18 # noqa: E402 + + +def show(s, t): + n = 7 + print("=== split (%d,%d) n=7 (E=F2^6, |A|+|B|=%d) ===" % (s, t, s + t)) + eo = s * t - (1 << (n - 1)) + print(" odd_excess E_o = s*t - 2^(n-1) = %d" % eo) + print(" even_half_max (self-sum bound) = %d" % c18.even_half_max(n, s, t)) + # rho square attainable values and the min + if eo <= 24: + vals = c18.rho_square_values(eo) + print(" attainable sum rho^2 (partition square sums of E_o=%d): %s" % (eo, vals)) + print(" min sum rho^2 = %d, max = %d" % (vals[0], vals[-1])) + else: + print(" E_o=%d out of rho budget (>24): not attempted" % eo) + if "--full" in sys.argv: + for nzb in (False, True): + rec = c18.fourier_profile_feasibility(n, s, t, nonzero_both=nzb) + print(" fourier_profile_feasibility(nonzero_both=%s): feasible=%s" + % (nzb, rec["feasible"])) + print(" reason: %s" % rec["reason"]) + print(" feasible_S (rho square sums): %s" % rec.get("feasible_S")) + # squeeze numbers + sq = c18.squeeze_numbers(n, s, t) + print(" squeeze_numbers: opposite_parity=%s contradiction=%s reason=%s" + % (sq["opposite_parity"], sq["contradiction"], sq["reason"])) + for side in sq["sides"]: + print(" side %s card=%d parseval_remainder=%s max_char=%s max_allowed=%s deficit=%s" + % (side["side"], side["cardinality"], side["parseval_remainder"], + side["max_char"], side["max_allowed"], side["deficit"])) + + +if __name__ == "__main__": + show(11, 7) + show(9, 9) + # controls: the decided/deciding classes for reference + print() + show(12, 6) + show(10, 8) diff --git a/research/f7-18point-remainder-kb3i-a1/parity_census.py b/research/f7-18point-remainder-kb3i-a1/parity_census.py new file mode 100644 index 0000000000..cad49d7631 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/parity_census.py @@ -0,0 +1,169 @@ +"""KB3i probe: exact covering-split census for the reduced (A, B) problem, +to understand the even-split obstruction behind the m=5 ground truth +(F2^5 covers exist only in splits (2,8)(4,6)(6,4)(8,2)) and to test whether +it lifts to the both-odd splits (11,7)/(9,9) of the 18-point question. + +Reduced covering object (PR 2911 reduction lemma, cover18.py docstring): +for a group G = F2^m (2^m elements, XOR), a pair (A, B) of subsets COVERS iff + (i) A + B = G (cross sums reach every element) + (ii) (A+A) u (B+B) = G (self sums reach every element) +where + is XOR. The original P+P = F2^{m+1} cover with parity split (s, t) +corresponds to the reduced (A, B) cover of F2^m with |A| = s, |B| = t. + +Everything is exact integer arithmetic (int bitmasks, no floats). Brute +force is complete at m = 3 (2^8 x 2^8) and targeted-complete at m = 4 for +the splits that matter. A found cover is a WITNESS (the split is possible); +an exhaustive empty scan PROVES the split impossible for that m. +""" + +import sys +from itertools import combinations + +sys.stdout.reconfigure(encoding="utf-8") + + +def popcount(x): + return x.bit_count() + + +def mask_of(idxs): + m = 0 + for i in idxs: + m |= 1 << i + return m + + +def elems(mask): + out = [] + while mask: + lsb = mask & -mask + out.append(lsb.bit_length() - 1) + mask ^= lsb + return out + + +def trans(mask, a): + """{x ^ a : x in mask} as a bitmask.""" + out = 0 + x = mask + while x: + lsb = x & -x + out |= 1 << ((lsb.bit_length() - 1) ^ a) + x ^= lsb + return out + + +def sumset(mx, my): + out = 0 + x = mx + while x: + lsb = x & -x + out |= trans(my, lsb.bit_length() - 1) + x ^= lsb + return out + + +def selfsum(mx): + return sumset(mx, mx) + + +def covers_pair(amask, bmask, gsize): + """Reduced covering test: A+B = G and (A+A) u (B+B) = G.""" + allg = (1 << gsize) - 1 + cross = sumset(amask, bmask) + if cross != allg: + return False, "cross" + selfs = selfsum(amask) | selfsum(bmask) + if selfs != allg: + return False, "self" + return True, "cover" + + +def census_m3(): + """Complete census of reduced covering pairs (A, B) in F2^3 (8 elements), + by split (|A|, |B|). Every subset pair is tested.""" + gsize = 8 + subsets = list(range(1 << gsize)) + # For each split (a, b) count covering pairs and record a witness. + result = {} + for a in range(gsize + 1): + for b in range(gsize + 1): + count = 0 + witness = None + Alist = [s for s in subsets if popcount(s) == a] + Blist = [s for s in subsets if popcount(s) == b] + for am in Alist: + for bm in Blist: + ok, _ = covers_pair(am, bm, gsize) + if ok: + count += 1 + if witness is None: + witness = (elems(am), elems(bm)) + result[(a, b)] = (count, witness) + return result + + +def census_m4_split(a, b): + """Complete census of reduced covering pairs (A, B) in F2^4 (16 elements) + for one split (a, b). Returns (count, witness). Complete: enumerates + every A of size a and every B of size b.""" + gsize = 16 + Alist = [mask_of(c) for c in combinations(range(gsize), a)] + Blist = [mask_of(c) for c in combinations(range(gsize), b)] + count = 0 + witness = None + for am in Alist: + for bm in Blist: + ok, _ = covers_pair(am, bm, gsize) + if ok: + count += 1 + if witness is None: + witness = (elems(am), elems(bm)) + return count, witness + + +def summarize_m3(): + res = census_m3() + print("=== Reduced covering census, F2^3 (G has 8 elements), COMPLETE ===") + print("split covers witness") + for a in range(9): + for b in range(9): + cnt, wit = res[(a, b)] + if cnt > 0: + print("(%d,%d) %d A=%s B=%s" % (a, b, cnt, wit[0], wit[1])) + print("--- empty (no cover) splits ---") + empties = [(a, b) for a in range(9) for b in range(9) if res[(a, b)][0] == 0] + # group by parity + both_odd_empty = [s for s in empties if s[0] % 2 == 1 and s[1] % 2 == 1] + both_even_empty = [s for s in empties if s[0] % 2 == 0 and s[1] % 2 == 0] + mixed_empty = [s for s in empties if s[0] % 2 != s[1] % 2] + print("both-odd empty:", both_odd_empty) + print("both-even empty:", both_even_empty) + print("mixed empty:", mixed_empty) + nonempty = [(a, b) for a in range(9) for b in range(9) if res[(a, b)][0] > 0] + print("nonempty splits:", nonempty) + both_odd_nonempty = [s for s in nonempty if s[0] % 2 == 1 and s[1] % 2 == 1] + print("both-odd NONEMPTY (any cover):", both_odd_nonempty) + + +def summarize_m4(): + print("=== Reduced covering census, F2^4 (G has 16 elements), targeted ===") + # splits summing to 10 (the F2^5 k=10 analogue) and to 18's analogue. + targets = [ + (1, 9), (2, 8), (3, 7), (4, 6), (5, 5), (6, 4), (7, 3), (8, 2), (9, 1), + (2, 2), (3, 3), (4, 4), # small both parity controls + ] + print("split covers witness") + for (a, b) in targets: + cnt, wit = census_m4_split(a, b) + print("(%d,%d) %d %s" % (a, b, cnt, ("A=%s B=%s" % wit) if wit else "-")) + + +if __name__ == "__main__": + mode = sys.argv[1] if len(sys.argv) > 1 else "m3" + if mode == "m3": + summarize_m3() + elif mode == "m4": + summarize_m4() + else: + raise SystemExit("usage: parity_census.py m3|m4") diff --git a/research/f7-18point-remainder-kb3i-a1/self_obstruction.py b/research/f7-18point-remainder-kb3i-a1/self_obstruction.py new file mode 100644 index 0000000000..47b091e69e --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/self_obstruction.py @@ -0,0 +1,116 @@ +"""Probe the (5,5) self-obstruction at m=4: every cross-covering (A,B) pair +(|A|=|B|=5, A+B=F2^4) fails the self condition (A+A) u (B+B) = F2^4. This +records WHY (the self-union deficit and the selfsum sizes / ranks), to see +whether the mechanism generalizes to the (9,9) split at m=6. Exact integer +arithmetic (int masks). +""" + +import sys +from itertools import combinations + +sys.stdout.reconfigure(encoding="utf-8") + + +def mask_of(idxs): + m = 0 + for i in idxs: + m |= 1 << i + return m + + +def elems(mask): + out = [] + while mask: + lsb = mask & -mask + out.append(lsb.bit_length() - 1) + mask ^= lsb + return out + + +def build(m): + gsize = 1 << m + allg = (1 << gsize) - 1 + xors = [[1 << (i ^ j) for j in range(gsize)] for i in range(gsize)] + + def trans(mask, a): + out = 0 + x = mask + while x: + lsb = x & -x + out |= xors[lsb.bit_length() - 1][a] + x ^= lsb + return out + + def sumset(mx, my): + out = 0 + x = mx + while x: + lsb = x & -x + out |= trans(my, lsb.bit_length() - 1) + x ^= lsb + return out + + return gsize, allg, sumset + + +def rank_of(mask): + """Linear rank over F2 of the elements of mask (as vectors).""" + els = elems(mask) + basis = [] + for e in els: + v = e + for b in basis: + v = min(v, v ^ b) + if v: + basis.append(v) + basis.sort(reverse=True) + return len(basis) + + +def probe(m, a, b): + gsize, allg, sumset = build(m) + Alist = [mask_of(c) for c in combinations(range(gsize), a)] + Blist = [mask_of(c) for c in combinations(range(gsize), b)] + # For cross-covering pairs, record self-union size and per-side selfsum size. + selfcover = 0 + crosscover = 0 + max_selfunion = -1 + selfunion_hist = {} + selfsumA_hist = {} + selfsumB_hist = {} + example = None + for am in Alist: + ssa = sumset(am, am) + for bm in Blist: + if sumset(am, bm) != allg: + continue + crosscover += 1 + ssb = sumset(bm, bm) + su = ssa | ssb + su_sz = su.bit_count() + selfunion_hist[su_sz] = selfunion_hist.get(su_sz, 0) + 1 + selfsumA_hist[ssa.bit_count()] = selfsumA_hist.get(ssa.bit_count(), 0) + 1 + selfsumB_hist[ssb.bit_count()] = selfsumB_hist.get(ssb.bit_count(), 0) + 1 + if su == allg: + selfcover += 1 + if su_sz > max_selfunion: + max_selfunion = su_sz + example = (elems(am), elems(bm), ssa.bit_count(), ssb.bit_count(), + elems(allg ^ su)) + print("F2^%d (%d,%d): cross_covering=%d, of those self_covering=%d" + % (m, a, b, crosscover, selfcover)) + print(" max |(A+A) u (B+B)| over cross-covering pairs = %d (of %d)" + % (max_selfunion, gsize)) + print(" self-union size histogram:", dict(sorted(selfunion_hist.items()))) + print(" |A+A| histogram:", dict(sorted(selfsumA_hist.items()))) + print(" |B+B| histogram:", dict(sorted(selfsumB_hist.items()))) + if example: + print(" max example: A=%s B=%s |A+A|=%d |B+B|=%d missed=%s" + % (example[0], example[1], example[2], example[3], example[4])) + + +if __name__ == "__main__": + m = int(sys.argv[1]) + a = int(sys.argv[2]) + b = int(sys.argv[3]) + probe(m, a, b) diff --git a/research/f7-18point-remainder-kb3i-a1/split_census.py b/research/f7-18point-remainder-kb3i-a1/split_census.py new file mode 100644 index 0000000000..8e62c86404 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/split_census.py @@ -0,0 +1,99 @@ +"""Fast reduced-covering census for one split (a, b) in F2^m, with a +precomputed XOR-translate table. Reports covering count, a first witness, +and a breakdown of WHICH condition fails (cross-only, self-only, both) so the +obstruction to a split is localized. Exact integer arithmetic (int masks). + +Reduced covering (PR 2911 lemma): (A,B) covers G=F2^m iff + cross: A+B = G + self: (A+A) u (B+B) = G +""" + +import sys +from itertools import combinations + +sys.stdout.reconfigure(encoding="utf-8") + + +def mask_of(idxs): + m = 0 + for i in idxs: + m |= 1 << i + return m + + +def elems(mask): + out = [] + while mask: + lsb = mask & -mask + out.append(lsb.bit_length() - 1) + mask ^= lsb + return out + + +def build(m): + gsize = 1 << m + allg = (1 << gsize) - 1 + # XOR table: xors[a][b] = 1 << (a ^ b) + xors = [[1 << (i ^ j) for j in range(gsize)] for i in range(gsize)] + + def trans(mask, a): + out = 0 + x = mask + while x: + lsb = x & -x + out |= xors[lsb.bit_length() - 1][a] + x ^= lsb + return out + + def sumset(mx, my): + out = 0 + x = mx + while x: + lsb = x & -x + out |= trans(my, lsb.bit_length() - 1) + x ^= lsb + return out + + return gsize, allg, sumset + + +def census_split(m, a, b, stop_on_witness=False): + gsize, allg, sumset = build(m) + Alist = [mask_of(c) for c in combinations(range(gsize), a)] + Blist = [mask_of(c) for c in combinations(range(gsize), b)] + count = 0 + witness = None + cross_only = 0 # cross covers but self fails + self_only = 0 # self covers but cross fails + both_fail = 0 + for am in Alist: + # precompute selfsum(A) once per A + ssa = sumset(am, am) + for bm in Blist: + cross = sumset(am, bm) == allg + selfs = (ssa | sumset(bm, bm)) == allg + if cross and selfs: + count += 1 + if witness is None: + witness = (elems(am), elems(bm)) + if stop_on_witness: + return count, witness, (cross_only, self_only, both_fail) + elif cross and not selfs: + cross_only += 1 + elif selfs and not cross: + self_only += 1 + else: + both_fail += 1 + return count, witness, (cross_only, self_only, both_fail) + + +if __name__ == "__main__": + m = int(sys.argv[1]) + a = int(sys.argv[2]) + b = int(sys.argv[3]) + stop = len(sys.argv) > 4 and sys.argv[4] == "stop" + cnt, wit, brk = census_split(m, a, b, stop_on_witness=stop) + print("F2^%d split (%d,%d): covers=%d cross_only=%d self_only=%d both_fail=%d" + % (m, a, b, cnt, brk[0], brk[1], brk[2])) + if wit: + print(" witness A=%s B=%s" % (wit[0], wit[1])) diff --git a/research/f7-18point-remainder-kb3i-a1/vendor/agent64_cover17.py b/research/f7-18point-remainder-kb3i-a1/vendor/agent64_cover17.py new file mode 100644 index 0000000000..5add3747a3 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/vendor/agent64_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-18point-remainder-kb3i-a1/vendor/agent64_search17.py b/research/f7-18point-remainder-kb3i-a1/vendor/agent64_search17.py new file mode 100644 index 0000000000..ef17635967 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/vendor/agent64_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-18point-remainder-kb3i-a1/vendor/anchors.py b/research/f7-18point-remainder-kb3i-a1/vendor/anchors.py new file mode 100644 index 0000000000..d07fa31100 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/vendor/anchors.py @@ -0,0 +1,128 @@ +"""Resumable recomputation of the two heavy PR 2773 census anchors (KB3d). + +Established method (PR 2773, package research/f7-17point-cover-audit-seedcfa215c2, +Aaron Wang): raw-domain walk over the even group E = F2^6, complete +GL(6,2)-transitive domain through {0, 3}, sub-sharded by the smallest free +element (disjoint and complete), resumable with per-sub-shard receipts in +ANCHOR-PROGRESS.json. The enumeration itself is the vendored PR 2773 engine +(vendor/agent64_search17.py, byte-pinned; credit: Aaron Wang, PR 2773). + + anchors.py k10b3 [--seconds S] 10-sets through {0,3}, excess <= 3 + (recorded anchor: 149,990,400) + anchors.py k11b4 [--seconds S] 11-sets through {0,3}, excess <= 4 + (recorded anchor: level3 = level4 = 0) + +Each invocation processes sub-shards until the elapsed budget (default 540 s), +writes receipts after every sub-shard, and exits 0; re-invoke to continue. +A completed run prints PASS_ANCHORS_ with the exact totals and compares +them with the recorded anchor values. +""" + +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "vendor")) + +import agent64_search17 as s17 + +PROGRESS = HERE / "ANCHOR-PROGRESS.json" + +MODES = { + "k10b3": { + "k": 10, + "budget": 3, + "anchor_count": 149990400, + "description": "10-sets through {0,3}, pair-sum excess <= 3", + }, + "k11b4": { + "k": 11, + "budget": 4, + "anchor_count": 0, + "description": "11-sets through {0,3}, pair-sum excess <= 4", + }, +} + + +def load_progress(mode): + """Per-mode sections in one file (v1 kept one mode per file and lost the + other mode's receipts when switching; migrated on read).""" + data = {"modes": {}} + if PROGRESS.exists(): + old = json.loads(PROGRESS.read_text(encoding="utf-8")) + if "modes" in old: + data = old + elif "mode" in old: + data["modes"][old["mode"]] = { + k: v for k, v in old.items() if k != "mode" + } + return data["modes"].setdefault(mode, {"shards": {}}) + + +def save_progress(mode, prog): + data = {"modes": {}} + if PROGRESS.exists(): + old = json.loads(PROGRESS.read_text(encoding="utf-8")) + if "modes" in old: + data = old + elif "mode" in old: + data["modes"][old["mode"]] = { + k: v for k, v in old.items() if k != "mode" + } + data["modes"][mode] = prog + PROGRESS.write_text(json.dumps(data, indent=2, sort_keys=True), encoding="utf-8") + + +def main(): + mode = sys.argv[1] if len(sys.argv) > 1 else "" + if mode not in MODES: + raise SystemExit("usage: anchors.py k10b3|k11b4 [--seconds S]") + budget_seconds = 540.0 + if "--seconds" in sys.argv: + budget_seconds = float(sys.argv[sys.argv.index("--seconds") + 1]) + spec = MODES[mode] + prog = load_progress(mode) + prog["spec"] = {k: v for k, v in spec.items()} + t_start = time.time() + for v0 in sorted(s17.EVEN): + if v0 in (0, 3): + continue + key = f"v0={v0}" + if key in prog["shards"]: + continue + t1 = time.time() + hist, examples = s17.hist_sets( + s17.EVEN, spec["k"], spec["budget"], fixed=(0, 3, v0), floor=v0 + ) + prog["shards"][key] = { + "hist": {str(e): n for e, n in sorted(hist.items())}, + "examples": examples, + "seconds": round(time.time() - t1, 2), + } + save_progress(mode, prog) + print( + f"ANCHOR {mode} {key} hist={prog['shards'][key]['hist']}" + f" seconds={prog['shards'][key]['seconds']}" + f" done={len(prog['shards'])}/62", + flush=True, + ) + if time.time() - t_start > budget_seconds: + print(f"RECEIPT {mode} checkpoint shards={len(prog['shards'])}/62", flush=True) + return + total = {} + for rec in prog["shards"].values(): + for e, n in rec["hist"].items(): + total[e] = total.get(e, 0) + n + count = sum(total.values()) + prog["total_hist"] = {str(e): n for e, n in sorted(total.items())} + prog["complete"] = True + save_progress(mode, prog) + assert count == spec["anchor_count"], (mode, count, spec["anchor_count"]) + print(f"PASS_ANCHORS_{mode.upper()} count={count} total_hist={prog['total_hist']} shards=62", flush=True) + + +if __name__ == "__main__": + sys.stdout.reconfigure(encoding="utf-8") + main() diff --git a/research/f7-18point-remainder-kb3i-a1/vendor/cover18.py b/research/f7-18point-remainder-kb3i-a1/vendor/cover18.py new file mode 100644 index 0000000000..3faa640d79 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/vendor/cover18.py @@ -0,0 +1,741 @@ +"""KB3e engine: the 18-point cover question for F2^7. + +Object. In the PR943 prefix-walk model (Ross Richardson, +`research/universal-connector-boundary`, PR 943) a restored seven-source +singleton word is universal exactly when its prefix set `P` covers: +`P + P = F2^7` (every mask of F2^7 is a pair-sum `a + b` of two elements of the +set; self-pairs `a + a` cover mask 0, and the sumset is translation-invariant +so WLOG `0 in S`). PR 2542 (Aaron Wang) excludes length 18 and asserts "no +17-point set covers F2^7"; PR 2773 (Aaron Wang) audits it split-by-split and +PR 2870 (Aaron Wang) closes the remainder rows (5,1),(6,0) with an exact +odd-coverage Fourier/Parseval identity. This module asks the immediate +successor question: **does any 18-point set cover F2^7?** + +Parity splits. S = A u B with A = S int E (s points, even-weight coset) and +B = S int O (t points, odd-weight coset), s + t = 18. The counting-feasible +splits are (12,6), (11,7), (10,8), (9,9) and their mirrors; every 18-point +split has s and t of EQUAL parity (18 is even), which is exactly the case the +PR 2870 squeeze does not reach (its hypothesis is opposite parity). + +Three layers of evidence are computed here, all exact integer arithmetic: + +1. `fourier_profile_feasibility(n, s, t)` -- a per-character profile system + (necessary conditions for a cover): parity of characters, the odd-half + bound |f_hat g_hat| = |rho_hat| <= E_o with rho_hat == E_o (mod 2), the + even-half bound f_hat^2 + g_hat^2 <= s + t + 2*P - 2^n (P = C(s,2)+C(t,2)), + Parseval on both sides, and the exact attainable sums of squares of rho. + Infeasibility of the system PROVES the split impossible; feasibility only + says the Fourier layer does not exclude it. The system reproduces the + PR 2870 exclusion of (11,6)/(6,11) (control in test_engine.py). +2. `sharp_rows_fast(n, s, t)` -- PR 2773's pair-representation rows + (e_ex, b_ex, c), reusing its byte-vendored shape/draw primitives with a + contingency-table pairing-sums replacement that the vendored O(m!) pairing + loop cannot run at the 18-point row sizes. Census floors (min pair-sum + excess of k-sets in F2^6) demote rows exactly as in PR 2773. +3. `search_split(...)` / `search_direct(...)` -- a bounded, seeded local + search for a covering pair (A, D) resp. an 18-point set. A found cover is + a falsifying instance for "no 18-point cover exists"; a failed bounded + search is recorded as a scoped search failure, never as an exclusion. + +Reduction lemma (checked exhaustively at n = 3 in test_engine.py). Fix an +odd mask p and set D = p + B (a subset of E). Then S = A u B covers F2^n iff +(i) A + D = E and (ii) (A + A) u (D + D) = E. So every split (s, t) is a +two-set covering problem in the even group E =~ F2^6. + +All arithmetic is exact Python integers; no floats are used. +""" + +import random +import time +from collections import Counter +from functools import lru_cache +from itertools import combinations +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "vendor")) + +import agent64_cover17 as c17 # noqa: E402 + +# Byte pins of the vendored PR 2773 engine (credit: Aaron Wang, PR 2773, +# head 6739c799799621878a9249c93e2b12cc799c1482; extracted with +# agent_tools.py pr-tree-extract from PR 2870's hash-pinned vendor/). +VENDOR_PIN_COVER17 = ( + "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654" +) +VENDOR_PIN_SEARCH17 = ( + "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674" +) + + +# ------------------------------------------------------------- coverage + + +def dot(s, x): + return (s & x).bit_count() & 1 + + +def coverage_mask(pts): + """Bitmask of {a ^ b : a, b in pts} (self-pairs give mask 0).""" + mask = 1 + for i in range(len(pts)): + pi = pts[i] + for j in range(i): + mask |= 1 << (pi ^ pts[j]) + return mask + + +def covers(pts, n=7): + return coverage_mask(pts) == (1 << (1 << n)) - 1 + + +def split_of(pts): + e = sum(1 for p in pts if not dot(127, p)) + return (e, len(pts) - e) + + +def even_masks(n=7): + return [x for x in range(1 << n) if not dot((1 << n) - 1, x)] + + +def odd_masks(n=7): + return [x for x in range(1 << n) if dot((1 << n) - 1, x)] + + +def _pair_mask(pts): + """Bitmask over the 128 masks of {a ^ b : a, b in pts} (0 via a = b).""" + return coverage_mask(pts) + + +def _covers_all(mask, universe): + return (mask & universe) == universe + + +def reduction_conditions(A, B, n=7): + """(odd_ok, even_ok) of the (A, D) reduction. D = p + B for an odd p; + A u B covers F2^n iff odd_ok and even_ok both hold.""" + p = 1 + D = [p ^ b for b in B] + ev = even_masks(n) + universe = 0 + for x in ev: + universe |= 1 << x + cross = 0 + for a in A: + for d in D: + cross |= 1 << (a ^ d) + selfs = _pair_mask(A) | _pair_mask(D) + return _covers_all(cross, universe), _covers_all(selfs, universe) + + +# ------------------------------------------------------- rho bookkeeping + + +def _partitions(total): + 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 + + +@lru_cache(maxsize=None) +def rho_square_values(excess): + """Attainable sums of squares sum rho_x^2 over integer rho >= 0 with + sum rho_x = excess (partition square sums). Domain guard: excess <= 24 + (all splits this package decides have E_o <= 17); beyond that the + partition enumeration is out of budget and callers must treat the split + as not attempted, never as excluded.""" + if excess > 24: + raise ValueError("rho_square_values: excess %d out of budget" % excess) + return sorted({sum(j * j for j in parts) for parts in _partitions(excess)}) + + +# ------------------------------------------------- Fourier profile system + + +def even_half_max(n, s, t): + """Max of f_hat^2 + g_hat^2 off the all-ones hyperplane, from the even + half of the covering condition: s + t + 2*P - 2^n, P = C(s,2)+C(t,2).""" + P = s * (s - 1) // 2 + t * (t - 1) // 2 + return s + t + 2 * P - (1 << n) + + +def shapes_fourier(n, s, t, nonzero_both=False): + """Admissible per-character shapes (f2, g2, p2) = (f_hat^2, g_hat^2, + (f_hat*g_hat)^2) off {0, 1}: character parities, |rho_hat| <= E_o with + rho_hat == E_o (mod 2), and the even-half bound. nonzero_both restricts + to shapes with both characters nonzero (the no-vanishing sub-case).""" + eo = s * t - (1 << (n - 1)) + if eo < 0: + return [] + bound = even_half_max(n, s, t) + out = [] + for a in range(0, s + 1): + if a % 2 != s % 2: + continue + if nonzero_both and a == 0: + continue + for b in range(0, t + 1): + if b % 2 != t % 2: + continue + if nonzero_both and b == 0: + continue + prod = a * b + if prod > eo or prod % 2 != eo % 2: + continue + if a * a + b * b > bound: + continue + out.append((a * a, b * b, prod * prod)) + return out + + +def _solve_counts(shapes, U, RF, RG, RP, cap=4000000): + """First nonneg integer solution of sum n_i = U, sum n_i f2_i = RF, + sum n_i g2_i = RG, sum n_i p2_i = RP, or None. Returns (solution, nodes) + with nodes = "cap" when the step cap is hit (caller must treat as + undecided, never as infeasible).""" + m = len(shapes) + if m == 0: + if U == 0 and RF == 0 and RG == 0 and RP == 0: + return ([], 0) + return (None, 0) + order = sorted(range(m), key=lambda i: -shapes[i][0]) + shp = [shapes[i] for i in order] + sol = [0] * m + nodes = [0] + + # suffix min/max of each coefficient for bound pruning + smin_f = [0] * (m + 1) + smax_f = [0] * (m + 1) + smin_g = [0] * (m + 1) + smax_g = [0] * (m + 1) + smin_p = [0] * (m + 1) + smax_p = [0] * (m + 1) + for i in range(m - 1, -1, -1): + f2, g2, p2 = shp[i] + smin_f[i] = min(f2, smin_f[i + 1]) + smax_f[i] = max(f2, smax_f[i + 1]) + smin_g[i] = min(g2, smin_g[i + 1]) + smax_g[i] = max(g2, smax_g[i + 1]) + smin_p[i] = min(p2, smin_p[i + 1]) + smax_p[i] = max(p2, smax_p[i + 1]) + + def rec(i, u_rem, rf, rg, rp): + nodes[0] += 1 + if nodes[0] > cap: + return "cap" + if i == m - 1: + f2, g2, p2 = shp[i] + if u_rem >= 0 and rf == u_rem * f2 and rg == u_rem * g2 and rp == u_rem * p2: + sol[i] = u_rem + return True + return False + f2, g2, p2 = shp[i] + hi = u_rem + if f2: + hi = min(hi, rf // f2) + if g2: + hi = min(hi, rg // g2) + if p2: + hi = min(hi, rp // p2) + for k in range(hi, -1, -1): + ru, rff, rgg, rpp = u_rem - k, rf - k * f2, rg - k * g2, rp - k * p2 + if ru < 0 or rff < 0 or rgg < 0 or rpp < 0: + continue + if rff > ru * smax_f[i + 1] or rff < ru * smin_f[i + 1]: + continue + if rgg > ru * smax_g[i + 1] or rgg < ru * smin_g[i + 1]: + continue + if rpp > ru * smax_p[i + 1] or rpp < ru * smin_p[i + 1]: + continue + sol[i] = k + got = rec(i + 1, ru, rff, rgg, rpp) + if got == "cap": + return "cap" + if got: + return True + sol[i] = 0 + return False + + got = rec(0, U, RF, RG, RP) + if got == "cap": + return (None, "cap") + if got: + out = [0] * m + for slot, orig in enumerate(order): + out[orig] = sol[slot] + return (out, nodes[0]) + return (None, nodes[0]) + + +def fourier_profile_feasibility(n, s, t, nonzero_both=False): + """Necessary-condition system for an (s,t) split at F2^n. `feasible` + False PROVES the odd half (hence the cover) impossible; `feasible` True + means only that this Fourier layer does not exclude the split. With + nonzero_both=True the system is restricted to per-characters with both + sides nonzero: infeasibility then PROVES every cover of this split must + have at least one vanishing character off {0, 1}.""" + eo = s * t - (1 << (n - 1)) + res = { + "n": n, + "split": (s, t), + "odd_excess": eo, + "nonzero_both": nonzero_both, + "even_half_max": even_half_max(n, s, t), + } + if eo < 0: + res["feasible"] = False + res["reason"] = "counting: fewer cross pairs than odd masks" + res["feasible_S"] = [] + return res + if eo > 24: + res["feasible"] = None + res["reason"] = "E_o out of the rho-square enumeration budget: not attempted" + res["feasible_S"] = [] + return res + shapes = shapes_fourier(n, s, t, nonzero_both=nonzero_both) + res["shapes"] = shapes + U = (1 << n) - 2 + RF = (1 << n) * s - 2 * s * s + RG = (1 << n) * t - 2 * t * t + res["parseval_remainders"] = (RF, RG) + feasible_S = [] + example = None + capped = False + for S in rho_square_values(eo): + RP = (1 << n) * S - 2 * eo * eo + sol, nodes = _solve_counts(shapes, U, RF, RG, RP) + if nodes == "cap": + capped = True + continue + if sol is not None: + feasible_S.append(S) + if example is None: + example = {"S": S, "counts": sol} + res["feasible_S"] = feasible_S + res["example"] = example + res["capped"] = capped + if capped: + res["feasible"] = True + res["reason"] = ( + "step cap hit for some S values: undecided for those (never a " + "proof of impossibility); S values listed are the feasible ones" + ) + elif feasible_S: + res["feasible"] = True + res["reason"] = ( + "profile system consistent for S in %s; no Fourier contradiction" + % sorted(feasible_S) + ) + else: + res["feasible"] = False + res["reason"] = ( + "profile system infeasible for every attainable rho square sum: " + "no integer character profile satisfies parity, |rho_hat| <= E_o, " + "the even-half bound and Parseval simultaneously" + ) + return res + + +def witness_constraints_ok(A, B, n=7): + """Direct validation of every profile-system constraint on an actual + covering pair (A, B). Used as the soundness control: a real cover can + never violate a constraint the system uses.""" + N = 1 << n + half = 1 << (n - 1) + eo = len(A) * len(B) - half + if eo < 0: + return False + s, t = len(A), len(B) + # odd half: r = 1_A * 1_B >= 1 on O + r = [0] * N + for a in A: + for b in B: + r[a ^ b] += 1 + odds = [x for x in range(N) if dot(N - 1, x)] + if any(r[x] < 1 for x in odds): + return False + rho = {x: r[x] - 1 for x in odds if r[x] > 1} + if sum(rho.values()) != eo: + return False + # even half: A_x + B_x >= 1 on E \ {0} + pairA = Counter() + pairB = Counter() + for i in range(len(A)): + for j in range(i): + pairA[A[i] ^ A[j]] += 1 + for i in range(len(B)): + for j in range(i): + pairB[B[i] ^ B[j]] += 1 + evs = [x for x in range(N) if not dot(N - 1, x) and x != 0] + if any(pairA[x] + pairB[x] < 1 for x in evs): + return False + P = s * (s - 1) // 2 + t * (t - 1) // 2 + bound = s + t + 2 * P - N + # characters off {0, 1} + for u in range(N): + if u in (0, N - 1): + continue + f_hat = sum(1 - 2 * dot(u, a) for a in A) + g_hat = sum(1 - 2 * dot(u, b) for b in B) + if f_hat % 2 != s % 2 or g_hat % 2 != t % 2: + return False + rho_hat = sum(c * (1 - 2 * dot(u, x)) for x, c in rho.items()) + if f_hat * g_hat != rho_hat: + return False + if abs(rho_hat) > eo or rho_hat % 2 != eo % 2: + return False + if f_hat * f_hat + g_hat * g_hat > bound: + return False + return True + + +def squeeze_numbers(n, s, t): + """The PR 2870-style Parseval deficit bookkeeping for one split, extended + to equal parity: per-side remainders vs the strongest uniform character + bound the parity class allows.""" + eo = s * t - (1 << (n - 1)) + N = 1 << n + res = {"n": n, "split": (s, t), "odd_excess": eo} + if eo < 0: + res.update( + bounded_side=None, + parseval_remainder=None, + max_allowed=None, + deficit=None, + contradiction=True, + reason="counting: fewer cross pairs than odd masks", + ) + return res + opposite = (s % 2) != (t % 2) + sides = [] + for name, card, par in (("A", s, s % 2), ("B", t, t % 2)): + remainder = N * card - 2 * card * card + if opposite and par == 0: + max_char = 2 * (eo // 2) # largest even <= E_o + elif (not opposite) and par == 1: + max_char = eo if eo % 2 == 1 else eo - 1 # largest odd <= E_o + else: + max_char = None # side can vanish: no uniform bound + allowed = None if max_char is None else (N - 2) * max_char * max_char + deficit = None if allowed is None else remainder - allowed + sides.append( + dict( + side=name, + cardinality=card, + max_char=max_char, + parseval_remainder=remainder, + max_allowed=allowed, + deficit=deficit, + ) + ) + res["opposite_parity"] = opposite + res["sides"] = sides + if opposite: + bounded = next(x for x in sides if x["max_char"] is not None) + res.update( + bounded_side=bounded["side"], + parseval_remainder=bounded["parseval_remainder"], + max_allowed=bounded["max_allowed"], + deficit=bounded["deficit"], + contradiction=bounded["deficit"] > 0, + reason=( + "PR 2870 squeeze applies (opposite parity): %d > %d" + % (bounded["parseval_remainder"], bounded["max_allowed"]) + if bounded["deficit"] > 0 + else "PR 2870 squeeze applies but reaches no contradiction" + ), + ) + else: + res.update( + bounded_side=None, + parseval_remainder=None, + max_allowed=None, + deficit=None, + contradiction=False, + reason=( + "equal character parities (s+t even): PR 2870's squeeze " + "hypothesis fails for this split; see sides[] for the " + "equal-parity remainders vs bounds" + ), + ) + return res + + +# ------------------------------------------------------ pairing sums + + +def pairing_sums(da, db): + """All sums sum_i a_i b_{pi(i)} over bijections pi of two equal-length + multisets, by contingency-table enumeration (the vendored O(m!) loop + cannot run at 18-point row sizes).""" + ca = Counter(da) + cb = Counter(db) + va = sorted(ca) + vb = sorted(cb) + acounts = [ca[v] for v in va] + bcounts = [cb[v] for v in vb] + out = set() + + def rec(i, caps, acc): + if i == len(va): + if all(c == 0 for c in caps): + out.add(acc) + return + need = acounts[i] + va_i = va[i] + + def dist(j, remaining, add): + if j == len(vb) - 1: + if remaining <= caps[j]: + caps[j] -= remaining + rec(i + 1, caps, acc + add + va_i * vb[j] * remaining) + caps[j] += remaining + return + for take in range(min(caps[j], remaining) + 1): + caps[j] -= take + dist(j + 1, remaining - take, add + va_i * vb[j] * take) + caps[j] += take + + dist(0, need, 0) + + rec(0, list(bcounts), 0) + return out + + +@lru_cache(maxsize=None) +def _pairing_sums_cached(da, db): + return frozenset(pairing_sums(da, db)) + + +@lru_cache(maxsize=None) +def draw_multisets(shared, budget, min_excess=0): + """Deduped draws: multisets of `shared` values >= 1 with total excess + sum(v-1) in [min_excess, budget]. (Embeddable in some multiplicity shape + of support `shared` + complement with total excess `budget`.)""" + out = set() + + def rec(lo, remaining, excess_left, acc): + if remaining == 0: + out.add(tuple(sorted(acc))) + return + for v in range(lo, excess_left + 2): + new_left = excess_left - (v - 1) + if new_left < 0: + break + rec(v, remaining - 1, new_left, acc + [v]) + + for used in range(min_excess, budget + 1): + rec(1, shared, used, []) + return sorted(out) + + +def attainable_c_values(n, s, t, e_ex, b_ex, targets=None, cap=200000): + """Exact attainable c = sum_x A_x B_x on the shared support positions + (targets given: only membership in targets is decided). Returns + (values_or_flags, status) with status in {"exact", "capped"}.""" + odd_masks_n = 1 << (n - 1) + even_nonzero = odd_masks_n - 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(), "exact") + if shared == 0: + return ({0}, "exact") + comp_a = A - e_ex - shared + comp_b = B - b_ex - shared + das = draw_multisets(shared, e_ex, e_ex if comp_a == 0 else 0) + dbs = draw_multisets(shared, b_ex, b_ex if comp_b == 0 else 0) + found = set() + steps = 0 + for da in das: + for db in dbs: + steps += 1 + if steps > cap: + return (found, "capped") + vals = _pairing_sums_cached(da, db) + if targets is not None: + found |= vals & set(targets) + else: + found |= vals + return (found, "exact") + + +# ------------------------------------------------------------ rows + + +def max_attain(e_ex, b_ex, shared): + """Largest attainable c for one row (rearrangement on the extreme draws).""" + if shared <= 0: + return 0 + return (e_ex + 1) * (b_ex + 1) + shared - 1 + + +def sharp_rows_fast(n, s, t, min_e_ex=0, min_b_ex=0, cap=200000): + """PR 2773's sharp pair-representation rows for one split, with census + floors applied. Row status: "sharp" (exact attainability computed), + "interval" (kept conservatively: exact check capped), "dead" (dropped).""" + odd_masks_n = 1 << (n - 1) + even_nonzero = odd_masks_n - 1 + A = s * (s - 1) // 2 + B = t * (t - 1) // 2 + excess = s * t - odd_masks_n + need = (excess + 1) // 2 if excess > 0 else 0 + c_vals = c17.profile_c_values(n, s, t) + rows = [] + best = -1 + capped_rows = 0 + if excess < 0 or A + B < even_nonzero: + return dict(feasible=False, rows=[], best=best, need=need, c_vals=c_vals) + for e_ex in range(min_e_ex, A + 1): + for b_ex in range(min_b_ex, B + 1): + shared = A + B - e_ex - b_ex - even_nonzero + if shared < 0: + continue + attain, status = attainable_c_values(n, s, t, e_ex, b_ex, cap=cap) + if status == "capped": + capped_rows += 1 + best = max(best, max_attain(e_ex, b_ex, shared)) + hits = [c for c in c_vals if c <= max_attain(e_ex, b_ex, shared)] + for c in hits: + rows.append( + dict(e_ex=e_ex, b_ex=b_ex, shared=shared, c=c, status="interval") + ) + continue + if not attain: + continue + best = max(best, max(attain)) + for c in sorted(set(attain) & set(c_vals)): + rows.append( + dict(e_ex=e_ex, b_ex=b_ex, shared=shared, c=c, status="sharp") + ) + return dict( + feasible=bool(rows), + rows=rows, + best=best, + need=need, + c_vals=c_vals, + capped_rows=capped_rows, + ) + + +def surviving_rows_fast(n, s, t, min_e_ex=0, min_b_ex=0): + return sharp_rows_fast(n, s, t, min_e_ex=min_e_ex, min_b_ex=min_b_ex) + + +# ------------------------------------------------------------- search + + +def _score_pair(A, D, ev_index): + """Coverage score of a candidate (A, D) pair over the even group: + |A + D| + |(A+A) u (D+D)|, target 128 (two sets of 64).""" + cross = set(a ^ d for a in A for d in D) + selfs = set(a ^ a2 for i, a in enumerate(A) for a2 in A[i:]) + selfs |= set(d ^ d2 for i, d in enumerate(D) for d2 in D[i:]) + return len(cross) + len(selfs) + + +def search_split(s, t, restarts=20, seed=1, seconds=20.0, n=7): + """Bounded seeded local search for a covering pair (A, D) in the even + group E =~ F2^6 with |A| = s, |D| = t (reduction lemma). A found pair is + a falsifying instance; otherwise a scoped search failure.""" + rng = random.Random(seed) + ev = even_masks(n) + pool = ev[:] + best = (0, None) + t0 = time.time() + moves = 0 + for _ in range(restarts): + if time.time() - t0 > seconds: + break + A = rng.sample(pool, s) + D = rng.sample(pool, t) + sc = _score_pair(A, D, None) + improved = True + while improved and time.time() - t0 < seconds: + improved = False + for side, size in ((0, s), (1, t)): + cur = A if side == 0 else D + outside = [x for x in pool if x not in cur] + for i in range(size): + for v in outside: + moves += 1 + old = cur[i] + cur[i] = v + new = _score_pair(A, D, None) + if new > sc: + sc = new + improved = True + outside[outside.index(v)] = old + if sc == 128: + return dict( + found=True, + score=128, + A=sorted(A), + D=sorted(D), + restarts=_, + moves=moves, + seconds=round(time.time() - t0, 2), + ) + else: + cur[i] = old + if sc > best[0]: + best = (sc, (sorted(A), sorted(D))) + return dict( + found=False, + score=best[0], + best_pair=best[1], + restarts=restarts, + moves=moves, + seconds=round(time.time() - t0, 2), + ) + + +def search_direct(k=18, restarts=30, seed=1, seconds=20.0, n=7): + """Bounded seeded local search for a k-point cover of F2^n directly + (0 in S, translation WLOG).""" + rng = random.Random(seed) + pool = list(range(1 << n)) + best = (0, None) + t0 = time.time() + for _ in range(restarts): + if time.time() - t0 > seconds: + break + S = [0] + rng.sample(pool[1:], k - 1) + sc = coverage_mask(S).bit_count() + improved = True + while improved and time.time() - t0 < seconds: + improved = False + outside = [x for x in pool if x not in S] + for i in range(1, k): + for v in outside: + old = S[i] + S[i] = v + new = coverage_mask(S).bit_count() + if new > sc: + sc = new + improved = True + outside[outside.index(v)] = old + if sc == (1 << n): + return dict( + found=True, + score=sc, + S=sorted(S), + seconds=round(time.time() - t0, 2), + ) + else: + S[i] = old + if sc > best[0]: + best = (sc, sorted(S)) + return dict( + found=False, + score=best[0], + best_set=best[1], + restarts=restarts, + seconds=round(time.time() - t0, 2), + ) diff --git a/research/f7-18point-remainder-kb3i-a1/vendor/tight.py b/research/f7-18point-remainder-kb3i-a1/vendor/tight.py new file mode 100644 index 0000000000..2e0e151ccf --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/vendor/tight.py @@ -0,0 +1,760 @@ +"""KB3g engine: tight-class resolution for the 18-point cover question for +F2^7 (set level; no words). Exact Python integer arithmetic only. + +Object (unchanged from PR 2911/2933): S = A u B covers F2^7 iff P + P = F2^7. +With D = p + B inside E = F2^6 (PR 2911 reduction, PROVEN there) the pair +(A, D) covers iff (i) A + D = E and (ii) (A+A) u (D+D) = E. + +This module decides the two PR 2933 TIGHT classes of the (10,8) split and +the full-sumset class (6,0) of (12,6) by exact enumeration of the L7-forced +Sidon equality configurations. All arithmetic is integers; masks are Python +ints. + +Halves. Fix the character psi = bit 0 (WLOG under GL(6,2)). H = ker(psi) +and the coset H' are both identified with F2^5 = {0..31}; every cross sum is +the XOR of the two F2^5 coordinates (the coset offset cancels in pairs, and +H'-valued sums are read in H' coordinates). A = A0 u A1 with A0 in H, A1 in +H'; D = D0 u D1 likewise. Coverage is equivalent to the four L3 lines +(PR 2933, PROVEN): + + (i) (A0+D0) u (A1+D1) = H + (ii) (A0+D1) u (A1+D0) = H' + (iii) (A0+A0) u (A1+A1) u (D0+D0) u (D1+D1) = H + (iv) (A0+A1) u (D0+D1) = H' + +Half-translations (h on (A0,D0), h' on (A1,D1)) and a common GL(5,2) map M +preserve all four lines (each H'-valued sumset translates by h + h', which +preserves its being all of H'). Hence WLOG 0 in A0, 0 in A1. + +L7 (PR 2933, PROVEN; general pigeonhole valid at m = 6): at F1 equality +a0*a1 + d0*d1 = 32 with (iv) holding, |A0+A1| = a0*a1, |D0+D1| = d0*d1 (both +Sidon: all cross sums distinct) and the two cross sumsets are disjoint with +union H'. + +Class (10,8) A-vanish (7,1): A0, A1 5-sets with |A0+A1| = 25; D0 a 7-set, +D1 a singleton {d1}. (iv) forces D0 + d1 = T := H' \\ (A0+A1) (7 points). +Substituting D0 = T + d1 into (i)-(iii) and translating by d1 shows coverage +is INDEPENDENT of d1: + (I) (A0+T) u A1 = F2^5 + (II) (A1+T) u A0 = F2^5 + (III) (A0+A0) u (A1+A1) u (T+T) = F2^5 +and (iv) holds by construction. Each covering (A0, A1) yields 32 covering +configurations (one per d1) in the normalized chart. + +Class (10,8) D-vanish (8,2): D0, D1 4-sets with |D0+D1| = 16; A splits +(8,2): A0 an 8-set, A1 = {w, w+delta}, delta != 0. |A0+A1| = 16 iff +A0 u (A0+delta) = 16 points iff A0 n (A0+delta) = 0. Normalize instead on +the D side: 0 in D0, 0 in D1 (the class forces both nonempty), and WLOG +delta = 1 under GL(5,2). With T = D0+D1 (16 points) and C = H' \\ T, +(iv) forces A0 + w to choose one element of each pair {x, x+1} inside C, so +C must be 1-invariant; the choice is one of at most 2^8 sets A0t = A0 + w. +Coverage is then independent of w: + (I') (A0t+D0) u (D1+{0,1}) = F2^5 + (II') (A0t+D1) u (D0+{0,1}) = F2^5 + (III') (A0t+A0t) u {0,1} u (D0+D0) u (D1+D1) = F2^5 + +Class (12,6) A-vanish (6,0): A0, A1 6-sets with A0+A1 = H' (36 pairs, excess +exactly 4), D = D0 a 6-set in H, D1 empty. Lines reduce to + (I'') A0+D = F2^5, (II'') A1+D = F2^5, + (III'') (A0+A0) u (A1+A1) u (D+D) = F2^5. +Normalize 0 in A0, 0 in A1. +""" + +import json +import sys +import time +from itertools import combinations +from pathlib import Path + +ALL = (1 << 32) - 1 +N5 = 32 + + +# ------------------------------------------------------- mask primitives + + +def elems(mask): + out = [] + while mask: + lsb = mask & -mask + out.append(lsb.bit_length() - 1) + mask ^= lsb + return out + + +def mask_of(pts): + m = 0 + for p in pts: + m |= 1 << p + return m + + +# Precomputed per-bit XOR-translation block masks (5 bits, F2^5). +_BIT_LO = [] +_BIT_HI = [] +for _i in range(5): + _b = 1 << _i + _lo = 0 + for _p in range(N5): + if not (_p & _b): + _lo |= 1 << _p + _BIT_LO.append(_lo) + _BIT_HI.append(ALL ^ _lo) + + +def trans(mask, a): + """{x ^ a : x in mask} as a bitmask.""" + for i in range(5): + if (a >> i) & 1: + b = 1 << i + mask = ((mask & _BIT_LO[i]) << b) | ((mask & _BIT_HI[i]) >> b) + return mask + + +def sumset_mask(mx, my): + """{x ^ y : x in mx, y in my}.""" + out = 0 + x = mx + while x: + lsb = x & -x + out |= trans(my, lsb.bit_length() - 1) + x ^= lsb + return out + + +def selfsum_mask(mx): + """{x ^ y : x, y in mx} (includes 0).""" + return sumset_mask(mx, mx) + + +def delta_mask(mx): + """{x ^ y : x != y in mx} = selfsum minus {0}.""" + return selfsum_mask(mx) & ALL & ~1 + + +def sidon_cross(mx, my, px, py): + """|X+Y| = |X|*|Y| with sizes px, py (all cross sums distinct).""" + return sumset_mask(mx, my).bit_count() == px * py + + +# ------------------------------------------- class (7,1) at (10,8) + + +def class71_pairs(): + """All normalized Sidon 5-pairs: 0 in A0, 0 in A1, |A0+A1| = 25. + Backtracks A0 = {0, a1, a2, a3, a4} against the forbidden difference + set of A1 (condition Delta(A0) n Delta(A1) = 0).""" + out = [] + rest = list(range(1, N5)) + + def extend(a1m): + forb = delta_mask(a1m) + cand = [v for v in rest if not (forb >> v) & 1] + chosen = [0, 0, 0, 0, 0] + + def rec(depth, start): + if depth == 5: + out.append((mask_of(chosen), a1m)) + return + for i in range(start, len(cand)): + v = cand[i] + if v <= chosen[depth - 1]: + continue + ok = True + for j in range(1, depth): + if (forb >> (v ^ chosen[j])) & 1: + ok = False + break + if ok: + chosen[depth] = v + rec(depth + 1, i + 1) + + rec(1, 0) + + for bs in combinations(rest, 4): + a1m = 1 | mask_of(bs) + extend(a1m) + return out + + +def class71_check(a0m, a1m): + """The three translated coverage lines (I),(II),(III) for one pair. + Returns (ok, which_lines_fail).""" + sums = sumset_mask(a0m, a1m) + if sums.bit_count() != 25: + return False, ("sidon",) + tm = ALL ^ sums + fails = [] + if (sumset_mask(a0m, tm) | a1m) != ALL: + fails.append("I") + if (sumset_mask(a1m, tm) | a0m) != ALL: + fails.append("II") + if (selfsum_mask(a0m) | selfsum_mask(a1m) | selfsum_mask(tm)) != ALL: + fails.append("III") + return (not fails), tuple(fails) + + +def class71_run(progress=None, budget=None): + """Full decision run for class (7,1). Counts every normalized equality + configuration (A0, A1, d1) and every covering one; records witnesses.""" + t0 = time.time() + pairs = class71_pairs() + total = len(pairs) + checked = 0 + covering = 0 + fail_hist = {} + witnesses = [] + for (a0m, a1m) in pairs: + ok, fails = class71_check(a0m, a1m) + checked += 1 + if ok: + covering += 1 + if len(witnesses) < 5: + witnesses.append((elems(a0m), elems(a1m))) + else: + fail_hist[fails] = fail_hist.get(fails, 0) + 1 + if budget is not None and checked % 5000 == 0 and time.time() - t0 > budget: + break + return dict( + normalized_pairs=total, + checked=checked, + covering_pairs=covering, + equality_configs_normalized=total * 32, + covering_configs_normalized=covering * 32, + fail_hist={str(k): v for k, v in sorted(fail_hist.items())}, + witnesses=witnesses, + seconds=round(time.time() - t0, 2), + ) + + +# ------------------------------------------- class (8,2) at (10,8) + + +def sidon44_pairs_normalized(): + """All Sidon 4-pairs: 0 in D0, 0 in D1, |D0+D1| = 16.""" + out = [] + rest = list(range(1, N5)) + for c0 in combinations(rest, 3): + d0m = 1 | mask_of(c0) + for c1 in combinations(rest, 3): + d1m = 1 | mask_of(c1) + if sumset_mask(d0m, d1m).bit_count() == 16: + out.append((d0m, d1m)) + return out + + +def class82_choices(tm): + """All A0t = choice sets: one element of each {x, x+1} pair inside + C = H' \\ T, where T = D0+D1 must have 1-invariant complement. + Returns (choices, reason): choices empty with reason if impossible.""" + cm = ALL ^ tm + if trans(cm, 1) != cm: + return [], "C_not_1_invariant" + pairs = [] + seen = 0 + x = cm + choices = [0] + while x: + lsb = x & -x + p = lsb.bit_length() - 1 + if (seen >> p) & 1: + x ^= lsb + continue + q = p ^ 1 + if not (cm >> q) & 1: + return [], "C_pair_incomplete" + seen |= (1 << p) | (1 << q) + choices = [c | (1 << p) for c in choices] + [c | (1 << q) for c in choices] + x ^= lsb + return choices, "ok" + + +def class82_check(a0tm, d0m, d1m): + """The three coverage lines (I'),(II'),(III') for one configuration. + Returns (ok, which_lines_fail).""" + fails = [] + if (sumset_mask(a0tm, d0m) | sumset_mask(d1m, 3)) != ALL: + fails.append("I") + if (sumset_mask(a0tm, d1m) | sumset_mask(d0m, 3)) != ALL: + fails.append("II") + if (selfsum_mask(a0tm) | 3 | selfsum_mask(d0m) | selfsum_mask(d1m)) != ALL: + fails.append("III") + return (not fails), tuple(fails) + + +def class82_run(budget=None, shard=0, shards=1): + """Full decision run for class (8,2): every normalized Sidon D-pair, every + admissible A0t choice. Counts equality configurations and coverings. + Per-pair D-side masks are precomputed; (I') and (II') are decided by + OR-chains over the 8 chosen candidate translates, (III') only for + survivors. Deterministic sharding: pairs[shard::shards].""" + import itertools as _it + + t0 = time.time() + pairs = sidon44_pairs_normalized() + n_pairs_total = len(pairs) + pairs = pairs[shard::shards] + n_pairs = len(pairs) + n_choice_sets = 0 + covering = 0 + checked = 0 + fail_hist = {} + witnesses = [] + noninv = 0 + budget_hit = False + for (d0m, d1m) in pairs: + tm = sumset_mask(d0m, d1m) + choices, reason = class82_choices(tm) + if not choices: + noninv += 1 + continue + n_choice_sets += len(choices) + md1_01 = sumset_mask(d1m, 3) + md0_01 = sumset_mask(d0m, 3) + mdd = selfsum_mask(d0m) | selfsum_mask(d1m) + # per {x, x+1} pair inside C: (bit_p, bit_q, d0p, d0q, d1p, d1q) + cand = [] + seen = 0 + x = ALL ^ tm + while x: + lsb = x & -x + p = lsb.bit_length() - 1 + if (seen >> p) & 1: + x ^= lsb + continue + q = p ^ 1 + seen |= (1 << p) | (1 << q) + cand.append( + ( + 1 << p, + 1 << q, + trans(d0m, p), + trans(d0m, q), + trans(d1m, p), + trans(d1m, q), + ) + ) + x ^= lsb + for pick in _it.product((0, 1), repeat=len(cand)): + a0tm = 0 + s0 = 0 + s1 = 0 + for i, which in enumerate(pick): + c = cand[i] + if which == 0: + a0tm |= c[0] + s0 |= c[2] + s1 |= c[4] + else: + a0tm |= c[1] + s0 |= c[3] + s1 |= c[5] + checked += 1 + fails = [] + if (s0 | md1_01) != ALL: + fails.append("I") + if (s1 | md0_01) != ALL: + fails.append("II") + if (selfsum_mask(a0tm) | 3 | mdd) != ALL: + fails.append("III") + if fails: + fail_hist[tuple(fails)] = fail_hist.get(tuple(fails), 0) + 1 + else: + covering += 1 + if len(witnesses) < 5: + witnesses.append((elems(a0tm), elems(d0m), elems(d1m))) + if budget is not None and time.time() - t0 > budget: + budget_hit = True + break + return dict( + shard=shard, + shards=shards, + normalized_sidon_pairs_total=n_pairs_total, + normalized_sidon_pairs=n_pairs, + non_1_invariant_pairs=noninv, + admissible_choice_sets=n_choice_sets, + checked=checked, + covering_configs=covering, + fail_hist={str(k): v for k, v in sorted(fail_hist.items())}, + witnesses=witnesses, + budget_hit=budget_hit, + seconds=round(time.time() - t0, 2), + ) + + +# ------------------------------------------- class (6,0) at (12,6) + + +def transversals6(dm): + """All 6-sets X with X + D = F2^5 (X hits every translate x + D), for + D = dm. Complete branch-on-uncovered-requirement search with a bitmask + of covered requirements; results deduplicated as sets.""" + cov_by = [0] * N5 + for v in range(N5): + m = 0 + for x in range(N5): + if (dm >> (x ^ v)) & 1: + m |= 1 << x + cov_by[v] = m + out = set() + cur = [] + + def rec(uncov, vlo): + if len(cur) == 6: + if not uncov: + out.add(frozenset(cur)) + return + if uncov.bit_count() > 6 * (6 - len(cur)): + return + if not uncov: + for v in range(vlo, N5): + if v in cur: + continue + cur.append(v) + rec(uncov, v + 1) + cur.pop() + return + i = (uncov & -uncov).bit_length() - 1 + target = trans(dm, i) + for v in elems(target): + if v in cur: + continue + cur.append(v) + rec(uncov & ~cov_by[v], 0) + cur.pop() + + rec((1 << N5) - 1, 0) + return out + + +def class60_check(a0m, a1m, dm): + """Lines (I''),(II''),(III'') for one (A0, A1, D) triple.""" + fails = [] + if (sumset_mask(a0m, dm)) != ALL: + fails.append("I") + if (sumset_mask(a1m, dm)) != ALL: + fails.append("II") + if (selfsum_mask(a0m) | selfsum_mask(a1m) | selfsum_mask(dm)) != ALL: + fails.append("III") + return (not fails), tuple(fails) + + +def class60_run(budget=None, shard=0, shards=1): + """Decision run for class (6,0) at (12,6): complete D-side transversal + walk. Normalize 0 in D (H-half translation) and 0 in A1 (H'-half + translation; the class forces D1 = empty). For each normalized 6-set D, + F(D) = {6-sets X : X + D = F2^5} by complete search; then test every + (A0, A1) with A0 in F(D), A1 in F(D) containing 0 against A0+A1 = F2^5 + and line (III''). If F(D) is empty for every D, no (6,0) cover exists + (lines (I'')/(II'') are unsatisfiable). Deterministic sharding over the + C(31,5) normalized D by index.""" + t0 = time.time() + total_d = 169911 + tested_triples = 0 + covering = 0 + witnesses = [] + d_with_transversals = 0 + transversal_total = 0 + d_done = 0 + budget_hit = False + for idx, dc in enumerate(combinations(range(1, N5), 5)): + if idx % shards != shard: + continue + d_done += 1 + dm = 1 | mask_of(dc) + F = transversals6(dm) + if F: + d_with_transversals += 1 + transversal_total += len(F) + f_list = sorted(tuple(sorted(s)) for s in F) + for a1t in f_list: + if 0 not in a1t: + continue + a1m = mask_of(a1t) + for a0t in f_list: + a0m = mask_of(a0t) + if sumset_mask(a0m, a1m) != ALL: + continue + dm_self = selfsum_mask(dm) + if (selfsum_mask(a0m) | selfsum_mask(a1m) | dm_self) != ALL: + continue + tested_triples += 1 + covering += 1 + if len(witnesses) < 5: + witnesses.append((a0t, a1t, tuple(sorted(dc)) + (0,))) + if budget is not None and d_done % 64 == 0 and time.time() - t0 > budget: + budget_hit = True + break + return dict( + shard=shard, + shards=shards, + normalized_d_total=total_d, + d_checked=d_done, + d_with_transversals=d_with_transversals, + transversals_total=transversal_total, + tested_triples=tested_triples, + covering_triples=covering, + witnesses=witnesses, + budget_hit=budget_hit, + seconds=round(time.time() - t0, 2), + ) + + +# ------------------------------------------------- Fourier identity (7,1) + + +def fourier_71_identity(): + """Exact-integer contradiction for the (10,8) A-vanish tight class (7,1). + + L7 forces |A0+A1| = 25 with |A0| = |A1| = 5 (both odd) inside F2^5. + With f = 1_A0, g = 1_A1 and h = 1_S on S = A0+A1 (|S| = 25, all pair + sums distinct), Fourier over F2^5 gives h_hat(v) = f_hat(v) g_hat(v) for + every v (r = 1_S exactly). Parseval: + sum_{v != 0} f_hat^2 = 32*5 - 25 = 135 = sum_{v != 0} g_hat^2, + sum_{v != 0} h_hat^2 = 32*25 - 625 = 175. + Parity: |A0| odd makes every f_hat(v) odd, so f_hat^2 >= 1 pointwise; + hence (f_hat^2 - 1)(g_hat^2 - 1) >= 0 gives f_hat^2 g_hat^2 >= + f_hat^2 + g_hat^2 - 1 pointwise on v != 0 and therefore + sum h_hat^2 >= 135 + 135 - 31 = 239 > 175. Contradiction. + + Returns exact integers; the m=4 analogue (|A0| = 7, |A1| = 1 in F2^3) + computes need = lower = 7 (no contradiction), matching the real covers + of the m=4 analogue class in the PR 2933 F2^5 census.""" + out = {} + for tag, m, kx, ky, s_size in (("m5_k5", 5, 5, 5, 25), ("m3_k2", 3, 2, 2, 4)): + n = 1 << m + need = n * s_size - s_size * s_size + sum_alpha = n * kx - kx * kx + sum_beta = n * ky - ky * ky + odd = (kx % 2 == 1) and (ky % 2 == 1) + lower = sum_alpha + sum_beta - (n - 1) if odd else 0 + out[tag] = dict( + n=n, + kx=kx, + ky=ky, + s_size=s_size, + need=need, + sum_alpha=sum_alpha, + sum_beta=sum_beta, + lower_bound=lower, + parity_odd=odd, + contradiction=bool(odd and lower > need), + ) + n = 8 + out["m3_analogue_71"] = dict( + n=n, + kx=7, + ky=1, + s_size=7, + need=n * 7 - 49, + sum_alpha=n * 7 - 49, + sum_beta=n * 1 - 1, + lower_bound=(n * 7 - 49) + (n * 1 - 1) - (n - 1), + parity_odd=True, + contradiction=(n * 7 - 49) + (n * 1 - 1) - (n - 1) > n * 7 - 49, + ) + return out + + +# ------------------------------------------------- m=4 brute-force control + + +def control_m4_bruteforce(): + """Complete brute force of the two m=4 analogue classes (soundness and + completeness control for the L7 structural reduction). + + Analogue of the (7,1)-tight class: D-vanish (1,1), A split (7,1), + F1 = 7*1 + 1*1 = 8 = need. Analogue of the (8,2)-tight class: + A-vanish (2,2), D split (2,2), F1 = 4 + 4 = 8 = need. + + Direct route: every (A, D) pair with those splits inside E = F2^4 + (H = bit-0-even half, 8 points each coset), tested against the four L3 + lines. Every direct cover must show the L7 equality structure (both + cross sumsets Sidon, disjoint, union the whole odd half).""" + H = [x for x in range(16) if not (x & 1)] + Hp = [x for x in range(16) if x & 1] + + def ss(X, Y): + return {x ^ y for x in X for y in Y} + + def se(X): + return {x ^ y for x in X for y in X} + + def l3_lines(a0, a1, d0, d1): + ok_i = ss(a0, d0) | ss(a1, d1) == set(H) + ok_ii = ss(a0, d1) | ss(a1, d0) == set(Hp) + ok_iii = se(a0) | se(a1) | se(d0) | se(d1) == set(H) + ok_iv = ss(a0, a1) | ss(d0, d1) == set(Hp) + return ok_i and ok_ii and ok_iii and ok_iv + + res = {} + + covers_71 = [] + struct_71 = [] + for a0t in combinations(H, 7): + a0 = list(a0t) + for a1 in Hp: + for d0 in H: + for d1 in Hp: + if l3_lines(a0, [a1], [d0], [d1]): + covers_71.append((a0t, a1, d0, d1)) + sums = ss(a0, [a1]) + tset = set(Hp) - sums + struct_71.append( + len(sums) == 7 + and len(tset) == 1 + and ({d0 ^ d1} == tset) + ) + res["m4_class71_analogue"] = dict( + direct_covers=len(covers_71), + all_have_l7_structure=all(struct_71) if struct_71 else None, + ) + + covers_82 = [] + struct_82 = [] + for a0c in combinations(H, 2): + for a1c in combinations(Hp, 2): + for d0c in combinations(H, 2): + for d1c in combinations(Hp, 2): + a0, a1 = list(a0c), list(a1c) + d0, d1 = list(d0c), list(d1c) + if l3_lines(a0, a1, d0, d1): + covers_82.append((a0c, a1c, d0c, d1c)) + sumsA = ss(a0, a1) + sumsD = ss(d0, d1) + struct_82.append( + len(sumsA) == 4 + and len(sumsD) == 4 + and not (sumsA & sumsD) + and (sumsA | sumsD) == set(Hp) + ) + res["m4_class82_analogue"] = dict( + direct_covers=len(covers_82), + all_have_l7_structure=all(struct_82) if struct_82 else None, + ) + return res + + +def rho_classification(): + """Exact classification of the cross-multiplicity pattern of any + full-sumset pair of 6-sets in F2^5 (the forced structure of the (12,6) + A-vanish class (6,0), and of every (A, D) line (I'')/(II'')). + + Let X, Y be 6-sets with X + Y = F2^5 and r(s) = #{(x,y): x+y = s} = + 1 + rho(s), sum rho = 36 - 32 = 4. Fourier: rho_hat(v) = f_hat(v) + g_hat(v) for v != 0. Every f_hat(v), g_hat(v) is even and + |rho_hat(v)| <= sum rho = 4, so per nonzero v: f_hat(v) g_hat(v) is in + {0, 4, -4}, i.e. (f_hat, g_hat) = (0, *) or (*, 0) or both +-2. + Parseval gives sum_{v != 0} f_hat^2 = 156 and rho-Parseval gives + |V22| = 2 sum rho^2 - 1 where V22 = {v != 0: |f_hat| = |g_hat| = 2}. + + Case table (exact integers; the Walsh constraints are machine-checked in + test_engine.py): + + rho type sum rho^2 |V22| needed Walsh constraint verdict + 4 delta_p 16 31 rho_hat = +-4 always DEAD + 3+1 10 19 +-2 occurs for p != q DEAD + 2+2 8 15 subspace size 15 SURVIVES + 2+1+1 6 11 sizes 2^{5-r}-1 DEAD + 1+1+1+1 4 7 rank-3 flat / rank-2 SURVIVES + + DEAD reasons: (4 delta_p) Parseval 156 = 4*31 + (36a+16b) forces + 32 = 36a+16b with |Vf| = a + b = 0, impossible; (3+1) rho_hat = + 3(-1)^{vq} + (-1)^{vp} lies in {+-2, +-4} and |rho_hat| <= 4 needs + v*(p+q) = 0 for every v != 0, i.e. p = q; (2+1+1) V22 is + {v: v*(p1+p2) = 0 and v*(p1+q) = 0} minus {0}, of size 2^{5-r} - 1 in + {1,3,7,15,31}, never 11. + + Surviving types: + (T1) rho = 1 on an affine 2-flat {p1, p2, p3, p1+p2+p3} and 0 else; + (T2) rho = 2 on two distinct points {q1, q2} and 0 else. + Both sides' spectra are pinned: T1 has |Vf| = |Vg| = 8 all of magnitude + 4 and |V00| = 8; T2 has |Vf| = |Vg| = 6 and |V00| = 4.""" + return { + "types": [ + dict( + rho="4*delta_p", + sum_rho2=16, + v22_needed=31, + verdict="DEAD", + reason="Parseval 156 = 4*31 + (36a+16b) needs 32 = 36a+16b with |Vf| = 0", + ), + dict( + rho="3+1", + sum_rho2=10, + v22_needed=19, + verdict="DEAD", + reason="v*(p+q) = 0 for all v != 0 forces p = q", + ), + dict( + rho="2+2", + sum_rho2=8, + v22_needed=15, + verdict="SURVIVES", + v22=15, + vf=6, + vg=6, + v00=4, + ), + dict( + rho="2+1+1", + sum_rho2=6, + v22_needed=11, + verdict="DEAD", + reason="2^{5-r}-1 in {1,3,7,15,31}, never 11", + ), + dict( + rho="1+1+1+1", + sum_rho2=4, + v22_needed=7, + verdict="SURVIVES", + v22=7, + vf=8, + vg=8, + v00=8, + ), + ], + "surviving": ["2+2", "1+1+1+1"], + } + + +def identity_odd_sides(s, t, m=6): + """Cross-sum multiplicity identity for splits with BOTH sides odd (the + (11,7) and (9,9) splits, where no character can vanish - PR 2933 L2). + + With A an s-set and D a t-set in E = F2^m covering the odd line + A + D = E, the multiplicity is r = 1 + rho with sum rho = s*t - 2^m. + Fourier over E: rho_hat(v) = f_hat(v) g_hat(v) for v != 0, every f_hat + and g_hat is odd (s, t odd), so f_hat^2 g_hat^2 >= f_hat^2 + g_hat^2 - 1 + pointwise. Parseval: sum_{v != 0} f_hat^2 = 2^m s - s^2 and likewise + for g, sum_{v != 0} rho_hat^2 = 2^m sum rho^2 - (sum rho)^2. + + The pointwise inequality yields the EXACT necessary condition + 2^m sum rho^2 - (st - 2^m)^2 >= (2^m s - s^2) + (2^m t - t^2) + - (2^m - 1), + i.e. a lower bound on sum rho^2. For (11,7) and (9,9) at m = 6 the + bound is satisfiable (the excess 13 resp. 17 is too large for the + identity to contradict), so the identity is DEMOTED as an exclusion + mechanism for these splits; the numbers below are exact.""" + n = 1 << m + excess = s * t - n + sum_alpha = n * s - s * s + sum_beta = n * t - t * t + lower = sum_alpha + sum_beta - (n - 1) + # sum rho^2 >= ceil((lower + excess^2) / n) + num = lower + excess * excess + rho2_min = -(-num // n) + parity_odd = (s % 2 == 1) and (t % 2 == 1) + # products f_hat*g_hat must lie within +-excess pointwise + return dict( + split=(s, t), + m=m, + excess=excess, + sum_alpha=sum_alpha, + sum_beta=sum_beta, + pointwise_lower_sum_rho_hat_sq=lower, + sum_rho2_min=rho2_min, + sum_rho2_max=excess * excess, + parity_odd=parity_odd, + contradiction=bool(parity_odd and rho2_min > excess * excess), + ) diff --git a/research/f7-18point-remainder-kb3i-a1/vendor/vanish.py b/research/f7-18point-remainder-kb3i-a1/vendor/vanish.py new file mode 100644 index 0000000000..2dca0053f3 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/vendor/vanish.py @@ -0,0 +1,604 @@ +"""KB3f engine: vanishing-character classification for the 18-point cover +question for F2^7 (set level; no words). + +Object (unchanged from PR 2911, which this package presses): in the PR943 +prefix-walk model a restored seven-source singleton word is universal exactly +when its prefix set P covers, P + P = F2^7. A parity split S = A u B has A in +the even coset E (s points), B in the odd coset O (t points), s + t = 18. +PR 2911 PROVED that any (12,6) or (10,8) cover must have a vanishing +character off the all-ones hyperplane; this module classifies those +vanishing configurations and tests each class against coverage of the +remaining masks. + +Everything is exact Python integer arithmetic; no floats are used. + +Conventions. The even coset E is identified with F2^6 (m = 6); a character +of E is nontrivial psi_v(x) = (-1)^(v.x), v in 1..2^m-1. The (A, D) +reduction (PR 2911, PROVEN there): fix an odd p in F2^7 and D = p + B inside +E; S covers iff (i) A + D = E and (ii) (A+A) u (D+D) = E. + +Classification lemmas (all machine-checked in test_engine.py): + +L2 (halving). char_sum(A, v) = 0 iff A splits |A|/2 + |A|/2 across + ker(psi_v); so a vanishing on side A needs s even and forces the split + (s/2, s/2), and on side D needs t even and forces (t/2, t/2). At + (11,7) and (9,9) both sides are odd: NO character can vanish there. + +L3 (half-decomposition). With H = ker(psi_v), H' = E \\ H and A = A0 u A1, + D = D0 u D1 the two sides of ker(psi_v), coverage is equivalent to + (A0+D0) u (A1+D1) = H, (A0+D1) u (A1+D0) = H', + (A0+A0) u (A1+A1) u (D0+D0) u (D1+D1) = H, (A0+A1) u (D0+D1) = H'. + +L4 (class floors, exact union-size bounds on L3). With a split (a0, a1) of + A and (d0, d1) of D across ker(psi_v), the H'-even line forces + (F1) a0*a1 + d0*d1 >= 2^(m-1); the H-even line forces + (F2) sum over the four parts p of (1 + C(p,2) if p >= 1 else 0) >= 2^(m-1); + the odd lines force (F3) a0*d0 + a1*d1 >= 2^(m-1) and + (F4) a0*d1 + a1*d0 >= 2^(m-1). A class whose forced splits violate any + floor is PROVEN impossible: no cover realizes it. + +A class = (vanishing side, forced split of the vanishing side, split of the +other side). class_table enumerates all classes of a split; classify_cover +decides the classes of a concrete cover; census_f4/census_f5 enumerate the +smallest covers as ground truth for which classes actually occur. +""" + +import hashlib +import itertools +import random +import time +from collections import Counter + + +# ---------------------------------------------------------- F2^n basics + + +def dot(x, y): + return (x & y).bit_count() & 1 + + +def char_sum(pts, v): + """sum over pts of (-1)^(v.x).""" + return sum(1 - 2 * dot(p, v) for p in pts) + + +def split_sizes(pts, v, n): + """(|pts int ker(psi_v)|, |pts \\ ker(psi_v)|).""" + h0 = sum(1 for p in pts if not dot(v, p)) + return (h0, len(pts) - h0) + + +def char_representatives(n): + """One representative per nontrivial character of E: min(v, v ^ all1).""" + all1 = (1 << n) - 1 + out = [] + for v in range(1, all1): + if v < (v ^ all1): + out.append(v) + return out + + +def vanishing_set(pts, n): + """Character-level vanishing set (one entry per nontrivial character).""" + return {v for v in char_representatives(n) if char_sum(pts, v) == 0} + + +def vanishing_set_u(pts, n): + """u-level vanishing set: all indices v off {0, all-ones} with sum 0.""" + all1 = (1 << n) - 1 + return {v for v in range(1, all1) if char_sum(pts, v) == 0} + + +def sumset_xor(x, y): + return {a ^ b for a in x for b in y} + + +def selfsum_xor(x): + return {a ^ b for i, a in enumerate(x) for b in x[i:]} + + +def covers_f2n(pts, n): + cov = selfsum_xor(pts) + return len(cov) == (1 << n) + + +def cover_conditions(A, D, m): + """(A + D = F2^m, (A+A) u (D+D) = F2^m) -- the (A, D) reduction.""" + full = set(range(1 << m)) + odd_ok = sumset_xor(A, D) == full + even_ok = selfsum_xor(A) | selfsum_xor(D) == full + return odd_ok, even_ok + + +# ------------------------------------------------- half decomposition + + +def half_conditions(A, D, v, m): + """The four half lines of L3 for character psi_v.""" + A0 = [a for a in A if not dot(v, a)] + A1 = [a for a in A if dot(v, a)] + D0 = [d for d in D if not dot(v, d)] + D1 = [d for d in D if dot(v, d)] + H = {x for x in range(1 << m) if not dot(v, x)} + Hp = {x for x in range(1 << m) if dot(v, x)} + od0 = sumset_xor(A0, D0) | sumset_xor(A1, D1) + od1 = sumset_xor(A0, D1) | sumset_xor(A1, D0) + ev0 = selfsum_xor(A0) | selfsum_xor(A1) | selfsum_xor(D0) | selfsum_xor(D1) + ev1 = sumset_xor(A0, A1) | sumset_xor(D0, D1) + return ( + H <= od0, + Hp <= od1, + H <= ev0, + Hp <= ev1, + (len(A0), len(A1), len(D0), len(D1)), + ) + + +def check_half_decomposition(m, exhaustive=True, samples=0, seed=1): + """Verify L2 and L3 on every (A, D) pair (m <= 3) or on random samples.""" + rng = random.Random(seed) + N = 1 << m + pairs = 0 + if exhaustive: + sets = [] + for mask in range(1 << N): + sets.append([x for x in range(N) if (mask >> x) & 1]) + iterator = itertools.product(sets, repeat=2) + else: + def rand_iter(): + for _ in range(samples): + A = [x for x in range(N) if rng.randrange(2)] + D = [x for x in range(N) if rng.randrange(2)] + yield (A, D) + iterator = rand_iter() + for A, D in iterator: + pairs += 1 + for v in range(1, N): + cs = char_sum(A, v) + a0, a1 = split_sizes(A, v, m) + l2 = (cs == 0) == (len(A) % 2 == 0 and a0 == len(A) // 2) + if not l2: + return dict(ok=False, pairs=pairs, fail="L2", A=A, D=D, v=v) + od0, od1, ev0, ev1, _ = half_conditions(A, D, v, m) + direct = cover_conditions(A, D, m) + if (od0 and od1 and ev0 and ev1) != all(direct): + return dict(ok=False, pairs=pairs, fail="L3", A=A, D=D, v=v) + return dict(ok=True, pairs=pairs) + + +def two_vanishing_structure(A, v1, v2, m): + """L5 (multi-vanishing structure). If char_sum(A, v1) = char_sum(A, v2) + = 0 for distinct characters, the counts of A across the four parts of the + (ker(psi_v1), ker(psi_v2)) grid are (x, y, y, x) with x + y = |A|/2. + Returns (counts, ok) where counts = (n00, n01, n10, n11) in the grid.""" + n00 = n01 = n10 = n11 = 0 + for a in A: + b1, b2 = dot(v1, a), dot(v2, a) + if b1 == 0 and b2 == 0: + n00 += 1 + elif b1 == 0: + n01 += 1 + elif b2 == 0: + n10 += 1 + else: + n11 += 1 + ok = n00 == n11 and n01 == n10 + return (n00, n01, n10, n11), ok + + +def check_multi_vanishing(m): + """Verify L5 for every subset A of F2^m and every vanishing pair.""" + N = 1 << m + checked = 0 + for mask in range(1 << N): + A = [x for x in range(N) if (mask >> x) & 1] + van = [v for v in range(1, N) if char_sum(A, v) == 0] + for i in range(len(van)): + for j in range(i): + counts, ok = two_vanishing_structure(A, van[j], van[i], m) + checked += 1 + if not ok: + return dict(ok=False, checked=checked, A=A, v=(van[j], van[i]), counts=counts) + return dict(ok=True, checked=checked) + + +def sidon_pair(X, Y): + """All |X|*|Y| sums x+y distinct (no nontrivial common difference).""" + return len(sumset_xor(X, Y)) == len(X) * len(Y) + + +def check_tight_equality(m): + """L7 (equality analysis of the F1 floor). Whenever a0*a1 + d0*d1 = + 2^(m-1) and the pair (A, D) covers, the H' even line forces + |A0+A1| = a0*a1 (a Sidon pair), |D0+D1| = d0*d1 (a Sidon pair), and the + two cross sumsets are disjoint (their union is H').""" + N = 1 << m + need = 1 << (m - 1) + checked = 0 + sets = [[x for x in range(N) if (mask >> x) & 1] for mask in range(1 << N)] + for A in sets: + for D in sets: + if not all(cover_conditions(A, D, m)): + continue + for v in range(1, N): + A0 = [a for a in A if not dot(v, a)] + A1 = [a for a in A if dot(v, a)] + D0 = [d for d in D if not dot(v, d)] + D1 = [d for d in D if dot(v, d)] + if len(A0) * len(A1) + len(D0) * len(D1) != need: + continue + checked += 1 + sA = sumset_xor(A0, A1) + sD = sumset_xor(D0, D1) + if len(sA) != len(A0) * len(A1): + return dict(ok=False, checked=checked, fail="A0+A1 not Sidon", A=A, D=D, v=v) + if len(sD) != len(D0) * len(D1): + return dict(ok=False, checked=checked, fail="D0+D1 not Sidon", A=A, D=D, v=v) + if sA & sD: + return dict(ok=False, checked=checked, fail="cross sumsets overlap", A=A, D=D, v=v) + return dict(ok=True, checked=checked) + + +# ------------------------------------------------------- class table + + +def _bound2(part): + return (1 + part * (part - 1) // 2) if part >= 1 else 0 + + +def class_table(s, t, m=6): + """All vanishing classes of the split (s, t) at E = F2^m and their floor + verdicts. A class: vanishing side A (forced split s/2 + s/2) with the + other side's split (d0, d1), or vanishing side D (forced t/2 + t/2) with + the other side's split (a0, a1). Verdict dead iff some exact floor of L4 + fails; survives-tight iff F1 holds with equality.""" + need = 1 << (m - 1) + out = {"split": (s, t), "m": m, "floor_need_F1": need, "vanishing_possible": False} + + def floors(a0, a1, d0, d1): + return { + "F1": a0 * a1 + d0 * d1, + "F2": _bound2(a0) + _bound2(a1) + _bound2(d0) + _bound2(d1), + "F3": a0 * d0 + a1 * d1, + "F4": a0 * d1 + a1 * d0, + } + + def entry(vanishing_side, van_split, other_split, a0, a1, d0, d1): + fl = floors(a0, a1, d0, d1) + ok = all(v >= need for v in fl.values()) + tight = ok and fl["F1"] == need + forced = None + if ok and tight: + forced = ( + "equality: |A0+A1| = a0*a1 and |D0+D1| = d0*d1 (both Sidon), " + "the two cross sumsets disjoint with union the whole odd half" + ) + elif ok and d0 * d1 == 0: + forced = "D cross sums empty: |A0+A1| = the whole odd half" + elif ok and a0 * a1 == 0: + forced = "A cross sums empty: |D0+D1| = the whole odd half" + return dict( + vanishing_side=vanishing_side, + vanishing_split=van_split, + other_split=other_split, + splits=dict(A=(a0, a1), D=(d0, d1)), + floors=fl, + floor_value=fl["F1"], + floor_need=need, + verdict=("survives" if ok else "dead"), + tight=tight, + forced=forced, + ) + + A_rows, D_rows = [], [] + if s % 2 == 0: + out["vanishing_possible"] = True + for d0 in range(t, (t - 1) // 2, -1): + d1 = t - d0 + A_rows.append(entry("A", (s // 2, s // 2), (d0, d1), s // 2, s // 2, d0, d1)) + if t % 2 == 0: + out["vanishing_possible"] = True + for a0 in range(s, (s - 1) // 2, -1): + a1 = s - a0 + D_rows.append(entry("D", (t // 2, t // 2), (a0, a1), a0, a1, t // 2, t // 2)) + out["A_vanish"] = A_rows + out["D_vanish"] = D_rows + return out + + +# ---------------------------------------------------- cover census + + +def classify_cover(S, n): + """Classify a covering set S of F2^n by its vanishing classes (ground + truth for 'which characters can vanish').""" + A = [x for x in S if x.bit_count() % 2 == 0] + B = [x for x in S if x.bit_count() % 2 == 1] + D = [1 ^ b for b in B] + m = n - 1 + need = 1 << (m - 1) + k_A = vanishing_set(A, n) + k_D = vanishing_set(D, n) + rows = [] + dead = [] + for v in sorted(k_A | k_D): + a0, a1 = split_sizes(A, v, n) + d0, d1 = split_sizes(D, v, n) + val = a0 * a1 + d0 * d1 + verdict = "survives" if val >= need else "dead" + side = ("A" if v in k_A else "") + ("D" if v in k_D else "") + rows.append((v, side, (a0, a1), (d0, d1), verdict)) + if verdict == "dead": + dead.append((v, side, (a0, a1), (d0, d1))) + return dict( + S=sorted(S), + split=(len(A), len(B)), + k_A=len(k_A), + k_D=len(k_D), + vanish_rows=rows, + dead_classes_hit=dead, + ) + + +def _aggregate(rec, agg, class_agg): + agg[("%d_%d" % rec["split"], rec["k_A"], rec["k_D"])] += 1 + for (v, side, a_sp, d_sp, verdict) in rec["vanish_rows"]: + class_agg[(side, a_sp, d_sp, verdict)] += 1 + + +def _ser_agg(agg): + return sorted(["%s kA=%d kD=%d" % k, v] for k, v in agg.items()) + + +def _ser_class_agg(class_agg): + return sorted( + ["%s a=%d,%d d=%d,%d %s" % (side, a_sp[0], a_sp[1], d_sp[0], d_sp[1], verdict), v] + for (side, a_sp, d_sp, verdict), v in class_agg.items() + ) + + +def census_f4(keep=100): + """Exhaustive: every subset S of F2^4 with S + S = F2^4, classified.""" + N = 16 + full = set(range(N)) + pair = [[0] * N for _ in range(N)] + for i in range(N): + for j in range(N): + pair[i][j] = i ^ j + agg = Counter() + class_agg = Counter() + covers = [] + covers_total = 0 + dead_hit = [] + for mask in range(1, 1 << N): + S = [x for x in range(N) if (mask >> x) & 1] + cov = {0} + for i in range(len(S)): + for j in range(i): + cov.add(pair[S[i]][S[j]]) + if cov != full: + continue + covers_total += 1 + rec = classify_cover(S, 4) + _aggregate(rec, agg, class_agg) + if rec["dead_classes_hit"]: + dead_hit.append(rec["dead_classes_hit"]) + if len(covers) < keep: + covers.append(S) + return dict( + covers_total=covers_total, + covers=covers, + agg=_ser_agg(agg), + class_agg=_ser_class_agg(class_agg), + dead_classes_hit=dead_hit, + ) + + +def census_f5(shard=0, shards=16, keep_covers=5, n=5, k=10, max_combos=None): + """Shard `shard` of the full k-subset census of F2^n (n = 5, k = 10): + every k-subset S with S + S = F2^n is classified by vanishing class. + Independent enumeration route (all C(32,10) combinations) for the + recorded PR 2773 n5 control value 99,200 ten-point covers. max_combos + truncates a shard (smoke tests only; a complete census passes None).""" + N = 1 << n + full = (1 << N) - 1 + pairbit = [[0] * N for _ in range(N)] + for i in range(N): + for j in range(N): + pairbit[i][j] = 1 << (i ^ j) + agg = Counter() + class_agg = Counter() + covers = [] + covers_total = 0 + dead_hit = [] + combos = 0 + for S in itertools.combinations(range(N), k): + if S[0] % shards != shard: + continue + combos += 1 + if max_combos is not None and combos > max_combos: + combos -= 1 + return dict( + shard=shard, + shards=shards, + status="partial", + combos=combos, + covers_total=covers_total, + covers=covers, + agg=_ser_agg(agg), + class_agg=_ser_class_agg(class_agg), + dead_classes_hit=dead_hit, + ) + cov = 1 + for i in range(k): + si = S[i] + row = pairbit[si] + for j in range(i): + cov |= row[S[j]] + if cov != full: + continue + covers_total += 1 + rec = classify_cover(list(S), n) + _aggregate(rec, agg, class_agg) + if rec["dead_classes_hit"]: + dead_hit.append(rec["dead_classes_hit"]) + if len(covers) < keep_covers: + covers.append(sorted(S)) + return dict( + shard=shard, + shards=shards, + status="complete", + combos=combos, + covers_total=covers_total, + covers=covers, + agg=_ser_agg(agg), + class_agg=_ser_class_agg(class_agg), + dead_classes_hit=dead_hit, + ) + + +# ------------------------------------------------- class-restricted search + + +def _score_pair(A, D): + """|A + D| + |(A+A) u (D+D)| as integer bitmasks (target 2^(m+1)).""" + cm = 1 + for a in A: + for d in D: + cm |= 1 << (a ^ d) + sm = 1 + for i, a in enumerate(A): + for b in A[i:]: + sm |= 1 << (a ^ b) + for i, d in enumerate(D): + for b in D[i:]: + sm |= 1 << (d ^ b) + return cm.bit_count() + sm.bit_count() + + +def search_class(s, t, side, other_split, restarts=20, seed=1, seconds=20.0, m=6): + """Bounded seeded local search for a covering (A, D) pair in E = F2^m + constrained to one vanishing class: psi = bit 0 (WLOG under GL(m, 2)), + the vanishing side split equally across ker(psi), the other side split + exactly `other_split`. A found pair is a falsifying instance for the + class contradiction and (at m = 6) an 18-point cover witness; a failed + bounded search is a scoped search failure, never an exclusion.""" + rng = random.Random(seed) + N = 1 << m + target = 2 * N + + if side == "A_vanish": + a_h0 = s // 2 + a_h1 = s // 2 + d_h0, d_h1 = other_split + else: + d_h0 = t // 2 + d_h1 = t // 2 + a_h0, a_h1 = other_split + half0 = [x for x in range(N) if not (x & 1)] + half1 = [x for x in range(N) if (x & 1)] + + def build(): + A = rng.sample(half0, a_h0) + rng.sample(half1, a_h1) + D = rng.sample(half0, d_h0) + rng.sample(half1, d_h1) + return A, D + + best = (0, None) + moves = 0 + t0 = time.time() + for _ in range(restarts): + if time.time() - t0 > seconds: + break + A, D = build() + sc = _score_pair(A, D) + improved = True + while improved and time.time() - t0 < seconds: + improved = False + for cur in (A, D): + for half in (half0, half1): + for i in range(len(cur)): + if (cur[i] & 1) != (half[0] & 1): + continue + for v in half: + if v in cur: + continue + moves += 1 + old = cur[i] + cur[i] = v + new = _score_pair(A, D) + if new > sc: + sc = new + improved = True + break + cur[i] = old + if sc == target: + break + if sc == target: + break + if sc == target: + break + if sc == target: + return dict( + found=True, + score=sc, + A=sorted(A), + D=sorted(D), + side=side, + other_split=other_split, + moves=moves, + seconds=round(time.time() - t0, 2), + ) + if sc > best[0]: + best = (sc, (sorted(A), sorted(D))) + return dict( + found=False, + score=best[0], + best_pair=best[1], + side=side, + other_split=other_split, + restarts=restarts, + moves=moves, + seconds=round(time.time() - t0, 2), + ) + + +def search_free(s, t, restarts=20, seed=1, seconds=20.0, m=6): + """Unconstrained bounded seeded search for a covering (A, D) pair in + E = F2^m (non-vacuity control for the class-restricted machinery).""" + rng = random.Random(seed) + N = 1 << m + target = 2 * N + pool = list(range(N)) + best = (0, None) + t0 = time.time() + for _ in range(restarts): + if time.time() - t0 > seconds: + break + A = rng.sample(pool, s) + D = rng.sample(pool, t) + sc = _score_pair(A, D) + improved = True + while improved and time.time() - t0 < seconds: + improved = False + for cur, size in ((A, s), (D, t)): + outside = [x for x in pool if x not in cur] + for i in range(size): + for v in outside: + old = cur[i] + cur[i] = v + new = _score_pair(A, D) + if new > sc: + sc = new + improved = True + outside[outside.index(v)] = old + if sc == target: + return dict(found=True, score=sc, A=sorted(A), D=sorted(D)) + else: + cur[i] = old + if sc > best[0]: + best = (sc, (sorted(A), sorted(D))) + return dict(found=False, score=best[0], best_pair=best[1]) + + +def sha256_file(path): + return hashlib.sha256(path.read_bytes()).hexdigest() diff --git a/research/f7-18point-remainder-kb3i-a1/verify.py b/research/f7-18point-remainder-kb3i-a1/verify.py new file mode 100644 index 0000000000..24b7e45ba8 --- /dev/null +++ b/research/f7-18point-remainder-kb3i-a1/verify.py @@ -0,0 +1,232 @@ +"""KB3i registered replay: re-derives every number cited in the README/PR for +the 18-point cover question remainder ((4,2)/(3,3)/(11,7)/(9,9)), set level. + +Modes: + quick vendored pins + anchor reproduction (FOURIER 7,1 =175/239, + OBSTRUCTION 696/504/192, CLASSIFY 32=32 TIGHT cases=6720), + the complete m=3 reduced-covering census (parity-shortcut DEMOTION), + and the (11,7)/(9,9) identity-frontier numbers. + marker PASS_KB3I_QUICK + full quick + the complete m=4 sum-10 split censuses (the m=5 ground + truth: (2,8),(4,6) cover; (1,9),(3,7),(5,5) empty) and the (5,5) + self-obstruction localization. Slower (minutes). + marker PASS_KB3I_FULL + search the bounded construction search ceiling (route c). marker PASS_KB3I_SEARCH + +Everything is exact integer arithmetic (int bitmasks, no floats). The census +counts below are COMPLETE enumerations (brute force over all subset pairs at +the stated sizes); a zero count with complete enumeration PROVES the split +empty at that (m, split). +""" + +import hashlib +import sys +import time +from itertools import combinations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE / "vendor")) +sys.stdout.reconfigure(encoding="utf-8") + +import cover18 as c18 # noqa: E402 +import tight # noqa: E402 +import vanish # noqa: E402 + +VENDOR_PINS = { + "vendor/tight.py": "14670ef2d3df9e4ecc9e1db962f4e8cb77545d1c889144352760c1fd14e2273b", + "vendor/cover18.py": "24c6a2f4911dc2d5de76972eb5ae93dc4e66d8fa1e904443de6d0638e70c0a04", + "vendor/vanish.py": "6c605c54074f725321c5d770d538a652bf7727598a128270831f92fe7b9746d9", + "vendor/agent64_cover17.py": "082bc838134cba9754368cff894d53c729467a689b4cafee8374423688d93654", + "vendor/agent64_search17.py": "9eb1bf79ffb99b0efcdaf57916c493bc781abd4a0096d584dc6bc6ca294bf674", + "vendor/anchors.py": "73d73a9b94539403448d7ff8c914c03711907f75c019c4ccb6843b32c259e8e7", +} + + +def sha256_file(p): + return hashlib.sha256(Path(p).read_bytes()).hexdigest() + + +def check_pins(): + for rel, want in VENDOR_PINS.items(): + got = sha256_file(HERE / rel) + assert got == want, (rel, got, want) + print("PIN all %d vendored engines sha256 match" % len(VENDOR_PINS), flush=True) + + +# ---------------------------------------------------- reduced-covering census + + +def _build(m): + gsize = 1 << m + allg = (1 << gsize) - 1 + xors = [[1 << (i ^ j) for j in range(gsize)] for i in range(gsize)] + + def trans(mask, a): + out = 0 + x = mask + while x: + lsb = x & -x + out |= xors[lsb.bit_length() - 1][a] + x ^= lsb + return out + + def sumset(mx, my): + out = 0 + x = mx + while x: + lsb = x & -x + out |= trans(my, lsb.bit_length() - 1) + x ^= lsb + return out + + return gsize, allg, sumset + + +def _mask_of(idxs): + m = 0 + for i in idxs: + m |= 1 << i + return m + + +def census_split_count(m, a, b): + """COMPLETE count of reduced covering (A,B) pairs in F2^m with |A|=a,|B|=b. + Returns (covers, cross_covering, self_covering_when_cross, max_selfunion).""" + gsize, allg, sumset = _build(m) + Alist = [_mask_of(c) for c in combinations(range(gsize), a)] + Blist = [_mask_of(c) for c in combinations(range(gsize), b)] + covers = 0 + cross_cov = 0 + self_when_cross = 0 + max_su = -1 + for am in Alist: + ssa = sumset(am, am) + for bm in Blist: + if sumset(am, bm) != allg: + continue + cross_cov += 1 + su = ssa | sumset(bm, bm) + su_sz = su.bit_count() + if su_sz > max_su: + max_su = su_sz + if su == allg: + self_when_cross += 1 + covers += 1 + return covers, cross_cov, self_when_cross, max_su + + +def m3_census(): + """Complete reduced-covering census of F2^3 by split; return the both-odd + nonempty list and the (5,5),(3,3) counts.""" + gsize, allg, sumset = _build(3) + both_odd_nonempty = [] + counts = {} + for a in range(9): + for b in range(9): + Alist = [_mask_of(c) for c in combinations(range(gsize), a)] + Blist = [_mask_of(c) for c in combinations(range(gsize), b)] + cnt = 0 + for am in Alist: + ssa = sumset(am, am) + for bm in Blist: + if sumset(am, bm) == allg and (ssa | sumset(bm, bm)) == allg: + cnt += 1 + counts[(a, b)] = cnt + if cnt > 0 and a % 2 == 1 and b % 2 == 1: + both_odd_nonempty.append((a, b)) + return counts, both_odd_nonempty + + +def mode_quick(): + t0 = time.time() + check_pins() + # Anchor: PR 2961 FOURIER (7,1) + fid = tight.fourier_71_identity() + assert (fid["m5_k5"]["need"], fid["m5_k5"]["lower_bound"]) == (175, 239), fid + print("ANCHOR PR2961 FOURIER (7,1) need=175 lower=239 contradiction=True", flush=True) + # Anchor: PR 2933 CLASSIFY 32=32 TIGHT cases=6720 + res7 = vanish.check_tight_equality(3) + assert res7["checked"] == 6720 and res7["ok"], res7 + print("ANCHOR PR2933 CLASSIFY tight-equality Sidon m=3 cases=6720 ok=true", flush=True) + tight_seen = 0 + for (s, t) in [(12, 6), (11, 7), (10, 8), (9, 9)]: + tab = vanish.class_table(s, t, m=6) + for side in ("A_vanish", "D_vanish"): + for c in tab[side]: + if c["tight"]: + tight_seen += 1 + assert tight_seen == 2, tight_seen + print("ANCHOR PR2933 CLASSIFY 32=32 TIGHT count=2 across splits", flush=True) + # Anchor: PR 2870 OBSTRUCTION + sq = c18.squeeze_numbers(7, 11, 6) + assert (sq["parseval_remainder"], sq["max_allowed"], sq["deficit"]) == (696, 504, 192), sq + print("ANCHOR PR2870 OBSTRUCTION parseval=696 allowed=504 deficit=192", flush=True) + + # PARITY-SHORTCUT DEMOTION: complete m=3 census. + counts, bon = m3_census() + assert counts[(5, 5)] == 3136, counts[(5, 5)] + assert counts[(7, 7)] == 64, counts[(7, 7)] + assert counts[(3, 3)] == 0, counts[(3, 3)] + expected_bon = [(3, 5), (3, 7), (5, 3), (5, 5), (5, 7), (7, 3), (7, 5), (7, 7)] + assert bon == expected_bon, bon + print("DEMOTION m=3 COMPLETE: both-odd covers EXIST: %s" % (bon,), flush=True) + print(" (5,5) covers=%d, (7,7) covers=%d, (3,3) covers=0" + % (counts[(5, 5)], counts[(7, 7)]), flush=True) + print(" => 'both-odd impossible by parity' is FALSE; cannot kill (11,7)/(9,9)", flush=True) + + # IDENTITY FRONTIER for (11,7)/(9,9). + for (s, t, eo_want, eh_want) in ((11, 7, 13, 42), (9, 9, 17, 34)): + eo = s * t - 64 + eh = c18.even_half_max(7, s, t) + assert eo == eo_want and eh == eh_want, (s, t, eo, eh) + vals = c18.rho_square_values(eo) + sqz = c18.squeeze_numbers(7, s, t) + print("FRONTIER (%d,%d): E_o=%d even_half_max=%d min_sum_rho2=%d squeeze_opposite=%s" + % (s, t, eo, eh, vals[0], sqz["opposite_parity"]), flush=True) + print("PASS_KB3I_QUICK seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_full(): + mode_quick() + t0 = time.time() + # m=5 ground truth: complete m=4 sum-10 split censuses. + print("=== m=5 ground truth: COMPLETE m=4 reduced covering by sum-10 split ===", flush=True) + expect = {(2, 8): ">0", (4, 6): ">0", (1, 9): 0, (3, 7): 0, (5, 5): 0} + for (a, b), want in expect.items(): + covers, cross_cov, self_when_cross, max_su = census_split_count(4, a, b) + if want == ">0": + assert covers > 0, (a, b, covers) + else: + assert covers == 0, (a, b, covers) + print(" (%d,%d): covers=%d cross_covering=%d self_when_cross=%d max_selfunion=%d/16" + % (a, b, covers, cross_cov, self_when_cross, max_su), flush=True) + # (5,5) self obstruction localization. + covers, cross_cov, self_when_cross, max_su = census_split_count(4, 5, 5) + assert covers == 0 and self_when_cross == 0 and cross_cov > 0, (covers, self_when_cross, cross_cov) + assert max_su == 15, max_su + print("SELF-OBSTRUCTION (5,5): cross_covering=%d, self_covering_when_cross=%d, " + "max_self_union=%d/16 (never 16)" % (cross_cov, self_when_cross, max_su), flush=True) + print("PASS_KB3I_FULL seconds=%.1f" % (time.time() - t0), flush=True) + + +def mode_search(): + t0 = time.time() + check_pins() + rec = c18.search_direct(k=18, restarts=40, seed=1, seconds=25.0, n=7) + print("SEARCH k=18 direct: found=%s score=%d/128 (record ceiling 119/128)" + % (rec["found"], rec["score"]), flush=True) + assert not rec["found"], rec + print("PASS_KB3I_SEARCH seconds=%.1f" % (time.time() - t0), flush=True) + + +def main(): + mode = sys.argv[1] if len(sys.argv) > 1 else "quick" + modes = {"quick": mode_quick, "full": mode_full, "search": mode_search} + if mode not in modes: + raise SystemExit("usage: verify.py quick|full|search") + modes[mode]() + + +if __name__ == "__main__": + main()