diff --git a/research/binary-projector-sharpness/README.md b/research/binary-projector-sharpness/README.md new file mode 100644 index 0000000000..e2051752d9 --- /dev/null +++ b/research/binary-projector-sharpness/README.md @@ -0,0 +1,41 @@ +# Binary projectors attain the Schur-commutator bound 2d for every d + +**Task:** independent-moment (original successor result). **Base:** canonical main `f626db5c`. **No κ is claimed.** + +## Background + +- **#4597** (petalas, open) proves rank [S, Z] ≤ min(2d, n−d) for the Schur complements of commuting P, Q with invertible leading d×d blocks. It shows sharpness over F₅ and asks, in its open question 2, for sharp bounds over fixed fields, especially F₂. +- **#4609** (mine) refines this for idempotents to min(2d, 2⌊(n−d)/2⌋). It shows that over F₂ the value 2d is first reached at n = 5 for d = 1 and at n = 6 for d = 2. + +## Corollary + +**Over F₂, for every d ≥ 1, there are commuting idempotents in M_{5d}(F₂) with invertible leading d×d blocks whose Schur commutator has rank exactly 2d.** So the refined bound is attained over F₂ for every d. + +**Proof.** + +- **Base.** Take #4609's binary witness (P, Q) in M₅(F₂) at d = 1. It has p₀₀ = q₀₀ = 1 and rank [S, Z] = 2. +- **Tensor.** Put P′ = P ⊗ I_d and Q′ = Q ⊗ I_d, with coordinate (i, k) at index i·d + k. Then P′ and Q′ are commuting idempotents, and their leading d×d blocks are I_d. +- **Complements.** The Schur complements are S ⊗ I_d and Z ⊗ I_d. +- **Rank.** Their commutator is [S, Z] ⊗ I_d, which has rank 2d. +- **Sharpness.** Since min(2d, 2⌊4d/2⌋) = 2d, the bound is attained. ∎ + +The verifier checks the base witness and the tensored witnesses for d = 1, …, 4: commuting, idempotent, idempotent complements, and rank 2d at n = 5d. + +## Verify + +```text +python3 -B research/binary-projector-sharpness/verify.py +``` + +The check takes well under 1 s and uses the standard library only. + +## Limitations + +- **Minimal n is not determined.** n = 5d is sufficient, but #4609 shows that d = 2 already reaches 4 at n = 6 < 10. +- **Not claimed.** A density, a caller, a supplier or κ. + +## Open next questions + +- **Minimal n over F₂ for each d.** The values so far are 5 for d = 1 and 6 for d = 2. First step: test whether a direct sum of the n = 6, d = 2 witness with I_{d−2}-tensored copies of the n = 5, d = 1 witness gives n = 6 + 5(d−2), and search d = 3 at n = 9 to 11. + +Credit: petalas (Nick Petalas) for #4597's tensor construction idea and #4278. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/binary-projector-sharpness/SOURCES.json b/research/binary-projector-sharpness/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/binary-projector-sharpness/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/binary-projector-sharpness/TASK.json b/research/binary-projector-sharpness/TASK.json new file mode 100644 index 0000000000..2034f6c332 --- /dev/null +++ b/research/binary-projector-sharpness/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "unchanged", + "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "scope_change_reason": null, + "bottleneck_link": "Completes binary sharpness for #4597 OQ2 at every d.", + "budget_minutes": 20, + "stop_rule": "Stop at the tensor corollary.", + "outcome": "completed", + "evidence": "Tensored F2 witnesses P (x) I_d, Q (x) I_d are commuting idempotents with I_d leading blocks and Schur commutator rank 2d at n = 5d; checked d = 1..4; written proof.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Minimal n over F2 for each d.", + "why_it_matters": "Sharp binary dimension threshold.", + "first_step": "Direct sums of the d=2,n=6 and d=1,n=5 witnesses; search d=3 at n=9..11.", + "blocked_by": "None." + } + ] +} diff --git a/research/binary-projector-sharpness/VERIFY.json b/research/binary-projector-sharpness/VERIFY.json new file mode 100644 index 0000000000..4012b9f0b0 --- /dev/null +++ b/research/binary-projector-sharpness/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Base F2 witness and tensored witnesses d=1..4: commuting idempotents, invertible leading blocks, idempotent complements, Schur commutator rank 2d at n=5d." + } + ] +} diff --git a/research/binary-projector-sharpness/verify.py b/research/binary-projector-sharpness/verify.py new file mode 100644 index 0000000000..7c16d4b205 --- /dev/null +++ b/research/binary-projector-sharpness/verify.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +"""Binary projectors attain the Schur-commutator bound 2d for every d (follow-up to #4597 OQ2 and #4609). + +#4597 (petalas) proves rank [S,Z] <= min(2d, n-d) for the Schur complements of commuting P, Q with invertible leading +d x d blocks, with sharpness over F5; #4609 refines this for idempotents to min(2d, 2 floor((n-d)/2)) and shows that +over F2 the value 2d is first reached at n = 5 for d = 1 and at n = 6 for d = 2. + +Corollary (proved below, checked for d = 1..4): over F2, for every d >= 1 there are commuting idempotents in M_{5d} +with invertible leading d x d blocks whose Schur commutator has rank exactly 2d. +Proof: take the #4609 witness (P, Q) in M_5(F2) at d = 1 (p_00 = q_00 = 1, rank [S,Z] = 2) and put P' = P (x) I_d, +Q' = Q (x) I_d with coordinate (i, k) at index i*d + k, so the first d coordinates are (0, k), k < d. Then P', Q' +are commuting idempotents, +the leading d x d blocks are p_00 I_d = I_d, the Schur complements are S (x) I_d and Z (x) I_d, and +[S (x) I_d, Z (x) I_d] = [S,Z] (x) I_d has rank 2d. The bound 2d is attained since min(2d, 2 floor(4d/2)) = 2d. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import json +import sys + +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 need(condition, message): + if not condition: + raise AssertionError(message) + + +def mul(a, b): + return tuple(tuple(sum(a[i][k] & b[k][j] for k in range(len(b))) & 1 for j in range(len(b[0]))) + for i in range(len(a))) + + +def sub(a, b): + return tuple(tuple(x ^ y for x, y in zip(ra, rb)) for ra, rb in zip(a, b)) + + +def block(m, r0, r1, c0, c1): + return tuple(tuple(m[i][c0:c1]) for i in range(r0, r1)) + + +def rank(m): + rows, r = [list(x) for x in m], 0 + for c in range(len(rows[0]) if rows else 0): + p = next((i for i in range(r, len(rows)) if rows[i][c]), None) + if p is None: + continue + rows[r], rows[p] = rows[p], rows[r] + for i in range(len(rows)): + if i != r and rows[i][c]: + rows[i] = [x ^ y for x, y in zip(rows[i], rows[r])] + r += 1 + return r + + +def inverse(m): + n = len(m) + rows = [list(r) + [int(i == j) for j in range(n)] for i, r in enumerate(m)] + for c in range(n): + p = next((i for i in range(c, n) if rows[i][c]), None) + if p is None: + return None + rows[c], rows[p] = rows[p], rows[c] + for i in range(n): + if i != c and rows[i][c]: + rows[i] = [x ^ y for x, y in zip(rows[i], rows[c])] + return tuple(tuple(r[n:]) for r in rows) + + +def kron_identity(m, d): + n = len(m) + return tuple(tuple(m[i // d][j // d] if i % d == j % d else 0 for j in range(n * d)) for i in range(n * d)) + + +def schur_rank(p, q, d): + n = len(p) + ai, bi = inverse(block(p, 0, d, 0, d)), inverse(block(q, 0, d, 0, d)) + need(ai is not None and bi is not None, "invertible leading blocks") + s = sub(block(p, d, n, d, n), mul(mul(block(p, d, n, 0, d), ai), block(p, 0, d, d, n))) + z = sub(block(q, d, n, d, n), mul(mul(block(q, d, n, 0, d), bi), block(q, 0, d, d, n))) + need(mul(s, s) == s and mul(z, z) == z, "idempotent Schur complements") + return rank(sub(mul(s, z), mul(z, s))) + + +def main(): + need(mul(P5, P5) == P5 and mul(Q5, Q5) == Q5 and mul(P5, Q5) == mul(Q5, P5), "base witness") + need(schur_rank(P5, Q5, 1) == 2, "base rank 2 at n = 5, d = 1") + ranks = {} + for d in range(1, 5): + p, q = kron_identity(P5, d), kron_identity(Q5, d) + need(mul(p, p) == p and mul(q, q) == q and mul(p, q) == mul(q, p), "tensored commuting idempotents") + r = schur_rank(p, q, d) + need(r == 2 * d == min(2 * d, 2 * ((5 * d - d) // 2)), "rank 2d attained at n = 5d") + ranks[str(d)] = {"n": 5 * d, "rank": r} + print(json.dumps({"status": "PASS_BINARY_PROJECTOR_SHARPNESS_ALL_D", "ranks": ranks, + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())