diff --git a/research/leech-minor-byte-lanes/BENCHMARK.json b/research/leech-minor-byte-lanes/BENCHMARK.json new file mode 100644 index 0000000000..753587486b --- /dev/null +++ b/research/leech-minor-byte-lanes/BENCHMARK.json @@ -0,0 +1,88 @@ +{ + "adapter_sha256": { + "PINS.json": "47d4c05d3753e26cb84aeaea12a697174e62a7bf24f7c4699c4a5f9f19afe6d0", + "benchmark.py": "0e0d7e9c9f2c6d7f050bf015a5d6fbc892df809bbac5faae9b88a1f004fd1bf2", + "lanes.py": "2c242d4284e1c8520cbc0cfbbb20ddf186c662e5f6173bed400bbd4022df34c7", + "replay.py": "aa73a3ea405c1b3cdbe20888624b2f3e93a8ddff65476e25171c71975f4b8490" + }, + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "certificate_sha256": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "machine": "x86_64", + "median_speedup": 2.107932325412675, + "median_wall_seconds": { + "baseline": 18.94655950699996, + "lanes": 8.988220009999964 + }, + "platform": "Linux-6.18.44-x86_64-with-glibc2.41", + "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]", + "samples": [ + { + "mode": "baseline", + "receipt": { + "certificate_sha256": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "executed_geometry_sha256": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1", + "mode": "baseline", + "status": "PASS_AFFINE_VECTOR_REPLAY" + }, + "round": 1, + "wall_seconds": 17.051406369999995 + }, + { + "mode": "lanes", + "receipt": { + "certificate_sha256": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "executed_geometry_sha256": "e3b1cfb013afc4ac8d4306836b8840d9776a2ac82eb76b44582fa6bd46a6f957", + "mode": "lanes", + "status": "PASS_AFFINE_VECTOR_REPLAY" + }, + "round": 1, + "wall_seconds": 8.988220009999964 + }, + { + "mode": "lanes", + "receipt": { + "certificate_sha256": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "executed_geometry_sha256": "e3b1cfb013afc4ac8d4306836b8840d9776a2ac82eb76b44582fa6bd46a6f957", + "mode": "lanes", + "status": "PASS_AFFINE_VECTOR_REPLAY" + }, + "round": 2, + "wall_seconds": 7.5365457379999725 + }, + { + "mode": "baseline", + "receipt": { + "certificate_sha256": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "executed_geometry_sha256": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1", + "mode": "baseline", + "status": "PASS_AFFINE_VECTOR_REPLAY" + }, + "round": 2, + "wall_seconds": 18.94655950699996 + }, + { + "mode": "baseline", + "receipt": { + "certificate_sha256": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "executed_geometry_sha256": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1", + "mode": "baseline", + "status": "PASS_AFFINE_VECTOR_REPLAY" + }, + "round": 3, + "wall_seconds": 22.67777050899997 + }, + { + "mode": "lanes", + "receipt": { + "certificate_sha256": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "executed_geometry_sha256": "e3b1cfb013afc4ac8d4306836b8840d9776a2ac82eb76b44582fa6bd46a6f957", + "mode": "lanes", + "status": "PASS_AFFINE_VECTOR_REPLAY" + }, + "round": 3, + "wall_seconds": 14.988175710000064 + } + ], + "scope": "Complete nine-screen historical affine-vector audit; process startup, source admission, all checks and output included. No timing threshold.", + "status": "PASS_IDENTICAL_COMPLETE_CERTIFICATES" +} diff --git a/research/leech-minor-byte-lanes/CLAIM.md b/research/leech-minor-byte-lanes/CLAIM.md new file mode 100644 index 0000000000..200cbba8f8 --- /dev/null +++ b/research/leech-minor-byte-lanes/CLAIM.md @@ -0,0 +1,57 @@ +# Seed 86 verification engineering claim + +- Assignment: OS randomness (`secrets.randbelow(100)`) returned **86** at + 2026-10-13 10:29:34 UTC; track 85–94, verification engineering. +- Exact base: `f567884aeb8851b6e794af1184119a3bfbe1e631` (fetched upstream main). +- Object: the five historical Leech lattice minor replays in + `scripts/experiments/affine_vector_screens.py`, using every recorded row and + column in `scripts/experiments/affine_vector_witnesses.json`. +- Method: replace pairwise Python dot products by carry-safe exact integer + lanes; compare full packed row streams, ranks and certificates on identical + inputs. Preserve validation and rejection checks; no probabilistic ranks. +- Deliverable: opt-in source-pinned accelerator, before/after benchmark, + complete equivalence checks and negative controls. No new kappa or theorem. +- Expected finish: 2026-10-13 11:10 UTC (22:10 Australia/Sydney). + +Three candidates were (0) memoizing repeated subset-core interval evaluations, +(1) accelerating the coded-carry exhaustive affine-agreement control, and +(2) reconstructing the five Leech minors with exact integer lanes. `86 % 3 = 2` +selects the last after excluding occupied recent tooling targets. Seed 86 also +fixes the supplemental generated test cases; it does not change the five +historical fixtures or their complete coverage. + +The selected record was followed to the PR799 X4 construction and maintainer +review (conditional kappa 0.001661634653669567, with PR589/555). The PR ledger, +contribution guidance and historical affine-vector negative-result scope were +read. The latest 100 open PRs through #891 and all-state tooling, subset, +affine, coded-tooling, Leech-tooling and `affine_vector_screens` searches were +checked. #752 accelerates quadratic-affine minors and #778 single-intersection +Gram matrices: related integer-packing techniques, distinct matrices and +checks. #849 concerns dyadic X4 arithmetic and #871 historical joint-frame +rank checks. No duplicate Leech-minor accelerator was found. + +Only issue #650 (request to enable Discussions) was open and had no comments; +no pinned sprint coordination issue was available. Claim recorded locally per +the sprint instructions. No delegated workers. + +Contributor: CubeJerry, with substantial OpenAI Codex assistance. Apache-2.0. + +## Result — 2026-10-13 10:50 UTC + +Completed the opt-in accelerator: all 5,927 original Leech rows (7,531,037 +entries) and the complete nine-screen certificate agree exactly. Three final +alternating fresh-process pairs measured 18.946560s to 8.988220s median, +**2.107932x** on Linux/CPython 3.12.14. Eleven test groups, all three unchanged +predecessor tests in both modes, minimal offline relocation, selected-record +integrity and its five tests pass. No new kappa is claimed. + +Result package and reproducible evidence: +[leech-minor-byte-lanes](https://github.com/CubeJerry/integer-mult-bounds/tree/tooling/seed86-exact-verification/research/leech-minor-byte-lanes). + +Final metadata refresh covered new PRs through #894 and all-state Leech and +affine-checker searches. No overlapping accelerator was found. DominikScholz's +#598 (head `615ca6f06fdea0c50dbef733370c47349e25c555`) studies different +Leech/Turyn constructions and fitting bounds; those negative searches are not +reopened here. The pinned-issues GraphQL query returned no coordination issue. +Upstream main remains the recorded base. All 41 retained input hashes also +match the base Git objects. The branch is ready for one focused tooling PR. diff --git a/research/leech-minor-byte-lanes/EXPECTED.json b/research/leech-minor-byte-lanes/EXPECTED.json new file mode 100644 index 0000000000..a9c89543c4 --- /dev/null +++ b/research/leech-minor-byte-lanes/EXPECTED.json @@ -0,0 +1,49 @@ +{ + "assignment_seed": 86, + "cases": [ + { + "columns": 715, + "rows": 683, + "rows_sha256": "b54f09a244ab154e868979e71fd81a428a6b4a9169f96bc6ded04e45d8fdfa35", + "shift": 0, + "signed": false + }, + { + "columns": 1343, + "rows": 1311, + "rows_sha256": "f743deb780a127a387d8e086ae1d48b42259e3070cc2c506516f0a51d2a88f33", + "shift": -16, + "signed": true + }, + { + "columns": 1343, + "rows": 1311, + "rows_sha256": "51e0a2e8c02829aa8cac3dc1bde9d917e6330a7cb3526c35691b94be8cb8a833", + "shift": -8, + "signed": true + }, + { + "columns": 1343, + "rows": 1311, + "rows_sha256": "10ecb66bffb241e22238f9b6264821f95f5f6924414a007df63ba59db2260fb5", + "shift": 8, + "signed": true + }, + { + "columns": 1343, + "rows": 1311, + "rows_sha256": "c99ed2b19e1210503de5cba13452b355e351f238e6a4676f6bfe8036bf9de4d0", + "shift": 16, + "signed": true + } + ], + "complete_certificate_sha256": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "executed_geometry_sha256": { + "baseline": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1", + "lanes": "e3b1cfb013afc4ac8d4306836b8840d9776a2ac82eb76b44582fa6bd46a6f957" + }, + "full_rows_compared": 5927, + "matrix_entries_compared": 7531037, + "scope": "Five historical Leech minors and unchanged nine-screen certificate; no new kappa.", + "status": "PASS_LEECH_BYTE_LANES" +} diff --git a/research/leech-minor-byte-lanes/NOTICE.md b/research/leech-minor-byte-lanes/NOTICE.md new file mode 100644 index 0000000000..dfa3599e3a --- /dev/null +++ b/research/leech-minor-byte-lanes/NOTICE.md @@ -0,0 +1,34 @@ +# Attribution and source pins + +Contribution: Jerry Chen (@CubeJerry), with substantial OpenAI Codex assistance +in implementation, analysis, tests and documentation. Apache-2.0; the +repository LICENSE applies. No independent human review is claimed. + +The original affine-vector families, Golay/Leech generator, fixed witnesses, +rank rejections and audit are by **Douglas R. Colkitt**, retained from commit +`d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0`. The source note credits Brouwer and +Van Maldeghem, *Strongly Regular Graphs*, section 6.3.1 for the minimal-vector +construction. The original note, source files and all attribution remain +unchanged. `PINS.json` gives exact file hashes at base +`f567884aeb8851b6e794af1184119a3bfbe1e631`. + +**Curtis Dransfield (@Curtis-D), PR752**, head +`3603d8d9184995ae1cc67c0f5e01f02f3a1d634e`, supplies the related carry-safe +integer-lane approach for quadratic-affine Hermitian minors. Its technique and +coverage discipline are credited; no code or fixture from that PR is copied. +This contribution reconstructs a distinct set of five signed real Leech +minors and decodes bytes directly. + +**merramil, PR778**, head `f015b04c74801fa330f818d178e809c760fb5469`, improves +historical single-intersection Gram construction with symmetric packing. +It is related concurrent performance work, not a dependency of this package. +The original `rank_of_rows` imported here remains unchanged. + +The retained upstream OpenAI manuscript and sources are pinned at +`adc7f1241b42e322a6451854ab7e4b4c146bf78a` with their original Apache-2.0 +license and notices. No upstream file is modified. + +Selected-result context follows Jeremy Kothe's PR799 X4 construction, +Chafik Boukhalfa's PR741 and DreamingOfClouds' PR589 on eumemic's PR555. +Those constructions and their predecessors are not changed or re-certified +by this historical-checker optimization. diff --git a/research/leech-minor-byte-lanes/PINS.json b/research/leech-minor-byte-lanes/PINS.json new file mode 100644 index 0000000000..4ce857853f --- /dev/null +++ b/research/leech-minor-byte-lanes/PINS.json @@ -0,0 +1,46 @@ +{ + "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "files": { + "certificates/affine-vector-screens.json": "f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0", + "docs/research/affine-vector-screens.md": "22e5beab6df8127fc4377142768fc1a0a3317d7e8fba52c089670ecf1aa076b6", + "scripts/audit_affine_vectors.py": "a3fccaeadb9a5db72c33787a055a54374504a6aa231907080396b2cf822e94a7", + "scripts/audit_cancellation.py": "508934ee4d9514a5519813603b6192a0d53103b6e30d65b8d53a1a774de244b6", + "scripts/audit_fused_block.py": "2afb83ca8e5f193ca8a4c242becf267ad1d9dc2578ba238b820e98d5185f6288", + "scripts/audit_joint_frames.py": "3df8061392ce0ba42bbde8c02f2a30c8141145e70e9a48c18da73d3aafb14423", + "scripts/certify.py": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e", + "scripts/exclusion_circuit.py": "b253f9d7318becda1c1f3b24e2287ed44a9c27fcea00cf9d531afb950d0457a0", + "scripts/experiments/affine_vector_screens.py": "756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1", + "scripts/experiments/affine_vector_witnesses.json": "672a4318c48f5286ce088d34736c38957b7f662a5f753d440dbc638e7da5f62a", + "scripts/experiments/cube_core_family.py": "e58f1f4067bda2d4838343f42ec2505316f006561f0702e869847d88b85413a8", + "scripts/experiments/rank_product_core.py": "7a91c1188c5d42e864a5d2e42397b09c435b526ae4f4210c44bf615de488708e", + "scripts/experiments/single_intersection.py": "08ddae46e5621a5b4c525b504e67ae655abe9b49461d894feaa7abc89a51847d", + "scripts/paired_exclusion_circuit.py": "8f05f04cf06217befd6d0ee0f2d7d0c5c5eb32cfab8c9a8ca7917fd6d620b7d2", + "scripts/paired_network.py": "991223dc3c1374284c361ed017e42bf732dd971fa0bea2be2282cfb18257b3f7", + "scripts/prepare_layers.py": "a6e2adc612f264b1c0e51d18ce6315de9ae5e2ae2420aa22e99a22d8bf304947", + "scripts/rational_tensor.py": "629b3f00a1aaab32fe908a73ca8f8412918209a300e6b1e5afe6325b9cfed3c3", + "scripts/search_network.py": "3a4faa5037d9b8e7ca5828afac193a96b6966a8b114f14937921795b24ec4f6a", + "scripts/shared_point_circuit.py": "c9bb7a5df92d260a4e3ad532b53e26936730d7c93f7facfb0784957c1e81c8ba", + "scripts/shared_point_network.py": "a85e7f0d8c42d6a27e3846308571ca324a1824ac5c2d59e4daa5c7673c33c697", + "tests/test_affine_vector_screens.py": "ab2c301c10a28438ac3d45a7e052e453b87a1f8057ce3ea897b14573f99f8bed", + "upstream/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "upstream/README.md": "8d1ceff898a4e0e681679f91c4def485820be9e99f04e4861f2ce601a364723e", + "upstream/build/figures/multiplication-flow.tex": "3654d2728b0c98919d61760e1802804ed616546a747f9167a93e17bb8697f320", + "upstream/build/figures/proof-map.tex": "76d4deacf07bea355412abcfd798c7cbe6dcccef29a4a420a9e2a7b158f23848", + "upstream/build/main.tex": "42f0f506976bc2084374a71e97edc1549689a7accf35dda4db2a18af4f13c1aa", + "upstream/build/references.bib": "33cc2df13ccf85330849e8fb34d4ac7613b23f625787457a5b7b9aa6d7369476", + "upstream/build/sections/00-introduction.tex": "98721f03682ccf1cc7d0850b07adabaa2d8f3afe552e3861753eba9d284d0da0", + "upstream/build/sections/01-history.tex": "798956c8150c31e3e2f5f29c47110d25ce619faad1374f4d3a0f15fa3ee33ead", + "upstream/build/sections/02-streams.tex": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab", + "upstream/build/sections/03-motifs.tex": "ed76761194988a01af77ead0ea6469cb5dcd29690ab985a0b5a4006b0f2b69bb", + "upstream/build/sections/04-swap.tex": "412b170ccaab38dba96e95e3cbfae09f4876a9818f8d278776a746b0f8044906", + "upstream/build/sections/05-layers.tex": "20cfc8d12099d4e4ed9e3e7eeb6162edd9b6e0e076f24693364cd24377252594", + "upstream/build/sections/06-transforms.tex": "924316e4bc905066281d8f9e8746a49d8829aeb393688608deb1e61c3c87853c", + "upstream/build/sections/07-resampling.tex": "8a6b91670f9163afb54892489fa2210c77fe1b058f0325ec7d18b44b94be6e2c", + "upstream/build/sections/08-assembly.tex": "763d7945b1e1ec4ebae9b799bcefcc45fa9bae6e2ffad799868a9c3d513dbd4a", + "upstream/build/sections/09-exact-arithmetic.tex": "5714e5d0656c78c6a1fde8d01fd11f1ba856a7ea94149b283bd9a50fdbf516c3", + "upstream/build/sections/10-transposition.tex": "c14ad8d56112f6578678a58211bc8d63c3a4b60e55078ac73bc38f7348e713cb", + "upstream/build/sections/11-grouped-rectangles.tex": "6525cd0a01980e56accfeaf06e9d875bc699197ba42c6e22b69435e352275174", + "upstream/formalization.yaml": "2dcbd0d6e6a22475f53d49bfdfcac9b6d2b470653c332a9f56522f5be166edb9", + "upstream/manifest.json": "16ab13971694cabab09440c47ebf2fc0496a9d35fc3af33950fda3498f8e2392" + } +} diff --git a/research/leech-minor-byte-lanes/README.md b/research/leech-minor-byte-lanes/README.md new file mode 100644 index 0000000000..f6f50385e8 --- /dev/null +++ b/research/leech-minor-byte-lanes/README.md @@ -0,0 +1,141 @@ +# Exact byte lanes for historical Leech minors + +**Verification tooling; no new kappa or new negative result.** This opt-in +adapter accelerates the five Leech minors in the historical affine-vector +audit. It reconstructs every recorded matrix entry and retains the original +Golay inventory, vector norms, rational spans, exact binary elimination, +admission checks and nine-screen certificate. The other four polynomial-code +screens run unchanged. The original checker and its default command remain +available. + +Reproduce with standard-library Python 3.11+ from the repository: + +```sh +python3 -I -B research/leech-minor-byte-lanes/verify.py +python3 -I -B research/leech-minor-byte-lanes/test_lanes.py -v +``` + +The first command compares **5,927 complete rows / 7,531,037 matrix entries** +against the pinned pairwise implementation, compares both full certificates +byte for byte with the committed certificate, and checks `EXPECTED.json`. +Its final line is: + +```text +PASS_LEECH_BYTE_LANES all_frozen_rows_equal=true cases=5 +``` + +To use just the accelerator, provide a fresh output path: + +```sh +python3 -I -B research/leech-minor-byte-lanes/replay.py --output /tmp/leech-certificate.json +``` + +The output is the complete original certificate; the stdout receipt explicitly +identifies the executed geometry source. The certificate's original source +hashes still refer to the unchanged files on disk. They do **not** identify the +adapter: `EXPECTED.json` pins the transformed geometry, while `BENCHMARK.json` +records hashes of the adapter, wrapper, benchmark and input pin manifest. +Neither entry point overwrites an existing output file. Optimized Python is +rejected so no inherited assertion can be disabled. + +## Exact arithmetic + +Let columns be vectors `v_j` with coordinates in `[-4,4]`. For each coordinate +`k`, pack two nonnegative base-256 integers, with column `j` in byte `j`: + +``` +P_k = sum_j (v_j[k] + 4) 256^j +M_k = sum_j (4 - v_j[k]) 256^j +``` + +For a row vector `u`, calculate + +``` +S_u = sum_(u[k]>0) u[k] P_k + sum_(u[k]<0) (-u[k]) M_k. +``` + +Byte `j` is exactly `dot(u,v_j) + 4 ||u||_1`. Every summand is nonnegative and +the final byte is at most `8 ||u||_1`. The adapter admits only `||u||_1 <= 31`, +giving a bound of 248, strictly below 256; every partial sum also fits. There +are no carries between columns and no signed borrowing. Original Leech rows +have l1 norms 8, 16 or 26, so this bound includes every allowed historical row. + +The adapter decodes all bytes, compares each with `shift + 4 ||u||_1`, and +explicitly includes the diagonal. Thus it returns precisely +`C[i,j] = (i == j or dot(v_i,v_j) == shift)`, in the original column order. +No floating-point arithmetic, modular-rank surrogate, sampled comparison, +zero-byte bit trick or omitted row is used. Invalid lane domains fail before +packing. The extra packed coordinate arrays occupy approximately `48 * m` +bytes of integer payload for an `m`-column, 24-coordinate sample, plus Python +object overhead; the existing vector inventory and binary rows are retained. + +## Source admission and coverage + +Base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. `PINS.json` records SHA256 +for all 41 consumed predecessor sources, fixtures, expected certificate, +original tests, historical note and retained upstream inputs. The geometry +source has SHA256 +`756778eeca27f490adc7354a122dc50c40375156259991469c47a90949118ea1`. +The wrapper checks the pins before importing the audit. It requires one exact +match for the old row-construction block and replaces only that block in a +separate namespace. The original functions outside that block and all caller +checks remain. The alternative cannot silently activate after source drift. + +| Shift | Signed family | Rows | Columns | +| ---: | :---: | ---: | ---: | +| 0 | no | 683 | 715 | +| -16 | yes | 1,311 | 1,343 | +| -8 | yes | 1,311 | 1,343 | +| 8 | yes | 1,311 | 1,343 | +| 16 | yes | 1,311 | 1,343 | + +All row hashes remain unchanged. The full certificate SHA256 is +`f72787ebf4a991e32705c7fb7ef7ad559a9964b27c0f91d1b5a034c05027cfb0`. + +Supplemental controls use assignment seed **86** and cover all 81 two-coordinate +vectors in `[-4,4]^2` for every integer shift from -32 through 32; 192 shuffled +signed Leech vectors from all three generator families at seven shifts; zero +lanes, the maximum admitted lane, and mandatory diagonals. Controls detect +wrong signs, wrong shifts, omitted diagonals, reversed columns, dependent +rows, faulty-kernel output, invalid inputs, changed or missing pinned files, +incomplete receipts, disabled assertions and attempted output reuse. Column +reversal demonstrates why a matching rank alone is insufficient. The three +unchanged predecessor tests are also run against both implementations. + +## Benchmark + +Run the same complete nine-screen audit in alternating fresh processes: + +```sh +python3 -I -B research/leech-minor-byte-lanes/benchmark.py --rounds 3 --output /tmp/leech-benchmark.json +``` + +Every timed process includes interpreter startup, imports, source admission, +all nine witnesses and their checks, exact complete-certificate comparison and +output. The runner checks every resulting file again. Timing is descriptive; +no speed threshold controls mathematical acceptance. Raw measurements and +the tested adapter hashes are retained in `BENCHMARK.json`. + +The initial instrumented profile attributed 42.3 of 49.7 seconds to Leech +minor replay. Instrumented figures are diagnostic, not benchmark samples. A +preliminary timing run overlapped supplemental testing and is excluded from +the retained comparison. See `VALIDATION.md` for final measurements and limits. + +## Mathematical scope and credit + +These are the same five specified central matrices rejected by Douglas R. +Colkitt's historical audit, and the same four polynomial-code screens. The +rank lower bounds rule out positive deficit only for those stated full +relations in the historical compiler. This does not reopen the search, +exclude arbitrary supported matrices or subfamilies, improve a supplier, or +raise the selected conditional kappa. The selected #799/#589 result remains +0.001661634653669567 with its inherited all-size, realization, hosting, +precision/tape and analytic assumptions. This is finite verification, not a +formal proof of the multiplication theorem. + +Credit and immutable predecessor pins are in `NOTICE.md`; selection and overlap +checks are in `CLAIM.md`. The technique follows the related integer-lane idea +of Curtis Dransfield's #752, here applied to signed real Leech minors with +direct byte decoding. No pending PR code is imported. This package is by +Jerry Chen (@CubeJerry), with substantial OpenAI Codex assistance, under +Apache-2.0. No independent human review is claimed. diff --git a/research/leech-minor-byte-lanes/VALIDATION.md b/research/leech-minor-byte-lanes/VALIDATION.md new file mode 100644 index 0000000000..0c61a89691 --- /dev/null +++ b/research/leech-minor-byte-lanes/VALIDATION.md @@ -0,0 +1,76 @@ +# Validation receipt + +2026-10-13, Linux x86_64, CPython 3.12.14. Base: +`f567884aeb8851b6e794af1184119a3bfbe1e631`. All consumed predecessor files +are pinned in `PINS.json`; all benchmarked implementation hashes are recorded +in `BENCHMARK.json`. + +## Exact comparison and controls + +- Full differential replay: **5,927 rows / 7,531,037 entries**, all five Leech + fixtures, all equal. Both complete nine-screen certificates are byte-identical + to `certificates/affine-vector-screens.json`; `EXPECTED.json` retains the + per-case row hashes and geometry source hashes. +- `python3 -I -B research/leech-minor-byte-lanes/test_lanes.py -v`: + **11 test groups pass**, including the **three unchanged predecessor tests + in each of the two modes**. The retained run took 9.884 seconds; this test + runtime is not an accelerator benchmark. +- Literal integer oracles compare every entry for 81 small vectors at 65 + shifts (426,465 comparisons), and 192 signed Leech vectors at seven shifts + (258,048 comparisons). They include all three vector families, mandatory + diagonals, extremal byte values and assignment seed 86. +- Controls detect sign/shift errors, missing diagonals, column permutation + despite equal rank, dependent rows, zero-output kernels, malformed lane + domains, changed source/fixture/certificate/rank-helper bytes, missing input, + missing case or changed count in the expected receipt, disabled assertions + and reused output paths. They do not authenticate arbitrary hostile runtime + modifications or prove the full multiplication theorem. +- Selected-record integrity passes with kappa + `1661634653669567/1000000000000000000`; all **five** tests in + `tests/test_selected_result.py` pass. + +## Timing + +The final command was: + +```sh +python3 -I -B research/leech-minor-byte-lanes/benchmark.py --rounds 3 --output /tmp/seed86-benchmark-final.json +``` + +The resulting file is retained as `BENCHMARK.json`. The process order was +baseline/lanes, lanes/baseline, baseline/lanes. No other test or benchmark from +this task ran concurrently during this final comparison. System-wide resource +contention on the shared runner was not controlled. + +| Pair | Baseline seconds | Byte-lane seconds | +| ---: | ---: | ---: | +| 1 | 17.051406 | 8.988220 | +| 2 | 18.946560 | 7.536546 | +| 3 | 22.677771 | 14.988176 | +| Median | **18.946560** | **8.988220** | + +Ratio of medians: **2.107932×**. Each process replays the same full nine-screen +audit, including the unchanged four polynomial-code screens, source admission, +all original checks, complete certificate comparison and writing the result. +The parent compares each file again. All six certificates are identical. +This is not a whole-repository or selected-supplier runtime claim. The sample +variation is retained; timing is never an acceptance threshold. + +An earlier profile and exploratory three-pair run are excluded. The profile +added instrumentation overhead; the exploratory run overlapped supplemental +tests. No favorable subset of the final samples was selected. + +## Portability and limits + +The minimal dependency closure (41 pinned predecessor files plus this package +and repository license/notices) was copied to a fresh directory whose path +contains spaces. The complete differential verifier was invoked with `-I -B` +from `/tmp`, outside the checkout. It passed, and every copied input byte and +the file inventory remained unchanged. The relocation log is retained in +`validation/relocation.log`. + +Original sources, default entry points, the selected frontier and `upstream/` +are unchanged. This optional adapter has no Makefile or CI activation. Full +`make verify`, cold selected-supplier replay, Lean and hosted CI were not run +or claimed. The relevant local checks above cover the new package; they do +not establish inherited all-size or analytic hypotheses. diff --git a/research/leech-minor-byte-lanes/benchmark.py b/research/leech-minor-byte-lanes/benchmark.py new file mode 100644 index 0000000000..0d8993d44c --- /dev/null +++ b/research/leech-minor-byte-lanes/benchmark.py @@ -0,0 +1,63 @@ +#!/usr/bin/env python3 +"""Alternating fresh-process timings, including complete certificate checking.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import tempfile +import time + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from replay import ROOT, check_pins, require + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--rounds', type=int, default=3) + parser.add_argument('--output', type=Path, required=True) + args = parser.parse_args() + require(not sys.flags.optimize, 'Assertions must remain enabled') + require(args.rounds >= 1, 'At least one timing pair required') + require(not args.output.exists(), 'Output already exists') + pins = check_pins() + samples = [] + expected = (ROOT / 'certificates/affine-vector-screens.json').read_bytes() + with tempfile.TemporaryDirectory(prefix='leech-lanes-') as temporary: + for round_index in range(args.rounds): + modes = ('baseline', 'lanes') if round_index % 2 == 0 else ('lanes', 'baseline') + for mode in modes: + output = Path(temporary) / f'{round_index}-{mode}.json' + command = [sys.executable, '-I', '-B', str(HERE / 'replay.py'), + '--mode', mode, '--output', str(output)] + started = time.perf_counter() + process = subprocess.run(command, text=True, capture_output=True, check=True) + seconds = time.perf_counter() - started + require(output.read_bytes() == expected, 'Timed certificate changed') + receipt = json.loads(process.stdout) + require(receipt['status'] == 'PASS_AFFINE_VECTOR_REPLAY', 'Missing replay success') + samples.append({'round': round_index + 1, 'mode': mode, + 'wall_seconds': seconds, 'receipt': receipt}) + print(f'{mode} round {round_index + 1}: {seconds:.6f}s', flush=True) + medians = {mode: statistics.median(s['wall_seconds'] for s in samples if s['mode'] == mode) + for mode in ('baseline', 'lanes')} + result = {'status': 'PASS_IDENTICAL_COMPLETE_CERTIFICATES', + 'base_commit': pins['base_commit'], 'python': sys.version, + 'platform': platform.platform(), 'machine': platform.machine(), + 'samples': samples, 'median_wall_seconds': medians, + 'median_speedup': medians['baseline'] / medians['lanes'], + 'certificate_sha256': sha256(expected).hexdigest(), + 'adapter_sha256': {name: sha256((HERE / name).read_bytes()).hexdigest() + for name in ('lanes.py', 'replay.py', 'benchmark.py', 'PINS.json')}, + 'scope': 'Complete nine-screen historical affine-vector audit; process startup, source admission, all checks and output included. No timing threshold.'} + with args.output.open('x') as out: + out.write(json.dumps(result, indent=2, sort_keys=True) + '\n') + print(result['status'], f"median_speedup={result['median_speedup']:.3f}") + + +if __name__ == '__main__': + main() diff --git a/research/leech-minor-byte-lanes/lanes.py b/research/leech-minor-byte-lanes/lanes.py new file mode 100644 index 0000000000..095173fba9 --- /dev/null +++ b/research/leech-minor-byte-lanes/lanes.py @@ -0,0 +1,45 @@ +"""Exact signed dot-product rows for the historical Leech minors. + +CubeJerry, with substantial OpenAI Codex assistance. Apache-2.0. +See README.md for the no-carry argument and predecessor credit. +""" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def lane_rows(sample, indices, shift): + """Return C[i,j] = (i == j or dot(sample[i], sample[j]) == shift). + + Each coordinate lies in [-4, 4]. Each selected row has l1 norm <= 31, + so every accumulated base-256 digit is at most 8*31 < 256. This holds + for every signed Leech vector (actual l1 norms: 8, 16, 26). + """ + require(sample and sample[0], 'Empty sample') + dimension = len(sample[0]) + require(all(len(v) == dimension and + all(type(x) is int and -4 <= x <= 4 for x in v) + for v in sample), 'Invalid byte-lane coordinates') + require(indices and len(set(indices)) == len(indices) and + all(type(i) is int and 0 <= i < len(sample) for i in indices), + 'Invalid selected rows') + require(type(shift) is int, 'Integer shift required') + require(all(sum(abs(x) for x in sample[i]) <= 31 for i in indices), + 'Byte-lane carry bound exceeded') + + plus = [int.from_bytes(bytes(v[k] + 4 for v in sample), 'little') + for k in range(dimension)] + minus = [int.from_bytes(bytes(4 - v[k] for v in sample), 'little') + for k in range(dimension)] + rows = [] + for i in indices: + u = sample[i] + offset = 4 * sum(abs(x) for x in u) + packed = sum(x * plus[k] if x > 0 else -x * minus[k] + for k, x in enumerate(u) if x) + values = packed.to_bytes(len(sample), 'little') + rows.append(sum(1 << j for j, value in enumerate(values) + if i == j or value == shift + offset)) + return rows diff --git a/research/leech-minor-byte-lanes/replay.py b/research/leech-minor-byte-lanes/replay.py new file mode 100644 index 0000000000..4ec31707d8 --- /dev/null +++ b/research/leech-minor-byte-lanes/replay.py @@ -0,0 +1,97 @@ +#!/usr/bin/env python3 +"""Opt-in, source-pinned replay of all nine historical affine-vector screens.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from lanes import lane_rows, require + +SOURCE = 'scripts/experiments/affine_vector_screens.py' +OLD = ''' packed=[];digest=sha256() + for i in independent_rows: + sparse=[(a,x) for a,x in enumerate(sample[i]) if x] + row=sum(1<