diff --git a/research/marked-tape-ddg-reversal/PROOF.md b/research/marked-tape-ddg-reversal/PROOF.md
new file mode 100644
index 0000000000..5a042f2251
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/PROOF.md
@@ -0,0 +1,148 @@
+# Counterless reversal with an owned delimiter
+
+This is a scoped proof for one fixed two-tape machine. The source sampling
+law and edge-inverse lemma are credited premises, not new sampling theorems.
+The new step replaces a numerical stopping counter by a local tape boundary.
+
+## Statement and exact boundary
+
+Let the random tape contain an infinite binary string beginning at position s,
+with one caller-owned blank symbol `_` at s-1. Positions below s-1 are arbitrary
+and protected. The random head begins at s. A second tape has one stationary
+head on a dirty four-symbol cell A, interpreted as a two-bit accumulator.
+The caller supplies the fixed `(1,1)` denominator-13 DDG of zxv's PR #6072.
+Write i for its first output and T for its stopping depth on the binary string.
+
+For every string with finite T, the machine in `machine.py` terminates with
+A replaced by A XOR i, every random-tape symbol and both heads restored, the
+owned delimiter cell blank, and finite control at its fixed return label.
+It uses exactly 3T+4 two-tape transitions and 2T+4 random-head moves, has
+maximum random-head excursion T to the right and one cell to the left, and
+writes the delimiter cell exactly twice. It has no numerical stopping counter,
+position register or per-step history. A finite certificate establishes 1,563
+control states and 10,000 rules for this fixed graph.
+
+A two-tape transition reads both current symbols, writes their replacements,
+and moves the random head by -1, 0 or 1. The output head stays fixed. The random
+tape alphabet is `{0,1,_,#}`; the output alphabet has four symbols. These are
+finite-alphabet machine steps, not individual binary gates or the repository's
+native paid calls. Fixed rule selection is part of finite control, with no
+unit-cost RAM lookup assumption. Binary-alphabet lowering has an additional
+constant cost not computed here.
+
+## Predecessor facts used
+
+The retained `vendor/paired_sampler.py` is zxv's exact PR #6072 source at
+`9011bf83e85ecd0443c789cf03259442f750877d`. Only `make(1,1)` is called to obtain
+its graph, phase layout and cited expectation. Its original `main`, sampling
+census and optimality checks are not run.
+
+JoyboyBrian's PR #6102 at `0422af13625c2e7e8ece28bdd74364a61764c64a`, retained in
+`vendor/PROOF.reversal.md`, proves that the predecessor phase p, consumed bit u
+and current DDG target identify a unique previous node. For an internal target,
+recover q by adding the sum of the four binary digits to its node index. For a
+leaf, recover q from that leaf's digit slot. Then the previous node is
+(q-u)/2. The digit ordering and phase are essential. We use that lemma, rather
+than claiming a new inverse or auditing the predecessor proof.
+
+The source law gives the independent output probabilities `(144,12,12,1)/169`
+and E[T] = 9960277917013927549978 / 4649714690825496825793 < 9/4.
+These probabilistic statements remain predecessor premises. Our pathwise
+construction does not need fair bits or independent bits for reversibility.
+
+## Local machine
+
+`F(p,j)` means forward DDG state j in phase p. `B(p,j)` means that j is the
+current reverse target and the random head is immediately after its prefix.
+`R(p,j)` means that the head has moved left onto the next bit to undo.
+Here j may be a leaf in B and R. The phase is always modulo 156.
+
+1. In `entry`, move left. In `prepare`, replace the owned blank by `#`, move
+   right, and enter `F(0,0)`. These are two transitions.
+2. For `F(p,j)` reading u, apply the source edge and move right. At an internal
+   target enter its F state. At leaf i, XOR i into the second tape's symbol and
+   enter `B(p+1,leaf_i)`. Output retention is part of this last transition.
+3. In any B state, move left and enter the corresponding R state.
+4. In R on a binary symbol u, apply the predecessor's inverse edge, decrement
+   phase modulo 156, and enter its B state without moving the head.
+5. The only rule on `#` in R is `R(0,0)`: replace `#` by `_`, move right, and
+   return. Other R states have no marker transition.
+
+No transition reads an absolute coordinate, stopping depth or elapsed time.
+The Python observer's bounded loop, head coordinate and measured counters are
+outside the finite rule key. The full rule key contains only control, current
+random-tape symbol and current output symbol.
+
+## Correctness for arbitrary terminating paths
+
+After k forward steps, the head is at s+k and F has exactly the source's
+phase and node, until the source first terminates. Thus after T steps the
+output cell is A XOR i, the head is s+T and B stores the last target and phase.
+
+By backwards induction, after reversing T-k edges, B stores the exact source
+state after k steps, phase k modulo 156, and the head is at s+k. For k>0,
+the next left move reads a binary symbol at s+k-1. The cited inverse lemma
+recovers exactly the source state after k-1 steps. It leaves the output cell
+unchanged. At k=0 the next left move reads the delimiter at s-1 and B's state
+is the root at phase zero. The final rule erases the marker and returns to s.
+
+A root revisit at a positive multiple of 156 does not terminate reversal:
+its preceding tape cell is binary. The unique delimiter, rather than a root
+state test, distinguishes the initial visit. No numerical T survives or is
+needed during the call. The output value need not be retained in separate
+scratch because it was copied before the leaf was undone.
+
+All data symbols are read-only. The only first-tape writes are blank-to-marker
+in preparation and marker-to-blank on return. Hence arbitrary protected cells,
+the entire random string and the owned blank are restored. The output head
+never moves. This proves the stated map on every terminating path.
+
+The local rules are also one-step injective as a partial machine on arbitrary
+configurations. Every destination control has a unique incoming head direction.
+Given that direction, the written symbol and output symbol identify a unique
+incoming rule. Forward injectivity is the cited phase-and-coin inverse. Reverse
+injectivity is forward determinism. The marker/preparation ranges are disjoint
+from binary ranges. The verifier checks these two finite injectivity predicates
+on every generated rule. Invalid configurations may have no transition; total
+behavior outside the stated entry invariant is not asserted.
+
+## Exact accounting and finite certificate
+
+Preparation costs two steps. The forward walk costs T steps, including output
+XOR. Reversal costs two steps per consumed bit and two final delimiter steps.
+The total is 3T+4. Preparation and the final marker probe each move twice;
+each data bit contributes one forward and one backward head move. Travel is
+2T+4. No per-step controller bit is allocated.
+
+There are 312 F states. The actual source edges produce 624 distinct target/
+phase pairs: 312 internal pairs and 312 leaf/phase pairs. Each has B and R
+states. Entry, prepare and return add three, giving 312+2*624+3=1,563.
+For each of four dirty output symbols, the rules contain 624 forward edges,
+1,248 B moves, 624 inverse edges, two entry rules, one prepare rule and one
+return rule. Thus 4*(624+1248+624+2+1+1)=10,000. The verifier enumerates the
+states and rules instead of inferring these finite counts from a sample run.
+
+Using the cited source mean, E[steps] = 3E[T]+4 equals
+48479692514343769953106 / 4649714690825496825793 < 43/4.
+This counts finite-alphabet machine steps. It is not a wall-clock speedup or a
+comparison with a native recursive invoice.
+
+The finite replay covers 4,088 short dirty-output runs and all 938 terminating
+prefixes through depth 470. Those longer runs contain 942 reverse root revisits.
+They corroborate the interpreter, wrap handling and exact bills. The induction,
+not the finite fixture depth, proves correctness for arbitrary finite T.
+
+## Scope and remaining cost
+
+The changed contract supplies one owned blank immediately beside the random
+segment and a stationary output head. The machine pays to mark and clear that
+blank. Providing these positions in an actual caller, fixed binary-machine
+lowering, parameter dispatch and native adaptation remain separate obligations.
+The graph and finite control are fixed before any random bits are read.
+
+The resident transcript and the random-head excursion have no finite worst-case
+bound. This is constant auxiliary control and delimiter storage, not constant
+total space. After output retention, the consumed tape is correlated with that
+output. Restoring its symbols does not make them conditionally fresh. No actual
+multiplier caller, supplier admission, new kappa, complete multiplication theorem,
+independent human acceptance or proof-kernel verification is claimed.
diff --git a/research/marked-tape-ddg-reversal/README.md b/research/marked-tape-ddg-reversal/README.md
new file mode 100644
index 0000000000..1d45919d30
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/README.md
@@ -0,0 +1,108 @@
+# A marked resident tape removes the DDG stopping counter
+
+For the fixed `(1,1)` paired sampler, one owned blank beside the random segment
+replaces the unbounded stopping counter of [JoyboyBrian's PR #6102](https://github.com/CrocSwap/integer-mult-bounds/pull/6102).
+The new finite-state two-tape machine prepares a delimiter, copies the sampled
+two-bit output into a dirty XOR accumulator, reverses to that delimiter, clears
+it and returns both heads. For every terminating path of depth T it uses exactly
+**3T+4 finite-alphabet transitions** and **2T+4 input-head moves**.
+The controller has **1,563 states and 10,000 rules**, independent of T.
+
+This is a **scoped proof with a finite machine certificate**. It supplies a
+counterless local tape service under the stated changed boundary. The resident
+random transcript and head excursion remain unbounded. The output accumulator
+becomes A XOR i; its old value is not erased or required to be zero. The random
+tape, its owned blank and both head positions are restored.
+
+[PROOF.md](PROOF.md) states the machine model, proves the arbitrary-path
+induction and one-step injectivity, and derives the exact bill. Preparation and
+marker erasure are included. The random alphabet is `{0,1,_,#}` and the output
+cell has four symbols. The second head stays stationary. This is a concrete
+finite transition system; its rule selection does not use a RAM oracle.
+Binary-alphabet lowering and repository native paid calls have different costs.
+
+## Evidence and reproduction
+
+From the repository root, using Python 3.12 and the standard library:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/marked-tape-ddg-reversal/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/marked-tape-ddg-reversal/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/marked-tape-ddg-reversal
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/marked-tape-ddg-reversal --check-source-history
+```
+
+`PASS_MARKED_TAPE_DDG_REVERSAL` enumerates every rule and state, checks local
+injectivity and permitted writes, then runs 4,088 short dirty-output fixtures
+and all 938 terminating prefixes through depth 470. The long fixtures contain
+942 reverse root revisits. Each run checks exact steps/travel, output XOR,
+complete tape restoration, returned head and delimiter erasure. Controls reject
+wrong output, exhausted fixtures, bad input, missing marker return and premature
+halting on a wrapped root. Finite tests support the implementation; the proof's
+induction establishes arbitrary finite stopping depth.
+
+[RESULT.json](RESULT.json) is generated by the verifier and binds the proof,
+machine, verifier and retained source bytes by SHA256. The verifier writes
+nothing during ordinary replay. Its optional `--write-result` path is only for
+explicit regeneration. The Python interpreter's position and bounded observer
+counter are measurement state. They do not occur in the machine's rule keys.
+
+Using zxv's cited source expectation, the new exact bill has expected value
+`48479692514343769953106/4649714690825496825793 < 43/4` transitions.
+This is a consequence of the predecessor law, not a new sampling optimum or
+runtime benchmark. The source's probability/census suite is not rerun.
+
+## Scope and credit
+
+The changed `formal-interface-lemma` task takes the first Open next question of
+PR #6102 and supplies one local service boundary. It is not a proof-assistant
+formalization. An actual caller must provide the owned adjacent blank and the
+stationary output head; it must also preserve the random segment throughout
+cleanup. No conditional freshness of reused bits, parameter selection, binary
+gate tariff, native supplier, complete multiplier or new kappa is claimed.
+The five selected framework assumptions are not discharged.
+
+This scoped construction was produced by Nick Petalas. New work is Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+zxv's PR #6072 supplies the fixed DDG, classical sampling argument and mean.
+JoyboyBrian's PR #6102 supplies the phase-and-coin edge inverse and identifies
+physical tape/counter costs as open. Their exact sources and original credit
+are retained unchanged in `vendor/`; [vendor/ORIGIN.json](vendor/ORIGIN.json)
+records public origin heads and hashes. The new contribution is the delimiter
+construction, explicit local machine and exact counterless tariff. It does not
+claim the classical technique of reversing a recorded computation as new.
+
+The frozen card, base and source pins are in [TASK.json](TASK.json) and
+[SOURCES.json](SOURCES.json). The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241748)
+predicted a persistent delimiter; the delivered service also pays to prepare
+and erase it in one owned blank cell.
+
+## Related open work
+
+- [PR #6102](https://github.com/CrocSwap/integer-mult-bounds/pull/6102) supplies
+  the edge inverse and a counter-based logical reversal. This adds a changed
+  local tape boundary that removes its growing counter.
+- [PR #6072](https://github.com/CrocSwap/integer-mult-bounds/pull/6072) supplies
+  the graph and exact sampling law. This uses only its fixed `(1,1)` graph.
+- [PR #6096](https://github.com/CrocSwap/integer-mult-bounds/pull/6096) concerns
+  the applicability of denominator-13 sampling to actual inverse residues.
+  This service does not establish that caller applicability.
+
+- [PR #6124](https://github.com/CrocSwap/integer-mult-bounds/pull/6124) shares
+  forward graphs across parameter pairs. This machine retains the literal fixed
+  graph; the quotient's reversibility is outside this proof.
+- [PR #6068](https://github.com/CrocSwap/integer-mult-bounds/pull/6068) gives
+  finite-cap sampling obstructions. This service retains unbounded stopping.
+
+## Open next questions
+
+Can one actual nonadaptive caller supply the owned adjacent blank and stationary
+output head at the point it needs both decisions? Start with one reached residue
+pair and its tape ownership layout. The missing caller and conditionally fresh
+input randomness are the blockers; restoring consumed bits does not fund reuse.
+
+What is the explicit binary-alphabet transition constant for this fixed
+finite-control machine? Start by encoding each four-symbol cell by two bits and
+lowering every local rule while preserving head return and scratch cleanup.
+The current exact bill counts finite-alphabet two-tape steps, so the binary
+constant must be proved before comparison with a binary physical tariff.
diff --git a/research/marked-tape-ddg-reversal/RESULT.json b/research/marked-tape-ddg-reversal/RESULT.json
new file mode 100644
index 0000000000..7a95745c6c
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/RESULT.json
@@ -0,0 +1,28 @@
+{
+  "claim_type": "scoped proof with finite machine certificate",
+  "deepest_fixture": 470,
+  "expected_transitions": "48479692514343769953106/4649714690825496825793",
+  "expected_transitions_upper": "43/4",
+  "finite_control_states": 1563,
+  "head_moves": "2*T+4",
+  "marker_writes": 2,
+  "owned_delimiter_cells": 1,
+  "reverse_targets": 624,
+  "root_revisits": 942,
+  "rules": 10000,
+  "scope": "marked resident tape; fixed pair; no caller, freshness or new kappa",
+  "short_dirty_output_runs": 4088,
+  "source_sha256": {
+    "PROOF.md": "a182430c3360c6c89daa49141a9233a566fd425d1a869a4686382323c0cdaf19",
+    "machine.py": "34be31b9322fffd854ad7fec554762c1c551abebaa61650e83259da25c64db78",
+    "vendor/ORIGIN.json": "c812c46103220bdbbfef592f7112997179508597128c7b6af6a3e2750a78fa48",
+    "vendor/PROOF.reversal.md": "ed1bd5b54af0c1ab7f8208bb474bdb5e5b5ae073d62c2dad840349942caea88e",
+    "vendor/README.reversal.md": "6ca82d87d1dbaf11199419393c1782ea8ff9ff9efba1648a15c0ce65db79bb4b",
+    "vendor/README.sampler.md": "4a8d35da8cde11b127b490abdcaf0f085643313603d8b93d5773968a2e81a695",
+    "vendor/paired_sampler.py": "a3f14b87169b934489fc7d01d82ff36f6a671bc6c38e4761443f5481e36c2f63",
+    "verify.py": "f3cb2dd82c1c62ad6cf6380b6c6d8bcd32fc0ece0d6c04699917d66a136e447f"
+  },
+  "status": "PASS_MARKED_TAPE_DDG_REVERSAL",
+  "terminating_wrap_paths": 938,
+  "transitions": "3*T+4"
+}
diff --git a/research/marked-tape-ddg-reversal/SOURCES.json b/research/marked-tape-ddg-reversal/SOURCES.json
new file mode 100644
index 0000000000..79080a5d07
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/SOURCES.json
@@ -0,0 +1,53 @@
+{
+  "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/marked-tape-ddg-reversal/vendor/ORIGIN.json",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/ORIGIN.json",
+      "git_blob": "db79b8b81a00971494a0233c6fc1defa97b81bf8",
+      "sha256": "c812c46103220bdbbfef592f7112997179508597128c7b6af6a3e2750a78fa48"
+    },
+    {
+      "path": "research/marked-tape-ddg-reversal/vendor/PROOF.reversal.md",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/PROOF.reversal.md",
+      "git_blob": "05c37b0a6e2267aefda26b129c618ca376999f06",
+      "sha256": "ed1bd5b54af0c1ab7f8208bb474bdb5e5b5ae073d62c2dad840349942caea88e"
+    },
+    {
+      "path": "research/marked-tape-ddg-reversal/vendor/README.reversal.md",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/README.reversal.md",
+      "git_blob": "799f80fb0f3d1952d4107d18a1beaf8623d9fe8a",
+      "sha256": "6ca82d87d1dbaf11199419393c1782ea8ff9ff9efba1648a15c0ce65db79bb4b"
+    },
+    {
+      "path": "research/marked-tape-ddg-reversal/vendor/README.sampler.md",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/README.sampler.md",
+      "git_blob": "615c4890ec797561fd4287445ceb1019905175bc",
+      "sha256": "4a8d35da8cde11b127b490abdcaf0f085643313603d8b93d5773968a2e81a695"
+    },
+    {
+      "path": "research/marked-tape-ddg-reversal/vendor/paired_sampler.py",
+      "usage": "input",
+      "pin": "head:82b9ccab6fb6bb7a9b49b3dc48eebc0904daec84:research/marked-tape-ddg-reversal/vendor/paired_sampler.py",
+      "git_blob": "eda448fbda7b6a78f340086fcaac6e7556bf1383",
+      "sha256": "a3f14b87169b934489fc7d01d82ff36f6a671bc6c38e4761443f5481e36c2f63"
+    }
+  ]
+}
diff --git a/research/marked-tape-ddg-reversal/TASK.json b/research/marked-tape-ddg-reversal/TASK.json
new file mode 100644
index 0000000000..da7ace8e36
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/TASK.json
@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Construct a counterless local two-tape reversal of the fixed paired DDG using one owned delimiter cell.",
+  "scope_change_reason": "The card suggests proof-assistant interface formalization. This instead proves a new tape boundary and certifies its complete finite rule system, following the first open question of PR6102.",
+  "bottleneck_link": "Side interface result: removes unbounded stopping-counter allocation from one stochastic inverse service. An actual caller, randomness lifetime and full native invoice remain open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first pathwise construction with a bounded local verifier and exact tape bill; do not extend to other pairs or callers.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves arbitrary terminating paths. RESULT.json enumerates 1563 states and 10000 local rules, with 4088 short dirty-output runs and 938 terminating paths through depth470.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual nonadaptive caller supply the adjacent owned blank and stationary output head?",
+      "why_it_matters": "The local service does not establish usable native batching or conditionally fresh random input.",
+      "first_step": "Bind one reached residue pair and its random/output tape ownership layout.",
+      "blocked_by": "Actual caller placement and randomness lifetime."
+    },
+    {
+      "question": "What is the exact binary-alphabet lowering constant for this fixed machine?",
+      "why_it_matters": "Finite-alphabet transitions and native binary costs have different tariffs.",
+      "first_step": "Encode the four random and output symbols by two bits, lower every rule, and prove returned heads and scratch cleanup.",
+      "blocked_by": "A fixed binary microprogram and its complete local bill."
+    }
+  ],
+  "claim_type": "scoped proof with finite machine certificate",
+  "environment": {
+    "python": "3.12.15",
+    "dependencies": "standard library",
+    "platform": "darwin"
+  }
+}
diff --git a/research/marked-tape-ddg-reversal/VALIDATION.md b/research/marked-tape-ddg-reversal/VALIDATION.md
new file mode 100644
index 0000000000..5d5496d096
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/VALIDATION.md
@@ -0,0 +1,70 @@
+# Verification limits and implementation checks
+
+The mathematical claim and finite-alphabet cost model are in PROOF.md.
+This note records the verifier's boundaries.
+
+## Local checks
+
+CPython 3.12.15 on macOS, standard library only, passes direct isolated normal
+and optimized execution with warnings treated as errors. Their single measured
+wall times were 0.19 and 0.22 seconds. These establish replay timeout headroom,
+not a performance comparison. The registered package runs those same two
+commands with 60-second limits and passes metadata/source validation.
+
+The selected baseline initially failed because its source closure was omitted
+by sparse checkout. After materializing its 41 research roots, the unchanged
+baseline reports PASS_RESEARCH_BASELINE_BINDINGS_ONLY. This is orientation,
+not a selected scientific replay. The new package changes no selected input.
+
+The verifier executes all 10,000 local rules through finite injectivity and
+write-permission checks. Literal paths then check the new implementation's
+actual output, returned head, preserved tape, marker erasure and exact bill.
+It does not replay the predecessor's 144-pair probability/optimality census.
+The expected-cost consequence uses the cited predecessor mean.
+
+No Lean, Docker, full selected/native replay, binary-alphabet lowering, actual
+caller integration or conditional-randomness reuse was run or proved.
+No independent human or proof-kernel review is claimed.
+
+## Code constraints
+
+`machine.py` has no recursion. Every machine-building loop is bounded by the
+fixed 312-state source graph, 624 edges, 624 reverse targets or four output
+symbols. The observer accepts at most 1,024 binary fixture symbols, start offsets
+1 through 64, and at most 10,000 steps. It fails on a missing transition,
+exhausted fixture, exhausted step budget or unreturned tape/head.
+
+`verify.py` visits the 1,024 ten-bit fixtures, four output values, and 470
+compact prefix levels with at most three unfinished prefixes each. It never
+expands the full depth-470 binary tree. All new functions are at most 26 lines.
+Contracts use explicit exceptions, so optimized Python retains them. Source
+byte hashes are checked before executing the retained sampler definitions.
+The modules compile cleanly under `-W error`; ruff, mypy and pyright are not
+installed. No repository-wide analyzer configuration was changed.
+
+The following bounded deviations from low-level allocation/call restrictions
+are explicit:
+
+- Python allocates dictionary entries, tuples and observer traces dynamically.
+  The target is a finite machine description; its 10,000 rules are constructed
+  before execution. The observer's bounded fixtures and 10,000-step cap bound
+  live data. Python allocation is not claimed to implement constant physical
+  auxiliary storage. A future physical lowering must use the finite rule model.
+- Loading executes source bytes for two fixed Python modules. The retained
+  predecessor is hash-authenticated before compilation, `main` is not called,
+  and only `make(1,1)` is used. New machine bytes compile directly without
+  bytecode-cache lookup. There is no input-generated code or plugin registry.
+  The required module registration supports the frozen Trace dataclass.
+- Negative controls use fixed local lambdas. Their targets are explicit and
+  bounded. No machine rule dispatches through a Python function pointer;
+  rules contain only finite data.
+
+These deviations apply to the checking program. They do not add a stopping
+counter, Python heap, callback or absolute-address test to the machine's finite
+control. Binary gate implementation remains an open question.
+
+The internal read-only review found no blocking issue in the construction,
+proof or initial checker. It identified missing source bindings and draft
+packaging as follow-up items. RESULT.json now binds the proof, machine,
+verifier and retained sources by SHA256; the completed package passes its
+registered checks. The review does not constitute independent human acceptance.
diff --git a/research/marked-tape-ddg-reversal/VERIFY.json b/research/marked-tape-ddg-reversal/VERIFY.json
new file mode 100644
index 0000000000..1edab8df51
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/VERIFY.json
@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/marked-tape-ddg-reversal/vendor/ORIGIN.json",
+    "research/marked-tape-ddg-reversal/vendor/PROOF.reversal.md",
+    "research/marked-tape-ddg-reversal/vendor/README.reversal.md",
+    "research/marked-tape-ddg-reversal/vendor/README.sampler.md",
+    "research/marked-tape-ddg-reversal/vendor/paired_sampler.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "All generated local rules and finite states; one-step injectivity; exact per-path tape bill and output/head/delimiter cleanup; phase-wrap and failure controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Same construction and controls with optimized interpreter; required checks do not use removable assertions."
+    }
+  ]
+}
diff --git a/research/marked-tape-ddg-reversal/machine.py b/research/marked-tape-ddg-reversal/machine.py
new file mode 100644
index 0000000000..ab970cf8ad
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/machine.py
@@ -0,0 +1,110 @@
+"""Finite two-tape rules for a fixed sampler, with one owned delimiter cell.
+
+The interpreter's position and step counters are observations, never rule inputs.
+New construction produced by Nick Petalas. Apache-2.0.
+"""
+from dataclasses import dataclass
+
+PERIOD = 156
+ENTRY = ('entry', 0, 0)
+PREPARE = ('prepare', 0, 0)
+HALT = ('halt', 0, 0)
+
+
+def require(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def add_rule(rules, key, value):
+    require(key not in rules, 'duplicate rule key')
+    rules[key] = value
+
+
+def forward_rules(table, phases, rules):
+    """One right-moving step, including output XOR on a leaf edge."""
+    for state, phase in enumerate(phases):
+        for bit in (0, 1):
+            target = table[state][bit]
+            next_phase = (phase + 1) % PERIOD
+            mode = 'back' if target >= 312 else 'forward'
+            for accumulator in range(4):
+                out = accumulator ^ (target - 312) if target >= 312 else accumulator
+                key = (('forward', phase, state), bit, accumulator)
+                add_rule(rules, key, ((mode, next_phase, target), bit, out, 1))
+
+
+def reverse_rules(table, phases, rules):
+    """Move left, then apply the predecessor's phase-and-coin inverse."""
+    targets = set()
+    for state, phase in enumerate(phases):
+        for bit in (0, 1):
+            target = table[state][bit]
+            next_phase = (phase + 1) % PERIOD
+            targets.add((next_phase, target))
+            for accumulator in range(4):
+                key = (('read', next_phase, target), bit, accumulator)
+                value = (('back', phase, state), bit, accumulator, 0)
+                add_rule(rules, key, value)
+    require((0, 0) in targets, 'root must be a recurrent internal target')
+    for phase, state in sorted(targets):
+        for bit in (0, 1):
+            for accumulator in range(4):
+                key = (('back', phase, state), bit, accumulator)
+                add_rule(rules, key, (('read', phase, state), bit, accumulator, -1))
+    return len(targets)
+
+
+def build_rules(table, counts):
+    require(len(table) == 312 and len(counts) == PERIOD, 'fixed graph dimensions')
+    phases = tuple(p for p, count in enumerate(counts) for _ in range(count))
+    require(len(phases) == 312, 'phase layout')
+    rules = {}
+    forward_rules(table, phases, rules)
+    targets = reverse_rules(table, phases, rules)
+    for accumulator in range(4):
+        for bit in (0, 1):
+            add_rule(rules, (ENTRY, bit, accumulator), (PREPARE, bit, accumulator, -1))
+        add_rule(rules, (PREPARE, '_', accumulator),
+                 (('forward', 0, 0), '#', accumulator, 1))
+        add_rule(rules, (('read', 0, 0), '#', accumulator),
+                 (HALT, '_', accumulator, 1))
+    return rules, targets
+
+
+@dataclass(frozen=True)
+class Trace:
+    output: int
+    steps: int
+    head_moves: int
+    marker_writes: int
+    max_excursion: int
+    root_revisits: int
+
+
+def execute(rules, bits, accumulator=0, start=3, max_steps=4000):
+    """Bounded observer for local rules. No position or time enters a rule key."""
+    require(1 <= len(bits) <= 1024 and all(type(x) is int and x in (0, 1) for x in bits),
+            'observer binary fixture length 1..1024')
+    require(type(accumulator) is int and 0 <= accumulator < 4, 'two-bit output cell')
+    require(type(start) is int and 1 <= start <= 64, 'observer start 1..64')
+    require(type(max_steps) is int and 1 <= max_steps <= 10000, 'observer step bound')
+    tape = ['dirty'] * (start - 1) + ['_'] + list(bits)
+    initial = tuple(tape)
+    state, head, output = ENTRY, start, accumulator
+    moves = writes = excursion = revisits = 0
+    for step in range(1, max_steps + 1):
+        require(0 <= head < len(tape), 'observer fixture exhausted')
+        key = (state, tape[head], output)
+        require(key in rules, 'undefined machine transition')
+        state, symbol, output, move = rules[key]
+        writes += symbol != tape[head]
+        tape[head] = symbol
+        head += move
+        moves += abs(move)
+        excursion = max(excursion, head - start)
+        revisits += state == ('back', 0, 0) and head != start
+        if state == HALT:
+            require(head == start and tuple(tape) == initial, 'head or tape not restored')
+            return Trace(output, step, moves, writes, excursion, revisits)
+    raise ValueError('observer step bound exhausted')
diff --git a/research/marked-tape-ddg-reversal/vendor/ORIGIN.json b/research/marked-tape-ddg-reversal/vendor/ORIGIN.json
new file mode 100644
index 0000000000..db79b8b81a
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/vendor/ORIGIN.json
@@ -0,0 +1,37 @@
+{
+  "license": "Apache-2.0",
+  "files": [
+    {
+      "file": "paired_sampler.py",
+      "original_path": "research/paired-residue-sampler/verify.py",
+      "source_head": "9011bf83e85ecd0443c789cf03259442f750877d",
+      "source_author": "zxv",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/9011bf83e85ecd0443c789cf03259442f750877d/research/paired-residue-sampler/verify.py",
+      "sha256": "a3f14b87169b934489fc7d01d82ff36f6a671bc6c38e4761443f5481e36c2f63"
+    },
+    {
+      "file": "README.sampler.md",
+      "original_path": "research/paired-residue-sampler/README.md",
+      "source_head": "9011bf83e85ecd0443c789cf03259442f750877d",
+      "source_author": "zxv",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/9011bf83e85ecd0443c789cf03259442f750877d/research/paired-residue-sampler/README.md",
+      "sha256": "4a8d35da8cde11b127b490abdcaf0f085643313603d8b93d5773968a2e81a695"
+    },
+    {
+      "file": "README.reversal.md",
+      "original_path": "research/paired-ddg-reversal/README.md",
+      "source_head": "0422af13625c2e7e8ece28bdd74364a61764c64a",
+      "source_author": "JoyboyBrian",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/0422af13625c2e7e8ece28bdd74364a61764c64a/research/paired-ddg-reversal/README.md",
+      "sha256": "6ca82d87d1dbaf11199419393c1782ea8ff9ff9efba1648a15c0ce65db79bb4b"
+    },
+    {
+      "file": "PROOF.reversal.md",
+      "original_path": "research/paired-ddg-reversal/PROOF.md",
+      "source_head": "0422af13625c2e7e8ece28bdd74364a61764c64a",
+      "source_author": "JoyboyBrian",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/0422af13625c2e7e8ece28bdd74364a61764c64a/research/paired-ddg-reversal/PROOF.md",
+      "sha256": "ed1bd5b54af0c1ab7f8208bb474bdb5e5b5ae073d62c2dad840349942caea88e"
+    }
+  ]
+}
diff --git a/research/marked-tape-ddg-reversal/vendor/PROOF.reversal.md b/research/marked-tape-ddg-reversal/vendor/PROOF.reversal.md
new file mode 100644
index 0000000000..05c37b0a6e
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/vendor/PROOF.reversal.md
@@ -0,0 +1,130 @@
+# A pathwise inverse for the literal paired DDG
+
+Fix `(a,b)=(1,1)` before reading any fair bits. Use exactly `make(1,1)` in
+zxv's retained PR6072 source. It has 312 internal states `(p,j)`, phase
+`p in Z/156`, and four tagged leaves. This note proves a logical clean
+lifecycle for every **terminating** path. Probability and expected-draw
+claims reuse the predecessor's product-law/depth-count argument; no physical
+reversible machine or complete multiplier is asserted.
+
+## 1. The actual transition is locally injective when phase and bit survive
+
+At phase p let `d_i = floor(2*(w_i*2^p mod169)/169)`, for weights
+`w=(144,12,12,1)`. Every digit is 0 or1. Put `D=sum_i d_i` and
+`c_i=sum_{h<i}d_h`. For old node j and coin u, the source constructor forms
+`q=2j+u`. It returns leaf i exactly when `d_i=1` and `q=c_i`; otherwise
+it returns internal `(p+1 mod156, q-D)`.
+
+Consequently, given p,u and the target, reconstruct q by:
+
+* internal node j': `q=j'+D`, with the required next phase;
+* leaf i: require `d_i=1`, then `q=c_i`.
+
+Require `q mod2=u` and a valid old node `j=(q-u)/2`. This gives the unique
+predecessor. The source stores leaves as `312+i`; internal IDs are the
+lexicographic enumeration of `(p,j)`. The verifier checks this formula on
+all624 literal source transitions and rejects the opposite bit for each.
+No table regeneration at a neighboring residue pair is used as evidence.
+
+Phase is essential at a leaf: source states0 and1 both return leaf0 with
+coin0, but lie at phases0 and1. An overwrite retaining only leaf and coin
+is not injective. Retaining p, or deriving it from the stopping counter,
+repairs that collision. The known start phase alone does not repair it.
+
+## 2. Complete transcript/controller lifecycle
+
+Inputs are fixed parameters, an immutable binary tape, a known start cursor s,
+and a disjoint two-bit accumulator A. The tape is initially independent fair
+bits for the exact product-law assertion. Pathwise reversibility itself holds
+for every binary tape having a finite terminating prefix. The caller owns
+that resident transcript until cleanup ends; no tape cell is overwritten.
+
+Owned call registers begin `(state,phase,t,cursor)=(0,0,0,s)` plus clean
+scratch. A forward step reads the current tape bit u, performs the source
+transition, increments phase modulo156, increments t, and moves cursor right.
+The loop ends on its first leaf `312+i`, at random stopping time T. Thus
+`phase=T mod156`, `t=T`, `cursor=s+T`.
+
+Perform reversible output retention `A <- A XOR i`. The leaf remains in the
+controller during this copy; the accumulator is not the sole cleanup record.
+Then, while t>0, read the bit at cursor-1, decrement phase modulo156, and apply
+the inverse from section1 to the current target and that predecessor phase.
+Move the cursor left and decrement t. The forward relation checks that the
+computed predecessor regenerates the target, enabling scratch uncomputation.
+
+Induction backwards on t recovers the exact preceding controller on each
+step. At t=0 it returns `(state,phase,t,cursor)=(0,0,0,s)`, with scratch clean,
+tape unchanged and accumulator `A_initial XOR i`. Both the stopping counter
+and owned phase register are cleared by this reverse walk. There is no
+per-step state history and no retained final T. Storage of the counter during
+the call is still necessary in this construction. Never stop reversal merely
+on seeing state0: a surviving path can revisit phase0/root after156 steps.
+The counter distinguishes that visit from the beginning. Phase wrap does not
+invalidate the inverse formula or its induction.
+
+To realize a single state update reversibly, compute the next state into a
+clean nine-bit scratch register using an XOR oracle, swap state and scratch,
+and erase the old state with the inverse XOR oracle while phase and coin are
+still available. Reverse the two oracles for a backward step. Counter,
+phase and cursor updates are invertible increments/decrements. The table
+oracles extend to total reversible XOR maps, but cleanup correctness and loop
+termination are claimed on the valid-path invariant only. The Python verifier
+is an exact reference interpreter, not itself a bit-level reversible circuit.
+
+## 3. Costs that this construction does and does not pay
+
+The chosen realization keeps nine state bits, nine scratch bits, eight phase
+bits, O(1) bounded lookup/work flags, and `ceil(log2(T+1))` stopping-counter
+bits at maximum occupancy. The cursor and known start address belong to the
+tape interface; a numerical address implementation must additionally pay its
+address storage/arithmetic. The consumed T bits remain resident throughout;
+no new per-step state log is stored. There is no finite worst-case T or
+worst-case storage bound. Counter allocation itself is a physical obligation;
+the space expression describes occupied logical bits, not a free allocator.
+
+Precisely T forward and T reverse transitions and one two-bit XOR retention
+are required, with 2T accesses to the resident transcript. There are T cursor
+moves in each direction. From the retained source,
+
+`E[T]=9960277917013927549978/4649714690825496825793 < 9/4`.
+
+Thus expected traversed transitions are `2E[T] < 9/2`; cleanup doubles the
+logical traversal count but draws **no new randomness**. It does not make the
+T used random bits independent of the retained result.
+
+An explicit conditional implementation can scan every one of the624 edge
+records for each oracle, XORing the target or predecessor under equality of
+its key. Store source phase alongside each record (or compute it with a paid
+fixed decoder). At most two scans implement each reversible state transition,
+so forward-plus-reverse uses **2496T record visits**. This is a deliberately
+conservative concrete lookup tariff, not a free RAM assumption. It requires
+paid reversible equality/XOR/scan movement at the fixed record widths. The
+original5616-bit packed target table does not include these phase records,
+scan positioning machinery, or controller scratch: storing an eight-bit phase
+per edge adds4992 bits in this simple layout, for10548 data bits total, before
+any physical routing/control overhead.
+
+If a record visit costs K and counter update at occupied length ell costs
+C(ell), the additional conditional bill is `2496KT + O(T*C(log(T+1)))`
+plus tape movement, addressing, phase updates and one output copy. With a paid
+ripple-style increment/decrement tariff C(ell)=O(ell), counter work is
+O(T log(T+1)); this is not charged as constant time. The source bound
+`Pr(T>k)<=3/2^k` ensures finite expectation for that polynomial-logical work,
+but a bounded physical tariff is not supplied by the Python experiment.
+No runtime speedup follows from expected fair-bit savings alone.
+
+## 4. Quantifiers and remaining boundaries
+
+The inverse algebra applies to any binary-digit DDG with this same ordered
+leaf allocation, subject to its valid-node recurrence. The source binding,
+resource counts, path fixtures and exact mean here cover only `(1,1)`;
+all144 denominator13 configurations are deliberately not replayed.
+
+A fresh call after this cleanup may not treat the restored consumed bits as
+fresh conditional randomness once the output is retained or used adaptively.
+The proof restores the original tape, not its independence from outputs.
+Actual reached residue pairs, nonadaptive batching, overflow, table selection,
+physical random-bit/tape service and outer error bounds remain open. No
+selected frontier, deterministic inverse, supplier admission or framework
+assumption is changed. No formal proof-kernel or independent human review is
+claimed.
diff --git a/research/marked-tape-ddg-reversal/vendor/README.reversal.md b/research/marked-tape-ddg-reversal/vendor/README.reversal.md
new file mode 100644
index 0000000000..799f80fb0f
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/vendor/README.reversal.md
@@ -0,0 +1,94 @@
+# Reverse the literal paired DDG without a visited-state log
+
+For the fixed `(1,1)` denominator13 pair in [zxv's PR6072](https://github.com/CrocSwap/integer-mult-bounds/pull/6072),
+the actual312-state DDG has a unique inverse edge when the consumed coin and
+predecessor phase are retained. This package supplies that inverse and a
+pathwise output-copy/cleanup protocol: retain the two-bit output in a disjoint
+XOR accumulator, restore the original tape cursor, clear the controller and
+stopping counter, and leave the resident input tape unchanged. **No per-step
+node history is required; the stopping counter and transcript are required.**
+
+The source-bound result is logical reversibility on every terminating path,
+not a physical sampler, fixed worst-case storage, freshness after output
+retention, or a speedup. The input pair must be fixed before sampling. The
+selected frontier and its five framework assumptions remain unchanged.
+
+## What changed
+
+PR6072 proves the exact product law and optimal expected fair-bit count while
+leaving reversal and stopping records open. Its source leaf overwrite loses
+phase: literal states0 and1 both return leaf0 on coin0. Keeping phase (or
+deriving it from the stopping count) resolves that collision. The inverse
+formula uses `q=next_node+sum(digits)` for an internal child, or the leaf's
+unique digit slot for a leaf, and recovers old node `(q-bit)/2`.
+[PROOF.md](PROOF.md) gives the full arbitrary-path induction, counter/phase
+wrap, output retention and conditional physical bill. This is a refined
+`formal-interface-lemma` task, proved in prose with exact executable source
+bindings, without a formal proof assistant.
+
+The protocol performs T forward and T reverse transitions, using the same T
+resident transcript bits. It uses O(log(T+1)) controller/counter storage beyond
+fixed table/scratch and the transcript; T remains unbounded. For this source
+pair, expected traversed transitions are exactly twice
+`9960277917013927549978/4649714690825496825793`.
+An explicit scan implementation charges2496T fixed-record visits plus counter,
+phase, addressing and tape costs. The source's702-byte table is not claimed
+to include that implementation's extra phase records or machinery.
+
+## Exact retained sources and credit
+
+`vendor/paired_sampler.py` and `vendor/README.source.md` retain byte-for-byte
+PR6072 head`9011bf83e85ecd0443c789cf03259442f750877d`, by zxv with substantial
+OpenAI Codex assistance, Apache-2.0. [vendor/ORIGIN.json](vendor/ORIGIN.json)
+records their original paths and hashes. Only `make(1,1)` is invoked; its
+144-pair `main` is never called. These retained files have their own commit in
+this branch and source pins refer to that reachable retention commit, so cold
+replay does not depend on an unmerged external Git object. No synthetic history
+merge or predecessor modification is used.
+
+The classical DDG method, predecessor proof and their credits remain in the
+retained README. JoyboyBrian, with substantial OpenAI Codex assistance,
+prepared this scoped inverse/protocol and verifier. Apache-2.0. Nick Petalas's
+stochastic-prefix context and the JoyboyBrian#5069/#5037 inverse lineage retain
+credit; their scientific replays are not imported or repeated here.
+
+## Evidence and reproduction
+
+```sh
+python3 -I -W error -B research/paired-ddg-reversal/verify.py
+python3 -I -W error -O -B research/paired-ddg-reversal/verify.py
+python3 -B scripts/research_package.py --package research/paired-ddg-reversal
+python3 -B scripts/check_research_commit.py --package research/paired-ddg-reversal --check-source-history
+```
+
+The standard-library verifier checks all624 inverse edges and624 wrong-bit
+rejections,1022 terminating literal ten-bit tapes at a nonzero cursor with all
+four accumulator values, and315 terminating paths through one/two phase wraps
+up to T=314. It also rejects wrong counter, cursor, phase and output labels,
+a finite surviving tape, and records the concrete phase-free collision.
+The bounded paths validate implementation and failure controls; the arbitrary
+terminating-path claim follows from the written edge-inverse induction.
+No Monte Carlo or full historical catalogue replay is used. Direct verification
+is read-only and Git-free once this package is exported. Registered commands
+exercise normal and optimized modes; explicit checks remain active in both.
+
+Canonical base is`721c03822c421b7f7fcbb2598993b947c4d88419`, priority8.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/6073#discussioncomment-19234412)
+sets this exact task. Root coordination searched355 open PRs,5737 Discussions
+and8348 local records on2026-10-28 UTC; coverage is not proof of novelty.
+The public PR6072 head was rechecked before implementation. Later pair selection
+belongs to another task; this package does not search for an actual caller.
+
+## Open next questions
+
+Can one physical tape/table service implement the explicit scans, counter
+allocation and cursor restoration with a complete uniform tariff? Begin with
+one fixed `(1,1)` service and the2496T record-visit bill in the proof, retaining
+address movement and unbounded stopping. The physical service is the blocker.
+
+Can an actual caller supply a nonadaptive pair and independent input tape
+conditional on its retained outputs? Bind one stage and its randomness lifetime
+before reusing the cleaned transcript. This proof restores bits but does not
+restore their independence from the retained sampled decision.
+Structured questions are in TASK.json. No new kappa or full multiplication
+theorem, independent human approval, Lean or Docker result is claimed.
diff --git a/research/marked-tape-ddg-reversal/vendor/README.sampler.md b/research/marked-tape-ddg-reversal/vendor/README.sampler.md
new file mode 100644
index 0000000000..615c4890ec
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/vendor/README.sampler.md
@@ -0,0 +1,188 @@
+# Joint denominator-13 decisions use fewer expected fair bits
+
+For every fixed pair of nonzero residue probabilities $a/13,b/13$, an explicit
+finite-state sampler produces **two independent** Bernoulli decisions with
+optimal expected fair-bit count strictly below $7/2$. Two separate exact
+standalone samplers require expected count at least four. When both probabilities
+are $1/13$, the joint expected count is below $9/4$, saving more than 43.75% of
+the standalone expected draws.
+
+Each parameter pair has exactly 312 internal control states and 624 binary
+transitions. Including its four output labels, every target fits nine bits;
+a packed transition table uses 5,616 bits, or 702 bytes, per parameter pair.
+The implementation generates one table at a time rather than storing all 144.
+
+This is a finite exact sampling construction and an expected-bit optimum,
+not a physical inverse, worst-case latency bound, reversible cleanup protocol,
+supplier or new κ. It deliberately changes the **standalone-call** hypothesis
+of [PR #6068](https://github.com/CrocSwap/integer-mult-bounds/pull/6068).
+The underlying dyadic decision-graph method is classical; the contribution is
+this small complete denominator-13 catalogue, exact means and resource ledger.
+
+## Contract and source relevance
+
+The denominator-13 inverse in
+[PR #5069](https://github.com/CrocSwap/integer-mult-bounds/pull/5069) motivates
+rounding probabilities with this denominator. Both probabilities must be known
+**before** this sampler consumes any bits. Their intended decisions are
+independent. A second probability that depends on the first rounded result
+cannot be substituted into this batch without a new contract.
+
+No actual native caller is asserted to provide the required residue pair or
+batching window. The retained deterministic inverse is not alleged defective.
+The stochastic prefix of
+[Nick Petalas](https://github.com/petalas)'s
+[PR #6026](https://github.com/CrocSwap/integer-mult-bounds/pull/6026) supplies a
+related arithmetic context, but its adaptive updates are not automatically
+batchable, and its native/caller error analysis is not extended here.
+
+## Exact joint decision graph
+
+In output order 00, 01, 10, 11, set the integer weights
+
+$$
+(w_0,w_1,w_2,w_3)
+=((13-a)(13-b),(13-a)b,a(13-b),ab).
+$$
+
+Their sum is 169. Dividing by 169 gives exactly the product law, hence the
+required independent marginals. Write the binary digits of each probability
+as $d_{i,k}$ at depth $k\geq1$. Define
+
+$$
+n_k=2^k-\sum_{i=0}^3\lfloor2^k w_i/169\rfloor.
+$$
+
+This is the number of unfinished binary prefixes after depth $k$. At the root,
+$n_0=1$. At the next depth, double every unfinished node, label the first
+$d_{i,k}$ available children with output $i$, and retain the rest as unfinished.
+Each digit is zero or one, and
+
+$$
+n_k=2n_{k-1}-\sum_i d_{i,k}.
+$$
+
+Thus this rule never overfills a level. An executable version stores the
+unfinished-node index $j$: after drawing one bit $u$, set $j\leftarrow2j+u$,
+then subtract the four probability digits in output order. The first subtraction
+making $j$ negative returns that output; otherwise the remaining $j$ is the
+next unfinished-node index. All four digits come from exact residue doubling
+modulo 169.
+
+By induction, the completed output-$i$ prefixes at depth $k$ number exactly
+$\lfloor2^k w_i/169\rfloor$. Since $1\leq n_k\leq3$, unfinished probability
+is at most $3/2^k$, tending to zero. The resulting output law is therefore
+exactly $w_i/169$, not an approximation from finite samples.
+
+## Finite periodic controller and exact expected cost
+
+The order of two modulo 169 is 156; replay checks this with exact integer
+powers. Every weight is coprime to 13, so its residue sequence is periodic
+with that period. The digits and unfinished-node counts repeat. There are
+exactly 312 internal phase/node pairs for every one of the 144 residue pairs;
+this finite count is checked exhaustively. Two transitions per state give the
+624-entry table. No growing arithmetic precision is needed to represent the
+sampler's logical control state, although its random tape and stopping length
+have no finite worst-case bound.
+
+The exact expected draw count is
+
+$$
+E[T]=\frac{\sum_{k=0}^{155} n_k2^{-k}}{1-2^{-156}}.
+$$
+
+For $(a,b)=(1,1)$ this is
+
+$$
+E[T]=\frac{9960277917013927549978}{4649714690825496825793}<\frac94.
+$$
+
+The exact finite catalogue certifies $2<E[T]<7/2$ for all 144 nonzero residue
+pairs. These numerical bounds and state counts are finite certificates; the
+construction, law and expected-cost formula have the preceding written proof.
+No floating-point logarithms or Monte Carlo estimates are used.
+
+## Optimality and the changed standalone hypothesis
+
+For any exact fair-bit decision tree with these four output probabilities,
+completed output-$i$ mass after $k$ bits is an integer multiple of $2^{-k}$
+and cannot exceed $w_i/169$. Its completed prefix count is therefore at most
+$\lfloor2^k w_i/169\rfloor$. Its unfinished probability is at least $n_k/2^k$.
+Summing these tail bounds proves that its expected draw count is at least the
+displayed formula. This sampler saturates every depth bound, so it is optimal
+for the stated fixed joint law, with no free initial random state.
+
+A standalone non-dyadic Bernoulli sampler must leave at least one fair prefix
+unfinished at every depth, giving expectation at least two. Separate calls
+without a shared entropy reservoir therefore require at least four draws in
+expectation. The joint four-outcome tree changes that boundary; it preserves
+independence of the **decisions**, without requiring separately executed
+sampling trees. Reusing a single sampled flag for both decisions would have
+the right marginals but the wrong joint law and is rejected by a control.
+
+The sampler still has a positive unfinished probability at every finite depth.
+It chooses the unbounded-stopping option in #6068's tradeoff, not an escape
+from that worst-case theorem. A finite control table is not a finite draw cap.
+
+## Costs and unproved physical obligations
+
+The logical sampler performs one table transition per consumed fair bit, then
+returns one two-bit outcome. Per-configuration packed table storage is 702
+bytes and control needs nine bits including output labels. Selecting or building
+the table from actual data residues, table access, random-bit movement, output
+storage, stopping-record retention and reversible cleanup are additional costs.
+The returned decisions are correlated with the consumed tape, so that tape is
+not automatically a fresh reusable random resource.
+
+No source-bound physical batching window, all-column primitive, deterministic
+tariff, compiler or outer error budget is supplied. The expected bit reduction
+must not be read as a runtime speedup or an admitted exponent improvement.
+
+## Evidence and reproduction
+
+```
+python3.12 -B scripts/research_package.py --package research/paired-residue-sampler
+python3.12 -B scripts/check_research_commit.py --package research/paired-residue-sampler
+```
+
+The standard-library verifier constructs every table, checks the complete
+outcome-prefix counts for two full 156-step periods, independently enumerates
+36,864 literal eight-bit tapes, certifies the exact expected counts and resource
+bounds, and rejects corrupted output labels and false independence/latency
+claims. Normal and optimized modes write no package files. Universal probability
+and optimality come from the written depth-count argument, not the literal tapes.
+
+Canonical main was refreshed on 2026-10-28 UTC at
+721c03822c421b7f7fcbb2598993b947c4d88419, priority 8. The navigation-only repair
+from [PR #6050](https://github.com/CrocSwap/integer-mult-bounds/pull/6050) is
+included. The optional full-history check is unavailable in this shallow checkout;
+source pins use its reachable base. No selected/native cold replay, independent
+human review or formal-kernel acceptance is claimed. Frozen sources stay unchanged.
+
+## Significance for researchers
+
+The standalone two-draw lower bound is not a per-scalar amortized limit. A small
+joint interface can reduce expected randomness while preserving the exact
+independent rounding law. This supplies a concrete batching target and exposes
+the next obligation: an actual nonadaptive residue pair and a full hosting and
+cleanup bill, rather than free entropy or a claimed bounded-time sampler.
+
+## Open next questions
+
+Does one actual inverse-service stage expose two residue probabilities before
+either output is consumed? First bind that data-dependence and timing boundary,
+then price table selection, access and random-tape cleanup. No such caller is
+instantiated here.
+
+Can the table be shared or parameterized across residue pairs with less total
+physical control cost? Start with two configurations and an explicit dispatcher
+that preserves the joint law. A lower expected bit count alone does not fund it.
+
+## Credit
+
+Prepared by [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance.
+The dyadic distribution-generation tree and depth-count optimality argument are
+classical and not claimed as new. [JoyboyBrian](https://github.com/JoyboyBrian)'s
+#5069/#5037 lineage supplies the inverse context;
+[Nick Petalas](https://github.com/petalas)'s #6026 supplies the stochastic-prefix
+context. Their sources and attribution remain unchanged. Apache-2.0.
diff --git a/research/marked-tape-ddg-reversal/vendor/paired_sampler.py b/research/marked-tape-ddg-reversal/vendor/paired_sampler.py
new file mode 100644
index 0000000000..eda448fbda
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/vendor/paired_sampler.py
@@ -0,0 +1,121 @@
+"""Exact periodic DDG samplers for paired denominator-13 decisions. Apache-2.0."""
+from fractions import Fraction as Q
+from itertools import product
+from pathlib import Path
+import hashlib
+import json
+
+HERE=Path(__file__).resolve().parent
+ROOT=HERE.parents[1]
+DEN=169
+PERIOD=156
+
+
+def need(ok,msg):
+    if not ok:raise ValueError(msg)
+
+
+def make(a,b):
+    need(type(a) is int and type(b) is int and 1<=a<=12 and 1<=b<=12,'nonzero residue pair')
+    weights=((13-a)*(13-b),(13-a)*b,a*(13-b),a*b)
+    need(sum(weights)==DEN,'joint mass')
+    need(weights[2]+weights[3]==13*a and weights[1]+weights[3]==13*b,'marginals')
+    need(weights[0]*weights[3]==weights[1]*weights[2],'independence')
+    residues=[tuple(w*pow(2,k,DEN)%DEN for w in weights) for k in range(PERIOD)]
+    counts=[sum(row)//DEN for row in residues]
+    need(all(sum(row)%DEN==0 and 1<=n<=3 for row,n in zip(residues,counts)),'unresolved nodes')
+    states=[(k,j) for k,n in enumerate(counts) for j in range(n)]
+    need(len(states)==312,'finite internal states')
+    ids={s:i for i,s in enumerate(states)};table=[]
+    for phase,node in states:
+        digits=tuple(2*r//DEN for r in residues[phase]);row=[]
+        for bit in (0,1):
+            j=2*node+bit;target=None
+            for out,digit in enumerate(digits):
+                j-=digit
+                if j<0:target=312+out;break
+            if target is None:
+                target=ids.get(((phase+1)%PERIOD,j))
+                need(target is not None,'valid remaining node')
+            row.append(target)
+        table.append(tuple(row))
+    mean=sum((Q(n,1<<k) for k,n in enumerate(counts)),Q(0))/(1-Q(1,1<<PERIOD))
+    return weights,counts,table,mean
+
+
+def census(table,weights,depth):
+    need(len(table)==312 and all(len(row)==2 and all(type(t) is int and 0<=t<316 for t in row) for row in table),'table domain')
+    active={0:1};done=[0]*4
+    for k in range(1,depth+1):
+        done=[2*n for n in done];nxt={}
+        for state,n in active.items():
+            for target in table[state]:
+                if target>=312:done[target-312]+=n
+                else:nxt[target]=nxt.get(target,0)+n
+        active=nxt
+        need(done==[w*(1<<k)//DEN for w in weights],'complete outcome-prefix counts')
+        need(sum(active.values())+(sum(done))==1<<k,'complete fair-prefix mass')
+        need(all(n==1 for n in active.values()) and 1<=len(active)<=3,'unresolved-prefix structure')
+    return tuple(done),sum(active.values())
+
+
+def run(table,bits):
+    state=0
+    for used,bit in enumerate(bits,1):
+        target=table[state][bit]
+        if target>=312:return target-312,used
+        state=target
+    return None,len(bits)
+
+
+def rejected(fn):
+    try:fn()
+    except ValueError:return
+    raise ValueError('negative control accepted')
+
+
+def main():
+    pins=json.loads((HERE/'SOURCES.json').read_text())
+    for row in pins['files']:
+        if row['usage']=='input':
+            need(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'source bytes')
+    need(pow(2,PERIOD,DEN)==1 and all(pow(2,k,DEN)!=1 for k in range(1,PERIOD)),'exact binary period')
+    maximum=Q(0);minimum=Q(4);cases=literal=0
+    for a,b in product(range(1,13),repeat=2):
+        weights,counts,table,mean=make(a,b)
+        census(table,weights,2*PERIOD)
+        need(2<mean<Q(7,2),'certified paired expected cost')
+        need(len(table)*2==624 and max(max(row) for row in table)<512,'nine-bit table targets')
+        if (a,b)==(1,1):need(mean<Q(9,4),'strict two-small-residue gain')
+        maximum=max(maximum,mean);minimum=min(minimum,mean)
+        observed=[0]*4;left=0
+        for bits in product((0,1),repeat=8):
+            out,used=run(table,bits)
+            if out is None:left+=1
+            else:observed[out]+=1
+            need(1<=used<=8,'bounded finite-tape test');literal+=1
+        want=census(table,weights,8)
+        need((tuple(observed),left)==want,'independent literal-tape oracle')
+        cases+=1
+    weights,counts,table,mean=make(1,1)
+    need(mean==Q(9960277917013927549978,4649714690825496825793),'exact displayed pair mean')
+    need(census(table,weights,PERIOD)[1]==1,'positive survival at one whole period')
+    bad=list(table)
+    for i,row in enumerate(bad):
+        if 315 in row:
+            bad[i]=tuple(312 if t==315 else t for t in row);break
+    rejected(lambda:census(bad,weights,PERIOD))
+    rejected(lambda:make(0,1))
+    rejected(lambda:make(1,13))
+    rejected(lambda:need(mean>=4,'false additivity of standalone lower bounds'))
+    rejected(lambda:need(mean<=2,'understated joint mean'))
+    rejected(lambda:need(census(table,weights,PERIOD)[1]==0,'false finite draw cap'))
+    need(Q(1,13)!=Q(1,169),'reused single flag violates independent joint law')
+    print(json.dumps(dict(status='PASS_PAIRED_RESIDUE_SAMPLER',residue_pairs=cases,
+                         internal_states=312,transitions_per_pair=624,depths_checked_per_pair=312,
+                         literal_tapes=literal,mean_one_one=str(mean),maximum_mean=str(maximum),
+                         minimum_mean=str(minimum),
+                         scope='optimal expected fair-bit count for a fixed nonadaptive pair; physical costs open; no new kappa'),sort_keys=True))
+
+
+if __name__=='__main__':main()
diff --git a/research/marked-tape-ddg-reversal/verify.py b/research/marked-tape-ddg-reversal/verify.py
new file mode 100644
index 0000000000..5e46534753
--- /dev/null
+++ b/research/marked-tape-ddg-reversal/verify.py
@@ -0,0 +1,171 @@
+"""Check the new finite tape machine, without replaying predecessor sampling claims."""
+from collections import Counter
+from fractions import Fraction
+from hashlib import sha256
+from itertools import product
+import argparse
+import json
+from pathlib import Path
+import sys
+
+HERE = Path(__file__).resolve().parent
+# Run precisely these source bytes, without consulting bytecode caches.
+# dataclasses resolves its defining module through sys.modules.
+import types
+module = types.ModuleType('marked_tape_machine')
+sys.modules[module.__name__] = module
+exec(compile((HERE / 'machine.py').read_bytes(), str(HERE / 'machine.py'), 'exec'), module.__dict__)
+require = module.require
+
+
+def load_sampler():
+    origin = json.loads((HERE / 'vendor/ORIGIN.json').read_text())
+    for row in origin['files']:
+        raw = (HERE / 'vendor' / row['file']).read_bytes()
+        require(sha256(raw).hexdigest() == row['sha256'], 'retained source bytes changed')
+    path = HERE / 'vendor/paired_sampler.py'
+    raw = path.read_bytes()
+    scope = {'__name__': 'retained_sampler_definitions', '__file__': str(path)}
+    exec(compile(raw, str(path), 'exec'), scope)
+    return scope['make'](1, 1)
+
+
+def rejected(fn):
+    try:
+        fn()
+    except ValueError:
+        return
+    raise ValueError('negative control accepted')
+
+
+def check_local_injectivity(rules):
+    """Check global one-step injectivity using the destination head displacement."""
+    incoming = {}
+    for (control, symbol, accumulator), (target, written, out, move) in rules.items():
+        require(symbol == written or (symbol, written) in (('_', '#'), ('#', '_')),
+                'random data must be immutable')
+        require(move in (-1, 0, 1), 'local head motion')
+        # Each destination control has one incoming direction. The prior cell
+        # is therefore known, so written symbol and output determine a unique key.
+        if target in incoming:
+            require(incoming[target] == move, 'destination has inconsistent incoming direction')
+        incoming[target] = move
+    images = Counter((target, written, out) for target, written, out, _ in rules.values())
+    require(max(images.values()) == 1, 'one-step machine is not injective')
+    return len(incoming)
+
+
+def one_path(rules, bits, output, depth, accumulator=0, start=3):
+    trace = module.execute(rules, bits, accumulator, start)
+    require(trace.output == accumulator ^ output, 'wrong dirty output XOR')
+    require(trace.steps == 3 * depth + 4, 'wrong exact transition tariff')
+    require(trace.head_moves == 2 * depth + 4, 'wrong exact tape travel')
+    require(trace.marker_writes == 2 and trace.max_excursion == depth, 'marker or excursion')
+    return trace
+
+
+def short_paths(rules, table):
+    total = 0
+    for bits in product((0, 1), repeat=10):
+        state, result = 0, None
+        for depth, bit in enumerate(bits[:9], 1):
+            state = table[state][bit]
+            if state >= 312:
+                result = (state - 312, depth)
+                break
+        if result is None:
+            continue
+        for accumulator in range(4):
+            one_path(rules, bits, *result, accumulator=accumulator, start=1 + total % 7)
+            total += 1
+    return total
+
+
+def wrap_paths(rules, table):
+    """Enumerate every surviving prefix compactly, then each terminating edge."""
+    active = [(0, ())]
+    paths = revisits = deepest = 0
+    wrapped_fixture = None
+    for depth in range(1, 471):
+        nxt = []
+        for state, prefix in active:
+            for bit in (0, 1):
+                target = table[state][bit]
+                bits = prefix + (bit,)
+                if target >= 312:
+                    trace = one_path(rules, bits + (0,), target - 312, depth)
+                    revisits += trace.root_revisits
+                    if trace.root_revisits:
+                        wrapped_fixture = (bits + (0,), target - 312, depth)
+                    deepest = max(deepest, depth)
+                    paths += 1
+                else:
+                    nxt.append((target, bits))
+        require(len(nxt) <= 3, 'fixture worklist capacity exceeded')
+        active = nxt
+    require(wrapped_fixture is not None, 'missing wrapped fixture')
+    return paths, revisits, deepest, active[0][1], wrapped_fixture
+
+
+def controls(rules):
+    # A one-bit termination exists on coin zero, with a guard bit afterwards.
+    rejected(lambda: one_path(rules, (0, 1), 1, 1))
+    rejected(lambda: module.execute(rules, (0,)))
+    rejected(lambda: module.execute(rules, (0, 1), max_steps=1))
+    rejected(lambda: module.execute(rules, (2, 1)))
+    rejected(lambda: module.execute(rules, (0, 1), accumulator=4))
+    bad = dict(rules)
+    del bad[(('read', 0, 0), '#', 0)]
+    rejected(lambda: module.execute(bad, (0, 1)))
+    # A wrapped root must continue left instead of declaring early completion.
+    bad = dict(rules)
+    for bit in (0, 1):
+        bad[(('back', 0, 0), bit, 0)] = (module.HALT, bit, 0, 0)
+    return bad
+
+
+def compute():
+    _, counts, table, mean = load_sampler()
+    rules, targets = module.build_rules(table, counts)
+    destinations = check_local_injectivity(rules)
+    states = {key[0] for key in rules} | {value[0] for value in rules.values()}
+    require(destinations == len(states) - 1, 'entry must be the only source-only control')
+    short = short_paths(rules, table)
+    wrapped, revisits, deepest, survivor, wrap_fixture = wrap_paths(rules, table)
+    bad = controls(rules)
+    bits, output, depth = wrap_fixture
+    rejected(lambda: one_path(bad, bits, output, depth))
+    rejected(lambda: module.execute(rules, survivor + (0,), max_steps=100))
+    require((len(rules), len(states), targets) == (10000, 1563, 624), 'machine inventory')
+    expected = 3 * mean + 4  # The predecessor expectation is cited, not rederived.
+    require(expected < Fraction(43, 4), 'expected transition consequence')
+    bound_files = ['machine.py', 'verify.py', 'PROOF.md', 'vendor/ORIGIN.json']
+    bound_files += ['vendor/' + row['file'] for row in
+                    json.loads((HERE / 'vendor/ORIGIN.json').read_text())['files']]
+    hashes = {name: sha256((HERE / name).read_bytes()).hexdigest() for name in bound_files}
+    return dict(status='PASS_MARKED_TAPE_DDG_REVERSAL', source_sha256=hashes, rules=len(rules),
+                finite_control_states=len(states), reverse_targets=targets,
+                short_dirty_output_runs=short, terminating_wrap_paths=wrapped,
+                root_revisits=revisits, deepest_fixture=deepest,
+                transitions='3*T+4', head_moves='2*T+4', owned_delimiter_cells=1,
+                marker_writes=2, expected_transitions=str(expected),
+                expected_transitions_upper='43/4',
+                claim_type='scoped proof with finite machine certificate',
+                scope='marked resident tape; fixed pair; no caller, freshness or new kappa')
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--write-result', type=Path)
+    args = parser.parse_args()
+    result = compute()
+    encoded = json.dumps(result, indent=2, sort_keys=True) + '\n'
+    if args.write_result:
+        args.write_result.write_text(encoded)
+    else:
+        require(json.loads((HERE / 'RESULT.json').read_text()) == result, 'stored result changed')
+    print(encoded, end='')
+
+
+if __name__ == '__main__':
+    main()