From 3bf6fccaf17521ffdb9b3bec2740ba4886478556 Mon Sep 17 00:00:00 2001 From: DaysSky <88261516+DaysSky@users.noreply.github.com> Date: Tue, 13 Oct 2026 10:44:56 +0000 Subject: [PATCH] Add a BW16 unit screen: main's window screen ranks Barnes-Wall below E8 No new kappa. A frozen 72-line set of pairwise non-orthogonal BW16 lines forces the window of the format-limits C.6 decoder pattern to c >= 72, so main's unit screen (ade_screen.py: x = c*h/v, #595's certified skel.X) gives a ceiling of at most 3.8923e-3 at every s = 3..39, 0.649x E8's bit ceiling. BW16 already loses for c >= 63; the window is bracketed in [72, 191]. bw16_check.py rebuilds BW16 by Construction D (all 4320 minimal vectors, 2160 lines), checks the inner-product profile of every line, the clique, an exact E8 reference (largest non-orthogonal set 8) and the ceiling screen. --- .gitattributes | 1 + .github/workflows/bw16-unit-screen.yml | 39 ++++ research/bw16-unit-screen/LICENSE | 201 ++++++++++++++++++ research/bw16-unit-screen/NOTICE.md | 8 + research/bw16-unit-screen/README.md | 94 +++++++++ research/bw16-unit-screen/bw16_check.py | 202 +++++++++++++++++++ research/bw16-unit-screen/data/clique72.json | 1 + 7 files changed, 546 insertions(+) create mode 100644 .github/workflows/bw16-unit-screen.yml create mode 100644 research/bw16-unit-screen/LICENSE create mode 100644 research/bw16-unit-screen/NOTICE.md create mode 100644 research/bw16-unit-screen/README.md create mode 100644 research/bw16-unit-screen/bw16_check.py create mode 100644 research/bw16-unit-screen/data/clique72.json diff --git a/.gitattributes b/.gitattributes index 6b648c37d1..62f34437f1 100644 --- a/.gitattributes +++ b/.gitattributes @@ -119,3 +119,4 @@ research/tintagel-source-lookup/** -text -whitespace research/trace-curvature-preload/** -text -whitespace research/witness-spec-tools/** -text -whitespace research/community-family588-audit/** -text -whitespace +research/bw16-unit-screen/** -text -whitespace diff --git a/.github/workflows/bw16-unit-screen.yml b/.github/workflows/bw16-unit-screen.yml new file mode 100644 index 0000000000..3055bc3379 --- /dev/null +++ b/.github/workflows/bw16-unit-screen.yml @@ -0,0 +1,39 @@ +name: Check the BW16 unit screen + +on: + push: + paths: + - 'research/bw16-unit-screen/**' + - 'research/format-limits/scripts/skel.py' + - 'research/format-limits/scripts/cert.py' + - '.github/workflows/bw16-unit-screen.yml' + pull_request: + paths: + - 'research/bw16-unit-screen/**' + - 'research/format-limits/scripts/skel.py' + - 'research/format-limits/scripts/cert.py' + - '.github/workflows/bw16-unit-screen.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + check: + runs-on: ubuntu-24.04 + timeout-minutes: 20 + strategy: + fail-fast: false + matrix: + python-version: ['3.11', '3.14'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: ${{ matrix.python-version }} + - name: Rebuild BW16, check the clique, the window bracket and the ceiling screen + run: python3 -B research/bw16-unit-screen/bw16_check.py + - name: Require committed files to remain unchanged + run: git diff --exit-code diff --git a/research/bw16-unit-screen/LICENSE b/research/bw16-unit-screen/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/bw16-unit-screen/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/bw16-unit-screen/NOTICE.md b/research/bw16-unit-screen/NOTICE.md new file mode 100644 index 0000000000..a11483131a --- /dev/null +++ b/research/bw16-unit-screen/NOTICE.md @@ -0,0 +1,8 @@ +# Notice + +This note, `bw16_check.py` and `data/clique72.json` were prepared by DaysSky, with assistance from Claude. They are +released under the Apache-2.0 license in `LICENSE`. + +The checker imports, without modifying, `research/format-limits/scripts/skel.py` and `cert.py` (#595). Those files +keep their own authors, notices and licenses; see the repository's `NOTICE`, `CONTRIBUTORS.md` and the +`format-limits` package. diff --git a/research/bw16-unit-screen/README.md b/research/bw16-unit-screen/README.md new file mode 100644 index 0000000000..0205ba8e01 --- /dev/null +++ b/research/bw16-unit-screen/README.md @@ -0,0 +1,94 @@ +# BW16 as a unit: main's window screen ranks it below E8 + +**No new κ is claimed.** This note screens the Barnes–Wall lattice BW16 (2160 minimal-vector lines in rank 16) as +a unit with the screen that main already applies to the ADE root systems, K12, Leech and the Niemeier lattices +(`research/e8-decoder-floors-and-cold14-notes/ade_screen.py`, #598, #606). BW16 has not been screened before. + +The screen's result: + +- 72 pairwise non-orthogonal lines force the window to c ≥ 72 (E8: c = 9). +- So the copy proxy is x ≥ 8/15. +- The certified ceiling is then at most 3.8923·10⁻³ at every stage count s = 3…39, which is 0.649× E8's bit + ceiling (6.0005·10⁻³). +- BW16 already loses at c ≥ 63, so the conclusion does not depend on finding the largest clique. + +```sh +python3 -B research/bw16-unit-screen/bw16_check.py +``` + +It uses the standard library only, runs in about 3 minutes and ends with `PASS_BW16_UNIT_SCREEN (21 checks)`. + +## Setting + +The checks use the conventions of main's unit screen (`ade_screen.py`, #620): + +- v lines, lattice rank h, window c, copy proxy x = c·h/v; +- #595's certified ceiling `X(s, h, 1, x)`, imported unchanged from `research/format-limits/scripts/skel.py`. + +The decoder pattern is that of `research/format-limits/README.md` §C.6 (#446 Theorem A): over F₂, +B_TS = 0 where G_TS ≠ 0 and B_TT = 1, with window = rank B. On a set K of pairwise non-orthogonal lines the pattern +forces B[K, K] = I, so c ≥ |K|. + +## What is checked + +| Step | Check | Result | +|---|---|---| +| Lattice | BW16 = RM(1,4) + 2·RM(3,4) + 4ℤ¹⁶ (Construction D) | codes rebuilt from their generators | +| Minimal vectors | the norm-8 vectors are exactly the shapes (±2²) and (±1⁸); both are enumerated in full | 480 + 3840 = 4320, no shorter vector | +| Lines | | 2160 | +| Inner products | \|⟨x, y⟩\| profile of every line | {0: 855, 2: 1024, 4: 280}, the same for all lines | +| E8 reference | 120 lines, exhaustive branch and bound | 63 orthogonal neighbours per line; largest non-orthogonal set 8 | +| Clique | `data/clique72.json`, 64 lines of shape (1⁸) and 8 of shape (2²), pairwise non-orthogonal | \|⟨x, y⟩\| ∈ {2, 4}; a deterministic greedy reproduces it exactly | +| Window | c ≥ 72 from the clique; the pattern's natural decoder B₀ = I + [orthogonal pairs] is checked against the pattern | 72 ≤ c_min ≤ rank_F₂ B₀ = 191 | +| Ceiling | X(s, 16, 1, 8/15) for s = 3, 5, …, 39 | max 3.8923·10⁻³ at s = 3 | +| Reference | E8 bit, X(5, 8, 1, 63/111) (#595 A.3); full E8, X(5, 8, 1, 3/5) | 6.0005·10⁻³; 5.1598·10⁻³ | +| Break-even | the smallest c at which BW16 is below E8's bit ceiling at every s (X is non-increasing in x, #595 A.2) | c = 63 (c = 62 still wins at some s) | + +## Why BW16 loses + +The loss is entirely the copy charge. + +- With free copies (x = 0), BW16's ceiling X(3, 16, 1, 0) = 1.9614·10⁻² would be more than 3× E8's. +- But BW16's lines are too densely non-orthogonal. Each line is orthogonal to only 855 of the other 2159, so large + pairwise non-orthogonal sets exist. The decoder pattern then pays one window unit per clique line. +- E8 escapes this. Its largest non-orthogonal set is exactly 8 lines among 120, also checked. +- At the natural decoder B₀ the window is 191. That gives x = 191·16/2160 > 1, the regime that main's ADE note + records as giving no saving. + +## Scope + +- **This is a ranking screen, not a κ bound.** + - The selected record, κ = 1.661634653669567·10⁻³ (#799), sits below BW16's screen ceiling, as it does below E8's. + - The record realises 0.277 of E8's bit ceiling. Nothing here bounds what fraction BW16 could realise. + - The statement is the same kind as main's ADE, Leech and Niemeier screens: BW16's ceiling is 35% below E8's. +- **Helper cost.** X* alone does not rank unit families (#620 §4). Helper cost grows with the number of orthogonal + neighbours per line: 63 for E8, 855 for BW16. That points the same way as the screen but is not priced here. +- **Decoder pattern.** Only decoders on the §C.6 pattern are covered. Off-pattern decoders, for example lossy + corrections with B_TS ≠ 0 on non-orthogonal pairs, are outside this note, as they are outside #620's. +- **Window.** c_min is not determined. Only the bracket [72, 191] is proved. The conclusion needs only c ≥ 63. +- **Clique.** 72 is not claimed to be the largest clique. +- **Parameters.** k = 1, as in `ade_screen.py`. + +## Related work + +- Main's screens: `ade_screen.py` and §4 of `research/e8-decoder-floors-and-cold14-notes/README.md` (#620: ADE, + extension rings, K12), #598 (Leech, Turyn), #606 (Niemeier). +- The Gaussian E8 clique ceilings: #738, #770, #868. +- None of these screens BW16. That was checked against the titles and bodies of all hub PRs through #883 and + against main at `f567884a`. + +## Files + +- `bw16_check.py`: the checks. +- `data/clique72.json`: the 72-line clique, also rebuilt by the checker. +- `NOTICE.md`, `LICENSE` (Apache-2.0). +- `.github/workflows/bw16-unit-screen.yml`: CI. + +## Credits + +- DreamingOfClouds, for #595's certified ceiling `skel.X` and the decoder-pattern results of `format-limits`. +- Joel Pulikkan (GamingPuzzled), for #620's unit screen. +- The authors of #446 (Theorem A), #598 and #606. +- BW16 and Construction D are classical: Barnes and Wall (1959); Conway and Sloane, *Sphere Packings, Lattices and + Groups*, ch. 4 and 8. +- Prepared by DaysSky, with assistance from Claude. diff --git a/research/bw16-unit-screen/bw16_check.py b/research/bw16-unit-screen/bw16_check.py new file mode 100644 index 0000000000..cab68cb103 --- /dev/null +++ b/research/bw16-unit-screen/bw16_check.py @@ -0,0 +1,202 @@ +"""Barnes-Wall BW16 as a unit for the E8-style decoder screen: the checks behind README.md (no kappa claim). + +Run from the repository root: python3 -B research/bw16-unit-screen/bw16_check.py +Standard library only. The ceiling X(s, h, k, x) is #595's certified function, imported unchanged from +research/format-limits/scripts/skel.py, exactly as research/e8-decoder-floors-and-cold14-notes/ade_screen.py uses it.""" +import collections +import itertools +import json +import operator +import os +import sys +from fractions import Fraction as Fr + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(os.path.dirname(HERE)) +sys.path.insert(0, os.path.join(ROOT, 'research', 'format-limits', 'scripts')) +from skel import X # noqa: E402 + +N_CHECKS = 0 + + +def check(name, ok, detail=''): + global N_CHECKS + N_CHECKS += 1 + print('%-4s %-46s %s' % ('ok' if ok else 'FAIL', name, detail), flush=True) + if not ok: + sys.exit(1) + + +# 1. BW16 = RM(1,4) + 2 RM(3,4) + 4 Z^16 (Construction D); minimal norm 8 in this scaling. +def rm(r, m=4): + pts = list(itertools.product((0, 1), repeat=m)) + rows = [tuple(int(all(p[i] for i in S)) for p in pts) + for k in range(r + 1) for S in itertools.combinations(range(m), k)] + code = {(0,) * 16} + for row in rows: + code |= {tuple((a + b) % 2 for a, b in zip(c, row)) for c in code} + return code + + +RM1, RM3 = rm(1), rm(3) +check('RM(1,4) and RM(3,4)', len(RM1) == 32 and len(RM3) == 2 ** 15 and RM1 <= RM3, '32 and 32768 words, nested') +check('RM(1,4) weights', sorted({sum(c) for c in RM1}) == [0, 8, 16], '0, 8, 16') +check('RM(3,4) = even-weight code', all(sum(c) % 2 == 0 for c in RM3), '') + + +def member(x): + c1 = tuple(v % 2 for v in x) + if c1 not in RM1: + return False + return tuple(((v - a) // 2) % 2 for v, a in zip(x, c1)) in RM3 + + +# A vector of norm <= 8 has at most 8 odd coordinates, and they form a word of RM(1,4): 0 or 8 of them. +# 8 odd: the odd entries are +-1 (norm already 8) and the rest 0, so shape (+-1^8) on a weight-8 word. +# 0 odd: x = 2y with |y|^2 <= 2 and y mod 2 an even-weight word, so y = +-e_i +- e_j: shape (+-2^2). +# So the minimal vectors are exactly these two families; both are enumerated in full. +vecs = [] +for i, j in itertools.combinations(range(16), 2): + for a, b in itertools.product((2, -2), repeat=2): + v = [0] * 16 + v[i] = a + v[j] = b + vecs.append(tuple(v)) +check('shape (2^2): all in the lattice', all(member(v) for v in vecs), '%d vectors' % len(vecs)) +n_odd_tried = 0 +for c in sorted(RM1): + if sum(c) != 8: + continue + idx = [i for i in range(16) if c[i]] + for sg in itertools.product((1, -1), repeat=8): + v = [0] * 16 + for i, s in zip(idx, sg): + v[i] = s + n_odd_tried += 1 + if member(tuple(v)): + vecs.append(tuple(v)) +check('shape (1^8): half of each sign class', n_odd_tried == 30 * 256 and len(vecs) == 480 + 30 * 128, + '%d of %d sign patterns lie in the lattice' % (len(vecs) - 480, n_odd_tried)) +check('minimal vectors = kissing number of BW16', len(vecs) == 4320, '4320') +# The only norm < 8 candidates are x = 2y with |y|^2 = 1 (the 8-odd family already has norm 8). +check('no nonzero vector of norm < 8', not any(member(tuple(2 * sg * int(k == i) for k in range(16))) + for i in range(16) for sg in (1, -1)), 'x = +-2 e_i excluded') + +lines = sorted({v if next(a for a in v if a) > 0 else tuple(-a for a in v) for v in vecs}) +v_lines = len(lines) +check('lines', v_lines == 2160, '2160') + + +def ip(u, w): + return sum(map(operator.mul, u, w)) + + +# 2. inner-product classes, for every line; nonorth[i] is the bitmask of lines not orthogonal to line i +nonorth = [] +profile_ok = True +for k, L in enumerate(lines): + cnt = collections.Counter() + m = 0 + for j, M in enumerate(lines): + if j == k: + continue + g = abs(ip(L, M)) + cnt[g] += 1 + if g: + m |= 1 << j + nonorth.append(m) + profile_ok &= dict(cnt) == {0: 855, 2: 1024, 4: 280} +check('|| profile of every line', profile_ok, '{0: 855, 2: 1024, 4: 280}: two nonzero classes, degree 1304') + +# 3. a 72-line set K of pairwise non-orthogonal lines (frozen in data/, reproduced by a deterministic greedy) +index = {L: k for k, L in enumerate(lines)} +K = [tuple(L) for L in json.load(open(os.path.join(HERE, 'data', 'clique72.json')))] +check('frozen clique lines are BW16 lines', all(L in index for L in K) and len(set(K)) == 72, '72 distinct lines') +check('frozen clique is pairwise non-orthogonal', all(ip(a, b) != 0 for a, b in itertools.combinations(K, 2)), + str(dict(sorted(collections.Counter(abs(ip(a, b)) for a, b in itertools.combinations(K, 2)).items())))) +shapes = collections.Counter('(1^8)' if 1 in map(abs, L) else '(2^2)' for L in K) +G, cand = [], (1 << v_lines) - 1 +while cand: + i = max((i for i in range(v_lines) if cand >> i & 1), key=lambda i: ((nonorth[i] & cand).bit_count(), -i)) + G.append(i) + cand &= nonorth[i] +check('deterministic greedy reproduces the clique', sorted(lines[i] for i in G) == sorted(K), + 'max degree in the candidate set, ties to the smallest index; shapes %s' % dict(shapes)) + +# E8 reference (doubled coordinates): 120 lines, 63 orthogonal neighbours each, largest non-orthogonal set exactly 8 +E8 = [tuple(2 * (k == i) + 2 * s * (k == j) for k in range(8)) + for i, j in itertools.combinations(range(8), 2) for s in (1, -1)] +E8 += [sg for sg in itertools.product((1, -1), repeat=8) if sg[0] == 1 and sg.count(-1) % 2 == 0] +e8_nb = [sum(1 << j for j in range(120) if j != i and ip(E8[i], E8[j])) for i in range(120)] +e8_best = [0] + + +def grow(P, size): # exhaustive branch and bound + if size + P.bit_count() <= e8_best[0]: + return + if not P: + e8_best[0] = size + while P and size + P.bit_count() > e8_best[0]: + u = P.bit_length() - 1 + P &= ~(1 << u) + grow(P & e8_nb[u], size + 1) + + +grow((1 << 120) - 1, 0) +check('E8 reference', len(E8) == 120 and all(119 - m.bit_count() == 63 for m in e8_nb) and e8_best[0] == 8, + '63 orthogonal neighbours per line; largest non-orthogonal set 8 (exact)') + +# 4. window bounds at the decoder pattern of format-limits C.6 (B_TS = 0 where G_TS != 0, B_TT = 1, over F2). +# On K the pattern forces B[K, K] = I, so window = rank B >= |K|. The pattern's natural decoder B0 = I + [orthogonal] +# (the analogue of E8's B0 = (J + G) mod 2) satisfies it, so its F2 rank bounds the least window from above. +def f2_rank(rows): + piv = {} + r = 0 + for row in rows: + while row: + h = row.bit_length() - 1 + if h in piv: + row ^= piv[h] + else: + piv[h] = row + r += 1 + break + return r + + +full = (1 << v_lines) - 1 +B0 = [(full & ~nonorth[i]) for i in range(v_lines)] # orthogonal lines and the diagonal +check('B0 obeys the pattern', all((B0[i] >> i) & 1 and not (B0[i] & nonorth[i]) for i in range(v_lines)), '') +c_lo, c_hi = len(K), f2_rank(B0) +check('window bracket', c_lo <= c_hi, '%d <= c_min <= rank_F2(B0) = %d (E8: c = 9)' % (c_lo, c_hi)) + +# 5. main's ADE screen: h = lattice rank, k = 1, x = c*h/v (ade_screen.py), here at the certified c >= 72 +h_bw = 16 +x_bw = Fr(c_lo * h_bw, v_lines) +check('copy proxy x = c*h/v at c = 72', x_bw == Fr(8, 15), '8/15') +S = range(3, 40, 2) +e8_bit = X(5, 8, 1, Fr(63, 111)) # #595 A.3: X* = 6.0005e-3, bit P111 +e8_full = X(5, 8, 1, Fr(3, 5)) # full 120-line E8, c = 9: x = 3/5 +check('E8 bit ceiling reproduced', abs(float(e8_bit['lo']) - 6.0005e-3) < 1e-7, '%.6e at s = 5' % e8_bit['lo']) +bw = {s: X(s, h_bw, 1, x_bw) for s in S} +best_s = max((s for s in S if bw[s]), key=lambda s: bw[s]['hi']) +check('BW16 ceiling below E8 bit at every s in 3..39', all((r is None) or r['hi'] < e8_bit['lo'] for r in bw.values()), + 'max %.4e at s = %d; E8 bit %.4e (ratio %.3f)' % (bw[best_s]['hi'], best_s, e8_bit['lo'], + float(bw[best_s]['hi'] / e8_bit['lo']))) +check('BW16 ceiling below full-E8 ceiling', all((r is None) or r['hi'] < e8_full['lo'] for r in bw.values()), + 'E8 x = 3/5: %.4e' % e8_full['lo']) +free = X(3, h_bw, 1, Fr(0)) +check('copy-free BW16 would beat E8 (loss is the copy charge)', free['lo'] > e8_bit['hi'], 'X(3, 16, 1, 0) = %.4e' % free['lo']) + + +# X is non-increasing in x (#595 A.2), so the break-even c is found at s = 3 (binding here) and then checked at +# every s, at c and at c - 1. +def loses(c, stages): + xc = Fr(c * h_bw, v_lines) + return all((r is None) or r['hi'] < e8_bit['lo'] for r in (X(s, h_bw, 1, xc) for s in stages)) + + +c_be = next(c for c in range(73) if loses(c, (3,))) +check('break-even window', c_be < c_lo and loses(c_be, S) and not loses(c_be - 1, S), + 'BW16 loses at every s in 3..39 iff c >= %d; certified c >= %d' % (c_be, c_lo)) +print('PASS_BW16_UNIT_SCREEN (%d checks)' % N_CHECKS) diff --git a/research/bw16-unit-screen/data/clique72.json b/research/bw16-unit-screen/data/clique72.json new file mode 100644 index 0000000000..2b604e87c5 --- /dev/null +++ b/research/bw16-unit-screen/data/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