From eb5ccf9288808d973551e6264300d30d2f6e48a0 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 16:56:32 +0700 Subject: [PATCH] =?UTF-8?q?Refine=20#4597's=20Schur=20commutator=20bound?= =?UTF-8?q?=20for=20projectors:=20odd-codimension=20parity=20theorem=20and?= =?UTF-8?q?=20minimal=20binary/ternary=20sharpness=20witnesses=20(no=20new?= =?UTF-8?q?=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- research/schur-projector-refinement/README.md | 82 ++++++++ .../schur-projector-refinement/SOURCES.json | 18 ++ research/schur-projector-refinement/TASK.json | 100 +++++++++ .../schur-projector-refinement/VERIFY.json | 18 ++ research/schur-projector-refinement/verify.py | 191 ++++++++++++++++++ 5 files changed, 409 insertions(+) create mode 100644 research/schur-projector-refinement/README.md create mode 100644 research/schur-projector-refinement/SOURCES.json create mode 100644 research/schur-projector-refinement/TASK.json create mode 100644 research/schur-projector-refinement/VERIFY.json create mode 100644 research/schur-projector-refinement/verify.py diff --git a/research/schur-projector-refinement/README.md b/research/schur-projector-refinement/README.md new file mode 100644 index 0000000000..c6fc0e77d9 --- /dev/null +++ b/research/schur-projector-refinement/README.md @@ -0,0 +1,82 @@ +# Projector refinement of #4597's block Schur commutator bound + +**Task:** independent-moment (original successor result, a partial answer to #4597's open question 2). **Base:** canonical main `f626db5c`. **No κ is claimed.** + +## Background + +petalas's #4597 (head `dfeb8ca7`, open) proves the following for commuting P, Q with invertible leading d×d blocks: + +- the Schur complements satisfy rank [S, Z] ≤ min(2d, n−d); +- S and Z are idempotent when P and Q are; +- the bound is sharp over F₅. + +Its open question 2 asks for sharp bounds for projectors over a fixed field, especially F₂. + +## Results + +### 1. Parity theorem (written proof below; any field) + +If S and Z are idempotent of odd size, then [S, Z] is singular. Hence, for commuting idempotent P and Q, + +```text +rank [S,Z] ≤ min(2d, 2⌊(n−d)/2⌋). +``` + +This is strictly smaller than #4597's bound exactly when n−d is odd and n−d ≤ 2d. Example: n = 5, d = 2, where the bound drops from 3 to 2. The refinement needs idempotence. A general commuting pair over F₂ at n = 5, d = 2 reaches rank 3. + +### 2. Minimal dimensions for sharpness at small fields + +All "max" values in this table are exhaustive over every commuting idempotent pair. Every "rank" entry is an explicit verified witness. + +| field | d = 1, target rank 2 | d = 2 | +|---|---|---| +| F₅ | reached at n = 3 | rank 2 at n = 5, which equals the refined bound | +| F₃ | n = 3: max 1; **first at n = 4** | — | +| F₂ | n = 3, 4: max 1; **first at n = 5** | n = 4: max 1; rank 2 at n = 5 (refined bound); **rank 4 = 2d at n = 6** | + +So the refined bound is attained over F₂ at (n, d) = (5, 1), (5, 2) and (6, 2). Over very small fields, attaining it needs more room than over F₅. + +## Proof of the parity theorem + +**Setup.** Let A = F̄⟨s, z⟩/(s² − s, z² − z), and let u = (s − z)². Then u is central: + +```text +su = s − szs = us, and similarly for z. +``` + +**Small quotients.** On a simple A-module M, u acts as a scalar λ by Schur's lemma, so M is a module over A/(u − λ). In that quotient: + +- szs = (1 − λ)s and zsz = (1 − λ)z; +- sz + zs = s + z − λ. + +So the quotient is spanned by 1, s, z and sz, and has dimension at most 4. By Jacobson density, End(M) is a quotient of it. Hence dim M ≤ 2. + +**One-dimensional factors.** On a 1-dimensional module, s and z act as scalars, so c = sz − zs acts as 0. + +**Conclusion.** Let V = F̄^k with idempotents S and Z. Then C = [S, Z] lies in the image of A and preserves a composition series of V, so det C is the product of its determinants on the composition factors. If C is invertible, no factor is 1-dimensional. Every factor then has dimension 2, so k is even. Finally, apply this to the idempotent Schur complements S and Z, which have size n−d. ∎ + +The verifier also checks: + +- the centrality of u on every idempotent pair in M₃(F₂) and M₃(F₃); +- singularity on every idempotent pair in those algebras, whether or not the pair commutes; +- singularity on 3,000 random idempotent pairs each in M₅(F₂), M₅(F₃) and M₅(F₅). + +## Verify + +```text +python3 -B research/schur-projector-refinement/verify.py +``` + +The check takes about 50 s and uses the standard library only. + +## Limitations + +- **Minimal dimensions** are established only where an exhaustive negative is shown: n ≤ 4 over F₂ and n = 3 over F₃. Larger cells have witnesses only. +- **Not settled.** A closed-form sharp bound for every field and every (n, d). For instance, it is open whether F₂ reaches 2d for every d once n is large enough. Fixed projector ranks are not separated. +- **Not claimed.** A header density, caller, supplier or κ. + +## Open next questions + +- **Binary sharpness for all d.** Is min(2d, 2⌊(n−d)/2⌋) attained over F₂ for every d once n ≥ 3d? First step: tensor the n = 5, d = 1 binary witness with I_d, following #4597's tensor construction, and test whether the Schur structure survives. + +Credit: petalas (Nick Petalas) for #4597 and #4278. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/schur-projector-refinement/SOURCES.json b/research/schur-projector-refinement/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/schur-projector-refinement/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/schur-projector-refinement/TASK.json b/research/schur-projector-refinement/TASK.json new file mode 100644 index 0000000000..54cc880309 --- /dev/null +++ b/research/schur-projector-refinement/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": "Partial answer to #4597 OQ2: sharp Schur-commutator rank for commuting projectors over small fields.", + "budget_minutes": 60, + "stop_rule": "Stop at the parity theorem and minimal small-field witnesses.", + "outcome": "completed", + "evidence": "Parity theorem (idempotent commutator singular in odd dimension, any field) with written proof and exhaustive/random checks; refined bound min(2d, 2 floor((n-d)/2)); exhaustive commuting-idempotent maxima M3(F2), M4(F2), M3(F3); witnesses F5 n3d1, F3 n4d1, F2 n5d1, F2 n5d2, F2 n6d2 (rank 4), F5 n5d2; general-pair control reaches 3.", + "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": "Is the refined bound attained over F2 for every d when n >= 3d?", + "why_it_matters": "Completes the binary case of #4597 OQ2.", + "first_step": "Tensor the binary n=5,d=1 witness with I_d and test the Schur structure.", + "blocked_by": "None." + } + ] +} diff --git a/research/schur-projector-refinement/VERIFY.json b/research/schur-projector-refinement/VERIFY.json new file mode 100644 index 0000000000..3735334535 --- /dev/null +++ b/research/schur-projector-refinement/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": 300, + "checks": "Parity theorem checks; exhaustive commuting-idempotent maxima; six witnesses attaining the refined bound; general-pair failure control." + } + ] +} diff --git a/research/schur-projector-refinement/verify.py b/research/schur-projector-refinement/verify.py new file mode 100644 index 0000000000..1c10340b83 --- /dev/null +++ b/research/schur-projector-refinement/verify.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +"""Projector refinement of PR #4597's block Schur commutator bound (its open question 2). + +#4597 (petalas, head dfeb8ca7): for commuting P, Q with invertible leading d x d blocks, the Schur complements S, Z +satisfy rank [S,Z] <= min(2d, n-d); for idempotent P, Q the complements are idempotent; the bound is sharp over F5. + +Here, for commuting idempotent P, Q: + (1) parity theorem (PROOF in README): two idempotents never have an invertible commutator in odd dimension, over + any field, so rank [S,Z] <= min(2d, 2 floor((n-d)/2)). Checked here on every pair of idempotents (commuting or + not) in M_3(F_2) and M_3(F_3), on random idempotent pairs in M_5(F_2), M_5(F_3), M_5(F_5), and on the + algebra identities used in the proof; + (2) minimal-dimension sharpness at small fields, by exhaustive negatives over all commuting idempotent pairs + (enumerated here from the full idempotent lists) and explicit witnesses: + d = 1, rank 2: F5 at n = 3; F3 first at n = 4 (n = 3 exhaustively max 1); F2 first at n = 5 (n = 3, 4 max 1); + d = 2 over F2: rank 2 first at n = 5 (n = 4 exhaustively max 1), which is the refined bound there; + rank 4 = 2d at n = 6; + d = 2 over F5 at n = 5: rank 2, again the refined bound (the unrefined bound would be 3). +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from itertools import product +import json +import random +import sys + +WITNESSES = [ # (q, n, d, P, Q, rank) + (5, 3, 1, ((3, 2, 2), (1, 2, 1), (1, 1, 2)), ((4, 0, 4), (0, 1, 0), (2, 0, 2)), 2), + (3, 4, 1, ((2, 2, 2, 0), (0, 1, 0, 0), (2, 1, 2, 0), (2, 1, 1, 1)), + ((1, 0, 2, 1), (2, 2, 1, 1), (1, 2, 2, 0), (1, 2, 2, 0)), 2), + (2, 5, 1, ((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)), + ((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)), 2), + (2, 5, 2, ((1, 0, 0, 0, 0), (1, 1, 1, 1, 0), (1, 0, 0, 1, 0), (0, 0, 0, 1, 0), (1, 0, 1, 1, 1)), + ((1, 1, 0, 1, 1), (0, 1, 0, 0, 0), (0, 0, 1, 0, 0), (0, 1, 0, 0, 1), (0, 0, 0, 0, 1)), 2), + (2, 6, 2, ((0, 1, 1, 1, 0, 1), (1, 1, 1, 1, 1, 0), (0, 1, 1, 0, 1, 1), (1, 0, 1, 0, 1, 0), (1, 0, 1, 1, 0, 0), + (0, 1, 0, 0, 1, 0)), + ((0, 1, 0, 1, 1, 1), (1, 1, 1, 1, 0, 0), (0, 1, 0, 0, 1, 1), (0, 0, 0, 1, 0, 0), (1, 0, 1, 1, 1, 0), + (0, 0, 0, 0, 0, 1)), 4), + (5, 5, 2, ((0, 4, 4, 0, 0), (3, 3, 2, 2, 4), (2, 3, 4, 3, 1), (0, 1, 1, 4, 1), (0, 1, 1, 3, 2)), + ((4, 3, 1, 2, 1), (2, 0, 0, 0, 4), (2, 4, 1, 0, 4), (2, 3, 2, 0, 4), (1, 1, 2, 4, 3)), 2), +] + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def mul(a, b, q): + return tuple(tuple(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): + return tuple(tuple((x - y) % q 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, q): + 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] + inv = pow(rows[r][c], q - 2, q) + rows[r] = [v * inv % q for v in rows[r]] + for i in range(len(rows)): + if i != r and rows[i][c]: + f = rows[i][c] + rows[i] = [(x - f * y) % q for x, y in zip(rows[i], rows[r])] + r += 1 + return r + + +def inverse(m, q): + 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] + inv = pow(rows[c][c], q - 2, q) + rows[c] = [v * inv % q for v in rows[c]] + for i in range(n): + if i != c and rows[i][c]: + f = rows[i][c] + rows[i] = [(x - f * y) % q for x, y in zip(rows[i], rows[c])] + return tuple(tuple(r[n:]) for r in rows) + + +def schur_commutator(p, qm, d, q): + """(S, Z, rank [S,Z]) or None when a leading block is singular.""" + n = len(p) + ai, bi = inverse(block(p, 0, d, 0, d), q), inverse(block(qm, 0, d, 0, d), q) + if ai is None or bi is None: + return None + s = sub(block(p, d, n, d, n), mul(mul(block(p, d, n, 0, d), ai, q), block(p, 0, d, d, n), q), q) + z = sub(block(qm, d, n, d, n), mul(mul(block(qm, d, n, 0, d), bi, q), block(qm, 0, d, d, n), q), q) + return s, z, rank(sub(mul(s, z, q), mul(z, s, q), q), q) + + +def idempotents(n, q): + out = [] + for e in product(range(q), repeat=n * n): + m = tuple(tuple(e[i * n:(i + 1) * n]) for i in range(n)) + if mul(m, m, q) == m: + out.append(m) + return out + + +def random_idempotent(n, q, rng): + while True: + m = tuple(tuple(rng.randrange(q) for _ in range(n)) for _ in range(n)) + mi = inverse(m, q) + if mi is not None: + diag = tuple(tuple(rng.randrange(2) if i == j else 0 for j in range(n)) for i in range(n)) + return mul(mul(m, diag, q), mi, q) + + +def gaussian_binomial_count(n, q): + """Number of idempotents in M_n(F_q): sum_k [n choose k]_q q^(k(n-k)).""" + total = 0 + for k in range(n + 1): + num = den = 1 + for i in range(k): + num *= q ** (n - i) - 1 + den *= q ** (i + 1) - 1 + total += num // den * q ** (k * (n - k)) + return total + + +def main(): + # (1) parity theorem checks + for n, q in ((3, 2), (3, 3)): + ids = idempotents(n, q) + need(len(ids) == gaussian_binomial_count(n, q), "idempotent count M_%d(F_%d)" % (n, q)) + need(all(rank(sub(mul(s, z, q), mul(z, s, q), q), q) < n for s in ids for z in ids), + "odd dimension: every idempotent pair in M_%d(F_%d) has a singular commutator" % (n, q)) + for s in ids: + for z in ids: + u = mul(sub(s, z, q), sub(s, z, q), q) + need(mul(s, u, q) == mul(u, s, q) and mul(z, u, q) == mul(u, z, q), "(S-Z)^2 is central") + rng = random.Random(4597) + for n, q in ((5, 2), (5, 3), (5, 5)): + for _ in range(3000): + s, z = random_idempotent(n, q, rng), random_idempotent(n, q, rng) + need(rank(sub(mul(s, z, q), mul(z, s, q), q), q) < n, "random odd-dimension pair singular") + # (2a) exhaustive negatives over all commuting idempotent pairs + maxima = {} + for n, q in ((3, 2), (4, 2), (3, 3)): + ids = idempotents(n, q) + for d in range(1, n): + best = 0 + for p in ids: + for qm in ids: + if mul(p, qm, q) == mul(qm, p, q): + res = schur_commutator(p, qm, d, q) + if res is not None: + need(mul(res[0], res[0], q) == res[0] and mul(res[1], res[1], q) == res[1], + "Schur complements of idempotents are idempotent") + need(res[2] <= min(2 * d, 2 * ((n - d) // 2)), "refined bound") + best = max(best, res[2]) + maxima["M%d(F%d) d=%d" % (n, q, d)] = best + need(maxima == {"M3(F2) d=1": 1, "M3(F2) d=2": 0, "M4(F2) d=1": 1, "M4(F2) d=2": 1, "M4(F2) d=3": 0, + "M3(F3) d=1": 1, "M3(F3) d=2": 0}, "exhaustive maxima") + # (2b) witnesses + rows = [] + for q, n, d, p, qm, r in WITNESSES: + need(mul(p, p, q) == p and mul(qm, qm, q) == qm and mul(p, qm, q) == mul(qm, p, q), "witness inputs") + s, z, rk = schur_commutator(p, qm, d, q) + need(mul(s, s, q) == s and mul(z, z, q) == z, "witness complements idempotent") + need(rk == r == min(2 * d, 2 * ((n - d) // 2)), "witness attains the refined bound") + rows.append({"field": "F%d" % q, "n": n, "d": d, "rank": rk, "unrefined_bound": min(2 * d, n - d)}) + # failure control: without idempotence the refinement is false (general commuting pair, F2, n = 5, d = 2, rank 3) + gp = ((1, 0, 1, 0, 1), (1, 1, 1, 1, 0), (0, 0, 1, 1, 0), (1, 1, 0, 0, 1), (0, 1, 0, 0, 0)) + gq = ((1, 0, 0, 0, 1), (0, 1, 1, 1, 1), (0, 0, 1, 1, 1), (1, 0, 0, 0, 0), (0, 1, 0, 1, 1)) + need(mul(gp, gq, 2) == mul(gq, gp, 2) and mul(gp, gp, 2) != gp, "control: commuting, not idempotent") + need(schur_commutator(gp, gq, 2, 2)[2] == 3, "control: general commuting pair reaches the unrefined bound 3") + print(json.dumps({"status": "PASS_PR4597_PROJECTOR_REFINEMENT", + "general_pair_control_F2_n5_d2_rank": 3, + "parity_checks": "all idempotent pairs M3(F2), M3(F3); 3000 random pairs each M5(F2/F3/F5)", + "exhaustive_commuting_idempotent_maxima": maxima, "witnesses": rows, + "minimal_n_for_rank_2_at_d1": {"F5": 3, "F3": 4, "F2": 5}, + "new_kappa_claimed": False}, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())