Skip to content

Research audit: literal binary spectra and moment-preserving corruption control (no new kappa) - #812

Merged
Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
ljste:audit/single-intersection-spectrum-seed65
Oct 13, 2026
Merged

Mister-Meeseeks merged 1 commit into
CrocSwap:mainfrom
ljste:audit/single-intersection-spectrum-seed65

Conversation

@ljste

@ljste ljste commented Oct 13, 2026

Copy link
Copy Markdown
Contributor

The historical single-intersection screen checks two integer spectral moments, but those checks can miss a wrong modular characteristic polynomial. This research audit adds an independent exact calculation from literal subset-intersection matrices. No new kappa is claimed.

All 41 cases with 4 <= h <= 10, 2 <= k <= min(4, floor(h/2)), and 0 <= j < k match the claimed binary polynomial and rank lower bound. The largest matrix has order 210. The bound is strict in 21 cases, so the evidence preserves the distinction between a lower bound and a binary diagonalization.

The useful negative control is a two-edge switch at (h,k,j)=(7,3,0): it preserves every row degree, integer trace 35 and squared trace 175, but changes the characteristic polynomial. The independent audit rejects it. A complementary-subset nilpotent example and a wrong odd-multiplicity control document the other failure boundaries.

Reproduce from the repository root with standard-library Python:

python3 -B research/single-intersection-spectrum-audit/spectrum_audit.py

Expected: PASS_LITERAL_BINARY_SPECTRAL_AUDIT, completed_cases: 41. The command checks pinned source bytes, recomputes every case and both rejection controls, and compares the complete result with the committed certificate. The README gives the matrix-similarity argument, polynomial recurrence, exact domain, stopping rule, dependencies and limits.

Validation passed on Python 3.14.6: 559 tests in 85 isolated repository modules and all 20 historical patch checks, 10 focused tests normally and under -O, standalone audit under -S and -O, selected-record integrity, and mypy on both new Python files. The determinant engine is compared with direct Leibniz expansion on all 512 binary 3-by-3 matrices and 48 seeded matrices of orders 4,5,6; ranks are checked independently by exhaustive kernel enumeration. Full make verify, the selected supplier cold replay and Lean were not rerun for this isolated audit.

Exact base: 66849e1475c930fd7732b1a0067ffee7e1e95f60. OS-random assignment seed 65, adversarial mathematical audit. Three narrow candidates and the local claim are retained in SOURCE.json; no pinned sprint coordination issue existed. Final overlap metadata was refreshed through PR #811. #778 (merramil, head f015b04c74801fa330f818d178e809c760fb5469) checks large orbit Gram packing in the same family; this adds the distinct modular characteristic-polynomial obligation and moment-preserving corruption control, without importing its code.

Credit Douglas R. Colkitt's historical screen and the Johnson-spectrum sources cited in the README. Contribution by Lucas Steinmetz (ljste), with substantial OpenAI Codex assistance, under the repository's Apache-2.0 license. This is finite verification evidence, not a formal proof of the all-size spectral formula or multiplication theorem. The selected frontier, inherited construction assumptions and upstream/ are unchanged.

@Mister-Meeseeks
Mister-Meeseeks merged commit 9a16422 into CrocSwap:main Oct 13, 2026
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants