diff --git a/research/pr4597-schur-exhaustive/README.md b/research/pr4597-schur-exhaustive/README.md
new file mode 100644
index 0000000000..dcd3848e3d
--- /dev/null
+++ b/research/pr4597-schur-exhaustive/README.md
@@ -0,0 +1,59 @@
+# Exhaustive check of #4597's block Schur commutator bound on all commuting pairs
+
+**Task:** independent-moment (independent check). **Base:** canonical main `f626db5c`. **No κ is claimed.**
+
+## The claim
+
+petalas's #4597 (head `dfeb8ca7`) concerns commuting P and Q over a field whose leading d×d blocks A and B are invertible. It proves that the Schur complements S and Z satisfy
+
+- **the identity** [S, Z] = XV − UY;
+- **the bound** rank [S, Z] ≤ min(2d, n−d);
+- **the equality criterion:** rank 2d exactly when [X U] and [V; −Y] both have rank 2d.
+
+Its finite corroboration covers the polynomial families (P, P²) and one GL₄(F₂) orbit.
+
+## What is checked here
+
+This package covers **every commuting pair** in M₃(F₂), M₃(F₃) and M₄(F₂), and every split 1 ≤ d < n with A and B invertible. Nothing is imported from #4597.
+
+- **Enumeration.** Pairs are generated as Q in the centralizer of P, a nullspace computed here.
+- **Symmetry reduction.** P runs over orbit representatives under simultaneous block-diagonal conjugation by GL_d × GL_{n−d}. This preserves every quantity checked. Results are weighted by orbit size.
+- **Totals.** The weights recover the exact number of commuting pairs: 7,456, 809,433 and 2,526,976 respectively.
+
+## Results
+
+The identity, the bound and the equality criterion hold for **every** admitted pair.
+
+| domain | d | bound | admitted pairs | rank 0 / 1 / 2 | idempotent pairs, max rank |
+|---|---|---|---|---|---|
+| M₃(F₂) | 1 | 2 | 1,864 | 1,684 / 132 / 48 | 1 |
+| M₃(F₂) | 2 | 1 | 1,104 | 1,104 / 0 / 0 | 0 |
+| M₃(F₃) | 1 | 2 | 359,748 | 237,060 / 64,512 / 58,176 | 1 |
+| M₃(F₃) | 2 | 1 | 267,840 | all 0 | 0 |
+| M₄(F₂) | 1 | 2 | 631,744 | 428,128 / 140,112 / 63,504 | 1 |
+| M₄(F₂) | 2 | 2 | 336,096 | 275,256 / 30,168 / 30,672 | 1 |
+| M₄(F₂) | 3 | 1 | 241,248 | all 0 | 0 |
+
+- **The bound is attained.** General commuting pairs reach min(2d, n−d) whenever it is at least 2: M₃ at d = 1 over F₂ and F₃, and M₄(F₂) at d = 1 and 2.
+- **When n − d = 1**, the commutator always vanishes, as it must for a 1×1 commutator.
+- **Finding, relevant to #4597's open question 2.** **Commuting idempotent pairs never exceed rank 1** in these exhaustive domains: F₂ with n = 3, 4 and F₃ with n = 3. The 2d bound is therefore not attained by binary or ternary projectors at these sizes, even where general commuting pairs attain it.
+- **Positive control.** Over F₅, #4597's sharpness field, the verifier exhibits a commuting idempotent pair in M₃ with commutator rank 2 = 2d at d = 1. So the gap depends on the field, not on the code.
+
+## Verify
+
+```text
+python3 -B research/pr4597-schur-exhaustive/verify.py
+```
+
+The check takes about 80 s and uses the standard library only.
+
+## Limitations
+
+- **Sizes.** Coverage is exhaustive only at n ≤ 4 over F₂ and n = 3 over F₃. This corroborates the written proof but does not replace it.
+- **The idempotent finding** is an exhaustive statement at these sizes. It is not a theorem for larger n.
+
+## Open next questions
+
+- **Binary projectors.** Do commuting binary idempotent pairs reach commutator rank 2d at a larger n, or is there a field-dependent bound below 2d for F₂ and F₃? First step: enumerate commuting idempotent pairs in M₅(F₂) and M₆(F₂) directly, as simultaneously diagonalizable pairs M·diag·M⁻¹, with d = 1 and 2.
+
+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/pr4597-schur-exhaustive/SOURCES.json b/research/pr4597-schur-exhaustive/SOURCES.json
new file mode 100644
index 0000000000..a2a5ea8bbd
--- /dev/null
+++ b/research/pr4597-schur-exhaustive/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/pr4597-schur-exhaustive/TASK.json b/research/pr4597-schur-exhaustive/TASK.json
new file mode 100644
index 0000000000..a61202fd79
--- /dev/null
+++ b/research/pr4597-schur-exhaustive/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": "Independent exhaustive coverage of a new algebraic bound (#4597) beyond its polynomial-family corroboration.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at M_4(F_2).",
+  "outcome": "completed",
+  "evidence": "All commuting pairs in M3(F2), M3(F3), M4(F2) (7,456 / 809,433 / 2,526,976) and all splits: identity, bound and equality criterion hold for every admitted pair; bound attained by general pairs; commuting idempotent pairs max rank 1 in all domains; F5 idempotent control reaches 2.",
+  "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": "Do binary commuting idempotents reach 2d at larger n?",
+      "why_it_matters": "#4597 OQ2 (fixed-field sharp bounds).",
+      "first_step": "Enumerate simultaneously diagonalizable idempotent pairs in M5(F2), M6(F2).",
+      "blocked_by": "None."
+    }
+  ]
+}
diff --git a/research/pr4597-schur-exhaustive/VERIFY.json b/research/pr4597-schur-exhaustive/VERIFY.json
new file mode 100644
index 0000000000..92a2915d7a
--- /dev/null
+++ b/research/pr4597-schur-exhaustive/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": 400,
+      "checks": "Every commuting pair in M3(F2), M3(F3), M4(F2), every split: identity, rank bound, equality criterion; pair totals; max ranks; idempotent max rank 1; F5 idempotent rank-2 control."
+    }
+  ]
+}
diff --git a/research/pr4597-schur-exhaustive/verify.py b/research/pr4597-schur-exhaustive/verify.py
new file mode 100644
index 0000000000..7d58ec18a5
--- /dev/null
+++ b/research/pr4597-schur-exhaustive/verify.py
@@ -0,0 +1,226 @@
+#!/usr/bin/env python3
+"""Exhaustive check of PR #4597 (petalas) on all commuting pairs: block Schur commutator identity and rank bound.
+
+#4597 (head dfeb8ca7) proves, for commuting P = [[A,R],[C,D]], Q = [[B,L],[E,F]] over a field with invertible d x d
+leading blocks A, B (not assumed to commute), S = D - C A^-1 R, Z = F - E B^-1 L:
+    [S,Z] = X V - U Y,  U = C A^-1 - E B^-1, V = A^-1 R - B^-1 L, X = W - E B^-1 H, Y = T - H B^-1 L,
+    rank [S,Z] <= min(2d, n-d), with equality 2d iff [X U] has column rank 2d and [V; -Y] has row rank 2d,
+where PQ = [[H,T],[W,J]]. Its finite corroboration covers the polynomial families (P, P^2) and one GL_4(F_2) orbit.
+
+This verifier covers every commuting pair (P, Q) in M_3(F_2), M_3(F_3) and M_4(F_2), and every split 1 <= d < n
+with A and B invertible. It is written independently (nothing imported from #4597):
+  * commuting pairs are enumerated as Q in the centralizer of P, a nullspace computed here over F_q;
+  * P runs over orbit representatives of simultaneous block-diagonal conjugation by GL_d x GL_{n-d}, which maps
+    commuting pairs to commuting pairs, A, B to conjugates, S, Z, X, U, V, Y to conjugates/equivalents, and so
+    preserves invertibility of A, B, both ranks and the identity; every result is weighted by the orbit size, so
+    the reported counts are exact counts over all pairs (checked against the total number of commuting pairs);
+  * for each admitted pair it checks the identity entrywise, the bound, and the equality criterion, and records
+    the commutator-rank distribution, the maximum attained rank, and the same restricted to idempotent pairs.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+from collections import Counter
+from itertools import product
+import json
+import sys
+
+COMMUTING_PAIRS = {(3, 2): 7456, (3, 3): 809433, (4, 2): 2526976}   # recomputed below from centralizer dimensions
+
+
+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 neg(a, q):
+    return tuple(tuple(-x % q for x in r) for r in a)
+
+
+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 = [list(r) for r in m]
+    r = 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 all_matrices(n, q):
+    for e in product(range(q), repeat=n * n):
+        yield tuple(tuple(e[i * n:(i + 1) * n]) for i in range(n))
+
+
+def centralizer(p, q):
+    """All Q with PQ = QP, from a nullspace basis over F_q."""
+    n = len(p)
+    eqs = []
+    for i, j in product(range(n), repeat=2):
+        row = [0] * (n * n)
+        for k in range(n):
+            row[k * n + j] = (row[k * n + j] + p[i][k]) % q
+            row[i * n + k] = (row[i * n + k] - p[k][j]) % q
+        eqs.append(row)
+    rows, pivots, r = [x[:] for x in eqs], [], 0
+    for c in range(n * n):
+        piv = next((i for i in range(r, len(rows)) if rows[i][c]), None)
+        if piv is None:
+            continue
+        rows[r], rows[piv] = rows[piv], 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])]
+        pivots.append(c)
+        r += 1
+    free = [c for c in range(n * n) if c not in pivots]
+    basis = []
+    for f in free:
+        v = [0] * (n * n)
+        v[f] = 1
+        for i, c in enumerate(pivots):
+            v[c] = -rows[i][f] % q
+        basis.append(v)
+    out = []
+    for coeffs in product(range(q), repeat=len(basis)):
+        v = [sum(c * b[t] for c, b in zip(coeffs, basis)) % q for t in range(n * n)]
+        out.append(tuple(tuple(v[i * n:(i + 1) * n]) for i in range(n)))
+    return out
+
+
+def block_group(n, d, q):
+    g1 = [g for g in all_matrices(d, q) if inverse(g, q) is not None]
+    g2 = [g for g in all_matrices(n - d, q) if inverse(g, q) is not None]
+    out = []
+    for a, b in product(g1, g2):
+        g = tuple(tuple(a[i] + (0,) * (n - d)) for i in range(d)) + tuple(tuple((0,) * d + b[i]) for i in range(n - d))
+        out.append((g, inverse(g, q)))
+    return out
+
+
+def orbit_reps(n, d, q):
+    group, seen, reps = block_group(n, d, q), set(), []
+    for p in all_matrices(n, q):
+        if p in seen:
+            continue
+        orbit = {mul(mul(g, p, q), gi, q) for g, gi in group}
+        seen |= orbit
+        reps.append((p, len(orbit)))
+    need(sum(s for _, s in reps) == q ** (n * n), "orbits partition M_n")
+    return reps
+
+
+def check_pair(p, qm, d, q):
+    n = len(p)
+    a, r_, c_, dd = block(p, 0, d, 0, d), block(p, 0, d, d, n), block(p, d, n, 0, d), block(p, d, n, d, n)
+    b, l_, e_, f_ = block(qm, 0, d, 0, d), block(qm, 0, d, d, n), block(qm, d, n, 0, d), block(qm, d, n, d, n)
+    ai, bi = inverse(a, q), inverse(b, q)
+    if ai is None or bi is None:
+        return None
+    pq = mul(p, qm, q)
+    h, t, w = block(pq, 0, d, 0, d), block(pq, 0, d, d, n), block(pq, d, n, 0, d)
+    s = sub(dd, mul(mul(c_, ai, q), r_, q), q)
+    z = sub(f_, mul(mul(e_, bi, q), l_, q), q)
+    comm = sub(mul(s, z, q), mul(z, s, q), q)
+    u = sub(mul(c_, ai, q), mul(e_, bi, q), q)
+    v = sub(mul(ai, r_, q), mul(bi, l_, q), q)
+    x = sub(w, mul(mul(e_, bi, q), h, q), q)
+    y = sub(t, mul(mul(h, bi, q), l_, q), q)
+    need(comm == sub(mul(x, v, q), mul(u, y, q), q), "identity [S,Z] = XV - UY")
+    rk = rank(comm, q)
+    need(rk <= min(2 * d, n - d), "rank bound")
+    left = tuple(xr + ur for xr, ur in zip(x, u))
+    right = v + neg(y, q)
+    need((rk == 2 * d) == (rank(left, q) == 2 * d and rank(right, q) == 2 * d), "equality criterion")
+    idem = mul(p, p, q) == p and mul(qm, qm, q) == qm
+    return rk, idem
+
+
+def survey(n, q):
+    total = sum(len(centralizer(p, q)) for p in all_matrices(n, q))
+    need(total == COMMUTING_PAIRS[(n, q)], "commuting pairs in M_%d(F_%d)" % (n, q))
+    out = {}
+    for d in range(1, n):
+        dist, idem_dist, pairs = Counter(), Counter(), 0
+        for p, size in orbit_reps(n, d, q):
+            for qm in centralizer(p, q):
+                pairs += size
+                res = check_pair(p, qm, d, q)
+                if res is not None:
+                    dist[res[0]] += size
+                    if res[1]:
+                        idem_dist[res[0]] += size
+        need(pairs == total, "orbit weights recover every commuting pair")
+        out[d] = {"bound": min(2 * d, n - d), "admitted": sum(dist.values()),
+                  "rank_distribution": {str(k): v for k, v in sorted(dist.items())},
+                  "max_rank": max(dist), "idempotent_rank_distribution":
+                  {str(k): v for k, v in sorted(idem_dist.items())}}
+    return out
+
+
+def main():
+    results = {"M3(F2)": survey(3, 2), "M3(F3)": survey(3, 3), "M4(F2)": survey(4, 2)}
+    for name, res in results.items():
+        for d, r in res.items():
+            need(r["max_rank"] <= r["bound"], "bound")
+    # controls: the bound is attained in M3 at d = 1 over F2 and F3, and in M4(F2) at d = 1 and d = 2
+    need(results["M3(F2)"][1]["max_rank"] == 2 and results["M3(F3)"][1]["max_rank"] == 2, "M3, d = 1 attains 2")
+    need(results["M4(F2)"][1]["max_rank"] == 2 and results["M4(F2)"][2]["max_rank"] == 2, "M4(F2) attains bound")
+    need(all(r[n - 1]["max_rank"] == 0 for r, n in ((results["M3(F2)"], 3), (results["M3(F3)"], 3),
+                                                     (results["M4(F2)"], 4))), "n - d = 1 forces rank 0")
+    # finding: commuting idempotent pairs never reach 2d in these exhaustive domains (maximum 1)
+    idem_max = {name: {d: max(map(int, r["idempotent_rank_distribution"])) for d, r in res.items()}
+                for name, res in results.items()}
+    need(all(m <= 1 for res in idem_max.values() for m in res.values()), "idempotent pairs stay at rank <= 1")
+    need(idem_max["M3(F3)"][1] == 1 and idem_max["M4(F2)"][1] == 1 and idem_max["M4(F2)"][2] == 1, "rank 1 attained")
+    # positive control: over F5 (the #4597 sharpness field) a commuting idempotent pair in M_3 reaches 2 at d = 1
+    p5 = ((3, 2, 2), (1, 2, 1), (1, 1, 2))
+    q5 = ((4, 0, 4), (0, 1, 0), (2, 0, 2))
+    need(mul(p5, q5, 5) == mul(q5, p5, 5), "F5 control commutes")
+    need(check_pair(p5, q5, 1, 5) == (2, True), "F5 control: idempotent pair with commutator rank 2 = 2d")
+    print(json.dumps({"status": "PASS_PR4597_EXHAUSTIVE_COMMUTING_PAIRS", "results": results,
+                      "idempotent_max_rank": idem_max, "f5_idempotent_control_rank": 2,
+                      "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())