diff --git a/research/schur-central-spectrum/README.md b/research/schur-central-spectrum/README.md new file mode 100644 index 0000000000..29444eb40e --- /dev/null +++ b/research/schur-central-spectrum/README.md @@ -0,0 +1,241 @@ +# A central-spectrum law for scalar Schur deletion + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped algebraic proof with exact finite corroboration.** Let P,Q be +commuting idempotent matrices over any field F, with common leading scalar +entry 1. Let S,T be their Schur complements after deleting that entry, and set + +```text +h = (PQ)[1,1], D = S-T, Z = D^2, C = ST-TS, theta = h(2-h). +``` + +Then + +```text +(Z-theta I) C = 0, +Z(Z-I)(Z-theta I) = 0. +``` + +Thus the central operator Z has no eigenvalues outside `{0,1,h(2-h)}`. +If these three scalars are distinct, Z is diagonalizable over F and its +`theta`-eigenspace equals `im C`, of dimension at most two. The polynomial +retains its repeated factors when theta is 0 or 1. A ternary example below +has nonzero Z with Z^2=0, so replacing the polynomial by its square-free part +is false in general. + +This supplies one constraint on the higher-rank residual invariants asked for +in [codyw912's PR4735](https://github.com/CrocSwap/integer-mult-bounds/pull/4735). +The known centrality of Z for arbitrary idempotent pairs is credited to +[Ryanson Jonathan's PR4609](https://github.com/CrocSwap/integer-mult-bounds/pull/4609) +in this repository. The new statement is the specific scalar action of Z on +the commutator image after a commuting scalar identity-pivot deletion. +It is neither a sufficient conjugacy invariant nor a full-guard count. + +## Proof over every field + +Write the original matrices in blocks as + +```text +P = [[1,r],[c,A]], Q = [[1,s],[e,B]], +S = A-cr, T = B-es. +``` + +Here r,s are rows and c,e are columns. Products are ordered as displayed. +Idempotency gives + +```text +rc=se=0, rS=Sc=0, sT=Te=0, S^2=S, T^2=T. +``` + +For example, P^2=P gives `rA=0`, `Ac=0`, `rc=0`, and `A^2=A-cr`. +Substitution in `(A-cr)^2` proves S^2=S. The proof for T is identical. +These residual facts already occur in the credited Schur lineage. + +The top-left block of PQ=QP gives + +```text +re=sc=h-1. +``` + +The top-right and bottom-left blocks respectively give + +```text +rT-sS = h(r-s), +Se-Tc = h(e-c). +``` + +Put `x=e-c`, `y=r-s`, and `w=Tc`. Expanding the bottom-right commutation +identity and substituting the last two equations gives + +```text +C = w y + x(sS+h y). (1) +``` + +For clarity, the unreduced equation is + +```text +0 = C + Se s - Tc r + c rT - e sS + h(cs-er). +``` + +Its last five terms reduce to `-w y-x sS-h x y`, proving (1). +Consequently `im C` is contained in `L=span{x,w}`, whose dimension is at most +two. No independence of x,w is assumed. + +The same identities determine D on this subspace: + +```text +Sx = w+hx, Tx = -w, +Sw = (1-h)w+h(1-h)x, Tw = w, +Dx = hx+2w, Dw = h(1-h)x-hw. (2) +``` + +To obtain Sw, apply S^2=S to e and use `Se=w+hx` and `Sx=w+hx`. +Squaring the two equations for D in (2) now gives + +```text +D^2 x = h(2-h)x, D^2 w = h(2-h)w. +``` + +They are polynomial identities and hold in characteristic two as well. +Together with (1) they prove `(Z-theta I)C=0`. + +For any two idempotents, without a commutation assumption on them, + +```text +Z = S+T-ST-TS, +ZS = SZ = S-STS, ZT = TZ = T-TST, +C^2 = Z^2-Z. +``` + +The first two lines prove centrality; expansion using S^2=S,T^2=T proves +the last. Multiply `(Z-theta I)C=0` on the right by C and substitute +`C^2=Z(Z-I)`. All factors are polynomials in Z, so +`Z(Z-I)(Z-theta I)=0`. + +When 0,1,theta are distinct, this annihilating polynomial splits into +distinct linear factors, proving diagonalizability. Equation (1) and the +first identity give `im C` inside the theta-eigenspace. Conversely, if +`Zv=theta v`, then `C^2 v=theta(theta-1)v`, so v belongs to im C. This +proves equality and the dimension bound. + +## A necessary repeated root + +Over F3 use the commuting diagonal pair + +```text +P0 = diag(0,1,0,1), Q0 = diag(0,0,1,1). +``` + +Choose first header column `a=(1,1,1,1)^t` and inverse first row +`b=(1,2,2,2)`. They satisfy `ba=bP0a=bQ0a=1` and `bP0Q0a=2`. +Complete the header with the kernel basis of b used by the verifier. +The resulting three-dimensional Schur pair has h=2, theta=0, and nonzero +Z with Z^2=0. The checker constructs the full header, inverts it, and +checks the input hypotheses and the literal Schur complements. Thus this +is an attained deletion example, not merely an arbitrary idempotent pair. +The factor Z^2 in the cubic at theta=0 is necessary. + +## Reproduce and verification scope + +From the repository root, the exact local interpreter is +`/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12`: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/schur-central-spectrum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/schur-central-spectrum --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/schur-central-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/schur-central-spectrum/verify.py +``` + +The standalone checker needs only Python 3.12's standard library and the +package files; it has no Git or predecessor-code dependency. It prints +its exact finite histograms, hashes of the package files it read, and +`PASS_SCHUR_CENTRAL_SPECTRUM`. It writes no receipt or generated file. +The stdout hash report is generated from the actual file bytes. + +The finite domains are all split pairs for the following fixed diagonal +sector profiles, in sector order 00,10,01,11: + +| Field | Sector dimensions | Split pairs | Admitted identity pivots | +|---|---|---:|---:| +| F2 | (1,1,1,2) | 496 | 172 | +| F3 | (1,1,1,1) | 2,160 | 306 | +| F5 | (1,1,1,1) | 78,000 | 4,260 | + +Every admitted split tests the new identities on the full-space lifts +`P0-P0abP0` and `Q0-Q0abQ0`. These maps kill a and have image in ker b; +in any completing header they are `diag(0,S)` and `diag(0,T)`. Hence the +lift checks are exactly the claimed polynomial identities for the residuals. +For the first twelve admitted splits in each profile the checker also +constructs the header and compares the lifted matrix with the literal Schur +matrix. The binary profile is the first working example from Mihir +Srivastava's #4689; its 172 admissions are cited corroboration, not a new count. + +Another 28 explicit eight-dimensional examples cover every h in each of +F2,F3,F5,F7,F11 and are checked with literal headers. Eight controls reject +missing pivot, idempotency, commutation, field and shape hypotheses; replacing +theta by h; forcing central idempotency; and extending the theta=0 identity +to arbitrary idempotent pairs. All checks use explicit exceptions under -O. +The all-field theorem rests on the written proof, not extrapolation from these +domains. The histograms are corroborating outputs, not complete-header counts. + +## Scope, provenance and credit + +Canonical base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +The selected conditional kappa remains 0.00302015. The original +`formal-interface-lemma` card is explicitly changed to an algebraic side +question following #4735. This does not discharge a selected supplier premise. +The family decision is to stop at this identity, with complete producer, +consumer, emission, reads, restoration, stock and physical costs still unknown. + +The public [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132032) +records the original question. Live overlap searches and their limits are +recorded in TASK.json. All-main README and merged-PR searches supplement the +sparse local-note search. An absence of matches is not proof of novelty. +No existing package or selected-frontier file is changed. + +Credit codyw912 #4735 for the sufficient-invariant question and residual +recurrence; Mihir Srivastava #4689 for the first binary profile and state +census; Ryanson Jonathan #4609 for the central-operator viewpoint and projector +refinement; ssafwann #4678/#4671 for header counting and sector methods; +Nick Petalas #4597/#4278 for ordered Schur factorization and residual identities; +lee-phys for binary dimension work; and Cinna Davis and the retained normalizer +lineage, source527, commdata2338 and Jose Manuel, for the BIT/header context. +Exact source paths and hashes are provenance entries in SOURCES.json. +No predecessor code is imported. Existing predecessor credit remains unchanged. + +Independent human and formal proof-kernel review are unclaimed. Lean, Docker, +the selected cold replay, a sufficient higher-rank conjugacy classification, +block pivots of size greater than one and physical caller admission were not +run or proved. No new kappa or complete multiplication theorem is claimed. + +## Open next questions + +1. Can the central-operator constraint be combined with image/kernel data to + give a sufficient residual invariant? Begin with the theta=0 repeated-root + example and distinguish its nilpotent blocks. The identity is only a + necessary condition, so completeness is the unresolved obligation. +2. What replaces the scalar action h(2-h) for a common identity block I_d? + Start from the two-column calculation (1)-(2) with matrix H and retain + product order. Noncommuting matrix coefficients obstruct treating h as a + scalar; no larger-block identity is asserted here. + +## Verifier engineering limits + +The checker has structured finite loops, no recursion, and functions shorter +than 60 lines. Prime fields and matrix sizes are fixed internally; matrices +have at most eight rows, and enumeration materializes at most 625 vectors in +the registered domains. There are no subprocesses, network operations, dynamic +code evaluation or shared mutable caches. Explicit exceptions check the +mathematical invariants in ordinary and optimized Python. + +Power-of-Ten rules 3 and 9 require a managed-runtime deviation here. Python +allocates tuples, integers and generator objects during arithmetic, and its +standard library uses runtime dispatch. The scope is this finite standalone +checker; bounded dimensions, finite domains and five package reads of at most +1 MiB each bound live data. Normal and optimized warning-strict registered +replays are the compensating checks. Reassess these bounds before adding an +input-driven search or an external dependency. There is no compiled build or +repository-configured Python type checker for this isolated checker; Python's +warning-strict execution and the package CI replay provide diagnostics. diff --git a/research/schur-central-spectrum/SOURCES.json b/research/schur-central-spectrum/SOURCES.json new file mode 100644 index 0000000000..d99316b2bc --- /dev/null +++ b/research/schur-central-spectrum/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/schur-invariant-transitions/README.md", + "usage": "provenance", + "git_blob": "d5118b9f5911949964245eb8942065faff972900", + "sha256": "fccdd2bff1ee00c120796bb1b6c3739cce90dcffbff7c96e897300ed81bba72e" + }, + { + "path": "research/schur-projector-refinement/README.md", + "usage": "provenance", + "git_blob": "c6fc0e77d9f1022d519df8e3d8266672df793adb", + "sha256": "7edb11d24ffd6fa4604ebfa9d27215d74a684ea23a484a0cf36a970f08571232" + }, + { + "path": "research/schur-residual-orbits/README.md", + "usage": "provenance", + "git_blob": "a2361477d9373969ccb7ab0f4f3c4b9919c051ba", + "sha256": "15e2f1a7d4edcc8f71e75ead949928c2ac883a3fb8268bb5827f290de4d28d76" + }, + { + "path": "research/schur-commutator-criterion/README.md", + "usage": "provenance", + "git_blob": "6b37342de04f5c42c198dd6ba14cea9845be6f05", + "sha256": "5616da2e708a8425f1bf0bf5c89c236ef8ed0a23d0544d30ae2142ffe167dc01" + }, + { + "path": "research/block-schur-commutator/README.md", + "usage": "provenance", + "git_blob": "79790ccea54cfea1aab611768927651a81f2fb18", + "sha256": "945c1420fe9fb5c26dec49e7d6005d77382ca9dc6ca0f424d8baa1500bfc092c" + }, + { + "path": "research/schur-header-count/README.md", + "usage": "provenance", + "git_blob": "5e644cf316312c0fdd489c8d33911583f1b88af2", + "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e" + }, + { + "path": "research/identity-pivot-sector-bound/README.md", + "usage": "provenance", + "git_blob": "80c587372713ca47a79d4880dab330e642c3a25a", + "sha256": "c997446a1fc4683694987feea5f2a8423b57d48d5513a27e178f84ecf56ffc12" + } + ] +} diff --git a/research/schur-central-spectrum/TASK.json b/research/schur-central-spectrum/TASK.json new file mode 100644 index 0000000000..0a173c5a1b --- /dev/null +++ b/research/schur-central-spectrum/TASK.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the all-field scalar identity-pivot Schur central-spectrum law (Z-h(2-h)I)[S,T]=0 and its cubic annihilator.", + "scope_change_reason": "Take the explicit sufficient-invariant open question in codyw912 #4735 as a scoped algebraic side problem, rather than formalizing selected-interface arithmetic.", + "bottleneck_link": "A necessary state invariant for Schur/header recursion; it supplies neither a paid header cover nor selected supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop after the first written all-field identity and bounded exact corroboration; do not extend to a conjugacy classification or larger pivots.", + "outcome": "completed", + "evidence": "README.md contains the all-field proof. verify.py exhausts three specified split domains, checks every h over five prime fields with literal headers, and runs eight rejection controls. Registered replay output supplies generated file hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the central constraint and image/kernel data give a sufficient residual invariant?", + "why_it_matters": "A sufficient invariant could make header recursion scalable.", + "first_step": "Classify the nilpotent central blocks of the ternary theta=0 witness.", + "blocked_by": "The proved polynomial is only a necessary condition." + }, + { + "question": "What replaces h(2-h) for a common identity block I_d?", + "why_it_matters": "Larger block deletion leaves higher-rank residuals.", + "first_step": "Repeat the ordered two-column calculation with matrix H.", + "blocked_by": "The coefficients no longer commute; no block formula is proved." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132032", + "overlap": { + "remote_open_prs": 325, + "remote_open_prs_fetched_at": "2026-10-22T20:12:02.519131+00:00", + "discussion_records": 3742, + "discussions_fetched_at": "2026-10-22T20:12:48.702307+00:00", + "local_notes_searched": 82, + "local_notes_total": 6321, + "limits": "Sparse local notes omit 6239 paths. Direct all-main README searches for central Schur/residual spectra and annihilators, targeted merged searches, live predecessor bodies and recent handoffs supplement this cache. Arbitrary diffs and unpublished work are outside coverage.", + "submission_refresh": "2026-10-22: origin/main remained 624de9dc66858af0945e5f8a0942488d62280d43; live Schur PR bodies #4774/#4785 and latest 25 handoff posts reread; repeated main/merged spectral terms found no duplicate. New shared-H rank-pair and guard-count claims concern different quantities." + } +} diff --git a/research/schur-central-spectrum/VERIFY.json b/research/schur-central-spectrum/VERIFY.json new file mode 100644 index 0000000000..9a64b9a0f5 --- /dev/null +++ b/research/schur-central-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": "All-field identity corroboration on three exhaustive split domains, all-h explicit constructions, literal Schur comparisons and eight rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All-field identity corroboration on three exhaustive split domains, all-h explicit constructions, literal Schur comparisons and eight rejection controls." + } + ] +} diff --git a/research/schur-central-spectrum/verify.py b/research/schur-central-spectrum/verify.py new file mode 100644 index 0000000000..1723a15603 --- /dev/null +++ b/research/schur-central-spectrum/verify.py @@ -0,0 +1,266 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the scalar Schur central-spectrum identity.""" +from __future__ import annotations + +import hashlib +import itertools +import json +from pathlib import Path + +Matrix = tuple[tuple[int, ...], ...] + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def identity(n: int) -> Matrix: + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def multiply(a: Matrix, b: Matrix, q: int) -> Matrix: + n = len(a) + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(n)) % q + for j in range(n)) for i in range(n)) + + +def subtract(a: Matrix, b: Matrix, q: int) -> Matrix: + return tuple(tuple((x - y) % q for x, y in zip(r, s, strict=True)) + for r, s in zip(a, b, strict=True)) + + +def scale(a: Matrix, c: int, q: int) -> Matrix: + return tuple(tuple(c * x % q for x in row) for row in a) + + +def rank(a: Matrix, q: int) -> int: + rows = [list(row) for row in a] + height, width = len(rows), len(rows[0]) + pivot = 0 + for col in range(width): + candidate = next((i for i in range(pivot, height) if rows[i][col]), None) + if candidate is None: + continue + rows[pivot], rows[candidate] = rows[candidate], rows[pivot] + inv = pow(rows[pivot][col], -1, q) + rows[pivot] = [x * inv % q for x in rows[pivot]] + for i in range(height): + if i != pivot: + c = rows[i][col] + rows[i] = [(x - c * y) % q + for x, y in zip(rows[i], rows[pivot], strict=True)] + pivot += 1 + if pivot == height: + break + return pivot + + +def inverse(a: Matrix, q: int) -> Matrix: + n = len(a) + rows = [list(row) + list(unit) for row, unit in zip(a, identity(n), strict=True)] + for col in range(n): + candidate = next((i for i in range(col, n) if rows[i][col]), None) + require(candidate is not None, "singular header") + rows[col], rows[candidate] = rows[candidate], rows[col] + inv = pow(rows[col][col], -1, q) + rows[col] = [x * inv % q for x in rows[col]] + for i in range(n): + if i != col: + c = rows[i][col] + rows[i] = [(x - c * y) % q + for x, y in zip(rows[i], rows[col], strict=True)] + return tuple(tuple(row[n:]) for row in rows) + + +def validate_pair(p: Matrix, r: Matrix, q: int) -> None: + require(q in (2, 3, 5, 7, 11), "unsupported prime") + n = len(p) + require(2 <= n <= 8 and len(r) == n, "matrix size outside bounded domain") + require(all(len(row) == n for row in p + r), "nonsquare matrices") + require(all(type(x) is int and 0 <= x < q for row in p + r for x in row), + "noncanonical field entry") + require(p[0][0] == r[0][0] == 1, "common identity pivot required") + require(multiply(p, p, q) == p and multiply(r, r, q) == r, + "idempotent inputs required") + require(multiply(p, r, q) == multiply(r, p, q), "commuting inputs required") + + +def schur(p: Matrix, q: int) -> Matrix: + return tuple(tuple((p[i][j] - p[i][0] * p[0][j]) % q + for j in range(1, len(p))) for i in range(1, len(p))) + + +def check_residual(s: Matrix, t: Matrix, h: int, q: int) -> dict[str, int]: + unit = identity(len(s)) + d = subtract(s, t, q) + z = multiply(d, d, q) + c = subtract(multiply(s, t, q), multiply(t, s, q), q) + theta = h * (2 - h) % q + require(multiply(s, s, q) == s and multiply(t, t, q) == t, + "residual idempotency") + require(multiply(z, s, q) == multiply(s, z, q), "centrality with S") + require(multiply(z, t, q) == multiply(t, z, q), "centrality with T") + require(multiply(z, c, q) == scale(c, theta, q), "central-spectrum identity") + require(multiply(c, c, q) == subtract(multiply(z, z, q), z, q), + "universal commutator square") + polynomial = multiply(multiply(z, subtract(z, unit, q), q), + subtract(z, scale(unit, theta, q), q), q) + require(not any(map(any, polynomial)), "cubic annihilator") + require(rank(c, q) <= 2, "scalar deletion rank bound") + return {"h": h, "theta": theta, "commutator_rank": rank(c, q), + "central_rank": rank(z, q), + "central_idempotent": int(multiply(z, z, q) == z)} + + +def diagonal(values: tuple[int, ...]) -> Matrix: + n = len(values) + return tuple(tuple(values[i] if i == j else 0 for j in range(n)) + for i in range(n)) + + +def split_header(a: tuple[int, ...], b: tuple[int, ...], q: int) -> Matrix: + n = len(a) + require(sum(x * y for x, y in zip(a, b, strict=True)) % q == 1, + "split functional must send first column to one") + pivot = next(i for i, x in enumerate(b) if x) + columns = [a] + for j in range(n): + if j != pivot: + v = [0] * n + v[j] = 1 + v[pivot] = -b[j] * pow(b[pivot], -1, q) % q + columns.append(tuple(v)) + return tuple(tuple(columns[j][i] for j in range(n)) for i in range(n)) + + +def lifted_residual(p: tuple[int, ...], a: tuple[int, ...], + b: tuple[int, ...], q: int) -> Matrix: + n = len(p) + return tuple(tuple(((p[i] if i == j else 0) - p[i] * a[i] * b[j] * p[j]) % q + for j in range(n)) for i in range(n)) + + +def check_split(p: tuple[int, ...], r: tuple[int, ...], a: tuple[int, ...], + b: tuple[int, ...], q: int, literal: bool) -> dict[str, int]: + h = sum(b[i] * p[i] * r[i] * a[i] for i in range(len(a))) % q + s, t = lifted_residual(p, a, b, q), lifted_residual(r, a, b, q) + result = check_residual(s, t, h, q) + if literal: + m = split_header(a, b, q) + mi = inverse(m, q) + pp = multiply(multiply(mi, diagonal(p), q), m, q) + rr = multiply(multiply(mi, diagonal(r), q), m, q) + validate_pair(pp, rr, q) + actual = check_residual(schur(pp, q), schur(rr, q), h, q) + require(actual == result, "lift versus literal Schur invariant") + ss = multiply(multiply(mi, s, q), m, q) + require(ss[0] == (0,) * len(a) and all(row[0] == 0 for row in ss), + "lift must vanish on deleted coordinate") + require(tuple(row[1:] for row in ss[1:]) == schur(pp, q), + "lift versus literal Schur matrix") + return result + + +def enumerate_profile(q: int, sectors: tuple[int, ...]) -> dict: + p = tuple(int(i in (1, 3)) for i, size in enumerate(sectors) for _ in range(size)) + r = tuple(int(i in (2, 3)) for i, size in enumerate(sectors) for _ in range(size)) + n = len(p) + require(q in (2, 3, 5) and 2 <= n <= 5, "profile exceeds enumeration cap") + vectors = tuple(itertools.product(range(q), repeat=n)) + total = admitted = literal = 0 + histogram: dict[tuple[int, ...], int] = {} + for a in vectors: + for b in vectors: + if sum(x * y for x, y in zip(a, b, strict=True)) % q != 1: + continue + total += 1 + if any(sum(b[i] * v[i] * a[i] for i in range(n)) % q != 1 for v in (p, r)): + continue + admitted += 1 + direct = admitted <= 12 + literal += int(direct) + result = check_split(p, r, a, b, q, direct) + key = tuple(result.values()) + histogram[key] = histogram.get(key, 0) + 1 + require(total == (q ** n - 1) * q ** (n - 1), "complete split domain") + require(admitted > 0, "empty positive domain") + return {"q": q, "sectors": sectors, "split_pairs": total, + "admitted": admitted, "literal_headers": literal, + "histogram_columns": list(result), + "histogram": [[list(k), v] for k, v in sorted(histogram.items())]} + + +def core_examples() -> list[dict]: + results = [] + p = (0, 0, 1, 1, 0, 0, 1, 1) + r = (0, 0, 0, 0, 1, 1, 1, 1) + a = (1, 0) * 4 + for q in (2, 3, 5, 7, 11): + for h in range(q): + weights = ((h - 1) % q, (1 - h) % q, (1 - h) % q, h) + b = tuple(x for w in weights for x in (w, 1)) + result = check_split(p, r, a, b, q, True) + require(result["h"] == h, "prescribed product scalar") + results.append({"q": q, **result}) + return results + + +def rejection_controls() -> int: + # Hypothesis controls use actual matrices and the same entry validator. + good = diagonal((1, 0)) + bad_cases = [ + (diagonal((0, 1)), good, 2), + (((1, 1), (1, 0)), good, 2), + (((1, 1), (0, 0)), good, 2), + (good, good, 4), + (((1, 0, 0), (0, 0, 0)), good, 2), + ] + for p, r, q in bad_cases: + try: + validate_pair(p, r, q) + except ValueError: + pass + else: + raise ValueError("hypothesis control accepted") + # A genuine ternary identity-pivot example has theta=0 but Z^2 != Z. + p, r = (0, 1, 0, 1), (0, 0, 1, 1) + a, b = (1, 1, 1, 1), (1, 2, 2, 2) + check_split(p, r, a, b, 3, True) + s, t = lifted_residual(p, a, b, 3), lifted_residual(r, a, b, 3) + z = multiply(subtract(s, t, 3), subtract(s, t, 3), 3) + c = subtract(multiply(s, t, 3), multiply(t, s, 3), 3) + require(any(map(any, z)) and not any(map(any, multiply(z, z, 3))), + "repeated zero root is necessary") + require(multiply(z, c, 3) != scale(c, 2, 3), "theta=h mutant survived") + require(multiply(z, z, 3) != z, "central-idempotent mutant survived") + # A commuting pair is essential; the proposed identity is not universal. + s, t = ((1, 0), (0, 0)), ((2, 1), (1, 2)) + require(multiply(t, t, 3) == t, "negative residual must be idempotent") + z = multiply(subtract(s, t, 3), subtract(s, t, 3), 3) + c = subtract(multiply(s, t, 3), multiply(t, s, 3), 3) + require(any(map(any, multiply(z, c, 3))), "arbitrary-pair theta=0 control") + return len(bad_cases) + 3 + + +def main() -> None: + profiles = [enumerate_profile(2, (1, 1, 1, 2)), + enumerate_profile(3, (1, 1, 1, 1)), + enumerate_profile(5, (1, 1, 1, 1))] + examples = core_examples() + controls = rejection_controls() + root = Path(__file__).resolve().parent + names = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = root / name + require(path.stat().st_size <= 1024 * 1024, "package file exceeds 1 MiB") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + print(json.dumps({"profiles": profiles, "all_h_examples": examples, + "rejection_controls": controls, "file_sha256": hashes}, + sort_keys=True)) + print("PASS_SCHUR_CENTRAL_SPECTRUM") + + +if __name__ == "__main__": + main()