From 4219727be784f329a5bf2949cb4c29f0a04456e8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 22:01:33 +0000 Subject: [PATCH] feat(research): prove full rank of four-subset side maps --- research/four-subset-side-spectrum/PROOF.md | 142 +++++++++++++++ research/four-subset-side-spectrum/README.md | 100 +++++++++++ .../four-subset-side-spectrum/SOURCES.json | 24 +++ research/four-subset-side-spectrum/TASK.json | 93 ++++++++++ .../four-subset-side-spectrum/VERIFY.json | 34 ++++ research/four-subset-side-spectrum/verify.py | 163 ++++++++++++++++++ 6 files changed, 556 insertions(+) create mode 100644 research/four-subset-side-spectrum/PROOF.md create mode 100644 research/four-subset-side-spectrum/README.md create mode 100644 research/four-subset-side-spectrum/SOURCES.json create mode 100644 research/four-subset-side-spectrum/TASK.json create mode 100644 research/four-subset-side-spectrum/VERIFY.json create mode 100644 research/four-subset-side-spectrum/verify.py diff --git a/research/four-subset-side-spectrum/PROOF.md b/research/four-subset-side-spectrum/PROOF.md new file mode 100644 index 0000000000..520f905bd2 --- /dev/null +++ b/research/four-subset-side-spectrum/PROOF.md @@ -0,0 +1,142 @@ +# Exact spectrum and full side rank for the four-subset decoder + +This is a scoped proof over Q, also valid over every characteristic-zero +field. It takes the definition of K from Cinna Davis's +[PR #2225](https://github.com/CrocSwap/integer-mult-bounds/pull/2225). +The predecessor's fitting, dyadic-coefficient and physical-support claims +are cited background. They are not reverified here. + +Let n >= 5 be odd, let V be the set of four-subsets of [n], and put + + K(S,T) = binomial(|S intersection T|/2, 2). + +The new conclusion is that I-K is invertible for every such n. Thus the +exact side response cannot factor through fewer than binomial(n,4) scalar +linear intermediates. This only excludes a factorization with no direct +source-to-output bypass. It is not a lower bound on arbitrary side circuits, +their work, native calls, or their paid rank profile. + +## 1. Incidence decomposition + +For j=1,2 let W_j have rows indexed by four-subsets and columns by +j-subsets, with entry one for containment and zero otherwise. Since + + binomial(t/2,2) = (1/4) binomial(t,2) - (1/8) binomial(t,1), + +the definition gives + + 8K = 2 W_2 W_2^T - W_1 W_1^T. (1) + +Let B be the n-by-binomial(n,2) vertex/pair incidence matrix. Directly +counting four-subsets containing a prescribed union gives + + W_2^T W_2 = a I + (n-4) B^T B + J, + a = (n-4)(n-5)/2, (2) + B B^T = (n-2) I + J, + W_2 B^T = 3 W_1. (3) + +Here each J is the all-ones matrix of its displayed size. For (2), the +three entries, according to pair intersection size 2,1,0, are +binomial(n-2,2), n-3, 1. This proves (2) without invoking a spectrum theorem. + +Assume n >= 7. Pair-coordinate space is the orthogonal direct sum + + E0 = constants, dimension 1, + E1 = B^T {u : sum(u)=0}, dimension n-1, + E2 = ker B, dimension binomial(n,2)-n. + +The formula for B B^T shows that B has row rank n. The three eigenvalues +of W_2^T W_2 in (2) are respectively + + 6 binomial(n-2,2), 3 binomial(n-3,2), binomial(n-4,2). + +They are positive for n >= 7. Hence W_2 has full column rank and maps +these subspaces injectively into port space. The orthogonal complement +of its image has dimension binomial(n,4)-binomial(n,2). + +On W_2 E0 the eigenvalue of W_1 W_1^T is 4 binomial(n-1,3), by its +constant row sum. On W_2 E2 it is zero, by (3). To check the remaining +space directly, counting vertex/pair incidences gives + + W_1^T W_2 = binomial(n-3,2) B + (n-3) J. + +For sum(u)=0 use B B^T u=(n-2)u and W_1 u=W_2 B^T u/3. +It follows that W_1 W_1^T acts on W_2 E1 with eigenvalue +binomial(n-2,3). Both terms of (1) vanish on the remaining port space. + +## 2. The spectrum + +Substitution into (1) gives the following eigenvalues of K, with their +multiplicities. Coincident eigenvalues have additive multiplicities. + +| Eigenvalue | Multiplicity | +| --- | ---: | +| (n-2)(n-3)(10-n)/12 | 1 | +| (n-3)(n-4)(20-n)/48 | n-1 | +| (n-4)(n-5)/8 | binomial(n,2)-n | +| 0 | binomial(n,4)-binomial(n,2) | + +For odd n >= 7 the first three are nonzero, so rank(K)=binomial(n,2). +This rank statement concerns rational linear intermediates; it supplies +no implementation of a smaller dyadic feature basis. + +For n=5, distinct four-subsets intersect in three points. Thus +K=(5/8)I+(3/8)J. Its eigenvalues are 5/2 once and 5/8 four times. +Its rank is five. The n>=7 incidence multiplicities do not apply here. + +## 3. No eigenvalue is one + +For the first eigenvalue, n=7 and n=9 give 5 and 7/2; every odd n>=11 +gives a negative value. For the second, each odd n in [7,15] has numerator +at least 4*3*5=60>48. At n=17 and n=19 its numerators are 546 and 240. +Every odd n>=21 gives a negative value. For the third, n=7 gives 3/4; +every odd n>=9 gives at least 5/2. The zero eigenvalue and the two n=5 +eigenvalues also differ from one. + +Therefore I-K is invertible for every allowed n. For the first requested +side-map instance n=9, the exact spectra are + + K: (7/2)^1, (55/8)^8, (5/2)^27, 0^90; + I-K: (-5/2)^1, (-47/8)^8, (-3/2)^27, 1^90. + +In particular, rank(K)=36 and rank(I-K)=126, and + + det(I-K) = 5 * 3^27 * 47^8 / 2^52. + +The source incidence expansion has 45 features. Its feature count is not +asserted to be its rational rank. + +## 4. The exact compression obstruction + +If all source dependence reaches the output through h scalar linear +intermediates, the side map has a factorization I-K=D A, with A having h +rows and D having h columns. Therefore + + binomial(n,4) = rank(I-K) <= h. + +This bound is sharp in that declared algebraic model: A=I and D=I-K use +exactly binomial(n,4) intermediates. No physical cost is assigned to this +attaining factorization. A direct identity contribution and a separate +compressed -K correction fall outside the no-bypass hypothesis and remain +available to a future side circuit. Dirty helpers, restoration, actual +frames, chronology, native orientation and a complete invoice still need +separate constructions and proofs. + +## 5. Evidence and scope + +The standalone verifier builds the complete integer matrix 8K directly +from intersections at n=5,7,9. Fraction-free elimination checks every +predicted eigenspace dimension and the full determinant of 8K-8I. It also +counts literal pair-incidence Gram entries at n=7,9 and checks the scalar +formulas on a bounded larger domain. The proof above, not that finite +domain, supplies the every-n quantifier. Mutations and an actual rank-four +compression control test the new conclusions. Nothing imports or replays +the predecessor's verifier. The output receipt is generated from results +and package hashes; no receipt is handwritten. + +The new result was produced by Nick Petalas. The kernel definition, +decoder motivation and open side-map obligation are by Cinna Davis, with +the subset/compiler ancestry retained in PR #2225. Incidence decompositions +and the rank inequality for a product are classical. No new general +spectral method, supplier, kappa, selected-frontier update, formal-kernel +acceptance or independent human review is claimed. diff --git a/research/four-subset-side-spectrum/README.md b/research/four-subset-side-spectrum/README.md new file mode 100644 index 0000000000..9c34668405 --- /dev/null +++ b/research/four-subset-side-spectrum/README.md @@ -0,0 +1,100 @@ +# Full side rank for the four-subset decoder + +For every odd n >= 5, the complementary four-subset kernel +K(S,T)=binomial(|S intersection T|/2,2) has invertible side map I-K over Q. +At n=9 its ranks are rank(K)=36 and rank(I-K)=126. The +[proof](PROOF.md) gives the complete spectrum for every n and a sharp +algebraic consequence: implementing the whole side response through scalar +linear intermediates, with no direct source-to-output bypass, needs at least +binomial(n,4) intermediates. This is a scoped proof, not a physical tariff or +a new kappa. + +This takes a partial step on Cinna Davis / 1337isnot1337's +[PR #2225](https://github.com/CrocSwap/integer-mult-bounds/pull/2225), which +leaves the side map open. It derives a new side-map obstruction from that +kernel's definition. It does not audit the predecessor's fitting theorem, +feature supports or numbers. A direct identity contribution plus a compressed +-K correction remains outside this obstruction and may still help a circuit. + +Ali Romman's merged [PR #5458](https://github.com/CrocSwap/integer-mult-bounds/pull/5458) +studies the cube restriction of the same kernel and separate binary endpoint +hulls. Here the port set is the entire constant-weight shell, with 126 ports +at n=9, and the conclusion is its full side-map spectrum. Full-rank +compensation in other geometries is also prior work, including Dominik +Scholz's [PR #606](https://github.com/CrocSwap/integer-mult-bounds/pull/606) +on E8 squared. This package claims the four-subset result, not the general +idea of a compensation-rank obstruction. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/four-subset-side-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/four-subset-side-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/four-subset-side-spectrum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/four-subset-side-spectrum --check-source-history +``` + +Another CPython 3.12 path can be substituted. The direct success marker is +`PASS_FOUR_SUBSET_SIDE_SPECTRUM`. The registered launcher must print +`PASS_REGISTERED_RESEARCH_PACKAGE`; the publication check must print +`PASS_RESEARCH_COMMIT_BYTES`. + +The read-only verifier reconstructs all 17,126 matrix entries at n=5,7,9 +directly from intersections. Exact fraction-free elimination checks all ten +eigenspace dimensions, the three full side ranks and their complete +determinants. Literal incidence counting checks 1,737 pair-Gram entries. +The bounded formula check covers 499 odd n through 1001; it is not the proof +of the unbounded statement. Three malformed spectra are rejected, and an +actual smaller compression has the expected deficient rank. A generated +stdout receipt records results, interpreter version and all six package-file +hashes. No receipt or replay output is written into the checkout. + +## Scope and implementation limits + +The result is over characteristic zero. It covers k=4, not every even k. +It proves no bound on circuits with retained source access, general dirty +workspace, native queries or paid recursive work. The rank-36 kernel at n=9 +does not supply a 36-feature dyadic circuit. Its predecessor's 45-feature +incidence expansion remains credited and unchanged. Physical side construction, +restoration, both native orientations, hosting, precision and the complete +supplier invoice remain open. The selected frontier and its five framework +assumptions are unchanged. No selected cold replay, Lean, Docker, independent +human review or formal proof-kernel review is claimed. + +The verifier uses no external runtime inputs. `SOURCES.json` pins the source +definition and task/selected-record provenance through ancestor Git blobs. +The bounded checker uses dynamic Python allocation, a managed-runtime +deviation from Power of Ten's fixed-allocation rule. Its largest dense matrix +is 126 by 126, its incidence list has 36 pairs, and every loop has a finite +bound from the explicit replay domain. Elimination checks every exact division; +exceptions propagate. Warning-strict normal and optimized execution retain +all acceptance checks. There is no recursive or generated executable code. + +## Open next questions + +- Can a legal direct identity route plus a compressed -K correction implement + the n=9 side map cheaply? Begin with explicit input/output frames and charge + arbitrary dirty restoration. This theorem does not exclude that route. +- For another even k, when is one an eigenvalue of the complementary-subset + kernel? Derive its incidence action before inferring any physical invoice. + +## Credit and coordination + +This contribution was produced by Nick Petalas. Cinna Davis supplies the +kernel definition, dyadic fitting construction, support theorem and open +side-map question in PR #2225. The source retains the Zhihao Chen subset and +compiler ancestry. Incidence decomposition and rank bounds for products are +classical; the contribution is this exact spectrum and its scoped side-map +consequence. + +Base: `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8. +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228386) +records the scope. The initial P104-oriented selection changed to this +specific decoder-side obligation. Main, merged PRs, open PRs, this account's +recent contributions and active claims were searched. The cached open snapshot +covered 393 PRs and complete Discussion pagination; sparse local note coverage +was incomplete. The relevant source was materialized and main was searched +through Git. No matching side-spectrum result was found in that coverage; +unpublished work remains outside it. diff --git a/research/four-subset-side-spectrum/SOURCES.json b/research/four-subset-side-spectrum/SOURCES.json new file mode 100644 index 0000000000..379dc75845 --- /dev/null +++ b/research/four-subset-side-spectrum/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/even-subset-dyadic-kernels/PROOF.md", + "usage": "provenance", + "git_blob": "5f760220be590e9b891e8867d5c366a601bc019d", + "sha256": "ddc0d91dff486a4593c6f200191f12774406ea84f52bde8bf75d1a473b5e6d52" + } + ] +} diff --git a/research/four-subset-side-spectrum/TASK.json b/research/four-subset-side-spectrum/TASK.json new file mode 100644 index 0000000000..f0fb2bfc3b --- /dev/null +++ b/research/four-subset-side-spectrum/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact characteristic-zero spectrum of the complementary four-subset kernel and invertibility of I-K for every odd n>=5; derive its sharp no-bypass linear-intermediate floor.", + "scope_change_reason": "The initial P104-oriented selection encountered a distinct explicit side-map obligation in Cinna Davis PR2225. This is a scoped algebraic decoder-side result, not a priced supplier or a coframe search.", + "bottleneck_link": "PR2225 leaves I-K unimplemented. Its full rank rules out compressing the entire side response through fewer linear intermediates without a direct source bypass; it does not rule out a complete side circuit.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved and exactly checked side-map rank obstruction; do not extend to other k or synthesize a physical caller.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-n proof; verify.py checks complete n=5,7,9 eigenspaces and determinants plus literal incidence counts and controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a legal direct identity route and a compressed -K correction implement the n=9 side map cheaply?", + "why_it_matters": "That route escapes the no-bypass compression obstruction.", + "first_step": "Specify the physical entry/exit frames and emit one arbitrary-input side circuit with dirty restoration.", + "blocked_by": "No physical side word or complete invoice is supplied." + }, + { + "question": "For other even k, when is one an eigenvalue of the complementary-subset kernel?", + "why_it_matters": "The side rank can then change.", + "first_step": "Derive the incidence action for one changed k.", + "blocked_by": "Only k=4 is proved here." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228386", + "source": "PR #2225", + "source_author": "1337isnot1337", + "open_pr_records": 393, + "discussion_records": 5631, + "local_note_records": 68, + "local_head_note_records": 8136, + "sparse_local_coverage_complete": false, + "playbook": "Autonomous local run", + "preserved_state": "Clean detached HEAD at 19fdb086ea96af9a9f87936a2b888e10af4ed810; no earlier branch name." + } +} diff --git a/research/four-subset-side-spectrum/VERIFY.json b/research/four-subset-side-spectrum/VERIFY.json new file mode 100644 index 0000000000..92c802b6f9 --- /dev/null +++ b/research/four-subset-side-spectrum/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Complete exact n=5,7,9 eigenspaces and side determinants; literal incidence Gram counts; finite scalar formula checks and four controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete check under optimized Python; explicit acceptance checks remain enabled." + } + ] +} diff --git a/research/four-subset-side-spectrum/verify.py b/research/four-subset-side-spectrum/verify.py new file mode 100644 index 0000000000..64be93b73c --- /dev/null +++ b/research/four-subset-side-spectrum/verify.py @@ -0,0 +1,163 @@ +"""Exact finite checks of the new four-subset side spectrum; stdlib only.""" + +from hashlib import sha256 +from itertools import combinations +import json +from math import comb, prod +from pathlib import Path +import platform + + +MAX_PORTS = 126 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def bareiss(matrix: list[list[int]]) -> tuple[int, int]: + """Return exact rank and determinant by fraction-free elimination.""" + size = len(matrix) + require(0 < size <= MAX_PORTS, "matrix size outside finite replay") + require(all(len(row) == size for row in matrix), "nonsquare matrix") + work = [row[:] for row in matrix] + previous, rank, sign = 1, 0, 1 + for column in range(size): + pivot_row = next( + (row for row in range(rank, size) if work[row][column]), None + ) + if pivot_row is None: + continue + if pivot_row != rank: + work[rank], work[pivot_row] = work[pivot_row], work[rank] + sign = -sign + pivot = work[rank][column] + for row in range(rank + 1, size): + factor = work[row][column] + for target in range(column + 1, size): + numerator = pivot * work[row][target] - factor * work[rank][target] + quotient, remainder = divmod(numerator, previous) + require(remainder == 0, "nonexact Bareiss division") + work[row][target] = quotient + work[row][column] = 0 + previous = pivot + rank += 1 + if rank == size: + break + determinant = sign * previous if rank == size else 0 + return rank, determinant + + +def shifted(matrix: list[list[int]], scalar: int) -> list[list[int]]: + return [ + [value - (scalar if row == column else 0) + for column, value in enumerate(values)] + for row, values in enumerate(matrix) + ] + + +def spectrum(n: int) -> dict[int, int]: + """Eigenvalues of 8K with their claimed multiplicities.""" + require(5 <= n <= 1001 and n % 2 == 1, "finite odd formula domain required") + if n == 5: + return {20: 1, 5: 4} + a, remainder_a = divmod(2 * (n - 2) * (n - 3) * (10 - n), 3) + b, remainder_b = divmod((n - 3) * (n - 4) * (20 - n), 6) + require(remainder_a == remainder_b == 0, "nonintegral scaled eigenvalue") + rows = [(a, 1), (b, n - 1), ((n - 4) * (n - 5), comb(n, 2) - n), + (0, comb(n, 4) - comb(n, 2))] + result: dict[int, int] = {} + for eigenvalue, multiplicity in rows: + result[eigenvalue] = result.get(eigenvalue, 0) + multiplicity + return result + + +def check_dense(n: int) -> dict[str, object]: + require(n in (5, 7, 9), "finite dense domain required") + ports = [frozenset(port) for port in combinations(range(n), 4)] + size = len(ports) + require(size <= MAX_PORTS, "port bound exceeded") + # Literal t(t-2), independently of incidence-space spectral formulas. + matrix = [[len(s & t) * (len(s & t) - 2) for t in ports] for s in ports] + expected = spectrum(n) + require(sum(expected.values()) == size, "wrong total multiplicity") + for eigenvalue, multiplicity in expected.items(): + rank, _ = bareiss(shifted(matrix, eigenvalue)) + require(size - rank == multiplicity, "wrong dense eigenspace dimension") + rank, determinant = bareiss(shifted(matrix, 8)) + predicted = prod((eigenvalue - 8) ** count + for eigenvalue, count in expected.items()) + require(rank == size, "side response is singular") + require(determinant == predicted, "wrong side determinant") + kernel_rank, _ = bareiss(matrix) + require(kernel_rank == size - expected.get(0, 0), "wrong kernel rank") + return {"n": n, "ports": size, "scaled_kernel_spectrum": expected, + "kernel_rank": kernel_rank, "side_rank": rank, + "det_8K_minus_8I": str(determinant), + "dense_eigenspaces": len(expected), "literal_entries": size * size} + + +def check_incidence(n: int) -> int: + require(n in (7, 9), "finite incidence domain required") + pairs = [frozenset(pair) for pair in combinations(range(n), 2)] + ports = [frozenset(port) for port in combinations(range(n), 4)] + checked = 0 + for left in pairs: + for right in pairs: + literal = sum(left <= port and right <= port for port in ports) + expected = ((n - 4) * (n - 5) // 2 if left == right else 0) + expected += (n - 4) * len(left & right) + 1 + require(literal == expected, "wrong pair-incidence Gram identity") + checked += 1 + return checked + + +def check_controls() -> int: + # Wrong matrices retain the original spectrum as their rejection target. + ports = [frozenset(port) for port in combinations(range(5), 4)] + correct = [[len(s & t) * (len(s & t) - 2) for t in ports] for s in ports] + mutants = [[row[:] for row in correct] for _ in range(3)] + mutants[0][0][0] += 1 + mutants[1][0][1] *= -1 + mutants[2] = [[-len(s & t) for t in ports] for s in ports] + rejected = 0 + for mutant in mutants: + failed = False + for eigenvalue, count in spectrum(5).items(): + rank, _ = bareiss(shifted(mutant, eigenvalue)) + failed = failed or len(mutant) - rank != count + require(failed, "a false spectrum survived") + rejected += 1 + # An actual smaller intermediate space has rank at most four, not five. + compressed = [[1 if row == column and row < 4 else 0 + for column in range(5)] for row in range(5)] + rank, _ = bareiss(compressed) + require(rank == 4, "compression control rank") + return rejected + 1 + + +def main() -> None: + cases = [check_dense(n) for n in (5, 7, 9)] + incidence_checks = sum(check_incidence(n) for n in (7, 9)) + formula_cases = 0 + for n in range(5, 1002, 2): + expected = spectrum(n) + require(8 not in expected, "eigenvalue one contradicts side theorem") + require(sum(expected.values()) == comb(n, 4), "formula dimension") + formula_cases += 1 + controls = check_controls() + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps({"status": "PASS_FOUR_SUBSET_SIDE_SPECTRUM", + "python": platform.python_version(), "cases": cases, + "incidence_gram_entries": incidence_checks, + "formula_cases": formula_cases, "controls": controls, + "package_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()