From 11af08b8ff57dc26492501b4efaffdb34d298a00 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 08:57:06 +0000 Subject: [PATCH] Record the reflected P112 frame's transported weight-16 equality. One simple reflection of the #7007 puncture rebuilds a different 112-line frame. A half-split of that kernel matches the transported supports. Selected kappa is unchanged. Co-authored-by: unpaidmoon --- research/p112-reflected-frame-code/README.md | 242 ++++++++ .../p112-reflected-frame-code/SOURCES.json | 24 + research/p112-reflected-frame-code/TASK.json | 67 +++ .../p112-reflected-frame-code/VERIFY.json | 21 + research/p112-reflected-frame-code/scan.c | 195 +++++++ research/p112-reflected-frame-code/verify.py | 540 ++++++++++++++++++ 6 files changed, 1089 insertions(+) create mode 100644 research/p112-reflected-frame-code/README.md create mode 100644 research/p112-reflected-frame-code/SOURCES.json create mode 100644 research/p112-reflected-frame-code/TASK.json create mode 100644 research/p112-reflected-frame-code/VERIFY.json create mode 100644 research/p112-reflected-frame-code/scan.c create mode 100644 research/p112-reflected-frame-code/verify.py diff --git a/research/p112-reflected-frame-code/README.md b/research/p112-reflected-frame-code/README.md new file mode 100644 index 0000000000..a640f1e44b --- /dev/null +++ b/research/p112-reflected-frame-code/README.md @@ -0,0 +1,242 @@ +# One reflected P112 frame keeps the transported weight-16 equality + +**Exhaustive finite census of one reflected frame code. No new κ.** +The selected conditional exponent stays `781451/250000000`. Reflect the first +punctured line that the pinned E8 simple system moves, rebuild the 112-line +complement, and transport the seven supports recorded for the unreflected +frame. One half-split of the rebuilt incidence kernel returns exactly those +seven transported words. + +## Result + +The unreflected root list and the eight punctured lines are the model in +`research/p112-rank6-frame-coverage/engine.py`. An independent E8 builder +reproduces that ordered list. The seven recorded supports, in the order +published with their hash, are + +```text +64691900160 +1034819666160 +280375465144335 +4772259772306660006937399132160 +15509841550538713979819718082560 +1216944648758260568639796318044160 +3955070108453721685622467917250560 +``` + +Their SHA256, of `json.dumps` of that sorted list, is +`ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3`. +This package uses those integers as the set to transport. It does not rerun +the unreflected half-split. + +The simple system is the eight roots fixed by +`research/p112-a3-six-flat/geometry.py`, in that order. Each has norm 8. +The Gram matrix divided by 4 is the Cartan matrix + +```text +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 +``` + +The diagram is E8: node 3 is the branch, with legs of 1, 2 and 4 nodes. +Each simple reflection permutes the 120 lines and is an involution on the +stored vectors. 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 reflection coefficient is `β·α / 4 = 1`, so + +```text +s_α(β) = β - α = (1, -1, 1, 1, 1, 1, 1, -1). +``` + +That vector is line 88 of the pinned list. The same reflection applied to +the whole puncture fixes four lines and moves four: + +| Old line | Old vector | New line | Image vector | +|---:|---|---:|---| +| 0 | `(2, 2, 0, 0, 0, 0, 0, 0)` | 0 | same line | +| 1 | `(2, -2, 0, 0, 0, 0, 0, 0)` | 88 | `(1, -1, 1, 1, 1, 1, 1, -1)` | +| 26 | `(0, 0, 2, 2, 0, 0, 0, 0)` | 95 | `(1, -1, 1, 1, -1, -1, -1, 1)` | +| 27 | `(0, 0, 2, -2, 0, 0, 0, 0)` | 27 | same line | +| 44 | `(0, 0, 0, 0, 2, 2, 0, 0)` | 113 | `(1, -1, -1, -1, 1, 1, -1, 1)` | +| 45 | `(0, 0, 0, 0, 2, -2, 0, 0)` | 45 | same line | +| 54 | `(0, 0, 0, 0, 0, 0, 2, 2)` | 54 | same line | +| 55 | `(0, 0, 0, 0, 0, 0, 2, -2)` | 118 | `(1, -1, -1, -1, -1, -1, 1, -1)` | + +The image is a different orthogonal 8-frame. The rebuilt 112-line list is +the complement of that frame, in increasing position in the same 120-line +order. Its SHA256, of `json.dumps` of the 112 coordinate lists, is +`a2ac7049d9eef1cff8af1eec35b084e6d261efad5311625e5356cceafe260da7`. + +Transport sends each old live line to its reflected line and records the +new position. The resulting permutation of the 112 bit positions is a +bijection and fixes one position. The transported supports are + +```text +12726038110963558112484457976320 +61084916320812443394843581087904 +2433889152476423258413102440464394 +6363012028601310481939177671680 +954453281446482856702353473856 +580303949270928947429810196 +2677278706012631304342476888735745 +``` + +Their SHA256, of `json.dumps` of that sorted list, is +`9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb`. +They are seven disjoint weight-16 words and cover every rebuilt line. + +On that line list there are 1260 orthogonal 8-frames, and every line lies +in 90 of them. The F2 incidence matrix has rank 76. A 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) +``` + +is orthogonal to every frame row. These free coordinates and the basis +weights differ from the unreflected basis. The seven transported supports +meet every frame evenly. Each of the seven untransported integers fails a +frame parity, so the recorded masks are not codewords until they are +transported. + +`scan.c` lists the span of the first 18 generators and the span of the +other 18 by doubling. The basis identity makes the 36 generators +independent, so each of the `2^36` kernel words is the XOR of exactly one +pair. The scan's seen-count and the histogram both equal `68719476736`. +The words of weight 1 through 16 are exactly the seven transported +supports, and the least positive weight is 16. The weight distribution is +the same tuple recorded for the unreflected frame: + +```text +0:1 16:7 20:336 22:3584 24:3752 26:10752 28:6864 30:50176 +32:872613 34:2243584 36:5633600 38:21482496 40:123827424 +42:275960832 44:878407488 46:1531507712 48:3797117779 +50:4774038528 52:8574631520 54:8427087872 56:11893702896 +58:8427087872 60:8574631520 62:4774038528 64:3797117779 +66:1531507712 68:878407488 70:275960832 72:123827424 +74:21482496 76:5633600 78:2243584 80:872613 82:50176 +84:6864 86:10752 88:3752 90:3584 92:336 96:7 112:1 +``` + +That agreement is a comparison of this split's histogram with the recorded +unreflected enumerator. It is a separate run, on the reflected basis. + +A copy of the low-weight set with one support removed compares unequal. +Clearing the top bit of a transported support produces a weight-15 word +that fails a frame parity, and the weight predicate rejects a set that +contains it. The seven untransported integers are not the low-weight set. + +## Scope + +Task card `replay-runtime`, priority revision 8, base +`17469fff78c22941280f04d39dc5a1faee09c840`. Scope status is **refined**. + +The card asks for a new measured speedup that keeps coverage. The +revision-8 verification row instead says that faster output is not the same +coverage until checked. Open PR #7007 recorded the unreflected P112 +weight-16 equality and asked whether one simple reflection preserves that +equality after the root list is transported. This package is that +comparison for the first moving pair: simple root 0 and punctured line 1. +Width 112, weight bound 16, one split after 18 generators. + +The selected record's κ is `781451/250000000`. The priority note on this +base still quotes the older displayed value `0.00310045` from PR #5599. +This package uses the selected record and leaves it unchanged. + +Ordered overlap check on 2026-11-10, after fetching upstream `main` at +`17469fff78c22941280f04d39dc5a1faee09c840`. `scripts/find_overlap.py +--refresh` read 317 open pull requests, including drafts (fetched +`2026-11-10T08:51:47Z`, pagination complete) and 10180 local notes at that +head, with a complete local inventory. The only match was open PR #7007, +which states this question and does not build the reflected frame. The +discussion refresh returned HTTP 504 and left no usable discussion +snapshot. A separate search for the recorded support hash found that same +pull request and no second item, and the latest top-level comments on +discussion #1166 do not treat this frame. No fork `cursor/*` branch had +named this reflected-frame comparison. That partial discussion coverage is +not a proof that no comment mentions it. + +This is an exhaustive finite census of one finite code: all `2^36` kernel +words of this reflected frame, through one half-split. The domain is the +kernel of this one incidence matrix. The basis identity and the seen-count +are the completeness argument. It is not a census of every simple +reflection, not a proof that the iterator is correct for every generator +matrix, and not an unrestricted nonexistence result. A failed search was +not used. The unreflected equality of #7007, the D6 equality of #6959, and +the E6 equality of #6948 are not claimed as this result. + +## Reproduce + +Python 3.12, `gcc`, and the standard library, from the repository root. +One half-split of this kernel measured about 70 seconds on 4 cores. + +```sh +python3 -B scripts/research_package.py --package research/p112-reflected-frame-code --check-only +python3 -I -B research/p112-reflected-frame-code/verify.py +python3 -B scripts/research_package.py --package research/p112-reflected-frame-code +``` + +The direct verifier prints + +```text +PASS_P112_REFLECTED_FRAME_CODE width=112 frames=1260 dimension=36 minimum=16 supports=7 codewords=68719476736 split=18 simple=0 punctured=1 moved_lines=4 same_frame=false unreflected_census=false engine=false no_new_kappa=true +``` + +Outside this run: the unreflected half-split, a second split of this +kernel, `low_weight_words`, `research/e7-intersection-counters/engine.py`, +the E6 and D6 censuses, any other simple root's frame, Lean, Docker, and +`scripts/research_selected_baseline.py` as a scientific replay. The +selected record is provenance only. + +## Open next questions + +1. Does the next simple root, in this same pinned order, that moves a + punctured line induce the same set equality on its own rebuilt list? + This census is the first moving pair only. The reflected frame changes + with the simple root, so the transported integers above do not answer + the next pair. First continue the lexicographic scan of simple root, + then punctured line, and compare one half-split with that pair's + transported supports. +2. Does `low_weight_words` on this reflected 36-generator basis return the + same seven transported supports? This is the bit-lane iterator on the + reflected basis, compared with + `9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb`. + It is separate from the intersection-counter comparison on the + unreflected basis and the hash + `ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3`. + First run that iterator at one batch size on the basis pinned here. + +## Credit + +The 120-line coordinate order and the unreflected puncture are 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. The seven supports, their hash, and the unreflected weight +distribution are the recorded result of open PR #7007. The doubling +half-split follows that package's scanner and reads a different basis. +The question answered here is open question 1 of #7007. + +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-code/SOURCES.json b/research/p112-reflected-frame-code/SOURCES.json new file mode 100644 index 0000000000..7acbb1d69f --- /dev/null +++ b/research/p112-reflected-frame-code/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/p112-rank6-frame-coverage/engine.py", + "usage": "input", + "git_blob": "6afabd3777975310683e4cdc8a4e4b95f0a330ac", + "sha256": "b59101564855a89de04f39fd28b0a853aa3c46ce0ce99951d93d7dd018543536" + } + ] +} diff --git a/research/p112-reflected-frame-code/TASK.json b/research/p112-reflected-frame-code/TASK.json new file mode 100644 index 0000000000..618d0d885c --- /dev/null +++ b/research/p112-reflected-frame-code/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 the first simple reflection that moves a punctured line of the #7007 P112 frame induce the same weight-16 set equality after the 112-line list is rebuilt and the seven recorded supports are transported?", + "scope_change_reason": "The replay-runtime card asks for a measured speedup. The revision-8 verification row says a published faster replay is not equivalent coverage until checked. Open PR #7007 recorded the unreflected P112 equality and asked whether one simple reflection preserves it after transport. This package answers that question for the first moving pair. It does not time an engine or rerun the unreflected census.", + "bottleneck_link": "Frame-code coverage checks remain usable only when the low-weight set still matches after the root list changes. This comparison binds the seven recorded supports to one reflected P112 frame. It does not change a supplier bill or the selected kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the first simple reflection that moves a punctured line, one rebuilt 112-line list, and one half-split compared with the transported supports. Do not test another simple root, rerun the unreflected census, or call the bit-lane or intersection-counter engines.", + "outcome": "completed", + "evidence": "The first simple root in the pinned E8 system that moves a punctured line is alpha=(1,-1,-1,-1,-1,-1,-1,1), acting on (2,-2,0,0,0,0,0,0). The image frame fixes four punctured lines and moves four, and it is a different orthogonal 8-frame. The rebuilt 112-line complement has SHA256 a2ac7049d9eef1cff8af1eec35b084e6d261efad5311625e5356cceafe260da7. Transporting the seven recorded supports gives SHA256 9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb. The incidence matrix has 1260 rows, rank 76 and kernel dimension 36, with free coordinates distinct from the unreflected basis. One half-split after 18 generators visits all 68719476736 kernel words and returns exactly those seven weight-16 supports. The weight distribution equals the distribution recorded for the unreflected frame. The seven untransported integers fail frame parity. Selected kappa stays 781451/250000000.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does the next simple root, in this same pinned order, that moves a punctured line induce the same set equality on its own rebuilt list?", + "why_it_matters": "This census is the first moving pair only. A different simple root produces a different frame, so these transported integers do not answer the next pair.", + "first_step": "Continue the lexicographic scan of simple root, then punctured line, rebuild that 112-line list, and compare one half-split with the transported supports.", + "blocked_by": "This package stops once the first moving pair has been compared." + }, + { + "question": "Does low_weight_words on this reflected 36-generator basis return the same seven transported supports?", + "why_it_matters": "The half-split is one enumeration of this kernel. The bit-lane iterator is a different procedure, and agreement on the unreflected basis does not bind the reflected basis. This is separate from the intersection-counter comparison with hash ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3.", + "first_step": "Run low_weight_words at one batch size on the reflected basis and compare it with support hash 9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb.", + "blocked_by": "This package does not call low_weight_words." + } + ] +} diff --git a/research/p112-reflected-frame-code/VERIFY.json b/research/p112-reflected-frame-code/VERIFY.json new file mode 100644 index 0000000000..cf1485689a --- /dev/null +++ b/research/p112-reflected-frame-code/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-rank6-frame-coverage/engine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate the live E8 line list, check the pinned E8 simple system, reflect the first punctured line that moves, rebuild the 112-line complement, and transport the seven recorded supports. Compare one half-split after 18 generators, visiting all 2^36 kernel words, with those transported supports. Reject a dropped support, a weight-15 injection, and the untransported integers." + } + ] +} diff --git a/research/p112-reflected-frame-code/scan.c b/research/p112-reflected-frame-code/scan.c new file mode 100644 index 0000000000..d0e64bcd5c --- /dev/null +++ b/research/p112-reflected-frame-code/scan.c @@ -0,0 +1,195 @@ +/* Exhaustive half-split of one 112-bit, dimension-36 binary basis. + * + * Each generator is a 112-bit integer, written as 28 lowercase hex digits. + * A split s lists the span of the first s generators and the span of the + * rest by doubling. Every codeword is the XOR of exactly one pair. The + * integer popcount is the Hamming weight. This file does not implement the + * bit-lane iterator. The doubling method is the one used for the unreflected + * P112 frame in PR #7007; this scanner reads only the reflected basis. + * + * Apache-2.0. + */ +#include +#include +#include +#include +#include +#include + +enum { DIM = 36, WIDTH = 112, MAX_LOW = 64 }; + +typedef struct { uint64_t lo, hi; } Word; + +static Word basis[DIM]; +static Word *low_words; +static Word *high_words; +static size_t n_low; +static size_t n_high; +static pthread_mutex_t low_mu = PTHREAD_MUTEX_INITIALIZER; +static Word low_found[MAX_LOW]; +static int n_low_found; +static int overflow; + +typedef struct { + size_t begin, end; + uint64_t hist[WIDTH + 1]; + uint64_t seen; +} Job; + +static Word wxor(Word a, Word b) { + Word c; + c.lo = a.lo ^ b.lo; + c.hi = a.hi ^ b.hi; + return c; +} + +static int weight(uint64_t lo, uint64_t hi) { + return __builtin_popcountll(lo) + __builtin_popcountll(hi); +} + +static int hex_value(char ch) { + if (ch >= '0' && ch <= '9') return ch - '0'; + if (ch >= 'a' && ch <= 'f') return ch - 'a' + 10; + return -1; +} + +static int load_basis(const char *path) { + FILE *fp = fopen(path, "r"); + char hex[80]; + if (!fp) return 0; + for (int i = 0; i < DIM; i++) { + uint64_t lo = 0, hi = 0; + if (fscanf(fp, "%79s", hex) != 1 || strlen(hex) != 28) { + fclose(fp); + return 0; + } + for (int k = 0; k < 28; k++) { + int v = hex_value(hex[k]); + if (v < 0) { + fclose(fp); + return 0; + } + hi = (hi << 4) | (lo >> 60); + lo = (lo << 4) | (unsigned)v; + } + if (hi >> 48) { + fclose(fp); + return 0; + } + basis[i].lo = lo; + basis[i].hi = hi; + } + if (fscanf(fp, "%79s", hex) == 1) { + fclose(fp); + return 0; + } + fclose(fp); + return 1; +} + +static void span(Word *out, int start, int count, size_t expected) { + size_t len = 1; + out[0].lo = 0; + out[0].hi = 0; + for (int i = 0; i < count; i++) { + Word g = basis[start + i]; + for (size_t j = 0; j < len; j++) out[len + j] = wxor(out[j], g); + len <<= 1; + } + if (len != expected) { + fprintf(stderr, "span length mismatch\n"); + exit(1); + } +} + +static void *worker(void *arg) { + Job *job = arg; + memset(job->hist, 0, sizeof job->hist); + job->seen = 0; + for (size_t i = job->begin; i < job->end; i++) { + uint64_t hlo = high_words[i].lo; + uint64_t hhi = high_words[i].hi; + for (size_t j = 0; j < n_low; j++) { + uint64_t lo = hlo ^ low_words[j].lo; + uint64_t hi = hhi ^ low_words[j].hi; + int wt = weight(lo, hi); + job->hist[wt]++; + job->seen++; + if (wt > 0 && wt <= 16) { + pthread_mutex_lock(&low_mu); + if (n_low_found >= MAX_LOW) overflow = 1; + else { + low_found[n_low_found].lo = lo; + low_found[n_low_found].hi = hi; + n_low_found++; + } + pthread_mutex_unlock(&low_mu); + } + } + } + return NULL; +} + +int main(int argc, char **argv) { + int split, threads; + long cpus; + Job *jobs; + pthread_t *ids; + uint64_t hist[WIDTH + 1]; + uint64_t seen = 0; + if (argc != 3) { + fprintf(stderr, "usage: scan BASIS SPLIT\n"); + return 2; + } + split = atoi(argv[2]); + if (split < 1 || split >= DIM || !load_basis(argv[1])) { + fprintf(stderr, "bad basis or split\n"); + return 2; + } + n_low = (size_t)1 << split; + n_high = (size_t)1 << (DIM - split); + low_words = calloc(n_low, sizeof(Word)); + high_words = calloc(n_high, sizeof(Word)); + if (!low_words || !high_words) return 1; + span(low_words, 0, split, n_low); + span(high_words, split, DIM - split, n_high); + cpus = sysconf(_SC_NPROCESSORS_ONLN); + if (cpus < 1) cpus = 1; + if (cpus > 4) cpus = 4; + threads = (int)cpus; + jobs = calloc((size_t)threads, sizeof(Job)); + ids = calloc((size_t)threads, sizeof(pthread_t)); + if (!jobs || !ids) return 1; + for (int t = 0; t < threads; t++) { + size_t chunk = n_high / (size_t)threads; + jobs[t].begin = (size_t)t * chunk; + jobs[t].end = (t + 1 == threads) ? n_high : ((size_t)t + 1) * chunk; + if (pthread_create(&ids[t], NULL, worker, &jobs[t]) != 0) return 1; + } + memset(hist, 0, sizeof hist); + for (int t = 0; t < threads; t++) { + pthread_join(ids[t], NULL); + seen += jobs[t].seen; + for (int w = 0; w <= WIDTH; w++) hist[w] += jobs[t].hist[w]; + } + if (overflow) { + fprintf(stderr, "more than %d words of weight 1..16\n", MAX_LOW); + return 1; + } + printf("SPLIT %d\n", split); + printf("SEEN %llu\n", (unsigned long long)seen); + printf("THREADS %d\n", threads); + for (int w = 0; w <= WIDTH; w++) { + if (hist[w]) printf("HIST %d %llu\n", w, (unsigned long long)hist[w]); + } + for (int i = 0; i < n_low_found; i++) { + printf("LOW %012llx%016llx\n", + (unsigned long long)low_found[i].hi, + (unsigned long long)low_found[i].lo); + } + free(jobs); + free(ids); + free(low_words); + free(high_words); + return 0; +} diff --git a/research/p112-reflected-frame-code/verify.py b/research/p112-reflected-frame-code/verify.py new file mode 100644 index 0000000000..56d1cc4551 --- /dev/null +++ b/research/p112-reflected-frame-code/verify.py @@ -0,0 +1,540 @@ +#!/usr/bin/env python3 +"""One reflected P112 frame and the transported weight-16 set. + +Reflect the first punctured line that a pinned simple root moves, rebuild the +112-line complement, and compare one half-split with the transported images of +the seven supports recorded for the unreflected frame. The scanner lists every +kernel word once. It does not call the bit-lane iterator. +""" + +import json +import subprocess +import sys +import tempfile +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 +CODEWORDS = 1 << DIMENSION +SPLIT_AT = 18 +SIMPLE_INDEX = 0 +PUNCTURE_INDEX = 1 +MOVED_LINES = 4 +FIXED_BITS = 1 +LINE_SHA256 = "a2ac7049d9eef1cff8af1eec35b084e6d261efad5311625e5356cceafe260da7" +RECORDED_SUPPORT_SHA256 = "ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3" +TRANSPORTED_SUPPORT_SHA256 = "9ce7e5edc72ee3104d62cb068146b73840e9a3c42c4132403dece70c8146cccb" +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, +) +# The P112 simple system, in the order fixed by +# research/p112-a3-six-flat/geometry.py. The Gram matrix divided by 4 is the +# E8 Cartan matrix: one branch, with legs of 1, 2 and 4 nodes. +SIMPLE = ( + (1, -1, -1, -1, -1, -1, -1, 1), + (2, 2, 0, 0, 0, 0, 0, 0), + (-2, 2, 0, 0, 0, 0, 0, 0), + (0, -2, 2, 0, 0, 0, 0, 0), + (0, 0, -2, 2, 0, 0, 0, 0), + (0, 0, 0, -2, 2, 0, 0, 0), + (0, 0, 0, 0, -2, 2, 0, 0), + (0, 0, 0, 0, 0, -2, 2, 0), +) +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,), +) +HISTOGRAM = { + 0: 1, + 16: 7, + 20: 336, + 22: 3584, + 24: 3752, + 26: 10752, + 28: 6864, + 30: 50176, + 32: 872613, + 34: 2243584, + 36: 5633600, + 38: 21482496, + 40: 123827424, + 42: 275960832, + 44: 878407488, + 46: 1531507712, + 48: 3797117779, + 50: 4774038528, + 52: 8574631520, + 54: 8427087872, + 56: 11893702896, + 58: 8427087872, + 60: 8574631520, + 62: 4774038528, + 64: 3797117779, + 66: 1531507712, + 68: 878407488, + 70: 275960832, + 72: 123827424, + 74: 21482496, + 76: 5633600, + 78: 2243584, + 80: 872613, + 82: 50176, + 84: 6864, + 86: 10752, + 88: 3752, + 90: 3584, + 92: 336, + 96: 7, + 112: 1, +} + + +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 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 support_digest(words): + payload = json.dumps(sorted(words)).encode() + return sha256(payload).hexdigest() + + +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 == 1, "one live input") + need(support_digest(RECORDED_SUPPORTS) == RECORDED_SUPPORT_SHA256, + "recorded support hash") + need(support_digest(TRANSPORTED_SUPPORTS) == TRANSPORTED_SUPPORT_SHA256, + "pinned transported hash") + return checked + + +def independent_lines(): + roots = [] + for i, j in combinations(range(8), 2): + for si in (2, -2): + for sj in (2, -2): + root = [0] * 8 + root[i], root[j] = si, sj + 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_frame_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, live, 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] = [value - factor * base + for value, base in zip(rows[other], rows[column])] + coeffs = [] + for row in rows: + value = row[-1] + need(value.denominator == 1, "nonintegral simple coordinates") + coeffs.append(int(value)) + built = [0] * 8 + for coeff, simple in zip(coeffs, simples): + for coordinate in range(8): + built[coordinate] += coeff * simple[coordinate] + need(tuple(built) == tuple(root), "simple coordinates do not rebuild the root") + return tuple(coeffs) + + +def check_simple_system(lines, signed): + need(len(SIMPLE) == 8, "simple count") + 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 simple in SIMPLE: + images = {index_of[line_key(reflect(row, simple))] for row in lines} + need(images == set(range(120)), "a simple reflection misses a line") + for row in lines: + need(reflect(reflect(row, simple), simple) == tuple(row), + "a simple reflection is not an involution on the stored vector") + for simple in SIMPLE: + coeffs = integer_combination(simple, SIMPLE) + place = next(index for index, value in enumerate(coeffs) if value) + need(coeffs == tuple(int(index == place) for index in range(8)), + "simple roots are not the coordinate basis") + for root in signed: + coeffs = integer_combination(root, SIMPLE) + need(all(value >= 0 for value in coeffs) or all(value <= 0 for value in coeffs), + "a root is neither positive nor negative on this system") + return index_of + + +def select_reflection(lines, puncture, index_of): + found = None + for simple_index, simple in enumerate(SIMPLE): + 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 = tuple(pair for pair in zip(puncture, images) if pair[0] != pair[1]) + need(len(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") + roots = [list(lines[index]) for index in new_live] + digest = sha256(json.dumps(roots).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 half_split(basis): + with tempfile.TemporaryDirectory(prefix="p112-reflected-") as directory: + work = Path(directory) + binary = work / "scan" + subprocess.run( + ["gcc", "-O3", "-std=c11", "-pthread", "-Wall", "-Werror", + "-o", str(binary), str(HERE / "scan.c")], + check=True, cwd=work, timeout=60, + ) + path = work / "basis.txt" + path.write_text("".join("%028x\n" % vector for vector in basis), encoding="ascii") + completed = subprocess.run( + [str(binary), str(path), str(SPLIT_AT)], + check=True, capture_output=True, text=True, timeout=480, + ) + need(completed.stderr == "", "scan wrote to stderr") + histogram = {} + found = [] + seen = None + reported = None + for line in completed.stdout.splitlines(): + kind, *rest = line.split() + if kind == "SPLIT": + reported = int(rest[0]) + elif kind == "SEEN": + seen = int(rest[0]) + elif kind == "THREADS": + need(1 <= int(rest[0]) <= 4, "thread cap") + elif kind == "HIST": + histogram[int(rest[0])] = int(rest[1]) + elif kind == "LOW": + need(len(rest[0]) == 28, "low-word width") + found.append(int(rest[0], 16)) + else: + raise ValueError("unexpected scan line") + need(reported == SPLIT_AT, "scan split") + need(seen == CODEWORDS, "half-split missed a codeword") + need(sum(histogram.values()) == CODEWORDS, "histogram sum") + for weight, count in histogram.items(): + need(histogram[WIDTH - weight] == count, "complement asymmetry") + need(histogram == HISTOGRAM, "weight distribution changed") + need(min(weight for weight in histogram if weight) == WEIGHT_BOUND, "minimum left 16") + supports = set(found) + need(len(found) == len(supports) == SUPPORT_COUNT, "support count") + need(all(word.bit_count() == WEIGHT_BOUND for word in supports), "a lighter positive word") + return supports + + +def positive_words_have_weight(words, weight): + return all(word.bit_count() == weight for word in words if word) + + +def main(): + authenticate() + lines, puncture, live, signed = pinned_model() + need(live == tuple(index for index in range(120) if index not in set(puncture)), + "live list") + index_of = check_simple_system(lines, signed) + simple, images = select_reflection(lines, puncture, index_of) + new_live, permutation = rebuilt_list(lines, puncture, images, index_of, simple) + supports = transported_supports(permutation) + frames = orthogonal_frames(lines, new_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) + need(all(in_code(mask, rows) for mask in supports), "a transported support leaves a frame") + need(in_code((1 << WIDTH) - 1, rows), "all-ones leaves a frame") + need(all(not in_code(mask, rows) for mask in RECORDED_SUPPORTS), + "an untransported support is a codeword of the reflected frame") + scanned = half_split(basis) + need(scanned == set(supports), "half-split disagrees with the transported supports") + dropped = set(supports) + dropped.remove(supports[0]) + need(dropped != scanned, "dropping one support still compared equal") + lighter = supports[0] ^ (1 << (supports[0].bit_length() - 1)) + need(lighter.bit_count() == WEIGHT_BOUND - 1, "clearing the top bit did not reduce weight") + need(lighter not in scanned and not in_code(lighter, rows), + "a weight-fifteen word was already in the code") + forged = set(scanned) + forged.add(lighter) + need(not positive_words_have_weight(forged, WEIGHT_BOUND), + "weight-fifteen injection was accepted") + need(set(RECORDED_SUPPORTS) != scanned, + "the untransported integers equal the reflected low-weight set") + print( + "PASS_P112_REFLECTED_FRAME_CODE" + " width=%d frames=%d dimension=%d minimum=%d supports=%d" + " codewords=%d split=%d simple=%d punctured=%d moved_lines=%d" + " same_frame=false unreflected_census=false engine=false no_new_kappa=true" + % (WIDTH, FRAME_COUNT, DIMENSION, WEIGHT_BOUND, SUPPORT_COUNT, + CODEWORDS, SPLIT_AT, SIMPLE_INDEX, PUNCTURE_INDEX, MOVED_LINES) + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main())