diff --git a/research/weight1-image4-irreducible-witness/PROOF.md b/research/weight1-image4-irreducible-witness/PROOF.md
new file mode 100644
index 0000000000..3dc5997404
--- /dev/null
+++ b/research/weight1-image4-irreducible-witness/PROOF.md
@@ -0,0 +1,282 @@
+# A weight-1 no-edge pool of image dimension 4 can be irreducible
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+No new κ is claimed. At the base commit the selected record is
+`363005817/100000000000`. This note does not change that record.
+`docs/research/current-priorities.md` on the same commit still quotes an
+older checkpoint; the selected record is the frontier value used here.
+
+Evidence class: a **proof** that one explicit pool meets the hypotheses
+below and acts irreducibly. The 67-element subspace lattice of its joint
+image is an **exhaustive finite census** of that one four-dimensional
+space and agrees with the proof. The width-4 through width-8 pool scans
+are finite checks of those widths. They are not a census of all
+weight-1 pattern spaces, and no search is used as a nonexistence proof.
+
+## Witness
+
+Work over `F2`. For a matrix `N`, write `off(N)` for `N` with its diagonal
+deleted. For a linear space `P` of zero-diagonal matrices, the complete
+noncoordinate pool is
+
+```text
+C(P) = {N = x y^T : y^T x = 1, off(N) ∈ P, off(N) ≠ 0}.
+```
+
+`V(P)` is the sum of the images of `C(P)`. A subspace `W ⊆ V(P)` is
+invariant when `N(W) ⊆ W` for every `N ∈ C(P)`. The action is irreducible
+when the only invariant subspaces are `0` and `V(P)`.
+
+Index coordinates by `Z/4Z`. For each `i` put
+
+```text
+x_i = e_i + e_{i+1} + e_{i+2},    N_i = x_i e_i^T,
+```
+
+and let `P` be the span of the four off-diagonal patterns, padded by zero
+rows and columns when the ambient width `W` is greater than 4. Each
+covector `e_i` has weight 1. Each image `x_i` has weight 3.
+
+**Witness.** For every `W ≥ 4`, this `P` has dimension 4 and contains no
+matrix unit, `C(P) = {N_0, N_1, N_2, N_3}`, every pool covector has weight
+1, and `dim V(P) = 4`. The action on `V(P)` is irreducible.
+
+So the answer to the question left by #7138 is no: not every weight-1
+no-edge pool of pattern dimension 4 and joint-image dimension 4 is
+reducible. The four disjoint weight-1 lines recorded in #7138 meet the
+same dimension counts and are reducible. Section 5 recalls them so this
+witness is not read as a claim that every such pool is irreducible.
+
+These four operators are the transposes of the #6962 four-cycle. There
+`M_i = e_i x_i^T` has image weight 1 and covector weight 3. Here
+`N_i = M_i^T = x_i e_i^T` swaps those weights. Completeness and
+irreducibility are proved below for `N_i`; they are not quoted from the
+argument for `M_i`, because the representation has changed.
+
+## 1. The pattern space
+
+Deleting the diagonal of `N_i` leaves
+
+```text
+p_i = E_{i+1,i} + E_{i+2,i}.
+```
+
+Column `i` has weight 2, and the other columns are zero. The four patterns
+occupy four different columns, so they are linearly independent and
+`dim P = 4`. A general element is indexed by `A ⊆ Z/4Z`,
+
+```text
+p_A = sum_{i ∈ A} p_i.
+```
+
+Column `i` of `p_A` is zero when `i ∉ A` and has weight 2 when `i ∈ A`.
+The columns are disjoint, so `p_A` has weight `2|A|`. Every nonzero
+element has weight at least 2, and `P` contains no matrix unit.
+
+## 2. The pool is exactly the four projectors
+
+Each `N_i` lies in `C(P)`: `e_i · x_i = 1`, and `off(N_i) = p_i`.
+
+Let `x, y ∈ F2^W` satisfy `y · x = 1` and `off(x y^T) ∈ P`, with the
+pattern nonzero.
+
+Both vectors are supported on `{0,1,2,3}`. Every matrix in `P` is zero in
+each row `t ≥ 4` and each column `t ≥ 4`. Suppose `x_t = 1` for some
+`t ≥ 4`. The off-diagonal part of row `t` of `x y^T` is `y` with
+coordinate `t` cleared, and that row of `P` is zero, so `y = e_t`. Then
+`y · x = 1`. Column `t` of `x y^T` is `x`, and the off-diagonal part of
+that column is zero, so `x = e_t`. The pattern is zero, which is excluded.
+Thus `x_t = 0` for every `t ≥ 4`.
+
+Suppose instead `y_t = 1`. The off-diagonal part of column `t` is zero, so
+`x ∈ {0, e_t}`. The case `x = 0` contradicts `y · x = 1`, so `x = e_t`.
+That contradicts `x_t = 0`. Thus `y_t = 0` as well. For `W = 4` there is
+no such `t`, and this paragraph is vacuous.
+
+Now `x` and `y` lie in `F2^4`. Let `T` be the support of `y`. For each
+`b ∈ T`, the off-diagonal column `b` of `x y^T` is `x` with coordinate
+`b` cleared. The only possible nonzero column of an element of `P` in
+position `b` is
+
+```text
+v_b = e_{b+1} + e_{b+2},
+```
+
+which has weight 2 and a zero in row `b`.
+
+That off-diagonal column cannot be zero. If it were, then `x = e_b` and
+`y · x = y_b = 1`. Any other index `s ∈ T` would then have off-diagonal
+column `e_b`, which has weight 1. It is neither zero nor `v_s`. So no
+such `s` exists, `T = {b}`, and the pattern is zero, which is excluded.
+Therefore every `b ∈ T` has off-diagonal column `v_b`, and
+
+```text
+x = α_b e_b + e_{b+1} + e_{b+2},    α_b = x_b.
+```
+
+If `|T| ≥ 2`, take distinct `b, s ∈ T`. The two expressions for `x` agree.
+
+When `s = b+1`, the expressions are `α e_b + e_{b+1} + e_{b+2}` and
+`β e_{b+1} + e_{b+2} + e_{b+3}`. Coordinate `b` forces `α = 0`.
+Coordinate `b+3` is 0 on the left and 1 on the right.
+
+When `s = b+2`, the expressions are `α e_b + e_{b+1} + e_{b+2}` and
+`β e_{b+2} + e_{b+3} + e_b`. Coordinate `b` forces `α = 1`. Coordinate
+`b+1` is 1 on the left and 0 on the right.
+
+Every pair in `Z/4Z` has difference 1 or 2. Both cases contradict.
+Therefore `|T| = 1`. Let `T = {b}`. Idempotence forces `α_b = 1`, so
+
+```text
+x = e_b + e_{b+1} + e_{b+2} = x_b,    y = e_b,
+```
+
+and the pattern is `p_b`. This projector is `N_b`.
+
+Hence `C(P) = {N_0, N_1, N_2, N_3}` at every width `W ≥ 4`. Every covector
+has weight 1.
+
+## 3. The joint image is four-dimensional and the kernel is zero
+
+The four images lie in `span{e_0, e_1, e_2, e_3}`. In that basis, with
+columns `x_0, x_1, x_2, x_3`, the matrix is
+
+```text
+1 0 1 1
+1 1 0 1
+1 1 1 0
+0 1 1 1.
+```
+
+Add row 0 to rows 1 and 2. Add the new row 1 to rows 2 and 3. Add the new
+row 3 to the new row 2. Add that row 2 and row 3 to row 0, then add row 2
+to row 1. The result is the identity. The four images are a basis of the
+coordinate subspace, so `dim V(P) = 4` and
+
+```text
+V(P) = span{e_0, e_1, e_2, e_3}
+```
+
+inside `F2^W`. Each covector is a distinct coordinate functional `e_i`.
+Their common kernel on `V(P)` is zero. The kernel test of #7138, which
+needs a positive-dimensional common kernel, does not see an invariant
+subspace of this pool.
+
+## 4. The action is irreducible
+
+On `V = V(P)`, the operator `N_i` is `z ↦ (e_i · z) x_i`. Let `W ⊆ V` be
+invariant and set
+
+```text
+A = {i ∈ Z/4Z : x_i ∈ W}.
+```
+
+If `i ∉ A`, then `x_i ∉ W`. For every `w ∈ W`, the vector `N_i(w)` is
+either `0` or `x_i`, so invariance forces `e_i · w = 0`. Thus
+
+```text
+W ⊆ {z ∈ V : z_i = 0 for every i ∉ A} = span{e_j : j ∈ A}.
+```
+
+The right-hand side has dimension `|A|`, and it is contained in `V`
+because Section 3 identifies `V` with the full coordinate subspace. Each
+`x_i` with `i ∈ A` therefore lies in `span{e_j : j ∈ A}`, which means
+
+```text
+{i, i+1, i+2} ⊆ A.
+```
+
+If `A` is nonempty, pick `i ∈ A`. Then `i+1 ∈ A`, then `i+2 ∈ A`, then
+`i+3 ∈ A`. So `A = Z/4Z`.
+
+The empty set forces `W ⊆ {0}`. The full set puts every `x_i` into `W`.
+Those four vectors are a basis of `V`, so `W = V`. No subspace
+`0 < W < V` is invariant.
+
+In particular no line `span(x_i)` is invariant: `e_{i+1} · x_i = 1`, so
+`N_{i+1}(x_i) = x_{i+1}`, and Section 3 says `x_{i+1}` is not a scalar
+multiple of `x_i`.
+
+## 5. The four disjoint lines stay reducible
+
+#7138, Section 5, records a different weight-1 pool. On twelve
+coordinates, for `b = 0,1,2,3`,
+
+```text
+u_b = e_{3b} + e_{3b+1} + e_{3b+2},    L_b = u_b e_{3b}^T.
+```
+
+That note proves the four operators are the complete pool of their
+pattern span: dimension 4, no matrix unit, image dimension 4, and trivial
+common kernel, with each line `span(u_b)` invariant. This package does not
+reprove that completeness statement. The operators themselves already show
+the contrast used here. Each covector has weight 1, the four images are
+independent, and `e_{3c} · u_b = 0` for `c ≠ b`, so each line is invariant
+and the common kernel on the image is zero.
+
+The same dimension counts and a trivial kernel therefore occur both for a
+reducible pool and for the irreducible witness of Sections 1 through 4.
+Kernel dimension zero does not decide the question.
+
+## 6. An irreducible example has four columns of dimension 1
+
+This lemma locates the witness. It is not a classification.
+
+Let `P` be a linear space of zero-diagonal `W` by `W` matrices with
+`dim P = 4` and with no matrix unit. Suppose every covector of `C(P)` has
+weight 1, `dim V(P) = 4`, and the action on `V(P)` is irreducible. Then
+`P` is the direct sum of four one-dimensional column spaces, on four
+distinct columns, and the four coordinate functionals are a basis of the
+dual of `V(P)`.
+
+A weight-1 covector is some `e_j`. The pattern `off(x e_j^T)` is supported
+in column `j`. Let `U_j` be the space of patterns in `P` supported in
+column `j`. Patterns in different columns occupy disjoint positions, so
+`sum_j dim U_j ≤ dim P = 4`. The hypothesis that every pool covector has
+weight 1 says that every pool pattern is a nonzero vector of some `U_j`.
+Such a vector has weight at least 2, because `P` contains no matrix unit.
+Its lift is `(e_j + v) e_j^T`.
+
+The active columns are those with `U_j ≠ 0`. Each contributes the
+coordinate functional `e_j` on `V = V(P)`, and that functional is nonzero
+because it pairs to 1 with the image `e_j + v`. The common kernel
+
+```text
+K = {z ∈ V : e_j · z = 0 for every active column j}
+```
+
+is invariant, since every pool operator is `z ↦ (e_j · z) x`. Some image
+pairs to 1 with its covector, so `K ≠ V`. Irreducibility forces `K = 0`.
+The active coordinate functionals therefore span the dual of a
+four-dimensional space, and at least four of them are linearly
+independent. Hence there are at least four active columns. Combined with
+`sum_j dim U_j ≤ 4` and `dim U_j ≥ 1` on each active column, there are
+exactly four active columns, each of dimension 1, and their sum of
+dimensions equals `dim P`. Those four lines are all of `P`.
+
+The witness in Sections 1 through 4 is one pool of this shape, and it is
+irreducible. The four lines of Section 5 are another pool of this shape,
+and they are reducible. The lemma does not say which of the two behaviors
+occurs.
+
+## 7. What this does not claim
+
+The selected κ and its five framework assumptions are unchanged. Nothing
+here re-proves the weight-1 image bound of #7138 or the all-width
+dimension-4 bound of #7139. Both already allow an irreducible joint image
+of dimension 4; #6962 attains it with covector weight 3. The new
+statement is the weight-1 case at image dimension 4.
+
+#7094 attains irreducible dimension 5 with a heavier covector. That pool
+is outside the weight-1 hypothesis, and this note does not extend it.
+
+Section 6 is not a list of the irreducible four-column pools. The finite
+scans in `verify.py` cover one pattern space, widths 4 through 8, and the
+67 subspaces of one four-dimensional image. They corroborate the
+width-independent casework. They are not a search over all
+four-dimensional pattern spaces.
+
+The note produces no rational-address word, native primitive, supplier
+admission, or multiplication identity.
diff --git a/research/weight1-image4-irreducible-witness/README.md b/research/weight1-image4-irreducible-witness/README.md
new file mode 100644
index 0000000000..57af6c08c7
--- /dev/null
+++ b/research/weight1-image4-irreducible-witness/README.md
@@ -0,0 +1,135 @@
+# A weight-1 no-edge pool of image dimension 4 can be irreducible
+
+**Witness, proved for one pool. No new κ.** The selected record stays
+`363005817/100000000000`.
+
+## Result
+
+Over `F2`, the four projectors
+
+```text
+N_i = (e_i + e_{i+1} + e_{i+2}) e_i^T,    i in Z/4Z,
+```
+
+are the complete pool of their off-diagonal pattern span at every ambient
+width at least 4. That span has dimension 4 and contains no matrix unit.
+Every covector has weight 1. The joint image has dimension 4, its common
+kernel is zero, and the action is irreducible.
+
+The answer to open question 2 of #7138 is therefore no. Not every weight-1
+no-edge pool of pattern dimension 4 and joint-image dimension 4 is
+reducible. The argument is in [PROOF.md](PROOF.md).
+
+This is one witness. The four disjoint weight-1 lines of #7138 meet the
+same dimension counts, also have trivial common kernel, and are reducible
+because each line is invariant. The kernel test, which needs image
+dimension at least `dim P + 1`, does not decide either example.
+
+These operators are the transposes of the #6962 four-cycle. That cycle has
+covector weight 3. Transposing swaps the image and the covector, so the
+weight-1 hypothesis holds here and fails there. Irreducibility is proved
+again for the transposed action.
+
+## Scope and evidence
+
+Catalogue card: `bit-new-register-model`, priority revision 8, base commit
+`e54523517d0f03e58352e647c403a5af3e525a57`. Scope status is **changed**.
+The card asks for a larger or nonabelian register alphabet. This package
+answers the weight-1 image-dimension-4 question left by #7138. The reason
+is recorded in [TASK.json](TASK.json). The original native acceptance gate
+is unmet, and the selected frontier is unchanged. No register-alphabet
+construction round is opened.
+
+[PROOF.md](PROOF.md) is the argument. Section 2 puts every factor on the
+first four coordinates and then rules out every covector of weight at
+least 2 by a pair computation on `Z/4Z`. Section 4 splits an invariant
+subspace according to which images it contains. Section 5 recalls the four
+disjoint lines without reproving their completeness. Section 6 records the
+column shape forced by a trivial kernel; it is not a classification.
+
+[verify.py](verify.py) repeats the finite parts: the sixteen pattern
+weights, the six pairs, both support checks at widths 4 through 8, the
+complete subspace lattice of `F2^4` (67 subspaces), and the controls.
+Deleting one witness projector leaves an invariant line. The four disjoint
+lines are reducible. The #6962 four-cycle is irreducible under the same
+lattice scan and has covector weight 3, so the scan is not hard-wired to
+one answer and that cycle stays outside the weight-1 hypothesis. These
+checks do not replace the width-independent casework, and they do not
+enumerate all four-dimensional pattern spaces.
+
+Evidence class: a proof for this pool, plus an exhaustive census of its
+67 image subspaces and finite pool scans at widths 4 through 8. Not a
+census of all weight-1 pattern spaces, and not a search.
+
+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. On that commit, `docs/research/current-priorities.md` still
+quotes an older selected checkpoint. This package follows
+`certificates/selected-result.json`. Nothing here reruns the selected
+baseline as a scientific replay.
+
+Overlap was checked on 2026-11-11 against open upstream pull requests.
+A search for `pattern dimension 4` returned #7094, #7138, and #7139.
+#7094 is the heavier irreducible dimension-5 witness. #7138 proves the
+weight-1 image bound 6 and reducibility for image dimension at least 5,
+and leaves image dimension 4 open. #7139 proves the all-width image bound
+6 and that dimension 6 is reducible. Searches for `weight-1 image`,
+`joint-image dimension 4`, and `every weight-1` returned no further open
+pull request. Local notes at the base commit do not contain this witness.
+The offline overlap helper had no remote snapshot; those distinctions are
+from the live pull-request search and from reading the packages. No match
+is not a novelty certificate.
+
+The predecessor package is fork pull request 260, head
+`5690b63f877654bca13e3d4777c081e7d538d7bc`, branch
+`cursor/weight1-pattern-dim4-reducible-b5eb`. No fork `cursor/*` branch
+already named this image-dimension-4 witness.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and the standard library only:
+
+```sh
+python3 -B research/weight1-image4-irreducible-witness/verify.py
+python3 -I -O -B research/weight1-image4-irreducible-witness/verify.py
+python3 -B scripts/research_package.py --package research/weight1-image4-irreducible-witness --check-only
+python3 -B scripts/research_package.py --package research/weight1-image4-irreducible-witness
+```
+
+The verifier prints `PASS_WEIGHT1_IMAGE4_IRREDUCIBLE` with `pool=4`,
+`image_dim=4`, `kernel_dim=0`, and `new_kappa=null`.
+
+Not run: Lean, Docker, the selected cold replay, and any enumeration of
+all 4096 diagonal-ones matrices. An incomplete search is not evidence in
+this package.
+
+## Open next questions
+
+Which weight-1 no-edge pools of pattern dimension 4 and joint-image
+dimension 4 are irreducible, up to coordinate permutation? The witness
+shows that reducibility can fail, and the four disjoint lines show that it
+need not fail. Section 6 of the proof says that any irreducible example
+has exactly four columns of dimension 1. The smallest next step is to
+enumerate the 4096 matrices over `F2` with ones on the diagonal and to
+decide which invertible strongly connected matrices admit extra
+coordinates that preserve the weight-1 and no-matrix-unit hypotheses,
+after writing why that list is complete. This package does not run that
+enumeration. Extra coordinates are not bounded here, so those 4096
+matrices are not yet an exhaustive domain.
+
+## Credit
+
+The fiber lemma is Nick Petalas, #5921, and is not an input: membership of
+the witness pool is the support casework in Section 2. CubeJerry, #6838,
+proved the pattern-dimension-at-most-3 total-image bound. #6921 proved the
+irreducible bound 3 for pattern dimension at most 3. #6962, package
+`research/pattern-dim4-irreducible-image`, gave the four-cycle whose
+transpose is the witness; that irreducibility proof is not reused. #7138,
+fork pull request 260, proved the weight-1 image bound 6 and left this
+dimension-4 question open; its four disjoint lines are the reducible
+control. #7139 proved the all-width image bound 6. #7094 is the heavier
+irreducible dimension-5 witness and is outside the hypothesis. This
+package does not replace those arguments.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. New work is
+Apache-2.0. No independent human or formal-kernel review is claimed.
diff --git a/research/weight1-image4-irreducible-witness/SOURCES.json b/research/weight1-image4-irreducible-witness/SOURCES.json
new file mode 100644
index 0000000000..5335fa97d9
--- /dev/null
+++ b/research/weight1-image4-irreducible-witness/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}
diff --git a/research/weight1-image4-irreducible-witness/TASK.json b/research/weight1-image4-irreducible-witness/TASK.json
new file mode 100644
index 0000000000..070caed3fc
--- /dev/null
+++ b/research/weight1-image4-irreducible-witness/TASK.json
@@ -0,0 +1,73 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "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 every weight-1 no-edge pool of pattern dimension 4 and joint-image dimension 4 is reducible.",
+  "scope_change_reason": "The card asks for a larger or nonabelian register alphabet. This package instead answers open question 2 of #7138: the weight-1 no-edge pools of pattern dimension 4 whose joint image has dimension 4, which the kernel test does not reach. No new alphabet, word, or kappa is claimed. The same card was already moved to scalar pattern-pool questions by #5921, #6838, #6921, #6962, and #7138.",
+  "bottleneck_link": "Side result. The weight-1 image bound does not decide reducibility when the joint image has dimension equal to the pattern dimension. This package does not open a new register-alphabet construction round, and the family expansion gate is not used. The original native acceptance gate remains unmet, and the selected frontier is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once one explicit weight-1 no-edge pool of pattern dimension 4 and joint-image dimension 4 is proved irreducible at every width at least 4, and the four disjoint weight-1 lines are rechecked as reducible. Do not classify all such pools, redo the image-at-most-6 theorem, or change kappa.",
+  "outcome": "completed",
+  "evidence": "PROOF.md exhibits the transpose of the #6962 four-cycle and proves that it is a complete weight-1 no-edge pool of pattern dimension 4 acting irreducibly on a four-dimensional joint image at every width at least 4. verify.py repeats the finite tables, the width-4 through width-8 pool scan, the 67-subspace lattice, and the reducible four-line and deleted-projector 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": "Which weight-1 no-edge pools of pattern dimension 4 and joint-image dimension 4 are irreducible, up to coordinate permutation?",
+      "why_it_matters": "The transpose four-cycle is irreducible, while the four disjoint weight-1 lines are reducible. Both have pattern dimension 4, image dimension 4, and trivial common kernel, so neither a single witness nor the kernel test classifies the boundary.",
+      "first_step": "Use the four-column lemma in PROOF.md: any irreducible example has exactly four columns of dimension 1. Enumerate the 4096 matrices over F2 with ones on the diagonal, keep the invertible strongly connected ones, and decide which admit extra coordinates that preserve weight-1 covectors and exclude matrix units. Write the completeness argument before calling the list a census.",
+      "blocked_by": "This package does not enumerate those matrices. Extra coordinates are not bounded here, so the 4096 matrices are not yet an exhaustive domain. A partial list would not be a classification."
+    }
+  ],
+  "coordination": {
+    "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166",
+    "question_source": "https://github.com/CrocSwap/integer-mult-bounds/pull/7138",
+    "fork_source": "https://github.com/unpaidmoon/integer-mult-bounds/pull/260",
+    "depends_on": [
+      "https://github.com/CrocSwap/integer-mult-bounds/pull/6962",
+      "https://github.com/CrocSwap/integer-mult-bounds/pull/7138"
+    ]
+  }
+}
diff --git a/research/weight1-image4-irreducible-witness/VERIFY.json b/research/weight1-image4-irreducible-witness/VERIFY.json
new file mode 100644
index 0000000000..bc7cf7ab3e
--- /dev/null
+++ b/research/weight1-image4-irreducible-witness/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": "Witness pattern weights, pair obstruction, width-4 through width-8 pool scan, 67-subspace irreducibility census, deleted-projector and four-line reducible controls, and the weight-3 four-cycle scanner control."
+    },
+    {
+      "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/weight1-image4-irreducible-witness/verify.py b/research/weight1-image4-irreducible-witness/verify.py
new file mode 100644
index 0000000000..87a854aeb0
--- /dev/null
+++ b/research/weight1-image4-irreducible-witness/verify.py
@@ -0,0 +1,327 @@
+#!/usr/bin/env python3
+"""Finite checks for one irreducible weight-1 image-dimension-4 pool.
+
+PROOF.md is the all-width argument. This program repeats the pattern
+weights, the pair obstruction, the width-4 through width-8 pool scan, and
+the 67 subspaces of the joint image. The four disjoint lines and a deleted
+projector are reducible controls. The #6962 four-cycle is a weight-3
+control. The program does not use assert, so python -O does not skip
+checks. Standard library only.
+"""
+
+import itertools
+import sys
+
+MARKER = "PASS_WEIGHT1_IMAGE4_IRREDUCIBLE"
+WIDTHS = range(4, 9)
+
+
+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 transpose_mask(mask, width):
+    out = 0
+    for row in range(width):
+        for col in range(width):
+            bit = row * width + col
+            if (mask >> bit) & 1:
+                out |= 1 << (col * width + row)
+    return out
+
+
+def witness_projectors():
+    """N_i = x_i e_i^T, x_i = e_i + e_{i+1} + e_{i+2}."""
+    projectors = []
+    for index in range(4):
+        image = (1 << index) | (1 << ((index + 1) % 4)) | (1 << ((index + 2) % 4))
+        covector = 1 << index
+        projectors.append((image, covector))
+    return tuple(projectors)
+
+
+def heavy_cycle_projectors():
+    """M_i = e_i x_i^T, the #6962 four-cycle, covector weight 3."""
+    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 disjoint_lines():
+    """The four weight-1 lines of #7138, Section 5. Operators only."""
+    projectors = []
+    for block in range(4):
+        column = 3 * block
+        image = (1 << column) | (1 << (column + 1)) | (1 << (column + 2))
+        projectors.append((image, 1 << column))
+    return tuple(projectors)
+
+
+def span_data(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(projectors, width):
+    generators = [pattern_mask(image, covector, width) for image, covector in 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 gaussian_count(dimension, rank):
+    numerator = 1
+    denominator = 1
+    for step in range(rank):
+        numerator *= (1 << dimension) - (1 << step)
+        denominator *= (1 << rank) - (1 << step)
+    return numerator // denominator
+
+
+def subspaces_of(vectors):
+    universe = list(dict.fromkeys(vectors))
+    seen = {frozenset((0,))}
+    queue = [frozenset((0,))]
+    while queue:
+        current = queue.pop()
+        for vector in universe:
+            grown = set(current)
+            grown.update(old ^ vector for old in current)
+            frozen = frozenset(grown)
+            if frozen not in seen:
+                seen.add(frozen)
+                queue.append(frozen)
+    return seen
+
+
+def is_invariant(subspace, projectors):
+    for image, covector in projectors:
+        for vector in subspace:
+            image_vector = image if dot(vector, covector) else 0
+            if image_vector not in subspace:
+                return False
+    return True
+
+
+def invariant_subspaces(projectors):
+    images = [image for image, _ in projectors]
+    dimension, pivots = span_data(images)
+    vectors = enumerate_span(pivots)
+    require(len(vectors) == (1 << dimension), "image span is not a flat of the computed rank")
+    subspaces = subspaces_of(vectors)
+    expected = sum(gaussian_count(dimension, rank) for rank in range(dimension + 1))
+    require(len(subspaces) == expected, "subspace census missed a flat")
+    invariant = [subspace for subspace in subspaces if is_invariant(subspace, projectors)]
+    return dimension, vectors, invariant
+
+
+def kernel_of(vectors, covectors):
+    return [vector for vector in vectors if all(dot(vector, covector) == 0 for covector in covectors)]
+
+
+def check_pattern_weights():
+    dimension, space = pattern_space(witness_projectors(), 4)
+    require(dimension == 4, "witness pattern dimension")
+    require(len(space) == 16, "witness pattern count")
+    weights = sorted(mask.bit_count() for mask in space)
+    require(weights == [0, 2, 2, 2, 2, 4, 4, 4, 4, 4, 4, 6, 6, 6, 6, 8], "witness pattern weights")
+    require(all(item == 0 or item >= 2 for item in weights), "witness matrix unit")
+
+
+def check_pair_obstruction():
+    def shaped(index, alpha):
+        return (alpha << index) | (1 << ((index + 1) % 4)) | (1 << ((index + 2) % 4))
+
+    for left, right in itertools.combinations(range(4), 2):
+        agreements = [
+            (alpha, beta)
+            for alpha in (0, 1)
+            for beta in (0, 1)
+            if shaped(left, alpha) == shaped(right, beta)
+        ]
+        require(agreements == [], "pair " + str(left) + "," + str(right) + " shares an image")
+    images = [image for image, _ in witness_projectors()]
+    for index in range(4):
+        require(shaped(index, 1) == images[index], "singleton lift")
+        require(dot(shaped(index, 0), 1 << index) == 0, "alpha zero is not idempotent")
+
+
+def check_pool_scans():
+    expected = sorted(witness_projectors())
+    for width in WIDTHS:
+        dimension, space = pattern_space(witness_projectors(), width)
+        require(dimension == 4, "pattern dimension at width " + str(width))
+        found = sorted(complete_pool(width, space))
+        require(found == expected, "pool at width " + str(width))
+        require(all(weight(covector) == 1 for _, covector in found), "covector weight")
+        image_rank, _ = span_data([image for image, _ in found])
+        require(image_rank == 4, "image dimension at width " + str(width))
+
+
+def check_support_closure():
+    full = {0, 1, 2, 3}
+
+    def closed(active):
+        return all({index, (index + 1) % 4, (index + 2) % 4} <= active for index in active)
+
+    require(closed(full), "the full index set is support-closed")
+    require(closed(set()), "the empty index set is vacuously support-closed")
+    for mask in range(1, 15):
+        active = {index for index in range(4) if (mask >> index) & 1}
+        require(not closed(active), "proper support set " + str(sorted(active)) + " closed")
+
+
+def check_irreducible_lattice():
+    projectors = witness_projectors()
+    dimension, vectors, invariant = invariant_subspaces(projectors)
+    require(dimension == 4, "witness image rank")
+    require(len(invariant) == 2, "witness invariant-subspace count")
+    orders = sorted(len(subspace) for subspace in invariant)
+    require(orders == [1, 16], "witness invariant subspaces are not 0 and V")
+    kernel = kernel_of(vectors, [covector for _, covector in projectors])
+    require(kernel == [0], "witness common kernel")
+    for index, (image, covector) in enumerate(projectors):
+        require(dot(image, covector) == 1, "witness idempotent")
+        neighbour = projectors[(index + 1) % 4][0]
+        require(dot(image, projectors[(index + 1) % 4][1]) == 1, "witness cross term")
+        line_rank, _ = span_data([image, neighbour])
+        require(line_rank == 2, "witness images are not independent in pairs")
+        for vector in vectors:
+            once = image if dot(vector, covector) else 0
+            twice = image if dot(once, covector) else 0
+            require(once == twice, "witness projector is not idempotent on the image")
+
+
+def check_deleted_projector():
+    kept = witness_projectors()[:3]
+    line = frozenset((0, 1 << 3))
+    require(is_invariant(line, kept), "deleted pool should keep the e3 line")
+    require(not is_invariant(line, witness_projectors()), "full pool should move the e3 line")
+    _, _, invariant = invariant_subspaces(kept)
+    proper = [subspace for subspace in invariant if len(subspace) not in (1, 16)]
+    require(proper, "deleted pool should be reducible")
+
+
+def check_disjoint_lines():
+    projectors = disjoint_lines()
+    dimension, vectors, invariant = invariant_subspaces(projectors)
+    require(dimension == 4, "four-line image rank")
+    require(all(weight(covector) == 1 for _, covector in projectors), "four-line covector weight")
+    require(kernel_of(vectors, [covector for _, covector in projectors]) == [0], "four-line kernel")
+    for image, _ in projectors:
+        line = frozenset((0, image))
+        require(is_invariant(line, projectors), "four-line span is not invariant")
+    proper = [subspace for subspace in invariant if len(subspace) not in (1, len(vectors))]
+    require(proper, "four lines should be reducible")
+
+
+def check_heavy_cycle_control():
+    projectors = heavy_cycle_projectors()
+    require(all(weight(covector) == 3 for _, covector in projectors), "four-cycle covector weight")
+    dimension, _, invariant = invariant_subspaces(projectors)
+    require(dimension == 4, "four-cycle image rank")
+    require(sorted(len(subspace) for subspace in invariant) == [1, 16], "four-cycle scanner")
+    witness = witness_projectors()
+    for index in range(4):
+        heavy_image, heavy_covector = projectors[index]
+        witness_image, witness_covector = witness[index]
+        require(heavy_image == witness_covector and heavy_covector == witness_image, "transpose factors")
+        heavy_pattern = pattern_mask(heavy_image, heavy_covector, 4)
+        witness_pattern = pattern_mask(witness_image, witness_covector, 4)
+        require(transpose_mask(heavy_pattern, 4) == witness_pattern, "transpose pattern")
+
+
+def expect_failure(function, label):
+    try:
+        function()
+    except SystemExit as stopped:
+        text = str(stopped)
+        require(text.startswith("FAIL:"), label + " did not fail closed")
+        return
+    fail(label + " did not fail")
+
+
+def bad_line_claim():
+    image = witness_projectors()[0][0]
+    require(is_invariant(frozenset((0, image)), witness_projectors()), "witness line is not invariant")
+
+
+def bad_four_line_claim():
+    projectors = disjoint_lines()
+    image = projectors[0][0]
+    require(not is_invariant(frozenset((0, image)), projectors), "four-line span should not be invariant")
+
+
+def main():
+    check_pattern_weights()
+    check_pair_obstruction()
+    check_support_closure()
+    check_pool_scans()
+    check_irreducible_lattice()
+    check_deleted_projector()
+    check_disjoint_lines()
+    check_heavy_cycle_control()
+    expect_failure(bad_line_claim, "witness line")
+    expect_failure(bad_four_line_claim, "four-line invariance")
+    print(MARKER + " pool=4 image_dim=4 kernel_dim=0 new_kappa=null")
+    return 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())