From 93cd7d9f5d1108d28dca7ef0409acc8f0fd07f95 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 10:38:07 +0000 Subject: [PATCH] Record one P112 27-generator set that returns the eight-word stream. The seven disjoint weight-16 supports plus kernel basis vectors 0..19 form an independent 27-tuple inside the punctured frame code. A Gray-code census of that span and the published intersection-counter engine at batch size 20 both return the recorded eight words. The selected kappa is unchanged. Co-authored-by: unpaidmoon --- .../README.md | 218 +++++++ .../SOURCES.json | 36 ++ .../TASK.json | 67 ++ .../VERIFY.json | 34 + .../verify.py | 587 ++++++++++++++++++ 5 files changed, 942 insertions(+) create mode 100644 research/p112-length27-intersection-return/README.md create mode 100644 research/p112-length27-intersection-return/SOURCES.json create mode 100644 research/p112-length27-intersection-return/TASK.json create mode 100644 research/p112-length27-intersection-return/VERIFY.json create mode 100644 research/p112-length27-intersection-return/verify.py diff --git a/research/p112-length27-intersection-return/README.md b/research/p112-length27-intersection-return/README.md new file mode 100644 index 0000000000..9ef0bbeb0c --- /dev/null +++ b/research/p112-length27-intersection-return/README.md @@ -0,0 +1,218 @@ +# One length-27 P112 generating set returns the eight-word intersection stream + +**One witnessed generating set, one exhaustive span census, and one engine comparison. The selected conditional exponent stays `781451/250000000`.** + +On an explicit independent 27-tuple inside the P112 punctured frame code, +`research/e7-intersection-counters/engine.py` at batch size 20 returns zero +and the seven weight-16 supports whose SHA256 is +`ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3`. + +## Result + +The lines and the punctured frame are the model in +`research/p112-rank6-frame-coverage`. The 1260 orthogonal 8-frames on the +112 live lines have F2 incidence 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, 14, 16, 18, 20, 24, 25, 26, +28, 30, 32, 34, 36, 40, 42, 48, 49, 50, 51, 52, 56, 58, 64, 80 +``` + +is the same 36-generator basis whose ordered 27-prefix contains the first +three published supports and misses the other four. Open PR #7034 records +that the published engine raises `dimension exceeds 27` on all 36 generators. +This package uses a different ordered tuple. + +The seven supports, in the recorded order, are pairwise disjoint and each has +weight 16. They partition the 112 coordinates. The XOR of a subset therefore +has weight `16` times the subset size: bits from different supports do not +cancel. In the F2-span of these seven vectors, the words of weight at most 16 +are exactly zero and the seven supports. That is a proof about these seven +integers. It does not by itself describe a larger span. + +The 27-tuple is those seven supports, followed by the first twenty kernel +basis vectors. Each of those twenty vectors stays independent after the seven +supports under the same high-bit elimination the published engine uses. Their +weights are the first twenty basis weights, from 22 through 50, so each lies +in the span and outside the weight-at-most-16 set. The ordered integers are + +```text +64691900160 +1034819666160 +280375465144335 +4772259772306660006937399132160 +15509841550538713979819718082560 +1216944648758260568639796318044160 +3955070108453721685622467917250560 +4443670059850152665101255383351297 +476478169960083547941896362557442 +1235404508498744078868673813159940 +9983029542622351334877321371656 +1551087412582331123977819014078480 +333427041513561210778684215566368 +2596466671826523360078412021669952 +389342703893815899092640717774976 +3833216057007571418503107247251712 +432611841641411318609815106396672 +2920587414949371429908798658749440 +454485081471164625171710277756928 +1225342658187465785230322160381952 +4146009544401891323911366300975104 +3306510103253472586250966597304320 +1622990553999583501864018977226752 +263432417834582793991910927106048 +2435278157458505060063050639343616 +476517444942813366547851144855552 +3172674985599289618361799917174784 +``` + +SHA256 of `json.dumps` of that list, with the default separators, is +`2d580566f960c80d3f0f6f76342e83a4bf9b650ee9697226e58d8cc15da7da98`. + +The twenty-seven vectors are independent, lie in the frame-code kernel, and +every published support is one of the generators. The span therefore contains +all seven supports. It is a 27-dimensional subspace of the 36-dimensional code. +A binary-reflected Gray code visits each of its `2^27 = 134217728` vectors +once: the coefficient at step `i` is `i xor (i >> 1)`, and the verifier checks +that identity at every step. Exactly eight of those vectors have weight at +most 16, and they are zero together with the seven supports. + +The engine call is `low_weight_words` from +`research/e7-intersection-counters/engine.py`, with `population_planes` and +`at_most` injected from `research/e7-bitsliced-exhaustion/binary.py`. The +published `checked_rows` still contains `need(index < 27, "dimension exceeds 27")`. +This package does not edit that file. The bit-lane enumerator in `binary.py` +rejects the same keyword arguments with `TypeError`. Batch size 20 puts 20 +generators in the lane block and leaves `2^7 = 128` high-offset batches. +The stream is eight distinct words, with no missed support and no extra word. +Its positive-word SHA256, of `json.dumps(sorted(positive_words))`, is +`ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3`. +The stream equals the Gray-code census. + +| Quantity | Value | +|---|---:| +| Live lines | 112 | +| Orthogonal 8-frames | 1260 | +| Incidence rank | 76 | +| Kernel dimension | 36 | +| Generating-set length | 27 | +| Appended basis vectors | indices 0..19 | +| Span words | 134217728 | +| Batch size | 20 | +| Lane generators | 20 | +| High-offset batches | 128 | +| Census words of weight at most 16 | 8 | +| Engine stream | 8 distinct words | +| Set equality | yes | +| Missed supports | 0 | +| Extra words | 0 | +| Positive-word SHA256 | `ff8861dab1…c941e3d3` | + +Three claim types are separate. The disjointness argument is a proof about +the seven supports. The Gray code is an exhaustive finite census of one +27-dimensional span; the domain is finite, every coefficient is visited, and +the bijection check is in `verify.py`. The engine run is a set comparison of +one call at batch size 20. A second 27-tuple is outside this census. The +36-generator input remains outside the published dimension guard. + +Removing the least positive support changes the hash. Passing the first +generator twice raises `dependent generators`. Length 28, formed by repeating +the first generator, raises `dimension exceeds 27` before any yield. Batch +size 10 on the same 27-tuple raises `batch count exceeds 65536`, because +`27 - 10 = 17` exceeds the published limit of 16. The ordered 27-prefix of +the kernel basis is a different tuple: it contains the first three supports +and misses the last four. That membership split is recomputed here from the +kernel. The prefix stream is not enumerated. + +## Scope + +Task card `replay-runtime`, priority revision 8, base +`17469fff78c22941280f04d39dc5a1faee09c840`. Scope status is **refined**. + +The card asks for a measured speedup that keeps coverage. Priority revision 8 +requires the yielded sets to be compared before a faster replay counts as the +same coverage. Open PR #7034 compares every legal batch size on the +36-generator basis and records a capacity refusal. Its second open question +asks whether some other independent generating set of length at most 27, +still inside this code, makes the same engine return the eight-word set at +batch size 20. This package names one such 27-tuple and compares that stream. +The selected record at this base is `781451/250000000`. The priorities page +on the same base still prints the older PR #5599 decimal. This package uses +the selected record. No timing is recorded. + +Ordered overlap check on 2026-11-10, after fetching canonical `main` at +`17469fff78c22941280f04d39dc5a1faee09c840`. `scripts/find_overlap.py --refresh +--include-closed` searched `ff8861dab18040c0`, `length at most 27`, +`admissible 27`, `ordered 27-prefix`, and `p112 intersection-counter`. +Coverage: local notes at that head, 10178 records, complete inventory; 339 +open PR bodies fetched at `2026-11-10T10:29:31Z`; 7013 discussion records +fetched at `2026-11-10T10:30:33Z`; 6175 closed PR bodies fetched at +`2026-11-10T10:31:23Z`. Five matches: open #7034, discussion reply 19513866, +discussion reply 19507785, open #7007, and open #7017. #7034 and reply +19513866 state the 36-generator refusal and leave this 27-tuple question +open. #7007 and reply 19507785 record the bit-lane eight-word set and leave +the intersection-counter engine unrun. #7017 compares a reflected frame with +the bit-lane iterator and separates that hash from this engine. None names +this 27-tuple or runs the published engine on a length-27 generating set. +The helper searches titles and bodies, not code diffs. + +## Reproduce + +Python 3.12 and the standard library, from the repository root. The Gray-code +census is `2^27` popcounts and finishes in a few seconds on this host. The +engine call is one batch-size-20 stream with 128 high-offset batches. + +```sh +python3 -B scripts/research_package.py --package research/p112-length27-intersection-return --check-only +python3 -I -B research/p112-length27-intersection-return/verify.py +python3 -I -O -B research/p112-length27-intersection-return/verify.py +python3 -B scripts/research_package.py --package research/p112-length27-intersection-return +``` + +The direct verifier prints + +```text +PASS_P112_LENGTH27_INTERSECTION_RETURN batch=20 generators=27 span_words=134217728 words=8 hash=ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3 equal=True missed=0 extra=0 timed=false no_new_kappa=true +``` + +Checked here: normal and optimized direct runs, the metadata check, and the +registered package runner. `scripts/research_selected_baseline.py` printed +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` with selected κ `781451/250000000` +and is provenance only. The 36-dimensional bit-lane census, the E6 and D6 comparisons, +the E7 census, a copy of the engine with the dimension guard raised, Lean, +Docker, and any timing harness were not run. + +## Open next questions + +1. Does this same 27-tuple return the eight-word set at batch size 11? Batch + size changes the lane split. Batch size 20 uses 20 lane generators and 128 + high-offset batches. Batch size 11 is the smallest legal batch for 27 + generators, because `27 - 11 = 16`, and it uses 65536 high-offset batches. + First rerun this comparison with `batch_bits` 11, the same 27 integers, + weight bound 16, and support hash. This package stops after batch size 20, + so that split has not been compared. The published dimension guard stays 27. + +2. Does one other admissible 27-tuple inside this code, whose span contains + the seven supports and which is not this extension by basis vectors 0 + through 19, return the same stream at batch size 20? This census covers + one span. A different subspace could contain another word of weight at + most 16. First name that tuple and compare one batch-size-20 stream with + the hash above. The 36-dimensional bit-lane census is open PR #7007 and is + not replayed here, so this package does not treat it as a proof that every + containing subspace has the same low-weight set. + +## Credit + +The 120-line order and the punctured frame are the model in +`research/p112-rank6-frame-coverage`, from the PR1226/PR1323 listing used by +Cinna Davis. The intersection-counter engine is Nick Petalas's +`research/e7-intersection-counters/engine.py`. The injected population and +threshold routines are Ali Romman's PR #5729. The seven supports, the +eight-word hash, and the bit-lane set equality are open PR #7007. The +36-generator refusal, the ordered prefix that misses four supports, and the +question answered here are open PR #7034. The reflected-frame comparison is +open PR #7017 and uses a different iterator. + +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-length27-intersection-return/SOURCES.json b/research/p112-length27-intersection-return/SOURCES.json new file mode 100644 index 0000000000..2d791fe9db --- /dev/null +++ b/research/p112-length27-intersection-return/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/p112-rank6-frame-coverage/engine.py", + "usage": "input", + "git_blob": "6afabd3777975310683e4cdc8a4e4b95f0a330ac", + "sha256": "b59101564855a89de04f39fd28b0a853aa3c46ce0ce99951d93d7dd018543536" + }, + { + "path": "research/e7-bitsliced-exhaustion/binary.py", + "usage": "input", + "git_blob": "cad9fc43ec0244bce415a76bc61b6445ffbd7519", + "sha256": "e79ad4d1d4be1748cf09aacc4274a316000d4b5922f13495778892b9309dc56e" + }, + { + "path": "research/e7-intersection-counters/engine.py", + "usage": "input", + "git_blob": "0283d450aee499682b0fd0ed0585e6d98085ef8a", + "sha256": "882d0177e990b0534bb16ec188a622b6167051505bdb5a7b19b4462499a72e47" + } + ] +} diff --git a/research/p112-length27-intersection-return/TASK.json b/research/p112-length27-intersection-return/TASK.json new file mode 100644 index 0000000000..649cd18ffc --- /dev/null +++ b/research/p112-length27-intersection-return/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 one independent generating set of length 27 inside the P112 punctured frame code, whose span contains all seven weight-16 supports, make research/e7-intersection-counters/engine.py return that eight-word set at batch size 20, with support hash ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3?", + "scope_change_reason": "The replay-runtime card asks for a measured speedup that keeps coverage. Priority revision 8 says faster output is equivalent coverage only after the sets are compared. Open PR #7034 shows that the published intersection-counter engine refuses the 36-generator P112 basis at every legal batch size, and its ordered 27-prefix misses four supports. Its second open question asks for another generating set of length at most 27 whose span contains all seven supports. This package names one such 27-tuple, censuses that span, and compares one batch-size-20 stream. It records no timing and leaves the selected conditional exponent unchanged.", + "bottleneck_link": "Decoder and deletion certificates can reuse a faster iterator only when that iterator still returns every low-weight word of the code being certified. This comparison binds the opt-in intersection-counter engine to one admissible length-27 generating set inside the P112 punctured frame code. It does not change a supplier bill or the selected conditional exponent.", + "budget_minutes": 60, + "stop_rule": "Stop after one explicit 27-tuple, one Gray-code census of its span, and one batch-size-20 call to the published engine. Do not raise the dimension guard, edit engine.py, time the call, or rerun the 36-dimensional bit-lane census.", + "outcome": "completed", + "evidence": "The seven published supports are pairwise disjoint weight-16 codewords, so their span contains exactly eight words of weight at most 16. Appending kernel basis vectors 0 through 19 gives the pinned 27 integers, with generator-list SHA256 2d580566f960c80d3f0f6f76342e83a4bf9b650ee9697226e58d8cc15da7da98. Those vectors are independent codewords and every support is a generator. A binary-reflected Gray code visits all 134217728 span vectors; eight have weight at most 16, and they are zero plus the seven supports. At batch size 20 the published intersection-counter stream is those same eight words, with positive-word SHA256 ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3. Length 28 raises dimension exceeds 27. Batch size 10 raises batch count exceeds 65536. A repeated generator is rejected. The ordered 27-prefix remains a different tuple and misses four supports.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does this same 27-tuple return the eight-word set at batch size 11?", + "why_it_matters": "Batch size changes the engine's lane split. Batch size 20 uses 20 lane generators and 128 high-offset batches. Batch size 11 is the smallest legal batch for 27 generators and uses 65536 high-offset batches.", + "first_step": "Rerun this comparison with batch_bits set to 11 and the same 27 integers, weight bound 16, and support hash.", + "blocked_by": "This package stops after batch size 20, so batch size 11 has not been compared. The published dimension guard stays 27." + }, + { + "question": "Does one other admissible 27-tuple inside this code, whose span contains the seven supports and which is not this extension by basis vectors 0 through 19, return the same stream at batch size 20?", + "why_it_matters": "This census covers one span. A different subspace could contain another word of weight at most 16, and the engine could then return a different set.", + "first_step": "Name one other independent 27-tuple of codewords that contains every published support and is not this coordinate extension, then compare one batch-size-20 stream with the same hash.", + "blocked_by": "This package records one tuple. The 36-dimensional bit-lane census is open PR #7007 and is not replayed here." + } + ] +} diff --git a/research/p112-length27-intersection-return/VERIFY.json b/research/p112-length27-intersection-return/VERIFY.json new file mode 100644 index 0000000000..3f9ed1fbd0 --- /dev/null +++ b/research/p112-length27-intersection-return/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-rank6-frame-coverage/engine.py", + "research/e7-bitsliced-exhaustion/binary.py", + "research/e7-intersection-counters/engine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Rebuild the P112 36-dimensional kernel, require the pinned 27-tuple and support hash ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3, census all 2^27 span words, and compare one published intersection-counter stream at batch size 20 with that eight-word set. Reject a dropped support, a repeated generator, a 28th generator, and batch size 10." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Repeat the same batch-size-20 set comparison under optimized bytecode. The checks are ValueError guards, so optimization does not disable them." + } + ] +} diff --git a/research/p112-length27-intersection-return/verify.py b/research/p112-length27-intersection-return/verify.py new file mode 100644 index 0000000000..6eccca7114 --- /dev/null +++ b/research/p112-length27-intersection-return/verify.py @@ -0,0 +1,587 @@ +#!/usr/bin/env python3 +"""One length-27 P112 generating set returns the eight-word intersection stream. + +The seven partition supports are pairwise disjoint weight-16 codewords. Their +F2-span therefore contains exactly those seven words and zero at weight at +most 16. Appending the first twenty kernel-basis vectors that stay independent +under the engine's high-bit elimination produces an explicit 27-tuple inside +the same code. A binary-reflected Gray code lists every vector of that span. +The published intersection-counter engine is then called once, at batch size +20, and the yielded set is compared with that census and with hash +ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3. +""" + +import inspect +import json +from functools import partial +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 +TUPLE_LENGTH = 27 +NAMED_BATCH = 20 +LANE_GENERATORS = 20 +HIGH_OFFSETS = 1 << (TUPLE_LENGTH - LANE_GENERATORS) +SPAN_WORDS = 1 << TUPLE_LENGTH +FREE_COORDINATES = ( + 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 14, 16, 18, 20, 24, 25, 26, + 28, 30, 32, 34, 36, 40, 42, 48, 49, 50, 51, 52, 56, 58, 64, 80, +) +BASIS_WEIGHTS = ( + 38, 34, 38, 30, 42, 34, 26, 30, 42, 30, 50, 30, 38, 42, 34, 22, 32, 32, + 32, 30, 32, 32, 30, 22, 24, 36, 20, 36, 28, 36, 28, 32, 32, 32, 32, 32, +) +SUPPORTS = ( + 64691900160, + 1034819666160, + 280375465144335, + 4772259772306660006937399132160, + 15509841550538713979819718082560, + 1216944648758260568639796318044160, + 3955070108453721685622467917250560, +) +GENERATORS = ( + 64691900160, + 1034819666160, + 280375465144335, + 4772259772306660006937399132160, + 15509841550538713979819718082560, + 1216944648758260568639796318044160, + 3955070108453721685622467917250560, + 4443670059850152665101255383351297, + 476478169960083547941896362557442, + 1235404508498744078868673813159940, + 9983029542622351334877321371656, + 1551087412582331123977819014078480, + 333427041513561210778684215566368, + 2596466671826523360078412021669952, + 389342703893815899092640717774976, + 3833216057007571418503107247251712, + 432611841641411318609815106396672, + 2920587414949371429908798658749440, + 454485081471164625171710277756928, + 1225342658187465785230322160381952, + 4146009544401891323911366300975104, + 3306510103253472586250966597304320, + 1622990553999583501864018977226752, + 263432417834582793991910927106048, + 2435278157458505060063050639343616, + 476517444942813366547851144855552, + 3172674985599289618361799917174784, +) +SUPPORT_SHA256 = ( + "ff8861dab18040c03d403a860773218df7c120d03770d701afb61b78c941e3d3" +) +GENERATOR_LIST_SHA256 = ( + "2d580566f960c80d3f0f6f76342e83a4bf9b650ee9697226e58d8cc15da7da98" +) +BASIS_LIST_SHA256 = ( + "c93a6ec3f6d61b3bbf4086218c723761e517bc42ac2c26f551436d271a081e9d" +) +JSON_LIST_SHA256 = ( + "3a316d6d3226f84c1e46e4447fa8d5fd800bff4a1bc6498152523cd4a602b69b" +) +SELECTED_KAPPA = "781451/250000000" +PAIRS = ((0, 1), (2, 3), (4, 5), (6, 7)) +MATCHINGS = (((0, 3), (1, 2)), ((0, 2), (1, 3)), ((0, 1), (2, 3))) +SPINOR_REPS = ((0, 0, 0, 0), (0, 0, 1, 1), (0, 1, 0, 1), (0, 1, 1, 0)) +DIMENSION_MESSAGE = "dimension exceeds 27" +BATCH_COUNT_MESSAGE = "batch count exceeds 65536" +DEPENDENT_MESSAGE = "dependent generators" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +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") + selected = json.loads( + (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8") + ) + need(selected["kappa"] == SELECTED_KAPPA, "selected kappa changed") + return checked + + +def support_hash(words): + payload = json.dumps(sorted(word for word in words if word)).encode() + return sha256(payload).hexdigest() + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def canonical(vector): + first = next(value for value in vector if value) + return tuple(vector) if first > 0 else tuple(-value for value in vector) + + +def independent_lines(): + roots = [] + for i, j in combinations(range(8), 2): + for si, sj in product((2, -2), repeat=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 = max(root, tuple(-value for value in 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) + + +def pinned_model(): + model = run_path( + str(ROOT / "research/p112-rank6-frame-coverage/engine.py"), + run_name="p112_length27_model", + )["model"]() + lines = tuple(tuple(row) for row in model["lines"]) + puncture = tuple(model["punctured_frame"]) + live = tuple(model["live"]) + own_lines, own_puncture = 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, "width") + need(all(dot(line, line) == 8 for line in lines), "norms") + return lines, live + + +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 <= 200000, "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])) + need(len(frames) == len(set(frames)) == FRAME_COUNT, "live 8-frame count") + frames = tuple(sorted(frames)) + degree = [0] * WIDTH + for frame in frames: + need(len(frame) == FRAME_SIZE, "frame length") + for index in frame: + degree[index] += 1 + need( + all( + dot(lines[live[i]], lines[live[j]]) == 0 + for i, j in combinations(frame, 2) + ), + "frame not orthogonal", + ) + need(set(degree) == {DEGREE}, "frame degree") + need(steps == 56262, "frame search did not finish in 56262 states") + 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, "P112 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 + basis.append(vector) + basis = tuple(basis) + need(tuple(vector.bit_count() for vector in basis) == BASIS_WEIGHTS, "basis weights") + 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") + need(all((vector & row).bit_count() % 2 == 0 for row in rows), "basis left the code") + digest = sha256(json.dumps(list(basis)).encode()).hexdigest() + need(digest == BASIS_LIST_SHA256, "basis-list hash " + digest) + return basis + + +def partition_masks(lines, live): + by_root = {lines[old]: bit for bit, old in enumerate(live)} + + def pair_mask(matching): + mask = 0 + for left, right in matching: + for i in PAIRS[left]: + for j in PAIRS[right]: + for sign in (1, -1): + root = [0] * 8 + root[i] = 2 + root[j] = 2 * sign + mask |= 1 << by_root[canonical(root)] + return mask + + spinors = [ + lines[old] for old in live if all(abs(value) == 1 for value in lines[old]) + ] + need(len(spinors) == 64, "spinor line count") + + def relative(root): + return tuple( + 0 if root[2 * pair] == root[2 * pair + 1] else 1 for pair in range(4) + ) + + def spin_mask(representative): + patterns = {representative, tuple(1 - bit for bit in representative)} + mask = 0 + for root in spinors: + if relative(root) in patterns: + mask |= 1 << by_root[root] + return mask + + masks = tuple(pair_mask(item) for item in MATCHINGS) + tuple( + spin_mask(item) for item in SPINOR_REPS + ) + covered = 0 + for mask in masks: + need(mask.bit_count() == WEIGHT_BOUND, "partition block weight") + need(covered & mask == 0, "partition blocks meet") + covered |= mask + need(covered == (1 << WIDTH) - 1, "partition misses a live line") + return masks + + +def absorb(pivots, row): + """Return whether `row` is independent under the engine's high-bit scan.""" + residual = row + for pivot in range(WIDTH - 1, -1, -1): + if residual >> pivot & 1: + if pivot in pivots: + residual ^= pivots[pivot] + else: + pivots[pivot] = residual + return True + return False + + +def extend_supports(supports, basis): + """Published supports, then basis vectors that remain independent.""" + pivots = {} + chosen = [] + for row in supports: + need(absorb(pivots, row), "a published support is dependent") + chosen.append(row) + added = [] + for index, row in enumerate(basis): + if len(chosen) == TUPLE_LENGTH: + break + if absorb(pivots, row): + chosen.append(row) + added.append(index) + need(len(chosen) == TUPLE_LENGTH, "the extension did not reach length 27") + need(tuple(added) == tuple(range(20)), "the first twenty basis vectors were not all used") + return tuple(chosen) + + +def in_span(word, generators): + pivots = {} + for row in generators: + need(absorb(pivots, row), "span test received a dependent generator") + residual = word + for pivot in range(WIDTH - 1, -1, -1): + if residual >> pivot & 1: + if pivot not in pivots: + return False + residual ^= pivots[pivot] + return residual == 0 + + +def disjoint_support_span(supports): + """Proof check: disjoint weight-16 words have no other light combination. + + The XOR of a subset has weight 16 times the subset size, because bits from + distinct supports never cancel. Weight at most 16 holds for the empty sum + and the seven singletons, and for no other subset. + """ + covered = 0 + for word in supports: + need(word.bit_count() == WEIGHT_BOUND, "a support is not weight 16") + need(covered & word == 0, "two supports meet") + covered |= word + need(covered == (1 << WIDTH) - 1, "the supports do not partition the 112 bits") + for size in range(2, len(supports) + 1): + need(WEIGHT_BOUND * size > WEIGHT_BOUND, "a multiple sum could stay at weight 16") + + +def gray_low(generators, maximum): + """List every span word of weight at most `maximum`, each subset once. + + At index i the coefficient mask is the binary-reflected Gray code + i xor (i >> 1). That map is a bijection of the coefficient integers, so + the loop visits each of the 2**len(generators) combinations once. The + bit flipped between i and i+1 is the trailing-zero count of i+1. + """ + limit = 1 << len(generators) + word = 0 + mask = 0 + found = [] + for index in range(limit): + if mask != index ^ (index >> 1): + raise ValueError("gray coefficient left index " + str(index)) + if word.bit_count() <= maximum: + found.append(word) + nxt = index + 1 + if nxt == limit: + break + bit = (nxt & -nxt).bit_length() - 1 + word ^= generators[bit] + mask ^= 1 << bit + return found + + +def toy_gray_control(): + found = gray_low((1, 2, 4, 8), 1) + need(set(found) == {0, 1, 2, 4, 8}, "toy weight-1 census changed") + entire = gray_low((1, 2, 4, 8), 4) + need(len(entire) == len(set(entire)) == 16, "toy census missed a combination") + + +def bind_engine(): + binary = run_path( + str(ROOT / "research/e7-bitsliced-exhaustion/binary.py"), + run_name="p112_length27_population", + ) + engine_ns = run_path( + str(ROOT / "research/e7-intersection-counters/engine.py"), + run_name="p112_length27_engine", + ) + engine = engine_ns["low_weight_words"] + signature = inspect.signature(engine) + for name in ("population_planes", "at_most"): + parameter = signature.parameters[name] + need( + parameter.kind is inspect.Parameter.KEYWORD_ONLY, + name + " is not keyword-only on the intersection engine", + ) + source = inspect.getsource(engine_ns["checked_rows"]) + need('need(index < 27, "dimension exceeds 27")' in source, "dimension guard text changed") + try: + binary["low_weight_words"]( + (1,), + 1, + 0, + 1, + population_planes=binary["population_planes"], + at_most=binary["at_most"], + ) + except TypeError: + separated = True + else: + separated = False + need(separated, "the bit-lane enumerator accepted the intersection keywords") + bound = partial( + engine, + population_planes=binary["population_planes"], + at_most=binary["at_most"], + ) + return bound, engine_ns["checked_rows"] + + +def stream_outcome(engine, generators, batch): + stream = engine(generators, WIDTH, WEIGHT_BOUND, batch) + try: + return list(stream), None + except ValueError as exc: + return [], str(exc) + finally: + stream.close() + + +def check(): + need( + sha256(json.dumps([1, 2]).encode()).hexdigest() == JSON_LIST_SHA256, + "JSON list encoding changed", + ) + need(len(GENERATORS) == TUPLE_LENGTH, "pinned tuple length") + need(GENERATORS[: len(SUPPORTS)] == SUPPORTS, "the tuple does not start with the supports") + need( + sha256(json.dumps(list(GENERATORS)).encode()).hexdigest() == GENERATOR_LIST_SHA256, + "pinned generator-list hash changed", + ) + need(HIGH_OFFSETS == 128 and SPAN_WORDS == 134217728, "span shape") + need(TUPLE_LENGTH - NAMED_BATCH == 7 and TUPLE_LENGTH - 10 == 17, "batch guards") + authenticate() + lines, live = pinned_model() + frames = orthogonal_frames(lines, live) + rows = tuple(sum(1 << index for index in frame) for frame in frames) + basis = kernel(rows) + rebuilt = partition_masks(lines, live) + need(tuple(sorted(rebuilt)) == tuple(sorted(SUPPORTS)), "partition integers changed") + digest = support_hash(SUPPORTS) + need(digest == SUPPORT_SHA256, "support hash " + digest) + dropped = support_hash(SUPPORTS[1:]) + need(dropped != SUPPORT_SHA256, "dropping one support kept the hash") + disjoint_support_span(SUPPORTS) + generators = extend_supports(SUPPORTS, basis) + need(generators == GENERATORS, "the extension does not match the pinned 27-tuple") + need(generators[len(SUPPORTS):] == basis[:20], "the tail is not basis vectors 0..19") + need(generators != basis[:TUPLE_LENGTH], "the tuple collapsed to the ordered 27-prefix") + inside = [word for word in SUPPORTS if in_span(word, basis[:TUPLE_LENGTH])] + outside = [word for word in SUPPORTS if word not in inside] + need(inside == list(SUPPORTS[:3]), "the ordered prefix does not contain the first three supports") + need(outside == list(SUPPORTS[3:]), "the ordered prefix does not miss the last four supports") + for word in SUPPORTS: + need(in_span(word, generators), "a support left the 27-span") + for vector in generators: + need(0 < vector < 1 << WIDTH, "generator outside 1..2^112-1") + need( + all((vector & row).bit_count() % 2 == 0 for row in rows), + "a generator leaves the frame code", + ) + engine, checked_rows = bind_engine() + admitted, count = checked_rows(generators, WIDTH, WEIGHT_BOUND, NAMED_BATCH) + need(len(admitted) == TUPLE_LENGTH and count == LANE_GENERATORS, "batch 20 rejected the 27-tuple") + toy_gray_control() + census = gray_low(generators, WEIGHT_BOUND) + need(len(census) == len(set(census)) == 8, "the 27-span census is not eight distinct words") + need(set(census) == set(SUPPORTS) | {0}, "the 27-span census is not the eight-word set") + need(support_hash(census) == SUPPORT_SHA256, "census hash changed") + yielded, message = stream_outcome(engine, generators, NAMED_BATCH) + need(message is None, "the engine refused the 27-tuple: " + str(message)) + need(len(yielded) == len(set(yielded)) == 8, "the engine stream is not eight distinct words") + missed = sorted(set(SUPPORTS) - set(yielded)) + extra = sorted(set(yielded) - set(SUPPORTS) - {0}) + need(missed == [] and extra == [], "missed " + str(missed) + " extra " + str(extra[:8])) + need(0 in yielded, "the engine omitted zero") + need(set(yielded) == set(census), "the engine stream differs from the Gray-code census") + need(support_hash(yielded) == SUPPORT_SHA256, "engine hash changed") + duplicate, duplicate_message = stream_outcome(engine, (generators[0], generators[0]), NAMED_BATCH) + need( + duplicate == [] and duplicate_message == DEPENDENT_MESSAGE, + "a repeated generator produced " + str(duplicate_message), + ) + longer, longer_message = stream_outcome(engine, generators + (generators[0],), NAMED_BATCH) + need( + longer == [] and longer_message == DIMENSION_MESSAGE, + "length 28 produced " + str(longer_message), + ) + small_batch, small_message = stream_outcome(engine, generators, 10) + need( + small_batch == [] and small_message == BATCH_COUNT_MESSAGE, + "batch size 10 produced " + str(small_message), + ) + return { + "status": "PASS_P112_LENGTH27_INTERSECTION_RETURN", + "claim_proof": "seven disjoint weight-16 supports span exactly eight light words", + "claim_census": "exhaustive Gray code of one 27-dimensional span", + "claim_comparison": "one intersection-counter stream at batch size 20", + "width": WIDTH, + "frames": FRAME_COUNT, + "rank": RANK, + "code_dimension": DIMENSION, + "generators": TUPLE_LENGTH, + "support_generators": len(SUPPORTS), + "appended_basis_indices": list(range(20)), + "named_batch": NAMED_BATCH, + "lane_generators": LANE_GENERATORS, + "high_offset_batches": HIGH_OFFSETS, + "span_words": SPAN_WORDS, + "census_words": len(census), + "engine_words": len(yielded), + "sets_equal": True, + "missed_supports": missed, + "extra_words": extra, + "prefix_contains_supports": len(inside), + "prefix_misses_supports": len(outside), + "supports_sha256": SUPPORT_SHA256, + "generator_list_sha256": GENERATOR_LIST_SHA256, + "dimension_guard_raised": False, + "engine_source_edited": False, + "codeword_enumeration_of_the_36_generator_code": False, + "bit_lane_iterator_replayed": False, + "timing_measured": False, + "selected_kappa": SELECTED_KAPPA, + "kappa_changed": False, + } + + +if __name__ == "__main__": + result = check() + print( + "PASS_P112_LENGTH27_INTERSECTION_RETURN" + " batch={named_batch}" + " generators={generators}" + " span_words={span_words}" + " words={engine_words}" + " hash={supports_sha256}" + " equal={sets_equal}" + " missed={missed}" + " extra={extra}" + " timed=false" + " no_new_kappa=true".format( + missed=len(result["missed_supports"]), + extra=len(result["extra_words"]), + **result, + ) + ) + print(json.dumps(result, indent=2, sort_keys=True))