diff --git a/research/sl2f3-all-dirty-minimum/PROOF.md b/research/sl2f3-all-dirty-minimum/PROOF.md
new file mode 100644
index 0000000000..9b4cf5e0e0
--- /dev/null
+++ b/research/sl2f3-all-dirty-minimum/PROOF.md
@@ -0,0 +1,174 @@
+# Five calls with any finite number of restored dirty roles
+
+This proof was produced by Nick Petalas. It extends Wentao Li's #4083 beyond
+one dirty role. The endpoint, alphabet and direct word come from Cinna Davis's
+#2010. The first-order argument builds on Sagar Thakrar's #4032 twisted
+radical-rank method. The proof below supplies the new all-role lower bound.
+
+## Statement and conventions
+
+Let G = SL2(F3), with matrix multiplication as its group law, and set
+
+```
+i = [[0,1],[-1,0]],    w = [[0,-1],[1,-1]],    c = w^-1 i w.
+```
+
+For every integer r >= 3, work in M_r(F2[G]). A paid factor is
+
+```
+D_N(g) = I + ([g]+[1])N,
+g in {i,i^-1,w,w^-1},    N = x y^t,    x,y in F2^r,    y^t x = 1.
+```
+
+The target is T = diag([i],[w],[c],1,...,1). All r roles have arbitrary
+initial values; the last r-3 roles must be restored. Arbitrary free constant
+GL_r(F2) mixing is allowed. Products are written as algebraic matrix products.
+
+**Theorem.** Every word realizing T contains at least two i/i^-1 factors and
+at least three w/w^-1 factors. The exact minimum is five for every finite r.
+
+The field of role coefficients is F2. Enlarging it is a change of model.
+Formal group-algebra equality, including all dirty roles, is required.
+
+## 1. A first-order representation of the semidirect product
+
+Let P = {+/-1,+/-i,+/-c,+/-ic}. Direct multiplication of the displayed
+matrices gives the quaternion relations i^2 = c^2 = -1 and ci = -ic.
+The matrix w has order three, and conjugation by w^-1 cycles the three
+nonzero classes i,c,ic of P/{+/-1}. Thus P is normal, P intersect <w> = {1},
+and G = <w>P has a unique expression w^a p, a in {0,1,2}, p in P.
+Indeed these expressions give 24 distinct determinant-one matrices, which
+exhaust G since its first column has 8 choices and its second then has 3.
+
+Write K = F4 = F2[omega], omega^2+omega+1 = 0. Define the additive map
+
+```
+mu(+/-1)=0,    mu(+/-i)=1,    mu(+/-c)=omega,    mu(+/-ic)=omega^2.
+```
+
+It is the identification of the binary vector space P/{+/-1} with K.
+The conjugation cycle gives mu(w^-1 p w) = mu(p) omega. For g = w^a p put
+
+```
+psi(g) = omega^a,    delta(g) = mu(p).
+```
+
+For g=w^a p and h=w^b q, gh=w^(a+b)(w^-b p w^b)q. Hence
+
+```
+psi(gh) = psi(g)psi(h),
+delta(gh) = delta(h) + delta(g)psi(h).
+```
+
+Extend psi and delta linearly to F2[G], and let aug be augmentation into F2.
+Linearity gives, for all group-algebra elements A,B,
+
+```
+delta(AB) = aug(A)delta(B) + delta(A)psi(B).
+```
+
+Apply these maps entrywise to matrices. The same identity holds with matrix
+products on the right. This is a first-order representation, equivalently
+the upper-right block of the homomorphism
+g -> [[1,delta(g)],[0,psi(g)]]. It does not assume that delta is multiplicative.
+
+## 2. Two quaternion calls are necessary
+
+Every paid factor has augmentation I. For W=F_1...F_L, repeated use of the
+matrix identity gives
+
+```
+delta(W) = sum_k delta(F_k) psi(F_(k+1)...F_L).
+```
+
+For F_k=D_N(g), delta(F_k)=delta(g)N. In our alphabet,
+delta(i)=delta(i^-1)=1 and delta(w)=delta(w^-1)=0. Each nonzero summand has
+K-rank at most one, because N has rank one. Thus
+
+```
+rank_K delta(W) <= number of i/i^-1 calls.
+```
+
+But delta(T)=diag(1,0,omega,0,...,0) has rank two. This proves the first floor
+for every r. This step is the semidirect-product extension of the predecessor's
+first-order rank argument needed here. No census is involved.
+
+## 3. At most two order-three calls are rigid
+
+Put E=diag(0,1,0,...,0). The character image of the target is
+
+```
+psi(T) = I + omega^2 E.
+```
+
+Quaternion calls map to I. A w call maps to I+omega^2 N; a w^-1 call maps
+to I+omega N. By the matrix determinant lemma their determinants are omega
+and omega^-1, respectively. The target determinant is omega.
+
+If there are no w/w^-1 calls, the determinant is wrong. If there is one,
+it must be a w call, and equality of its character image with psi(T) forces
+its projector to be E.
+
+If there are two, the determinant forces both labels to be w^-1. Write
+their binary projectors N,M in product order. Their character product is
+
+```
+(I+omega N)(I+omega M)
+ = I + NM + omega(N+M+NM),
+```
+
+whereas the target is I+E+omega E. Comparing coefficients in the binary basis
+{1,omega} gives NM=E and N+M+NM=E. Therefore N=M; idempotence then gives
+N=M=E. This argument uses binary role coefficients and holds for every r.
+
+It follows that if there are at most two order-three calls, every character
+suffix psi(F_(k+1)...F_L) is diagonal and fixes every column other than
+column 2. Quaternion factors have identity character, and the only remaining
+projector is E.
+
+## 4. The conjugated output forbids those rigid cases
+
+Use the sum in Section 2. Each quaternion contribution is N times a character
+suffix. Since N is binary and that suffix fixes every column other than
+column 2, every entry of delta(W) outside column 2 lies in F2. The other
+paid calls contribute zero.
+
+The target has delta(T)_(3,3)=omega, which is not in F2. Column 3 is different
+from column 2. This contradicts W=T. Therefore there are at least three
+w/w^-1 calls. Combined with Section 2, the length is at least five.
+
+## 5. Attainment and free mixing
+
+The inherited direct word applies i on role 1, w on role 2, and the algebraic
+product w^-1 i w on role 3. These are five paid calls with coordinate
+projectors. They have the required endpoint and act identically on every
+other role, independently of its initial value. Thus the lower bound is sharp.
+
+To include interleaved constant GL_r(F2) maps, move them to one end using
+
+```
+A^-1 D_N(g) A = D_(A^-1 N A)(g).
+```
+
+Conjugation preserves binary rank-one idempotents. The resulting expression
+is H times a pure paid word of the same length, with H in GL_r(F2).
+Augmentation of every paid factor and of T is I, so H=I. The preceding
+argument therefore covers arbitrary such free mixing and every finite amount
+of restored dirty workspace.
+
+## Scope and decision
+
+This is a scoped proof in the formal alphabet of #2010/#4083. It closes the
+two-or-more-dirty-role question in #4083 without enumerating a larger alphabet.
+Searching additional restored dirty roles cannot improve this endpoint's
+five-call bill under these hypotheses. The original three-role and one-dirty-role
+results retain predecessor credit; their enumerations are not replayed here.
+
+Clean-only inputs, partially restored roles, enlarged coefficient fields,
+different paid address operations and other targets are outside this theorem.
+The first-order map also kills the nontrivial central element -1, so it supplies
+no positive lower bound for a pure central defect. No native implementation,
+physical cost, admitted supplier, multiplication theorem or new kappa follows.
+The written proof is the all-r evidence. The verifier only corroborates finite
+instances and exposes boundary failures. Independent human and formal
+proof-kernel review are unclaimed.
diff --git a/research/sl2f3-all-dirty-minimum/README.md b/research/sl2f3-all-dirty-minimum/README.md
new file mode 100644
index 0000000000..b2b04a5a21
--- /dev/null
+++ b/research/sl2f3-all-dirty-minimum/README.md
@@ -0,0 +1,123 @@
+# The SL2(F3) conjugate triple needs five calls with any dirty workspace
+
+For every finite number of restored dirty roles, the exact formal paid-call
+minimum for `diag([i],[w],[w^-1 i w],1,...,1)` remains **five**. This is a
+scoped proof with finite corroboration. It answers Open next question 1 in
+Wentao Li's [#4083](https://github.com/CrocSwap/integer-mult-bounds/pull/4083),
+which settled one dirty role and left two or more open.
+
+The alphabet is unchanged: `G=SL2(F3)`, paid labels `i,i^-1,w,w^-1`, and
+`D_N(g)=I+([g]+[1])N` for any binary rank-one idempotent `N` on all roles.
+Here `i=[[0,1],[-1,0]]`, `w=[[0,-1],[1,-1]]` over F3. Arbitrary constant
+`GL_r(F2)` mixing is free; every input is arbitrary and every extra role must
+return unchanged. [PROOF.md](PROOF.md) proves the result for every `r>=3`.
+
+## New step and consequence
+
+The first-order representation of `Q8 semidirect C3` gives a rank-two target
+defect, forcing two quaternion-label calls. In the character quotient, any
+one- or two-call realization of the required order-three output has all its
+projectors on that output alone. Its other columns cannot acquire the
+nonbinary first-order coefficient of `w^-1 i w`. Therefore three order-three
+calls are necessary, independently of the number of restored dirty roles.
+The predecessor's coordinate word attains `2+3=5`.
+
+The new contribution is this all-role proof and the order-three projector
+rigidity argument. Cinna Davis's original three-role result
+[#2010](https://github.com/CrocSwap/integer-mult-bounds/pull/2010) and Wentao
+Li's one-dirty-role result retain their credit. Their searches are not rerun.
+Sagar Thakrar's [#4032](https://github.com/CrocSwap/integer-mult-bounds/pull/4032)
+supplies the predecessor twisted radical-rank method and the question about
+extending it to a normal 2-group with an odd-order complement.
+
+Further dirty-role censuses cannot improve this endpoint under these
+hypotheses. The decision is local to this formal alphabet. A physical native
+realization, its prices, supplier admission and a new kappa remain unproved.
+Clean-only inputs, partial restoration, other targets and enlarged coefficient
+fields are outside the result. In particular the first-order map kills the
+nonidentity central element -1; it cannot certify pure central defects.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and only the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/sl2f3-all-dirty-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/sl2f3-all-dirty-minimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sl2f3-all-dirty-minimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sl2f3-all-dirty-minimum --check-source-history
+```
+
+The registered commands use `{python}` for portability. The expected final
+marker is `PASS_SL2F3_ALL_DIRTY_MINIMUM minimum=5 i_floor=2 w_floor=3`.
+The verifier prints a generated receipt bound to all six package file hashes;
+it does not write files. No receipt is hand-authored or stored as an expected
+answer.
+
+Finite coverage is separate from the all-role proof:
+
+- All 576 group-pair cocycle identities.
+- All 308 one-call and 60,880 two-call quotient words on 2, 3 and 4 roles.
+  Exactly one of each length reaches the quotient target at each role count.
+- 312 deterministic sampled full-group-algebra words on 3, 5 and 8 roles,
+  with lengths 0 through 12. These are samples, not an exhaustive word census.
+- The five-call endpoint on all 384 regular-action basis inputs across
+  3, 5 and 8 roles, including two and five dirty roles.
+- Eleven enumerated controls: the five single-call omissions, reversed
+  conjugation, unrestored dirty output, a changed unconjugated target,
+  nonbinary projectors, wrong cocycle orientation and the central kernel.
+
+The nonbinary control exhibits two distinct F4 rank-one idempotents with
+the same quotient endpoint; the binary rigidity proof cannot be reused in
+that enlarged field. The dirty-output control passes data-only comparison
+and fails the required full endpoint. Checks use explicit exceptions under
+both normal and optimized Python.
+
+## Verification bounds
+
+All code is package-local; no predecessor executable is imported. Loops have
+fixed finite bounds, matrices have at most eight rows, sampled words have at
+most twelve factors, and the largest materialized quotient alphabet has 240
+entries. Its two-call product is streamed. Functions are below 60 lines.
+Warning-strict normal and optimized execution are the available diagnostics;
+the checkout supplies no Python linter configuration or installed static
+checker for this package.
+
+```
+Rule: 3, fixed memory before steady operation.
+Location: verify.py exact finite computations.
+Reason: CPython allocates integers, tuples and interpreter objects dynamically.
+Scope: this bounded one-shot verifier, with no input-driven growth.
+Compensating control: eight-role/twelve-factor limits and fixed fixture counts.
+Verification: both registered warning-strict replays exercise all fixtures.
+Follow-up: use fixed buffers if this verifier becomes a long-running service.
+```
+
+Sources, exact Git blobs and SHA256 hashes are in [SOURCES.json](SOURCES.json).
+Those literature and task files are provenance, not replay dependencies.
+[TASK.json](TASK.json) records the priority-7 card and the changed scope.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+Is there a fully priced native address-operation realization of this alphabet
+for a changed endpoint that could save paid work? This is the remaining
+physical-interface question from #4083, not a reason to enlarge the closed
+dirty-workspace search. Start by pinning one arbitrary-input `D_N(i)` or
+`D_N(w)` program and charging address movement, source access, hosting and
+restoration. The missing native implementation and complete producer/consumer
+bill are the blockers. No such program is supplied here.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Cinna Davis #2010 retains the endpoint, four-label alphabet and five-call
+direct word. Wentao Li / VictorLiwentao #4083 retains the one-dirty-role
+result and the explicit remaining question. Sagar Thakrar #4032 retains the
+twisted radical-rank method and its normal-2-group extension question, building
+on Cinna Davis #2116, #2047 and #2248. The retained register-model lineage
+includes Aaron Wang / navinor #1822, Ali Romman #468 and eumemic #288.
+The first-order representation and rank subadditivity are elementary tools;
+no literature-wide priority is claimed for them. The new claim is the stated
+all-role endpoint theorem and its explicit proof.
diff --git a/research/sl2f3-all-dirty-minimum/SOURCES.json b/research/sl2f3-all-dirty-minimum/SOURCES.json
new file mode 100644
index 0000000000..a706fe1021
--- /dev/null
+++ b/research/sl2f3-all-dirty-minimum/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/a4-seven-call-radical-rank/README.md",
+      "usage": "provenance",
+      "git_blob": "ab5ea83019119dcada4b654b137d418503014cf5",
+      "sha256": "26c9a90b1e73ce90b6711417db3f023e79192acdde8b94f1e7cfa0a93fafd42b"
+    },
+    {
+      "path": "research/sl2f3-conjugate-triple-seed592f/README.md",
+      "usage": "provenance",
+      "git_blob": "519b393c8cc7c6aba947b43d9c03bfa7591ed98a",
+      "sha256": "e3a491f3aa8b986e6047c9b41fb650e60a6c3f042223601257b0928ebd3771d6"
+    },
+    {
+      "path": "research/sl2f3-dirty-role-four/README.md",
+      "usage": "provenance",
+      "git_blob": "cb5fe755ea89535bab55b296e3bea6ef244c947a",
+      "sha256": "4e872b0915446491bdbaf661108e61d58b24ca0c2b58fecc98e72ca477db87d4"
+    }
+  ]
+}
diff --git a/research/sl2f3-all-dirty-minimum/TASK.json b/research/sl2f3-all-dirty-minimum/TASK.json
new file mode 100644
index 0000000000..dc9f56eb6b
--- /dev/null
+++ b/research/sl2f3-all-dirty-minimum/TASK.json
@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "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": "Scoped proof that diag([i],[w],[w^-1 i w],1,...,1) in F2[SL2(F3)] needs exactly five paid rank-one calls for every finite number of restored dirty roles, including arbitrary free constant binary mixing.",
+  "scope_change_reason": "Answer Open next question 1 in Wentao Li #4083 with an all-role proof, extending Cinna Davis #2010 and the first-order method of Sagar Thakrar #4032. The original card requests a changed nonabelian interface; this result closes a formal workspace route without claiming a native conversion.",
+  "bottleneck_link": "Eliminates arbitrary restored dirty workspace as a way to reduce the five-call bill of this explicit nonabelian target. A different endpoint or operation contract is required before native pricing is useful.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved all-role lower bound and bounded exact corroboration. Do not run predecessor censuses or expand to different endpoints.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives independent 2-call quaternion and 3-call order-three floors for every finite role count. verify.py checks the cocycle, the one/two-call quotient classification, sampled full-algebra telescoping, regular-action endpoints and eleven controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is there a fully priced native realization of this alphabet for a changed endpoint that saves paid work?",
+      "why_it_matters": "The all-role formal minimum alone cannot admit a supplier or change kappa.",
+      "first_step": "Pin one arbitrary-input D_N(i) or D_N(w) native program and charge source access, address movement, hosting and restoration.",
+      "blocked_by": "No native implementation or complete producer/consumer invoice is available here; enlarging dirty workspace for this fixed endpoint is closed."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 2010,
+      "credit": "Cinna Davis: endpoint, alphabet, original three-role minimum and direct word."
+    },
+    {
+      "pr": 4083,
+      "credit": "Wentao Li / VictorLiwentao: one restored dirty role and the two-or-more dirty-role open question."
+    },
+    {
+      "pr": 4032,
+      "credit": "Sagar Thakrar: twisted radical-rank method and normal-2-group extension question; retained Cinna Davis #2116/#2047/#2248 lineage."
+    },
+    {
+      "pr": 1822,
+      "credit": "Aaron Wang / navinor: Q8 register-model predecessor."
+    },
+    {
+      "pr": 468,
+      "credit": "Ali Romman: abelian three-register model."
+    },
+    {
+      "pr": 288,
+      "credit": "eumemic: rank-one idempotent register model."
+    }
+  ]
+}
diff --git a/research/sl2f3-all-dirty-minimum/VERIFY.json b/research/sl2f3-all-dirty-minimum/VERIFY.json
new file mode 100644
index 0000000000..dafdd037a6
--- /dev/null
+++ b/research/sl2f3-all-dirty-minimum/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Written all-role proof corroboration: exact cocycle, exhaustive small quotient rigidity, sampled full algebra, full regular-action upper word and semantic controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat every check with assertions disabled; all correctness checks use explicit exceptions."
+    }
+  ]
+}
diff --git a/research/sl2f3-all-dirty-minimum/verify.py b/research/sl2f3-all-dirty-minimum/verify.py
new file mode 100644
index 0000000000..fd12c5f1e7
--- /dev/null
+++ b/research/sl2f3-all-dirty-minimum/verify.py
@@ -0,0 +1,359 @@
+#!/usr/bin/env python3
+"""Exact finite corroboration of the separately written all-role proof."""
+
+from dataclasses import dataclass
+from hashlib import sha256
+from itertools import product
+import json
+from pathlib import Path
+from random import Random
+
+
+Matrix = tuple[tuple[int, ...], ...]
+Factor = tuple[int, int, int]
+MAX_ROLES = 8
+MAX_LENGTH = 12
+
+
+def need(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def fmul(a: int, b: int) -> int:
+    """F4 = F2[t]/(t^2+t+1), encoded by two polynomial bits."""
+    value = 0
+    for bit in range(2):
+        if b & (1 << bit):
+            value ^= a << bit
+    return value ^ 7 if value & 4 else value
+
+
+def mmul(a: Matrix, b: Matrix) -> Matrix:
+    n = len(a)
+    need(1 <= n <= MAX_ROLES and len(b) == n, "matrix size")
+    need(all(len(row) == n for row in (*a, *b)), "square matrices")
+    out = [[0] * n for _ in range(n)]
+    for row, col, inner in product(range(n), repeat=3):
+        out[row][col] ^= fmul(a[row][inner], b[inner][col])
+    return tuple(map(tuple, out))
+
+
+def madd(a: Matrix, b: Matrix) -> Matrix:
+    return tuple(tuple(x ^ y for x, y in zip(ar, br, strict=True))
+                 for ar, br in zip(a, b, strict=True))
+
+
+def scale(a: Matrix, value: int) -> Matrix:
+    return tuple(tuple(fmul(x, value) for x in row) for row in a)
+
+
+def identity(n: int) -> Matrix:
+    need(1 <= n <= MAX_ROLES, "role bound")
+    return tuple(tuple(int(i == j) for j in range(n)) for i in range(n))
+
+
+def outer(n: int, x: int, y: int) -> Matrix:
+    need(0 < x < (1 << n) and 0 < y < (1 << n), "nonzero binary vectors")
+    need((x & y).bit_count() % 2 == 1, "rank-one idempotent")
+    return tuple(tuple(((x >> i) & 1) * ((y >> j) & 1)
+                       for j in range(n)) for i in range(n))
+
+
+def qfactor(n: Matrix, value: int) -> Matrix:
+    return madd(identity(len(n)), scale(n, value ^ 1))
+
+
+def rank(a: Matrix) -> int:
+    rows = [list(row) for row in a]
+    height, width = len(rows), len(rows[0])
+    need(height <= MAX_ROLES and width <= MAX_ROLES, "rank dimensions")
+    pivots = 0
+    for col in range(width):
+        pivot = next((r for r in range(pivots, height) if rows[r][col]), None)
+        if pivot is None:
+            continue
+        rows[pivots], rows[pivot] = rows[pivot], rows[pivots]
+        inverse = (0, 1, 3, 2)[rows[pivots][col]]
+        rows[pivots] = [fmul(x, inverse) for x in rows[pivots]]
+        for r in range(height):
+            if r != pivots and rows[r][col]:
+                coefficient = rows[r][col]
+                rows[r] = [x ^ fmul(coefficient, y)
+                           for x, y in zip(rows[r], rows[pivots], strict=True)]
+        pivots += 1
+    return pivots
+
+
+def gmul(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]:
+    return ((a[0]*b[0] + a[1]*b[2]) % 3,
+            (a[0]*b[1] + a[1]*b[3]) % 3,
+            (a[2]*b[0] + a[3]*b[2]) % 3,
+            (a[2]*b[1] + a[3]*b[3]) % 3)
+
+
+@dataclass(frozen=True)
+class Model:
+    table: tuple[tuple[int, ...], ...]
+    psi: tuple[int, ...]
+    delta: tuple[int, ...]
+    unit: int
+    i: int
+    w: int
+    c: int
+    labels: tuple[int, ...]
+
+
+def make_model() -> Model:
+    group = tuple(a for a in product(range(3), repeat=4)
+                  if (a[0]*a[3] - a[1]*a[2]) % 3 == 1)
+    unit, i, w = (1, 0, 0, 1), (0, 1, 2, 0), (0, 2, 1, 2)
+    w2 = gmul(w, w)
+    c = gmul(gmul(w2, i), w)
+    ic = gmul(i, c)
+    mu = {}
+    for p, value in ((unit, 0), (i, 1), (c, 2), (ic, 3)):
+        mu[p] = value
+        mu[tuple((-x) % 3 for x in p)] = value
+    delta, psi = {}, {}
+    for h, character in ((unit, 1), (w, 2), (w2, 3)):
+        for p, value in mu.items():
+            g = gmul(h, p)
+            need(g not in delta, "unique semidirect normal form")
+            delta[g], psi[g] = value, character
+    need(len(group) == len(delta) == 24 and len(mu) == 8, "group orders")
+    need(set(group) == set(delta), "semidirect coverage")
+    for p, q in product(mu, repeat=2):
+        need(mu[gmul(p, q)] == mu[p] ^ mu[q], "Frattini homomorphism")
+    for p in mu:
+        need(mu[gmul(gmul(w2, p), w)] == fmul(mu[p], 2), "equivariance")
+    table = tuple(tuple(group.index(gmul(a, b)) for b in group) for a in group)
+    inverse_i = tuple((-x) % 3 for x in i)
+    return Model(table, tuple(psi[g] for g in group),
+                 tuple(delta[g] for g in group), group.index(unit),
+                 group.index(i), group.index(w), group.index(c),
+                 tuple(group.index(g) for g in (i, inverse_i, w, w2)))
+
+
+def check_cocycle(model: Model) -> dict:
+    pairs = 0
+    wrong_orientation = 0
+    for a, b in product(range(24), repeat=2):
+        ab = model.table[a][b]
+        need(model.psi[ab] == fmul(model.psi[a], model.psi[b]), "character")
+        expected = model.delta[b] ^ fmul(model.delta[a], model.psi[b])
+        need(model.delta[ab] == expected, "right cocycle")
+        inverse = (0, 1, 3, 2)[model.psi[b]]
+        wrong_orientation += model.delta[ab] != (model.delta[b] ^
+                                                fmul(model.delta[a], inverse))
+        pairs += 1
+    need(wrong_orientation > 0, "wrong-conjugation control")
+    need(tuple(model.delta[g] for g in model.labels) == (1, 1, 0, 0),
+         "paid-label defects")
+    need(model.delta[model.c] == 2, "conjugate defect")
+    minus_one = model.table[model.i][model.i]
+    need(minus_one != model.unit and model.delta[minus_one] == 0,
+         "central-kernel limitation")
+    return {"cocycle_pairs": pairs, "wrong_orientation_failures": wrong_orientation,
+            "cocycle_controls": ["wrong_orientation", "central_kernel"]}
+
+
+def projectors(n: int) -> tuple[Matrix, ...]:
+    need(2 <= n <= 4, "exhaustive quotient role bound")
+    matrices = tuple(outer(n, x, y) for x, y in
+                     product(range(1, 1 << n), repeat=2)
+                     if (x & y).bit_count() % 2 == 1)
+    need(len(matrices) == (2**n - 1)*2**(n - 1), "projector coverage")
+    need(len(set(matrices)) == len(matrices), "no repeated projectors")
+    return matrices
+
+
+def check_quotient() -> dict[str, int]:
+    singles = doubles = single_hits = double_hits = 0
+    for n in (2, 3, 4):
+        e = outer(n, 2, 2)
+        target = qfactor(e, 2)
+        alphabet = tuple((value, p, qfactor(p, value))
+                         for value, p in product((2, 3), projectors(n)))
+        for value, p, factor in alphabet:
+            hit = factor == target
+            need(hit == (value == 2 and p == e), "one-call rigidity")
+            singles += 1
+            single_hits += hit
+        for (v, p, a), (u, q, b) in product(alphabet, repeat=2):
+            hit = mmul(a, b) == target
+            need(hit == (v == u == 3 and p == q == e), "two-call rigidity")
+            doubles += 1
+            double_hits += hit
+    return {"quotient_single_words": singles, "quotient_double_words": doubles,
+            "quotient_single_hits": single_hits, "quotient_double_hits": double_hits}
+
+
+def translate(model: Model, mask: int, label: int, left: bool) -> int:
+    result = 0
+    for g in range(24):
+        if mask & (1 << g):
+            image = model.table[label][g] if left else model.table[g][label]
+            result ^= 1 << image
+    return result
+
+
+def ring_word(model: Model, n: int, word: tuple[Factor, ...]) -> Matrix:
+    need(3 <= n <= MAX_ROLES and len(word) <= MAX_LENGTH, "word bounds")
+    state = [[(1 << model.unit) if row == col else 0
+              for col in range(n)] for row in range(n)]
+    for label, x, y in word:
+        outer(n, x, y)
+        need(label in model.labels, "paid label")
+        column = [0] * n
+        for row, col in product(range(n), repeat=2):
+            if x & (1 << col):
+                column[row] ^= state[row][col]
+        changed = [v ^ translate(model, v, label, False) for v in column]
+        for row, col in product(range(n), repeat=2):
+            if y & (1 << col):
+                state[row][col] ^= changed[row]
+    return tuple(map(tuple, state))
+
+
+def evaluate(a: Matrix, values: tuple[int, ...]) -> Matrix:
+    out = []
+    for row in a:
+        output_row = []
+        for mask in row:
+            value = 0
+            for g in range(24):
+                if mask & (1 << g):
+                    value ^= values[g]
+            output_row.append(value)
+        out.append(tuple(output_row))
+    return tuple(out)
+
+
+def decomposition(model: Model, n: int, word: tuple[Factor, ...]) -> tuple[Matrix, Matrix]:
+    suffix = identity(n)
+    defect = scale(suffix, 0)
+    for label, x, y in reversed(word):
+        p = outer(n, x, y)
+        term = mmul(scale(p, model.delta[label]), suffix)
+        need(rank(term) <= int(model.delta[label] != 0), "rank per paid call")
+        defect = madd(defect, term)
+        suffix = mmul(qfactor(p, model.psi[label]), suffix)
+    return defect, suffix
+
+
+def check_words(model: Model) -> dict[str, int]:
+    rng = Random(1907)
+    words = 0
+    for n, length, _ in product((3, 5, 8), range(MAX_LENGTH + 1), range(8)):
+        factors = []
+        for _ in range(length):
+            x = rng.randrange(1, 1 << n)
+            ys = tuple(y for y in range(1, 1 << n)
+                       if (x & y).bit_count() % 2 == 1)
+            factors.append((rng.choice(model.labels), x, rng.choice(ys)))
+        word = tuple(factors)
+        state = ring_word(model, n, word)
+        defect, quotient = decomposition(model, n, word)
+        need(evaluate(state, model.delta) == defect, "full-algebra defect identity")
+        need(evaluate(state, model.psi) == quotient, "full-algebra quotient")
+        active = sum(model.delta[g] != 0 for g, _, _ in word)
+        need(rank(defect) <= active, "first-order rank floor")
+        words += 1
+    return {"sampled_full_algebra_words": words}
+
+
+def upper_word(model: Model) -> tuple[Factor, ...]:
+    return ((model.i, 1, 1), (model.w, 2, 2),
+            (model.labels[3], 4, 4), (model.i, 4, 4), (model.w, 4, 4))
+
+
+def target_matrix(model: Model, n: int) -> Matrix:
+    diagonal = (model.i, model.w, model.c) + (model.unit,) * (n - 3)
+    return tuple(tuple((1 << diagonal[i]) if i == j else 0
+                       for j in range(n)) for i in range(n))
+
+
+def regular_action(model: Model, n: int, word: tuple[Factor, ...],
+                   source: tuple[int, ...]) -> tuple[int, ...]:
+    state = list(source)
+    # A formal product F1...FL acts on columns by FL first.
+    for label, x, y in reversed(word):
+        total = 0
+        for row in range(n):
+            if y & (1 << row):
+                total ^= state[row]
+        change = total ^ translate(model, total, label, True)
+        for row in range(n):
+            if x & (1 << row):
+                state[row] ^= change
+    return tuple(state)
+
+
+def check_upper(model: Model) -> dict[str, int]:
+    word = upper_word(model)
+    basis_inputs = 0
+    for n in (3, 5, 8):
+        target = target_matrix(model, n)
+        need(ring_word(model, n, word) == target, "five-call formal endpoint")
+        need(rank(evaluate(target, model.delta)) == 2, "target rank two")
+        diagonal = (model.i, model.w, model.c) + (model.unit,) * (n - 3)
+        for row, address in product(range(n), range(24)):
+            source = tuple((1 << address) if j == row else 0 for j in range(n))
+            expected = tuple(translate(model, value, g, True)
+                             for value, g in zip(source, diagonal, strict=True))
+            need(regular_action(model, n, word, source) == expected,
+                 "independent regular-action basis endpoint")
+            basis_inputs += 1
+    return {"upper_role_counts": 3, "regular_basis_inputs": basis_inputs}
+
+
+def check_controls(model: Model) -> dict:
+    word, target = upper_word(model), target_matrix(model, 5)
+    controls = []
+    for omitted in range(5):
+        need(ring_word(model, 5, word[:omitted] + word[omitted + 1:]) != target,
+             "omitted-call control")
+        controls.append(f"omitted_call_{omitted}")
+    wrong_conjugate = word[:2] + (word[4], word[3], word[2])
+    need(ring_word(model, 5, wrong_conjugate) != target, "conjugate-order control")
+    controls.append("conjugate_order")
+    dirty = ring_word(model, 5, word + ((model.i, 8, 8),))
+    need(dirty != target and dirty[:3] == target[:3], "data-only equality control")
+    controls.append("unrestored_dirty_role")
+    short = ((model.i, 1, 1), (model.w, 2, 2), (model.i, 4, 4))
+    changed = [list(row) for row in target]
+    changed[2][2] = 1 << model.i
+    need(ring_word(model, 5, short) == tuple(map(tuple, changed)),
+         "unconjugated target has a three-call word")
+    controls.append("changed_target")
+    e = ((1, 0), (0, 0))
+    p, q = ((1, 1), (0, 0)), ((1, 2), (0, 0))
+    need(mmul(p, p) == p and mmul(q, q) == q and p != q,
+         "nonbinary rank-one idempotents")
+    need(mmul(qfactor(p, 3), qfactor(q, 3)) == qfactor(e, 2),
+         "binary-coefficient hypothesis is necessary for rigidity")
+    controls.append("nonbinary_projectors")
+    return {"endpoint_controls": controls}
+
+
+def main() -> None:
+    model = make_model()
+    report = {"claim_type": "scoped proof with finite corroboration",
+              "minimum_calls": 5, "quaternion_call_floor": 2,
+              "order_three_call_floor": 3,
+              "dirty_roles": "every finite number, by PROOF.md"}
+    for section in (check_cocycle(model), check_quotient(), check_words(model),
+                    check_upper(model), check_controls(model)):
+        report.update(section)
+    report["semantic_controls"] = len(report["cocycle_controls"]) + len(report["endpoint_controls"])
+    package = Path(__file__).resolve().parent
+    names = ("verify.py", "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json")
+    report["source_sha256"] = {
+        name: sha256((package / name).read_bytes()).hexdigest() for name in names}
+    print(json.dumps(report, sort_keys=True, indent=2))
+    print("PASS_SL2F3_ALL_DIRTY_MINIMUM minimum=5 i_floor=2 w_floor=3")
+
+
+if __name__ == "__main__":
+    main()