diff --git a/research/block-schur-commutator/README.md b/research/block-schur-commutator/README.md new file mode 100644 index 0000000000..79790ccea5 --- /dev/null +++ b/research/block-schur-commutator/README.md @@ -0,0 +1,220 @@ +# Sharp commutator bound after a common block Schur deletion + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with finite corroboration. Deleting a common +invertible block of size d from two commuting matrices over any field produces +Schur complements whose commutator has rank at most 2d. An ordered factorization +also characterizes equality. The bound is sharp for every d, even for commuting +idempotents over F5. This answers open question 2 of Nick Petalas's merged +[PR #4278](https://github.com/CrocSwap/integer-mult-bounds/pull/4278). + +The new step is the ordered block identity and its sharpness family. The scalar +criterion and its F5 example from #4278 are cited predecessors. This is original +successor work, not an audit of that package. No new kappa is claimed. + +## Theorem + +Let K be any field, let 1 <= d < n, and split two commuting n-by-n matrices +at the same first d coordinates: + +```text +P = [[A,R],[C,D]], Q = [[B,L],[E,F]], PQ = QP = [[H,T],[W,J]], +S = D - C A^-1 R, Z = F - E B^-1 L. +``` + +Assume A and B are invertible d-by-d blocks. They need not commute with each +other or with H. Define the following matrices in the displayed order: + +```text +U = C A^-1 - E B^-1, V = A^-1 R - B^-1 L, +X = W - E B^-1 H, Y = T - H B^-1 L. +``` + +Then + +```text +[S,Z] = SZ - ZS = X V - U Y = [X U] [ V ], + [-Y ] +rank [S,Z] <= min(2d, n-d). +``` + +Here X and U have shape (n-d)-by-d, and V and Y have shape d-by-(n-d). +Moreover, rank [S,Z] = 2d exactly when [X U] has column rank 2d and [V; -Y] +has row rank 2d. Thus equality is impossible when n-d < 2d. + +For idempotent inputs, S and Z are idempotents of ranks rank(P)-d and +rank(Q)-d. Nevertheless their commutator can attain rank 2d. + +## Proof + +The block equations from PQ=QP give, with no factor interchanges, + +```text +DF = J - C L, FD = J - E R, +D E = W - C B, F C = W - E A, +R F = T - A L, L D = T - B R, +R E = H - A B, L C = H - B A. +``` + +Expand the first Schur product and substitute these equations: + +```text +SZ = DF - D E B^-1 L - C A^-1 R F + C A^-1 R E B^-1 L + = J - C L - (W-CB) B^-1 L - C A^-1 (T-AL) + + C A^-1 (H-AB) B^-1 L + = J - W B^-1 L - C A^-1 T + C A^-1 H B^-1 L. +``` + +Interchanging the two input matrices gives + +```text +ZS = J - W A^-1 R - E B^-1 T + E B^-1 H A^-1 R. +``` + +Subtract the two expressions. Expanding the proposed factors gives exactly + +```text +XV - UY = W(A^-1 R - B^-1 L) - (C A^-1 - E B^-1)T + + C A^-1 H B^-1 L - E B^-1 H A^-1 R. +``` + +The two copies of E B^-1 H B^-1 L cancel without commuting any blocks. +This proves the identity. It factors through K^(2d), so the rank is at most +2d and also at most the output dimension n-d. If both rectangular factors +have rank 2d, the right factor surjects onto K^(2d) and the left factor is +injective there, so their product has rank 2d. Conversely a product of rank +2d forces both factors to have rank at least 2d, hence exactly 2d. + +For the idempotence assertion, P^2=P gives + +```text +D^2 = D-CR, DC = C(I-A), RD = (I-A)R, RC = A(I-A). +``` + +Substitute these four identities into S^2. Since A commutes with I-A and +with A^-1, the result is S^2=D-C A^-1 R=S. Invertible block row and column +operations take P to diag(A,S), so rank(P)=d+rank(S). Apply the same argument +to Q. This step does not require P and Q to commute. + +## Sharpness for every block size + +Use the following scalar-pivot example from #4278, over F5: + +```text +P0 = [[4,3,3], [3,4,3], [3,3,4]], +Q0 = [[4,4,3], [2,2,2], [0,0,1]]. +``` + +As established there, these are commuting rank-two idempotents. Their Schur +complements have commutator + +```text +K0 = [[4,2],[3,1]], det(K0) = 3 in F5. +``` + +For any positive d, take P=P0 tensor I_d and Q=Q0 tensor I_d, with the first +d coordinates as the pivot block. The pivots are both 4 I_d and are invertible. +Block multiplication shows the Schur complements and their commutator are +the scalar counterparts tensored with I_d. In particular the commutator is +K0 tensor I_d, which is invertible in dimension 2d because its inverse is +K0^-1 tensor I_d. Its rank is 2d. The inputs are commuting rank-2d +idempotents in dimension 3d. This proves that no smaller universal bound +as a function of d is possible, including in the projector subclass. + +## Evidence and reproduction + +The self-contained [verify.py](verify.py) imports no predecessor executable. +It compares the ordered factorization with the directly multiplied Schur +commutator, computes both rectangular ranks, and tests idempotence and rank +drops in the projector cases. Its complete finite domains are: + +- Every P in M4(F2), with Q=P^2 and a size-two pivot. Of 65,536 candidates, + 11,904 have both pivots invertible. Their commutator ranks are 0 in 10,392 + cases and 2 in 1,512 cases. In 4,032 admitted cases A and B do not commute. +- Every P in M3(F3), with Q=P^2 and a size-two pivot. Of 19,683 candidates, + 8,208 are admitted, all with zero commutator in their one-dimensional + Schur space. In 5,184 admitted cases A and B do not commute. +- Every G in GL4(F2), conjugating the coordinate projectors with masks 7 + and 11. Among all 20,160 headers, 4,032 admit both size-two pivots. The + Schur commutator has rank 0 in 2,304 cases and rank 1 in 1,728 cases. + These are header occurrences, not distinct projector-pair counts. +- The tensor family at d=1,2,3,4 over F5, attaining commutator rank 2d. +- Four boundary controls reject a singular pivot, malformed shape, exceeded + matrix capacity and noncommuting inputs. Four formula controls distinguish + an incorrect order of H and B^-1, omitted H corrections, an incorrect plus + sign and the false premise that admitted pivot blocks must commute. + +The polynomial domains enumerate only the specified pairs (P,P^2), not all +commuting pairs. The finite checks corroborate the written universal proof. +The generated stdout receipt binds every package file by SHA256; no stored +or handwritten receipt is supplied, and the verifier writes no files. + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/block-schur-commutator/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/block-schur-commutator/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/block-schur-commutator +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/block-schur-commutator --check-source-history +``` + +The scientific marker is `PASS_BLOCK_SCHUR_COMMUTATOR`. Another CPython 3.12 +path may replace the local interpreter. VERIFY.json registers both scientific +modes with 120-second timeouts. Every check uses explicit exceptions and +remains active under -O. SOURCES.json pins historical provenance, including +the predecessor README; no external live input is required. + +## Limits and code constraints + +This is a field-algebra proof with finite corroboration, not a formal-kernel +result or a complete multiplication theorem. Independent human and formal +proof-kernel review are unclaimed. It treats one common deletion with both +pivot blocks invertible. It does not classify subsequent simultaneous orbits, +count passing complete headers, extend rank claims to rings, or provide a +producer, header selection/emission, dispatch, dirty return, stock, precision +or complete physical invoice. Those costs remain unknown. The selected +frontier is unchanged; selected cold replay, Lean and Docker were not run. + +The verifier uses direct calls, no recursion, no subprocesses and no dynamic +code generation. All functions are below 60 physical lines. Matrices have at +most 12 rows and 12 columns; each exhaustive outer scan has at most 65,536 +candidates, and the tensor scan has four cases. Gaussian elimination has at +most 12 pivot rounds. Its temporary augmented rows have at most 24 entries. +The file-hash receipt has at most eight files. Finite scan counters and ranks +are kept locally and invalid inputs raise explicit exceptions. Warnings are +errors in both registered modes; local AST syntax and function-size inspection +supplements execution. No external static analyzer is installed. + +Power of Ten rule 3 deviation: CPython allocates tuples, integers and temporary +rows during arithmetic. The fixed matrix and scan capacities above bound live +state; matrices from exhaustive scans are discarded each iteration, retaining +only counters and the first witness. Both registered modes exercise those +bounds, and the capacity control rejects a 13-column matrix. A fixed-allocation +implementation would be a separate port if this verifier entered a long-lived +or native execution path. + +## Open next questions + +1. Can the changing Schur-pair state be classified by the ordered factors up + to simultaneous conjugacy? A header-density recursion needs more than the + rank bound. Start with size-two pivots and two rank-three projectors in + dimension four. The present factors do not classify their orbit. +2. What is the sharp projector bound for fixed input ranks and a fixed field, + especially F2? The F5 construction proves universal sharpness but does not + give attainment in every field. Start with block-diagonal lifts of binary + examples and compare rank restrictions on the two residual projectors. + +## Credit and relation to the research bottleneck + +Nick Petalas's #4278 supplies the scalar identity, the scalar F5 sharpness +example and the explicit block-pivot question. Nick Petalas's #4259 supplies +the laminar shared-header context, and #4228 supplies the single-projector +Schur framework. Cinna Davis's #4100 supplies the BIT request/complete-header +context. Those predecessors retain their credit; no predecessor file changes. + +This is a side result with scope changed from `uniform-transfer-audit` to an +original open interface question. It bounds the noncommutativity created by a +wider elimination step, without assuming the pivot blocks commute. It closes +no actual-caller admission or all-size transfer obligation. This package starts +no further construction campaign and treats no unknown consumer cost as zero. diff --git a/research/block-schur-commutator/SOURCES.json b/research/block-schur-commutator/SOURCES.json new file mode 100644 index 0000000000..6c33dd1c64 --- /dev/null +++ b/research/block-schur-commutator/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/schur-commutator-criterion/README.md", + "usage": "provenance", + "git_blob": "6b37342de04f5c42c198dd6ba14cea9845be6f05", + "sha256": "5616da2e708a8425f1bf0bf5c89c236ef8ed0a23d0544d30ae2142ffe167dc01" + } + ] +} diff --git a/research/block-schur-commutator/TASK.json b/research/block-schur-commutator/TASK.json new file mode 100644 index 0000000000..7738c51f26 --- /dev/null +++ b/research/block-schur-commutator/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the ordered block Schur commutator identity, the 2d rank bound and its sharpness for every d, including commuting idempotents.", + "scope_change_reason": "The user asks for an original contribution, not an audit. This takes open question 2 of merged PR4278, a side interface theorem, rather than rechecking PR4100.", + "bottleneck_link": "Side structural result for wider BIT shared-header elimination. It bounds the noncommutative defect; actual producer, header and consumer costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact block identity and sharp rank bound after bounded finite corroboration. Do not extend to orbit classification or header densities.", + "outcome": "completed", + "evidence": "README.md contains the ordered field-algebra proof and tensor sharpness construction; verify.py checks complete polynomial and projector-header domains, sharp examples and explicit controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Classify simultaneous Schur-pair states using the ordered low-rank factors.", + "why_it_matters": "A future header-density recursion needs a complete state class, not just the commutator rank.", + "first_step": "Classify size-two deletions of two rank-three projectors in dimension four.", + "blocked_by": "The displayed factorization does not determine a simultaneous conjugacy orbit." + }, + { + "question": "Determine sharp projector bounds with fixed ranks and a fixed field, particularly F2.", + "why_it_matters": "Universal sharpness over F5 does not settle field-specific attainable ranks.", + "first_step": "Lift binary examples block diagonally and compare residual projector rank constraints.", + "blocked_by": "This package does not classify all fixed-field projector pairs." + } + ] +} diff --git a/research/block-schur-commutator/VERIFY.json b/research/block-schur-commutator/VERIFY.json new file mode 100644 index 0000000000..f1fa57c708 --- /dev/null +++ b/research/block-schur-commutator/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Ordered block Schur identity, rectangular rank equivalence, complete bounded polynomial/projector-header domains, tensor sharpness, boundary and formula controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Ordered block Schur identity, rectangular rank equivalence, complete bounded polynomial/projector-header domains, tensor sharpness, boundary and formula controls." + } + ] +} diff --git a/research/block-schur-commutator/verify.py b/research/block-schur-commutator/verify.py new file mode 100644 index 0000000000..86f4de84c2 --- /dev/null +++ b/research/block-schur-commutator/verify.py @@ -0,0 +1,258 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the block Schur theorem. Apache-2.0.""" +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(rows): + result = tuple(tuple(row) for row in rows) + require(1 <= len(result) <= 12, "row capacity") + require(1 <= len(result[0]) <= 12, "column capacity") + require(all(len(row) == len(result[0]) for row in result), "ragged matrix") + return result + + +def mul(a, b, q): + require(len(a[0]) == len(b), "product shape") + return matrix([[sum(a[i][k] * b[k][j] for k in range(len(b))) % q + for j in range(len(b[0]))] for i in range(len(a))]) + + +def sub(a, b, q): + require(len(a) == len(b) and len(a[0]) == len(b[0]), "difference shape") + return matrix([[(x-y) % q for x, y in zip(ar, br)] for ar, br in zip(a, b)]) + + +def rank(a, q): + rows = [list(row) for row in a] + r = 0 + for col in range(len(a[0])): + pivots = [i for i in range(r, len(rows)) if rows[i][col]] + if not pivots: + continue + i = pivots[0] + rows[r], rows[i] = rows[i], rows[r] + inv = pow(rows[r][col], -1, q) + rows[r] = [x*inv % q for x in rows[r]] + for i in range(r+1, len(rows)): + scale = rows[i][col] + rows[i] = [(x-scale*y) % q for x, y in zip(rows[i], rows[r])] + r += 1 + return r + + +def inverse(a, q): + n = len(a) + require(n == len(a[0]), "inverse shape") + rows = [list(row) + [int(i == j) for j in range(n)] for i, row in enumerate(a)] + for col in range(n): + pivots = [i for i in range(col, n) if rows[i][col]] + if not pivots: + return None + i = pivots[0] + rows[col], rows[i] = rows[i], 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: + scale = rows[i][col] + rows[i] = [(x-scale*y) % q for x, y in zip(rows[i], rows[col])] + return matrix([row[n:] for row in rows]) + + +def blocks(p, d): + require(len(p) == len(p[0]) and 0 < d < len(p), "pivot shape") + return (matrix([row[:d] for row in p[:d]]), + matrix([row[d:] for row in p[:d]]), + matrix([row[:d] for row in p[d:]]), + matrix([row[d:] for row in p[d:]])) + + +def schur(p, d, q): + a, r, c, z = blocks(p, d) + ai = inverse(a, q) + require(ai is not None, "singular pivot") + return sub(z, mul(mul(c, ai, q), r, q), q) + + +def factors(p, z, d, q): + a, r, c, _ = blocks(p, d) + b, s, e, _ = blocks(z, d) + h, t, w, _ = blocks(mul(p, z, q), d) + ai, bi = inverse(a, q), inverse(b, q) + require(ai is not None and bi is not None, "factor pivots") + ca, eb = mul(c, ai, q), mul(e, bi, q) + ar, bs = mul(ai, r, q), mul(bi, s, q) + u, v = sub(ca, eb, q), sub(ar, bs, q) + x = sub(w, mul(eb, h, q), q) + y = sub(t, mul(h, bs, q), q) + return x, v, u, y + + +def inspect(p, z, d, q, idempotents=False): + require(mul(p, z, q) == mul(z, p, q), "commuting input premise") + s, t = schur(p, d, q), schur(z, d, q) + actual = sub(mul(s, t, q), mul(t, s, q), q) + x, v, u, y = factors(p, z, d, q) + predicted = sub(mul(x, v, q), mul(u, y, q), q) + require(actual == predicted, "ordered factorization") + left = matrix([list(xr)+list(ur) for xr, ur in zip(x, u)]) + right = matrix(list(v)+[tuple(-value % q for value in row) for row in y]) + r = rank(actual, q) + require(actual == mul(left, right, q), "rectangular factorization") + require(r <= min(2*d, len(p)-d), "block rank bound") + require((r == 2*d) == (rank(left, q) == rank(right, q) == 2*d), + "full rank equivalence") + if idempotents: + require(mul(p, p, q) == p and mul(z, z, q) == z, "projector inputs") + require(mul(s, s, q) == s and mul(t, t, q) == t, "Schur idempotents") + require(rank(s, q) == rank(p, q)-d, "first rank drop") + require(rank(t, q) == rank(z, q)-d, "second rank drop") + return r + + +def polynomial_census(n, d, q): + counts = Counter() + noncommuting_pivots = 0 + first = None + require(q**(n*n) <= 65536, "census capacity") + for entries in product(range(q), repeat=n*n): + p = matrix([entries[i*n:(i+1)*n] for i in range(n)]) + z = mul(p, p, q) + a, _, _, _ = blocks(p, d) + b, _, _, _ = blocks(z, d) + if inverse(a, q) is None or inverse(b, q) is None: + continue + r = inspect(p, z, d, q) + counts[r] += 1 + if mul(a, b, q) != mul(b, a, q): + noncommuting_pivots += 1 + if first is None: + first = {"P": p, "Q": z, "rank": r} + return {"n": n, "d": d, "q": q, "candidate_matrices": q**(n*n), + "ranks": dict(sorted(counts.items())), + "noncommuting_pivots": noncommuting_pivots, "first_witness": first} + + +def conjugate(g, gi, mask, q): + n = len(g) + return matrix([[sum(g[i][k]*gi[k][j] for k in range(n) if mask >> k & 1) % q + for j in range(n)] for i in range(n)]) + + +def projector_orbit(): + counts = Counter() + headers = 0 + for entries in product(range(2), repeat=16): + g = matrix([entries[i*4:(i+1)*4] for i in range(4)]) + gi = inverse(g, 2) + if gi is None: + continue + headers += 1 + p, z = conjugate(g, gi, 7, 2), conjugate(g, gi, 11, 2) + if inverse(blocks(p, 2)[0], 2) is not None and inverse(blocks(z, 2)[0], 2) is not None: + counts[inspect(p, z, 2, 2, True)] += 1 + require(headers == 20160, "complete GL4(F2) cover") + return {"headers": headers, "q": 2, "n": 4, "d": 2, + "projector_masks": [7, 11], "ranks": dict(sorted(counts.items()))} + + +def tensor_identity(p, d): + return matrix([[p[i//d][j//d]*int(i % d == j % d) + for j in range(len(p)*d)] for i in range(len(p)*d)]) + + +def sharp_examples(): + p = ((4, 3, 3), (3, 4, 3), (3, 3, 4)) + z = ((4, 4, 3), (2, 2, 2), (0, 0, 1)) + result = [] + for d in range(1, 5): + pp, zz = tensor_identity(p, d), tensor_identity(z, d) + r = inspect(pp, zz, d, 5, True) + require(r == 2*d, "sharp tensor rank") + require(rank(pp, 5) == rank(zz, 5) == 2*d, "sharp input ranks") + result.append({"q": 5, "n": 3*d, "d": d, "rank": r}) + return result + + +def boundary_controls(): + zero = ((0, 0), (0, 0)) + rejected = 0 + for operation in ("singular", "shape", "capacity", "premise"): + try: + if operation == "singular": + schur(zero, 1, 2) + elif operation == "shape": + blocks(((1, 0),), 1) + elif operation == "capacity": + matrix([[0]*13]) + else: + inspect(((1, 1), (0, 0)), ((1, 0), (1, 0)), 1, 3) + except ValueError: + rejected += 1 + require(rejected == 4, "invalid-input controls") + return rejected + + +def mutation_controls(domains): + order = correction = premise = False + for domain in domains: + w = domain["first_witness"] + if w is None: + continue + p, z, d, q = w["P"], w["Q"], domain["d"], domain["q"] + x, v, u, y = factors(p, z, d, q) + s, t = schur(p, d, q), schur(z, d, q) + actual = sub(mul(s, t, q), mul(t, s, q), q) + uy = mul(u, y, q) + a, _, _, _ = blocks(p, d) + b, _, e, _ = blocks(z, d) + h, ht, hw, _ = blocks(mul(p, z, q), d) + bi = inverse(b, q) + wrong_x = sub(hw, mul(mul(e, h, q), bi, q), q) + order |= actual != sub(mul(wrong_x, v, q), uy, q) + correction |= actual != sub(mul(hw, v, q), mul(u, ht, q), q) + premise |= mul(a, b, q) != mul(b, a, q) + require(order, "moving H past B inverse must fail") + require(premise, "noncommuting pivot blocks must be exercised") + # Odd characteristic makes the sign control observable in the sharp example. + p, z = ((4, 3, 3), (3, 4, 3), (3, 3, 4)), ((4, 4, 3), (2, 2, 2), (0, 0, 1)) + x, v, u, y = factors(p, z, 1, 5) + xv, uy = mul(x, v, 5), mul(u, y, 5) + plus = matrix([[(a+b) % 5 for a, b in zip(ar, br)] for ar, br in zip(xv, uy)]) + require(sub(xv, uy, 5) != plus, "plus-sign mutation differs") + _, ht, hw, _ = blocks(mul(p, z, 5), 1) + s, t = schur(p, 1, 5), schur(z, 1, 5) + actual = sub(mul(s, t, 5), mul(t, s, 5), 5) + correction |= actual != sub(mul(hw, v, 5), mul(u, ht, 5), 5) + require(correction, "omitting H corrections must fail") + return 4 + + +def main(): + domains = [polynomial_census(n, d, q) for n, d, q in ((4, 2, 2), (3, 2, 3))] + require(all(domain["noncommuting_pivots"] > 0 for domain in domains), + "genuine block cases in both fields") + result = {"polynomial_domains": domains, "projector_orbit": projector_orbit(), + "sharp_examples": sharp_examples(), "boundary_controls": boundary_controls(), + "mutation_controls": mutation_controls(domains)} + package = Path(__file__).resolve().parent + files = sorted(p for p in package.iterdir() if p.is_file()) + require(len(files) <= 8, "package receipt capacity") + result["package_sha256"] = {p.name: sha256(p.read_bytes()).hexdigest() for p in files} + canonical = json.dumps(result, sort_keys=True, separators=(",", ":")).encode() + result["receipt_sha256"] = sha256(canonical).hexdigest() + print("PASS_BLOCK_SCHUR_COMMUTATOR") + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()