From 9f053f7051e5fc3327d4337bb4bd8ac52cf5fcd0 Mon Sep 17 00:00:00 2001 From: lizhi Date: Thu, 22 Oct 2026 21:17:49 +0800 Subject: [PATCH] Prove optimal binary Schur sharpness dimension 3d for d >= 2 Give an explicit d=3, n=9 commuting-idempotent pair and a block-algebra construction for every odd d >= 3, also covering even d. The dimension lower bound is attained. Credit Nick Petalas and Ryanson Jonathan for the predecessor bound, binary examples and minimal-dimension question. Prepared with substantial OpenAI Codex assistance. --- .../binary-schur-minimal-dimension/README.md | 312 ++++++++++++++++++ .../SOURCES.json | 18 + .../binary-schur-minimal-dimension/TASK.json | 112 +++++++ .../VERIFY.json | 32 ++ .../binary-schur-minimal-dimension/verify.py | 214 ++++++++++++ 5 files changed, 688 insertions(+) create mode 100644 research/binary-schur-minimal-dimension/README.md create mode 100644 research/binary-schur-minimal-dimension/SOURCES.json create mode 100644 research/binary-schur-minimal-dimension/TASK.json create mode 100644 research/binary-schur-minimal-dimension/VERIFY.json create mode 100644 research/binary-schur-minimal-dimension/verify.py diff --git a/research/binary-schur-minimal-dimension/README.md b/research/binary-schur-minimal-dimension/README.md new file mode 100644 index 0000000000..c7acbef834 --- /dev/null +++ b/research/binary-schur-minimal-dimension/README.md @@ -0,0 +1,312 @@ +# Optimal binary Schur sharpness dimension: n = 3d for every d >= 2 + +**Written algebraic theorem with exact finite corroboration. No new kappa.** +Prepared by **lee-phys**, with substantial OpenAI Codex assistance, under +Apache-2.0. This resolves the minimal-dimension question left by +[PR4617](https://github.com/CrocSwap/integer-mult-bounds/pull/4617) for every +d >= 2 in its invertible-block setting. + +The requested first case, d = 3 and n = 9, has an explicit witness below. +A single block construction then handles every odd d >= 3 and every even d >= 2. +The proof uses only binary matrix algebra and two fixed seed matrices. + +## 1. Statement and conventions + +All matrices are over the field $\mathbb F_2$ and act on column vectors. +Addition and subtraction coincide. A projector means an algebraic idempotent, +not an orthogonal or symmetric projector. + +For an n-by-n matrix with a common coordinate split d + (n-d), write + +$$ +X=\begin{pmatrix}A&B\\ C&D\end{pmatrix}, \qquad +\operatorname{Sch}_d(X)=D-CA^{-1}B, +$$ + +when A is invertible. Define $[S,Z]=SZ-ZS$. + +**Theorem.** For every integer d >= 2, the smallest ambient dimension n for +which there exist commuting idempotents P,Q with invertible leading d-by-d +blocks and + +$$ +\operatorname{rank}[\operatorname{Sch}_d(P),\operatorname{Sch}_d(Q)]=2d +$$ + +is exactly n = 3d. The construction has +$\operatorname{rank}P=\operatorname{rank}Q=2d$ and equal leading blocks. +These blocks are invertible; they are **not required to be identity matrices**. + +The rank bound 2d for general commuting pairs is the predecessor result of +Nick Petalas, [PR4597](https://github.com/CrocSwap/integer-mult-bounds/pull/4597). +For the minimum-dimension theorem here, the necessary bound follows directly +from size: the commutator is (n-d)-by-(n-d), so rank 2d requires n-d >= 2d. +It remains to construct a pair at n = 3d. + +The case d = 1 is outside the new theorem. Ryanson Jonathan's +[PR4609](https://github.com/CrocSwap/integer-mult-bounds/pull/4609) reports +minimum n = 5 over $\mathbb F_2$ for that case. That negative classification +is credited, not independently repeated here. + +## 2. Construction from a matrix without eigenvalues 0 or 1 + +The construction isolates the compatibility between P and Q in their deleted +block. After elimination, the two surviving blocks are coupled by an invertible +matrix R. We arrange that both R and R+I are invertible, which makes their Schur +commutator invertible too. + +Let T be any d-by-d binary matrix for which T and $A=I+T$ are both invertible. +In three blocks of size d, set + +$$ +P=\begin{pmatrix} + A&A&T\\ + T&T&T\\ + 0&0&I +\end{pmatrix}, +\qquad +Q=\begin{pmatrix} + A&T&A\\ + 0&I&0\\ + T&T&T +\end{pmatrix}. \tag{1} +$$ + +Their leading blocks are both A. We now verify all remaining properties. + +### Idempotence, commutation and projector ranks + +Introduce the rectangular matrices + +$$ +L=\begin{pmatrix}I\\I\\0\end{pmatrix},\quad +M=\begin{pmatrix}I\\0\\I\end{pmatrix},\quad +F=\begin{pmatrix}T&A&T\end{pmatrix},\quad +G=\begin{pmatrix}T&T&A\end{pmatrix}. +$$ + +Because T+A=I and T+T=0, + +$$ +FL=GM=I,\qquad FM=GL=0. +$$ + +Directly expanding (1) gives $P=I_{3d}+LF$ and $Q=I_{3d}+MG$. +Consequently, + +$$ +(LF)^2=L(FL)F=LF,\qquad (MG)^2=M(GM)G=MG, +$$ + +and $LF\,MG=L(FM)G=0$, $MG\,LF=M(GL)F=0$. Thus + +$$ +P^2=P,\quad Q^2=Q,\quad PQ=I_{3d}+LF+MG=QP. +$$ + +Since FL=I, L is injective and LF is a projector of rank d. +The kernel of $I_{3d}+LF$ is exactly the image of LF: if +$x=LFx$ then x is in that image, and every vector in that image is fixed by LF. +Hence P has rank 3d-d=2d. The same argument applies to Q. + +### Schur complements + +T commutes with A=I+T and therefore with its inverse. Put $R=TA^{-1}$. +For P, the off-diagonal blocks at the d + 2d split are +$B_P=(A\ T)$ and $C_P=(T\ 0)^{\mathsf T}$, giving + +$$ +\begin{aligned} +S=\operatorname{Sch}_d(P) +&=\begin{pmatrix}T&T\\0&I\end{pmatrix} + +\begin{pmatrix}T\\0\end{pmatrix}A^{-1} + \begin{pmatrix}A&T\end{pmatrix}\\ +&=\begin{pmatrix}0&T+TA^{-1}T\\0&I\end{pmatrix} + =\begin{pmatrix}0&R\\0&I\end{pmatrix}. +\end{aligned} +$$ + +The last equality uses +$T+TA^{-1}T=TA^{-1}(A+T)=TA^{-1}$. +Likewise, with $B_Q=(T\ A)$ and $C_Q=(0\ T)^{\mathsf T}$, + +$$ +Z=\operatorname{Sch}_d(Q)=\begin{pmatrix}I&0\\R&0\end{pmatrix}. +$$ + +In particular, S and Z are idempotent. Their commutator is + +$$ +K=[S,Z]=\begin{pmatrix}R^2&R\\R&R^2\end{pmatrix}. \tag{2} +$$ + +Here R is invertible and + +$$ +R+I=(T+A)A^{-1}=A^{-1} +$$ + +is invertible. In characteristic two, the cross terms in the square of (2) +cancel, so + +$$ +K^2= +\begin{pmatrix} +R^2(R+I)^2&0\\ +0&R^2(R+I)^2 +\end{pmatrix}. \tag{3} +$$ + +Both diagonal blocks are invertible. Therefore K is invertible and has rank +2d. This proves the construction lemma for every admissible T, without any +assumption that T is diagonalizable or belongs to a field extension. + +## 3. The requested d = 3, n = 9 witness + +Take + +$$ +T_3=\begin{pmatrix}0&0&1\\1&0&1\\0&1&0\end{pmatrix}. +$$ + +Direct multiplication gives $T_3^3+T_3+I=0$, hence + +$$ +T_3(T_3^2+I)=I,\qquad (T_3+I)(T_3^2+T_3)=I. +$$ + +Thus both T_3 and I+T_3 are invertible. Inserting T_3 into (1) yields the +following matrices. Each binary string is one row in left-to-right column +order; multiplication is modulo two. + + P9 Q9 + 101101001 101001101 + 111111101 111101111 + 011011010 011010011 + 001001001 000100000 + 101101101 000010000 + 010010010 000001000 + 000000100 001001001 + 000000010 101101101 + 000000001 010010010 + +Deleting the first three coordinates gives the commutator + + K6 + 101111 + 111100 + 011110 + 111101 + 100111 + 110011 + +Equation (3) proves its invertibility; direct binary elimination independently +checks rank 6 in the accompanying verifier. P9 and Q9 both have rank 6. + +## 4. Every odd d, then all d >= 2 + +Use also the two-dimensional seed + +$$ +T_2=\begin{pmatrix}0&1\\1&1\end{pmatrix}. +$$ + +It satisfies $T_2^2+T_2+I=0$, so $T_2(T_2+I)=I$. Therefore T_2 and I+T_2 +are invertible. + +For odd d=3+2k with k >= 0, choose + +$$ +T=T_3\oplus T_2^{\oplus k}. +$$ + +For even d=2k with k >= 1, choose $T=T_2^{\oplus k}$. +In each case T and I+T are block diagonal with invertible blocks. +Section 2 therefore produces the required pair in dimension 3d. +Together with the size lower bound, this proves the theorem. + +Appending equal zero blocks to P and Q also attains rank 2d at every n > 3d +with the same leading d-coordinate split. This does not address all possible +projector ranks or prescribe the leading blocks to be identity. + +## 5. What is new, and what is checked + +- **Predecessor #4597:** ordered block-Schur commutator identity and the 2d + bound, with sharpness over $\mathbb F_5$. +- **Predecessor #4609:** binary examples at (n,d)=(5,1) and (6,2), and small + minimal-dimension results. Its d=2 example already yields optimal even d + by direct sums and a coordinate permutation. +- **Predecessor #4617:** uniform binary sharpness at n=5d, leaving minimal n + open. The new part here is the explicit optimal d=3 example and the + block-algebra proof closing every odd d>=3; the same formula covers even d. + +Exact heads inspected: + +| PR | Contributor | Head | +|---|---|---| +| [4597](https://github.com/CrocSwap/integer-mult-bounds/pull/4597) | Nick Petalas | dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb | +| [4609](https://github.com/CrocSwap/integer-mult-bounds/pull/4609) | Ryanson Jonathan | eb5ccf9288808d973551e6264300d30d2f6e48a0 | +| [4617](https://github.com/CrocSwap/integer-mult-bounds/pull/4617) | Ryanson Jonathan | 96c01a2124e234d798e9e97643c20fb5b430840d | + +The standalone verifier independently computes full-matrix products, inverses, +Schur complements and ranks. It checks the literal 9-by-9 witness, the block +formula for d=2 through 12, and one larger-ambient padding. It exhausts all +16 binary 2-by-2 and all 512 binary 3-by-3 seed matrices: respectively 2 and +48 have both T and I+T invertible, and every such seed passes the full checks. +This enumerates seeds for our family, not all projector pairs. + +Six rejecting controls preserve or break distinct hypotheses: a singular +leading block; zero T; nonzero singular T; identical projectors with zero +commutator; a bit change destroying idempotence; and a separately conjugated +projector retaining idempotence and its invertible pivot but losing commutation. +Checks remain active under optimized Python. + +The universal result is proved in Sections 1-4, not extrapolated from the finite +checks. This is author-checked work with substantial AI assistance; independent +human review and formal proof-kernel verification are not claimed. + +## 6. Reproduce and scope + +From the repository root, using Python 3.12 and the standard library: + + python3.12 -W error -B research/binary-schur-minimal-dimension/verify.py + python3.12 -W error -O -B research/binary-schur-minimal-dimension/verify.py + python3.12 -B scripts/research_package.py --package research/binary-schur-minimal-dimension --check-only + python3.12 -B scripts/research_package.py --package research/binary-schur-minimal-dimension + +Expected direct marker: PASS_BINARY_SCHUR_MINIMAL_DIMENSION. +The registered runner additionally reports PASS_REGISTERED_RESEARCH_PACKAGE. + +The proof and verifier are self-contained. No pending predecessor executable, +matrix file, or external library is a live input. SOURCES.json pins the task +catalogue and selected record only as historical provenance at main +fbc9ea0249746acca4f504d4fda2b84e0e36cf0d; neither enters the theorem. +TASK.json records the donor's explicit scope and the original card. + +This is a local algebraic interface result in the block-Schur line arising +from BIT/header work. It does not provide a header density, physical caller, +supplier admission or an improved integer-multiplication exponent. The +selected construction, full scientific replay, Lean and Docker are outside +the verification scope. The optional full-history preflight is not run in +this shallow checkout. + +## Open next questions + +**What changes if both leading blocks must equal I_d?** The present construction +uses A=I+T, and setting A=I in this family forces T=0 and destroys sharpness. +That observation excludes only this parametrization. The predecessor n=5d +construction has identity pivots, so existence is known with more room. + +This question separates arbitrary invertible pivots from a stronger interface. +Start by deriving the block identities forced by P^2=P, Q^2=Q and both pivots I_d, +then test whether they obstruct rank 2d at n=3d. A sharp result for that additional +constraint is not supplied here. The same question is structured in TASK.json. + +## Credit + +Nick Petalas supplies the block-Schur bound and its predecessor PR4278. +Ryanson Jonathan supplies the binary witnesses, the n=5d construction and the +minimal-dimension question, with Claude Code assistance as credited in those +packages. The present construction, written proof and standalone verifier were +prepared by lee-phys with substantial OpenAI Codex assistance. No predecessor +code or data is copied into this package. Apache-2.0. diff --git a/research/binary-schur-minimal-dimension/SOURCES.json b/research/binary-schur-minimal-dimension/SOURCES.json new file mode 100644 index 0000000000..9b3d9dc421 --- /dev/null +++ b/research/binary-schur-minimal-dimension/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "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" + } + ] +} diff --git a/research/binary-schur-minimal-dimension/TASK.json b/research/binary-schur-minimal-dimension/TASK.json new file mode 100644 index 0000000000..40ee5e85d6 --- /dev/null +++ b/research/binary-schur-minimal-dimension/TASK.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "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": "User-assigned original algebraic theorem: first construct binary commuting idempotents for d=3,n=9 with invertible leading blocks and Schur commutator rank 6; then prove optimal n=3d for every odd d>=3. The same family covers all d>=2.", + "scope_change_reason": "The donor explicitly chose the minimal-dimension question left by PR4617 instead of another maintenance task. This is a written constructive theorem and exact finite corroboration, not a Lean formalization or a random task-picker assignment.", + "bottleneck_link": "A local algebraic interface result in the block-Schur/BIT header line of PR4278 and PR4597. It resolves the minimal dimension for attaining rank 2d, but supplies no header density, physical caller or new multiplication exponent.", + "budget_minutes": 60, + "stop_rule": "Stop after the optimal-dimension theorem, explicit d=3 witness, self-contained proof, meaningful exact checks and a focused PR. Do not expand into a density census, identity-pivot classification, selected scientific replay, Lean or Docker.", + "outcome": "completed", + "evidence": "README.md Sections 1-4 prove n_min(d)=3d for every d>=2. verify.py checks the explicit 9x9 witness, d=2..12, one padding, all 16/512 seeds in dimensions 2/3 (2/48 admissible), and six rejecting controls.", + "author": "lee-phys", + "ai_assistance": "Substantial OpenAI Codex assistance in deriving the construction, writing the proof and verifier, checking algebra and preparing the contribution. No independent human or formal proof-kernel review is claimed.", + "open_questions": [ + { + "question": "What is the minimal ambient dimension for rank 2d when both leading d-by-d blocks are required to equal I_d?", + "why_it_matters": "Separates arbitrary invertible pivots from the stronger identity-pivot interface; PR4617 supplies an n=5d upper bound while this optimal n=3d construction uses a nonidentity pivot.", + "first_step": "Derive the block annihilation relations from idempotence with identity leading blocks, then test whether they forbid full Schur commutator rank at n=3d.", + "blocked_by": "The current parametrization degenerates at identity pivot; a general lower bound or different construction is needed." + } + ], + "predecessors": [ + { + "pr": 4597, + "head": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "credit": "Nick Petalas: block-Schur rank bound and predecessor PR4278." + }, + { + "pr": 4609, + "head": "eb5ccf9288808d973551e6264300d30d2f6e48a0", + "credit": "Ryanson Jonathan: binary witnesses and small minimal-dimension classification." + }, + { + "pr": 4617, + "head": "96c01a2124e234d798e9e97643c20fb5b430840d", + "credit": "Ryanson Jonathan: uniform binary n=5d construction and minimal-dimension open question." + } + ] +} diff --git a/research/binary-schur-minimal-dimension/VERIFY.json b/research/binary-schur-minimal-dimension/VERIFY.json new file mode 100644 index 0000000000..faebb6389f --- /dev/null +++ b/research/binary-schur-minimal-dimension/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": 30, + "checks": "Literal d=3 witness, general block formulas, finite d=2..12, exhaustive small seeds, and six hypothesis/failure controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "The same exact checks and rejection controls with Python assertions disabled." + } + ] +} diff --git a/research/binary-schur-minimal-dimension/verify.py b/research/binary-schur-minimal-dimension/verify.py new file mode 100644 index 0000000000..de56e4d16e --- /dev/null +++ b/research/binary-schur-minimal-dimension/verify.py @@ -0,0 +1,214 @@ +#!/usr/bin/env python3 +"""Exact binary checks for the written minimal-dimension theorem in README.md. + +Matrices are tuples of row bitsets: bit j is column j, acting on column vectors. +No predecessor verifier or third-party arithmetic is imported. Finite checks +corroborate, but do not replace, the proof for every d >= 2. +lee-phys, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def add(a, b): + require(len(a) == len(b), "addition row count") + return tuple(x ^ y for x, y in zip(a, b)) + + +def multiply(a, b): + result = [] + for row in a: + total = 0 + while row: + bit = row & -row + total ^= b[bit.bit_length() - 1] + row ^= bit + result.append(total) + return tuple(result) + + +def rank(a): + pivots = {} + for row in a: + while row: + col = row.bit_length() - 1 + if col not in pivots: + pivots[col] = row + break + row ^= pivots[col] + return len(pivots) + + +def inverse(a): + n = len(a) + rows = [row | (1 << (n + i)) for i, row in enumerate(a)] + for col in range(n): + pivot = next((i for i in range(col, n) if (rows[i] >> col) & 1), None) + if pivot is None: + return None + rows[col], rows[pivot] = rows[pivot], rows[col] + for i in range(n): + if i != col and (rows[i] >> col) & 1: + rows[i] ^= rows[col] + return tuple(row >> n for row in rows) + + +def block(a, r0, r1, c0, c1): + return tuple((row >> c0) & ((1 << (c1 - c0)) - 1) for row in a[r0:r1]) + + +def direct_sum(parts): + rows, offset = [], 0 + for part in parts: + rows.extend(row << offset for row in part) + offset += len(part) + return tuple(rows) + + +def join_blocks(grid, d): + return tuple(sum(part[i] << (j * d) for j, part in enumerate(row)) + for row in grid for i in range(d)) + + +T2 = (2, 3) # rows 01, 11; T2^2 + T2 + I = 0 +T3 = (4, 5, 2) # rows 001, 101, 010; T3^3 + T3 + I = 0 + + +def seed(d): + require(type(d) is int and d >= 2, "seed dimension must be at least two") + return direct_sum(([T3] if d % 2 else []) + [T2] * ((d - 3) // 2 if d % 2 else d // 2)) + + +def pair_from_t(t): + d = len(t) + unit, zero = identity(d), (0,) * d + a = add(unit, t) + p = join_blocks(((a, a, t), (t, t, t), (zero, zero, unit)), d) + q = join_blocks(((a, t, a), (zero, unit, zero), (t, t, t)), d) + return p, q + + +def schur(a, d): + n = len(a) + pivot_inverse = inverse(block(a, 0, d, 0, d)) + require(pivot_inverse is not None, "singular leading block") + return add(block(a, d, n, d, n), + multiply(multiply(block(a, d, n, 0, d), pivot_inverse), + block(a, 0, d, d, n))) + + +def check_pair(p, q, d): + """Check the stated properties from full matrices, not their construction.""" + n = len(p) + require(0 < d < n and len(q) == n, "invalid common split") + require(all(type(row) is int and 0 <= row < 1 << n for row in p + q), + "invalid binary square matrix") + require(multiply(p, p) == p, "P is not idempotent") + require(multiply(q, q) == q, "Q is not idempotent") + require(multiply(p, q) == multiply(q, p), "P and Q do not commute") + s, z = schur(p, d), schur(q, d) + require(multiply(s, s) == s and multiply(z, z) == z, "Schur idempotence") + require(rank(p) == rank(q) == 2 * d, "projector rank") + c = add(multiply(s, z), multiply(z, s)) + require(rank(c) == 2 * d, "Schur commutator rank") + return s, z, c + + +def check_family(t): + d = len(t) + unit, zero = identity(d), (0,) * d + ai = inverse(add(unit, t)) + require(inverse(t) is not None and ai is not None, "T and I+T must be invertible") + p, q = pair_from_t(t) + s, z, c = check_pair(p, q, d) + r = multiply(t, ai) + require(s == join_blocks(((zero, r), (zero, unit)), d), "S block formula") + require(z == join_blocks(((unit, zero), (r, zero)), d), "Z block formula") + require(add(r, unit) == ai, "R+I inverse identity") + r2, ri2 = multiply(r, r), multiply(add(r, unit), add(r, unit)) + diagonal = multiply(r2, ri2) + require(multiply(c, c) == direct_sum((diagonal, diagonal)), "commutator square") + require(rank(diagonal) == d, "square block invertibility") + return p, q, c + + +def parse_rows(rows): + return tuple(sum(int(bit) << j for j, bit in enumerate(row)) for row in rows) + + +P9 = parse_rows(("101101001", "111111101", "011011010", "001001001", "101101101", + "010010010", "000000100", "000000010", "000000001")) +Q9 = parse_rows(("101001101", "111101111", "011010011", "000100000", "000010000", + "000001000", "001001001", "101101101", "010010010")) +C6 = parse_rows(("101111", "111100", "011110", "111101", "100111", "110011")) + + +def rejection(label, p, q, d, expected): + try: + check_pair(p, q, d) + except ValueError as exc: + require(str(exc) == expected, label + ": wrong rejection: " + str(exc)) + return label + raise ValueError(label + ": invalid pair accepted") + + +def controls(): + p, q = pair_from_t(identity(3)) + rejected = [rejection("singular_pivot", p, q, 3, "singular leading block")] + p, q = pair_from_t((0, 0, 0)) + rejected.append(rejection("zero_T", p, q, 3, "Schur commutator rank")) + p, q = pair_from_t(direct_sum((T2, (0,)))) + rejected.append(rejection("nonzero_singular_T", p, q, 3, "Schur commutator rank")) + rejected.append(rejection("identical_projectors", P9, P9, 3, "Schur commutator rank")) + damaged = (P9[0] ^ 1,) + P9[1:] + rejected.append(rejection("broken_idempotence", damaged, Q9, 3, "P is not idempotent")) + # Conjugate Q alone by the permutation swapping its first two coordinates. + swap = (2, 1) + identity(9)[2:] + changed_q = multiply(multiply(swap, Q9), swap) + require(multiply(changed_q, changed_q) == changed_q, "control remains idempotent") + require(inverse(block(changed_q, 0, 3, 0, 3)) is not None, "control keeps its pivot") + rejected.append(rejection("noncommuting_projectors", P9, changed_q, 3, + "P and Q do not commute")) + return rejected + + +def main(): + require(add(add(multiply(T2, T2), T2), identity(2)) == (0,) * 2, "quadratic seed") + require(add(add(multiply(multiply(T3, T3), T3), T3), identity(3)) == (0,) * 3, + "cubic seed") + require(check_pair(P9, Q9, 3)[2] == C6, "literal d=3 witness") + require(pair_from_t(T3) == (P9, Q9), "literal and constructed witness agree") + + examples = [] + for d in range(2, 13): + p, q, c = check_family(seed(d)) + examples.append({"d": d, "n": len(p), "commutator_rank": rank(c)}) + # A zero padding illustrates attainment in every larger ambient dimension. + check_pair(direct_sum((P9, (0,))), direct_sum((Q9, (0,))), 3) + + exhaustive = {} + for d in (2, 3): + accepted = 0 + for bits in range(1 << (d * d)): + t = tuple((bits >> (i * d)) & ((1 << d) - 1) for i in range(d)) + if inverse(t) is not None and inverse(add(t, identity(d))) is not None: + check_family(t) + accepted += 1 + require(accepted == {2: 2, 3: 48}[d], "exhaustive seed count") + exhaustive[str(d)] = {"all_T": 1 << (d * d), "admissible_T": accepted} + print(json.dumps({"status": "PASS_BINARY_SCHUR_MINIMAL_DIMENSION", + "theorem_scope": "Written proof: n_min(d)=3d for every d>=2 over F2", + "finite_examples": examples, "exhaustive_seed_checks": exhaustive, + "rejected_controls": controls(), "new_kappa_claimed": False}, indent=2)) + + +if __name__ == "__main__": + main()