diff --git a/research/unsigned-connector-residue-count/PROOF.md b/research/unsigned-connector-residue-count/PROOF.md
new file mode 100644
index 0000000000..c5126d4578
--- /dev/null
+++ b/research/unsigned-connector-residue-count/PROOF.md
@@ -0,0 +1,181 @@
+# Exact counts of optimal unsigned one-source words
+
+## Model and statement
+
+Let R be a nonzero unital ring of exact finite characteristic m >= 2. Let
+X, Z and Y be left R-modules, and let B: X -> Z and A: Z -> Y be arbitrary
+compatible R-linear maps. The three distinct data roles x, z and y may be
+arbitrarily dirty. The only paid calls are
+
+```text
+B: z += Bx
+A: y += Az
+```
+
+Calls are complete, source-preserving additive implementations, with their own
+private state restored and their heads returned. Every call includes its full
+implementation price. No inverse, sign change, scalar multiplier, frame change,
+copy, direct AB call, source mutation, or additional connector is free. The
+word is independent of input contents, and y is observed only after completion.
+Correctness is universal in the maps and modules. Additional relations in a
+particular choice of maps can permit shorter specialized words.
+
+For c in {1,...,m-1}, the target is y += c ABx with x and z unchanged. The
+minimum length is 2m. Write N_m(c) for the number of distinct literal words
+attaining this minimum. Define N_m(0) as an auxiliary count over **balanced**
+words with exactly m A events and m B events. It is not the optimum-word
+count for the zero target, whose optimum is the empty word.
+
+Let mu be the Mobius function and define the integer Ramanujan sum
+
+```text
+R_d(c) = sum_{e | gcd(d,c)} e mu(d/e).
+```
+
+Then, for every m >= 2 and every 0 <= c < m,
+
+```text
+N_m(c) = (1/m) sum_{d | m} R_d(c) binom(2m/d, m/d).                 (1)
+```
+
+For nonzero c this is the complete optimal-word count. The complete number of
+restored length-2m words for the zero target is N_m(0)+2, adding A^(2m) and
+B^(2m). The number for each other target is unchanged.
+
+If p is prime, (1) reduces to
+
+```text
+N_p(0) = [binom(2p,p) + 2(p-1)]/p,
+N_p(c) = [binom(2p,p) - 2]/p,             1 <= c < p.              (2)
+```
+
+The nonzero target coefficients have equal optimal-word counts **if and only
+if m is prime**. For any m, N_m(c) depends only on gcd(m,c); in particular all
+unit coefficients have the same count. Reversing a word changes c to -c and
+gives an unsigned inverse of the same length.
+
+This is a scoped proof in the complete-call interface. The finite verifier is
+corroboration of the proof, not its all-characteristic justification.
+
+## 1. Dirty-state reduction and optimal length
+
+For a word w, let a and b be its A and B counts. Let I(w) be the number of
+ordered event pairs in which B occurs before A. Straight-line substitution
+gives the exact action
+
+```text
+x_final = x,
+z_final = z + b Bx,
+y_final = y + a Az + I(w) ABx.
+```
+
+No commutation of A and B is used. Their order is AB because B writes z and
+A reads z. Universal correctness forces b = 0 mod m to restore z and a = 0
+mod m to cancel arbitrary connector dirt. To see necessity, take X=Y=Z=R,
+use identity maps, and vary x and z independently. Exact characteristic m
+means k*1_R=0 exactly when m divides k.
+
+For nonzero c, both operators must occur. Thus a,b >= m and the total length
+is at least 2m. The literal word
+
+```text
+B^c A B^(m-c) A^(m-1)
+```
+
+has a=b=m and I(w)=c mod m. It attains the bound. Every length-2m word for
+nonzero c must therefore have a=b=m, and it realizes c exactly when I(w)=c
+mod m. This also gives the minimum fixed-price bill m(c_A+c_B) for any positive
+complete-call prices c_A,c_B. The count theorem, rather than this elementary
+minimum-length extension of the F3 argument, is the contribution here.
+
+For a balanced word, reversing the event order exchanges before and after in
+all m^2 B/A pairs. Hence I(reverse(w))=m^2-I(w)=-I(w) mod m. This proves the
+inverse statement without granting a free signed call.
+
+## 2. The coefficient is a subset-position statistic
+
+Choose the m positions of A in {0,...,2m-1}, written s_1<...<s_m. Before the
+jth A, there are s_j earlier events and j-1 of them are A. Consequently
+
+```text
+I(w) = sum_j [s_j-(j-1)] = sum_j s_j - m(m-1)/2.                  (3)
+```
+
+Each m-element position subset determines exactly one balanced word. In
+particular sum_c N_m(c)=binom(2m,m). The shift in (3) cannot be dropped in
+even characteristic.
+
+## 3. Exact root-of-unity transform
+
+Fix a divisor d of m, and a primitive complex dth root zeta. Complex roots
+are only a finite counting device; they impose no assumption on R. By (3),
+with t=m(m-1)/2,
+
+```text
+sum_w zeta^I(w)
+  = zeta^(-t) [u^m] product_{s=0}^{2m-1} (1 + u zeta^s)
+  = zeta^(-t) [u^m] [1-(-u)^d]^(2m/d)
+  = zeta^(-t) (-1)^((d+1)m/d) binom(2m/d,m/d).                  (4)
+```
+
+The product identity follows because each dth root occurs 2m/d times and
+product_{s=0}^{d-1}(1+u zeta^s)=1-(-u)^d.
+
+The phase and sign in (4) cancel. If d is odd, d divides t because d divides
+m and 2 is invertible modulo d. Thus zeta^(-t)=1, and d+1 is even. If d is
+even, m is even, zeta^(d/2)=-1 and
+
+```text
+zeta^(-t) = (-1)^((m/d)(m-1)) = (-1)^(m/d).
+```
+
+Since d+1 is odd, the other sign is also (-1)^(m/d). Therefore
+
+```text
+sum_w zeta^I(w) = binom(2m/d,m/d).                              (5)
+```
+
+This includes d=1, which gives the total number of balanced words.
+
+## 4. Fourier inversion gives the divisor formula
+
+Let omega be a primitive mth root. The elementary finite geometric sum gives
+
+```text
+1_{I=c mod m} = (1/m) sum_{k=0}^{m-1} omega^(k(I-c)).
+```
+
+Sum over balanced words and use (5). Group k by the exact order d of omega^k.
+The resulting sum of primitive dth roots to the power -c is R_d(c).
+For completeness its integer form follows from inclusion-exclusion. If
+
+```text
+S_d(c) = sum_{zeta primitive of order d} zeta^(-c),
+```
+
+then sum_{e|d} S_e(c) is the sum of all dth roots to the power -c. This is d
+if d divides c and zero otherwise. Mobius inversion yields
+
+```text
+S_d(c) = sum_{e|d} mu(d/e) e 1_{e|c}
+       = sum_{e|gcd(d,c)} e mu(d/e) = R_d(c).
+```
+
+This proves (1). No census or numerical complex arithmetic is needed.
+
+## 5. Exactly the primes have uniform nonzero counts
+
+When m=p is prime, its divisors are 1,p. R_p(0)=p-1 and R_p(c)=-1 for
+nonzero c, while binom(2,1)=2. This proves (2).
+
+Conversely suppose all N_m(c) for c!=0 were a common value b. Their Fourier
+transform at any nontrivial mth root would then be N_m(0)-b, because the sum
+of the nontrivial powers of that root over the residues is -1. It would be
+independent of the root's order. If m is composite, choose a proper prime
+divisor p of m. Equation (5) at order m gives 2; at order p it gives
+binom(2m/p,m/p)>2 since m/p>=2. Both roots are nontrivial, a contradiction.
+Thus uniformity holds exactly for prime m.
+
+Finally gcd(m,c) determines gcd(d,c) for every divisor d of m, so (1) proves
+the asserted gcd dependence. This gives N_m(c)=N_m(-c) as also witnessed by
+word reversal.
diff --git a/research/unsigned-connector-residue-count/README.md b/research/unsigned-connector-residue-count/README.md
new file mode 100644
index 0000000000..f221f46b41
--- /dev/null
+++ b/research/unsigned-connector-residue-count/README.md
@@ -0,0 +1,114 @@
+# Exact counts of shortest unsigned connector words
+
+This scoped proof gives a closed formula for the number of optimal schedules
+at a one-source dirty-connector boundary, over every finite characteristic.
+It also proves that the nonzero coefficient counts are equal exactly in prime
+characteristic. The contribution was produced by Nick Petalas.
+
+Let the only complete calls be `B: z += Bx` and `A: y += Az`, with arbitrary
+dirty data, immutable source x and generic compatible linear maps over a
+nonzero unital ring of exact characteristic m. For a nonzero integer residue
+c modulo m, require `y += c ABx`, with x and z unchanged.
+
+Every optimal word has m calls of each operator, hence length 2m. The new
+result counts these words, rather than improving this elementary call floor:
+
+```text
+N_m(c) = (1/m) sum_{d | m} R_d(c) binom(2m/d, m/d),
+R_d(c) = sum_{e | gcd(d,c)} e mu(d/e).
+```
+
+Here mu is the Mobius function and R is the integer Ramanujan sum. In prime
+characteristic p every nonzero c has `(binom(2p,p)-2)/p` optimal words. Composite
+characteristics have unequal nonzero counts. For example, the counts for c=1,2,3
+at m=4 are 16,18,16. All residues with the same gcd(m,c) have equal counts.
+Reversing any balanced word gives its same-length unsigned inverse.
+
+[PROOF.md](PROOF.md) gives the complete all-characteristic proof from the
+dirty-state action, a subset-position statistic and exact finite Fourier
+inversion. It uses no finite census as a universal premise. N_m(0) is an
+auxiliary **balanced-word** count; the zero target has empty optimal word.
+The full zero-target length-2m count adds the two pure words to N_m(0).
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/unsigned-connector-residue-count/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unsigned-connector-residue-count
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unsigned-connector-residue-count --check-source-history
+```
+
+Any CPython 3.12 path can replace the local interpreter path. The verifier prints
+a generated JSON receipt with every package/input SHA256, followed by
+`PASS_UNSIGNED_CONNECTOR_RESIDUE_COUNT moduli=31 residues=527`. It writes no
+files. Both ordinary and optimized Python commands are registered.
+
+The exact finite checks cover:
+
+- All 527 residue counts at m=2,...,32, comparing the formula with a separate
+  chronological dynamic program.
+- All 250,950 balanced position subsets at m=2,...,10, plus literal dirty
+  coefficient execution of all 17,574 balanced words at m=2,...,8.
+- All 21,840 unrestricted length-2m words at m=2,...,7, finding 4,716 restored
+  words. This includes the two pure zero-target words in each characteristic.
+- 496 explicit nonzero-coefficient witnesses, 3,968 noncommuting two-coordinate
+  dirty-input cases and 3,968 inverse roundtrips, through m=32.
+- Eight controls for a missing position shift, a prime-only formula misused in
+  composite characteristic, omitted source/readout cancellation, the wrong
+  target coefficient, reversed AB order, a clean-only shortcut, and invalid
+  executable-domain inputs.
+
+The finite program restricts m to 2 through 32. The largest dynamic-programming
+table has 34,848 integer slots. Subset enumeration visits at most binom(20,10)
+objects per characteristic; literal words have at most 64 events. Functions
+have no recursion, all scientific contracts use explicit exceptions, and
+`-W error` diagnostics run in both registered modes. Python allocates dynamic
+objects within those fixed finite bounds; fixed-memory execution is not claimed.
+
+The card's first working control prints
+`PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings=945 max_coverage=31 queries=74 leaves=182`.
+The selected binding baseline also passes. These are orientation checks, not
+part of the new counting proof or a cold replay of the selected construction.
+
+## Attribution and scope
+
+Ross Richardson's [#943/#934 lineage](../universal-connector-boundary/README.md)
+supplies the complete-call dirty-connector interface and prefix viewpoint.
+Riquelme Soares's [#4189](https://github.com/CrocSwap/integer-mult-bounds/pull/4189),
+head `5fb3936dfc8082f438f21c72dd6ca49ff4366ae7`, supplies the unsigned F3
+one-source problem, the mod-three count floor and its six optimal words.
+Equation (2) of the new proof recovers that six-word count as its p=3 case.
+The general count uses classical subset generating functions, finite Fourier
+inversion and Ramanujan sums; no novelty is claimed for those tools themselves.
+Concurrent [#4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231),
+head `8a956cbc80dc55697fd3e214812ce567b5eca48f`, classifies the unsigned five-source
+optimum by characteristic and also gives the one-source 2m call floor. That
+floor is shared context; the new result here is its complete word-count law.
+No pending executable or archived source is imported.
+
+The `connector-alphabet-change` card is explicitly changed to this scheduling
+side question. The characteristic-two coefficient premise changes; the
+operations stay unsigned. This does not add a new connector operation or find
+a selected-supplier saving. The neighboring five-source and signed-ring tasks
+remain separate. Exact base and input pins are in [SOURCES.json](SOURCES.json).
+
+All calls must include their complete implementation prices. Admission,
+coefficient preparation, instruction storage, dispatch and word-dependent
+physical routing remain additional. No concrete supplier caller, native/tape
+implementation, precision analysis, outer multiplication theorem, formal-kernel
+proof or new kappa is supplied. Independent human and formal proof-kernel review
+are unclaimed. Apache-2.0.
+
+## Open next questions
+
+The structured questions in [TASK.json](TASK.json) give first steps and blockers.
+
+1. Can these marginal coefficient spectra constrain simultaneous demands in a
+   multi-source unsigned connector? A joint readout-position argument is needed;
+   multiplying independent marginal counts would discard their correlations.
+2. Can a concrete recursive caller choose among its minimum-length words to
+   reduce fully charged routing? Start with one pinned caller and compare two
+   schedules including all accesses and head returns. This package supplies no
+   physical price for that choice.
diff --git a/research/unsigned-connector-residue-count/SOURCES.json b/research/unsigned-connector-residue-count/SOURCES.json
new file mode 100644
index 0000000000..8df80116ba
--- /dev/null
+++ b/research/unsigned-connector-residue-count/SOURCES.json
@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/universal-connector-boundary/README.md",
+      "usage": "input",
+      "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f",
+      "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476"
+    }
+  ],
+  "context_only": [
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4189",
+      "head_commit": "5fb3936dfc8082f438f21c72dd6ca49ff4366ae7",
+      "credit": "Riquelme Soares",
+      "role": "Unsigned F3 one-source problem and six optimal words; no executable dependency."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4231",
+      "head_commit": "8a956cbc80dc55697fd3e214812ce567b5eca48f",
+      "credit": "Nick Petalas",
+      "role": "Concurrent five-source characteristic classification and shared one-source 2m call floor; no executable dependency."
+    }
+  ]
+}
diff --git a/research/unsigned-connector-residue-count/TASK.json b/research/unsigned-connector-residue-count/TASK.json
new file mode 100644
index 0000000000..4f99cb0054
--- /dev/null
+++ b/research/unsigned-connector-residue-count/TASK.json
@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the complete shortest-word coefficient multiplicity distribution for the unsigned one-source dirty connector over every finite characteristic, with a divisor-sum formula and prime/composite equidistribution criterion.",
+  "scope_change_reason": "The live handoffs assign five-source and signed-ring characteristic optima elsewhere. This self-contained side result changes the binary coefficient assumption and answers a different exact question: how many optimal schedules realize each coefficient. It does not extend a source-count census or claim a supplier improvement.",
+  "bottleneck_link": "The law identifies the exact scheduling freedom at a dirty recursive boundary, including the failure of prime-field coefficient uniformity in composite characteristic. No selected consumer is supplied, so this is a scheduling side result, not a paid-profile or kappa gain.",
+  "budget_minutes": 60,
+  "stop_rule": "Finish one uniform counting proof, bounded exact enumerations, dirty noncommuting replay and source-bound publication checks; no larger supplier construction or search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-characteristic divisor formula and prime/composite criterion. verify.py compares exact DP and position-subset enumerations, literal dirty coefficient words, complete length classes and noncommuting dense replay, with refusal controls and a generated source-hash receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the one-source coefficient spectra constrain the joint coefficient demands of a multi-source unsigned connector?",
+      "why_it_matters": "One-source uniformity fails in composite characteristic. A usable simultaneous obstruction could prune multi-source schedules without assuming independent choices.",
+      "first_step": "Project one pinned multi-source source path onto each source and compare the attainable joint readout coefficient tuples with the marginal spectra. Retain boundary correlations.",
+      "blocked_by": "Marginal counts alone do not enforce simultaneous readout positions; this package proves no multi-source obstruction."
+    },
+    {
+      "question": "Can a concrete recursive caller exploit distinct minimum-length schedules to reduce physical routing while preserving the full call bill?",
+      "why_it_matters": "All counted words have the same operator bill, but physical access, dispatch and restoration can depend on their order.",
+      "first_step": "Extract one actual one-source caller with exact characteristic, immutable source, unobserved target and dirty connector, then price two distinct optimal words including all head returns.",
+      "blocked_by": "No selected-supplier caller or word-dependent physical tariff is bound here."
+    }
+  ]
+}
diff --git a/research/unsigned-connector-residue-count/VERIFY.json b/research/unsigned-connector-residue-count/VERIFY.json
new file mode 100644
index 0000000000..7fb05efdd8
--- /dev/null
+++ b/research/unsigned-connector-residue-count/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/universal-connector-boundary/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Divisor formula for all 527 residues at characteristics 2 through 32; independent exact DP, 250950 subset words, 17574 literal balanced words, 21840 complete length words, 496 witnesses, 3968 dirty dense inputs and inverse roundtrips, eight controls, source hashes."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same scientific checks with Python assertions disabled; all contracts use explicit exceptions."
+    }
+  ]
+}
diff --git a/research/unsigned-connector-residue-count/counts.py b/research/unsigned-connector-residue-count/counts.py
new file mode 100644
index 0000000000..b581977386
--- /dev/null
+++ b/research/unsigned-connector-residue-count/counts.py
@@ -0,0 +1,106 @@
+"""Exact finite corroboration of the all-characteristic counting theorem.
+
+The theorem has no upper characteristic limit. Executable checks deliberately
+accept only 2 <= m <= 32, bounding every loop and the dynamic-programming table.
+"""
+
+from math import comb, gcd
+
+MAX_MODULUS = 32
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise ValueError(message)
+
+
+def check_modulus(modulus: int) -> None:
+    require(type(modulus) is int and 2 <= modulus <= MAX_MODULUS,
+            "characteristic must be an integer between 2 and 32")
+
+
+def divisors(number: int) -> tuple[int, ...]:
+    require(type(number) is int and 1 <= number <= MAX_MODULUS,
+            "divisor input outside finite verification domain")
+    return tuple(d for d in range(1, number + 1) if number % d == 0)
+
+
+def mobius(number: int) -> int:
+    require(type(number) is int and 1 <= number <= MAX_MODULUS,
+            "Mobius input outside finite verification domain")
+    remaining, sign = number, 1
+    for prime in range(2, number + 1):
+        if remaining % prime == 0:
+            remaining //= prime
+            sign = -sign
+            if remaining % prime == 0:
+                return 0
+    require(remaining == 1, "factorization did not finish")
+    return sign
+
+
+def ramanujan(order: int, coefficient: int) -> int:
+    require(type(order) is int and 1 <= order <= MAX_MODULUS,
+            "root order outside finite verification domain")
+    require(type(coefficient) is int and 0 <= coefficient < MAX_MODULUS,
+            "coefficient outside finite verification domain")
+    return sum(e * mobius(order // e) for e in divisors(gcd(order, coefficient)))
+
+
+def formula_counts(modulus: int) -> tuple[int, ...]:
+    check_modulus(modulus)
+    counts = []
+    for coefficient in range(modulus):
+        numerator = sum(ramanujan(d, coefficient) * comb(2 * modulus // d, modulus // d)
+                        for d in divisors(modulus))
+        require(numerator >= 0 and numerator % modulus == 0,
+                "divisor formula did not produce a nonnegative integer")
+        counts.append(numerator // modulus)
+    require(sum(counts) == comb(2 * modulus, modulus), "formula mass mismatch")
+    return tuple(counts)
+
+
+def chronological_counts(modulus: int) -> tuple[int, ...]:
+    """Append actual A/B events, retaining source count and AB coefficient."""
+    check_modulus(modulus)
+    table = [[[0] * modulus for _ in range(modulus + 1)]
+             for _ in range(modulus + 1)]
+    table[0][0][0] = 1
+    for sources in range(modulus + 1):
+        for readouts in range(modulus + 1):
+            for residue in range(modulus):
+                count = table[sources][readouts][residue]
+                if sources < modulus:
+                    table[sources + 1][readouts][residue] += count
+                if readouts < modulus:
+                    new_residue = (residue + sources) % modulus
+                    table[sources][readouts + 1][new_residue] += count
+    result = tuple(table[modulus][modulus])
+    require(sum(result) == comb(2 * modulus, modulus), "chronological mass mismatch")
+    return result
+
+
+def signature(word: str, modulus: int) -> tuple[int, int, int]:
+    """Return Bx in z, Az_initial in y, and ABx in y, modulo m."""
+    check_modulus(modulus)
+    require(type(word) is str and len(word) <= 2 * MAX_MODULUS,
+            "word exceeds the finite replay bound")
+    source, dirt, product = 0, 0, 0
+    for event in word:
+        require(event in "AB", "unknown connector event")
+        if event == "B":
+            source = (source + 1) % modulus
+        else:
+            dirt = (dirt + 1) % modulus
+            product = (product + source) % modulus
+    return source, dirt, product
+
+
+def witness(modulus: int, coefficient: int) -> str:
+    check_modulus(modulus)
+    require(type(coefficient) is int and 0 < coefficient < modulus,
+            "nonzero coefficient required")
+    word = "B" * coefficient + "A" + "B" * (modulus - coefficient)
+    word += "A" * (modulus - 1)
+    require(signature(word, modulus) == (0, 0, coefficient), "witness action mismatch")
+    return word
diff --git a/research/unsigned-connector-residue-count/verify.py b/research/unsigned-connector-residue-count/verify.py
new file mode 100644
index 0000000000..6ab6c644b8
--- /dev/null
+++ b/research/unsigned-connector-residue-count/verify.py
@@ -0,0 +1,201 @@
+#!/usr/bin/env python3
+"""Replay the closed counting law; print a source-bound receipt without writes."""
+
+import hashlib
+import itertools
+import json
+from math import comb
+from pathlib import Path
+
+from counts import (MAX_MODULUS, chronological_counts, formula_counts, require,
+                    signature, witness)
+
+PACKAGE = Path(__file__).resolve().parent
+ENUMERATION_MAX = 10
+
+
+def subset_counts(modulus: int, centered: bool = True) -> tuple[int, ...]:
+    """Choose readout positions, independently of chronological DP states."""
+    require(2 <= modulus <= ENUMERATION_MAX, "subset enumeration out of range")
+    counts = [0] * modulus
+    offset = modulus * (modulus - 1) // 2 if centered else 0
+    for positions in itertools.combinations(range(2 * modulus), modulus):
+        counts[(sum(positions) - offset) % modulus] += 1
+    require(sum(counts) == comb(2 * modulus, modulus), "subset mass mismatch")
+    return tuple(counts)
+
+
+def exact_count_checks() -> dict:
+    spectra = {}
+    enumerated = 0
+    residues = 0
+    for modulus in range(2, MAX_MODULUS + 1):
+        counts = formula_counts(modulus)
+        require(counts == chronological_counts(modulus), "formula/DP disagreement")
+        prime = all(modulus % d != 0 for d in range(2, modulus))
+        require((len(set(counts[1:])) == 1) == prime,
+                "nonzero equidistribution/primality disagreement")
+        require(all(counts[c] == counts[-c] for c in range(modulus)),
+                "reverse-word symmetry failed")
+        if modulus <= ENUMERATION_MAX:
+            require(counts == subset_counts(modulus), "formula/subset disagreement")
+            enumerated += comb(2 * modulus, modulus)
+        residues += modulus
+        spectra[str(modulus)] = counts
+    require(spectra["3"] == (8, 6, 6), "F3 specialization changed")
+    require(spectra["4"] == (20, 16, 18, 16), "composite specialization changed")
+    return {"spectra": spectra, "residues": residues,
+            "enumerated_words": enumerated}
+
+
+def positional_action_checks() -> int:
+    """Run every small word through the generic dirty coefficient action."""
+    checked = 0
+    for modulus in range(2, 9):
+        counts = [0] * modulus
+        for positions in itertools.combinations(range(2 * modulus), modulus):
+            selected = frozenset(positions)
+            word = "".join("A" if i in selected else "B"
+                           for i in range(2 * modulus))
+            source, dirt, product = signature(word, modulus)
+            require(source == dirt == 0, "unrestored balanced word")
+            counts[product] += 1
+            checked += 1
+        require(tuple(counts) == formula_counts(modulus), "word action count mismatch")
+    return checked
+
+
+def complete_length_checks() -> dict:
+    """Include the two pure words in the zero-target, length-2m class."""
+    checked, restored = 0, 0
+    for modulus in range(2, 8):
+        counts = [0] * modulus
+        for events in itertools.product("AB", repeat=2 * modulus):
+            source, dirt, product = signature("".join(events), modulus)
+            if source == dirt == 0:
+                counts[product] += 1
+                restored += 1
+            checked += 1
+        expected = list(formula_counts(modulus))
+        expected[0] += 2
+        require(counts == expected, "full restored word count mismatch")
+    return {"words": checked, "restored_words": restored}
+
+
+def matvec(matrix: tuple, vector: tuple, modulus: int) -> tuple:
+    require(len(matrix) == len(vector) == 2 and all(len(r) == 2 for r in matrix),
+            "dense replay expects two coordinates")
+    return tuple(sum(matrix[i][j] * vector[j] for j in range(2)) % modulus
+                 for i in range(2))
+
+
+def add(left: tuple, right: tuple, modulus: int) -> tuple:
+    return tuple((left[i] + right[i]) % modulus for i in range(2))
+
+
+def dense_replay(word: str, modulus: int, a: tuple, b: tuple,
+                 x: tuple, y: tuple, z: tuple) -> tuple:
+    require(2 <= modulus <= MAX_MODULUS and len(word) <= 2 * MAX_MODULUS,
+            "dense replay bound exceeded")
+    for event in word:
+        require(event in "AB", "unknown dense event")
+        if event == "B":
+            z = add(z, matvec(b, x, modulus), modulus)
+        else:
+            y = add(y, matvec(a, z, modulus), modulus)
+    return x, y, z
+
+
+def dense_checks() -> dict:
+    """Literal noncommuting maps; coordinate bases plus arbitrary dirty inputs."""
+    a, b = ((0, 1), (1, 1)), ((1, 1), (0, 1))
+    checked, roundtrips, witnesses = 0, 0, 0
+    for modulus in range(2, MAX_MODULUS + 1):
+        for coefficient in range(1, modulus):
+            word = witness(modulus, coefficient)
+            require(signature(word[::-1], modulus) == (0, 0, -coefficient % modulus),
+                    "reverse word is not the inverse")
+            witnesses += 1
+            for index in range(8):
+                values = [int(i == index) for i in range(6)]
+                if index >= 6:
+                    values = [(i * (index + 1) + index) % modulus for i in range(6)]
+                x, y, z = tuple(values[:2]), tuple(values[2:4]), tuple(values[4:])
+                abx = matvec(a, matvec(b, x, modulus), modulus)
+                target = add(y, tuple(coefficient * v for v in abx), modulus)
+                result = dense_replay(word, modulus, a, b, x, y, z)
+                require(result == (x, target, z), "dense dirty endpoint failed")
+                back = dense_replay(word[::-1], modulus, a, b, *result)
+                require(back == (x, y, z), "dense inverse failed")
+                checked += 1
+                roundtrips += 1
+    return {"witnesses": witnesses, "dense_inputs": checked, "roundtrips": roundtrips}
+
+
+def reject_controls() -> list[str]:
+    controls = []
+    require(subset_counts(2, centered=False) != formula_counts(2),
+            "missing positional shift was undetected")
+    controls.append("missing subset-position shift")
+    fake_prime = ((comb(8, 4) + 2 * 3) // 4,) + ((comb(8, 4) - 2) // 4,) * 3
+    require(fake_prime != formula_counts(4), "composite treated as prime")
+    controls.append("prime formula used at composite characteristic")
+    word = witness(4, 1)
+    for mutant, label in ((word.replace("B", "", 1), "omitted source restoration"),
+                          (word[:-1], "omitted dirty readout cancellation"),
+                          (witness(4, 2), "wrong product coefficient")):
+        require(signature(mutant, 4) != (0, 0, 1), f"undetected fault: {label}")
+        controls.append(label)
+    a, b = ((0, 1), (0, 0)), ((0, 0), (1, 0))
+    x, zero = (1, 0), (0, 0)
+    actual = dense_replay(word, 4, a, b, x, zero, zero)[1]
+    require(actual != matvec(b, matvec(a, x, 4), 4), "AB/BA swap undetected")
+    controls.append("noncommuting factor order reversed")
+    require(signature("BABBB", 4)[1] != 0, "clean-only shortcut accepted")
+    controls.append("one readout leaves arbitrary connector dirt")
+    for invalid in (1, 33, True, 2.0):
+        try:
+            formula_counts(invalid)
+        except ValueError:
+            continue
+        raise ValueError("invalid characteristic accepted")
+    controls.append("finite verifier domain enforced")
+    return controls
+
+
+def source_hashes() -> dict:
+    sources = json.loads((PACKAGE / "SOURCES.json").read_text())
+    require(len(sources["files"]) <= 8, "source list exceeds finite bound")
+    result = {}
+    for row in sources["files"]:
+        if row["usage"] == "input":
+            path = PACKAGE.parent.parent / row["path"]
+            require(path.stat().st_size <= 1_048_576, "input exceeds byte bound")
+            actual = hashlib.sha256(path.read_bytes()).hexdigest()
+            require(actual == row["sha256"], f"input hash mismatch: {row['path']}")
+            result[row["path"]] = actual
+    files = sorted(PACKAGE.iterdir())
+    require(len(files) <= 12, "unexpected package file count")
+    for path in files:
+        require(path.is_file() and not path.is_symlink(), "unexpected package entry")
+        require(path.stat().st_size <= 1_048_576, "package file exceeds byte bound")
+        result[f"package/{path.name}"] = hashlib.sha256(path.read_bytes()).hexdigest()
+    return result
+
+
+def main() -> None:
+    counts = exact_count_checks()
+    receipt = {"claim_type": "scoped proof with finite corroboration",
+               "counting": counts, "literal_words": positional_action_checks(),
+               "complete_length": complete_length_checks(),
+               "dense": dense_checks(), "controls": reject_controls(),
+               "sha256": source_hashes()}
+    encoded = json.dumps(receipt, sort_keys=True, separators=(",", ":"))
+    digest = hashlib.sha256(encoded.encode()).hexdigest()
+    print(encoded)
+    print(f"PASS_UNSIGNED_CONNECTOR_RESIDUE_COUNT moduli=31 "
+          f"residues={counts['residues']} receipt_sha256={digest}")
+
+
+if __name__ == "__main__":
+    main()