diff --git a/research/pattern-dim4-irreducible-image/PROOF.md b/research/pattern-dim4-irreducible-image/PROOF.md
new file mode 100644
index 0000000000..90de723226
--- /dev/null
+++ b/research/pattern-dim4-irreducible-image/PROOF.md
@@ -0,0 +1,249 @@
+# The no-edge irreducible bound does not stay 3 in pattern dimension 4
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. New work is
+Apache-2.0. This is a written proof for one explicit pool, checked again by
+finite enumeration. **No new κ.** The selected frontier stays
+`781451/250000000`.
+
+## 1. Statement
+
+Work over F2. For a matrix N, write off(N) for the matrix obtained by
+deleting its diagonal. Let P be a linear space of zero-diagonal W-by-W
+matrices, and define the complete noncoordinate pool
+
+    C(P) = {N = x y^T : y^T x = 1, off(N) in P, off(N) != 0}.
+
+The condition y^T x = 1 makes N a rank-one idempotent. Put
+
+    V(P) = sum_{N in C(P)} im(N),
+
+and let e(P) be the number of matrix units E_ab, a != b, contained in P.
+A subspace W ⊆ V(P) is invariant when N(W) ⊆ W for every N in C(P). The
+action is irreducible when no subspace 0 < W < V(P) is invariant.
+
+**Theorem.** For every ambient width W ≥ 4 there is a pattern space P of
+dimension 4 with e(P) = 0 whose complete pool acts irreducibly on a joint
+image of dimension 4. Explicitly, on coordinates Z/4Z,
+
+    N_i = e_i (e_i + e_{i+1} + e_{i+2})^T,    i in Z/4Z,
+
+and P is the span of their four off-diagonal patterns, padded by zero rows
+and columns when W > 4. Thus C(P) = {N_0, N_1, N_2, N_3}, dim V(P) = 4, and
+the action is irreducible.
+
+Under the same hypotheses used for pattern dimension at most 3 — a complete
+noncoordinate rank-one idempotent pool over F2, and no matrix unit — the
+irreducible joint-image bound 3 therefore does not remain an upper bound in
+pattern dimension 4.
+
+This note does not prove a replacement upper bound. It does not say that
+every pattern-dimension-4 pool is irreducible, and it does not say that 4 is
+the largest irreducible joint-image dimension. Section 6 recomputes the
+width-6 parity pool from #6838: its pattern dimension is 4 and its total
+image has dimension 5, but a four-dimensional kernel is invariant, so that
+pool does not decide the irreducible question.
+
+#6921 proves that the bound is 3 for pattern dimension at most 3. Its case
+split uses the Fano plane of a three-dimensional pattern space and is not
+reproved or reused here. The fiber lemma is not an input: membership of
+C(P) is settled by the support casework below.
+
+## 2. The four patterns
+
+Index coordinates by Z/4Z. For each i define
+
+    y_i = e_i + e_{i+1} + e_{i+2},    N_i = e_i y_i^T.
+
+Then y_i · e_i = 1, so N_i is a rank-one idempotent. Deleting the diagonal
+leaves the pattern
+
+    p_i = E_{i,i+1} + E_{i,i+2}.
+
+These four patterns occupy eight distinct positions, so they are linearly
+independent. Let P be their span. A general element is indexed by a subset
+A ⊆ Z/4Z,
+
+    p_A = sum_{i in A} p_i.
+
+Row i of p_A is zero when i is not in A. When i is in A, that row has ones
+in columns i+1 and i+2 only. Hence p_A has weight 2|A|. Every nonzero
+element has weight at least 2, so e(P) = 0 and dim P = 4.
+
+If W > 4, view each p_i as a W-by-W matrix with those two ones and with
+every other entry zero. The same weight count holds, and rows and columns
+indexed by t ≥ 4 are identically zero throughout P.
+
+The four images e_0, e_1, e_2, e_3 are independent. Once Section 4 shows
+that no further pool element exists, V(P) = span(e_0, e_1, e_2, e_3).
+
+## 3. Action on the joint image
+
+Identify V = span(e_0, e_1, e_2, e_3) with F2^4. On this space
+
+    N_i(v) = e_i    if φ_i(v) = 1,    and 0 otherwise,
+
+where φ_i = e_i* + e_{i+1}* + e_{i+2}*. In the basis e_0, e_1, e_2, e_3 the
+covector matrix, with rows φ_0 through φ_3, is
+
+    1 1 1 0
+    0 1 1 1
+    1 0 1 1
+    1 1 0 1.
+
+Row operations over F2 produce a permutation of the identity. Add row 0 to
+rows 2 and 3; add the new row 2 to rows 1 and 0; add the new row 1 to row 3
+and then to row 0; add the resulting row 3 to rows 0 and 2. The rows are
+then e_0*, e_2*, e_1*, and e_3*. Swapping the middle two rows gives the
+identity. The four functionals are therefore a basis of V*. Their common
+kernel on V is zero. Each column of the matrix has weight 3, so each basis
+vector e_j is sent to a different basis vector by at least two of the
+projectors.
+
+## 4. The pool is exactly the four projectors
+
+Let x, y in F2^W satisfy y · x = 1 and off(x y^T) in P, with the pattern
+nonzero.
+
+First, both vectors are supported on {0, 1, 2, 3}. Suppose some t ≥ 4 has
+x_t = 1. Row t of every matrix in P is zero, so the off-diagonal part of
+row t of x y^T is zero. That row, with its diagonal entry removed, is y
+with coordinate t cleared. Thus y vanishes off t, so y = y_t e_t. Idempotence
+gives y_t = x_t = 1. Column t of P is zero, so its off-diagonal entries
+x_i y_t = x_i vanish for i ≠ t. Hence x = e_t and the pattern is zero,
+which is excluded from C(P). Therefore x_t = 0 for every t ≥ 4.
+
+Suppose instead y_t = 1. Column t then contributes x_i for every i ≠ t, and
+those entries must vanish, so x vanishes off t. Combined with x_t = 0 this
+gives x = 0, contradicting y · x = 1. Thus y_t = 0 as well.
+
+Now x and y are vectors in F2^4, still with y · x = 1. Let S be the support
+of x. For each i in S, row i of the pattern is the off-diagonal part of y,
+so the shape of P forces
+
+    y_{i-1} = 0    and    y_{i+1} = y_{i+2}.
+
+In particular y vanishes on S - 1 = {i - 1 : i in S}. Indices are read in
+Z/4Z, so i+3 = i-1. Every nonempty S is a rotate of one of the five types
+below, and the argument is stated for an arbitrary index, so it covers
+every rotate.
+
+**|S| = 4.** Then S - 1 = S, so y = 0 and the pairing is 0.
+
+**|S| = 3.** Let S be the complement of {t}. Then y vanishes off {t-1}. The
+pairing is y_{t-1}, so y = e_{t-1}. The constraint at i = t+1, which lies
+in S, says y_{t+2} = y_{t-1}. The left side is 0 and the right side is 1.
+
+**|S| = 2, opposite.** Let S = {i, i+2}. The two constraints give
+y_{i-1} = y_{i+1} = 0 and y_{i+1} = y_{i+2}, y_{i+3} = y_i. Hence
+y_{i+2} = 0. Since y_i = y_{i+3} = y_{i-1} = 0, the covector is zero.
+
+**|S| = 2, adjacent.** Let S = {i, i+1}. The constraints give y_i = 0,
+y_{i-1} = 0, y_{i+1} = y_{i+2}, and y_{i+2} = y_{i+3}. The pairing reduces
+to y_{i+1} = 1, so y_{i+2} = 1. But y_{i+3} = y_{i-1} = 0, and the last
+constraint says those two bits agree.
+
+**|S| = 1.** Let S = {i}. Then y_i = 1, y_{i-1} = 0, and y_{i+1} = y_{i+2}.
+If y_{i+1} = 0, then y = e_i and the pattern is zero, which is excluded.
+If y_{i+1} = 1, then y = e_i + e_{i+1} + e_{i+2}, and the pattern is p_i.
+That projector is N_i.
+
+The empty support is impossible. Therefore C(P) = {N_0, N_1, N_2, N_3} at
+every width W ≥ 4, and dim V(P) = 4.
+
+## 5. The action is irreducible
+
+Let A(W) = {i : φ_i does not vanish on W}, for a subspace W ⊆ V. If the
+subspace is invariant and φ_i does not vanish on it, the corresponding image
+e_i lies in it. The four functionals span V*, so A(W) is nonempty whenever
+W is nonzero. They are distinct, so φ_i = ψ has at most one solution i for
+a given nonzero functional ψ.
+
+**Lines.** Each i in A(W) puts a distinct basis vector e_i into W, so a line
+has |A| ≤ 1. It cannot be 0. If A = {i}, the line is span(e_i), but column
+i of the covector matrix has two further ones, so some other φ_k also hits
+e_i and |A| ≥ 2.
+
+**Planes.** Three or more basis vectors cannot fit in a plane, so |A| ≤ 2.
+The case |A| = 1 would require some e_i in the plane and φ_k(e_i) = 0 for
+every k ≠ i, contradicting the column weight. Thus |A| = 2, the plane is
+span(e_i, e_j), and the other two functionals vanish on both basis vectors.
+All six pairs fail that test:
+
+| pair | a functional outside the pair that hits the pair |
+| --- | --- |
+| {0,1} | φ_2(e_0) = 1 |
+| {0,2} | φ_1(e_2) = 1 |
+| {0,3} | φ_1(e_3) = 1 |
+| {1,2} | φ_0(e_1) = 1 |
+| {1,3} | φ_0(e_1) = 1 |
+| {2,3} | φ_0(e_2) = 1 |
+
+**Hyperplanes.** Let H = ker(ψ) with ψ ≠ 0. For each i outside A(H),
+φ_i vanishes on H, so φ_i = ψ. At most one such i exists, hence |A(H)| ≥ 3.
+If |A(H)| = 4, then H contains every basis vector and H = V. If
+|A(H)| = 3, the three included basis vectors force ψ to be the remaining
+coordinate functional e_j*, and the omitted index must be j, so
+φ_j = e_j*. But φ_j has weight 3, not 1.
+
+No proper nonzero subspace is invariant. The action on V(P) is irreducible,
+and the irreducible joint-image dimension 4 is attained in pattern
+dimension 4.
+
+Deleting N_3 leaves the line span(e_0 + e_1 + e_3) in the common kernel of
+φ_0, φ_1, and φ_2. That line is invariant for the proper subpool. The
+four-projector statement uses the whole pool.
+
+## 6. The parity pool one dimension higher is reducible
+
+#6838 records the even-parity construction moved up one dimension as a scope
+control: pattern dimension 4, total joint image 5. It is recomputed here
+only to show that it does not already answer the irreducible question. This
+is not a new total-image bound.
+
+Use coordinates {0, 1, 2, 3, 4, 5}. Let U be the set of vectors supported
+on {1, 2, 3, 4, 5} whose weights are even. Then U is a four-dimensional
+subspace and contains no weight-one vector. Set
+
+    P_par = {u e_0^T : u in U},    N_u = (e_0 + u) e_0^T
+
+for each nonzero u in U. Every matrix in P_par is supported in column 0,
+and its weight equals the weight of u. Thus e(P_par) = 0 and dim P_par = 4.
+Each N_u is a rank-one idempotent with pattern u e_0^T. These 15 patterns
+are all the nonzero elements of P_par, so the displayed projectors are the
+complete pool. For distinct nonzero u, v in U,
+
+    (e_0 + u) + (e_0 + v) + (e_0 + u + v) = e_0,
+
+so e_0 lies in V(P_par) and then every u does. Hence
+
+    V(P_par) = span(e_0) ⊕ U,    dim V(P_par) = 5.
+
+Every covector is e_0. The subspace U is the kernel of e_0 on V(P_par). It
+is nonzero and proper, and every projector kills it. The action is
+reducible. The parity construction therefore shows that total image 5
+occurs in pattern dimension 4, and it does not show that an irreducible
+image of dimension greater than 3 occurs. The four-cycle of Sections 2
+through 5 is what shows that the irreducible bound changes.
+
+## 7. What this does not claim
+
+The selected κ and its five framework assumptions are unchanged. The
+dimension-at-most-3 theorem of #6921 is cited, not reproved. Nothing here
+is a paid-rank accounting for a three-relation word; that is question 1 of
+#6921 and is untouched. No upper bound is claimed for irreducible joint
+images in pattern dimension 4, and no classification of all such pools is
+claimed. The finite scans in `verify.py` cover one 16-element vector space
+and widths 4 through 8. They corroborate the width-independent casework;
+they are not a search over all four-dimensional pattern spaces. A failed
+search would not have been a proof.
+
+The note produces no rational-address word, native primitive, supplier
+admission, or multiplication identity.
+
+## Open next questions
+
+The packaged question is whether some complete no-edge pool of pattern
+dimension 4 acts irreducibly in joint-image dimension 5 or more. The parity
+pool is not an example. A single explicit witness, or a scoped upper bound
+with the same hypotheses, would be the next useful step. Absence from a
+partial search would not settle it.
diff --git a/research/pattern-dim4-irreducible-image/README.md b/research/pattern-dim4-irreducible-image/README.md
new file mode 100644
index 0000000000..2550d5ade4
--- /dev/null
+++ b/research/pattern-dim4-irreducible-image/README.md
@@ -0,0 +1,92 @@
+# Pattern dimension 4 irreducible image
+
+**Result.** The no-edge irreducible joint-image bound does not stay 3 when
+the pattern space has dimension 4. For every ambient width at least 4, the
+four projectors
+
+```text
+N_i = e_i (e_i + e_{i+1} + e_{i+2})^T,    i in Z/4Z,
+```
+
+are the complete pool of their pattern span. That span is four-dimensional
+and contains no matrix unit. The joint image is four-dimensional and the
+action is irreducible. **No new κ.** The selected value remains
+`781451/250000000`.
+
+This is an existence result under the same complete-pool and no-matrix-unit
+hypotheses as #6921. It is not an upper bound, and it is not a classification
+of every pattern-dimension-4 pool.
+
+## Scope and evidence
+
+Catalogue card: `bit-new-register-model`, priority revision 8, base commit
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. Scope status: **changed**. The
+card asks for a new register alphabet. This package answers open question 2
+of #6921, which #6921 left open because its Fano-plane case split stops at
+pattern dimension 3. The reason is recorded in [TASK.json](TASK.json). The
+original native acceptance gate is unmet, and the selected frontier is
+unchanged. Question 1 of #6921, paid-rank accounting after a relation split,
+is not this result.
+
+[PROOF.md](PROOF.md) is the argument. Section 4 puts every factor on the
+first four coordinates and then splits the support of the image vector by
+size. Section 5 splits invariant subspaces into lines, planes, and
+hyperplanes. Section 6 recomputes the #6838 width-6 parity pool: pattern
+dimension 4, total image 5, and a four-dimensional invariant kernel. That
+pool is reducible, so it does not by itself show that the irreducible bound
+changes.
+
+[verify.py](verify.py) repeats the finite parts: the covector matrix, the
+sixteen pattern weights, the six plane pairs, both support checks at widths
+4 through 8, the complete subspace lattice of F2^4 (67 subspaces), and the
+negative controls. Deleting one cycle projector leaves an invariant line.
+The #6921 three-projector example remains irreducible, and the normal-form
+triple remains reducible, so the lattice scan is not hard-wired to one
+answer. These checks do not replace the width-independent casework, and
+they do not enumerate all four-dimensional pattern spaces.
+
+Source pins are in [SOURCES.json](SOURCES.json). The catalogue and selected
+record are provenance at the base commit. Full Git history is needed to
+resolve them. Nothing here reruns the selected baseline as a scientific
+replay.
+
+Overlap was rechecked on 2026-11-10 against 885 open upstream PRs and 6934
+discussion records at base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The
+only records containing the question are #6921 and its finding,
+discussion comment 19474334. Both leave pattern dimension 4 open. #6785 is
+a one-edge exclusion and #6782 is an edge-quotient bound. No match is not
+a novelty certificate; those distinctions are from reading the records.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and the standard library only:
+
+```sh
+python3 -B research/pattern-dim4-irreducible-image/verify.py
+python3 -I -O -B research/pattern-dim4-irreducible-image/verify.py
+python3 -B scripts/research_package.py --package research/pattern-dim4-irreducible-image --check-only
+python3 -B scripts/research_package.py --package research/pattern-dim4-irreducible-image
+```
+
+The verifier prints `PASS_PATTERN_DIM4_IRREDUCIBLE_IMAGE`.
+
+## Open next questions
+
+1. **Irreducible dimension above 4, still at pattern dimension 4.** Can a
+   complete no-edge pool of pattern dimension 4 act irreducibly on a joint
+   image of dimension 5 or more? The four-cycle attains 4, so the old bound
+   fails, but it gives no replacement ceiling. The parity pool attains total
+   dimension 5 and is reducible. The smallest next step is one explicit pool
+   with a written invariant-subspace check, or a scoped upper bound under
+   these same hypotheses. No support reduction here makes an exhaustive
+   search finite, so a search that finds nothing would not be a proof.
+
+## Credit
+
+Nick Petalas, #5921, for the fiber lemma and the joint-image question; this
+proof does not rely on the fiber lemma. CubeJerry, #6838, for the total-image
+bound in pattern dimension at most 3 and for the parity pool rechecked in
+Section 6. #6921 proved the irreducible bound 3 for pattern dimension at
+most 3 and isolated this dimension-4 question; that theorem is not reproved.
+#6785 and #6782 are one-edge and edge-quotient context. Prepared by
+unpaidmoon with substantial Cursor Grok assistance. New work is Apache-2.0.
diff --git a/research/pattern-dim4-irreducible-image/SOURCES.json b/research/pattern-dim4-irreducible-image/SOURCES.json
new file mode 100644
index 0000000000..594089b9c7
--- /dev/null
+++ b/research/pattern-dim4-irreducible-image/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}
diff --git a/research/pattern-dim4-irreducible-image/TASK.json b/research/pattern-dim4-irreducible-image/TASK.json
new file mode 100644
index 0000000000..8cfb1a4328
--- /dev/null
+++ b/research/pattern-dim4-irreducible-image/TASK.json
@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Whether the no-edge irreducible joint-image bound stays 3 when the off-diagonal pattern space has dimension 4.",
+  "scope_change_reason": "The card asks for a larger or nonabelian register alphabet. This package instead answers open question 2 of #6921: the irreducible bound for a complete no-edge pool in pattern dimension 4. No new alphabet, word, or kappa is claimed. The same card was already moved to scalar pattern-pool questions by #5921, #6838 and #6921.",
+  "bottleneck_link": "Side result. The dimension-at-most-3 theorem does not transfer to pattern dimension 4, so a later word argument cannot quote bound 3 there. The original native acceptance gate remains unmet, and the selected frontier is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the four-cycle pool is proved complete and irreducible at every width at least 4, and the width-6 parity pool is rechecked as reducible. Do not classify all pattern-dimension-4 pools or start paid-rank accounting.",
+  "outcome": "completed",
+  "evidence": "PROOF.md shows that the four cyclic projectors form a complete no-edge pool of pattern dimension 4 and act irreducibly on a four-dimensional joint image at every width at least 4. The same note recomputes the #6838 width-6 parity pool and shows that its five-dimensional image has a four-dimensional invariant kernel. verify.py repeats the finite tables, the F2^4 subspace census, the width-4 through width-8 pool scan, and the negative controls.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance with the case analysis and the package verifier. Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a complete no-edge pool of pattern dimension 4 act irreducibly on a joint image of dimension 5 or more?",
+      "why_it_matters": "The four-cycle shows that irreducible dimension 4 occurs, so bound 3 fails, but it does not decide whether 4 is an upper bound. The width-6 parity pool has total image 5 and is reducible, so it is not a witness for a larger irreducible image.",
+      "first_step": "Either give one explicit complete no-edge pattern-dimension-4 pool with joint-image dimension at least 5 and a written invariant-subspace check, or prove an upper bound under these same hypotheses.",
+      "blocked_by": "No support reduction in this package bounds the search, and a search that finds no example would not be a proof."
+    }
+  ],
+  "coordination": {
+    "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166",
+    "question_source": "https://github.com/CrocSwap/integer-mult-bounds/pull/6921",
+    "depends_on": [
+      "https://github.com/CrocSwap/integer-mult-bounds/pull/6921",
+      "https://github.com/CrocSwap/integer-mult-bounds/pull/6838"
+    ]
+  }
+}
diff --git a/research/pattern-dim4-irreducible-image/VERIFY.json b/research/pattern-dim4-irreducible-image/VERIFY.json
new file mode 100644
index 0000000000..47c8c76ce3
--- /dev/null
+++ b/research/pattern-dim4-irreducible-image/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Four-cycle pattern space, complete pool at widths 4 through 8, F2^4 irreducibility census, parity-pool and deleted-projector controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same checks with assert statements disabled; the verifier raises SystemExit instead of using assert."
+    }
+  ]
+}
diff --git a/research/pattern-dim4-irreducible-image/verify.py b/research/pattern-dim4-irreducible-image/verify.py
new file mode 100644
index 0000000000..a67c62c685
--- /dev/null
+++ b/research/pattern-dim4-irreducible-image/verify.py
@@ -0,0 +1,320 @@
+#!/usr/bin/env python3
+"""Finite checks for the pattern-dimension-4 four-cycle pool.
+
+PROOF.md is the all-width argument. This program repeats the finite tables,
+the complete subspace lattice of the joint image, and the width-4 through
+width-8 pool scan. It also runs negative controls. It does not use assert,
+so python -O does not skip checks. Standard library only.
+"""
+
+import itertools
+import sys
+
+MARKER = "PASS_PATTERN_DIM4_IRREDUCIBLE_IMAGE"
+WIDTHS = range(4, 9)
+PARITY_IMAGES = (7, 11, 13, 19, 21, 25, 31, 35, 37, 41, 47, 49, 55, 59, 61)
+
+
+def fail(message):
+    raise SystemExit("FAIL: " + message)
+
+
+def require(condition, message):
+    if not condition:
+        fail(message)
+
+
+def weight(mask):
+    return mask.bit_count()
+
+
+def dot(left, right):
+    return weight(left & right) & 1
+
+
+def pattern_mask(image, covector, width):
+    mask = 0
+    for row in range(width):
+        if ((image >> row) & 1) == 0:
+            continue
+        for col in range(width):
+            if row != col and ((covector >> col) & 1):
+                mask |= 1 << (row * width + col)
+    return mask
+
+
+def cycle_projectors():
+    """N_i = e_i (e_i + e_{i+1} + e_{i+2})^T on Z/4Z."""
+    projectors = []
+    for index in range(4):
+        image = 1 << index
+        covector = (1 << index) | (1 << ((index + 1) % 4)) | (1 << ((index + 2) % 4))
+        projectors.append((image, covector))
+    return tuple(projectors)
+
+
+def rows_of(image, covector, width):
+    return [covector if ((image >> row) & 1) else 0 for row in range(width)]
+
+
+def matmul(left, right, width):
+    product = []
+    for row in left:
+        acc = 0
+        for index in range(width):
+            if (row >> index) & 1:
+                acc ^= right[index]
+        product.append(acc)
+    return product
+
+
+def gaussian_count(dimension, rank):
+    """Number of rank-dimensional subspaces of F2^dimension."""
+    numerator = 1
+    denominator = 1
+    for step in range(rank):
+        numerator *= (1 << dimension) - (1 << step)
+        denominator *= (1 << rank) - (1 << step)
+    return numerator // denominator
+
+
+def span_data(masks):
+    """Return (dimension, pivot map) for the XOR-span of masks."""
+    pivots = {}
+    for mask in masks:
+        value = mask
+        while value:
+            bit = value & -value
+            known = pivots.get(bit)
+            if known is None:
+                for other, vector in list(pivots.items()):
+                    if vector & bit:
+                        pivots[other] = vector ^ value
+                pivots[bit] = value
+                break
+            value ^= known
+    return len(pivots), pivots
+
+
+def enumerate_span(pivots):
+    vectors = [0]
+    for vector in pivots.values():
+        vectors += [old ^ vector for old in vectors]
+    return vectors
+
+
+def pattern_space(width):
+    generators = [pattern_mask(image, covector, width) for image, covector in cycle_projectors()]
+    dimension, pivots = span_data(generators)
+    return dimension, set(enumerate_span(pivots))
+
+
+def complete_pool(width, space):
+    found = []
+    for image, covector in itertools.product(range(1 << width), repeat=2):
+        if dot(image, covector) != 1:
+            continue
+        mask = pattern_mask(image, covector, width)
+        if mask and mask in space:
+            found.append((image, covector))
+    return found
+
+
+def subspace_masks(dimension):
+    """Every XOR-closed subset of F2^dimension, as a membership bitmask.
+
+    Bit v of the membership mask is set when vector v belongs to the subset.
+    The scan covers the power set, so the list is the complete subspace lattice.
+    """
+    size = 1 << dimension
+    found = []
+    for membership in range(1 << size):
+        if (membership & 1) == 0:
+            continue
+        closed = True
+        members = [vector for vector in range(size) if (membership >> vector) & 1]
+        for left in members:
+            for right in members:
+                if ((membership >> (left ^ right)) & 1) == 0:
+                    closed = False
+                    break
+            if not closed:
+                break
+        if closed:
+            found.append(membership)
+    return found
+
+
+def preserves(membership, projectors):
+    size = membership.bit_length()  # only used as a bound; vectors are below 1<<dim
+    for vector in range(size):
+        if ((membership >> vector) & 1) == 0:
+            continue
+        for image, covector in projectors:
+            if dot(covector, vector) and ((membership >> image) & 1) == 0:
+                return False
+    return True
+
+
+def generated_span(seed, projectors):
+    """Smallest subspace containing seed and closed under the projectors."""
+    span = {0, seed}
+    growing = True
+    while growing:
+        growing = False
+        for vector in list(span):
+            for image, covector in projectors:
+                if dot(covector, vector) and image not in span:
+                    span.update(old ^ image for old in tuple(span))
+                    growing = True
+                    break
+            if growing:
+                break
+    return span
+
+
+def check_covector_basis():
+    rows = [covector for _image, covector in cycle_projectors()]
+    require(rows == [0b0111, 0b1110, 0b1101, 0b1011], "cycle covectors moved: %s" % (rows,))
+    for index, row in enumerate(rows):
+        require(weight(row) == 3, "covector %s does not have weight 3" % index)
+        require(dot(1 << index, row) == 1, "projector %s is not idempotent" % index)
+    matrix = [row for row in rows]
+    # The row operations written in PROOF.md section 3.
+    matrix[2] ^= matrix[0]
+    matrix[3] ^= matrix[0]
+    matrix[1] ^= matrix[2]
+    matrix[0] ^= matrix[2]
+    matrix[3] ^= matrix[1]
+    matrix[0] ^= matrix[1]
+    matrix[0] ^= matrix[3]
+    matrix[2] ^= matrix[3]
+    require(matrix == [1, 4, 2, 8],
+            "covector reduction did not reach e0, e2, e1, e3: %s" % matrix)
+    matrix[1], matrix[2] = matrix[2], matrix[1]
+    require(matrix == [1, 2, 4, 8], "swapping the middle covector rows did not reach the identity")
+    for column in range(4):
+        hits = [row for row in rows if (row >> column) & 1]
+        require(len(hits) == 3, "column %s has weight %s" % (column, len(hits)))
+
+
+def check_pattern_space_and_pool():
+    expected = cycle_projectors()
+    for image, covector in expected:
+        rows = rows_of(image, covector, 4)
+        require(matmul(rows, rows, 4) == rows, "matrix square failed for %s, %s" % (image, covector))
+    for width in WIDTHS:
+        dimension, space = pattern_space(width)
+        require(dimension == 4, "pattern dimension at width %s is %s" % (width, dimension))
+        require(len(space) == 16, "pattern space at width %s is not 16 vectors" % width)
+        for mask in space:
+            if mask == 0:
+                continue
+            require(weight(mask) >= 2 and weight(mask) % 2 == 0,
+                    "pattern weight %s at width %s is not a positive even number" % (weight(mask), width))
+        unit = 1 << 1  # E_01 in row-major layout
+        require(weight(unit) == 1 and unit not in space, "E_01 was not detected as a missing edge")
+        edge_line = {0, unit}
+        require(any(weight(mask) == 1 for mask in edge_line),
+                "the edge control space does not contain a matrix unit")
+        found = complete_pool(width, space)
+        require(sorted(found) == sorted(expected),
+                "width %s pool is %s" % (width, sorted(found)))
+        for image, covector in found:
+            require(image < 16 and covector < 16, "a factor uses a coordinate outside Z/4Z")
+
+
+def check_irreducible_lattice():
+    projectors = cycle_projectors()
+    memberships = subspace_masks(4)
+    by_size = {}
+    for membership in memberships:
+        by_size[weight(membership)] = by_size.get(weight(membership), 0) + 1
+    expected_sizes = {1 << rank: gaussian_count(4, rank) for rank in range(5)}
+    require(by_size == expected_sizes,
+            "F2^4 subspace census %s does not match the Gaussian counts %s" % (by_size, expected_sizes))
+    invariant = [membership for membership in memberships
+                 if weight(membership) not in (1, 16) and preserves(membership, projectors)]
+    require(invariant == [], "the four-cycle lattice has an invariant subspace")
+    for seed in range(1, 16):
+        require(generated_span(seed, projectors) == set(range(16)),
+                "seed %s does not generate the joint image" % seed)
+
+    plane_failures = (
+        (0, 1, 2, 0),
+        (0, 2, 1, 2),
+        (0, 3, 1, 3),
+        (1, 2, 0, 1),
+        (1, 3, 0, 1),
+        (2, 3, 0, 2),
+    )
+    rows = [covector for _image, covector in projectors]
+    seen_pairs = set()
+    for left, right, outsider, hit in plane_failures:
+        seen_pairs.add(frozenset((left, right)))
+        require((rows[outsider] >> hit) & 1,
+                "plane pair %s,%s is not rejected by phi_%s" % (left, right, outsider))
+    require(len(seen_pairs) == 6, "the six coordinate planes were not all tested")
+
+
+def check_deletion_control():
+    kept = cycle_projectors()[:3]
+    line = 0b1011  # e0 + e1 + e3
+    for image, covector in kept:
+        require(dot(covector, line) == 0, "a retained projector moves the deleted-pool line")
+    image, covector = cycle_projectors()[3]
+    require(dot(covector, line) == 1 and image == 8, "N_3 does not move the control line")
+    require(generated_span(line, kept) == {0, line}, "the deleted pool does not leave this line invariant")
+
+
+def check_known_actions():
+    # #6921 sharp example, restricted to span(e0, e1, e2). Must be irreducible.
+    sharp = ((0b001, 0b111), (0b010, 0b011), (0b100, 0b101))
+    sharp_spaces = subspace_masks(3)
+    require(sum(gaussian_count(3, rank) for rank in range(4)) == len(sharp_spaces),
+            "F2^3 subspace census is incomplete")
+    sharp_invariant = [item for item in sharp_spaces if weight(item) not in (1, 8) and preserves(item, sharp)]
+    require(sharp_invariant == [], "the dimension-3 sharp example was reported reducible")
+    # Normal-form triple from #6921. Must be reducible.
+    normal = ((0b110, 0b101), (0b101, 0b110), (0b111, 0b111))
+    normal_invariant = [item for item in sharp_spaces if weight(item) not in (1, 8) and preserves(item, normal)]
+    require(normal_invariant != [], "the normal-form triple was reported irreducible")
+
+
+def check_parity_pool():
+    images = []
+    for mask in range(32):
+        if weight(mask) % 2 == 0:
+            images.append(1 ^ (mask << 1))
+    images = [image for image in images if image != 1]
+    require(sorted(images) == sorted(PARITY_IMAGES),
+            "parity images differ from the #6838 width-6 witness: %s" % sorted(images))
+    projectors = tuple((image, 1) for image in images)
+    patterns = [pattern_mask(image, 1, 6) for image, _covector in projectors]
+    dimension, pivots = span_data(patterns)
+    require(dimension == 4, "parity pattern dimension is %s" % dimension)
+    for mask in enumerate_span(pivots):
+        require(weight(mask) != 1, "parity pattern space contains a matrix unit")
+    image_dimension, image_pivots = span_data(images)
+    require(image_dimension == 5, "parity joint image has dimension %s" % image_dimension)
+    kernel = [vector for vector in enumerate_span(image_pivots) if (vector & 1) == 0]
+    require(len(kernel) == 16, "parity kernel on the joint image has size %s" % len(kernel))
+    require(any(vector & 1 for vector in enumerate_span(image_pivots)),
+            "parity image has no vector with a nonzero e0 coordinate")
+    # U is invariant because every covector is e0.
+    require(all(dot(1, vector) == 0 for vector in kernel), "parity kernel is not the e0 kernel")
+
+
+def main():
+    check_covector_basis()
+    check_pattern_space_and_pool()
+    check_irreducible_lattice()
+    check_deletion_control()
+    check_known_actions()
+    check_parity_pool()
+    print(MARKER)
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())