From 02f0ffab916042785f0a61ebfc4dacb9495a0ac2 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 11:30:31 +0000 Subject: [PATCH] feat(research): prove the first central Schur state collision --- research/schur-central-alias/PROOF.md | 131 ++++++++++++ research/schur-central-alias/README.md | 100 +++++++++ research/schur-central-alias/SOURCES.json | 36 ++++ research/schur-central-alias/TASK.json | 109 ++++++++++ research/schur-central-alias/VERIFY.json | 38 ++++ research/schur-central-alias/verify.py | 235 ++++++++++++++++++++++ 6 files changed, 649 insertions(+) create mode 100644 research/schur-central-alias/PROOF.md create mode 100644 research/schur-central-alias/README.md create mode 100644 research/schur-central-alias/SOURCES.json create mode 100644 research/schur-central-alias/TASK.json create mode 100644 research/schur-central-alias/VERIFY.json create mode 100644 research/schur-central-alias/verify.py diff --git a/research/schur-central-alias/PROOF.md b/research/schur-central-alias/PROOF.md new file mode 100644 index 0000000000..0f2d2ee748 --- /dev/null +++ b/research/schur-central-alias/PROOF.md @@ -0,0 +1,131 @@ +# The first central-class alias for sharp nilpotent Schur states + +Work over any field of characteristic two. The ordered pair matters: the +state equivalence is simultaneous conjugacy of S and T, without exchanging +the two requests. Put K=S+T and Z=K^2. + +## Contract and credited premises + +Start with commuting idempotents P0,Q0, a size-d common identity pivot, +and sharp residuals rank(ST-TS)=2d. The compressed product is the nilpotent +matrix H. Fix the four ordered original sector dimensions r00,r10,r01,r11. +Let a=dim ker H. The nilpotent normal form and its whole-pair rigidity are +Malik Safwan / ssafwann's #5267, not new claims here. They require + + r00=d+s00, r10=d+s10, r01=d+s01, r11=d+a+s11, + +with nonnegative padding. The minimal residual acts on U^3 plus F^a: + + S(x,y,z,t)=(H(x+z)+Nt, 0, (I+H)(z+x)+Nt, t), + T(x,y,z,t)=(0, H(y+z)+Nt, (I+H)(z+y)+Nt, t). + +Here im N complements im H. Add scalar pairs (0,0), (1,0), (0,1), (1,1) +with multiplicities s00,s10,s01,s11. All those statements, including +admissibility as genuine Schur residuals, are the cited predecessor model. +Ali Romman's #5287 already determines the complete central Jordan class, +and Mihir Srivastava's #5360 supplies the general-H ordered gluing theorem. +No predecessor scientific verifier is used as this contribution's evidence. + +The new result is the first same-profile central-class alias, its sharp +minimum dimension, and the explicit ordered-state separator below. It is +an obstruction to an ordered-state registry using only the central class. +It does not contradict a classifier whose declared output is only Z. + +## Rank information retained and discarded + +Write W=I+H. It is invertible. In coordinates +u=x+y, v=y+z, w=z, t, the minimal K is + + K(u,v,w,t)=(Hu, Wu+Hv+Nt, Wu, 0). + +For every j>=1, its jth power is + + (H^j u, + (j mod 2) W H^(j-1)u + H^j v + H^(j-1)Nt, + W H^(j-1)u, + 0). + +This follows by multiplying once and induction; no division by two occurs. +The u-column image is a graph over W im H^(j-1), so has dimension +rank H^(j-1). Its intersection with the v,t-column image is zero: a zero +w component forces H^(j-1)u=0 and then every u contribution is zero. +The v,t-column image has dimension rank H^(j-1), because + + im H^j + im H^(j-1)N = H^(j-1)(im H + im N) = im H^(j-1). + +The padding contributes c=s10+s01 to every positive power rank. Therefore + + rank K^j = 2 rank H^(j-1) + c, (1) + rank Z^j = 2 rank H^(2j-1) + c. (2) + +Equation (2) is also a rank-sequence restatement of #5287's credited +characteristic-two Jordan law. At fixed d and fixed original profile, c +and the total residual dimension are fixed. The multiplicity of eigenvalue +one is c and all other central blocks are nilpotent. Thus two such central +classes agree exactly when all odd positive power ranks of H agree. +In contrast, (1) retains every power rank of H. Nilpotent similarity is +determined by all power ranks. The normal-form rigidity supplies the converse +for full ordered pairs with the same H similarity class and profile. + +## The collision + +Take d=4, original profile (4,4,4,6), and no padding. Compare + + H_A=J3(0) direct-sum J1(0), H_B=J2(0) direct-sum J2(0). + +Both have a=2 and rank H=2. Every odd power of order at least three is zero. +Hence both fourteen-dimensional central operators have ranks + + rank Z=4, rank Z^2=0, + +and full Jordan partition (2,2,2,2,1,1,1,1,1,1). +A complete central similarity class, rather than just its spectrum, aliases. +However rank H_A^2=1 and rank H_B^2=0. Equation (1) gives + + rank (S_A+T_A)^3=2, rank (S_B+T_B)^3=0. + +Simultaneous conjugacy would preserve this rank. The two ordered pairs are +therefore nonconjugate over every field of characteristic two. + +## Literal original headers + +The standalone checker also constructs original eighteen-dimensional +commuting projectors; it does not just trust admissibility of a residual. +In the Jordan convention H e_(i+1)=e_i, let R extract the bottom coordinate +of each block, and let W=I+H. In sector order 00,10,01,11, use + + P0=diag(0_4,I_4,0_4,I_6), Q0=diag(0_4,0_4,I_4,I_6). + i=(I,I,I,H,R)^T, pi=(W,W,W,I,0). + +The last sector is U plus F^2. The map i is injective, pi i=I, +pi P0 i=pi Q0 i=I, and pi P0 Q0 i=H. A basis B of ker pi is + + B(x,y,z,t)=(x,y,z,W(x+y+z),t). + +Thus M=[i,B] is invertible. Conjugate P0,Q0 by M and delete the common +identity block by the literal Schur formula D-cb. This yields the two +witness pairs used by the verifier. All entries are in F2, so their exact +ranks and equations persist over every extension field of characteristic +two. The checker constructs an invertible fourteen-dimensional central +intertwiner as well as checking all stated ranks. + +## Minimality + +Consider any two states in this nilpotent sharp family at the same d and +same ordered original profile. Equal central classes imply equal rank Z. +By (2), their H ranks agree. At d=1,2,3, the nilpotent partitions are, +respectively, + + (1); (2),(1,1); (3),(2,1),(1,1,1). + +Within each dimension these partitions have distinct ranks. Equal central +classes therefore force similar H and, by #5267 rigidity, conjugate ordered +pairs. This proves the pivot threshold d=4. + +At d=4 the only distinct partitions sharing a rank are (3,1) and (2,2), +both with a=2. Their least possible residual dimension is 3d+a=14, attained +above. At d>=5 every nilpotent H has a>=1 and residual dimension at least +3d+a>=16. Thus fourteen is also the least residual dimension for this +same-d, same-profile nilpotent central alias. The corresponding least +ambient dimension is eighteen. These minima concern precisely this family; +no claim is made about arbitrary pairs of idempotents or nonsharp states. diff --git a/research/schur-central-alias/README.md b/research/schur-central-alias/README.md new file mode 100644 index 0000000000..26d9e94455 --- /dev/null +++ b/research/schur-central-alias/README.md @@ -0,0 +1,100 @@ +# Central Schur classes first alias at pivot dimension four + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with exact finite corroboration. In the +sharp nilpotent identity-pivot Schur family, over every characteristic-two +field, two ordered residual pairs with the same pivot size and four original +sector dimensions can have identical complete central similarity classes +without being simultaneously conjugate. The least pivot size is **four**; +the least residual and ambient dimensions are **fourteen** and **eighteen**. + +The witness has original sector dimensions (4,4,4,6) and compressed products +J3(0)+J1(0) and J2(0)+J2(0). Both central operators have full Jordan form +J2(0)^4 + J1(0)^6. The ranks of (S+T)^3 are two and zero, which distinguish +the ordered states. Consequently a complete central-class key cannot safely +deduplicate these ordered states. This is a local algebraic obstruction, +with no new kappa, physical cost saving or supplier-admission claim. + +[PROOF.md](PROOF.md) gives the argument and explicit original headers. The +central class retains precisely the odd positive power ranks of H; the sum +S+T retains every power rank. The minimality proof uses only the nilpotent +partitions through size four and the credited whole-pair rigidity theorem. + +Credit Malik Safwan / ssafwann [#5267](https://github.com/CrocSwap/integer-mult-bounds/pull/5267) +for the nilpotent model, admissibility and rigidity; Ali Romman +[#5287](https://github.com/CrocSwap/integer-mult-bounds/pull/5287) for the +already complete characteristic-two central law; Mihir Srivastava +[#5360](https://github.com/CrocSwap/integer-mult-bounds/pull/5360) for the +general-H ordered gluing boundary; Nick Petalas #4746/#4597, MatShep #4762, +codyw912 #4735, and the retained Ryanson Jonathan, lee-phys, Cinna Davis, +source527, commdata2338 and Jose Manuel lineage. Those results are cited +premises, not replay deliverables. Classical nilpotent power-rank facts are +not claimed as new. + +## Reproduction + +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/schur-central-alias/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/schur-central-alias/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/schur-central-alias +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/schur-central-alias --check-source-history +``` + +Other machines may substitute their CPython 3.12 path. Expected direct marker: +`PASS_SCHUR_CENTRAL_ALIAS`. The verifier writes no files. Its computed receipt +binds all package source hashes and a digest of both literal witness pairs, +the explicit central intertwiner, the finite minimality census and controls. +A receipt is printed, not hand-written or accepted as a mathematical premise. + +The exact checks construct two complete eighteen-dimensional original +headers and fourteen-dimensional residual pairs, verify the common identity +pivots, prescribed products, idempotence, original commutation and sharp +commutator rank eight, and compare eight power ranks of each sum and centre. +An invertible central intertwiner is checked by literal multiplication. +All eleven nilpotent partitions of sizes one through four and all fourteen +same-size unordered comparisons give exactly the displayed collision. +Eight controls cover invalid partitions, singular inversion, a non-square-zero +central input, a different central class and the ordered-state separator. +Normal and optimized checks enforce the same explicit exceptions. + +The all-field proof relies on the written argument and cited normal form; +finite evidence is not independent human or formal proof-kernel review. +The selected source-binding orientation passed at #7000. No predecessor +scientific suite, selected cold replay, native replay, Lean or Docker ran. +Physical access, movement, precision, stock, coefficient preparation, +restoration, dispatch, a complete supplier invoice and all five selected +framework assumptions remain outside scope. + +## Engineering and overlap + +The autonomous local run stopped at this first obstruction. The formal-interface- +lemma card is changed to a written state-information side result; no formal +caller binding is claimed. The baseline card example was run before the +experiment. New code uses bounded finite domains, no recursion, functions +below sixty lines and warning-strict normal/optimized checks. CPython allocation +is a Power of Ten rule-three deviation: the hard-coded largest matrix is +18 by 36 during augmented elimination, with bounded live fixture collections. +No external static analyzer is claimed. The verifier imports no predecessor +code and has no mutable external resources. + +Live open PR bodies, recent handoffs and main-tree README searches were +checked for Schur central collisions, ordered-pair classification and the +partitions (3,1)/(2,2). Merged #5287 closes the older characteristic-two +Jordan-law question; that law is expressly credited. Main #5267/#5360 do not +claim this minimal central alias. The overlap helper covered 502 open PRs +and 7,179 Discussion records with complete remote pagination; its sparse +local coverage was only 193 of 10,178 note paths. Separate Git-tree searches +covered relevant merged READMEs. Arbitrary diffs and unpublished work remain +outside that coverage. Source bytes and provenance are pinned in SOURCES.json. + +## Open next questions + +- Which extra invariant should an actual ordered-state registry retain? Start + with the full power-rank profile of S+T in this nilpotent family; a specified + consumer, representation and acquisition cost are still required. +- What is the first central alias outside the sharp nilpotent same-profile + family? Start with one explicitly named nonsharp or mixed-primary contract. + The present minima do not cover that domain, and no broader census is held. diff --git a/research/schur-central-alias/SOURCES.json b/research/schur-central-alias/SOURCES.json new file mode 100644 index 0000000000..aad1231535 --- /dev/null +++ b/research/schur-central-alias/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/schur-nilpotent-extension/README.md", + "usage": "input", + "git_blob": "1e738614a419c8f91941886179bdf235e4e5ed52", + "sha256": "7e5e74f4e5ddc1793ac6e427a80492d8d978aa78f01f189e33d2831147c9639a" + }, + { + "path": "research/schur-primary-gluing/README.md", + "usage": "input", + "git_blob": "b324f0cfc1886651d5a7954621d872dbec8a65cf", + "sha256": "dad194a3bb1211b0605a6c2667b7f40f6ba5c95efafcfa770dc1f85fbc1846d3" + }, + { + "path": "research/schur-whole-central-class/README.md", + "usage": "input", + "git_blob": "d31e16ddebadd946b92beea599dc8e743c5d7092", + "sha256": "ecf2a0ac1b9fb353ea8de8aa207af2fc3f63e97f4f6bae06b3d54bebc9ddc903" + } + ] +} diff --git a/research/schur-central-alias/TASK.json b/research/schur-central-alias/TASK.json new file mode 100644 index 0000000000..9324443c79 --- /dev/null +++ b/research/schur-central-alias/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "First central-class alias between nonconjugate sharp nilpotent ordered Schur states at the same pivot size and ordered original sector profile, in characteristic two.", + "scope_change_reason": "Original state-information obstruction; written algebraic side proof rather than a formal caller binding. The predecessor characteristic-two central law is already complete and is cited.", + "bottleneck_link": "Side result: a central-class key cannot deduplicate ordered Schur states. No paid supplier or kappa implication is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop at the first explicit collision and its minimality proof; leave other families and consumer costs open.", + "outcome": "completed", + "evidence": "PROOF.md; two literal original headers and residual pairs, explicit central intertwiner, 11 partitions and 14 comparisons, eight controls; standalone normal/optimized verifier.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which extra invariant should an actual ordered-state registry retain?", + "why_it_matters": "A complete central-class key loses ordered-state information at the stated first collision.", + "first_step": "Specify one consumer and use the full power ranks of S+T in this nilpotent family.", + "blocked_by": "No physical consumer, representation or acquisition-cost allowance is supplied." + }, + { + "question": "What is the first central alias outside the sharp nilpotent same-profile family?", + "why_it_matters": "The dimension minima are scoped, not universal idempotent-pair bounds.", + "first_step": "Name one nonsharp or mixed-primary contract before a new comparison.", + "blocked_by": "A separately bounded research claim and proof are required; no follow-on scope is held." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540664", + "playbook": "autonomous local run", + "source_question": "original", + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "requirements": "standard library only" + } +} diff --git a/research/schur-central-alias/VERIFY.json b/research/schur-central-alias/VERIFY.json new file mode 100644 index 0000000000..907203e608 --- /dev/null +++ b/research/schur-central-alias/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/schur-nilpotent-extension/README.md", + "research/schur-primary-gluing/README.md", + "research/schur-whole-central-class/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Literal original headers and sharp residuals, central intertwiner, ordered separator, first-collision partition census, rejection controls and computed source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same exact assertions enforced by explicit exceptions with optimization enabled." + } + ] +} diff --git a/research/schur-central-alias/verify.py b/research/schur-central-alias/verify.py new file mode 100644 index 0000000000..e3ccb15436 --- /dev/null +++ b/research/schur-central-alias/verify.py @@ -0,0 +1,235 @@ +"""Exact first central-key collision; standard library, no output files.""" +from __future__ import annotations + +import hashlib +import itertools +import json +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def eye(n: int) -> list[list[int]]: + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def add(a: list[list[int]], b: list[list[int]]) -> list[list[int]]: + return [[x ^ y for x, y in zip(ar, br, strict=True)] + for ar, br in zip(a, b, strict=True)] + + +def mul(a: list[list[int]], b: list[list[int]]) -> list[list[int]]: + columns = tuple(zip(*b, strict=True)) + return [[sum(x * y for x, y in zip(row, col, strict=True)) % 2 + for col in columns] for row in a] + + +def echelon(a: list[list[int]]) -> tuple[list[list[int]], list[int]]: + rows = [row[:] for row in a] + pivots: list[int] = [] + for col in range(len(rows[0])): + pivot = next((i for i in range(len(pivots), len(rows)) + if rows[i][col]), None) + if pivot is None: + continue + target = len(pivots) + rows[target], rows[pivot] = rows[pivot], rows[target] + for i in range(len(rows)): + if i != target and rows[i][col]: + rows[i] = [x ^ y for x, y in + zip(rows[i], rows[target], strict=True)] + pivots.append(col) + if len(pivots) == len(rows): + break + return rows, pivots + + +def rank(a: list[list[int]]) -> int: + return len(echelon(a)[1]) + + +def inverse(a: list[list[int]]) -> list[list[int]]: + n = len(a) + require(all(len(row) == n for row in a), "nonsquare matrix") + reduced, pivots = echelon([row + unit for row, unit in + zip(a, eye(n), strict=True)]) + require(pivots[:n] == list(range(n)), "singular matrix") + return [row[n:] for row in reduced] + + +def jordan(partition: tuple[int, ...]) -> tuple[list[list[int]], list[int]]: + require(bool(partition) and all(k > 0 for k in partition), "bad partition") + require(sum(partition) <= 8, "fixture dimension bound") + n = sum(partition) + h = [[0] * n for _ in range(n)] + bottoms: list[int] = [] + offset = 0 + for length in partition: + bottoms.append(offset) + for i in range(offset, offset + length - 1): + h[i][i + 1] = 1 + offset += length + return h, bottoms + + +def canonical_pair(partition: tuple[int, ...]) -> tuple[list[list[int]], list[list[int]]]: + h, bottoms = jordan(partition) + d, a = len(h), len(bottoms) + n = 3 * d + a + w = add(eye(d), h) + tops = [bottom + length - 1 for bottom, length in + zip(bottoms, partition, strict=True)] + s, t = [[0] * n for _ in range(n)], [[0] * n for _ in range(n)] + for i, j in itertools.product(range(d), repeat=2): + s[i][j] = s[i][2 * d + j] = h[i][j] + s[2 * d + i][j] = s[2 * d + i][2 * d + j] = w[i][j] + t[d + i][d + j] = t[d + i][2 * d + j] = h[i][j] + t[2 * d + i][d + j] = t[2 * d + i][2 * d + j] = w[i][j] + for i, top in enumerate(tops): + for matrix, row in ((s, top), (t, d + top), + (s, 2 * d + top), (t, 2 * d + top)): + matrix[row][3 * d + i] = 1 + s[3 * d + i][3 * d + i] = t[3 * d + i][3 * d + i] = 1 + return s, t + + +def literal_header(partition: tuple[int, ...]) -> tuple[list[list[int]], list[list[int]], dict]: + h, bottoms = jordan(partition) + d, a = len(h), len(bottoms) + n, m = 4 * d + a, 3 * d + a + w = add(eye(d), h) + iota = eye(d) * 3 + h + [[int(j == b) for j in range(d)] for b in bottoms] + pi = [w[i] * 3 + eye(d)[i] + [0] * a for i in range(d)] + basis = [[int(i == j) for j in range(m)] for i in range(3 * d)] + basis += [w[i] * 3 + [0] * a for i in range(d)] + basis += [[0] * (3 * d) + [int(i == j) for j in range(a)] for i in range(a)] + header = [x + y for x, y in zip(iota, basis, strict=True)] + inv = inverse(header) + pdiag = [0] * d + [1] * d + [0] * d + [1] * (d + a) + qdiag = [0] * (2 * d) + [1] * (2 * d + a) + p = mul(inv, [[v * x for x in row] for v, row in zip(pdiag, header, strict=True)]) + q = mul(inv, [[v * x for x in row] for v, row in zip(qdiag, header, strict=True)]) + require(mul(pi, iota) == eye(d), "split identity") + require(mul(p, p) == p and mul(q, q) == q, "full idempotents") + require(mul(p, q) == mul(q, p), "full commutation") + require([row[:d] for row in p[:d]] == eye(d), "P pivot") + require([row[:d] for row in q[:d]] == eye(d), "Q pivot") + require([row[:d] for row in mul(p, q)[:d]] == h, "compressed product") + residuals = [] + for matrix in (p, q): + correction = mul([row[:d] for row in matrix[d:]], [row[d:] for row in matrix[:d]]) + residuals.append(add([row[d:] for row in matrix[d:]], correction)) + return residuals[0], residuals[1], {"ambient": n, "residual": m, "sectors": [d, d, d, d + a]} + + +def power_ranks(matrix: list[list[int]]) -> list[int]: + power, result = eye(len(matrix)), [] + for _ in range(8): + power = mul(power, matrix) + result.append(rank(power)) + return result + + +def square_zero_basis(z: list[list[int]]) -> list[list[int]]: + n = len(z) + require(mul(z, z) == [[0] * n for _ in range(n)], "not square zero") + columns = [list(col) for col in zip(*z, strict=True)] + chosen: list[list[int]] = [] + for j in echelon(z)[1]: + chosen += [columns[j], eye(n)[j]] + reduced, pivots = echelon(z) + for free in range(n): + if free in pivots: + continue + vector = [int(i == free) for i in range(n)] + for row, pivot in zip(reduced, pivots): + vector[pivot] = row[free] + trial = [list(col) for col in zip(*(chosen + [vector]), strict=True)] + if rank(trial) > len(chosen): + chosen.append(vector) + require(len(chosen) == n, "incomplete Jordan basis") + return [list(row) for row in zip(*chosen, strict=True)] + + +def partitions(n: int) -> list[tuple[int, ...]]: + require(1 <= n <= 4, "partition domain") + result = [] + for length in range(1, n + 1): + for parts in itertools.combinations_with_replacement(range(1, n + 1), length): + if sum(parts) == n: + result.append(tuple(reversed(parts))) + return sorted(result, reverse=True) + + +def check_collision() -> dict: + fixtures = [] + for partition in ((3, 1), (2, 2)): + s, t, metadata = literal_header(partition) + require(mul(s, s) == s and mul(t, t) == t, "residual idempotents") + require(rank(add(mul(s, t), mul(t, s))) == 8, "not sharp") + k = add(s, t) + z = mul(k, k) + kranks, zranks = power_ranks(k), power_ranks(z) + cs, ct = canonical_pair(partition) + require(power_ranks(add(cs, ct)) == kranks, "canonical/literal mismatch") + require(zranks == [4] + [0] * 7, "central partition") + fixtures.append((s, t, z, kranks, metadata)) + require(fixtures[0][3] == [8, 4, 2] + [0] * 5, "first pair separator") + require(fixtures[1][3] == [8, 4] + [0] * 6, "second pair separator") + b0, b1 = [square_zero_basis(f[2]) for f in fixtures] + g = mul(b0, inverse(b1)) + require(rank(g) == 14 and mul(fixtures[0][2], g) == mul(g, fixtures[1][2]), "central intertwiner") + return {"fixtures": [{"partition": p, "S": f[0], "T": f[1], "K_ranks": f[3], **f[4]} + for p, f in zip(((3, 1), (2, 2)), fixtures, strict=True)], "central_intertwiner": g} + + +def check_minimality() -> dict: + collisions, comparisons, total = [], 0, 0 + for d in range(1, 5): + data = partitions(d) + total += len(data) + for left, right in itertools.combinations(data, 2): + comparisons += 1 + odd = lambda p: tuple(sum(max(k - j, 0) for k in p) for j in (1, 3, 5, 7)) + if odd(left) == odd(right): + collisions.append([left, right]) + require(collisions == [[(3, 1), (2, 2)]], "unexpected first collision") + return {"partitions": total, "comparisons": comparisons, "collisions": collisions} + + +def check_controls() -> int: + rejected = 0 + for operation in (lambda: jordan(()), lambda: jordan((0,)), + lambda: jordan((9,)), lambda: partitions(0), + lambda: inverse([[0, 0], [0, 0]]), + lambda: square_zero_basis(eye(2))): + try: + operation() + except ValueError: + rejected += 1 + require(rejected == 6, "missing input/control rejection") + s, t = canonical_pair((4,)) + require(power_ranks(mul(add(s, t), add(s, t)))[0] == 6, "distinct central control") + s, t = canonical_pair((3, 1)) + require(power_ranks(add(s, t))[2] != 0, "central-only equivalence control") + return rejected + 2 + + +def main() -> None: + scientific = {"collision": check_collision(), "minimality": check_minimality(), + "controls": check_controls()} + payload = json.dumps(scientific, sort_keys=True, separators=(",", ":")).encode() + package = Path(__file__).resolve().parent + source_hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + receipt = {"status": "PASS_SCHUR_CENTRAL_ALIAS", "evidence_sha256": hashlib.sha256(payload).hexdigest(), + "source_sha256": source_hashes, "minimality": scientific["minimality"], + "controls": scientific["controls"], "K_ranks": [x["K_ranks"] for x in scientific["collision"]["fixtures"]]} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()