From 812837d0b6a97e471535b8acb2c5b0888280e1d9 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:49:43 +0000 Subject: [PATCH] Record that the reflected P112 bit-lane iterator matches the transported supports. low_weight_words at batch size 16 on the #7017 36-generator basis returns the seven transported weight-16 words. The selected kappa is unchanged. Co-authored-by: unpaidmoon --- research/p112-reflected-frame-lane/README.md | 206 +++++++ .../p112-reflected-frame-lane/SOURCES.json | 36 ++ research/p112-reflected-frame-lane/TASK.json | 67 +++ .../p112-reflected-frame-lane/VERIFY.json | 23 + research/p112-reflected-frame-lane/verify.py | 557 ++++++++++++++++++ 5 files changed, 889 insertions(+) create mode 100644 research/p112-reflected-frame-lane/README.md create mode 100644 research/p112-reflected-frame-lane/SOURCES.json create mode 100644 research/p112-reflected-frame-lane/TASK.json create mode 100644 research/p112-reflected-frame-lane/VERIFY.json create mode 100644 research/p112-reflected-frame-lane/verify.py diff --git a/research/p112-reflected-frame-lane/README.md b/research/p112-reflected-frame-lane/README.md new file mode 100644 index 0000000000..192a75d1a7 --- /dev/null +++ b/research/p112-reflected-frame-lane/README.md @@ -0,0 +1,206 @@ +# The reflected P112 bit-lane iterator returns the transported supports + +**Set comparison of one published iterator on one reflected basis. No new κ.** +The selected conditional exponent stays `781451/250000000`. On the reflected +36-generator basis recorded by open PR #7017, `low_weight_words` at its +default batch size 16 returns zero and the seven transported weight-16 +supports. The SHA256 of `json.dumps` of those seven sorted integers is +`9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb`. + +## Result + +The line list is the coordinate model in +`research/p112-rank6-frame-coverage/engine.py`. An independent E8 builder +reproduces that ordered list. The simple system is the eight roots in +`research/p112-a3-six-flat/geometry.py`. Its Gram matrix divided by 4 is the +E8 Cartan matrix, and every one of the 240 roots is an integer combination of +these simple roots with coefficients all nonnegative or all nonpositive. + +In simple-root order, then punctured-line order, the first pair that moves a +line is simple root 0, + +```text +α = (1, -1, -1, -1, -1, -1, -1, 1) +``` + +acting on punctured line 1, + +```text +β = (2, -2, 0, 0, 0, 0, 0, 0). +``` + +The image is `(1, -1, 1, 1, 1, 1, 1, -1)`, line 88 of the pinned list. The +reflection fixes four punctured lines and moves four. The rebuilt 112-line +complement, in increasing position, has SHA256 +`a2ac7049d9eef1cff8af1eec35b084e6d261efad5311625e5356cceafe260da7`. + +Transport of the seven supports recorded for the unreflected frame is a +bijection of the 112 bit positions. The transported integers are + +```text +12726038110963558112484457976320 +61084916320812443394843581087904 +2433889152476423258413102440464394 +6363012028601310481939177671680 +954453281446482856702353473856 +580303949270928947429810196 +2677278706012631304342476888735745 +``` + +They are seven disjoint weight-16 words, they cover every rebuilt line, and +their sorted-list SHA256 is the hash above. Each meets every orthogonal +8-frame of the rebuilt list evenly. Each of the seven untransported integers +fails a frame parity. + +On that list there are 1260 orthogonal 8-frames, and every line lies in 90 +of them. The incidence matrix has rank 76. The kernel basis with an identity +on the free coordinates + +```text +(0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 15, 17, 19, 21, + 25, 26, 27, 28, 30, 34, 36, 38, 42, 43, 52, 53, 54, 55, 56, 60, 68, 84) +``` + +has the weights recorded by PR #7017. The SHA256 of `json.dumps` of these 36 +generator integers is +`f71157e487ad45377cb6a92651d3a8d8b1055b6978f14a44dea511049ca7da8c`. +A local comparison during this session, against the functions in PR #7017 at +`11af08b8ff57dc26492501b4efaffdb34d298a00`, found the same ordered basis and +the same transported integers. That comparison is not a registered input. +The replay rebuilds the basis from the three pinned files on this base and +checks the hashes above. + +`low_weight_words` is the function in +`research/e7-bitsliced-exhaustion/binary.py`. Its signature is +`(generators, width, maximum, batch_bits)` and the default of `batch_bits` +is 16. The call here is that function on this ordered basis, width 112, +weight bound 16, batch size 16. The yield has no duplicates. It is exactly + +```text +{0} ∪ {the seven transported supports} +``` + +Every positive yielded word has weight 16. Deleting one support makes the +sets unequal. Clearing the top bit of the first transported support produces +a weight-15 word outside the yield and outside the code, and the weight +predicate rejects a set that contains it. The seven untransported integers +are not the yielded set. The function rejects a repeated copy of the first +generator with `binary generators must be independent`. On generators +`(1, 2, 4)`, weight bound 1 returns `{0, 1, 2, 4}` and weight bound 0 +returns `{0}`. + +### Completeness of this call + +The domain is the span of these 36 independent generators, a set of `2^36` +words. Batch size `k = 16` splits each coefficient vector into a low part of +16 bits and a high part of 20 bits. The implementation walks the high part +by the Gray recurrence of length `2^20` and, at each step, stores all `2^16` +low parts as bit lanes. The coefficient-partition argument in +`research/e7-bitsliced-exhaustion/PROOF.md` says every coefficient vector +appears in exactly one batch and one lane, and the lane comparator keeps the +words of weight at most 16. Independence, which the basis identity and the +function's pivot check both give, makes those images distinct. This package +checks those hypotheses on this input and compares the yielded set with the +transported supports. It uses that published argument for the lane arithmetic +and does not reprove it. + +This is an exhaustive finite census of the weight-at-most-16 words of this +one ordered basis, through this one call at batch size 16. It is a set +comparison with the transported hash. It is not a second half-split, not a +census of another batch size, and not a statement about every generator +matrix. + +## Scope + +Task card `replay-runtime`, priority revision 8, base +`17469fff78c22941280f04d39dc5a1faee09c840`. Scope status is **refined**. + +The card asks for a measured speedup that keeps coverage. The revision-8 +verification row says faster output is the same coverage only after the sets +are compared. Open PR #7017 recorded the reflected half-split and asked +whether `low_weight_words` on this basis returns the transported supports. +This package is that comparison at the function's default batch size. +Width 112, weight bound 16, thirty-six generators, one call. On this +machine the direct call took 486.22 seconds and the registered package +runner took 278.75 seconds. Both finished inside the 600-second command +bound. Those figures are wall-clock observations of this environment, not +a coverage or speedup claim. The selected conditional exponent stays +unchanged. + +The priority note on this base still quotes the older displayed value +`0.00310045` from PR #5599. This package reads the selected record and +keeps `781451/250000000`. + +Ordered overlap check on 2026-11-10, after fetching upstream `main` at +`17469fff78c22941280f04d39dc5a1faee09c840`. `scripts/find_overlap.py +--refresh` read 339 open pull requests, including drafts (fetched +`2026-11-10T10:27:07Z`, pagination complete) and 7013 discussion records +(fetched `2026-11-10T10:28:11Z`, pagination complete), with 10178 local notes +and a complete local inventory at that head. The transported hash and the +reflected iterator question match open PR #7017 and discussion reply +[#1166 comment 19514152](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19514152). +Both state the question and record that the bit-lane iterator was not run. +Open PR #7007 is the unreflected half-split and the unreflected call at +batch size 20. Open PR #7034 is the intersection-counter refusal on the +unreflected 36-generator basis. No fork `cursor/*` branch had named this +reflected iterator comparison. + +## Reproduce + +Python 3.12 and the standard library, from the repository root. Assertions +must remain enabled. The registered command is one call at batch size 16. + +```sh +python3 -B scripts/research_package.py --package research/p112-reflected-frame-lane --check-only +python3 -I -B research/p112-reflected-frame-lane/verify.py +python3 -B scripts/research_package.py --package research/p112-reflected-frame-lane +``` + +The direct verifier prints + +```text +PASS_P112_REFLECTED_FRAME_LANE width=112 dimension=36 batch=16 supports=7 hash=9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb half_split_rerun=false intersection_engine=false no_new_kappa=true +``` + +`verify.py basis` rebuilds the basis and does not call the iterator. That +mode is not the registered comparison. + +Outside this run: the half-split in #7017, batch size 20 and every batch +size other than 16, a reversed generator order, the unreflected call from +#7007, `research/e7-intersection-counters/engine.py`, any other simple +root, Lean, Docker, and `scripts/research_selected_baseline.py` as a +scientific replay. The selected record is read only to require that its +kappa string is unchanged. + +## Open next questions + +1. Does `low_weight_words` at batch size 20 on this same ordered reflected + basis return the same seven transported supports? Batch size 20 is the + size used for the unreflected basis in #7007. The published iterator says + the batch size changes storage and runtime only. This package executes + the default batch size 16, so that statement is unchecked for batch 20 + on this basis. First call the same function at batch size 20 on the + generator tuple pinned by + `f71157e487ad45377cb6a92651d3a8d8b1055b6978f14a44dea511049ca7da8c` + and compare the positive words with + `9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb`. +2. Does the reversed 36-tuple, at batch size 16, return the same set? The + iterator's result is claimed independent of generator order once the + rows stay independent. This package uses the free-coordinate order only. + First reverse that pinned tuple and repeat the batch-16 call. + +## Credit + +The 120-line coordinate order is the model in +`research/p112-rank6-frame-coverage`, from the PR1226/PR1323 E8 listing +used by Cinna Davis. The simple system is the one fixed in +`research/p112-a3-six-flat/geometry.py`, from Nick Petalas's PR3161/PR3162 +lineage. `low_weight_words` and its coefficient-partition argument are Ali +Romman's `research/e7-bitsliced-exhaustion`. The seven unreflected supports +are the recorded result of open PR #7007. The reflection, the transported +integers, the free coordinates, and the basis weights are the recorded +result of open PR #7017. This package runs the iterator that #7017 left +unrun. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human review and no formal-kernel acceptance are claimed. diff --git a/research/p112-reflected-frame-lane/SOURCES.json b/research/p112-reflected-frame-lane/SOURCES.json new file mode 100644 index 0000000000..a19737fa4d --- /dev/null +++ b/research/p112-reflected-frame-lane/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/e7-bitsliced-exhaustion/binary.py", + "usage": "input", + "git_blob": "cad9fc43ec0244bce415a76bc61b6445ffbd7519", + "sha256": "e79ad4d1d4be1748cf09aacc4274a316000d4b5922f13495778892b9309dc56e" + }, + { + "path": "research/p112-a3-six-flat/geometry.py", + "usage": "input", + "git_blob": "222ea556faf2b275f73815c4e7d0d5f1e3294f2f", + "sha256": "b8ac379e41f5ad83bdb6c7f7c55129fc3d9c07801ea61591478f25d72ff0b021" + }, + { + "path": "research/p112-rank6-frame-coverage/engine.py", + "usage": "input", + "git_blob": "6afabd3777975310683e4cdc8a4e4b95f0a330ac", + "sha256": "b59101564855a89de04f39fd28b0a853aa3c46ce0ce99951d93d7dd018543536" + } + ] +} diff --git a/research/p112-reflected-frame-lane/TASK.json b/research/p112-reflected-frame-lane/TASK.json new file mode 100644 index 0000000000..87189b9db6 --- /dev/null +++ b/research/p112-reflected-frame-lane/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Does low_weight_words at its default batch size 16, on the reflected 36-generator basis of PR #7017, return the seven transported supports with hash 9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb?", + "scope_change_reason": "The replay-runtime card asks for a measured speedup. The revision-8 verification row says a published faster replay is equivalent coverage only after the sets are compared. Open PR #7017 recorded the reflected P112 half-split and asked whether low_weight_words on that 36-generator basis returns the transported supports. This package answers that set comparison at the function's default batch size. It does not time an engine or rerun the half-split.", + "bottleneck_link": "Frame-code coverage checks remain usable only when the published bit-lane iterator returns the same low-weight set as the recorded supports. This comparison binds that iterator to the reflected P112 basis. It does not change a supplier bill or the selected kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after one call of low_weight_words at batch size 16 on this ordered reflected basis, compared with the transported support hash. Do not run another batch size, reverse the basis, rerun the half-split, or call the intersection-counter engine.", + "outcome": "completed", + "evidence": "The reflected basis rebuilt from the pinned E8 line list and simple system matches the #7017 free coordinates, basis weights, line-list hash a2ac7049d9eef1cff8af1eec35b084e6d261efad5311625e5356cceafe260da7, and transported-support hash 9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb. The 36 generators have hash f71157e487ad45377cb6a92651d3a8d8b1055b6978f14a44dea511049ca7da8c. low_weight_words at batch size 16 returns exactly zero and those seven weight-16 supports, with no repeated yield. A dropped support, a weight-15 injection, the untransported integers, a repeated generator, and a toy bound change all fail. Selected kappa stays 781451/250000000.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does low_weight_words at batch size 20 on this same ordered reflected basis return the same seven transported supports?", + "why_it_matters": "Batch size 20 is the size used for the unreflected basis in #7007. The iterator says batch size changes storage and runtime only. This package executes the default batch size 16, so that claim is unchecked at batch 20 on this basis.", + "first_step": "Call low_weight_words at batch size 20 on the generator tuple with hash f71157e487ad45377cb6a92651d3a8d8b1055b6978f14a44dea511049ca7da8c and compare the positive words with hash 9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb.", + "blocked_by": "This package stops after the batch-16 call. A second scan is a separate execution." + }, + { + "question": "Does the reversed 36-tuple, at batch size 16, return the same set?", + "why_it_matters": "The iterator's result is claimed independent of generator order once the rows stay independent. This package uses the free-coordinate order only.", + "first_step": "Reverse the pinned generator tuple and repeat the batch-16 call against the same transported hash.", + "blocked_by": "This package does not reverse the basis." + } + ] +} diff --git a/research/p112-reflected-frame-lane/VERIFY.json b/research/p112-reflected-frame-lane/VERIFY.json new file mode 100644 index 0000000000..a2f7c0f8d9 --- /dev/null +++ b/research/p112-reflected-frame-lane/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e7-bitsliced-exhaustion/binary.py", + "research/p112-a3-six-flat/geometry.py", + "research/p112-rank6-frame-coverage/engine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Rebuild the reflected P112 36-generator basis, require generator hash f71157e487ad45377cb6a92651d3a8d8b1055b6978f14a44dea511049ca7da8c, and compare low_weight_words at the default batch size 16 and weight 16 with the seven transported supports of hash 9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb. Reject a dropped support, a weight-15 injection, the untransported integers, a repeated generator, and a toy bound change." + } + ] +} diff --git a/research/p112-reflected-frame-lane/verify.py b/research/p112-reflected-frame-lane/verify.py new file mode 100644 index 0000000000..99bcde48e5 --- /dev/null +++ b/research/p112-reflected-frame-lane/verify.py @@ -0,0 +1,557 @@ +#!/usr/bin/env python3 +"""Compare low_weight_words with the reflected P112 transported supports. + +Rebuild the reflected 36-generator basis from open PR #7017 and run the +published bit-lane iterator at its default batch size. The comparison is the +set of yielded words against the seven transported supports. No half-split +and no kappa change. +""" + +import inspect +import json +import sys +import time +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +from pathlib import Path +from runpy import run_path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WIDTH = 112 +FRAME_SIZE = 8 +FRAME_COUNT = 1260 +RANK = 76 +DIMENSION = 36 +DEGREE = 90 +WEIGHT_BOUND = 16 +SUPPORT_COUNT = 7 +ENGINE_BATCH = 16 +HIGH_BATCHES = 1 << (DIMENSION - ENGINE_BATCH) +LANE_COUNT = 1 << ENGINE_BATCH +SIMPLE_INDEX = 0 +PUNCTURE_INDEX = 1 +MOVED_LINES = 4 +FIXED_BITS = 1 +LINE_SHA256 = "a2ac7049d9eef1cff8af1eec35b084e6d261efad5311625e5356cceafe260da7" +RECORDED_SUPPORT_SHA256 = "ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3" +TRANSPORTED_SUPPORT_SHA256 = "9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb" +GENERATOR_SHA256 = "f71157e487ad45377cb6a92651d3a8d8b1055b6978f14a44dea511049ca7da8c" +SELECTED_KAPPA = "781451/250000000" +SELECTED_DECIMAL = "0.003125804" +NAMED_ROOT = (2, -2, 0, 0, 0, 0, 0, 0) +IMAGE_ROOT = (1, -1, 1, 1, 1, 1, 1, -1) +IMAGE_PUNCTURE = (0, 88, 95, 27, 113, 45, 54, 118) +FREE_COORDINATES = ( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 15, 17, 19, 21, 25, 26, 27, + 28, 30, 34, 36, 38, 42, 43, 52, 53, 54, 55, 56, 60, 68, 84, +) +BASIS_WEIGHTS = ( + 24, 30, 34, 38, 38, 30, 34, 26, 38, 42, 40, 32, 42, 40, 40, 40, 22, 24, 32, + 38, 24, 36, 24, 34, 36, 24, 36, 24, 34, 34, 26, 32, 30, 30, 30, 28, +) +RECORDED_SUPPORTS = ( + 64691900160, + 1034819666160, + 280375465144335, + 4772259772306660006937399132160, + 15509841550538713979819718082560, + 1216944648758260568639796318044160, + 3955070108453721685622467917250560, +) +TRANSPORTED_SUPPORTS = ( + 12726038110963558112484457976320, + 61084916320812443394843581087904, + 2433889152476423258413102440464394, + 6363012028601310481939177671680, + 954453281446482856702353473856, + 580303949270928947429810196, + 2677278706012631304342476888735745, +) +CARTAN = ( + (2, 0, -1, 0, 0, 0, 0, 0), + (0, 2, 0, -1, 0, 0, 0, 0), + (-1, 0, 2, -1, 0, 0, 0, 0), + (0, -1, -1, 2, -1, 0, 0, 0), + (0, 0, 0, -1, 2, -1, 0, 0), + (0, 0, 0, 0, -1, 2, -1, 0), + (0, 0, 0, 0, 0, -1, 2, -1), + (0, 0, 0, 0, 0, 0, -1, 2), +) +NEIGHBORS = ( + (2,), + (3,), + (0, 3), + (1, 2, 4), + (3, 5), + (4, 6), + (5, 7), + (6,), +) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def line_key(vector): + return max(tuple(vector), tuple(-value for value in vector)) + + +def support_hash(words): + return sha256(json.dumps(sorted(words)).encode()).hexdigest() + + +def reflect(vector, simple): + pairing = dot(vector, simple) + need(pairing % 4 == 0, "reflection coefficient is not integral") + return tuple(value - (pairing // 4) * coefficient + for value, coefficient in zip(vector, simple)) + + +def authenticate(): + sources = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + checked = 0 + for row in sources["files"]: + if row["usage"] != "input": + continue + path = ROOT / row["path"] + digest = sha256(path.read_bytes()).hexdigest() + need(digest == row["sha256"], "input hash mismatch: " + row["path"]) + checked += 1 + need(checked == 3, "three live inputs") + need(support_hash(RECORDED_SUPPORTS) == RECORDED_SUPPORT_SHA256, + "recorded support hash") + need(support_hash(TRANSPORTED_SUPPORTS) == TRANSPORTED_SUPPORT_SHA256, + "pinned transported hash") + need(len(FREE_COORDINATES) == len(set(FREE_COORDINATES)) == DIMENSION, + "free-coordinate count") + need(len(BASIS_WEIGHTS) == DIMENSION, "basis-weight count") + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == SELECTED_KAPPA, "selected kappa changed") + need(selected["decimal"] == SELECTED_DECIMAL, "selected decimal changed") + return checked + + +def independent_lines(): + roots = [] + for i, j in combinations(range(8), 2): + for signs in product((2, -2), repeat=2): + root = [0] * 8 + root[i], root[j] = signs + roots.append(tuple(root)) + for signs in product((1, -1), repeat=8): + if signs.count(-1) % 2 == 0: + roots.append(signs) + need(len(roots) == len(set(roots)) == 240, "E8 root count") + lines = [] + seen = set() + for root in roots: + key = line_key(root) + if key not in seen: + seen.add(key) + lines.append(root) + need(len(lines) == 120, "E8 line count") + puncture = [] + for pair in range(4): + for sign in (1, -1): + root = [0] * 8 + root[2 * pair] = 2 + root[2 * pair + 1] = 2 * sign + puncture.append(lines.index(tuple(root))) + return tuple(lines), tuple(puncture), tuple(roots) + + +def pinned_model(): + model = run_path( + str(ROOT / "research/p112-rank6-frame-coverage/engine.py"), + run_name="p112_reflected_lane_model", + )["model"]() + lines = tuple(tuple(row) for row in model["lines"]) + puncture = tuple(model["punctured_frame"]) + live = tuple(model["live"]) + own_lines, own_puncture, signed = independent_lines() + need(lines == own_lines, "pinned lines differ from the E8 builder") + need(puncture == own_puncture, "pinned puncture differs") + need(live == tuple(i for i in range(120) if i not in set(puncture)), + "live order") + need(len(live) == WIDTH, "unreflected width") + need(all(dot(row, row) == 8 for row in lines), "line norms") + need(all(dot(lines[i], lines[j]) == 0 for i, j in combinations(puncture, 2)), + "unreflected frame is not orthogonal") + return lines, puncture, signed + + +def integer_combination(root, simples): + rows = [] + for coordinate in range(8): + rows.append([Fraction(simple[coordinate]) for simple in simples] + + [Fraction(root[coordinate])]) + for column in range(8): + pivot = next((row for row in range(column, 8) if rows[row][column]), None) + need(pivot is not None, "singular simple system") + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = rows[column][column] + rows[column] = [value / scale for value in rows[column]] + for other in range(8): + if other == column or not rows[other][column]: + continue + factor = rows[other][column] + rows[other] = [left - factor * right + for left, right in zip(rows[other], rows[column])] + coefficients = [] + for row in rows: + value = row[-1] + need(value.denominator == 1, "nonintegral simple coordinates") + coefficients.append(int(value)) + built = [0] * 8 + for coefficient, simple in zip(coefficients, simples): + for coordinate in range(8): + built[coordinate] += coefficient * simple[coordinate] + need(tuple(built) == tuple(root), "simple coordinates do not rebuild the root") + return tuple(coefficients) + + +def load_simple_system(): + geometry = run_path( + str(ROOT / "research/p112-a3-six-flat/geometry.py"), + run_name="p112_reflected_lane_geometry", + ) + simple = tuple(tuple(row) for row in geometry["SIMPLE"]) + need(simple[0] == (1, -1, -1, -1, -1, -1, -1, 1), "first simple root") + need(all(len(row) == 8 for row in simple) and len(simple) == 8, "simple shape") + return simple + + +def check_simple_system(lines, signed, simple): + cartan = tuple(tuple(dot(left, right) // 4 for right in simple) for left in simple) + need(cartan == CARTAN, "Cartan matrix") + neighbors = tuple(tuple(j for j in range(8) if j != i and cartan[i][j] == -1) + for i in range(8)) + need(neighbors == NEIGHBORS, "E8 diagram") + need(all(dot(root, root) == 8 for root in simple), "simple norms") + index_of = {line_key(row): index for index, row in enumerate(lines)} + for root in simple: + images = {index_of[line_key(reflect(row, root))] for row in lines} + need(images == set(range(120)), "a simple reflection misses a line") + for row in lines: + image = reflect(row, root) + need(reflect(image, root) == tuple(row), + "a simple reflection is not an involution on the stored vector") + for root in simple: + coefficients = integer_combination(root, simple) + place = next(index for index, value in enumerate(coefficients) if value) + need(coefficients == tuple(int(index == place) for index in range(8)), + "simple roots are not the coordinate basis") + for root in signed: + coefficients = integer_combination(root, simple) + need(all(value >= 0 for value in coefficients) + or all(value <= 0 for value in coefficients), + "a root is neither positive nor negative on this system") + return index_of + + +def select_reflection(lines, puncture, index_of, simple_system): + found = None + for simple_index, simple in enumerate(simple_system): + for puncture_index, line in enumerate(puncture): + image = index_of[line_key(reflect(lines[line], simple))] + if image != line: + found = (simple_index, puncture_index, line, image, simple) + break + if found: + break + need(found is not None, "every simple root fixes every punctured line") + simple_index, puncture_index, line, image, simple = found + need((simple_index, puncture_index, line, image) + == (SIMPLE_INDEX, PUNCTURE_INDEX, 1, 88), + "first moving pair changed") + need(lines[line] == NAMED_ROOT and reflect(NAMED_ROOT, simple) == IMAGE_ROOT, + "named reflection arithmetic") + need(lines[image] == IMAGE_ROOT, "image line representative") + images = tuple(index_of[line_key(reflect(lines[old], simple))] + for old in puncture) + need(images == IMAGE_PUNCTURE, "image frame") + need(len(set(images)) == FRAME_SIZE, "image frame collapsed") + need(all(dot(lines[i], lines[j]) == 0 for i, j in combinations(images, 2)), + "image frame is not orthogonal") + moved = sum(old != new for old, new in zip(puncture, images)) + need(moved == MOVED_LINES, "moved punctured-line count") + need(set(images) != set(puncture), "reflection fixed the frame") + return simple, images + + +def rebuilt_list(lines, puncture, images, index_of, simple): + new_live = tuple(index for index in range(120) if index not in set(images)) + need(len(new_live) == WIDTH, "rebuilt width") + digest = sha256(json.dumps([list(lines[index]) for index in new_live]).encode()).hexdigest() + need(digest == LINE_SHA256, "rebuilt root-list hash") + old_live = tuple(index for index in range(120) if index not in set(puncture)) + position = {line: bit for bit, line in enumerate(new_live)} + permutation = [] + for line in old_live: + image = index_of[line_key(reflect(lines[line], simple))] + need(image in position, "a live line reflected into the new puncture") + permutation.append(position[image]) + need(sorted(permutation) == list(range(WIDTH)), "transport misses a new line") + fixed = sum(bit == image for bit, image in enumerate(permutation)) + need(fixed == FIXED_BITS, "transport moved a different number of positions") + return new_live, tuple(permutation) + + +def transport_mask(mask, permutation): + image = 0 + while mask: + bit = (mask & -mask).bit_length() - 1 + image |= 1 << permutation[bit] + mask &= mask - 1 + return image + + +def transported_supports(permutation): + images = tuple(transport_mask(mask, permutation) for mask in RECORDED_SUPPORTS) + need(images == TRANSPORTED_SUPPORTS, "transported integers changed") + covered = 0 + for mask in images: + need(mask.bit_count() == WEIGHT_BOUND, "transported weight") + need(covered & mask == 0, "transported supports meet") + covered |= mask + need(covered == (1 << WIDTH) - 1, "transported supports miss a line") + need(set(images) != set(RECORDED_SUPPORTS), "transport left the integers fixed") + return images + + +def orthogonal_frames(lines, live): + adjacency = [] + for index in live: + mask = 0 + for bit, other in enumerate(live): + if index != other and dot(lines[index], lines[other]) == 0: + mask |= 1 << bit + adjacency.append(mask) + frames = [] + stack = [((), (1 << WIDTH) - 1)] + steps = 0 + while stack: + steps += 1 + need(steps <= 5000000, "frame enumeration exceeded its state cap") + chosen, candidates = stack.pop() + if len(chosen) == FRAME_SIZE: + frames.append(chosen) + continue + need_more = FRAME_SIZE - len(chosen) + while candidates: + if candidates.bit_count() < need_more: + break + bit = candidates & -candidates + candidates ^= bit + index = bit.bit_length() - 1 + stack.append((chosen + (index,), candidates & adjacency[index])) + frames = tuple(sorted(set(frames))) + need(len(frames) == FRAME_COUNT, "reflected 8-frame count") + for frame in frames: + need(all(dot(lines[live[i]], lines[live[j]]) == 0 + for i, j in combinations(frame, 2)), + "frame not orthogonal") + return frames + + +def kernel(rows): + pivots = {} + for row in rows: + reduced = row + while reduced: + pivot = reduced.bit_length() - 1 + if pivot in pivots: + reduced ^= pivots[pivot] + else: + pivots[pivot] = reduced + break + order = sorted(pivots) + for pivot in order: + row = pivots[pivot] + for other in order: + if other != pivot and (pivots[other] >> pivot) & 1: + pivots[other] ^= row + free = tuple(coordinate for coordinate in range(WIDTH) if coordinate not in pivots) + need(len(pivots) == RANK and free == FREE_COORDINATES, "reflected frame-code rank") + basis = [] + for coordinate in free: + vector = 1 << coordinate + for pivot in order: + if (pivots[pivot] & vector).bit_count() % 2: + vector |= 1 << pivot + need(all((vector & row).bit_count() % 2 == 0 for row in rows), + "a frame parity survives a basis vector") + basis.append(vector) + weights = tuple(vector.bit_count() for vector in basis) + need(weights == BASIS_WEIGHTS, "basis weights changed") + for index, vector in enumerate(basis): + pattern = tuple((vector >> place) & 1 for place in free) + identity = tuple(int(place == index) for place in range(DIMENSION)) + need(pattern == identity, "free coordinates are not a basis identity") + return tuple(basis) + + +def in_code(mask, rows): + return all((mask & row).bit_count() % 2 == 0 for row in rows) + + +def positive_words_have_weight(words, weight): + return all(word.bit_count() == weight for word in words if word) + + +def engine_words(engine, basis, maximum, batch_bits): + listed = list(engine(tuple(basis), WIDTH, maximum, batch_bits)) + need(len(listed) == len(set(listed)), "engine repeated a word") + return set(listed) + + +def build_basis(): + lines, puncture, signed = pinned_model() + simple = load_simple_system() + index_of = check_simple_system(lines, signed, simple) + root, images = select_reflection(lines, puncture, index_of, simple) + live, permutation = rebuilt_list(lines, puncture, images, index_of, root) + supports = transported_supports(permutation) + frames = orthogonal_frames(lines, live) + degree = [0] * WIDTH + for frame in frames: + for index in frame: + degree[index] += 1 + need(set(degree) == {DEGREE}, "frame degree") + rows = tuple(sum(1 << index for index in frame) for frame in frames) + basis = kernel(rows) + generator_hash = sha256(json.dumps(list(basis)).encode()).hexdigest() + print("generator_sha256=" + generator_hash, file=sys.stderr) + need(generator_hash == GENERATOR_SHA256, "generator hash changed") + need(all(in_code(mask, rows) for mask in supports), + "a transported support misses a frame parity") + need(all(not in_code(mask, rows) for mask in RECORDED_SUPPORTS), + "an untransported support is a reflected codeword") + witness = supports[0] + lighter = witness ^ (1 << (witness.bit_length() - 1)) + need(lighter.bit_count() == WEIGHT_BOUND - 1, "clearing the top bit kept the weight") + need(not in_code(lighter, rows), "a weight-fifteen word meets every frame") + return basis, rows, supports, lighter, generator_hash + + +def load_engine(): + engine = run_path( + str(ROOT / "research/e7-bitsliced-exhaustion/binary.py"), + run_name="p112_reflected_lane_engine", + )["low_weight_words"] + signature = inspect.signature(engine) + need(list(signature.parameters) == ["generators", "width", "maximum", "batch_bits"], + "bit-lane signature changed") + need(signature.parameters["batch_bits"].default == ENGINE_BATCH, + "default batch size changed") + return engine + + +def check(mode): + need(mode in ("engine", "basis"), "mode") + authenticate() + started = time.perf_counter() + basis, rows, supports, lighter, generator_hash = build_basis() + basis_seconds = time.perf_counter() - started + target = set(supports) + if mode == "basis": + return { + "status": "BASIS_ONLY", + "generator_sha256": generator_hash, + "basis_seconds": round(basis_seconds, 3), + } + engine = load_engine() + engine_started = time.perf_counter() + produced = engine_words(engine, basis, WEIGHT_BOUND, ENGINE_BATCH) + engine_seconds = time.perf_counter() - engine_started + positive = produced - {0} + digest = support_hash(positive) + print("engine_positive_sha256=" + digest, file=sys.stderr) + need(produced == target | {0}, "engine set differs from the transported supports") + need(0 in produced and positive_words_have_weight(produced, WEIGHT_BOUND), + "engine minimum") + need(len(positive) == SUPPORT_COUNT, "support count") + need(digest == TRANSPORTED_SUPPORT_SHA256, "engine support hash") + need(produced - {supports[0]} != target | {0}, + "dropping one support still compared equal") + need(lighter not in produced, "a weight-fifteen word was yielded") + forged = set(produced) + forged.add(lighter) + need(not positive_words_have_weight(forged, WEIGHT_BOUND), + "weight-fifteen injection was accepted") + need(positive != set(RECORDED_SUPPORTS), "engine returned the untransported integers") + toy = engine_words(engine, (1, 2, 4), 1, 3) + need(toy == {0, 1, 2, 4}, "toy weight-1 set") + need(engine_words(engine, (1, 2, 4), 0, 3) == {0}, "toy bound change was ignored") + try: + list(engine((basis[0], basis[0]), WIDTH, WEIGHT_BOUND, 4)) + except ValueError as error: + need(str(error) == "binary generators must be independent", + "unexpected dependent-generator message") + rejected = True + else: + rejected = False + need(rejected, "a repeated generator was accepted") + need(all(in_code(word, rows) for word in produced), + "a yielded word leaves a frame") + return { + "status": "PASS_P112_REFLECTED_FRAME_LANE", + "width": WIDTH, + "frames": FRAME_COUNT, + "rank": RANK, + "dimension": DIMENSION, + "free_coordinates": list(FREE_COORDINATES), + "engine_batch": ENGINE_BATCH, + "high_batches": HIGH_BATCHES, + "lanes": LANE_COUNT, + "minimum_positive_weight": WEIGHT_BOUND, + "supports": SUPPORT_COUNT, + "yielded_with_zero": len(produced), + "supports_sha256": digest, + "generator_sha256": generator_hash, + "lines_sha256": LINE_SHA256, + "simple_index": SIMPLE_INDEX, + "punctured_index": PUNCTURE_INDEX, + "half_split_rerun": False, + "unreflected_engine_rerun": False, + "intersection_engine_called": False, + "batch_20_run": False, + "dependent_generator_rejected": rejected, + "basis_seconds": round(basis_seconds, 3), + "engine_seconds": round(engine_seconds, 3), + "selected_kappa": SELECTED_KAPPA, + "no_new_kappa": True, + } + + +if __name__ == "__main__": + selected = sys.argv[1] if len(sys.argv) > 1 else "engine" + result = check(selected) + print( + "{status}" + " width={width}" + " dimension={dimension}" + " batch={batch}" + " supports={supports}" + " hash={digest}" + " half_split_rerun=false" + " intersection_engine=false" + " no_new_kappa=true".format( + status=result["status"], + width=result.get("width", WIDTH), + dimension=result.get("dimension", DIMENSION), + batch=result.get("engine_batch", "not-run"), + supports=result.get("supports", SUPPORT_COUNT), + digest=result.get("supports_sha256", "not-run"), + ) + ) + print(json.dumps(result, indent=2, sort_keys=True))