From b79f90bc8d839a4998a40b10bcb437e87baa8397 Mon Sep 17 00:00:00 2001 From: ssafwann Date: Thu, 22 Oct 2026 22:26:36 +0800 Subject: [PATCH] Prove dimension bounds for binary identity-pivot Schur sharpness --- research/identity-pivot-schur/README.md | 308 ++++++++++++++++++++ research/identity-pivot-schur/SOURCES.json | 18 ++ research/identity-pivot-schur/TASK.json | 170 +++++++++++ research/identity-pivot-schur/VERIFY.json | 32 +++ research/identity-pivot-schur/verify.py | 314 +++++++++++++++++++++ 5 files changed, 842 insertions(+) create mode 100644 research/identity-pivot-schur/README.md create mode 100644 research/identity-pivot-schur/SOURCES.json create mode 100644 research/identity-pivot-schur/TASK.json create mode 100644 research/identity-pivot-schur/VERIFY.json create mode 100644 research/identity-pivot-schur/verify.py diff --git a/research/identity-pivot-schur/README.md b/research/identity-pivot-schur/README.md new file mode 100644 index 0000000000..9adb808ca3 --- /dev/null +++ b/research/identity-pivot-schur/README.md @@ -0,0 +1,308 @@ +# Binary Schur sharpness with identity pivots + +**Written algebraic result with exact finite corroboration; no new kappa.** +Prepared for ssafwann with substantial OpenAI Codex assistance. Apache-2.0. + +[PR4634](https://github.com/CrocSwap/integer-mult-bounds/pull/4634) attains +Schur-commutator rank `2d` in dimension `3d` with arbitrary invertible pivots, +and asks what changes if both pivots must be `I_d`. This package proves: + +1. **Identity pivots force `n >= ceil(17d/5)`** for Schur-commutator rank + `2d`. The sharper integer bound is + `L(d)=min_{t=0,...,d} max(3d+2t,4d-3t)`. In particular `n=3d` is + impossible for every positive `d`, and **`L(2)=8`**. +2. **Dimension `4d` suffices with identity pivots**, for every `d >= 2`. + This improves the identity-pivot `5d` construction of + [PR4617](https://github.com/CrocSwap/integer-mult-bounds/pull/4617). + Together with the lower bound, **the identity-pivot minimum at `d=2` + is exactly `n=8`**. +3. In the additional class where `H + H^2` is invertible, with `H` the leading + block of `PQ`, **`4d` is optimal**. The constructed family lies in this class. + +For unrestricted identity-pivot pairs with `d >= 2`, this proves only +`L(d) <= n_min(d) <= 4d`. The first remaining case is **`d=3,n=11`**: +the lower bound is 11 and the construction gives 12. The scalar `d=1` +minimum 5 is predecessor work in PR4609, not a new result. +All matrices below are over `F_2`, act on column vectors, and are algebraic +idempotents; symmetry or orthogonality in an inner product is not assumed. + +## 1. The specialized factorization + +Write, at one common `d + k` coordinate split, + +```text +P = [ I R ], Q = [ I L ], PQ = QP = [ H T ], k = n-d. + [ C D ] [ E F ] [ W * ] +``` + +Assume `P^2=P`, `Q^2=Q`, and `PQ=QP`. Their Schur complements are +`S=D+CR` and `Z=F+EL`. Nick Petalas's ordered factorization in +[PR4597](https://github.com/CrocSwap/integer-mult-bounds/pull/4597) +specializes to the following particularly useful pair of identities: + +```text +U = C+E, V = R+L, J = H+H^2, +A = [ ZC U ], B = [ V ], + [ RZ ] + +[S,Z] = AB, BA = [ J 0 ]. (1) + [ J J ] +``` + +`A` is `k` by `2d` and `B` is `2d` by `k`. In characteristic two the +commutator is `SZ+ZS`. The forward factorization and its `2d` rank bound +are predecessor work; the reverse product is the step used here. + +For completeness, all needed block algebra follows. Idempotence gives + +```text +RC=LE=0, DC=RD=FE=LF=0, +D^2=D+CR, F^2=F+EL. +``` + +Thus `S^2=S`, `Z^2=Z`, `ZE=0`, and `LZ=0`. Commutation gives +`RE=LC=H+I`, `FC=W+E`, `RF=T+L`, and `DF+FD=CL+ER`. +Expanding the two Schur products with the block equations gives + +```text +[S,Z] = W(R+L) + (C+E)T + CHL + EHR + = (W+EH)(R+L) + (C+E)(T+HL). +``` + +The factors simplify in the displayed order: + +```text +W+EH = FC+E+EH = (F+EL)C = ZC, +T+HL = RF+L+HL = R(F+EL) = RZ. +``` + +This proves `AB=[S,Z]` without interchanging noncommuting blocks. +For the reverse product, + +```text +VZC = RZC, VU = RC+RE+LC+LE = 0, +RZ^2C = RZC, RZU = RZC. +``` + +Finally `P(PQ)=PQ` implies `RW=0`, so + +```text +RZC = RFC+RELC + = R(W+E)+(H+I)^2 + = (H+I)+(H+I)^2 + = H+H^2 = J. +``` + +This proves all of (1). In particular `rank[S,Z] <= 2d`. If `J` is +invertible, `BA` is invertible, so `A` is injective and `B` is surjective; +therefore `rank(AB)=2d`. + +## 2. The dimension obstruction + +Suppose `rank[S,Z]=2d`. Both factors in (1) then have rank `2d`. +Put `t=dim ker J`. Elementary block-row elimination in (1) shows +`rank(BA)=2 rank(J)=2(d-t)`. Sylvester's rank inequality gives + +```text +2(d-t) = rank(BA) >= rank(B)+rank(A)-k = 4d-(n-d), +so n >= 3d+2t. (3) +``` + +This inequality can also be read directly: `im A` has dimension `2d`, +and at most `dim ker B=k-2d` of it is lost on applying `B`. + +The four joint-sector projectors are + +```text +E11 = PQ, E10 = P(I+Q), +E01 = (I+P)Q, E00 = (I+P)(I+Q). +``` + +They are pairwise annihilating idempotents whose sum is `I_n`. Their images +therefore form a direct sum, so their ranks sum to `n`. Their leading +`d` by `d` blocks are respectively `H, I+H, I+H, I+H`. +Let `a=dim ker H` and `b=dim ker(I+H)`. Their ranks give + +```text +n >= rank H + 3 rank(I+H) = 4d-a-3b. (4) +``` + +Moreover `ker J = ker H direct-sum ker(I+H)`, so `t=a+b`. +Indeed if `Jx=0`, then `x=(I+H)x+Hx`; the two summands lie respectively +in `ker H` and `ker(I+H)`, and the intersection of those kernels is zero. +Conversely both kernels are killed by `J=H(I+H)`. +Thus (4) implies `n >= 4d-3t`. Combining it with (3) gives + +```text +n >= max(3d+2t, 4d-3t) >= L(d). +``` + +Three times (3) plus twice `n>=4d-3t` gives `5n>=17d`, proving the +simpler bound `n>=ceil(17d/5)`. This strictly excludes `n=3d`. +For `d=2`, the three possible `t=0,1,2` yield lower bounds `8,8,10`, +so `n>=8`; Section 3 attains it. For `d=3`, the four values are +`12,11,13,15`, giving the first remaining dimension 11. + +If `J` is invertible, `t=0` and (4) gives `n>=4d`. That extra condition +is essential for this last bound. For rectangular factors, `AB` can have +rank `2d` while `BA` is singular. The credited PR4617 scalar witness has +`n=5`, `d=1`, rank `2`, and `J=0`; the verifier retains it as a control +against replacing (3)-(4) by the unjustified condition that `J` is invertible. + +## 3. An identity-pivot construction in dimension 4d + +Choose a binary `d` by `d` matrix `H` for which `H` and `I+H` are invertible. +In four blocks of size `d`, put + +```text +G = [ I+H I+H I+H H ], X = [ I ], + [ I ] + [ I ] + [ I ] + +W0 = H^-1(I+H), + +M = [ I I 0 0 ], P0 = diag(0,I,0,I), + [ I 0 I 0 ] Q0 = diag(0,0,I,I). + [ I 0 0 I ] + [ I W0 W0 W0 ] +``` + +Here `GX=I`. Each of the last three block columns of `M` lies in `ker G`, +and these `3d` columns are independent by their first three block rows. +Since `G` is surjective, they form a basis of `ker G`. The first block +column is `X`, complementary to that kernel. Thus `M` is invertible and +the first block row of `M^-1` is `G`. + +Set + +```text +P = M^-1 P0 M, Q = M^-1 Q0 M. (2) +``` + +They commute and are idempotents, each of rank `2d`. Their leading blocks are + +```text +G P0 X = (I+H)+H = I, G Q0 X = (I+H)+H = I, +G P0 Q0 X = H. +``` + +Therefore (1) applies with this prescribed `H`. Since `J=H(I+H)` is +invertible, the Schur commutator has rank exactly `2d`. The four joint +sectors each have dimension `d`, so (2) attains the lower bound in the +invertible-`J` class. + +Such `H` exists for every `d>=2`. Use the same elementary binary seeds as +lee-phys's PR4634 (their use is credited, not claimed as a new seed search): + +```text +H2 = [0 1], H3 = [0 0 1]. + [1 1] [1 0 1] + [0 1 0] +``` + +`H2^2+H2+I=0`, so `H2` and `I+H2` are mutual inverses. +`H3^3+H3+I=0`, so `H3^-1=H3^2+I` and +`(I+H3)^-1=H3^2+H3`. For even `d=2r`, take `r` copies of `H2`. +For odd `d=3+2r`, take `H3` and `r` copies of `H2`. Direct sums preserve +both invertibility conditions. These identities prove the family for all +`d>=2`; finite checks are corroboration only. + +For an immediately inspectable `d=2`, `n=8` instance, each string is one row: + +```text +P8 Q8 +10110011 10111100 +01100010 01101000 +10110011 10111100 +01100010 01101000 +00111011 10111100 +00100110 01101000 +10110011 00111110 +01100010 00101001 +``` + +Both leading blocks are `I_2`; both projector ranks and the six-dimensional +Schur commutator's rank are `4`. Appending zero blocks to both matrices +preserves the pivots and commutator rank, so every `n>=4d` is also attainable. + +## 4. Verification and limits + +From the repository root, using Python 3.12 and its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/identity-pivot-schur --check-only +python3.12 -B scripts/research_package.py --package research/identity-pivot-schur +``` + +The registered commands run `verify.py` in ordinary and optimized (`-O`) +modes, with warnings as errors. The verifier uses explicit exceptions, imports +no predecessor executable, writes no files, and prints +`PASS_IDENTITY_PIVOT_SCHUR` with a deterministic JSON receipt. It checks: + +- The literal 8-by-8 witness, (2) for `d=2..12`, zero padding, and a + mixed `d=3,n=13` fixture with nonzero singular `J` (direct sum with the + credited scalar witness). All sharp pairs check both dimension inequalities. +- All 16 size-two and 512 size-three seeds; exactly 2 and 48 are admissible, + and every admissible seed produces the claimed new identity-pivot pair. +- Every ordered commuting identity-pivot idempotent pair in `M3(F2)` at + `d=1` (253 pairs) and `M4(F2)` at `d=2` (1,219 pairs). These check both + factorizations, Schur idempotence/ranks, and all four joint sectors. + Their commutator rank histograms are `{0:241,1:12}` and `{0:1147,1:72}`. + These small calibration domains are not new minimal-dimension classifications. +- Eleven controls reject nonidentity pivots, broken idempotence, noncommuting + projectors with the other premises preserved, three invalid seed conditions, + nonbinary entries, two factor omissions, false sharpness of identical + projectors, and the invalid rectangular-factor inference from Section 2. + +The universal claims rest on the written proofs above. Independent human +review and formal-kernel verification are not claimed. No header-density, +physical execution, supplier, stock, precision or multiplication-exponent +result follows. No selected frontier is changed. Lean, Docker, the selected +cold replay and a global search over intermediate dimensions were not run. + +This began on canonical main `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, +priority revision 7, selected conditional kappa `0.00302015`. +The selected orientation command was attempted but stopped because the sparse +checkout omits `certificates/checkpoints/frontier4359.json`; no baseline pass +is claimed. None of the missing selected inputs is needed by this package. + +`SOURCES.json` pins the task catalogue and selected record as historical +provenance only. The four pending predecessors are exact-head citations and +source hashes in `TASK.json`, not replay-time Git dependencies. The two scalar +control matrices are contained in `verify.py`, transcribed from the attributed +PR4617 source. The proof and checker otherwise need no external mathematical +inputs. [Discussion #4653](https://github.com/CrocSwap/integer-mult-bounds/discussions/4653) +is the canonical claim and handoff. The initial overlap snapshot covered all +423 open PR bodies, 3,586 Discussion records and all 5,860 in-scope local +notes; it did not search every code diff, closed PR, or unpublished result. + +## Open next questions + +**Can singular `H+H^2` attain rank `2d` for `L(d)<=n<4d`?** This is the remaining +minimum-dimension gap under identity pivots. The first instance is `d=3,n=11`. +A useful next step is to combine the two factors in (1) with the four joint +sector dimensions, or enumerate a specified complete sector/header model. +A failed random search would not settle the question. The obstacle is that +full rank of a rectangular product does not imply invertibility of its reverse. +This package stops at the proved boundary; it starts no further search campaign. + +## Credit + +- **Nick Petalas**, PR4597 at `dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb`: + ordered block-Schur factorization, `2d` rank bound and idempotent Schur lemma; + PR4278 and its PR4259/PR4228 predecessors supply the shared-header context. +- **Ryanson Jonathan**, PR4609 at `eb5ccf9288808d973551e6264300d30d2f6e48a0` + and PR4617 at `96c01a2124e234d798e9e97643c20fb5b430840d`: binary scalar + witness and identity-pivot `5d` tensor family, with the Claude Code assistance + disclosed in those packages. Their scalar matrices are reproduced as a control. +- **lee-phys**, PR4634 at `9f053f7051e5fc3327d4337bb4bd8ac52cf5fcd0`: + optimal unrestricted-pivot `3d` family, the reused binary seeds and the + explicit identity-pivot question, with OpenAI Codex assistance. +- **Cinna Davis**, PR4100: the earlier BIT request/complete-header setting. + This side theorem closes no actual-caller or all-size transfer obligation. + +The new reverse-product argument, rank-nullity/four-sector obstruction, `4d` change of +basis and self-contained checker were prepared for ssafwann with substantial +OpenAI Codex assistance (gpt-6-astra), by one agent. Repository tooling retains +Douglas Colkitt's and other contributors' attribution. Apache-2.0. diff --git a/research/identity-pivot-schur/SOURCES.json b/research/identity-pivot-schur/SOURCES.json new file mode 100644 index 0000000000..4916cee8e5 --- /dev/null +++ b/research/identity-pivot-schur/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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/identity-pivot-schur/TASK.json b/research/identity-pivot-schur/TASK.json new file mode 100644 index 0000000000..a72b083101 --- /dev/null +++ b/research/identity-pivot-schur/TASK.json @@ -0,0 +1,170 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "Resolve the identity-pivot boundary left open by PR4634: can commuting binary idempotents with both leading d-blocks equal to I attain Schur-commutator rank 2d at n=3d? Seek a smaller-than-5d constructive upper bound for d>=2.", + "scope_change_reason": "Handoff-first selection: PR4634 explicitly leaves identity pivots open. This is a written algebraic interface theorem and exact finite corroboration, rather than a Lean formalization or a selected-caller audit.", + "bottleneck_link": "Side result in the BIT shared-header/Schur interface lineage: separates invertible-pivot and identity-pivot contracts. Does not establish header density, a physical caller, supplier admission or a new kappa.", + "budget_minutes": 60, + "stop_rule": "One session: stop after a scoped universal obstruction/construction with bounded exact checks, or report the unresolved implication. No global search or Lean build.", + "outcome": "completed", + "evidence": "README proves n>=L(d)=min_t max(3d+2t,4d-3t)>=ceil(17d/5), a construction at n=4d for all d>=2, exact minimum n=8 at d=2, and optimality at 4d when H+H^2 is invertible. Exact finite corroboration and eleven controls; no human or formal-kernel acceptance.", + "author": "ssafwann", + "ai_assistance": "Substantial OpenAI Codex assistance (gpt-6-astra). One agent; no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can singular H+H^2 attain Schur-commutator rank 2d with identity pivots for L(d)<=n<4d?", + "why_it_matters": "Determines the remaining optimal ambient dimension under the stronger pivot contract.", + "first_step": "Analyze the rectangular factors and four joint sectors; first unresolved case d=3,n=11. A complete enumerated model or proof is required.", + "blocked_by": "Full rank of AB does not force BA invertible for rectangular factors; the predecessor scalar witness rejects that shortcut." + } + ], + "upstream_refresh": { + "commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "priority_revision": 7, + "checked_at": "2026-10-22T14:14:00Z" + }, + "overlap": { + "open_prs": 423, + "discussion_records": 3586, + "local_notes": 5860, + "complete_pagination": true, + "local_head_inventory_complete": true, + "checked_at": "2026-10-22T14:12:56Z", + "scope": "titles/bodies, Discussion comments/replies, top-level README/TASK and ledger; not every code diff or unpublished work" + }, + "predecessors": [ + { + "pr": 4634, + "head": "9f053f7051e5fc3327d4337bb4bd8ac52cf5fcd0", + "author": "lee-phys", + "role": "Optimal n=3d with arbitrary invertible pivots; identity-pivot open question and binary seed matrices" + }, + { + "pr": 4597, + "head": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "author": "Nick Petalas", + "role": "Ordered Schur commutator factorization and 2d bound" + }, + { + "pr": 4609, + "head": "eb5ccf9288808d973551e6264300d30d2f6e48a0", + "author": "Ryanson Jonathan", + "role": "Binary examples and scalar minimal dimension" + }, + { + "pr": 4617, + "head": "96c01a2124e234d798e9e97643c20fb5b430840d", + "author": "Ryanson Jonathan", + "role": "Identity-pivot n=5d sharpness family" + } + ], + "predecessor_sources": [ + { + "commit": "9f053f7051e5fc3327d4337bb4bd8ac52cf5fcd0", + "path": "research/binary-schur-minimal-dimension/README.md", + "git_blob": "c7acbef834602cbda79736c46da167ff3f1e6eaa", + "sha256": "70dd1fc0d1936806aebcc9c71f57ab815b890380e20a7caae6c5ae1ff589aae4", + "usage": "citation; no replay-time Git dependency", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/9f053f7051e5fc3327d4337bb4bd8ac52cf5fcd0/research/binary-schur-minimal-dimension/README.md" + }, + { + "commit": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "path": "research/block-schur-commutator/README.md", + "git_blob": "79790ccea54cfea1aab611768927651a81f2fb18", + "sha256": "945c1420fe9fb5c26dec49e7d6005d77382ca9dc6ca0f424d8baa1500bfc092c", + "usage": "citation; no replay-time Git dependency", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb/research/block-schur-commutator/README.md" + }, + { + "commit": "eb5ccf9288808d973551e6264300d30d2f6e48a0", + "path": "research/schur-projector-refinement/README.md", + "git_blob": "c6fc0e77d9f1022d519df8e3d8266672df793adb", + "sha256": "7edb11d24ffd6fa4604ebfa9d27215d74a684ea23a484a0cf36a970f08571232", + "usage": "citation; no replay-time Git dependency", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/eb5ccf9288808d973551e6264300d30d2f6e48a0/research/schur-projector-refinement/README.md" + }, + { + "commit": "96c01a2124e234d798e9e97643c20fb5b430840d", + "path": "research/binary-projector-sharpness/verify.py", + "git_blob": "7c16d4b205ec62f7a07b823116299fc4dc5a59ff", + "sha256": "2e4139d97eb21ddedcbd6e0369dd724c04a0cbcd5bc65c7f6a522b5ed423a0e7", + "usage": "citation; no replay-time Git dependency", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/96c01a2124e234d798e9e97643c20fb5b430840d/research/binary-projector-sharpness/verify.py" + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4653" +} diff --git a/research/identity-pivot-schur/VERIFY.json b/research/identity-pivot-schur/VERIFY.json new file mode 100644 index 0000000000..178e3ca289 --- /dev/null +++ b/research/identity-pivot-schur/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": "Exact full-matrix family, literal witness, both ordered factorizations, exhaustive small domains and eleven rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks remain active with Python assertions disabled." + } + ] +} diff --git a/research/identity-pivot-schur/verify.py b/research/identity-pivot-schur/verify.py new file mode 100644 index 0000000000..efb941c63a --- /dev/null +++ b/research/identity-pivot-schur/verify.py @@ -0,0 +1,314 @@ +#!/usr/bin/env python3 +"""Exact binary matrix corroboration; ssafwann with OpenAI Codex, Apache-2.0. + +No predecessor executable, external input, numerical library or random search. +The all-d claims are proved in README.md, not inferred from these finite checks. +""" +import itertools +import json + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def zero(rows, cols): + return tuple((0,) * cols for _ in range(rows)) + + +def eye(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def add(a, b): + require(len(a) == len(b) and len(a[0]) == len(b[0]), "addition shape") + return tuple(tuple(x ^ y for x, y in zip(ar, br)) for ar, br in zip(a, b)) + + +def mul(a, b): + require(len(a[0]) == len(b), "multiplication shape") + cols = tuple(zip(*b)) + return tuple(tuple(sum(x * y for x, y in zip(row, col)) % 2 + for col in cols) for row in a) + + +def rank(a): + rows = [sum(x << j for j, x in enumerate(row)) for row in a] + pivot = 0 + for col in range(len(a[0])): + hit = next((i for i in range(pivot, len(rows)) if rows[i] >> col & 1), None) + if hit is None: + continue + rows[pivot], rows[hit] = rows[hit], rows[pivot] + for i in range(pivot + 1, len(rows)): + if rows[i] >> col & 1: + rows[i] ^= rows[pivot] + pivot += 1 + return pivot + + +def inverse(a): + n = len(a) + require(all(len(row) == n for row in a), "inverse shape") + rows = [list(row) + list(unit) for row, unit in zip(a, eye(n))] + for col in range(n): + hit = next((i for i in range(col, n) if rows[i][col]), None) + require(hit is not None, "singular matrix") + rows[col], rows[hit] = rows[hit], rows[col] + for i in range(n): + if i != col and rows[i][col]: + rows[i] = [x ^ y for x, y in zip(rows[i], rows[col])] + return tuple(tuple(row[n:]) for row in rows) + + +def block(a, r0, r1, c0, c1): + return tuple(tuple(row[c0:c1]) for row in a[r0:r1]) + + +def hcat(a, b): + require(len(a) == len(b), "horizontal shape") + return tuple(x + y for x, y in zip(a, b)) + + +def grid(rows): + result = () + for row in rows: + line = row[0] + for part in row[1:]: + line = hcat(line, part) + result += line + return result + + +def diagonal(blocks): + sizes = [len(b) for b in blocks] + return grid([[b if i == j else zero(sizes[i], sizes[j]) + for j, b in enumerate(blocks)] for i in range(len(blocks))]) + + +def validate_pair(p, q, d): + n = len(p) + require(0 < d < n <= 52 and len(q) == n, "matrix capacity or split") + require(all(len(row) == n for a in (p, q) for row in a), "square pair") + require(all(type(x) is int and x in (0, 1) + for a in (p, q) for row in a for x in row), "binary entries") + require(block(p, 0, d, 0, d) == eye(d), "P identity pivot") + require(block(q, 0, d, 0, d) == eye(d), "Q identity pivot") + require(mul(p, p) == p and mul(q, q) == q, "idempotence") + require(mul(p, q) == mul(q, p), "commutation") + + +def dimension_lower_bound(d): + return min(max(3 * d + 2 * t, 4 * d - 3 * t) for t in range(d + 1)) + + +def inspect_pair(p, q, d): + validate_pair(p, q, d) + n, k = len(p), len(p) - d + r, c, a = block(p, 0, d, d, n), block(p, d, n, 0, d), block(p, d, n, d, n) + l, e, b = block(q, 0, d, d, n), block(q, d, n, 0, d), block(q, d, n, d, n) + s, z = add(a, mul(c, r)), add(b, mul(e, l)) + comm = add(mul(s, z), mul(z, s)) + require(mul(s, s) == s and mul(z, z) == z, "Schur idempotence") + require(rank(p) == d + rank(s) and rank(q) == d + rank(z), "Schur ranks") + h = block(mul(p, q), 0, d, 0, d) + j = add(h, mul(h, h)) + u, v = add(c, e), add(r, l) + left = hcat(mul(z, c), u) + right = v + mul(r, z) + require(mul(left, right) == comm, "ordered commutator factorization") + reverse = grid([[j, zero(d, d)], [j, j]]) + require(mul(right, left) == reverse, "reverse-product identity") + pq = mul(p, q) + sectors = [pq, add(p, pq), add(q, pq), add(add(eye(n), p), add(q, pq))] + tops = [h] + [add(eye(d), h)] * 3 + for i, sector in enumerate(sectors): + require(mul(sector, sector) == sector, "joint sector idempotence") + require(block(sector, 0, d, 0, d) == tops[i], "joint compression") + for other in sectors[:i]: + require(mul(sector, other) == zero(n, n), "joint orthogonality") + require(sum(map(rank, sectors)) == n, "joint direct-sum dimensions") + rk = rank(comm) + defect = d - rank(j) + a, b = d - rank(h), d - rank(add(eye(d), h)) + require(a + b == defect, "coprime-factor kernel dimensions") + require(rank(mul(right, left)) == 2 * rank(j), "reverse-product rank") + require(rk <= min(2 * d, k), "universal rank bound") + if n == 3 * d: + require(rk < 2 * d, "identity-pivot 3d obstruction") + if rank(j) == d: + require(rk == 2 * d, "invertible reverse product implies sharpness") + require(all(rank(t) >= d for t in sectors), "four-sector lower bound") + require(n >= 4 * d, "invertible-J dimension bound") + if rk == 2 * d: + require(rank(left) == rank(right) == 2 * d, "sharp factor ranks") + require(n >= 3 * d + 2 * defect, "Sylvester lower bound") + require(n >= 4 * d - a - 3 * b, "joint-sector lower bound") + require(n >= dimension_lower_bound(d), "integer dimension bound") + require(5 * n >= 17 * d, "17d/5 lower bound") + return {"n": n, "d": d, "commutator_rank": rk, "J_rank": rank(j), + "J_nullity": defect, "dimension_lower_bound": dimension_lower_bound(d), + "sector_ranks": list(map(rank, sectors))}, (left, right, comm, reverse) + + +H2 = ((0, 1), (1, 1)) +H3 = ((0, 0, 1), (1, 0, 1), (0, 1, 0)) + +# Literal new witness, also printed in README.md. +P8 = tuple(tuple(map(int, row)) for row in ( + "10110011", "01100010", "10110011", "01100010", + "00111011", "00100110", "10110011", "01100010")) +Q8 = tuple(tuple(map(int, row)) for row in ( + "10111100", "01101000", "10111100", "01101000", + "10111100", "01101000", "00111110", "00101001")) + +# Ryanson Jonathan's PR4609 witness, transcribed from PR4617 verify.py +# at 96c01a2124e234d798e9e97643c20fb5b430840d (Apache-2.0). +# It prevents extending the square-factor argument to rectangular factors. +P5 = ((1, 1, 0, 0, 0), (0, 0, 0, 0, 0), (1, 0, 1, 1, 1), + (0, 0, 0, 1, 0), (1, 1, 0, 1, 0)) +Q5 = ((1, 1, 1, 0, 0), (1, 0, 0, 1, 1), (1, 0, 0, 1, 1), + (1, 0, 1, 0, 1), (1, 1, 0, 1, 0)) + + +def seed(d): + require(d >= 2, "seed dimension at least two") + return diagonal(([H3] if d % 2 else []) + [H2] * ((d - (3 if d % 2 else 0)) // 2)) + + +def construct(h): + d = len(h) + ident, blank = eye(d), zero(d, d) + require(rank(h) == d and rank(add(h, ident)) == d, "H and I+H invertible") + w = mul(inverse(h), add(ident, h)) + change = grid([[ident, ident, blank, blank], [ident, blank, ident, blank], + [ident, blank, blank, ident], [ident, w, w, w]]) + back = inverse(change) + p0 = diagonal([blank, ident, blank, ident]) + q0 = diagonal([blank, blank, ident, ident]) + return mul(mul(back, p0), change), mul(mul(back, q0), change) + + +def exhaustive_pairs(n, d): + """All binary matrices, then all ordered admissible idempotent pairs.""" + candidates = [] + for bits in range(1 << (n * n)): + a = tuple(tuple(bits >> (i * n + j) & 1 for j in range(n)) for i in range(n)) + if block(a, 0, d, 0, d) == eye(d) and mul(a, a) == a: + candidates.append(a) + counts = {} + for p, q in itertools.product(candidates, repeat=2): + if mul(p, q) != mul(q, p): + continue + receipt, _ = inspect_pair(p, q, d) + rk = receipt["commutator_rank"] + counts[str(rk)] = counts.get(str(rk), 0) + 1 + return {"n": n, "d": d, "idempotents_with_identity_pivot": len(candidates), + "ordered_commuting_pair_rank_histogram": counts} + + +def rejects(label, thunk): + try: + thunk() + except ValueError: + return label + raise ValueError("control was accepted: " + label) + + +def toggle(a, i, j): + rows = [list(row) for row in a] + rows[i][j] ^= 1 + return tuple(map(tuple, rows)) + + +def check_controls(p, q, factors): + left, right, comm, reverse = factors + bad_q = None + for i, j in itertools.combinations(range(2, 8), 2): + perm = list(range(8)) + perm[i], perm[j] = perm[j], perm[i] + candidate = tuple(tuple(q[a][b] for b in perm) for a in perm) + if mul(p, candidate) != mul(candidate, p): + bad_q = candidate + break + require(bad_q is not None, "noncommuting fixture exists") + require(mul(bad_q, bad_q) == bad_q and block(bad_q, 0, 2, 0, 2) == eye(2), + "noncommuting control preserves its other premises") + return [ + rejects("nonidentity pivot", lambda: inspect_pair(toggle(p, 0, 1), q, 2)), + rejects("broken idempotence", lambda: inspect_pair(toggle(p, 2, 2), q, 2)), + rejects("commutation with both projectors and pivots preserved", + lambda: inspect_pair(p, bad_q, 2)), + rejects("singular H", lambda: construct(zero(2, 2))), + rejects("singular I+H", lambda: construct(eye(2))), + rejects("nonzero singular H", lambda: construct(((1, 0), (0, 0)))), + rejects("nonbinary entry", lambda: inspect_pair(((2,) + p[0][1:],) + p[1:], q, 2)), + rejects("omitted first commutator factor", lambda: require( + mul(hcat(zero(6, 2), block(left, 0, 6, 2, 4)), right) == comm, + "omitting ZC changes commutator")), + rejects("omitted lower-left J", lambda: require( + mul(right, left) == grid([[block(reverse, 0, 2, 0, 2), zero(2, 2)], + [zero(2, 2), block(reverse, 2, 4, 2, 4)]]), + "lower-left J is necessary")), + rejects("zero commutator claimed sharp", lambda: require( + inspect_pair(p, p, 2)[0]["commutator_rank"] == 4, "sharpness")), + ] + + +def main(): + families = [] + for d in range(2, 13): + p, q = construct(seed(d)) + receipt, _ = inspect_pair(p, q, d) + require(receipt["commutator_rank"] == 2 * d and receipt["J_rank"] == d, + "constructed family sharpness") + require(receipt["sector_ranks"] == [d] * 4, "constructed sector dimensions") + families.append(receipt) + seed_counts = {} + for d in (2, 3): + count = 0 + for bits in range(1 << (d * d)): + h = tuple(tuple(bits >> (i * d + j) & 1 for j in range(d)) for i in range(d)) + if rank(h) == d and rank(add(h, eye(d))) == d: + p, q = construct(h) + require(inspect_pair(p, q, d)[0]["commutator_rank"] == 2 * d, + "admissible seed sharpness") + count += 1 + require(count == {2: 2, 3: 48}[d], "admissible seed census") + seed_counts[str(d)] = count + p, q = construct(H2) + require((p, q) == (P8, Q8), "literal eight-dimensional witness") + receipt, factors = inspect_pair(p, q, 2) + padded = inspect_pair(diagonal([p, zero(3, 3)]), diagonal([q, zero(3, 3)]), 2)[0] + require(padded["commutator_rank"] == 4, "padding retains sharpness") + controls = check_controls(p, q, factors) + predecessor, _ = inspect_pair(P5, Q5, 1) + require(predecessor["commutator_rank"] == 2 and predecessor["J_rank"] == 0, + "predecessor rectangular-factor boundary") + controls.append(rejects("sharpness does not imply invertible J for rectangular factors", + lambda: require(predecessor["J_rank"] == 1, "J may be singular"))) + # Direct sum with the pivot coordinates moved first: a singular-J case at d=3. + order = [0, 5, 6] + list(range(1, 5)) + list(range(7, 13)) + mixed_p, mixed_q = diagonal([P5, P8]), diagonal([Q5, Q8]) + mixed_p = tuple(tuple(mixed_p[i][j] for j in order) for i in order) + mixed_q = tuple(tuple(mixed_q[i][j] for j in order) for i in order) + mixed, _ = inspect_pair(mixed_p, mixed_q, 3) + require(mixed["commutator_rank"] == 6 and mixed["J_nullity"] == 1, + "nonzero-J singular reverse product") + require(dimension_lower_bound(2) == 8 and dimension_lower_bound(3) == 11, + "small integer dimension bounds") + report = {"scope": "finite corroboration of README proof; no new kappa", + "family": families, "all_admissible_seeds": seed_counts, + "exhaustive_pairs": [exhaustive_pairs(3, 1), exhaustive_pairs(4, 2)], + "padded": padded, "controls_rejected": controls, + "credited_PR4617_boundary_control": predecessor, + "mixed_singular_J_fixture": mixed, + "literal_d2": {"P": ["".join(map(str, row)) for row in p], + "Q": ["".join(map(str, row)) for row in q]}} + print(json.dumps(report, indent=2, sort_keys=True)) + print("PASS_IDENTITY_PIVOT_SCHUR") + + +if __name__ == "__main__": + main()