diff --git a/research/binary-distance-continuations/PROOF.md b/research/binary-distance-continuations/PROOF.md
new file mode 100644
index 0000000000..61df1236a5
--- /dev/null
+++ b/research/binary-distance-continuations/PROOF.md
@@ -0,0 +1,202 @@
+# Binary head-distance continuation frames
+
+New construction and proof produced by Nick Petalas. Apache-2.0.
+
+## Statement and exact contract
+
+Use Mihir Srivastava's PR #5364 local segment contract, retained at
+`fd74da128f0e5ab702a8fe7b2b00e1a316bb22ad`. There are sixteen disjoint payload
+tapes, a control tape, a descriptor tape and reverse scratch. The same nine
+symbols suffice. Each parent payload is an arbitrary contiguous binary word
+of length s_i after its local marker, with head at h_i in [0,s_i]. Let
+H_i=s_i-h_i, H=sum H_i, L=sum bitlength(H_i) and P=sum popcount(H_i), with
+bitlength(0)=0. A fixed sixteen-bit mask records presence. Absent roles are
+empty, but a present role may be empty. The opaque binary descriptor has
+length d and starts at its local beginning. Control is at its blank top;
+scratch is blank at its local beginning. Ancestor prefixes are arbitrary and
+inaccessible. Markers and tape identities are supplied entry conditions.
+
+The new push/pop construction has exactly the predecessor's restoration
+postcondition, for every finite properly nested successful call tree. Its
+control frame has exactly
+
+    d + 35 + L
+
+symbols, instead of the predecessor's d+35+H. Scratch needs at most
+max(d, max_i bitlength(H_i)) working symbols across a matched boundary.
+Scratch is empty at every child entry and parent return. During nested
+execution the same physical scratch tape is reused, so its historical extent
+is the maximum over frames, not a sum over active frames. Parent payload
+extents and their historical backing are unchanged by this result.
+The scratch interval includes its marker and the terminal blank in addition
+to the stated number of working symbols, so it has at most that maximum
+plus two cells. Erasure does not deallocate any visited cell.
+
+Let the seventeen child words, including its descriptor, have lengths t_j
+and return head offsets g_j in [0,t_j]. Put W=sum t_j and G=sum g_j. Counting
+each read, write and unit move separately, the complete matched boundary is
+exactly
+
+    22d + 24H - 10P + 22L + 613 + 2G + 5W.             (1)
+
+It is therefore at most
+
+    22d + 46H + 613 + 7W.                              (2)
+
+The action bound includes all child and scratch erasure. Child computation,
+descriptor production and designated output delivery have separate costs.
+Intended output must be delivered before destructive pop, as in #5364.
+There is a larger linear action constant in exchange for smaller headers.
+This is a local constructive refinement, not a new whole-caller allocation,
+binary compilation, supplier admission, exponent saving or multiplication
+theorem. No global tape-reserve improvement follows without rebinding the
+actual caller and accounting for all payload and historical extents.
+
+## Binary counter with finite control
+
+The counter is little endian on reverse scratch, immediately after its local
+marker. It starts as an empty word representing zero. For each physical step
+right while parking a payload head, increment it by changing the initial run
+of ones to zeros and the next zero or blank to one, then rewind to the local
+marker and step right. This stores the number of actual head movements;
+no numeric payload offset, length or saved pointer is controller state.
+
+If an increment crosses t trailing ones, its cost is 3t for their
+read/write/move actions, two actions for the final read/write, and 2t+3
+for rewind. Thus it costs 5t+5. Among the first h increments from zero,
+the sum of trailing-one counts is
+
+    sum_{a>=1} floor(h/2^a) = h-popcount(h).
+
+The sum counts each carry across each bit position exactly once. Hence the
+complete increment cost is 10h-5popcount(h). The counter never exceeds
+bitlength(h) cells.
+
+After parking, scan the counter to its terminal blank, then read it
+backward. Emit each bit to control, most significant first, encoding zero
+as `u` and one as `:`. Erase each counter bit as it is read, and return to
+its local beginning. For ell counter bits, the forward scan costs 2ell+1,
+the backward transfers cost 6ell, and the final marker return costs three.
+The exact transfer cost is 8ell+4, including the empty counter.
+
+The frame grammar is
+
+    [ descriptor : b_0 B(H_0) ; ... b_15 B(H_15) ; ]
+
+where B is the indicated most-significant-first encoding and B(0) is empty.
+Positive encodings start with `:`. Presence flags use 0/1, disjoint from
+count digits. Although `:` also terminates the descriptor, parsing is
+unambiguous: fixed role order and each presence bit separate the contexts.
+All thirty-five fixed symbols of the earlier grammar remain; H unary
+symbols become L binary symbols. This proves the frame-length formula.
+
+At pop, consume each role's count backward into scratch. The resulting
+word is little endian and has the original fixed width ell. Consuming the
+ell count digits costs 6ell, the next presence bit costs three, and rewind
+costs 2ell+3. The presence bit is retained in finite control while returning
+the corresponding payload head.
+
+For decrement, change each initial zero to one and move right until a one
+or terminal blank is read. If a one is found, replace it with zero and
+rewind. This subtracts one in the unchanged fixed-width word. Starting
+from a positive integer j, the initial zero-run length is its 2-adic
+valuation. Its cost is 5v_2(j)+5. The h positive decrements therefore cost
+10h-5popcount(h), by the same floor sum. Each successful decrement also
+causes one physical payload step left and a read of that parent bit.
+
+When the word is zero, all ell digits are temporarily changed to ones.
+The terminal blank identifies this case. Walk backward, erasing those
+ones, stop at the local marker and step right. Including the forward scan,
+this final failed decrement costs exactly 6ell+4. It returns false with
+scratch empty. There is no full-width zero test on every decrement; that
+would introduce an unnecessary H log H action bound.
+
+The code's only variable controller data are current symbols, a Boolean
+decrement result, fixed role indices and the sixteen-bit mask. Count
+arithmetic resides on tape. Helper call depth is fixed; all helpers can
+be duplicated at their finitely many call sites. Mathematical nested-call
+induction is not runtime recursion. The Python simulator's dictionaries,
+integer heads and snapshots belong to the test machine, not the controller.
+
+## Restoration and nesting
+
+The descriptor transfer, its two reversals, local child cleanup and parent
+suspension markers are the unchanged #5364 recipe. The new role loops
+replace only recording and consuming the return distance. After j parking
+steps the payload head is h_i+j and the counter represents j. The first
+blank occurs at j=H_i. Thus the child marker is placed at the exact parent
+end and the saved count is correct. Parent payload symbols are never written.
+
+After child cleanup, erase that suspension marker. The payload head is now
+at the parent end s_i. Each of H_i successful decrements moves it one cell
+left. Its final position is exactly h_i, and each visited parent cell is
+binary. The final failed decrement erases all counter cells. The saved
+presence bit restores that role's mask bit, including occupied empty roles.
+
+The unchanged descriptor return restores the original opaque word and its
+head. Consuming `[` leaves control at the original blank top. All new
+control and scratch cells are blank, and older control symbols are untouched.
+This proves one matched pair. Induction on any finite properly nested call
+tree proves the same assertion at every depth, since each inner matched
+pair restores the complete entry state required by its parent's remainder.
+No claim is made for malformed storage, failed children or unmatched calls.
+Invalid calls need not be transactional.
+
+## Derivation of the complete invoice
+
+The inherited `emit` and `take` cost three actions. A local rewind from
+offset x costs 2x+3. Clearing a child of length t from head g costs
+2g+5t+7, including empty children and all delimiter/blank reads.
+
+For one role, push costs presence emission three, payload scanning 2h+1,
+increments 10h-5popcount(h), counter transfer 8ell+4, suspension-marker
+write and movement two, and terminator emission three. Its total is
+12h-5popcount(h)+8ell+13. The inherited descriptor/frame setup costs
+8d+13, with one added initial scratch-blank read. Consequently
+
+    push = 8d + 12H - 5P + 8L + 13*16 + 14.
+
+For one role, pop costs six actions for its terminator and payload marker,
+8ell+6 for loading its count and presence bit, 10h-5popcount(h) for the
+positive decrements, 2h for payload return, and 6ell+4 for the final zero
+cleanup. Its total is 12h-5popcount(h)+14ell+16. The inherited descriptor
+and frame remainder is 14d+16, including the scratch-blank test. Hence
+
+    pop = 14d + 12H - 5P + 14L + 16*16 + 16
+          + sum_j (2g_j+5t_j+7),
+
+where there are seventeen child segments. Adding the two formulas yields
+(1). Since L<=H, P>=0 and G<=W, (2) follows for all nonnegative extents.
+These are symbolic tape-action identities, not elapsed-time benchmarks.
+
+## Verification and implementation boundaries
+
+The new verifier executes the new controller on the pinned predecessor's
+unit-action Tape simulator. It does not execute the predecessor's verifier
+or census. Independently computed binary strings, complete nineteen-tape
+snapshots and the displayed exact formulas are the oracles. A new controller
+object is created before return. Finite cases corroborate the written
+all-size proof; they are not a proof-kernel result.
+
+All loops in the controller are bounded by the declared finite tape segments,
+return distances, bit lengths or the fixed sixteen roles. In valid calls
+these decrease to a delimiter or a zero count. In the bounded verifier,
+payload lengths are at most 4097 in power-boundary cases and 4096 in its
+sixteen-role illustration; depth is at most 31 and prefixes at most 4096.
+The interpreter necessarily allocates managed Python objects; finite input
+bounds limit that test allocation. The finite-control program uses only its
+fixed tapes. The inherited simulator and helper implementation are unchanged.
+No repository-wide diagnostics or allocation refactor is part of this result.
+Dynamic imports are confined to authenticated, explicitly declared source
+paths; the four negative controls temporarily replace two named functions
+or damage one fixture symbol, and restore the original functions afterward.
+
+The standard binary carry argument is classical. The new result is this
+complete continuation-contract refinement, including the nine-symbol grammar,
+shared scratch, explicit restoration and exact space/action tradeoff.
+Mihir Srivastava retains #5364's contract, descriptor recipe and simulator;
+Ali Romman retains #5356/#5368's related stack/output construction; zxv
+retains #5404's complete historical-backing result. JoyboyBrian's segment
+boundary, Jose Manuel's sequential primitives, Douglas Colkitt's guard/repair,
+Cinna Davis's caller, Matarener's cover/stock and Sagar Thakrar's parent-return
+lineage retain their predecessor credit. None is reverified as the deliverable.
diff --git a/research/binary-distance-continuations/README.md b/research/binary-distance-continuations/README.md
new file mode 100644
index 0000000000..ed7d66599e
--- /dev/null
+++ b/research/binary-distance-continuations/README.md
@@ -0,0 +1,125 @@
+# Binary head-distance continuation frames
+
+Scoped constructive proof with exact finite corroboration.
+
+New construction and proof produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+The local continuation contract of Mihir Srivastava's
+[PR #5364](https://github.com/CrocSwap/integer-mult-bounds/pull/5364) can use
+binary head-return distances with the same nineteen tapes and nine symbols.
+Let H_i be each role's head-to-end distance, H their sum, d the opaque binary
+descriptor length, and L the sum of bitlength(H_i), with bitlength(0)=0.
+
+```text
+Unary control frame:   d + 35 + H symbols
+Binary control frame:  d + 35 + L symbols
+```
+
+The new construction records actual head movement with a little-endian
+counter on the existing reverse-scratch tape. It clears that counter into
+the frame and reconstructs it at return. All parent bytes, physical heads,
+role flags, descriptor, older stack symbols and scratch return exactly.
+Proper finite nesting is permitted, and child cleanup remains paid.
+
+With sixteen distances of 4096 and an empty descriptor, the executed frame
+uses **243 symbols instead of 65,571**, saving **65,328**. Its complete matched
+push/pop costs 1,577,893 read/write/unit-move actions for empty child words.
+This is an exact symbolic action invoice, not a runtime benchmark.
+
+[PROOF.md](PROOF.md) proves restoration, nesting, the grammar and the exact bill
+
+    22d + 24H - 10P + 22L + 613 + 2G + 5W,
+
+where P sums popcounts of the distances, W sums all seventeen child-word
+lengths, and G sums their return head offsets. Therefore the complete bill
+is at most **22d + 46H + 613 + 7W**. This exchanges a larger linear action
+constant for smaller headers. Scratch uses at most max(d,max_i bitlength(H_i))
+working symbols, plus its marker and terminal blank. Its historical extent
+is reused, and erased cells remain part of physical backing.
+
+## Evidence and reproduction
+
+CPython 3.12.15 on macOS 27.0.1 arm64; standard library only. From the repository
+root, the exact local interpreter is `/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12`.
+Use that interpreter in place of `python3.12` below on the supplied workspace.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/binary-distance-continuations
+python3.12 -I -W error -B research/binary-distance-continuations/verify.py
+python3.12 -I -O -W error -B research/binary-distance-continuations/verify.py
+python3.12 -B scripts/check_research_commit.py --package research/binary-distance-continuations --check-source-history
+```
+
+Expected markers are `PASS_BINARY_DISTANCE_CONTINUATIONS` and
+`PASS_REGISTERED_RESEARCH_PACKAGE`. Both registered commands run the complete
+check. [RESULT.json](RESULT.json) is generated by the verifier and binds the
+new implementation, verifier and written proof by SHA256. To regenerate it
+for an intentional source change, pass `--write-receipt /absolute/scratch/RESULT.json`
+and inspect that output before replacing the committed receipt.
+
+The checks execute 4,816 small matched boundaries, 36 distances immediately
+below/at/above powers of two through 4096, and 117 nested returns at depths
+1, 7 and 31 with ancestor-prefix lengths 16, 257 and 4096. The small domain
+covers every binary parent word of lengths zero through five, every parent
+head and every descriptor of lengths zero through three on a rotating role,
+plus the completely absent empty mask. Each matched boundary checks the
+independently generated frame, all nineteen tape snapshots, mask, exact
+action counts and conservative bill. A fresh controller object performs pop.
+Four controls reject a wrong top delimiter, omitted increment, omitted
+decrement and an absent nonempty role. Explicit exceptions remain active
+under optimized Python. No predecessor verifier or mathematical census is run.
+
+## Scope and limitations
+
+This original target changes the `uniform-transfer-audit` card to a local
+constructive side result relevant to `precision_tape` and `owned_erasure`.
+The selected baseline binding check passed. Neither selected assumption is
+discharged at its complete caller. The selected frontier is unchanged.
+
+The caller supplies well-formed contiguous binary segments, separate physical
+tapes and local markers. Intended child output must already be delivered
+before destructive pop. Malformed/failed calls need not restore state.
+Production dispatch, descriptor production, child-output installation, full
+historical payload backing, stock and a complete caller invoice remain open.
+No flat finite-state transition table, proof-kernel check, selected cold replay,
+Lean/Docker run or new kappa is supplied.
+
+The new controller is the rerunnable construction. Its loops terminate on
+finite local segments or counters under the entry contract. Test-side managed
+allocation, authenticated imports and narrowly bounded function replacement
+controls are documented in the proof. No shared implementation is changed.
+
+## Sources, overlap and credit
+
+Canonical base is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+[SOURCES.json](SOURCES.json) binds #5364's exact contract, proof and simulator
+as retained on that base. The new code reuses its primitive tape actions and
+descriptor/cleanup recipe. Mihir Srivastava retains that credit; this package
+adds the binary-distance construction and its exact space/action tradeoff.
+The carry-count identity and binary arithmetic are classical.
+
+Related merged work was read for scope: Ali Romman's #5356 local unary stack
+and #5368 output return, and zxv's #5404 historical-backing theorem. Their
+contracts are distinct and their results are cited, not audited. JoyboyBrian's
+segment boundary, Jose Manuel's sequential primitives, Douglas Colkitt's
+guard/repair, Cinna Davis's caller, Matarener's cover/stock and Sagar Thakrar's
+parent-return lineage retain their predecessor credit. No source notice changes.
+
+The overlap check covered live PR titles/bodies, this account's recent work,
+latest handoffs, active Discussions, local reservations, main README text and
+merged searches for binary continuations, head distances and compressed
+headers. No matching refinement was located in that coverage. Sparse cached
+notes, unpublished work and arbitrary historical code diffs remain limits;
+no literature-wide priority claim is made. The original target is reserved
+as a binary-head-distance continuation question, not as a predecessor audit.
+[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228524).
+
+## Open next questions
+
+Can an actual selected recursive caller use this frame with a smaller complete
+historical tape reserve? First bind one real continuation boundary and complete
+nested execution to the changed grammar, counting every tape's high-water
+extent. Production descriptor/dispatch semantics, designated output delivery,
+allocation and stock are blockers. The structured question is in
+[TASK.json](TASK.json). This result stops at the verified local reduction.
diff --git a/research/binary-distance-continuations/RESULT.json b/research/binary-distance-continuations/RESULT.json
new file mode 100644
index 0000000000..37cd8574ba
--- /dev/null
+++ b/research/binary-distance-continuations/RESULT.json
@@ -0,0 +1,23 @@
+{
+  "distance_4096_each_role": {
+    "binary_frame_symbols": 243,
+    "matched_actions": 1577893,
+    "saved_frame_symbols": 65328,
+    "unary_frame_symbols": 65571
+  },
+  "negative_controls": [
+    "wrong top delimiter",
+    "omitted increment",
+    "omitted decrement",
+    "absent nonempty role"
+  ],
+  "nested_returns": 117,
+  "power_boundaries": 36,
+  "small_boundaries": 4816,
+  "source_sha256": {
+    "PROOF.md": "f7ebf3bfd535cc71587572745701d3acd81e89e6ddfa77a189940571bebafca2",
+    "binary_stack.py": "2080a526d2991fd04e6953c5f5d1478d771eda7b87172891dc257820f0109c34",
+    "verify.py": "baad803ce804e5ec185d3dee16e18cd5c1594f051e2c65cf6fc2e5f1b0ab98d3"
+  },
+  "status": "PASS_BINARY_DISTANCE_CONTINUATIONS"
+}
diff --git a/research/binary-distance-continuations/SOURCES.json b/research/binary-distance-continuations/SOURCES.json
new file mode 100644
index 0000000000..997a5765e7
--- /dev/null
+++ b/research/binary-distance-continuations/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/segment-continuation-stack/PROOF.md",
+      "usage": "input",
+      "git_blob": "4a89021e16e838861f13f19a05df5eb38f7fb3b2",
+      "sha256": "f171e4181082037533848828da8bc6adba1f95f25e5c5ff4ee53a65fb05c0247"
+    },
+    {
+      "path": "research/segment-continuation-stack/README.md",
+      "usage": "input",
+      "git_blob": "ec62fb3f4457c7b3689b7cafb26a864c109557ec",
+      "sha256": "8b5c7b3d36ce34dab5bc24102a01e7a78e0aaadeee4a744abda7cb75b4e1474d"
+    },
+    {
+      "path": "research/segment-continuation-stack/stack.py",
+      "usage": "input",
+      "git_blob": "f551aec73ec7ce773adeb44321535316efd3f2e5",
+      "sha256": "d254d409d695942b4a0a58e54ff3a24da6a8a8b4b7211a19679faae63e76ff60"
+    }
+  ]
+}
diff --git a/research/binary-distance-continuations/TASK.json b/research/binary-distance-continuations/TASK.json
new file mode 100644
index 0000000000..f660ce1d2f
--- /dev/null
+++ b/research/binary-distance-continuations/TASK.json
@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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": "Construct binary head-distance continuation frames with exact restoration and linear sequential action cost.",
+  "scope_change_reason": "An original local construction reduces the unary header space in PR5364. It targets a precision/tape implementation component; it does not discharge a selected all-size assumption at its full caller.",
+  "bottleneck_link": "Scoped continuation-space improvement relevant to precision_tape and owned_erasure. Production caller integration and complete reserve remain open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified header-space reduction; do not extend to a full caller.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives an all-size local construction. RESULT.json is generated by verify.py with full restoration, exact costs, nested returns and negative controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual selected recursive caller use this binary continuation frame with a smaller complete historical tape reserve?",
+      "why_it_matters": "A local frame reduction is useful only after all payload and workspace high-water extents are included.",
+      "first_step": "Bind one source continuation boundary and a complete nested execution to the changed grammar and count every physical tape extent.",
+      "blocked_by": "Production descriptor/dispatch semantics, designated output delivery, and the complete caller allocation and stock contract are not supplied here."
+    }
+  ]
+}
diff --git a/research/binary-distance-continuations/VERIFY.json b/research/binary-distance-continuations/VERIFY.json
new file mode 100644
index 0000000000..97fe8c6837
--- /dev/null
+++ b/research/binary-distance-continuations/VERIFY.json
@@ -0,0 +1,38 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/segment-continuation-stack/PROOF.md",
+    "research/segment-continuation-stack/README.md",
+    "research/segment-continuation-stack/stack.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Source authentication, complete restoration and frame grammar, exact action invoices, 4816 small boundaries, 36 power boundaries, 117 nested returns, four negative controls and source-bound receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat the complete verifier with optimizations; explicit exceptions remain active."
+    }
+  ]
+}
diff --git a/research/binary-distance-continuations/binary_stack.py b/research/binary-distance-continuations/binary_stack.py
new file mode 100644
index 0000000000..440c4576a1
--- /dev/null
+++ b/research/binary-distance-continuations/binary_stack.py
@@ -0,0 +1,154 @@
+"""Binary-distance refinement of Mihir Srivastava's PR5364 contract.
+
+New construction produced by Nick Petalas. Apache-2.0.
+The inherited tape actions and descriptor/cleanup recipe retain PR5364 credit.
+Only symbols, fixed role indices and a sixteen-bit mask are controller state.
+"""
+
+from stack import (
+    BITS, BLANK, LEFT, ROLES, Controller as UnaryController,
+    clear, emit, need, rewind, take,
+)
+
+
+def increment(counter):
+    """Increment a little-endian count and return to its local beginning."""
+    while True:
+        symbol = counter.read()
+        need(symbol in BITS or symbol == BLANK, 'counter alphabet')
+        if symbol != '1':
+            counter.write('1')
+            break
+        counter.write('0')
+        counter.move(1)
+    rewind(counter)
+
+
+def store_count(counter, control):
+    """Emit most-significant-first u/: digits and erase the counter."""
+    while counter.read() != BLANK:
+        counter.move(1)
+    while True:
+        counter.move(-1)
+        symbol = counter.read()
+        if symbol == LEFT:
+            counter.move(1)
+            return
+        need(symbol in BITS, 'stored counter alphabet')
+        emit(control, 'u' if symbol == '0' else ':')
+        counter.write(BLANK)
+
+
+def load_count(control, counter):
+    """Consume reversed count digits; return the separate presence bit."""
+    leading = BLANK
+    symbol = take(control)
+    while symbol in ('u', ':'):
+        emit(counter, '0' if symbol == 'u' else '1')
+        leading = symbol
+        symbol = take(control)
+    need(leading in (BLANK, ':'), 'canonical binary distance')
+    need(symbol in BITS, 'role presence flag')
+    rewind(counter)
+    return symbol
+
+
+def decrement(counter):
+    """Subtract one, or erase the fixed-width zero word and return false."""
+    while True:
+        symbol = counter.read()
+        need(symbol in BITS or symbol == BLANK, 'counter alphabet')
+        if symbol == '1':
+            counter.write('0')
+            rewind(counter)
+            return True
+        if symbol == BLANK:
+            break
+        counter.write('1')
+        counter.move(1)
+    while True:
+        counter.move(-1)
+        symbol = counter.read()
+        if symbol == LEFT:
+            counter.move(1)
+            return False
+        need(symbol == '1', 'zero-count cleanup')
+        counter.write(BLANK)
+
+
+class Controller(UnaryController):
+    """The same nineteen tapes and nine symbols, with binary distance fields."""
+
+    def push(self):
+        need(self.reverse.read() == BLANK, 'counter scratch empty')
+        emit(self.control, '[')
+        while True:
+            symbol = self.descriptor.read()
+            if symbol == BLANK:
+                break
+            need(symbol in BITS, 'binary descriptor')
+            emit(self.control, symbol)
+            self.descriptor.write(BLANK)
+            self.descriptor.move(1)
+        rewind(self.descriptor, erased=True)
+        emit(self.control, ':')
+        for role in range(ROLES):
+            present = (self.occupied >> role) & 1
+            emit(self.control, '1' if present else '0')
+            tape = self.payload[role]
+            while True:
+                symbol = tape.read()
+                if symbol == BLANK:
+                    break
+                need(symbol in BITS, 'binary parent payload')
+                need(present, 'absent role must be empty')
+                tape.move(1)
+                increment(self.reverse)
+            store_count(self.reverse, self.control)
+            tape.write(LEFT)
+            tape.move(1)
+            emit(self.control, ';')
+        emit(self.control, ']')
+        self.occupied = 0
+
+    def pop(self):
+        for tape in self.payload:
+            clear(tape)
+        clear(self.descriptor)
+        need(self.reverse.read() == BLANK, 'counter scratch empty')
+        need(take(self.control) == ']', 'frame top delimiter')
+        self.occupied = 0
+        for role in reversed(range(ROLES)):
+            need(take(self.control) == ';', 'role terminator')
+            tape = self.payload[role]
+            tape.move(-1)
+            need(tape.read() == LEFT, 'payload suspension delimiter')
+            tape.write(BLANK)
+            flag = load_count(self.control, self.reverse)
+            while decrement(self.reverse):
+                tape.move(-1)
+                need(tape.read() in BITS, 'return distance within parent')
+            if flag == '1':
+                self.occupied |= 1 << role
+        need(take(self.control) == ':', 'descriptor terminator')
+        symbol = take(self.control)
+        while symbol in BITS:
+            emit(self.reverse, symbol)
+            symbol = take(self.control)
+        need(symbol == '[', 'frame beginning delimiter')
+        while True:
+            self.reverse.move(-1)
+            symbol = self.reverse.read()
+            if symbol == LEFT:
+                break
+            need(symbol in BITS, 'reverse scratch alphabet')
+            self.reverse.write(BLANK)
+            emit(self.descriptor, symbol)
+        self.reverse.move(1)
+        rewind(self.descriptor)
+
+
+def action_bound(descriptor_bits, return_distance, child_bits):
+    """Complete matched-boundary bound, including all child cleanup."""
+    need(min(descriptor_bits, return_distance, child_bits) >= 0, 'bound domain')
+    return 22 * descriptor_bits + 46 * return_distance + 613 + 7 * child_bits
diff --git a/research/binary-distance-continuations/verify.py b/research/binary-distance-continuations/verify.py
new file mode 100644
index 0000000000..a136bbe997
--- /dev/null
+++ b/research/binary-distance-continuations/verify.py
@@ -0,0 +1,233 @@
+"""Exact finite corroboration. Produced by Nick Petalas. Apache-2.0."""
+
+import argparse
+import ast
+import hashlib
+import itertools
+import json
+from pathlib import Path
+import sys
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def load_construction():
+    manifest = json.loads((PACKAGE / 'SOURCES.json').read_text())
+    for row in manifest['files']:
+        if row['usage'] == 'input':
+            actual = hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest()
+            require(actual == row['sha256'], 'changed source: ' + row['path'])
+    # Both import locations are explicit; the external code is authenticated.
+    sys.path.insert(0, str(ROOT / 'research/segment-continuation-stack'))
+    sys.path.insert(0, str(PACKAGE))
+    import binary_stack
+    import stack
+    return binary_stack, stack
+
+
+def exact_push(d, distances):
+    h = sum(distances)
+    bits = sum(x.bit_length() for x in distances)
+    ones = sum(x.bit_count() for x in distances)
+    return 8*d + 12*h - 5*ones + 8*bits + 13*16 + 14
+
+
+def exact_pop(d, distances, child_lengths, child_heads):
+    h = sum(distances)
+    bits = sum(x.bit_length() for x in distances)
+    ones = sum(x.bit_count() for x in distances)
+    cleanup = sum(2*g + 5*t + 7 for t, g in zip(child_lengths, child_heads))
+    return 14*d + 12*h - 5*ones + 14*bits + 16*16 + 16 + cleanup
+
+
+def frame(descriptor, mask, distances):
+    rows = []
+    for role, distance in enumerate(distances):
+        digits = format(distance, 'b') if distance else ''
+        encoded = ''.join('u' if bit == '0' else ':' for bit in digits)
+        rows.append(str((mask >> role) & 1) + encoded + ';')
+    return '[' + descriptor + ':' + ''.join(rows) + ']'
+
+
+def fixture(stack, words, heads, descriptor, mask, prefix='101[:;]'):
+    meter = stack.Meter()
+    payload = [stack.Tape(meter, prefix, word, head)
+               for word, head in zip(words, heads)]
+    control = stack.Tape(meter, prefix)
+    desc = stack.Tape(meter, prefix, descriptor)
+    scratch = stack.Tape(meter, prefix)
+    return meter, payload, control, desc, scratch, mask
+
+
+def snapshots(machine):
+    _, payload, control, desc, scratch, mask = machine
+    return tuple(t.snapshot() for t in [*payload, control, desc, scratch]), mask
+
+
+def write_child(tape, word, head, stack):
+    for symbol in word:
+        stack.emit(tape, symbol)
+    for _ in range(len(word) - head):
+        tape.move(-1)
+
+
+def boundary(module, stack, words, heads, descriptor, mask, children, child_heads):
+    machine = fixture(stack, words, heads, descriptor, mask)
+    meter, payload, control, desc, scratch, _ = machine
+    before = snapshots(machine)
+    distances = [len(w)-h for w, h in zip(words, heads)]
+    controller = module.Controller(payload, control, desc, scratch, mask)
+    start = meter.total
+    controller.push()
+    push = meter.total - start
+    require(push == exact_push(len(descriptor), distances), 'exact push invoice')
+    actual = ''.join(control._cells.get(i, '_')
+                     for i in range(before[0][-3][0], control._head))
+    expected = frame(descriptor, mask, distances)
+    require(actual == expected, 'binary frame grammar')
+    require(scratch.snapshot() == before[0][-1], 'scratch after push')
+    for tape, word, head in zip([*payload, desc], children, child_heads):
+        write_child(tape, word, head, stack)
+    # Discard the push controller so the return cannot use hidden saved state.
+    controller = module.Controller(payload, control, desc, scratch, 0)
+    start = meter.total
+    controller.pop()
+    pop = meter.total - start
+    lengths = [len(w) for w in children]
+    require(pop == exact_pop(len(descriptor), distances, lengths, child_heads),
+            'exact pop invoice')
+    restored = (*machine[:-1], controller.occupied)
+    require(snapshots(restored) == before, 'complete parent restoration')
+    require(push + pop <= module.action_bound(
+        len(descriptor), sum(distances), sum(lengths)), 'complete action bound')
+    return len(expected), push+pop
+
+
+def exhaustive_small(module, stack):
+    count = 0
+    descriptors = [''.join(x) for n in range(4)
+                   for x in itertools.product('01', repeat=n)]
+    for length in range(6):
+        for word_tuple in itertools.product('01', repeat=length):
+            word = ''.join(word_tuple)
+            for head in range(length+1):
+                for descriptor in descriptors:
+                    role = count % 16
+                    words, heads = ['']*16, [0]*16
+                    words[role], heads[role] = word, head
+                    children = ['']*17
+                    children[(role+3) % 17] = '01011'
+                    child_heads = [0]*17
+                    child_heads[(role+3) % 17] = count % 6
+                    boundary(module, stack, words, heads, descriptor, 1 << role,
+                             children, child_heads)
+                    count += 1
+    boundary(module, stack, ['']*16, [0]*16, '', 0, ['']*17, [0]*17)
+    return count+1
+
+
+def nested(module, stack, depth, prefix_length):
+    machine = fixture(stack, ['01011']*16, [3]*16, '10100', 65535,
+                      '1'*prefix_length)
+    _, payload, control, desc, scratch, mask = machine
+    saved = []
+    for level in range(depth):
+        before = snapshots((*machine[:-1], mask))
+        controller = module.Controller(payload, control, desc, scratch, mask)
+        controller.push()
+        saved.append(before)
+        for role, tape in enumerate(payload):
+            word = '10100' * (1 + (role+level) % 4)
+            write_child(tape, word, (role+level) % (len(word)+1), stack)
+        write_child(desc, '101' * (1 + level % 3), 0, stack)
+        mask = 65535
+    for before in reversed(saved):
+        controller = module.Controller(payload, control, desc, scratch, mask)
+        controller.pop()
+        mask = controller.occupied
+        require(snapshots((*machine[:-1], mask)) == before, 'nested restoration')
+    return depth
+
+
+def counter_boundaries(module, stack):
+    count = 0
+    for exponent in range(1, 13):
+        for distance in ((1 << exponent)-1, 1 << exponent, (1 << exponent)+1):
+            boundary(module, stack, ['1'*distance]+['']*15, [0]*16,
+                     '00101', 1, ['']*17, [0]*17)
+            count += 1
+    return count
+
+
+def negative_controls(module, stack):
+    rejected = []
+    machine = fixture(stack, ['101']+['']*15, [0]*16, '01', 1)
+    _, payload, control, desc, scratch, mask = machine
+    controller = module.Controller(payload, control, desc, scratch, mask)
+    controller.push()
+    control._cells[control._head-1] = '['
+    try:
+        controller.pop()
+    except ValueError:
+        rejected.append('wrong top delimiter')
+    for name, replacement in (('increment', lambda counter: None),
+                              ('decrement', lambda counter: False)):
+        original = getattr(module, name)
+        try:
+            setattr(module, name, replacement)
+            try:
+                boundary(module, stack, ['101']+['']*15, [0]*16, '01', 1,
+                         ['']*17, [0]*17)
+            except ValueError:
+                rejected.append('omitted ' + name)
+        finally:
+            setattr(module, name, original)
+    try:
+        boundary(module, stack, ['1']+['']*15, [0]*16, '', 0,
+                 ['']*17, [0]*17)
+    except ValueError:
+        rejected.append('absent nonempty role')
+    require(len(rejected) == 4, 'all semantic controls reject')
+    return rejected
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--write-receipt', type=Path)
+    args = parser.parse_args()
+    module, stack = load_construction()
+    tree = ast.parse((PACKAGE / 'binary_stack.py').read_text())
+    require(not any(isinstance(n, ast.Attribute) and n.attr.startswith('_')
+                    for n in ast.walk(tree)), 'no simulator metadata access')
+    result = {'status': 'PASS_BINARY_DISTANCE_CONTINUATIONS'}
+    result['small_boundaries'] = exhaustive_small(module, stack)
+    result['power_boundaries'] = counter_boundaries(module, stack)
+    result['nested_returns'] = sum(nested(module, stack, depth, prefix)
+                                   for depth in (1, 7, 31)
+                                   for prefix in (16, 257, 4096))
+    length, actions = boundary(module, stack, ['1'*4096]*16, [0]*16, '', 65535,
+                               ['']*17, [0]*17)
+    result['distance_4096_each_role'] = {
+        'binary_frame_symbols': length, 'unary_frame_symbols': 16*4096+35,
+        'saved_frame_symbols': 16*4096+35-length, 'matched_actions': actions,
+    }
+    result['negative_controls'] = negative_controls(module, stack)
+    result['source_sha256'] = {
+        name: hashlib.sha256((PACKAGE/name).read_bytes()).hexdigest()
+        for name in ('binary_stack.py', 'verify.py', 'PROOF.md')}
+    if args.write_receipt:
+        args.write_receipt.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n')
+    else:
+        require(result == json.loads((PACKAGE/'RESULT.json').read_text()),
+                'generated source-bound receipt')
+    print(json.dumps(result, sort_keys=True))
+
+
+if __name__ == '__main__':
+    main()