diff --git a/research/single-counter-aggregate-padding/PROOF.md b/research/single-counter-aggregate-padding/PROOF.md
new file mode 100644
index 0000000000..6d39f6ffef
--- /dev/null
+++ b/research/single-counter-aggregate-padding/PROOF.md
@@ -0,0 +1,183 @@
+# One counter for two coordinate phases
+
+Scoped constructive proof, produced by Nick Petalas. Apache-2.0.
+
+## Contract
+
+There are exactly five positive coordinate cardinalities q_i. Their immutable
+canonical descriptors store q_i-1, least significant bit first, between `^` and
+`$`. A singleton has an empty descriptor. Write
+
+```text
+L_i = bit_length(q_i-1), R_i = 2^L_i,
+D = sum_i L_i, N = product_i R_i, M = product_i q_i.
+```
+
+Each coordinate has one separate work tape with L_i owned zero bits between
+markers. All descriptor/work heads start at their first bit, or at `$` when
+empty. There is a separate immutable input tape and a fresh owned output tape.
+Their heads also start at the first data position. The input is the M-bit
+genuine rectangle for padding, or an arbitrary N-bit padded rectangle for
+restriction. The output has adequate owned space. Origins may differ by any
+integer. Cells outside the delimited/owned intervals are protected.
+
+The alphabet is `{0,1,^,$,_}`. Operations read one symbol, write one symbol or
+move one head by one cell. Finite-control state stores the five phase bits and
+fixed program state. The metered reference also charges one `emit` action per
+row and one `advance` action per visited coordinate. Testing five flags is one
+fixed finite-control transition, independent of widths. There is no decoded
+cardinality, width, coordinate, address, or unit-cost arithmetic in the machine.
+
+On successful return the output is lexicographic zero padding, or restriction
+to the genuine subrectangle. Input and descriptors retain every byte, all
+twelve heads return, and all D counter bits are zero. Output is retained.
+This is a well-formed successful-entry contract, not an adversarial parser or
+failure-restoration theorem.
+
+## Coordinate construction
+
+Suppress the coordinate subscript. The unchanged descriptor is the L-bit word
+for q-1. Its bitwise complement is exactly
+
+```text
+(2^L-1)-(q-1) = R-q = B.
+```
+
+This is a fixed-width identity, including L=0. `load` obtains that complement
+in one sequential pass and remembers only whether any copied bit was one.
+It restores both heads. No descriptor for B is retained.
+
+Initialize the counter to q-1 and the phase to genuine. At coordinate position
+x the invariant is
+
+```text
+0 <= x < q:    phase = genuine, counter = q-1-x;
+q <= x < R:   phase = padding, counter = R-1-x.
+```
+
+`borrow` subtracts one modulo 2^L and reports underflow. In either phase a
+positive counter decrements without a carry to the next coordinate.
+At the last genuine position it underflows. Load B by complementing the
+descriptor. If B is nonzero, subtract one once, enter the padding phase, and
+report no coordinate carry. The next position is x=q and its counter is
+B-1=R-1-q, as required. That preparatory subtraction cannot underflow.
+
+If B is zero, there is no padding position. Reload q-1, remain genuine,
+and report a coordinate carry immediately. At the last padding position,
+underflow likewise reloads q-1, resets the genuine phase, and reports a carry.
+These exhaust the cases and prove the invariant and reset for every q>=1.
+For q=1, L=0, the first subtraction underflows on `$`, the complement is
+empty/zero, and the coordinate carries after its one genuine position.
+For q=R, the complement is all zero and no spurious padding position is emitted.
+
+## Rectangle, ownership and termination
+
+The last coordinate advances fastest. Its carry advances the preceding one,
+and so on. The invariant shows that each coordinate makes exactly R_i visits
+per cycle and resets. Induction over this fixed five-level odometer gives
+exactly N visits in lexicographic padded order, then one outer carry.
+A visit is genuine precisely when all five phase bits say genuine, equivalently
+when every coordinate is less than q_i. Thus genuine visits appear in the
+original lexicographic order. Padding reads its next source bit exactly there
+and writes zero elsewhere. Restriction reads every input bit and writes its
+next output bit exactly at genuine visits. Arbitrary padded bits are discarded.
+
+All work writes target the five counter tapes. Descriptor and input tapes are
+read-only. `borrow`, `load`, and `clear` restore their starting heads by scanning
+to `^`; no head jump is free. After the outer carry all counters contain their
+initial q_i-1 and all phases are genuine. Clearing the same five intervals
+returns D zeros. Both payload heads rewind over their used intervals. Marker
+positions, protected cells and the immutable tapes are fixed. The argument is
+unchanged by translated origins and permits immediate reuse of the zero work.
+
+Every marker loop traverses at most L_i+1 cells per forward pass and L_i+1
+on rewind. Every countdown phase has at most R_i visits. The outer payload
+loop has exactly N visits. These are encoded finite bounds from the entry
+contract; the machine does not decode them into host integers.
+
+## Uniform complete action bound
+
+We count literal reads, writes, unit moves and the explicit finite-control
+charges described above. Constructor/counter initialization and final cleanup
+are included. Descriptor construction and physical allocation are external.
+
+A load, with either polarity, costs exactly 8L+8 actions. It uses L+1 descriptor
+reads, one counter-end read, L writes, 2L forward moves, then two rewinds,
+each with L+1 reads and L+2 moves. Clearing costs 5L+4 actions.
+
+If a decrement reaches j zero bits before a one, it costs 5(j+1) actions.
+Underflow at zero costs 5L+4, at most 5(L+1). For positive integers 1 through m,
+the total number of visited bits is
+
+```text
+sum_(v=1)^m (1+nu_2(v))
+  = m + sum_(j>=1) floor(m/2^j) <= 2m.
+```
+
+In one complete coordinate cycle, genuine-phase subtractions run through
+q-1,...,0. If B>0, the padding initialization and its later subtractions run
+through B,...,0. Their combined visits are at most
+
+```text
+2(q-1)+(L+1) + 2B+(L+1) = 2R+2L.
+```
+
+If B=0 the genuine subtractions alone obey the same upper bound. With two
+loads per cycle, all coordinate work after initialization costs at most
+10R+26L+16. For L>=1, L<=R/2 and R>=2, so this is at most 31R. For L=0,
+the literal empty-counter cycle costs 20=20R. Hence 32R bounds every case.
+
+Coordinate i completes N/(R_i times the product of its inner R_j) cycles,
+at most N/R_i. All five coordinates therefore cost at most 160N actions.
+Padding or restriction payload traffic, including both rewinds and endpoint
+checks, is 4M+4N+8 <= 8N+8. There are N emit and at most 5N advance charges.
+Initialization and final clearing cost 13D+60. The total is consequently
+
+```text
+<= 174N+13D+68 <= 192N+16D+80.
+```
+
+No measured timing enters this bound. The constant is sufficient, not optimal.
+The proof is uniform in the five positive cardinalities.
+
+## Resource comparison and scientific scope
+
+The new machine uses five descriptor tapes, five counter tapes and two payload
+tapes, for twelve distinct tapes. Its mutable counter contents occupy D cells,
+plus ten fixed counter delimiters. The cited PR2636 interface uses five
+descriptor tapes, ten counter tapes and two payload tapes, with 2D counter cells
+and twenty counter delimiters. It gives a 1024N+128D+128 sufficient bound.
+Those predecessor resources are cited from its written contract, not recomputed
+or audited. The contribution is the new two-phase sharing construction and the
+proof above. No minimum-tape or optimal-action claim is made.
+
+The scan remains a component. It requires canonical aggregate descriptors,
+owned zero work and fresh output. It does not produce these resources, execute
+the completed fast exchange, park ancestors, join a selected recursive caller,
+or supply a complete precision/stock/tape invoice. It does not discharge a
+selected framework assumption, change the selected frontier or claim a new
+kappa or a complete integer-multiplication theorem.
+
+## Executable evidence and code limits
+
+The independent oracle enumerates mixed-radix coordinates with host arithmetic;
+it imports no predecessor implementation. The machine reference reads only
+its tape API. The verifier checks 516 full scans, 1300 additional exhaustive
+payload scans, and 257 complete coordinate cycles. Thirteen controls cover
+short/long/nonbinary input, wrong coordinate count/phase, counter/descriptor
+symbols and width, immutable writes, nonunit moves, resource exhaustion,
+a wrong complement, and omitted cleanup. Counts are generated by the checker.
+Normal and optimized modes retain every check.
+
+Python's object allocation, integer instrument counters and fixture arrays are
+reference-model deviations from allocation-free operation. The claimed tape
+machine owns only the intervals specified above. Verification is bounded by
+258 fixed shapes of maximum padded volume 1024, exhaustive payload lengths
+at most nine, and q<=257 in the coordinate oracle. Each metered run has an
+explicit action cap. The call graph is nonrecursive and functions have fewer
+than 60 physical lines. The tape dispatch and metering callback have fixed
+local targets. Mutation controls temporarily replace two local functions and
+restore them in `finally`. Dynamic import loads only the new local machine.
+Warning-strict normal/optimized replay and syntax/function-size checks are the
+available diagnostics. A compiled finite-state transition table, proof-kernel
+check and independent human review are unclaimed.
diff --git a/research/single-counter-aggregate-padding/README.md b/research/single-counter-aggregate-padding/README.md
new file mode 100644
index 0000000000..c471192b5a
--- /dev/null
+++ b/research/single-counter-aggregate-padding/README.md
@@ -0,0 +1,97 @@
+# Aggregate padding on twelve tapes
+
+A new two-phase counter construction reduces ywz65's
+[PR #2636](https://github.com/CrocSwap/integer-mult-bounds/pull/2636)
+five-coordinate padding/restriction interface from seventeen tapes to twelve.
+Mutable counter contents decrease from 2D cells to D, where D is the sum of
+the descriptor widths. The complete scan has the uniform sufficient action bound
+
+```text
+192N + 16D + 80,
+```
+
+including initialization, payload traffic, all head returns and zero-counter
+cleanup. N is the binary-padded rectangle volume. This is a scoped constructive
+proof with finite corroboration, produced by Nick Petalas. No new kappa is claimed.
+
+The immutable q-1 descriptor supplies both countdowns. First count the q genuine
+positions. Then load its fixed-width bitwise complement R-q and count the padding
+positions using the same physical counter. Zero padding length carries immediately.
+The singleton case uses an empty counter. No new descriptor or decoded coordinate
+is needed. [PROOF.md](PROOF.md) proves correctness, ownership and the action bound.
+
+The comparison uses the predecessor's stated 17-tape, 2D-cell and
+1024N+128D+128 contract as a cited premise. Its verifier and scientific counts
+are not replayed. The new machine and independent mixed-radix oracle are standalone.
+The result is neither a minimum-tape theorem nor a wall-clock performance claim.
+
+## Reproduction
+
+From the repository root, with the standard-library CPython 3.12 interpreter:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/single-counter-aggregate-padding/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/single-counter-aggregate-padding/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/single-counter-aggregate-padding
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/single-counter-aggregate-padding --check-source-history
+```
+
+Another CPython 3.12 path may replace the local path. The direct command also
+runs from a Git-free package directory. Expected marker:
+`PASS_SINGLE_COUNTER_AGGREGATE_PADDING`. The verifier prints a generated receipt
+bound to all package file hashes; it writes nothing.
+
+Evidence covers 516 full scan cases, 1300 exhaustive payload scans, 257 complete
+coordinate cycles and thirteen rejection/mutation controls. Every successful
+scan checks the independent payload oracle, all twelve physical heads, immutable
+input/descriptors, protected boundaries, D zero counter cells, and the complete
+action bound. Restriction tests include arbitrary nonzero discarded padding.
+Finite cases corroborate the uniform written proof; they do not prove it by
+extrapolation. Warning-strict normal and optimized checks are registered.
+
+## Scope and provenance
+
+Canonical base is `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8.
+The selected metadata baseline passed at kappa 0.003125804. The task explicitly
+changes `uniform-transfer-audit` to this local physical-resource construction,
+relevant to the `precision_tape` and `owned_erasure` interfaces. No complete
+selected assumption is discharged. [TASK.json](TASK.json) records that change;
+[SOURCES.json](SOURCES.json) retains exact predecessor and catalogue provenance.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246892)
+reserves the same one-counter construction. Live open PRs, recent account work,
+handoffs and local locks were checked before claiming. Searches of main README
+text and merged PRs included the general five-coordinate, one-counter and
+two-phase forms. Cached overlap covered 407 open PRs and 5818 Discussion records;
+its sparse local text coverage was 70/8348 notes. Relevant source and adjacent
+padding packages were separately read. These are bounded overlap checks, not
+a literature-wide novelty guarantee.
+
+The source is ywz65's PR2636, retained at
+`c1e173b7af38603bc7660a8829e75006e93645d3`. PR2457 supplies aggregate-before-padding;
+commdata2338's PR2399, Jose Manuel's PR2234 and Adam Gall's PR2087 retain the
+preceding descriptor, parking and supplier credit. Binary countdown amortization
+and complement arithmetic are classical. The new contribution is their shared
+physical counter, successful ownership contract and complete uniform bound.
+All predecessor files and credit lines retain their bytes. Apache-2.0.
+
+## Limitations
+
+Canonical descriptors, owned zero counters and fresh output are inputs. Descriptor
+production, allocation, ancestor parking, the completed fast callee and selected
+caller integration remain external. Successful well-formed entries are covered;
+malformed calls need not restore state. No compiled transition table, physical
+allocator, all-size supplier admission, stock/precision theorem, selected scientific
+cold replay, Lean or Docker run is supplied. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Can an actual completed exchange use the twelve-tape scan within its fixed
+  tape inventory? Start at PR2457's complete callee boundary and count its
+  simultaneous tapes, payload intervals, head returns and ancestor parking.
+  The actual callee/ownership interface remains the blocker.
+- Can one shared physical work tape hold several coordinate counters while
+  retaining linear complete movement? Start with two unequal widths and include
+  travel between their delimiters. The present proof relies on separate heads
+  and gives no such serialization bound.
diff --git a/research/single-counter-aggregate-padding/SOURCES.json b/research/single-counter-aggregate-padding/SOURCES.json
new file mode 100644
index 0000000000..f71c5ea5a2
--- /dev/null
+++ b/research/single-counter-aggregate-padding/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/aggregate-padding-tapes/README.md",
+      "usage": "provenance",
+      "git_blob": "febce9e006ce6134f41900211460bae5a16a4d18",
+      "sha256": "4f679290f9a8a3eca760088b05618198f3a018455e980423c5cf96376f0eae28"
+    },
+    {
+      "path": "research/aggregate-padding-tapes/tapes.py",
+      "usage": "provenance",
+      "git_blob": "8cb10b925a961e73743151421b7099f22045474d",
+      "sha256": "22ab7af6fa5c0ef5201be25e1aed41b6ee6d7c24a71dc47646c73911c04eeef5"
+    }
+  ]
+}
diff --git a/research/single-counter-aggregate-padding/TASK.json b/research/single-counter-aggregate-padding/TASK.json
new file mode 100644
index 0000000000..f682281b57
--- /dev/null
+++ b/research/single-counter-aggregate-padding/TASK.json
@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "One-counter two-phase five-coordinate padding/restriction on twelve tapes, with D owned counter cells and a uniform 192N+16D+80 complete action bound.",
+  "scope_change_reason": "Original resource construction at the aggregate padding component, rather than an audit or discharge of a complete selected framework assumption.",
+  "bottleneck_link": "A local physical metadata/work reduction relevant to precision_tape and owned_erasure. Full caller allocation and admission remain separate; no new recursive profile or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified tape/work reduction; package it without further construction expansion.",
+  "outcome": "completed",
+  "evidence": "Standalone literal tape checker and independent mixed-radix oracle; full uniform proof in PROOF.md.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual completed exchange integrate this twelve-tape scan?",
+      "why_it_matters": "A local scan does not establish the complete physical supplier.",
+      "first_step": "Bind PR2457 complete callee inputs, simultaneous tapes, head returns and ancestor parking.",
+      "blocked_by": "The actual completed callee and ownership/parking interface are external."
+    },
+    {
+      "question": "Can several counters share one physical work tape at linear movement cost?",
+      "why_it_matters": "Separate counter heads account for five of the twelve tapes.",
+      "first_step": "Analyze two unequal counter widths, including all travel between delimiters.",
+      "blocked_by": "No serialized-counter movement bound or construction is supplied."
+    }
+  ],
+  "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19246892"
+}
diff --git a/research/single-counter-aggregate-padding/VERIFY.json b/research/single-counter-aggregate-padding/VERIFY.json
new file mode 100644
index 0000000000..f838f3400d
--- /dev/null
+++ b/research/single-counter-aggregate-padding/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": 60,
+      "checks": "Literal tape construction, independent rectangle oracle, complete action/work/head checks and thirteen rejection/mutation controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same complete checks with Python assertions disabled."
+    }
+  ]
+}
diff --git a/research/single-counter-aggregate-padding/machine.py b/research/single-counter-aggregate-padding/machine.py
new file mode 100644
index 0000000000..9a88c91be8
--- /dev/null
+++ b/research/single-counter-aggregate-padding/machine.py
@@ -0,0 +1,128 @@
+"""One-counter aggregate scan, produced by Nick Petalas; Apache-2.0.
+
+Only bit/marker reads, writes, and unit head moves drive this machine.
+Cardinality, width, position, and volume integers belong to the checker.
+"""
+
+
+def rewind(tape):
+    tape.move(-1)
+    while tape.read() != "^":
+        tape.move(-1)
+    tape.move(1)
+
+
+def borrow(counter):
+    """Subtract one at fixed width; return underflow and restore the head."""
+    while True:
+        bit = counter.read()
+        if bit == "$":
+            rewind(counter)
+            return True
+        if bit == "1":
+            counter.write("0")
+            rewind(counter)
+            return False
+        if bit != "0":
+            raise ValueError("invalid counter symbol")
+        counter.write("1")
+        counter.move(1)
+
+
+def load(descriptor, counter, complement=False):
+    """Copy q-1 or its fixed-width complement; report a nonzero result."""
+    nonzero = False
+    while True:
+        bit = descriptor.read()
+        if bit == "$":
+            break
+        if bit not in ("0", "1"):
+            raise ValueError("invalid descriptor symbol")
+        value = ("1" if bit == "0" else "0") if complement else bit
+        nonzero = nonzero or value == "1"
+        counter.write(value)
+        descriptor.move(1)
+        counter.move(1)
+    if counter.read() != "$":
+        raise ValueError("counter width mismatch")
+    rewind(descriptor)
+    rewind(counter)
+    return nonzero
+
+
+def clear(counter):
+    while counter.read() != "$":
+        counter.write("0")
+        counter.move(1)
+    rewind(counter)
+
+
+class Coordinate:
+    """One immutable descriptor, one zero-owned counter, one phase bit."""
+
+    def __init__(self, descriptor, counter):
+        self.descriptor = descriptor
+        self.counter = counter
+        self.genuine = True
+        load(descriptor, counter)
+
+    def advance(self):
+        if not borrow(self.counter):
+            return False
+        if self.genuine and load(self.descriptor, self.counter, True):
+            if borrow(self.counter):
+                raise RuntimeError("nonzero padding countdown underflowed")
+            self.genuine = False
+            return False
+        load(self.descriptor, self.counter)
+        self.genuine = True
+        return True
+
+    def finish(self):
+        clear(self.counter)
+
+
+def scan(coordinates, source, target, control, restrict=False):
+    """Scan five coordinates, then restore work and heads.
+
+    Entry tapes are well-formed delimited binary words. All counters have the
+    descriptor's width and initially contain zeros. Output is fresh owned work.
+    The callback records a fixed finite-control action in the model.
+    """
+    if len(coordinates) != 5:
+        raise ValueError("five coordinates required")
+    while True:
+        control("emit")
+        genuine = all(coordinate.genuine for coordinate in coordinates)
+        if restrict:
+            bit = source.read()
+            if bit not in ("0", "1"):
+                raise ValueError("short or nonbinary source")
+            source.move(1)
+            if genuine:
+                target.write(bit)
+                target.move(1)
+        else:
+            bit = "0"
+            if genuine:
+                bit = source.read()
+                if bit not in ("0", "1"):
+                    raise ValueError("short or nonbinary source")
+                source.move(1)
+            target.write(bit)
+            target.move(1)
+        complete = True
+        for coordinate in reversed(coordinates):
+            control("advance")
+            if not coordinate.advance():
+                complete = False
+                break
+        if complete:
+            break
+    if source.read() != "$":
+        raise ValueError("long source")
+    target.write("$")
+    rewind(source)
+    rewind(target)
+    for coordinate in coordinates:
+        coordinate.finish()
diff --git a/research/single-counter-aggregate-padding/verify.py b/research/single-counter-aggregate-padding/verify.py
new file mode 100644
index 0000000000..47dc8f7200
--- /dev/null
+++ b/research/single-counter-aggregate-padding/verify.py
@@ -0,0 +1,233 @@
+"""Literal tape execution and independent mixed-radix oracle; Apache-2.0."""
+
+import hashlib
+import importlib.util
+import itertools
+import json
+import math
+from pathlib import Path
+
+PACKAGE = Path(__file__).resolve().parent
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def module():
+    spec = importlib.util.spec_from_file_location("single_counter_machine", PACKAGE / "machine.py")
+    require(spec is not None and spec.loader is not None, "missing machine")
+    result = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(result)
+    return result
+
+
+class Meter:
+    def __init__(self, cap):
+        self.cap = cap
+        self.count = 0
+
+    def tick(self, _action):
+        self.count += 1
+        require(self.count <= self.cap, "action budget exhausted")
+
+
+class Tape:
+    """Finite tape with protected cells outside its two markers."""
+
+    def __init__(self, contents, meter, origin=0, writable=True):
+        self.cells = ["!"] + list(contents) + ["!"]
+        self.origin = origin
+        self.head = origin + 2
+        self.initial_head = self.head
+        self.meter = meter
+        self.writable = writable
+        self.capacity = len(self.cells)
+
+    def index(self):
+        index = self.head - self.origin
+        require(1 <= index < self.capacity - 1, "crossed protected boundary")
+        return index
+
+    def read(self):
+        self.meter.tick("read")
+        return self.cells[self.index()]
+
+    def write(self, value):
+        self.meter.tick("write")
+        require(self.writable, "write to immutable tape")
+        require(value in ("0", "1", "$"), "invalid write")
+        self.cells[self.index()] = value
+
+    def move(self, step):
+        self.meter.tick("move")
+        require(type(step) is int and step in (-1, 1), "nonunit move")
+        self.head += step
+        self.index()
+
+
+def descriptor(q):
+    return "" if q == 1 else bin(q - 1)[2:][::-1]
+
+
+def oracle(shape, payload, restrict):
+    widths = [(q - 1).bit_length() for q in shape]
+    padded = [1 << width for width in widths]
+    coordinates = itertools.product(*(range(r) for r in padded))
+    live = [all(x < q for x, q in zip(row, shape)) for row in coordinates]
+    if restrict:
+        return "".join(bit for bit, take in zip(payload, live) if take)
+    iterator = iter(payload)
+    return "".join(next(iterator) if take else "0" for take in live)
+
+
+def fixture(machine, shape, payload, restrict=False, origin=0, prepare=None):
+    widths = [(q - 1).bit_length() for q in shape]
+    volume = math.prod(1 << width for width in widths)
+    output_size = math.prod(shape) if restrict else volume
+    bound = 192 * volume + 16 * sum(widths) + 80
+    meter = Meter(bound)
+    descriptors = [Tape("^" + descriptor(q) + "$", meter, origin + i * 7, False)
+                   for i, q in enumerate(shape)]
+    counters = [Tape("^" + "0" * width + "$", meter, origin - i * 11)
+                for i, width in enumerate(widths)]
+    source = Tape("^" + payload + "$", meter, origin + 100, False)
+    target = Tape("^" + "_" * (output_size + 1), meter, origin - 100)
+    immutable = [(tape, tuple(tape.cells)) for tape in descriptors + [source]]
+    coordinates = [machine.Coordinate(d, c) for d, c in zip(descriptors, counters)]
+    if prepare is not None:
+        prepare(coordinates)
+    machine.scan(coordinates, source, target, meter.tick, restrict)
+    require("".join(target.cells[2:2 + output_size]) == oracle(shape, payload, restrict),
+            "wrong payload")
+    require(target.cells[2 + output_size] == "$", "missing output delimiter")
+    for tape, before in immutable:
+        require(tuple(tape.cells) == before, "immutable source changed")
+    for tape in counters:
+        require(set(tape.cells[2:-2]) <= {"0"}, "counter not zero")
+    for tape in descriptors + counters + [source, target]:
+        require(tape.head == tape.initial_head, "head not restored")
+        require(tape.cells[0] == tape.cells[-1] == "!", "outside cell changed")
+    require(len(descriptors + counters + [source, target]) == 12, "wrong tape count")
+    require(sum(len(t.cells) - 4 for t in counters) == sum(widths), "wrong work extent")
+    return meter.count, bound
+
+
+def payload(size, seed):
+    return "".join(str(((i * 13 + seed) ^ (i >> 1)) & 1) for i in range(size))
+
+
+def scan_cases(machine):
+    records = []
+    shapes = list(itertools.product((1, 2, 3), repeat=5))
+    shapes += [(q, 1, 1, 1, 1) for q in (4, 5, 7, 8, 9, 15, 16, 17, 31, 32, 33, 65, 129)]
+    shapes += [(3, 5, 2, 7, 1), (2, 3, 4, 5, 2)]
+    for index, shape in enumerate(shapes):
+        n = math.prod(1 << (q - 1).bit_length() for q in shape)
+        for restrict in (False, True):
+            size = n if restrict else math.prod(shape)
+            steps, bound = fixture(machine, shape, payload(size, index), restrict, index - 130)
+            records.append((shape, restrict, steps, bound))
+    return records
+
+
+def all_payloads(machine):
+    count = 0
+    for shape in ((1, 1, 1, 1, 1), (3, 1, 1, 1, 1), (3, 3, 1, 1, 1)):
+        size = math.prod(shape)
+        for bits in itertools.product("01", repeat=size):
+            word = "".join(bits)
+            fixture(machine, shape, word)
+            fixture(machine, shape, oracle(shape, word, False), True)
+            count += 2
+    for bits in itertools.product("01", repeat=8):
+        fixture(machine, (3, 2, 1, 1, 1), "".join(bits), True)
+        count += 1
+    return count
+
+
+def coordinate_cases(machine):
+    count = 0
+    for q in range(1, 258):
+        width = (q - 1).bit_length()
+        r = 1 << width
+        meter = Meter(96 * r + 32 * width + 128)
+        d = Tape("^" + descriptor(q) + "$", meter, -17, False)
+        c = Tape("^" + "0" * width + "$", meter, 39)
+        coordinate = machine.Coordinate(d, c)
+        for index in range(r):
+            require(coordinate.genuine == (index < q), "wrong coordinate phase")
+            require(coordinate.advance() == (index == r - 1), "wrong coordinate carry")
+        require(coordinate.genuine, "phase did not reset")
+        coordinate.finish()
+        require(set(c.cells[2:-2]) <= {"0"}, "coordinate cleanup")
+        require(c.head == c.initial_head and d.head == d.initial_head, "coordinate head")
+        count += 1
+    return count
+
+
+def rejection(action):
+    try:
+        action()
+    except (ValueError, RuntimeError):
+        return 1
+    raise ValueError("control accepted")
+
+
+def controls(machine):
+    count = 0
+    for word in ("", "00", "x"):
+        count += rejection(lambda word=word: fixture(machine, (1,) * 5, word))
+    count += rejection(lambda: fixture(machine, (1,) * 5, "0", prepare=lambda c: c.pop()))
+    count += rejection(lambda: fixture(machine, (3, 1, 1, 1, 1), "101",
+                                       prepare=lambda c: setattr(c[0], "genuine", False)))
+    meter = Meter(100)
+    count += rejection(lambda: machine.borrow(Tape("^x$", meter)))
+    count += rejection(lambda: machine.load(Tape("^x$", meter), Tape("^0$", meter)))
+    count += rejection(lambda: machine.load(Tape("^1$", meter), Tape("^00$", meter)))
+    count += rejection(lambda: Tape("^0$", meter, writable=False).write("1"))
+    count += rejection(lambda: Tape("^0$", meter).move(2))
+    count += rejection(lambda: Meter(0).tick("exhaustion"))
+    return count
+
+
+def mutation_controls(machine):
+    count = 0
+    original_load = machine.load
+    original_clear = machine.clear
+
+    def wrong_complement(descriptor, counter, complement=False):
+        return original_load(descriptor, counter, False)
+
+    try:
+        machine.load = wrong_complement
+        count += rejection(lambda: fixture(machine, (3, 1, 1, 1, 1), "101"))
+    finally:
+        machine.load = original_load
+    try:
+        machine.clear = lambda counter: None
+        count += rejection(lambda: fixture(machine, (3, 1, 1, 1, 1), "101"))
+    finally:
+        machine.clear = original_clear
+    require(machine.load is original_load and machine.clear is original_clear,
+            "mutation binding was not restored")
+    return count
+
+
+def main():
+    machine = module()
+    records = scan_cases(machine)
+    result = {"status": "PASS_SINGLE_COUNTER_AGGREGATE_PADDING", "claim_type": "scoped construction",
+              "scan_cases": len(records), "all_payload_scans": all_payloads(machine),
+              "coordinate_cycles": coordinate_cases(machine),
+              "controls": controls(machine) + mutation_controls(machine),
+              "tapes": 12, "counter_cells": "D", "action_bound": "192N+16D+80",
+              "scan_digest": hashlib.sha256(json.dumps(records).encode()).hexdigest()}
+    result["sha256"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest()
+                        for p in sorted(PACKAGE.iterdir()) if p.is_file()}
+    print(json.dumps(result, indent=2, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()