Repository navigation
Tooling: 2.09x faster exact single-intersection Gram replay - #778
Merged
Mister-Meeseeks merged 1 commit intoOct 14, 2026
Merged
Conversation
Contributor
|
100-PR batch review at Merged to Reviewed scope: Symmetric byte-packed Gram construction: same complete integer rows and certificates; focused independent differential tests, memory tradeoff remains disclosed. The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions. Batch review, attribution and evidence. Thank you for the contribution. |
Mister-Meeseeks
pushed a commit
that referenced
this pull request
Oct 14, 2026
The spectrum audit (#812) pins scripts/experiments/single_intersection.py by whole-file SHA-256 at its pre-#778 digest. #778 (f015b04) rewrote only minor_rows, which the audit never calls (it imports spectral_parity_bound, byte-identical), and the old and new minor_rows agree on all 41 audit cases. With the pin bypassed, a fresh certificate equals the committed RESULT.json in every field. Refresh the pin in SOURCE.json and regenerate RESULT.json with the audit's own --write (one line). This makes the `tests` group of Verify research artifacts pass again on main.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The historical single-intersection audit spends most of its runtime constructing exact binary Gram matrices. This replaces repeated large-integer sums with symmetric byte packing, preserving every matrix entry and every basis, closure, rank, and rejection check. Tooling improvement; no new κ.
Three alternating fresh-process pairs on CPython 3.13.1 / macOS arm64 measured median complete-audit time 13.766 → 6.597 seconds (2.087× faster). Median peak process RSS rises from 49,266,688 to 68,845,568 bytes (about 40%); this is an explicit speed/memory tradeoff. Every sample and source pin is retained in
research/single-intersection-packing/RESULT.json.Validation:
-O, including source corruption, changed certificate ranks/rows/bindings, a wrong matrix entry, malformed labels, dependent bases, missing closure, byte boundaries, permutations, and large labels.single-intersection.jsonandaffine-vector-screens.jsonchange only their implementation-source hashes; complete predecessor-certificate equivalence is regression-tested.PYTHONDONTWRITEBYTECODE=1 make verify-tests: 557 tests in 86 isolated modules and 20 patch checks pass. Selected-record integrity and whitespace checks also pass.Reproduce with standard-library Python 3.11+ on macOS or Linux, using a fresh output path:
Expected:
PASS_IDENTICAL_GRAM_ROWS_AND_COMPLETE_CERTIFICATES. Timing is descriptive, not a pass threshold. The engineering note atdocs/research/single-intersection-packing.mdexplains the packing identity, complete coverage, measured tradeoff, and commands.Base:
66849e1475c930fd7732b1a0067ffee7e1e95f60. OS-random seed 86, verification engineering. Candidates were gather schedules, coded-carry controls, and single-intersection replay; seed 86 mod 3 selected the latter. Profiling justified narrowing the initial feature-reuse hypothesis to Gram construction. There was no sprint coordination issue, so the claim is local. Overlap checks covered 594 open PRs through #775; #707 concerns R420 determinant prefixes and #756 balanced-Fano search. Neither supplies code here.Credit Douglas R. Colkitt's preserved single-intersection audit and its cited mathematical sources. Contribution by merramil with substantial OpenAI Codex assistance, under Apache-2.0;
NOTICE.mdidentifies the exact predecessor and source hash.upstream/and the selected frontier are unchanged. Fullmake verify, selected-supplier cold replay, and Lean were not rerun for this historical-checker change. All inherited construction, compiler, hosting, precision, tape, and analytic assumptions remain. This is finite verification tooling, not a formal proof of the multiplication theorem.