diff --git a/research/ut3-f4-nilpotent-tariff/README.md b/research/ut3-f4-nilpotent-tariff/README.md
new file mode 100644
index 0000000000..f23ff81827
--- /dev/null
+++ b/research/ut3-f4-nilpotent-tariff/README.md
@@ -0,0 +1,264 @@
+# Nilpotent calls do not lower the six-label UT3(F4) central tariff
+
+The central triple in Wentao Li's [PR #3788](https://github.com/CrocSwap/integer-mult-bounds/pull/3788)
+still needs exactly **twelve calls** after admitting every nonzero binary
+rank-one scalar coupling, including nilpotents. Each letter class needs at
+least six calls, for any finite number of restored dirty registers. This
+answers that package's first Open next question.
+
+Claim type: **scoped algebraic proof with exact finite corroboration**.
+The new step removes the scalar-idempotence restriction. The predecessor's
+twelve-call coordinate word remains the attaining construction and retains
+its credit. This is no new kappa, physical supplier or complete multiplication
+theorem. No predecessor executable is imported or replayed.
+
+## Model and theorem
+
+The proof has a short extension-field formulation. Let K be any field of
+characteristic two and let G=UT3(K), with
+
+```text
+(x,y,z)(x',y',z') = (x+x', y+y', z+z'+xy').
+X_alpha=(alpha,0,0), Y_beta=(0,beta,0), Z_z=(0,0,z).
+```
+
+Work in Mat_r(F2[G]). A paid call is
+
+```text
+D_N(g) = I + ([g]+[1]) N,
+N = u v^T,  u,v in F2^r nonzero,
+g = X_alpha or Y_beta,  alpha,beta in K nonzero.
+```
+
+No condition is imposed on v^T u. Trace one gives an idempotent N; trace
+zero gives a nilpotent N. Both are valid reversible calls because
+`([g]+[1])^2=0`, so `D_N(g)^2=I` regardless of N squared. Scalar GL_r(F2)
+mixing is free in this formal model. There are no free address maps, clean
+roles, COPY, ERASE, higher-rank calls or unpaid inverse calls.
+
+For arbitrary finite r>=d>=1 and nonzero z_1,...,z_d in K, require equality
+of the whole formal endpoint
+
+```text
+T = diag([Z_z1],...,[Z_zd],[1],...,[1]).
+```
+
+Every input, including every restored role, is arbitrary dirty data.
+
+**Theorem.** Every realizing word has n_X>=2d and n_Y>=2d. If all nonzero
+axis coefficients are available, the exact unit tariff is 4d, attained on
+the d target coordinates without extra roles. With positive uniform
+per-class prices A and B, the exact bill is 2d(A+B).
+
+For K=F4=F2[omega]/(omega^2+omega+1), the available alphabet is precisely
+the six labels of #3788. Setting d=3 and `(z_1,z_2,z_3)=(1,omega,omega^2)`
+gives n_X,n_Y>=6 and exact minimum twelve. The extension to arbitrary K
+uses the same proof, rather than an extrapolation from the F4 computation.
+
+## Proof
+
+First normalize scalar mixing. Moving each scalar map to the end conjugates
+the scalar rank-one matrices, preserving the allowed set. Augmentation
+`[g] -> 1` sends every paid call and T to I, so the residual scalar map is I.
+It suffices to prove the bound for a word of paid calls alone. This
+normalization is inherited from the register-model lineage.
+
+Use the associative K-algebra
+
+```text
+Q = K<X,Y> / (X^2, Y^2, all words of length at least three).
+```
+
+Its basis is `1,X,Y,XY,YX`. Define the F2-algebra map
+
+```text
+phi([x,y,z]) = 1 + xX + yY + zXY + (z+xy)YX.
+```
+
+Here scalars are extended from F2 to K only in the necessary-condition
+codomain; payloads and scalar couplings remain binary. Multiplication of
+the displayed polynomials has first-order coefficients x+x' and y+y',
+XY coefficient z+z'+xy', and YX coefficient
+
+```text
+z+xy+z'+x'y'+yx'
+  = (z+z'+xy') + (x+x')(y+y').
+```
+
+These are exactly phi of the group product. Therefore phi extends linearly
+and multiplicatively from the full formal group algebra. It need not be
+faithful. In particular,
+
+```text
+phi(D_N(X_alpha)) = I + alpha N X,
+phi(D_N(Y_beta))  = I + beta N Y.
+```
+
+Write the image of a realizing word as `I+AX+BY+CXY+DYX`. The endpoint gives
+
+```text
+A=B=0,  C=D=diag(z_1,...,z_d,0,...,0),  rank_K C=rank_K D=d.
+```
+
+For all X calls, factor N_i=u_i v_i^T and form the K-matrices
+
+```text
+U_X = [alpha_1 u_1 ... alpha_nX u_nX],
+V_X = [v_1^T; ...; v_nX^T].
+```
+
+Their product is A, hence zero. Every contribution to C selects an X call
+followed by a Y call, so its column space lies in col(U_X). Every
+contribution to D selects a Y call followed by an X call, so its row space
+lies in row(V_X). Noncommuting scalar matrix products keep their order;
+only their image and row-space inclusions are used. Consequently
+
+```text
+rank_K U_X >= d,  rank_K V_X >= d.
+```
+
+Since U_X V_X=0, im(V_X) is contained in ker(U_X), inside K^nX. Rank-nullity
+now gives `n_X >= rank_K U_X + rank_K V_X >= 2d`. Interchanging X and Y
+uses the columns of D and rows of C and gives n_Y>=2d. No step uses
+`v_i^T u_i=1`, any workspace dimension bound, or a split of coefficients
+into complementary binary summands.
+
+For attainment, on target coordinate i use the inherited coordinate word
+`X_zi,Y_1,X_zi,Y_1`. Its group product is Z_zi and it acts identically on
+all other coordinates. Concatenating the d words has exactly 2d calls of
+each class and restores every extra dirty role. It also attains the
+positive uniform-price lower bill. This completes the proof.
+
+The degree-two quotient and rank-nullity strategy are credited to
+steph4n-gh #1573, Arham Tahir #1589 and Hanson Sun #1607. The new use of
+the address coefficient field in the quotient removes the idempotence
+restriction in the F4 handoff and gives the characteristic-two formulation.
+No novelty is claimed for rank-nullity or the inherited coordinate word.
+
+## Exact finite evidence
+
+[verify.py](verify.py) is a new standard-library implementation. It uses
+F4 coefficient Gaussian elimination, a full F2 group-algebra operator, and
+a separately implemented literal regular action. The latter applies each
+axis update directly to every group address and dirty basis input. Both
+implementations share the checked F4 multiplication table; they are not
+independent human or proof-kernel reviews.
+
+The generated [RESULT.json](RESULT.json) authenticates all five source and
+metadata files and records:
+
+- All 16 F4 products agree with polynomial reduction modulo
+  `omega^2+omega+1`. All 4,096 group products satisfy the displayed quotient
+  homomorphism. All 256 two-by-two F4 matrices have twice their F4 rank
+  under an independent binary regular-representation rank calculation.
+- All 160,435 two-role expanded-alphabet words through length three satisfy
+  the extension-field coefficient-span inequalities. Of these, 112,446
+  contain at least one nilpotent call. All 2,971 words through length two
+  also agree between quotient and full formal implementations. For those
+  words, the literal regular action additionally compares all 5,942
+  identity-address input columns with the full formal coefficient vectors.
+- Nine coordinate endpoint fixtures with one through four central targets
+  and up to two dirty spectators agree formally. The separate regular
+  action checks all 1,856 basis columns of these endpoints.
+- All 294 six-label rank-one calls on three roles are formal involutions,
+  including the 126 calls formed from the 21 nilpotent couplings. These
+  counts are corroborating alphabet checks, not new idempotent-count results.
+- Twelve deleted-call controls fail the required full endpoint. Additional
+  named controls cover a wrong coefficient, an error visible only on dirty
+  workspace, four illegal call descriptions, noncentral first-order terms,
+  higher-rank parallel calls and a nonzero four-term formal polynomial
+  killed by the quotient. Thus quotient equality alone never admits an
+  endpoint.
+
+The general coefficient-span checks use
+`n_X >= rank[A C]+rank[A;D]-rank A` and its Y counterpart, the #1607
+inequalities over the new coefficient field. They corroborate the proof's
+matrix inclusions. The length-three enumeration is **not** a search through
+length eleven and is not the reason the minimum is twelve.
+
+## Reproduction
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ut3-f4-nilpotent-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ut3-f4-nilpotent-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/ut3-f4-nilpotent-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ut3-f4-nilpotent-tariff --check-source-history
+```
+
+Elsewhere replace the interpreter path with CPython 3.12. Normal replay is
+read-only. `verify.py --emit` prints a freshly computed, source-bound receipt
+to standard output. It does not overwrite package files. Expected marker:
+
+```text
+PASS_UT3_F4_NILPOTENT_TARIFF minimum=12 nX=6 nY=6 short_words=160435 involutions=294 no_new_kappa
+```
+
+Registered normal and optimized commands each have a 120-second timeout.
+The source/history preflight applies after the package is committed.
+
+## Scope, provenance and credit
+
+This package was produced by Nick Petalas. Independent human and formal
+proof-kernel review are unclaimed. Apache-2.0.
+
+The explicit source context is canonical main
+`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+[SOURCES.json](SOURCES.json) pins the predecessor texts and historical
+catalogue/selected-record provenance. They are context, not imported runtime
+code or predecessor replay obligations. [TASK.json](TASK.json) records the
+scope change from a new-alphabet card to #3788's explicit coupling extension.
+
+Credit Wentao Li #3774/#3788 for the F4 target, six-label idempotent theorem,
+coordinate words and nilpotent-coupling question; Cinna Davis #2261 for the
+F4 central-pair and three-output direction; Arham Tahir #1589 for arbitrary
+rank-one binary UT3 couplings and the two-corner quotient; Hanson Sun #1607
+for nonzero-first-order coefficient-span bounds; steph4n-gh #1573 for the
+all-register central rank proof; James Reed #3783-#3786 for parallel retained
+F4 calculations; and the eumemic/woklerx/Gareth Davidson register-model
+lineage. Nick Petalas #3800 is earlier finite reconstruction, not the proof
+of this newly expanded alphabet. All predecessor notices remain unchanged.
+
+Entry overlap used 365 open PR bodies and 3,819 Discussion records with
+complete pagination. Sparse local coverage was only 80 of 6,319 note paths;
+separate distinctive searches read all-main READMEs and merged PRs for this
+object, and the touching F4 PR bodies were read. No matching delivered
+nilpotent extension was found in that coverage. This is not a novelty
+guarantee. The advance claim is in
+[handoff #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133313).
+
+No finite word census through length eleven, proof-assistant formalization,
+native realization, compiler/hosting/precision/tape invoice, selected cold
+replay or outer analytic transfer was run. The physical price of these
+formal calls remains unknown. The selected conditional kappa stays
+0.00302015. Hosted CI is separate from the local evidence.
+
+## Open next questions
+
+Can a physically realizable additional address operation escape this exact
+axis-alphabet tariff with a favorable complete bill? Start with one pinned
+supplier's literal entry/call/exit contract, and charge the new operation's
+frames, preparation, dirty restoration, hosting and precision. This matters
+because neither nilpotent scalar mixing nor extra workspace can save calls
+inside the present model. The blocker is a legal physical realization and
+a justified recursive price; a new abstract label alone is insufficient.
+Structured details are in [TASK.json](TASK.json).
+
+## Implementation bounds
+
+The verifier has no recursion, subprocess, network or write path. Enumeration
+is capped at three calls from 54 two-role factors; endpoint words have at
+most 32 calls, five roles and 64 group elements. Rank matrices have at most
+ten rows and ten columns. Source/receipt reads are bounded at 65,537 bytes,
+with files over 65,536 rejected. Every function is shorter than 60 lines.
+Checks use exceptions and remain active under optimized Python.
+
+Power-of-Ten rule 3 has a managed-runtime deviation: Python dynamically
+allocates integers, tuples and bounded temporary matrices. The fixed domains
+above bound live algorithmic memory; Python allocator internals are not
+instrumented. Rules concerning raw pointers and preprocessing have no direct
+Python equivalent; calls are direct, with only fixed standard-library
+iteration/JSON callbacks. Warning-strict normal and optimized execution and
+AST inspection supply the available diagnostics. No static type checker is
+configured for this standalone package; no shared tooling is changed.
diff --git a/research/ut3-f4-nilpotent-tariff/RESULT.json b/research/ut3-f4-nilpotent-tariff/RESULT.json
new file mode 100644
index 0000000000..d6e0416891
--- /dev/null
+++ b/research/ut3-f4-nilpotent-tariff/RESULT.json
@@ -0,0 +1,41 @@
+{
+  "claim_type": "scoped proof with finite corroboration",
+  "controls": {
+    "dirty_restore": 1,
+    "higher_rank_excluded": 1,
+    "invalid_calls": 4,
+    "kernel_support": 4,
+    "noncentral_first_order": 1,
+    "nonfaithful_quotient": 1,
+    "omissions": 12,
+    "wrong_coefficient": 1
+  },
+  "field_products": 16,
+  "field_rank_controls": 256,
+  "full_endpoint_basis_columns": 1856,
+  "full_endpoint_fixtures": 9,
+  "full_short_word_checks": 2971,
+  "group_products": 4096,
+  "involution_checks": 294,
+  "minimum_X_calls": 6,
+  "minimum_Y_calls": 6,
+  "no_new_kappa": true,
+  "rank_one_idempotents_r3": 28,
+  "rank_one_nilpotents_r3": 21,
+  "regular_short_columns": 5942,
+  "short_words_by_length": [
+    1,
+    54,
+    2916,
+    157464
+  ],
+  "short_words_with_nilpotents": 112446,
+  "source_sha256": {
+    "README.md": "e400314a9d198accd9b2fd0ac451ae97072355da303a752efcdaeecdf9f3899f",
+    "SOURCES.json": "b224f10fa51bc52a05996b39cfe67df331d325d6646ab2e475a378f18e4c91fd",
+    "TASK.json": "ec6de232bc3ddb340e78fccff6d8c085b3bb67c0d2e3319f2a3ac57c16643f3f",
+    "VERIFY.json": "e58bfefd239889a4bf9f72760e247691b84fdbc23e29a89972bee28c31cd25c4",
+    "verify.py": "c625d027ae41a05d0316b38905674445beb30667203a6764ce54cc9c59bc928f"
+  },
+  "triple_minimum": 12
+}
diff --git a/research/ut3-f4-nilpotent-tariff/SOURCES.json b/research/ut3-f4-nilpotent-tariff/SOURCES.json
new file mode 100644
index 0000000000..dc81950959
--- /dev/null
+++ b/research/ut3-f4-nilpotent-tariff/SOURCES.json
@@ -0,0 +1,42 @@
+{
+  "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/ut3-f4-w2-lift-obstruction/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "6c65514ce5e7921fa44827b517d0e4161e0c3597",
+      "sha256": "8fe6d98b4f4bca899ad7edb840dfcd4848359d66b2f1e02da45e92f20af24a8d"
+    },
+    {
+      "path": "research/ut3-f4-w2-lift-obstruction/README.md",
+      "usage": "provenance",
+      "git_blob": "dd34206ebdeb421774e4159055760a308158e188",
+      "sha256": "24f56fc1e3e3041e22c2ddb76b706b0c721c6b6b5e5734a09ef6b66767ab1b5f"
+    },
+    {
+      "path": "research/ut3-mixed-target-tariffs/README.md",
+      "usage": "provenance",
+      "git_blob": "1778bfdb77e3c02eaa628da3a85b32fd37939a9a",
+      "sha256": "7c27f4cb1f97f65778c6b9e7a0025fdfdcb7cd1f0cf6ab34c14ece7db1b88124"
+    },
+    {
+      "path": "research/ut3-two-targets-any-registers/README.md",
+      "usage": "provenance",
+      "git_blob": "3fc4f569a2e9bc81a1f61bc8343a276671a2d13f",
+      "sha256": "f879e3009b1fd5c625480ef92bdc454030ae62e7b378af7869e188df718e7399"
+    }
+  ]
+}
diff --git a/research/ut3-f4-nilpotent-tariff/TASK.json b/research/ut3-f4-nilpotent-tariff/TASK.json
new file mode 100644
index 0000000000..29021bccbe
--- /dev/null
+++ b/research/ut3-f4-nilpotent-tariff/TASK.json
@@ -0,0 +1,87 @@
+{
+  "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": "Remove scalar idempotence from the six-label UT3(F4) central triple: exact minimum 12 with every nonzero binary rank-one coupling and arbitrary restored dirty workspace. A characteristic-two extension-field quotient proves the general 4d central-target law.",
+  "scope_change_reason": "Take Wentao Li PR3788 Open next question 1 rather than invent a physical alphabet. This is a new coupling-alphabet obstruction, not a predecessor audit or supplier implementation.",
+  "bottleneck_link": "Closes nilpotent scalar couplings and extra dirty workspace as escape routes for this axis alphabet. A changed physically priced address operation is needed before this side result can affect the bit moment.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified nilpotent-coupling extension and package it. No larger search, further alphabet extension or supplier admission.",
+  "outcome": "completed",
+  "evidence": "README.md gives the all-size proof. RESULT.json is generated by verify.py and binds every package source. Exact F4 quotient, expanded-alphabet words, full formal endpoints, literal dirty basis columns and named failure controls corroborate the result.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one physically realizable additional address operation escape the axis-alphabet tariff with a favorable complete bill?",
+      "why_it_matters": "Nilpotent scalar couplings and extra dirty workspace cannot lower the present exact formal bill.",
+      "first_step": "Pin one literal supplier entry/call/exit contract and price frames, preparation, dirty restoration, hosting and precision for the changed address operation.",
+      "blocked_by": "No legal physical realization or recursive price is supplied by the formal alphabet."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133313",
+    "predecessor_pr": 3788,
+    "predecessor_head": "595b9426cc2fac34d31a71b24b98ed080f54c99a"
+  },
+  "overlap": {
+    "entry_open_prs": 365,
+    "entry_discussion_records": 3819,
+    "complete_remote_pagination": true,
+    "local_notes_searched": 80,
+    "head_note_inventory": 6319,
+    "additional_search": "All-main distinctive README terms and merged PR searches; touching F4 PR titles and bodies read. Unpublished work, arbitrary code and sparse local notes are not fully covered."
+  },
+  "implementation": {
+    "playbook": "investigation",
+    "principles": [
+      "Build the Lever",
+      "Prove It Works",
+      "Power of Ten"
+    ],
+    "runtime_allocation_deviation": "Managed Python allocations; at most five roles, 64 group elements, 32 witness calls and three enumerated calls from a fixed 54-factor alphabet.",
+    "diagnostics": "Warning-strict normal and optimized Python, AST syntax and function-length inspection. No configured static type checker."
+  }
+}
diff --git a/research/ut3-f4-nilpotent-tariff/VERIFY.json b/research/ut3-f4-nilpotent-tariff/VERIFY.json
new file mode 100644
index 0000000000..65567824b5
--- /dev/null
+++ b/research/ut3-f4-nilpotent-tariff/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": "Extension-field quotient, all 160435 expanded-alphabet short words, full formal and literal regular-action dirty endpoints, rank/involution controls and source-bound receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same mathematical and source-bound checks with Python assertions disabled."
+    }
+  ]
+}
diff --git a/research/ut3-f4-nilpotent-tariff/verify.py b/research/ut3-f4-nilpotent-tariff/verify.py
new file mode 100644
index 0000000000..b875a564bf
--- /dev/null
+++ b/research/ut3-f4-nilpotent-tariff/verify.py
@@ -0,0 +1,406 @@
+"""Exact finite corroboration of the extension-field UT3 rank proof.
+
+Produced by Nick Petalas. Apache-2.0.
+No predecessor implementation is imported. Normal execution is read-only.
+"""
+
+import hashlib
+import itertools
+import json
+from pathlib import Path
+import sys
+
+
+MUL = ((0, 0, 0, 0), (0, 1, 2, 3), (0, 2, 3, 1), (0, 3, 1, 2))
+INV = (0, 1, 3, 2)
+PACKAGE = Path(__file__).resolve().parent
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def group(a, b):
+    x, y, z = a % 4, (a // 4) % 4, a // 16
+    xx, yy, zz = b % 4, (b // 4) % 4, b // 16
+    return (x ^ xx) + 4 * (y ^ yy) + 16 * (z ^ zz ^ MUL[x][yy])
+
+
+def phi(a):
+    x, y, z = a % 4, (a // 4) % 4, a // 16
+    return (1, x, y, z, z ^ MUL[x][y])
+
+
+def algebra(a, b):
+    out = [0] * 5
+    for i in range(5):
+        out[i] = MUL[a[0]][b[i]] ^ MUL[a[i]][b[0]]
+    out[0] = MUL[a[0]][b[0]]
+    out[3] ^= MUL[a[1]][b[2]]
+    out[4] ^= MUL[a[2]][b[1]]
+    return tuple(out)
+
+
+def rank(matrix):
+    if not matrix:
+        return 0
+    a = [list(row) for row in matrix]
+    rows, cols, pivot = len(a), len(a[0]), 0
+    need(rows <= 10 and cols <= 10, 'rank domain exceeded')
+    need(all(len(row) == cols for row in a), 'ragged matrix')
+    for col in range(cols):
+        candidates = [j for j in range(pivot, rows) if a[j][col]]
+        if not candidates:
+            continue
+        j = candidates[0]
+        a[pivot], a[j] = a[j], a[pivot]
+        scale = INV[a[pivot][col]]
+        a[pivot] = [MUL[scale][v] for v in a[pivot]]
+        for j in range(rows):
+            if j != pivot and a[j][col]:
+                scale = a[j][col]
+                a[j] = [v ^ MUL[scale][w] for v, w in zip(a[j], a[pivot])]
+        pivot += 1
+        if pivot == rows:
+            break
+    return pivot
+
+
+def zero(r):
+    return tuple((0,) * r for _ in range(r))
+
+
+def add(a, b):
+    return tuple(tuple(x ^ y for x, y in zip(ar, br)) for ar, br in zip(a, b))
+
+
+def outer(u, v, coefficient, r):
+    return tuple(tuple(coefficient if (u >> i) & (v >> j) & 1 else 0
+                       for j in range(r)) for i in range(r))
+
+
+def right_rank_one(a, u, v, coefficient, r):
+    column = [0] * r
+    for i in range(r):
+        for j in range(r):
+            if (u >> j) & 1:
+                column[i] ^= a[i][j]
+    return tuple(tuple(MUL[column[i]][coefficient] if (v >> j) & 1 else 0
+                       for j in range(r)) for i in range(r))
+
+
+def validate(call, r):
+    kind, coefficient, u, v = call
+    need(1 <= r <= 5, 'role domain exceeded')
+    need(kind in (0, 1), 'non-axis label')
+    need(coefficient in (1, 2, 3), 'zero or invalid label coefficient')
+    need(0 < u < 2**r and 0 < v < 2**r, 'non-rank-one call')
+
+
+def quotient_step(state, call, r):
+    validate(call, r)
+    kind, coefficient, u, v = call
+    a, b, c, d = state
+    n = outer(u, v, coefficient, r)
+    if kind == 0:
+        return add(a, n), b, c, add(d, right_rank_one(b, u, v, coefficient, r))
+    return a, add(b, n), add(c, right_rank_one(a, u, v, coefficient, r)), d
+
+
+def check_floor(state, nx, ny):
+    a, b, c, d = state
+    ax = tuple(ar + cr for ar, cr in zip(a, c))
+    by = tuple(br + dr for br, dr in zip(b, d))
+    lower_x = rank(ax) + rank(a + d) - rank(a)
+    lower_y = rank(by) + rank(b + c) - rank(b)
+    need(nx >= lower_x and ny >= lower_y, 'extension-field span floor failed')
+
+
+def identity(r):
+    return tuple(tuple(1 if i == j else 0 for j in range(r)) for i in range(r))
+
+
+def formal_step(word, call, r):
+    validate(call, r)
+    kind, coefficient, u, v = call
+    g = coefficient * (1 if kind == 0 else 4)
+    result = [list(row) for row in word]
+    for i in range(r):
+        p = 0
+        for j in range(r):
+            if (u >> j) & 1:
+                p ^= word[i][j]
+        translated = 0
+        for h in range(64):
+            if (p >> h) & 1:
+                translated ^= 1 << group(h, g)
+        for j in range(r):
+            if (v >> j) & 1:
+                result[i][j] ^= p ^ translated
+    return tuple(tuple(row) for row in result)
+
+
+def formal_quotient(word, r):
+    out = [[[0] * r for _ in range(r)] for _ in range(5)]
+    for i in range(r):
+        for j in range(r):
+            for h in range(64):
+                if (word[i][j] >> h) & 1:
+                    for k, value in enumerate(phi(h)):
+                        out[k][i][j] ^= value
+    need(tuple(map(tuple, out[0])) == identity(r), 'augmentation changed')
+    return tuple(tuple(map(tuple, matrix)) for matrix in out[1:])
+
+
+def execute(calls, r):
+    need(len(calls) <= 32, 'word domain exceeded')
+    state, word = (zero(r),) * 4, identity(r)
+    nx = ny = 0
+    for call in calls:
+        state = quotient_step(state, call, r)
+        word = formal_step(word, call, r)
+        nx += call[0] == 0
+        ny += call[0] == 1
+    need(state == formal_quotient(word, r), 'formal/quotient disagreement')
+    check_floor(state, nx, ny)
+    return word, state
+
+
+def witness(parameters):
+    calls = []
+    for i, z in enumerate(parameters):
+        calls.extend(((0, z, 1 << i, 1 << i), (1, 1, 1 << i, 1 << i)) * 2)
+    return tuple(calls)
+
+
+def target(parameters, r):
+    return tuple(tuple((1 << (16 * parameters[i]) if i < len(parameters) else 1)
+                       if i == j else 0 for j in range(r)) for i in range(r))
+
+
+def field_and_homomorphism():
+    for a, b in itertools.product(range(4), repeat=2):
+        polynomial = (a if b & 1 else 0) ^ ((a << 1) if b & 2 else 0)
+        if polynomial & 4:
+            polynomial ^= 7
+        need(polynomial == MUL[a][b], 'field table differs from polynomial reduction')
+    for a, b in itertools.product(range(64), repeat=2):
+        need(phi(group(a, b)) == algebra(phi(a), phi(b)), 'quotient is not multiplicative')
+    return 16, 4096
+
+
+def rank_controls():
+    count = 0
+    for entries in itertools.product(range(4), repeat=4):
+        matrix = (entries[:2], entries[2:])
+        binary_rows = []
+        for i, bit in itertools.product(range(2), repeat=2):
+            row = 0
+            for j, input_bit in itertools.product(range(2), repeat=2):
+                output = MUL[matrix[i][j]][1 << input_bit]
+                row |= ((output >> bit) & 1) << (2 * j + input_bit)
+            binary_rows.append(row)
+        basis, binary_rank = [0] * 4, 0
+        for row in binary_rows:
+            for pivot in reversed(range(4)):
+                if (row >> pivot) & 1:
+                    if basis[pivot]:
+                        row ^= basis[pivot]
+                    else:
+                        basis[pivot] = row
+                        binary_rank += 1
+                        break
+        need(binary_rank == 2 * rank(matrix), 'field/binary rank disagreement')
+        count += 1
+    return count
+
+
+def short_words():
+    factors = tuple(itertools.product(range(2), range(1, 4), range(1, 4), range(1, 4)))
+    counts, formal_checks, nilpotent_words = [0] * 4, 0, 0
+    for length in range(4):
+        for calls in itertools.product(factors, repeat=length):
+            state = (zero(2),) * 4
+            for call in calls:
+                state = quotient_step(state, call, 2)
+            nx = sum(call[0] == 0 for call in calls)
+            check_floor(state, nx, length - nx)
+            if any((u & v).bit_count() % 2 == 0 for _, _, u, v in calls):
+                nilpotent_words += 1
+            if length <= 2:
+                word, full_state = execute(calls, 2)
+                need(full_state == state and word is not None, 'full replay failed')
+                for source in range(2):
+                    need(regular_column(calls, 2, source, 0)
+                         == tuple(row[source] for row in word),
+                         'literal short-word action differs from formal coefficients')
+                formal_checks += 1
+            counts[length] += 1
+    need(counts == [1, 54, 2916, 157464], 'short-word enumeration incomplete')
+    return counts, formal_checks, nilpotent_words
+
+
+def regular_column(calls, r, source, address):
+    """Apply the word to one dirty basis column without formal polynomials."""
+    values = [0] * r
+    values[source] = 1 << address
+    for kind, coefficient, u, v in reversed(calls):
+        p = 0
+        for j in range(r):
+            if (v >> j) & 1:
+                p ^= values[j]
+        shifted = 0
+        for h in range(64):
+            if (p >> h) & 1:
+                x, y, z = h % 4, (h // 4) % 4, h // 16
+                if kind == 0:
+                    new = (x ^ coefficient) + 4 * y + 16 * (z ^ MUL[coefficient][y])
+                else:
+                    new = x + 4 * (y ^ coefficient) + 16 * z
+                shifted ^= 1 << new
+        for i in range(r):
+            if (u >> i) & 1:
+                values[i] ^= p ^ shifted
+    return tuple(values)
+
+
+def check_regular_witness(parameters, r):
+    count = 0
+    for source, address in itertools.product(range(r), range(64)):
+        expected = [0] * r
+        z = parameters[source] if source < len(parameters) else 0
+        expected[source] = 1 << (address ^ (16 * z))
+        need(regular_column(witness(parameters), r, source, address) == tuple(expected),
+             'literal regular-action endpoint failed')
+        count += 1
+    return count
+
+
+def witnesses_and_involutions():
+    fixtures = basis_columns = 0
+    for w in range(1, 5):
+        parameters = tuple(1 + i % 3 for i in range(w))
+        for r in (w, w + 1):
+            word, state = execute(witness(parameters), r)
+            need(word == target(parameters, r), 'full dirty endpoint failed')
+            need(state[:2] == (zero(r), zero(r)), 'first-order endpoint is nonzero')
+            need(rank(state[2]) == rank(state[3]) == w, 'central rank differs')
+            fixtures += 1
+            basis_columns += check_regular_witness(parameters, r)
+    word, _ = execute(witness((1, 2, 3)), 5)
+    need(word == target((1, 2, 3), 5), 'two dirty spectators changed')
+    idempotents = nilpotents = 0
+    for u, v in itertools.product(range(1, 8), repeat=2):
+        if (u & v).bit_count() % 2:
+            idempotents += 1
+        else:
+            nilpotents += 1
+        for kind, coefficient in itertools.product(range(2), range(1, 4)):
+            call = (kind, coefficient, u, v)
+            need(execute((call, call), 3)[0] == identity(3), 'paid call not involutive')
+    basis_columns += check_regular_witness((1, 2, 3), 5)
+    return fixtures + 1, basis_columns, idempotents, nilpotents
+
+
+def controls():
+    parameters, r = (1, 2, 3), 4
+    calls, expected = witness(parameters), target(parameters, r)
+    omissions = 0
+    for i in range(len(calls)):
+        need(execute(calls[:i] + calls[i + 1:], r)[0] != expected, 'omission undetected')
+        omissions += 1
+    wrong = calls[:-1] + ((1, 2, 4, 4),)
+    need(execute(wrong, r)[0] != expected, 'wrong coefficient undetected')
+    dirty, _ = execute(calls + ((0, 1, 1, 8),), r)
+    need(all(dirty[i][:3] == expected[i][:3] for i in range(r)), 'clean trap is not clean')
+    need(dirty != expected, 'dirty restoration not checked')
+    # The degree-three augmentation product is nonzero formally, zero in Q.
+    kernel = 0
+    for choose in itertools.product(range(2), repeat=3):
+        h = 0
+        for selected, g in zip(choose, (1, 4, 1)):
+            if selected:
+                h = group(h, g)
+        kernel ^= 1 << h
+    need(kernel != 0, 'kernel control vanished formally')
+    trap = [list(row) for row in identity(2)]
+    trap[0][1] ^= kernel
+    need(formal_quotient(trap, 2) == (zero(2),) * 4, 'kernel not in quotient kernel')
+    need(tuple(map(tuple, trap)) != identity(2), 'quotient used as faithful certificate')
+    rejected = 0
+    for call in ((2, 1, 1, 1), (0, 0, 1, 1), (0, 1, 0, 1), (0, 1, 1, 16)):
+        try:
+            validate(call, r)
+        except ValueError:
+            rejected += 1
+    need(rejected == 4, 'illegal paid alphabet accepted')
+    noncentral = quotient_step((zero(1),) * 4, (0, 1, 1, 1), 1)
+    need(rank(noncentral[0]) == 1 and 2 * rank(noncentral[0]) > 1,
+         'zero-sum hypothesis control failed')
+    # Four rank-two calls would implement two central targets, below 4w.
+    parallel = ((0, 1, 1, 1), (0, 1, 2, 2),
+                (1, 1, 1, 1), (1, 1, 2, 2)) * 2
+    need(execute(parallel, 2)[0] == target((1, 1), 2) and rank(identity(2)) == 2,
+         'higher-rank exclusion control failed')
+    return {'omissions': omissions, 'wrong_coefficient': 1, 'dirty_restore': 1,
+            'nonfaithful_quotient': 1, 'invalid_calls': rejected,
+            'noncentral_first_order': 1, 'higher_rank_excluded': 1,
+            'kernel_support': kernel.bit_count()}
+
+
+def compute():
+    field_products, group_products = field_and_homomorphism()
+    words, formal_checks, nilpotent_words = short_words()
+    fixtures, columns, idempotents, nilpotents = witnesses_and_involutions()
+    result = {
+        'claim_type': 'scoped proof with finite corroboration',
+        'triple_minimum': 12, 'minimum_X_calls': 6, 'minimum_Y_calls': 6,
+        'field_products': field_products, 'group_products': group_products,
+        'field_rank_controls': rank_controls(),
+        'short_words_by_length': words, 'short_words_with_nilpotents': nilpotent_words,
+        'full_short_word_checks': formal_checks, 'regular_short_columns': 2 * formal_checks,
+        'full_endpoint_fixtures': fixtures,
+        'full_endpoint_basis_columns': columns, 'rank_one_idempotents_r3': idempotents,
+        'rank_one_nilpotents_r3': nilpotents, 'involution_checks': 6 * (idempotents + nilpotents),
+        'controls': controls(), 'no_new_kappa': True,
+    }
+    result['source_sha256'] = {
+        name: hashlib.sha256(read_small(PACKAGE / name)).hexdigest()
+        for name in ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py')
+    }
+    return result
+
+
+def read_small(path):
+    with path.open('rb') as source:
+        raw = source.read(65537)
+    need(len(raw) <= 65536, 'oversized package file')
+    return raw
+
+
+def unique_object(pairs):
+    result = {}
+    for key, value in pairs:
+        need(key not in result, 'duplicate JSON key')
+        result[key] = value
+    return result
+
+
+def main():
+    need(sys.argv[1:] in ([], ['--emit']), 'usage: verify.py [--emit]')
+    actual = compute()
+    if sys.argv[1:] == ['--emit']:
+        print(json.dumps(actual, indent=2, sort_keys=True))
+        return
+    raw = read_small(PACKAGE / 'RESULT.json')
+    expected = json.loads(raw, object_pairs_hook=unique_object)
+    need(json.dumps(actual, sort_keys=True) == json.dumps(expected, sort_keys=True),
+         'receipt or authenticated source mismatch')
+    print('PASS_UT3_F4_NILPOTENT_TARIFF minimum=12 nX=6 nY=6 '
+          f'short_words={sum(actual["short_words_by_length"])} '
+          f'involutions={actual["involution_checks"]} no_new_kappa')
+
+
+if __name__ == '__main__':
+    main()