From bede750d1aaa0e47930a398d4779078f8107370d Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 10:42:04 +0100 Subject: [PATCH] feat(research): prove BW16 clique insertion barriers --- .../CLIQUE72.json | 1 + .../bw16-clique-exchange-barrier/NOTICE.md | 8 + .../bw16-clique-exchange-barrier/README.md | 198 +++++++++++++++++ .../bw16-clique-exchange-barrier/SOURCES.json | 29 +++ .../bw16-clique-exchange-barrier/TASK.json | 72 +++++++ .../bw16-clique-exchange-barrier/VERIFY.json | 57 +++++ .../bw16-clique-exchange-barrier/verify.py | 203 ++++++++++++++++++ 7 files changed, 568 insertions(+) create mode 100644 research/bw16-clique-exchange-barrier/CLIQUE72.json create mode 100644 research/bw16-clique-exchange-barrier/NOTICE.md create mode 100644 research/bw16-clique-exchange-barrier/README.md create mode 100644 research/bw16-clique-exchange-barrier/SOURCES.json create mode 100644 research/bw16-clique-exchange-barrier/TASK.json create mode 100644 research/bw16-clique-exchange-barrier/VERIFY.json create mode 100644 research/bw16-clique-exchange-barrier/verify.py diff --git a/research/bw16-clique-exchange-barrier/CLIQUE72.json b/research/bw16-clique-exchange-barrier/CLIQUE72.json new file mode 100644 index 0000000000..2b604e87c5 --- /dev/null +++ b/research/bw16-clique-exchange-barrier/CLIQUE72.json @@ -0,0 +1 @@ +[[0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, -2], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, -2, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, -2, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, -2, 0], [0, 0, 0, 0, 0, 0, 0, 0, 1, -1, -1, -1, -1, -1, 1, -1], [0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 1, -1, 1, -1, 1, -1], [0, 0, 0, 0, 0, 0, 0, 0, 1, 1, -1, 1, 1, 1, -1, 1], [0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, -1, 1, -1, 1], [0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, -2, 0], [0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, -2, 0], [0, 0, 0, 0, 1, -1, -1, -1, 0, 0, 0, 0, -1, -1, 1, -1], [0, 0, 0, 0, 1, -1, 1, -1, 0, 0, 0, 0, 1, -1, 1, -1], [0, 0, 0, 0, 1, 1, -1, 1, 0, 0, 0, 0, 1, 1, -1, 1], [0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, -1, 1, -1, 1], [0, 1, 0, 1, 0, -1, 0, -1, 0, -1, 0, -1, 0, -1, 0, -1], [1, 0, -1, 0, 0, -1, 0, -1, 0, -1, 0, -1, -1, 0, 1, 0], [0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1, 0, 1], [1, 0, -1, 0, 0, 1, 0, 1, 0, 1, 0, 1, 1, 0, -1, 0], [1, 0, 1, 0, 0, -1, 0, -1, 0, -1, 0, -1, 1, 0, 1, 0], [1, 0, 1, 0, 0, 1, 0, 1, 0, 1, 0, 1, -1, 0, -1, 0], [0, 0, 1, -1, -1, -1, 0, 0, -1, -1, 0, 0, 0, 0, 1, -1], [0, 0, 1, -1, 0, 0, -1, -1, 0, 0, -1, -1, 0, 0, 1, -1], [0, 0, 1, -1, 0, 0, 1, -1, 0, 0, 1, -1, 0, 0, 1, -1], [0, 0, 1, -1, 1, -1, 0, 0, 1, -1, 0, 0, 0, 0, 1, -1], [0, 1, 0, -1, 0, -1, 0, -1, 0, -1, 0, -1, 0, 1, 0, -1], [0, 0, 1, 1, -1, 1, 0, 0, 1, 1, 0, 0, 0, 0, -1, 1], [0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, -2, 0], [0, 0, 1, 1, 0, 0, -1, 1, 0, 0, 1, 1, 0, 0, -1, 1], [0, 0, 1, 1, 0, 0, 1, 1, 0, 0, -1, 1, 0, 0, -1, 1], [0, 0, 1, 1, 1, 1, 0, 0, -1, 1, 0, 0, 0, 0, -1, 1], [1, -1, 0, 0, -1, 1, 0, 0, 0, 0, -1, 1, 0, 0, -1, 1], [1, -1, -1, 1, 0, 0, 0, 0, 0, 0, 0, 0, -1, 1, -1, 1], [1, -1, 0, 0, 0, 0, -1, 1, -1, 1, 0, 0, 0, 0, -1, 1], [1, -1, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0, 0, 0, -1, 1], [1, -1, 0, 0, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, -1, 1], [1, -1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, -1, 1], [1, 0, 0, 1, -1, 0, 0, 1, 0, 1, 1, 0, 0, 1, -1, 0], [0, 1, -1, 0, 0, -1, -1, 0, 0, -1, -1, 0, 0, -1, 1, 0], [0, 1, -1, 0, 1, 0, 0, -1, 1, 0, 0, -1, 0, -1, 1, 0], [0, 1, 0, -1, 0, -1, 0, -1, 1, 0, -1, 0, 1, 0, 1, 0], [0, 1, 0, -1, 1, 0, -1, 0, 0, -1, 0, -1, 1, 0, 1, 0], [1, 0, 0, 1, 0, 1, 1, 0, -1, 0, 0, 1, 0, 1, -1, 0], [0, 1, 0, -1, -1, 0, -1, 0, 0, -1, 0, -1, -1, 0, 1, 0], [0, 1, 0, -1, 0, -1, 0, -1, 0, -1, 0, 1, 0, -1, 0, -1], [0, 1, 0, -1, 0, -1, 0, -1, 1, 0, 1, 0, -1, 0, 1, 0], [0, 1, 0, -1, 0, 1, 0, -1, 0, -1, 0, -1, 0, -1, 0, -1], [0, 1, 1, 0, -1, 0, 0, -1, 1, 0, 0, -1, 0, -1, 1, 0], [0, 1, 1, 0, 0, -1, -1, 0, 0, -1, 1, 0, 0, -1, 1, 0], [1, 0, 0, -1, -1, 0, 0, -1, 0, -1, -1, 0, 0, -1, 1, 0], [1, 0, 0, -1, 1, 0, 0, -1, 0, -1, 1, 0, 0, -1, 1, 0], [1, 0, 0, 1, 1, 0, 0, 1, 0, 1, -1, 0, 0, 1, -1, 0], [1, 1, 0, 0, 0, 0, -1, -1, 1, -1, 0, 0, 0, 0, 1, -1], [0, 1, -1, 0, -1, 0, 0, -1, -1, 0, 0, -1, 0, -1, 1, 0], [0, 1, -1, 0, 0, -1, 1, 0, 0, -1, 1, 0, 0, -1, 1, 0], [0, 1, 0, -1, -1, 0, 1, 0, 0, -1, 0, -1, 1, 0, 1, 0], [0, 1, 0, -1, 0, -1, 0, -1, -1, 0, -1, 0, -1, 0, 1, 0], [0, 1, 0, -1, 0, -1, 0, -1, -1, 0, 1, 0, 1, 0, 1, 0], [0, 1, 0, -1, 0, -1, 0, -1, 0, -1, 0, -1, 0, -1, 0, 1], [0, 1, 0, -1, 0, -1, 0, -1, 0, 1, 0, -1, 0, -1, 0, -1], [0, 1, 0, -1, 0, -1, 0, 1, 0, -1, 0, -1, 0, -1, 0, -1], [0, 1, 0, -1, 1, 0, 1, 0, 0, -1, 0, -1, -1, 0, 1, 0], [0, 1, 1, 0, 0, -1, 1, 0, 0, -1, -1, 0, 0, -1, 1, 0], [0, 1, 1, 0, 1, 0, 0, -1, -1, 0, 0, -1, 0, -1, 1, 0], [0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0], [1, 0, 0, -1, 0, -1, -1, 0, -1, 0, 0, -1, 0, -1, 1, 0], [1, 0, 0, -1, 0, -1, 1, 0, 1, 0, 0, -1, 0, -1, 1, 0], [1, 0, 0, 1, 0, 1, -1, 0, 1, 0, 0, 1, 0, 1, -1, 0], [1, 1, -1, -1, 0, 0, 0, 0, 0, 0, 0, 0, 1, -1, 1, -1], [1, 1, 0, 0, -1, -1, 0, 0, 0, 0, 1, -1, 0, 0, 1, -1], [1, 1, 0, 0, 0, 0, 1, -1, -1, -1, 0, 0, 0, 0, 1, -1], [1, 1, 0, 0, 1, -1, 0, 0, 0, 0, -1, -1, 0, 0, 1, -1], [1, 1, 1, -1, 0, 0, 0, 0, 0, 0, 0, 0, -1, -1, 1, -1]] \ No newline at end of file diff --git a/research/bw16-clique-exchange-barrier/NOTICE.md b/research/bw16-clique-exchange-barrier/NOTICE.md new file mode 100644 index 0000000000..dd577bde47 --- /dev/null +++ b/research/bw16-clique-exchange-barrier/NOTICE.md @@ -0,0 +1,8 @@ +CLIQUE72.json is an unchanged copy of DaysSky's +research/bw16-unit-screen/data/clique72.json from +CrocSwap/integer-mult-bounds PR #895, commit +3bf6fccaf17521ffdb9b3bec2740ba4886478556, licensed Apache-2.0. +Source: https://github.com/CrocSwap/integer-mult-bounds/pull/895 + +The new insertion theorem and verifier were produced by Nick Petalas. +Classical Barnes-Wall, Reed-Muller and Construction-D authorship is retained. diff --git a/research/bw16-clique-exchange-barrier/README.md b/research/bw16-clique-exchange-barrier/README.md new file mode 100644 index 0000000000..b74312b6df --- /dev/null +++ b/research/bw16-clique-exchange-barrier/README.md @@ -0,0 +1,198 @@ +# Exact insertion barriers around the BW16 72-line clique + +This finite certificate proves a new local obstruction for the 72-line +Barnes-Wall clique published by DaysSky in [PR #895](https://github.com/CrocSwap/integer-mult-bounds/pull/895). +Adding one new line requires deleting at least **20** old lines. Adding two +compatible new lines requires deleting at least **30** old lines. Both +insertion thresholds are attained. + +Consequently, any different clique with at least 72 lines must discard at +least 30 lines of the fixed clique. Every replacement that discards at most +29 old lines strictly decreases cardinality. A search that retains 43 or +more of these old lines cannot improve the 72-line witness. + +Claim type: **exact finite certificate and scoped combinatorial proof**. +The maximum BW16 clique and the minimum decoder-window rank remain unknown. +The predecessor's window floor stays 72; no new kappa is claimed. + +## Object and exact theorem + +Use the predecessor's scaling + +```text +L = RM(1,4) + 2 RM(3,4) + 4 Z^16. +``` + +Coordinates are indexed by the binary points 0 through 15. Let V be the +norm-eight lines of L, represented by the vector whose first nonzero +coordinate is positive. Let K be the fixed 72-element subset in +[CLIQUE72.json](CLIQUE72.json), copied byte for byte from DaysSky's source. +Two distinct lines are compatible when their integer inner product is +nonzero. A clique is a set of mutually compatible lines. + +For an outside line x, define its forced deletion set + +```text +S(x) = { k in K : = 0 }. +``` + +The exhaustive certificate establishes + +```text +min_(x in V\K) |S(x)| = 20, +min_(x,y in V\K, x != y, != 0) |S(x) union S(y)| = 30. (1) +``` + +There are 2,088 outside lines. Their deletion-set sizes have the exact +histogram `{20:378, 29:1080, 36:630}`. All 2,178,828 unordered outside pairs +are classified; 1,316,988 are compatible. Among the compatible pairs, +11,340 attain deletion size 30. The complete 18-bin pair histogram is +checked in [verify.py](verify.py) and emitted in its generated receipt. + +Writing e_j for coordinate j, zero based, explicit attainments are + +```text +x = 2(e_13 + e_15), +y = 2(e_11 + e_15). + +|S(x)| = |S(y)| = 20, + = 4, +|S(x) union S(y)| = 30. +``` + +Thus `(K\S(x)) union {x}` has 53 lines and +`(K\(S(x) union S(y))) union {x,y}` has 44 lines. +These are witnesses for the insertion thresholds, not improved cliques. + +A more precise local statement follows. Require a replacement to discard +exactly d old lines and to contain at least one outside line. No such +clique exists for d < 20. For every 20 <= d <= 29 its largest possible +cardinality is exactly `73-d`. + +## Proof and completeness of the finite component + +The shell description is inherited from DaysSky's Construction-D argument. +Here is the finite domain used by the new certificate. The low residue of +a norm-eight vector is an affine binary function on four bits. Its weight +is 0, 8 or 16, and norm eight excludes weight 16. At weight zero, division +by two leaves an even-weight residue of norm two, giving the vectors +`2(+-e_i +-e_j)`. There are 240 canonical lines. At weight eight, every +nonzero coordinate is +-1 and the negative-sign count must be even because +RM(3,4) is the even-weight code. Each of the 30 affine hyperplanes gives +64 canonical sign patterns, hence another 1,920 lines. The two cases are +disjoint and exhaustive, giving 2,160 lines. + +The verifier constructs that domain directly. A separate membership +predicate reconstructs an affine function from its values at zero and the +four coordinate points, checks all sixteen values, and checks the even +second-residue condition. The published clique is a fixed input premise; +its data hash, membership and pairwise compatibility are guarded before the +new outside-line computation. No predecessor executable or screen is run. + +For each outside line the verifier computes S(x) by all 72 literal integer +inner products. It then visits every unordered outside pair, tests its +compatibility, and counts the size of the deletion union. Exact minima, +histograms and attaining lines establish (1). The registered replay repeats +the complete pair computation with ordinary integer dot products instead +of signed-support bit masks. Neither method uses floating arithmetic. + +Now let C be any clique, D=K\C, and A=C\K. Compatibility forces +`S(x) subset D` for every x in A. If |D| < 20, (1) forces A to be empty. +If |D| <= 29, (1) forces |A| <= 1, since two lines in A would be compatible +and would require at least 30 deletions. Therefore, for 20 <= d <= 29, +`|C| <= 72-d+1`. This is attained by taking the 53-line one-insertion +witness and deleting any further d-20 old lines. For d < 20 the largest +clique after exactly d deletions is simply a subset of K, of size 72-d. +These statements prove the local obstruction without enumerating larger +cliques. They do not prove that 30 deletions suffice for another 72-line +clique or for an improvement. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bw16-clique-exchange-barrier +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/bw16-clique-exchange-barrier/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/bw16-clique-exchange-barrier/verify.py --literal +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bw16-clique-exchange-barrier --check-source-history +``` + +The registered commands execute both pair representations, each in normal +and optimized Python. Expected marker: +`PASS_BW16_CLIQUE_EXCHANGE_BARRIER one=20 two=30 outside=2088 compatible_pairs=1316988`. +Each run writes a receipt to stdout with the enumerated histograms, +attainments and SHA256 hashes of every package file. No receipt is +handwritten and no output file is generated in the checkout. + +The four boundary checks reject a nonaffine low residue and odd sign parity, +and distinguish a nonzero self contact and the invalid admission of an old +line as new. There are also 4,176 signed/scale encoding comparisons. All +checks use explicit exceptions and remain active under optimized Python. + +## Scope, evidence and stopping decision + +The initial claim sought a larger clique. Two short bounded serial +heuristics found none; this is only a search failure. The delivered result +is instead the exact local obstruction (1), which explains why small +replacement searches around this particular witness cannot succeed. +The first established new result ended the construction search. + +The theorem is specific to the exact K bytes below. It covers arbitrary +simultaneous insertions under its deletion bound, but no other 72-line +clique is asserted to have the same neighborhood. It neither determines +maximum clique nor closes the decoder-window interval. Thirty is a sharp +two-line insertion threshold, not a proved sharp radius for an improving +exchange. The inherited admissible-pairing rule turns a clique into a +window floor, but this package adds no larger clique and therefore raises +no window floor. Physical decoding, helper and restoration prices, +compiler/outer admission and the multiplication theorem remain unproved. +Independent human and formal proof-kernel review are unclaimed. + +Scientific base is `81e9bd69e4a5b00ba9c713a1620e36d576d5522e`, priority +revision 7. The selected record and family guidance were read. The original +card's historical ceiling control was attempted and raises +`KeyError: 'complex_profile'` on the changed selected certificate schema. +It is not evidence for this theorem and is left unchanged. No selected +cold replay, Lean, Docker or historical suite is needed by this isolated +finite result. + +Power-of-ten scope is the new verifier only. It has no recursion, dynamic +code loading, solver or imported predecessor implementation. All loops +are bounded by 16 coordinates, 72 old lines, 2,160 shell lines or +2,178,828 outside pairs. Functions stay below 60 lines. Rule 3 has a +managed-runtime deviation: Python allocates integers, tuples and generator +objects during checking. Live state is bounded by the fixed shell, 2,088 +72-bit deletion masks and 18 histogram bins; pairs are streamed. There is +no retained quadratic adjacency matrix. Normal/optimized warning-strict +execution checks this fixed domain. Revisit resource bounds before adding +a configurable dimension or shell. + +## Open next questions + +1. Can a larger BW16 clique be found by a move discarding at least 30 lines + of K, or by a different initial construction? This is the smallest search + direction not excluded here. Start with one explicitly retained subset + of at most 42 old lines; global optimality and the required replacement + size beyond this necessary bound remain unknown. +2. Can a structural proof replace the finite deletion-set certificate, or + establish its analogue for another inequivalent 72-line clique? Start + by classifying the 378 minimum-deletion outside lines under K's actual + stabilizer. No orbit or equivalence classification is supplied here. + +## Provenance and credit + +This contribution was produced by Nick Petalas. DaysSky supplies the +BW16 shell/screen setting and the published 72-line clique in PR #895, +head `3bf6fccaf17521ffdb9b3bec2740ba4886478556`. The copied source is +`research/bw16-unit-screen/data/clique72.json`, SHA256 +`c16f23f68fd3e840216032df458dbd8f281822fbe1e829aeb06710e4372d0d99`. +Its bytes are retained unchanged in CLIQUE72.json; see [NOTICE.md](NOTICE.md). + +DreamingOfClouds retains credit for the admissible-pairing framework, +#446/#595 and the #2244 line-system discussion. Joel Pulikkan retains +#620's screen credit; #598/#606 and the classical Barnes-Wall, +Reed-Muller and Construction-D lineage retain their contributions. +The new contribution is the outside-line insertion certificate and local +replacement theorem. No predecessor scientific acceptance is claimed. +New material is Apache-2.0. diff --git a/research/bw16-clique-exchange-barrier/SOURCES.json b/research/bw16-clique-exchange-barrier/SOURCES.json new file mode 100644 index 0000000000..71e9e34502 --- /dev/null +++ b/research/bw16-clique-exchange-barrier/SOURCES.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ], + "external_provenance": [ + { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 895, + "commit": "3bf6fccaf17521ffdb9b3bec2740ba4886478556", + "path": "research/bw16-unit-screen/data/clique72.json", + "local_copy": "CLIQUE72.json", + "sha256": "c16f23f68fd3e840216032df458dbd8f281822fbe1e829aeb06710e4372d0d99", + "usage": "Fixed clique input, exported byte for byte because this pending head is not a local Git object." + } + ] +} diff --git a/research/bw16-clique-exchange-barrier/TASK.json b/research/bw16-clique-exchange-barrier/TASK.json new file mode 100644 index 0000000000..3c092bab27 --- /dev/null +++ b/research/bw16-clique-exchange-barrier/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact one-line and two-compatible-line insertion thresholds around the published BW16 72-line clique, with a 29-deletion local obstruction.", + "scope_change_reason": "A bounded larger-clique search found no improvement. The first new verified result is the sharp local insertion obstruction, rather than a new helper inventory or paid supplier.", + "bottleneck_link": "Side result: excludes small replacement moves in the BW16 clique-based decoder-window method; it does not improve the selected moment or the existing 72 window floor.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original finite obstruction. Do not extend the clique search after the 20/30 insertion thresholds are established.", + "outcome": "negative-result", + "evidence": "All 2088 outside lines and 2178828 unordered outside pairs are classified; 1316988 pairs are compatible. Single threshold 20 and compatible-pair threshold 30 are attained. Both direct-dot and signed-mask replay are registered.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a larger BW16 clique be found after discarding at least 30 fixed-clique lines?", + "why_it_matters": "Smaller replacements cannot improve the known witness.", + "first_step": "Fix at most 42 old lines and test one larger replacement, or change the starting construction.", + "blocked_by": "Global maximum clique and sufficient exchange size are unknown." + }, + { + "question": "Can a structural stabilizer proof explain the insertion spectrum or extend it to another clique?", + "why_it_matters": "It could replace finite enumeration and identify an invariant obstruction.", + "first_step": "Classify the 378 outside lines with deletion size 20 under the actual stabilizer.", + "blocked_by": "No orbit or clique-equivalence classification is supplied." + } + ] +} diff --git a/research/bw16-clique-exchange-barrier/VERIFY.json b/research/bw16-clique-exchange-barrier/VERIFY.json new file mode 100644 index 0000000000..d4cc40889f --- /dev/null +++ b/research/bw16-clique-exchange-barrier/VERIFY.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaust every outside line/pair; direct-dot or signed-mask thresholds, full histograms, exact attainments and boundary controls, including optimized execution." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaust every outside line/pair; direct-dot or signed-mask thresholds, full histograms, exact attainments and boundary controls, including optimized execution." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--literal" + ], + "timeout_seconds": 120, + "checks": "Exhaust every outside line/pair; direct-dot or signed-mask thresholds, full histograms, exact attainments and boundary controls, including optimized execution." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py", + "--literal" + ], + "timeout_seconds": 120, + "checks": "Exhaust every outside line/pair; direct-dot or signed-mask thresholds, full histograms, exact attainments and boundary controls, including optimized execution." + } + ] +} diff --git a/research/bw16-clique-exchange-barrier/verify.py b/research/bw16-clique-exchange-barrier/verify.py new file mode 100644 index 0000000000..1a631f1afb --- /dev/null +++ b/research/bw16-clique-exchange-barrier/verify.py @@ -0,0 +1,203 @@ +"""Exact BW16 insertion thresholds around DaysSky's fixed 72-line clique.""" + +import argparse +from collections import Counter +import hashlib +from itertools import combinations +import json +from pathlib import Path +import sys +import time + + +HERE = Path(__file__).resolve().parent +SOURCE_SHA256 = "c16f23f68fd3e840216032df458dbd8f281822fbe1e829aeb06710e4372d0d99" +EXPECTED_PAIRS = { + 30: 11340, 34: 30240, 35: 30240, 40: 127008, 42: 56700, + 43: 75600, 44: 15120, 46: 117180, 47: 120960, 48: 105840, + 49: 98280, 50: 211680, 51: 181440, 52: 7560, 53: 7560, + 54: 21420, 56: 90720, 58: 8100, +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right, strict=True)) + + +def member(vector): + """Test Construction D directly, separately from shell enumeration.""" + if len(vector) != 16 or any(type(x) is not int for x in vector): + return False + low = tuple(x % 2 for x in vector) + constant = low[0] + coefficients = tuple(low[1 << j] ^ constant for j in range(4)) + for point in range(16): + value = constant + for j in range(4): + value ^= coefficients[j] * ((point >> j) & 1) + if value != low[point]: + return False + return sum((x - c) // 2 for x, c in zip(vector, low, strict=True)) % 2 == 0 + + +def shell(): + """Canonical norm-eight lines, using the two cited shell shapes.""" + vectors = [] + for i, j in combinations(range(16), 2): + for sign in (-2, 2): + vector = [0] * 16 + vector[i], vector[j] = 2, sign + vectors.append(tuple(vector)) + for normal in range(1, 16): + for constant in range(2): + support = tuple(i for i in range(16) + if ((normal & i).bit_count() + constant) % 2) + need(len(support) == 8, "affine hyperplane size") + for signs in range(128): + if signs.bit_count() % 2: + continue + vector = [0] * 16 + vector[support[0]] = 1 + for j in range(1, 8): + vector[support[j]] = -1 if signs >> (j - 1) & 1 else 1 + vectors.append(tuple(vector)) + result = tuple(sorted(vectors)) + need(len(result) == len(set(result)) == 2160, "shell size/distinctness") + need(all(member(v) and dot(v, v) == 8 for v in result), "shell membership") + return result + + +def load_clique(): + path = HERE / "CLIQUE72.json" + need(path.stat().st_size < 30000, "source size cap") + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == SOURCE_SHA256, "source bytes") + data = json.loads(raw) + need(isinstance(data, list) and len(data) == 72, "clique shape") + need(all(isinstance(v, list) and len(v) == 16 for v in data), "vector shape") + clique = tuple(tuple(v) for v in data) + need(len(set(clique)) == 72, "distinct source lines") + need(all(member(v) and dot(v, v) == 8 for v in clique), "source membership") + need(all(dot(v, w) != 0 for v, w in combinations(clique, 2)), "source premise") + return clique + + +def signed_bits(vector): + positive = sum(1 << i for i, x in enumerate(vector) if x > 0) + negative = sum(1 << i for i, x in enumerate(vector) if x < 0) + scale = max(map(abs, vector)) + need(all(x == 0 or abs(x) == scale for x in vector), "constant nonzero scale") + return positive, negative, scale + + +def bit_dot(left, right): + lp, ln, ls = left + rp, rn, rs = right + return ls * rs * ((lp & rp).bit_count() + (ln & rn).bit_count() + - (lp & rn).bit_count() - (ln & rp).bit_count()) + + +def missing_sets(outside, clique): + result = tuple(sum(1 << j for j, old in enumerate(clique) if dot(v, old) == 0) + for v in outside) + histogram = Counter(bits.bit_count() for bits in result) + need(histogram == {20: 378, 29: 1080, 36: 630}, "single insertion histogram") + return result, histogram + + +def pair_census(outside, missing, literal): + encoded = tuple(signed_bits(v) for v in outside) + counts = Counter() + witness = None + for i in range(2088): + for j in range(i): + product = (dot(outside[i], outside[j]) if literal + else bit_dot(encoded[i], encoded[j])) + if product == 0: + continue + deleted = (missing[i] | missing[j]).bit_count() + need(deleted >= 30, "two compatible new lines delete at least thirty") + counts[deleted] += 1 + if deleted == 30 and witness is None: + witness = i, j + need(dict(counts) == EXPECTED_PAIRS, "complete compatible-pair histogram") + need(sum(counts.values()) == 1316988, "compatible pair total") + need(witness is not None, "two-insertion bound is attained") + return counts, witness + + +def attainments(outside, missing, pair, clique): + one = next(i for i in range(2088) if missing[i].bit_count() == 20) + for deleted in range(20, 30): + mask = missing[one] + extras = tuple(j for j in range(72) if not (mask >> j & 1)) + for j in extras[:deleted - 20]: + mask |= 1 << j + kept = tuple(v for j, v in enumerate(clique) if not (mask >> j & 1)) + need(len(kept) + 1 == 73 - deleted, "exact deletion-size attainment") + need(all(dot(outside[one], v) != 0 for v in kept), "one-line attainment") + i, j = pair + mask = missing[i] | missing[j] + kept = tuple(v for k, v in enumerate(clique) if not (mask >> k & 1)) + need(len(kept) == 42 and dot(outside[i], outside[j]) != 0, "two-line attainment") + need(all(dot(v, w) != 0 for v in kept for w in (outside[i], outside[j])), + "two-line retained contacts") + return {"one": outside[one], "two": (outside[i], outside[j])} + + +def controls(clique, outside): + bad = list(outside[0]) + bad[0] += 1 + need(not member(tuple(bad)), "nonaffine-residue control") + bad_sign = list(next(v for v in outside if max(map(abs, v)) == 1)) + first = next(i for i, x in enumerate(bad_sign) if x) + bad_sign[first] *= -1 + need(not member(tuple(bad_sign)), "odd sign parity control") + need(dot(clique[0], clique[0]) == 8, "nonzero self contact") + need(sum(dot(clique[0], v) == 0 for v in clique) == 0, + "old-line admission would give zero deletions") + for v in outside: + encoded = signed_bits(v) + need(bit_dot(encoded, encoded) == dot(v, v) == 8, "encoded scale") + negated = tuple(-x for x in v) + need(bit_dot(encoded, signed_bits(negated)) == -8, "signed-dot control") + return 4 + 2 * len(outside) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--literal", action="store_true", help="use direct integer dot products") + args = parser.parse_args() + started = time.monotonic() + clique = load_clique() + vectors = shell() + old = set(clique) + need(old <= set(vectors), "source clique belongs to enumerated shell") + outside = tuple(v for v in vectors if v not in old) + need(len(outside) == 2088, "outside domain") + missing, singles = missing_sets(outside, clique) + pairs, witness = pair_census(outside, missing, args.literal) + attaining = attainments(outside, missing, witness, clique) + control_count = controls(clique, outside) + paths = tuple(sorted(p for p in HERE.iterdir() if p.is_file())) + receipt = { + "claim_type": "finite certificate and scoped combinatorial proof", + "shell_lines": len(vectors), "outside_lines": len(outside), + "single_histogram": dict(singles), "pair_histogram": dict(pairs), + "compatible_pairs": sum(pairs.values()), "one_threshold": 20, + "two_threshold": 30, "attainments": attaining, "controls": control_count, + "literal": args.literal, "python": sys.version.split()[0], + "package_sha256": {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in paths}, + } + print(json.dumps(receipt, sort_keys=True)) + print("PASS_BW16_CLIQUE_EXCHANGE_BARRIER", "one=20", "two=30", + "outside=2088", "compatible_pairs=1316988", f"seconds={time.monotonic()-started:.3f}") + + +if __name__ == "__main__": + main()