diff --git a/research/single-intersection-spectrum-audit/README.md b/research/single-intersection-spectrum-audit/README.md new file mode 100644 index 0000000000..0585e2cbbb --- /dev/null +++ b/research/single-intersection-spectrum-audit/README.md @@ -0,0 +1,163 @@ +# Literal audit of the single-intersection spectral rank bound + +**Adversarial mathematical audit, no new kappa.** All 41 specified literal +matrices agree with the historical modular characteristic polynomial and +binary rank lower bound. The audit finds no counterexample to that bound. +It adds an independent polynomial calculation and a corruption control that +preserves both integer moments already checked by the historical routine. + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. The selected conditional +certificate at this base is #626 with #543, +`kappa = 51110230636731/31250000000000000 = 0.001635527380375392`. +This historical-family audit does not alter that construction or certificate. + +## Exact statement audited + +The object is `spectral_parity_bound` in +[`scripts/experiments/single_intersection.py`](../../scripts/experiments/single_intersection.py) +and the characteristic-polynomial deduction in +[`docs/research/single-intersection.md`](../../docs/research/single-intersection.md). +For all k-subsets S,T of an h-point set, define the integer matrix + +```text +C[S,T] = 1 if S=T or |S intersection T|=j, otherwise 0. +``` + +Let n be its order and o the total rational multiplicity of odd integer +Johnson eigenvalues. The historical claim is + +```text +det(xI-C) mod 2 = x^(n-o) (x+1)^o, +rank over F2 of C >= o. +``` + +Reducing the integer determinant polynomial commutes with reduction of its +entries. The algebraic multiplicity of zero bounds its geometric multiplicity, +so binary nullity is at most n-o. This proves the implication from the +polynomial identity to the rank lower bound without reducing a rational +eigenbasis modulo two. The rational eigenvalue formula is inherited from +Ghareghani, Ghorbani and Mohammad-Noori, +[*Intersection matrices revisited*, Lemma 8 and Theorem 9](https://arxiv.org/html/0902.4367v4#S5.SS2). +This audit does not reprove that all-size formula by finite enumeration. + +## Independent calculation and completed coverage + +OS randomness produced assignment seed 65, selecting mathematical audit. +Three candidate tasks were the prime-power subset ceiling, Fano permutation +rigidity, and this spectral bound. `65 mod 3 = 2` selected the latter. +The seed sets the upper ground size to `9 + 65 mod 2 = 10` and upper subset +size to `2 + 65 mod 3 = 4`. Complete coverage is + +```text +4 <= h <= 10, +2 <= k <= min(4, floor(h/2)), +0 <= j < k. +``` + +The stopping rule is completion of these 41 cases once, with no expansion +to the large historical orbit fixtures. The largest matrix has order 210. +This is a complete finite audit of that domain, not a search for a supplier. + +`spectrum_audit.py` constructs entries from literal set intersections. It +does not call the existing incidence-factor, orbit-Gram, packed-row or rank +helpers. Its characteristic-polynomial engine applies simultaneous row/column +permutations and elementary similarities to obtain an upper Hessenberg matrix H. +Over F2, adding row r to row i and then column i to column r conjugates by +`E = I + e_(i,r)`, whose inverse is E. The implementation checks that all +entries below the first subdiagonal have vanished. + +For the leading i-by-i block, let p_i be its characteristic polynomial and +p_0=1. Expansion along the last column gives, in characteristic two, + +```text +p_i = (x + H[i-1,i-1]) p_(i-1) + + sum_(a=0)^(i-2) H[a,i-1] + product_(b=a+1)^(i-1) H[b,b-1] p_a. +``` + +The recurrence uses polynomial coefficient bits and no Johnson eigenvalues. +The legacy spectral routine supplies only the value o for comparison. +An independent ascending-column elimination computes the binary rank. +Each case records the full polynomial, literal-row hash, exact rank and rank +of C squared. A polynomial bit at position d is the coefficient of x^d; +`characteristic_polynomial_hex` records all coefficients, including zero ones. + +All 41 polynomials match, and all 41 lower bounds hold. In 21 cases the lower +bound is strict. These are observations in the fixed domain, not a formula +for binary ranks outside it. + +## Negative controls and the nonsemisimple boundary + +For `(h,k,j)=(7,3,0)`, n=35 and o=15. Its literal polynomial is +`0xffff00000`, equivalently `x^20 (x+1)^15`; its binary rank is 21. +In the lexicographic subset order, remove undirected edges `(0,32)` and +`(1,28)` and add `(0,1)` and `(28,32)`. + +This switch preserves symmetry, every diagonal entry and every row degree. +Both original and corrupted matrices therefore have integer trace 35 and +integer squared trace 175. The changed polynomial is `0xfccc30000`. +The new polynomial comparison rejects it even though both historical integer +moment checks would still pass. This is deliberately corrupted input, not a +counterexample within the subset family. Changing the claimed odd multiplicity +from 15 to 16 is rejected separately. + +For `(4,2,0)`, the matrix is three complementary-subset pairs, each with block +`[[1,1],[1,1]]`. Over F2 its polynomial is `x^6`, its square is zero, and its +rank is 3 while o=0. Thus **rank=o is false**, although the actual historical +lower bound remains valid. More generally, at h=2k,j=0, complement pairs give +these same blocks, so rank is `binom(2k,k)/2` and the square is zero. The tests +replay k=2,3,4,5. This elementary family corroborates the existing identity-minor +bound; it is not claimed as a new rank theorem or compiler exclusion. + +The engine controls compare characteristic polynomials with a separate direct +Leibniz determinant for all 512 binary 3-by-3 matrices and 48 seeded arbitrary +matrices of orders 4,5,6. Rank is checked against exhaustive kernel enumeration +on those same matrices. Further controls cover permutation similarity, +transpose, invalid matrix shapes, corrupted source pins and a corrupted +committed polynomial. These finite checks support the implementation and do +not formally verify it for every matrix order. + +## Reproduction, pins and scope + +From the repository root, using standard-library Python 3.11 or later: + +```sh +python3 -B research/single-intersection-spectrum-audit/spectrum_audit.py +``` + +Expected: `PASS_LITERAL_BINARY_SPECTRAL_AUDIT` with `completed_cases: 41`. +The command verifies exact dependency hashes, recomputes every case, runs both +rejection controls, and compares the entire fresh result to `RESULT.json`. +It also passes under `-S` and `-O`. `--write` regenerates only this package's +result. Focused tests: + +```sh +python3 -B -m unittest discover -s tests -p test_single_intersection_spectrum_audit.py -v +``` + +`SOURCE.json` pins the actual predecessor bytes, selected record and local +claim. The last predecessor change to the spectral source was +`d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0`. There is no solver, compiled library +or floating-point dependency. No provider, paid cost recurrence, Gaussian +assembly parameter, tape implementation or selected-frontier replay is changed. +The compiler, side representation and all-size multiplication obligations +remain those of the inherited construction. + +## Attribution and overlap + +Contribution: Lucas Steinmetz (`ljste`), with substantial OpenAI Codex +assistance in task selection, mathematical analysis, implementation and writing. +No independent human review or formal verification is claimed. Apache-2.0, +following the repository license. + +The historical screen and its source are Douglas R. Colkitt's work. The Johnson +spectrum is credited to the paper above and its cited predecessors. The selected +construction retains the contributors credited in the maintainer review; this +audit supplies neither that construction nor a stronger conditional exponent. + +PR #778, by `merramil`, independently addresses packing and replay of the +same historical family's large orbit Gram matrices. Its inspected head is +`f015b04c74801fa330f818d178e809c760fb5469`. This audit adds a different obligation: +literal modular characteristic polynomials and a moment-preserving corruption +control. It neither depends on nor imports #778's code. No pinned sprint issue +existed, so the claim is recorded locally in `SOURCE.json`. diff --git a/research/single-intersection-spectrum-audit/RESULT.json b/research/single-intersection-spectrum-audit/RESULT.json new file mode 100644 index 0000000000..31a5aab9d7 --- /dev/null +++ b/research/single-intersection-spectrum-audit/RESULT.json @@ -0,0 +1,570 @@ +{ + "assignment_seed": 65, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "cases": [ + { + "binary_rank": 3, + "characteristic_polynomial_hex": "0x40", + "h": 4, + "j": 0, + "k": 2, + "odd_eigenvalue_multiplicity": 0, + "order": 6, + "rank_gap": 3, + "rows_sha256": "8c829403fae7fc5d36d3b0fda7cce04a319d44d510b6c2a2ca1424e11215e472", + "squared_binary_rank": 0 + }, + { + "binary_rank": 6, + "characteristic_polynomial_hex": "0x55", + "h": 4, + "j": 1, + "k": 2, + "odd_eigenvalue_multiplicity": 6, + "order": 6, + "rank_gap": 0, + "rows_sha256": "4b38b97b4ae8d1bc51cf21c8b3f92c7fb44d2914d99c6e6341ac6fef9de53a9a", + "squared_binary_rank": 6 + }, + { + "binary_rank": 5, + "characteristic_polynomial_hex": "0x440", + "h": 5, + "j": 0, + "k": 2, + "odd_eigenvalue_multiplicity": 4, + "order": 10, + "rank_gap": 1, + "rows_sha256": "82d011338ecae7baa01cbb084dd00f066eef9b007fe68c1ec4b8367b89982f8b", + "squared_binary_rank": 4 + }, + { + "binary_rank": 6, + "characteristic_polynomial_hex": "0x550", + "h": 5, + "j": 1, + "k": 2, + "odd_eigenvalue_multiplicity": 6, + "order": 10, + "rank_gap": 0, + "rows_sha256": "84e0bf595d88a2ecd32ddcebd7f69f4a8de75eb82f8bf119785f3c24242ba3da", + "squared_binary_rank": 6 + }, + { + "binary_rank": 5, + "characteristic_polynomial_hex": "0xc000", + "h": 6, + "j": 0, + "k": 2, + "odd_eigenvalue_multiplicity": 1, + "order": 15, + "rank_gap": 4, + "rows_sha256": "96a823e43b9b8c61221b432f6820df18ff500cf30dfd5e616af9ba1eef63d133", + "squared_binary_rank": 1 + }, + { + "binary_rank": 15, + "characteristic_polynomial_hex": "0xffff", + "h": 6, + "j": 1, + "k": 2, + "odd_eigenvalue_multiplicity": 15, + "order": 15, + "rank_gap": 0, + "rows_sha256": "0a0f662d2ff632b0541e5c91f14018fd5506b78324b7be09f083e8eb92f82331", + "squared_binary_rank": 15 + }, + { + "binary_rank": 10, + "characteristic_polynomial_hex": "0x100000", + "h": 6, + "j": 0, + "k": 3, + "odd_eigenvalue_multiplicity": 0, + "order": 20, + "rank_gap": 10, + "rows_sha256": "90e20eca67ace17a95136acfc479c44029246ce6d3015bc3782b847f35107bc4", + "squared_binary_rank": 0 + }, + { + "binary_rank": 6, + "characteristic_polynomial_hex": "0x100000", + "h": 6, + "j": 1, + "k": 3, + "odd_eigenvalue_multiplicity": 0, + "order": 20, + "rank_gap": 6, + "rows_sha256": "4d6d6ec1a2dc0f4ceab610e8256362b1ad0141b0aefb55e399bfb545a5ed6bf4", + "squared_binary_rank": 0 + }, + { + "binary_rank": 6, + "characteristic_polynomial_hex": "0x100000", + "h": 6, + "j": 2, + "k": 3, + "odd_eigenvalue_multiplicity": 0, + "order": 20, + "rank_gap": 6, + "rows_sha256": "0483fe5db56ded0a1dc2edd88810471671668a314bddc0b2a4e3b552c4e2b602", + "squared_binary_rank": 0 + }, + { + "binary_rank": 7, + "characteristic_polynomial_hex": "0x3fc000", + "h": 7, + "j": 0, + "k": 2, + "odd_eigenvalue_multiplicity": 7, + "order": 21, + "rank_gap": 0, + "rows_sha256": "9517762028a9fe642d4366b27b6fcc31110f84387185d154fd04d94337e43a39", + "squared_binary_rank": 7 + }, + { + "binary_rank": 15, + "characteristic_polynomial_hex": "0x3fffc0", + "h": 7, + "j": 1, + "k": 2, + "odd_eigenvalue_multiplicity": 15, + "order": 21, + "rank_gap": 0, + "rows_sha256": "91bb63cb28e5d0d590fb28cbef7c4e32e1b5fa5341747fc276a9493f54cff7f7", + "squared_binary_rank": 15 + }, + { + "binary_rank": 21, + "characteristic_polynomial_hex": "0xffff00000", + "h": 7, + "j": 0, + "k": 3, + "odd_eigenvalue_multiplicity": 15, + "order": 35, + "rank_gap": 6, + "rows_sha256": "a65008c6ff531ea724ab9f1491323d6b30da6d779630f6217d71cae442be8392", + "squared_binary_rank": 15 + }, + { + "binary_rank": 7, + "characteristic_polynomial_hex": "0xc00000000", + "h": 7, + "j": 1, + "k": 3, + "odd_eigenvalue_multiplicity": 1, + "order": 35, + "rank_gap": 6, + "rows_sha256": "9185aead357f6b275f7becbdc2250b364b132a8af2f974f8264088a612cd5fcf", + "squared_binary_rank": 1 + }, + { + "binary_rank": 15, + "characteristic_polynomial_hex": "0xffff00000", + "h": 7, + "j": 2, + "k": 3, + "odd_eigenvalue_multiplicity": 15, + "order": 35, + "rank_gap": 0, + "rows_sha256": "f61c0179d6c89fb1da4c7c181c77786952d4b2b8b91e72d561e22b0b8828ccc4", + "squared_binary_rank": 15 + }, + { + "binary_rank": 7, + "characteristic_polynomial_hex": "0x10000000", + "h": 8, + "j": 0, + "k": 2, + "odd_eigenvalue_multiplicity": 0, + "order": 28, + "rank_gap": 7, + "rows_sha256": "1e0e4935c7d5ed8dbb7f467b5c7035a7380d9c5569dcc34c410eae4c1487af4e", + "squared_binary_rank": 0 + }, + { + "binary_rank": 28, + "characteristic_polynomial_hex": "0x11111111", + "h": 8, + "j": 1, + "k": 2, + "odd_eigenvalue_multiplicity": 28, + "order": 28, + "rank_gap": 0, + "rows_sha256": "a17a1945776c4dba4fc8a447f7719659a60293fc33b75f7d5f6d6be682439e3a", + "squared_binary_rank": 28 + }, + { + "binary_rank": 22, + "characteristic_polynomial_hex": "0x101000000000000", + "h": 8, + "j": 0, + "k": 3, + "odd_eigenvalue_multiplicity": 8, + "order": 56, + "rank_gap": 14, + "rows_sha256": "191b5f72e513650770521bde0e8be4b86cc080f2d8daa763ee58765deeb9f576", + "squared_binary_rank": 8 + }, + { + "binary_rank": 8, + "characteristic_polynomial_hex": "0x101000000000000", + "h": 8, + "j": 1, + "k": 3, + "odd_eigenvalue_multiplicity": 8, + "order": 56, + "rank_gap": 0, + "rows_sha256": "ad3137517ded374f1640a9f9118a5524b042e55935e15b1debc7b07e864d3abd", + "squared_binary_rank": 8 + }, + { + "binary_rank": 15, + "characteristic_polynomial_hex": "0x100000000000000", + "h": 8, + "j": 2, + "k": 3, + "odd_eigenvalue_multiplicity": 0, + "order": 56, + "rank_gap": 15, + "rows_sha256": "1d18b2e2098c57ed5eb2cca8319a826a6536fb7b7a0c116b910c6fa9ffcfb69b", + "squared_binary_rank": 0 + }, + { + "binary_rank": 35, + "characteristic_polynomial_hex": "0x400000000000000000", + "h": 8, + "j": 0, + "k": 4, + "odd_eigenvalue_multiplicity": 0, + "order": 70, + "rank_gap": 35, + "rows_sha256": "63e020548637f7c25893a6bb34564d78a9a23cd8dcf2de6113391b6006dbe500", + "squared_binary_rank": 0 + }, + { + "binary_rank": 70, + "characteristic_polynomial_hex": "0x550000000000000055", + "h": 8, + "j": 1, + "k": 4, + "odd_eigenvalue_multiplicity": 70, + "order": 70, + "rank_gap": 0, + "rows_sha256": "40dc36fbeb75db74073ecf9640e5d5f05d5c34d65194c4f95095250c2cacd517", + "squared_binary_rank": 70 + }, + { + "binary_rank": 70, + "characteristic_polynomial_hex": "0x550000000000000055", + "h": 8, + "j": 2, + "k": 4, + "odd_eigenvalue_multiplicity": 70, + "order": 70, + "rank_gap": 0, + "rows_sha256": "32d5f64c62710314bf9ad3ef1009a8e49aa7c1fe83961be19ea89f0bea42756c", + "squared_binary_rank": 70 + }, + { + "binary_rank": 70, + "characteristic_polynomial_hex": "0x550000000000000055", + "h": 8, + "j": 3, + "k": 4, + "odd_eigenvalue_multiplicity": 70, + "order": 70, + "rank_gap": 0, + "rows_sha256": "1b22c237f65c5cb43a75614064c0721a6e89275e4379aaf33ad6d98b430d92c7", + "squared_binary_rank": 70 + }, + { + "binary_rank": 9, + "characteristic_polynomial_hex": "0x1010000000", + "h": 9, + "j": 0, + "k": 2, + "odd_eigenvalue_multiplicity": 8, + "order": 36, + "rank_gap": 1, + "rows_sha256": "3b85cd77f7157b017d76261b42237c061b03f51a42529cd726ee2baa0d03b554", + "squared_binary_rank": 8 + }, + { + "binary_rank": 28, + "characteristic_polynomial_hex": "0x1111111100", + "h": 9, + "j": 1, + "k": 2, + "odd_eigenvalue_multiplicity": 28, + "order": 36, + "rank_gap": 0, + "rows_sha256": "f74bc6060226bc944c6d060c4ebbe4ced930c42c3cf6302022d7a08ff4b9f6ea", + "squared_binary_rank": 28 + }, + { + "binary_rank": 36, + "characteristic_polynomial_hex": "0x1100000011000000000000", + "h": 9, + "j": 0, + "k": 3, + "odd_eigenvalue_multiplicity": 36, + "order": 84, + "rank_gap": 0, + "rows_sha256": "30ae6293704659a82899cf04ac4096b2d45b3422e3bc4d48d811690a7e98141d", + "squared_binary_rank": 36 + }, + { + "binary_rank": 9, + "characteristic_polynomial_hex": "0x1010000000000000000000", + "h": 9, + "j": 1, + "k": 3, + "odd_eigenvalue_multiplicity": 8, + "order": 84, + "rank_gap": 1, + "rows_sha256": "6d60fd5066d513ad14791bed19ca072ca1b6bd7e31c8747b02d367d11731d2d0", + "squared_binary_rank": 8 + }, + { + "binary_rank": 28, + "characteristic_polynomial_hex": "0x1111111100000000000000", + "h": 9, + "j": 2, + "k": 3, + "odd_eigenvalue_multiplicity": 28, + "order": 84, + "rank_gap": 0, + "rows_sha256": "2e8e549fc9ac3eb8c3c16baa83f6be4ed3a0a477f7032fa2eae6a9c1bf55317d", + "squared_binary_rank": 28 + }, + { + "binary_rank": 83, + "characteristic_polynomial_hex": "0x40404040404040400000000000000000", + "h": 9, + "j": 0, + "k": 4, + "odd_eigenvalue_multiplicity": 56, + "order": 126, + "rank_gap": 27, + "rows_sha256": "ee8f742667aa77269f18aec585e4b19b52c7021babe271d1ace31b99dc7b784b", + "squared_binary_rank": 56 + }, + { + "binary_rank": 78, + "characteristic_polynomial_hex": "0x55550000000000005555000000000000", + "h": 9, + "j": 1, + "k": 4, + "odd_eigenvalue_multiplicity": 78, + "order": 126, + "rank_gap": 0, + "rows_sha256": "fd545ab44a3ba01543bd5a79858f04e4771bbc9fd428ecd51713df8878e1302e", + "squared_binary_rank": 78 + }, + { + "binary_rank": 78, + "characteristic_polynomial_hex": "0x55550000000000005555000000000000", + "h": 9, + "j": 2, + "k": 4, + "odd_eigenvalue_multiplicity": 78, + "order": 126, + "rank_gap": 0, + "rows_sha256": "d4daeb65d299debadb4356e1b9e535a056ded996720c9e89cc22e091f5713c8c", + "squared_binary_rank": 78 + }, + { + "binary_rank": 70, + "characteristic_polynomial_hex": "0x55000000000000005500000000000000", + "h": 9, + "j": 3, + "k": 4, + "odd_eigenvalue_multiplicity": 70, + "order": 126, + "rank_gap": 0, + "rows_sha256": "e7f2af6fee946e445883620fd9ea8b9217b2ae66a151b83a1670cb2bbe550a43", + "squared_binary_rank": 70 + }, + { + "binary_rank": 9, + "characteristic_polynomial_hex": "0x300000000000", + "h": 10, + "j": 0, + "k": 2, + "odd_eigenvalue_multiplicity": 1, + "order": 45, + "rank_gap": 8, + "rows_sha256": "8f28418f38d615847c156e75f941138e5843d57ecabf0f90a3a24003b017995a", + "squared_binary_rank": 1 + }, + { + "binary_rank": 45, + "characteristic_polynomial_hex": "0x333300003333", + "h": 10, + "j": 1, + "k": 2, + "odd_eigenvalue_multiplicity": 45, + "order": 45, + "rank_gap": 0, + "rows_sha256": "58cd68f1ed4ee23bf9f93115773bc1ad472a7fe86c7d54cb323ee91a83d4ca13", + "squared_binary_rank": 45 + }, + { + "binary_rank": 36, + "characteristic_polynomial_hex": "0x1000000000000000000000000000000", + "h": 10, + "j": 0, + "k": 3, + "odd_eigenvalue_multiplicity": 0, + "order": 120, + "rank_gap": 36, + "rows_sha256": "0c5b608a24a11dda932c1cb4ae1a11a7df3ce7006c58ea4deed3a945f245fcdb", + "squared_binary_rank": 0 + }, + { + "binary_rank": 10, + "characteristic_polynomial_hex": "0x1000000000000000000000000000000", + "h": 10, + "j": 1, + "k": 3, + "odd_eigenvalue_multiplicity": 0, + "order": 120, + "rank_gap": 10, + "rows_sha256": "e54494862619802dd90603bf5ef1f935428a1f951cc24819d82461a776e081fc", + "squared_binary_rank": 0 + }, + { + "binary_rank": 28, + "characteristic_polynomial_hex": "0x1000000000000000000000000000000", + "h": 10, + "j": 2, + "k": 3, + "odd_eigenvalue_multiplicity": 0, + "order": 120, + "rank_gap": 28, + "rows_sha256": "1fcfdaf305ad6280a1657b89ec0a03cc1c0e662e684e08f91c80bede608cb85d", + "squared_binary_rank": 0 + }, + { + "binary_rank": 93, + "characteristic_polynomial_hex": "0x44440000444400000000000000000000000000000000000000000", + "h": 10, + "j": 0, + "k": 4, + "odd_eigenvalue_multiplicity": 44, + "order": 210, + "rank_gap": 49, + "rows_sha256": "ca6648be61784f17648a7c7fe4d9d29885da465320b517544c01dcd01908f6f2", + "squared_binary_rank": 44 + }, + { + "binary_rank": 210, + "characteristic_polynomial_hex": "0x50005000000000005000500000000000500050000000000050005", + "h": 10, + "j": 1, + "k": 4, + "odd_eigenvalue_multiplicity": 210, + "order": 210, + "rank_gap": 0, + "rows_sha256": "14624b247aca6ade05554264a3cc4396a582fe038eb142a4c1b17e4c842c803e", + "squared_binary_rank": 210 + }, + { + "binary_rank": 174, + "characteristic_polynomial_hex": "0x55000000550000000000000000000000550000005500000000000", + "h": 10, + "j": 2, + "k": 4, + "odd_eigenvalue_multiplicity": 166, + "order": 210, + "rank_gap": 8, + "rows_sha256": "535578380b748e535766d76659354d2cb446bdcac1bcc9e6b95ce4d068716e7b", + "squared_binary_rank": 166 + }, + { + "binary_rank": 210, + "characteristic_polynomial_hex": "0x50005000000000005000500000000000500050000000000050005", + "h": 10, + "j": 3, + "k": 4, + "odd_eigenvalue_multiplicity": 210, + "order": 210, + "rank_gap": 0, + "rows_sha256": "b95e1392967c42c18edf511ab3f95f5e51d863605ef7d336ac040ef3c3d0e2e6", + "squared_binary_rank": 210 + } + ], + "controls": { + "nonsemisimple_witness": { + "characteristic_polynomial_hex": "0x40", + "h": 4, + "j": 0, + "k": 2, + "odd_multiplicity": 0, + "rank": 3, + "square_is_zero": true + }, + "rejected": [ + { + "name": "wrong_odd_multiplicity", + "reason": "Literal characteristic polynomial disagrees with claimed spectrum" + }, + { + "name": "degree_preserving_two_switch", + "reason": "Literal characteristic polynomial disagrees with claimed spectrum" + } + ], + "two_switch": { + "added_edges": [ + [ + 0, + 1 + ], + [ + 28, + 32 + ] + ], + "h": 7, + "integer_squared_trace": 175, + "integer_trace": 35, + "j": 0, + "k": 3, + "mutated_polynomial_hex": "0xfccc30000", + "original_polynomial_hex": "0xffff00000", + "preserves_each_row_degree": true, + "removed_edges": [ + [ + 0, + 32 + ], + [ + 1, + 28 + ] + ] + } + }, + "domain": { + "completed_cases": 41, + "h": [ + 4, + 10 + ], + "j": "0 through k-1", + "k": "2 through min(4, floor(h/2))" + }, + "implementation_sha256": "7bf1f2f61a6074bda5d731e694376a3b46f572a26189a7a973cc6ae59b23af3c", + "maximum_order": 210, + "scope": "Finite audit of modular characteristic polynomials and the associated binary rank lower bound. No all-size theorem, supplier construction, or new kappa.", + "source_sha256": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/single-intersection.md": "c3a9be97b38f4ac1e7983842d9f23656671e877ad5144f41894818f4551aa4dd", + "scripts/audit_single_intersection.py": "1de7f9a62edc93c624ff2693ae9bb725cf6dc9735ff1caad56f6913aae9448ee", + "scripts/experiments/single_intersection.py": "08ddae46e5621a5b4c525b504e67ae655abe9b49461d894feaa7abc89a51847d", + "tests/test_single_intersection.py": "333f14dee70ddffaf266a8041d0ee3a0bf64794e28c1f05cc8a6e8953a37543e" + }, + "status": "PASS_LITERAL_BINARY_SPECTRAL_AUDIT", + "strict_rank_gaps": 21 +} diff --git a/research/single-intersection-spectrum-audit/SOURCE.json b/research/single-intersection-spectrum-audit/SOURCE.json new file mode 100644 index 0000000000..536c8ea7d3 --- /dev/null +++ b/research/single-intersection-spectrum-audit/SOURCE.json @@ -0,0 +1,32 @@ +{ + "assignment_seed": 65, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "candidates": [ + "Prime-power common-subset infinite-tail ceiling", + "Fano permutation rigidity", + "Single-intersection spectral parity bound" + ], + "coordination": "No pinned issues returned; sole open issue #650 concerns Discussions, so claim recorded locally.", + "deliverable": "Scoped audit with exact per-case characteristic polynomials/ranks and semisimplicity/trace-preserving negative controls; no new kappa", + "expected_finish_utc": "2026-10-13T06:27:45Z", + "method": "Independent GF(2) Hessenberg characteristic polynomial and ascending-column elimination on literal subset-intersection matrices", + "object": "scripts/experiments/single_intersection.py:spectral_parity_bound and docs/research/single-intersection.md characteristic-polynomial rank deduction", + "overlap": "596 distinct open PRs checked across six API pages; #778 overlaps the family but verifies orbit Gram construction, not the modular spectral polynomial.", + "overlapping_pr": { + "head": "f015b04c74801fa330f818d178e809c760fb5469", + "number": 778, + "scope": "Gram packing and finite orbit replay, not an independent modular spectral polynomial" + }, + "parameter_domain": "4 <= h <= 10, 2 <= k <= min(4, floor(h/2)), 0 <= j < k; seed-dependent upper h=9+seed%2 and upper k=2+seed%3", + "randomness": "Operating-system randomness via secrets.randbelow(100)", + "selection": "seed modulo 3 = 2, single-intersection spectral parity bound", + "source_sha256": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/single-intersection.md": "c3a9be97b38f4ac1e7983842d9f23656671e877ad5144f41894818f4551aa4dd", + "scripts/audit_single_intersection.py": "1de7f9a62edc93c624ff2693ae9bb725cf6dc9735ff1caad56f6913aae9448ee", + "scripts/experiments/single_intersection.py": "08ddae46e5621a5b4c525b504e67ae655abe9b49461d894feaa7abc89a51847d", + "tests/test_single_intersection.py": "333f14dee70ddffaf266a8041d0ee3a0bf64794e28c1f05cc8a6e8953a37543e" + }, + "stopping_rule": "Complete the fixed domain once; do not expand to historical large orbit fixtures or repeated repository-wide replays.", + "track": "Adversarial mathematical audit" +} diff --git a/research/single-intersection-spectrum-audit/spectrum_audit.py b/research/single-intersection-spectrum-audit/spectrum_audit.py new file mode 100644 index 0000000000..8b81e0b48d --- /dev/null +++ b/research/single-intersection-spectrum-audit/spectrum_audit.py @@ -0,0 +1,246 @@ +"""Audit the historical Johnson spectral bound with literal binary matrices.""" +import argparse +import json +import sys +from hashlib import sha256 +from itertools import combinations +from pathlib import Path +from typing import Sequence, TypedDict + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT / "scripts")) + +from experiments.single_intersection import spectral_parity_bound + + +class AuditFailure(ValueError): + """A source pin or exact mathematical comparison failed.""" + + +class CaseResult(TypedDict): + h: int + k: int + j: int + order: int + characteristic_polynomial_hex: str + odd_eigenvalue_multiplicity: int + binary_rank: int + squared_binary_rank: int + rank_gap: int + rows_sha256: str + + +def require(condition: bool, message: str) -> None: + if not condition: + raise AuditFailure(message) + + +def validate_rows(rows: Sequence[int]) -> None: + limit = 1 << len(rows) + require(all(type(row) is int and 0 <= row < limit for row in rows), + "Rows must encode a square binary matrix") + + +def literal_rows(h: int, k: int, j: int) -> list[int]: + require(all(type(value) is int for value in (h, k, j)) and + 2 <= k <= h // 2 and 0 <= j < k, "Invalid subset parameters") + labels = [frozenset(label) for label in combinations(range(h), k)] + return [sum(1 << column for column, target in enumerate(labels) + if source == target or len(source & target) == j) + for source in labels] + + +def binary_rank(rows: Sequence[int]) -> int: + validate_rows(rows) + work = list(rows) + pivot_row = 0 + for column in range(len(rows)): + pivot = next((row for row in range(pivot_row, len(rows)) + if work[row] & (1 << column)), None) + if pivot is None: + continue + work[pivot_row], work[pivot] = work[pivot], work[pivot_row] + for row in range(pivot_row + 1, len(rows)): + if work[row] & (1 << column): + work[row] ^= work[pivot_row] + pivot_row += 1 + return pivot_row + + +def binary_square(rows: Sequence[int]) -> list[int]: + validate_rows(rows) + squared = [] + for row in rows: + value = 0 + indices = row + while indices: + bit = indices & -indices + value ^= rows[bit.bit_length() - 1] + indices ^= bit + squared.append(value) + return squared + + +def characteristic_polynomial(rows: Sequence[int]) -> int: + """Return det(xI-A), with polynomial coefficients encoded as bits.""" + validate_rows(rows) + work = list(rows) + order = len(rows) + for column in range(order - 1): + target = column + 1 + pivot = next((row for row in range(target, order) + if work[row] & (1 << column)), None) + if pivot is None: + continue + if pivot != target: + work[pivot], work[target] = work[target], work[pivot] + mask = (1 << target) | (1 << pivot) + for row in range(order): + if ((work[row] >> target) ^ (work[row] >> pivot)) & 1: + work[row] ^= mask + for row in range(target + 1, order): + if work[row] & (1 << column): + work[row] ^= work[target] + for index in range(order): + if work[index] & (1 << row): + work[index] ^= 1 << target + require(all(not (work[row] & ((1 << (row - 1)) - 1)) + for row in range(2, order)), "Hessenberg reduction failed") + leading = [1] + for size in range(1, order + 1): + column = size - 1 + polynomial = leading[-1] << 1 + if work[column] & (1 << column): + polynomial ^= leading[-1] + for row in range(column - 1, -1, -1): + if not (work[row + 1] & (1 << row)): + break + if work[row] & (1 << column): + polynomial ^= leading[row] + leading.append(polynomial) + return leading[-1] + + +def parity_polynomial(order: int, odd_multiplicity: int) -> int: + require(type(order) is int and type(odd_multiplicity) is int and + 0 <= odd_multiplicity <= order, "Invalid spectral multiplicity") + polynomial = 1 + for _ in range(odd_multiplicity): + polynomial = (polynomial << 1) ^ polynomial + return polynomial << (order - odd_multiplicity) + + +def check_spectrum(rows: Sequence[int], odd_multiplicity: int) -> int: + polynomial = characteristic_polynomial(rows) + require(polynomial == parity_polynomial(len(rows), odd_multiplicity), + "Literal characteristic polynomial disagrees with claimed spectrum") + actual_rank = binary_rank(rows) + require(actual_rank >= odd_multiplicity, + "Spectral rank lower bound exceeds literal binary rank") + return polynomial + + +def audit_case(h: int, k: int, j: int) -> CaseResult: + rows = literal_rows(h, k, j) + claimed = spectral_parity_bound(h, k, j) + odd_multiplicity = claimed["binary_rank_lower"] + require(type(odd_multiplicity) is int, "Claimed multiplicity must be integral") + polynomial = check_spectrum(rows, odd_multiplicity) + actual_rank = binary_rank(rows) + return CaseResult(h=h, k=k, j=j, order=len(rows), + characteristic_polynomial_hex=hex(polynomial), + odd_eigenvalue_multiplicity=odd_multiplicity, + binary_rank=actual_rank, + squared_binary_rank=binary_rank(binary_square(rows)), + rank_gap=actual_rank - odd_multiplicity, + rows_sha256=sha256(json.dumps(rows, separators=(",", ":")) + .encode()).hexdigest()) + + +def source_pins() -> dict[str, str]: + source = json.loads((PACKAGE / "SOURCE.json").read_text()) + pins: dict[str, str] = source["source_sha256"] + for path, expected in pins.items(): + require(sha256((ROOT / path).read_bytes()).hexdigest() == expected, + "Changed pinned source: " + path) + return pins + + +def negative_controls() -> dict[str, object]: + rows = literal_rows(7, 3, 0) + edges = ((0, 32), (1, 28), (0, 1), (28, 32)) + require(all(rows[left] & (1 << right) for left, right in edges[:2]) and + all(not (rows[left] & (1 << right)) for left, right in edges[2:]), + "Changed degree-preserving control fixture") + mutated = list(rows) + for left, right in edges: + mutated[left] ^= 1 << right + mutated[right] ^= 1 << left + require([row.bit_count() for row in rows] == + [row.bit_count() for row in mutated], "Control changed row degrees") + require(all((rows[index] ^ mutated[index]) & (1 << index) == 0 + for index in range(len(rows))), "Control changed diagonal") + rejected = [] + for name, candidate, multiplicity in ( + ("wrong_odd_multiplicity", rows, 16), + ("degree_preserving_two_switch", mutated, 15)): + try: + check_spectrum(candidate, multiplicity) + except AuditFailure as failure: + rejected.append({"name": name, "reason": str(failure)}) + else: + raise AuditFailure("Negative control was accepted: " + name) + nilpotent = literal_rows(4, 2, 0) + require(binary_rank(nilpotent) == 3 and binary_square(nilpotent) == [0] * 6, + "Changed nonsemisimple witness") + return {"rejected": rejected, + "two_switch": {"h": 7, "k": 3, "j": 0, + "removed_edges": [list(edge) for edge in edges[:2]], + "added_edges": [list(edge) for edge in edges[2:]], + "preserves_each_row_degree": True, + "integer_trace": 35, "integer_squared_trace": 175, + "original_polynomial_hex": hex(characteristic_polynomial(rows)), + "mutated_polynomial_hex": hex(characteristic_polynomial(mutated))}, + "nonsemisimple_witness": {"h": 4, "k": 2, "j": 0, + "characteristic_polynomial_hex": "0x40", + "odd_multiplicity": 0, "rank": 3, + "square_is_zero": True}} + + +def certificate() -> dict[str, object]: + pins = source_pins() + cases = [audit_case(h, k, j) for h in range(4, 11) + for k in range(2, min(4, h // 2) + 1) for j in range(k)] + return {"status": "PASS_LITERAL_BINARY_SPECTRAL_AUDIT", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 65, + "domain": {"h": [4, 10], "k": "2 through min(4, floor(h/2))", + "j": "0 through k-1", "completed_cases": len(cases)}, + "maximum_order": max(case["order"] for case in cases), + "strict_rank_gaps": sum(case["rank_gap"] > 0 for case in cases), + "cases": cases, "source_sha256": pins, + "controls": negative_controls(), + "implementation_sha256": sha256(Path(__file__).read_bytes()).hexdigest(), + "scope": "Finite audit of modular characteristic polynomials and the " + "associated binary rank lower bound. No all-size theorem, " + "supplier construction, or new kappa."} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", + help="Regenerate only this package's RESULT.json") + arguments = parser.parse_args() + result = certificate() + target = PACKAGE / "RESULT.json" + if arguments.write: + target.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + require(result == json.loads(target.read_text()), + "Committed result does not match fresh exact audit") + print(result["status"], result["domain"]) + + +if __name__ == "__main__": + main() diff --git a/tests/test_single_intersection_spectrum_audit.py b/tests/test_single_intersection_spectrum_audit.py new file mode 100644 index 0000000000..9074a33feb --- /dev/null +++ b/tests/test_single_intersection_spectrum_audit.py @@ -0,0 +1,154 @@ +"""Independent determinant and corruption controls for the spectral audit.""" +import json +import sys +import unittest +from hashlib import sha256 +from itertools import permutations +from pathlib import Path +from random import Random +from tempfile import TemporaryDirectory +from typing import Sequence +from unittest.mock import patch + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT / "research" / "single-intersection-spectrum-audit")) + +import spectrum_audit +from spectrum_audit import ( + AuditFailure, + binary_rank, + binary_square, + certificate, + characteristic_polynomial, + check_spectrum, + literal_rows, + main, + parity_polynomial, +) + + +def leibniz_polynomial(rows: Sequence[int]) -> int: + order = len(rows) + result = 0 + for permutation in permutations(range(order)): + product = 1 + for row, column in enumerate(permutation): + entry = (rows[row] >> column) & 1 + if row == column: + product = (product << 1) ^ (product if entry else 0) + elif not entry: + product = 0 + break + result ^= product + return result + + +def kernel_rank(rows: Sequence[int]) -> int: + kernel_size = sum(all((row & vector).bit_count() % 2 == 0 for row in rows) + for vector in range(1 << len(rows))) + return len(rows) - (kernel_size.bit_length() - 1) + + +class SpectrumAuditTests(unittest.TestCase): + + def test_every_three_by_three_binary_matrix_against_leibniz_and_kernel(self) -> None: + for packed in range(1 << 9): + rows = [(packed >> (3 * row)) & 7 for row in range(3)] + self.assertEqual(characteristic_polynomial(rows), leibniz_polynomial(rows)) + self.assertEqual(binary_rank(rows), kernel_rank(rows)) + + def test_larger_nonsymmetric_matrices_against_leibniz_and_kernel(self) -> None: + generator = Random(65) + for order in (4, 5, 6): + for _ in range(16): + rows = [generator.randrange(1 << order) for _ in range(order)] + self.assertEqual(characteristic_polynomial(rows), leibniz_polynomial(rows)) + self.assertEqual(binary_rank(rows), kernel_rank(rows)) + + def test_literal_complement_pairs_are_nonsemisimple(self) -> None: + for k in (2, 3, 4, 5): + rows = literal_rows(2 * k, k, 0) + self.assertEqual(characteristic_polynomial(rows), 1 << len(rows)) + self.assertEqual(binary_rank(rows), len(rows) // 2) + self.assertEqual(binary_square(rows), [0] * len(rows)) + check_spectrum(rows, 0) + + def test_degree_preserving_corruption_escapes_both_trace_checks(self) -> None: + rows = literal_rows(7, 3, 0) + mutated = list(rows) + for left, right in ((0, 32), (1, 28), (0, 1), (28, 32)): + mutated[left] ^= 1 << right + mutated[right] ^= 1 << left + for matrix in (rows, mutated): + self.assertEqual(sum((row >> index) & 1 for index, row in enumerate(matrix)), 35) + self.assertEqual(sum(row.bit_count() for row in matrix), 175) + self.assertEqual([row.bit_count() for row in rows], + [row.bit_count() for row in mutated]) + self.assertNotEqual(characteristic_polynomial(rows), + characteristic_polynomial(mutated)) + with self.assertRaisesRegex(AuditFailure, "characteristic polynomial"): + check_spectrum(mutated, 15) + + def test_wrong_spectral_parity_is_rejected(self) -> None: + rows = literal_rows(7, 3, 0) + with self.assertRaisesRegex(AuditFailure, "characteristic polynomial"): + check_spectrum(rows, 16) + + def test_permutation_similarity_and_transpose(self) -> None: + rows = literal_rows(6, 3, 1) + permutation = list(reversed(range(len(rows)))) + permuted = [sum(((rows[old_row] >> old_column) & 1) << column + for column, old_column in enumerate(permutation)) + for old_row in permutation] + transpose = [sum(((rows[row] >> column) & 1) << row + for row in range(len(rows))) for column in range(len(rows))] + for matrix in (permuted, transpose): + self.assertEqual(characteristic_polynomial(matrix), characteristic_polynomial(rows)) + self.assertEqual(binary_rank(matrix), binary_rank(rows)) + + def test_committed_certificate_matches_complete_domain(self) -> None: + expected = json.loads((ROOT / "research" / "single-intersection-spectrum-audit" / + "RESULT.json").read_text()) + self.assertEqual(certificate(), expected) + self.assertEqual(expected["domain"]["completed_cases"], 41) + + def test_changed_source_is_rejected(self) -> None: + with TemporaryDirectory() as directory: + root = Path(directory) + source = root / "dependency.py" + source.write_text("original source\n") + manifest = {"source_sha256": {"dependency.py": sha256(source.read_bytes()).hexdigest()}} + (root / "SOURCE.json").write_text(json.dumps(manifest)) + with patch.object(spectrum_audit, "ROOT", root), patch.object(spectrum_audit, "PACKAGE", root): + self.assertEqual(spectrum_audit.source_pins(), manifest["source_sha256"]) + source.write_text("changed source\n") + with self.assertRaisesRegex(AuditFailure, "Changed pinned source"): + spectrum_audit.source_pins() + + def test_default_command_rejects_changed_result(self) -> None: + package = ROOT / "research" / "single-intersection-spectrum-audit" + expected = json.loads((package / "RESULT.json").read_text()) + expected["cases"][0]["characteristic_polynomial_hex"] = "0x41" + with TemporaryDirectory() as directory: + temporary = Path(directory) + (temporary / "SOURCE.json").write_bytes((package / "SOURCE.json").read_bytes()) + (temporary / "RESULT.json").write_text(json.dumps(expected)) + with patch.object(spectrum_audit, "PACKAGE", temporary), patch.object(sys, "argv", ["audit"]): + with self.assertRaisesRegex(AuditFailure, "Committed result"): + main() + + def test_matrix_shape_and_spectral_domain_are_checked(self) -> None: + for rows in ([-1], [2], [True], [0, 4]): + for check in (binary_rank, binary_square, characteristic_polynomial): + with self.assertRaises(AuditFailure): + check(rows) + for order, odd in ((-1, 0), (2, 3), (2, -1), (True, 1)): + with self.assertRaises(AuditFailure): + parity_polynomial(order, odd) + for parameters in ((4, 3, 1), (4, 2, 2), (4, 2, -1)): + with self.assertRaises(AuditFailure): + literal_rows(*parameters) + + +if __name__ == "__main__": + unittest.main()