diff --git a/research/crt-binary-key-port/PROOF.md b/research/crt-binary-key-port/PROOF.md
new file mode 100644
index 0000000000..c7bffebbc1
--- /dev/null
+++ b/research/crt-binary-key-port/PROOF.md
@@ -0,0 +1,177 @@
+# Literal binary key at the retained repair port
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Object and claim
+
+This lowers the actual `service.py` program of #4795 (head
+`4e4cf7e47f3fc1c40e775d84fb2e7cd2603658cd`). For each fixed J in {0,1,2},
+its domain remains u2,t2,y8, every 12-bit address, and a supplied 32-bit F
+independent of yJ. The source proof gives the key T(S^-1(q)), three current-y
+queries, borrowed counter/ROM preservation, private erasure/head return,
+append of twelve source bit symbols and at most 3,287,110 source instructions.
+Those source semantics are a retained premise; this package proves their
+literal binary realization and tests its actual caller interface.
+
+There are the same fifteen physical tapes. Each source cell j is represented
+by bits 13j through 13j+12, little-endian; each source head j corresponds to
+physical head 13j. The stream may start at any source-cell boundary after an
+arbitrary legal payload/key prefix. Its twelve-symbol append advances the
+physical head **156** bits, not twelve. No input conversion occurs at a call.
+Packet construction/encoding and ROM supply are external entry premises.
+
+The complete program uses only one-bit reads/writes, unit physical head
+moves, one-bit assignments/copies, XOR (including a literal-bit operand),
+AND, OR, NOT, Boolean branch, jump and halt. Each executed instruction costs
+one action. It is the executable program, not a multiplication of an old
+receipt. A finite instruction transition includes its sequencing; explicit
+branches/jumps are charged instructions as well.
+
+## Encoding, including opaque payloads and finite control
+
+The source symbols have these thirteen-bit integer codes:
+
+| Symbol | blank `_` | `L` | `0` | `1` | `R` | `<` | `>` | `=` |
+| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: |
+| Code | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 |
+
+The opaque record `('R',v)` has code 4096+v, for 0<=v<4096. Thus all 4,104
+symbols are distinct, and the all-zero physical background represents blank.
+Codes 8..4095 are unused. The port theorem assumes correctly encoded finite
+records and aligned heads; it is not an arbitrary-bit-string admission theorem.
+`=` is a source finite-control value; including it in the common alphabet is
+harmless even though the retained key program does not write it to a tape.
+
+Each source register uses fourteen one-bit registers. A symbol is its 13-bit
+code followed by tag zero. Boolean false/true has low bit zero/one, twelve
+further zeros, and tag one. This distinguishes Boolean true from symbol `L`
+and Boolean false from blank. The source uses finite-control equality results
+as Boolean branch conditions; tape values and `0`/`1` arithmetic are symbols.
+Dropping the tag makes equality of true and L incorrect even though both have
+low code one. Registers and code locations have fixed finite cardinality.
+The compiled full service has 492 one-bit registers, independent of address,
+source ROM contents or stream-prefix length.
+
+Complete service compilation emits 492 initial zero assignments and another
+492 before each reachable halt. Only one halt is reached per invocation, so
+**984 lifecycle actions** are executed. The verifier deliberately starts the
+emulator registers dirty; input initialization and final erasure are paid.
+No free host allocation/reset is needed in the claimed machine. Primitive
+block tests omit this wrapper to supply arbitrary initial register values.
+
+## Per-block simulation
+
+Take any source state at an instruction boundary, with tape cells/heads and
+initialized register operands represented as above. The following invariant
+holds after each corresponding nonterminal binary block: all source-visible cells,
+registers and heads have exactly the indicated representation, and the binary
+PC is the relocated address of the next source instruction. Compiler-private
+comparison bits are not source-visible and are erased by the final lifecycle.
+
+| Source instruction | Binary implementation | Core actions |
+| --- | --- | ---: |
+| read | 13 single-bit reads, 12 moves right and 12 left, set the symbol tag to zero | 38 |
+| write / write_reg | 13 writes and the same 24 moves; return to cell start | 37 |
+| move ±1 | 13 unit moves in the same direction | 13 |
+| set / copy | fourteen one-bit assignments/copies | 14 |
+| eq / eq_reg | zero accumulator; 14 XOR+OR pairs; 13 Boolean output-tag/upper-bit assignments; NOT accumulator to low output bit | 43 |
+| xorbit / andbit / orbit | one Boolean gate on low operand bits, then 13 assignments to the remaining `0`/`1` symbol-code bits | 14 |
+| branch / jump / halt | one corresponding fixed-control operation | 1 |
+
+Read/write move only inside one encoded cell before returning, so they cannot
+read or overwrite neighboring payloads. Write writes all thirteen bits even
+when the old cell is dirty. The source data bits are codes two and three,
+which differ exactly in their low bit; the other code bits and tag are restored
+by the bit-arithmetic block. It computes the output low bit before assigning
+upper bits, so source/destination aliasing is safe.
+
+For equality, after bit i the scratch accumulator is the OR of all differences
+through i. Negating its final value is exactly equality of the full tagged
+words. All comparisons finish before writing destination bits, so aliasing a
+source and destination register is also safe. The reserved scratch names do
+not occur in the authenticated source program. Copying a word to itself is
+safe. The source's reachable branch operands are Booleans; their low bit is
+therefore the correct decision, and branch targets are statically relocated.
+
+At halt no source instruction remains; the source-visible register correspondence
+is replaced by the promised all-zero control endpoint. Source halt has a separate lifecycle suffix of 492 assignments and the halt
+itself; the table's one-action halt is its core, not a claim that cleanup is
+free. The initial 492 assignments precede the first source block. Labels are
+relocated after these expansions, including jumps across either halt suffix.
+
+Induction on the actual source execution proves the simulation, termination,
+key and ownership result. In particular, all cleared source private cells
+become thirteen zero bits, borrowed cells are unchanged, private/counter/ROM
+heads return to zero and the protected stream prefix is unchanged. All finite
+control bits also finish zero. This argument applies to every legal source
+input; testing a finite subset is corroboration, not the induction hypothesis.
+For a framed input on which the source rejects and cleans up, the same
+simulation gives rejection/cleanup, without claiming the legal-input time
+bound for arbitrary malformed packets.
+
+## Complete bound
+
+Let T be a legal #4795 source execution length, including its one halt, and
+let R=492. Every core block costs at most 43, and initialization/termination
+cost 2R. Therefore
+
+`T_binary <= 43*T + 2R <= 43*3,287,110 + 984 = 141,346,714`.
+
+This includes every executed bit action and Boolean/control instruction,
+current-state descriptor/header work, all three ROM traversals, full carry
+arithmetic, append, private erasure, physical head return and finite-control
+initialization/erasure. No asymptotic compiler bound is asserted: the compiler
+emits one of three fixed finite programs (106,583 / 106,713 / 106,843 bit
+instructions). Its static program size contains two halt cleanup paths; its
+runtime takes only one. The sampled counts near 0.9 million actions/key are
+not used to prove the upper bound.
+
+The interpreter's PC, register-number lookup, sparse tape dictionary indices,
+head coordinates and action census are emulator metadata. `Machine.step`
+never exposes a coordinate, tape length, decoded word or count to the program.
+Runtime values read from tapes or registers are individual bits. There is no
+symbol decoder or original key evaluator inside the binary executor. The
+source is compiled before any address/ROM/payload is supplied. All data paths
+in the executable are the stated primitive bit operations.
+
+## Caller-bound evidence and limits
+
+The verifier constructs the same middle-layer source ROM, raw compact-word
+payload stream and original guard mask as the retained source caller. The
+unchanged `bridge.split` runs on facades whose **only storage is physical bit
+tapes**. Facade reads decode symbols for the unlowered outer controller; facade
+writes/moves perform the corresponding bit operations. This outer decoding
+is an explicit boundary, not part of the binary key program or its tariff.
+
+At the original `evaluate_key(counter,bad,...)` call, the new adapter gives
+`Machine` those same underlying tapes, without reading/converting an address
+into an executor parameter or copying in/out a computed key. Observer-only
+address decoding checks the source reference, but never feeds the executor.
+The first two actual marked-hole calls return, and the original split then
+continues to the third hole at address two. This checks that both 156-bit
+advances and the next opaque payload write obey the original caller contract.
+The verifier interrupts before executing that third key, not after a full
+layer. It then closes the captured two-completed-pair prefix with an END marker
+as explicit verifier setup and passes it to the unchanged original `one_pass`.
+Its radix split preserves the captured payloads, rotates their actual returned
+keys correctly and returns the consumer heads. Closing/projecting the prefix
+is not claimed to be the full split/sort/reinsert algorithm.
+
+The first two caller addresses are simple keys; a separate transported parity
+case at q=892 checks every one of 44,340 source-instruction boundaries, all
+physical head scales, every written block and every defined register result.
+Three further complete binary runs cover nontrivial carry/boundary behavior
+and all retained targets. Primitive checks cover all 4,104 encodings and their
+read/dirty-write blocks, plus 172 equality/Boolean/alias cases. Mutants expose
+short physical moves, incorrect Boolean tagging, a dirty borrowed head and
+omitted finite-control erasure, and a colliding marker code. Three framed malformed
+packets also reject with complete physical/control cleanup. These are new execution/representation checks,
+not a replay of #4795's 376-case census.
+
+Not supplied: a full 2,944-call binary layer, a literal binary lowering or full
+control tariff for the outer producer/scanner/sort/reinsert, physical creation
+of raw S or the source ROM, encoded variable-width CRT parameters, uniform
+compiler/constructor cost, or complete E(p,ell). No multiplication theorem or
+new kappa follows. The fixed-geometry source proof and its predecessor credits
+remain explicit. Other current reservoir/layout or stopped-recursion results
+address different obligations.
diff --git a/research/crt-binary-key-port/README.md b/research/crt-binary-key-port/README.md
new file mode 100644
index 0000000000..1fcd4dde02
--- /dev/null
+++ b/research/crt-binary-key-port/README.md
@@ -0,0 +1,119 @@
+# Literal binary execution at the CRT key port
+
+This package compiles and **executes** the complete finite-control key service
+of [PR #4795](https://github.com/CrocSwap/integer-mult-bounds/pull/4795) using
+one-bit tape access, unit bit-head moves and one-bit Boolean/control operations.
+It closes that package's explicit binary-encoding gap for its retained
+u2,t2,y8 geometry and the original repair counter/bad-stream port.
+
+The [scoped proof](PROOF.md) gives
+
+`binary actions per key <= 43*3,287,110 + 984 = 141,346,714`.
+
+The factor 43 is proved per source instruction. The additional 984 actions
+actually initialize and erase all 492 control bits. This is a fixed-geometry
+program theorem, not a uniform CRT compiler, complete outer repair tariff or
+new multiplication result. The selected κ is unchanged.
+
+## Executed representation
+
+[binary.py](binary.py) produces three fixed bit programs, for source targets
+0, 1 and 2, with 106,583 / 106,713 / 106,843 instructions. Every source cell
+uses thirteen physical bits: all 4,096 opaque 12-bit payload labels and eight
+source symbols have distinct codes. A separate register tag distinguishes
+Boolean true/false from symbols. All runtime reads, writes, gates and branches
+operate on individual bits; no host-decoded address/key enters the executor.
+
+The same fifteen tape roles are retained. Source-cell head j is physical head
+13j. Appending twelve source bit symbols advances the stream by **156 physical
+bits**. Private tape bits and heads, borrowed heads and all control bits are
+returned as stated in the proof; borrowed counter/ROM and prior payloads are
+preserved. Serialization of input packets and source ROM creation are explicit
+external prerequisites.
+
+## Evidence at the actual caller
+
+[verify.py](verify.py) independently represents symbol/Boolean values and
+executes source instruction semantics. [RESULT.json](RESULT.json) records:
+
+- All 4,104 codec values; 8,208 literal read and dirty-cell write cases, plus
+  172 equality/Boolean/alias controls.
+- Four complete binary key runs, including a transported parity-source key
+  at address 892. Every one of its 44,340 source-instruction boundaries is
+  checked against the independent observer: control target, physical head,
+  written cell and defined register result.
+- The original `bridge.split` with its actual middle-layer guard mask/raw
+  source stream, calling the binary service on the **same physical tapes**
+  at its first two holes. The source caller then continues to the third hole,
+  at address two, demonstrating the returned head/record boundary.
+- The unchanged original `one_pass` consumes a projection of those two completed
+  pairs and preserves payload/key correspondence. Closing that captured prefix
+  with END is explicit verifier setup; this is not a whole-layer replay.
+- Five discriminating faults: short bit stride, dirty ROM head, omitted control
+  erasure, missing Boolean tag and colliding marker code. Three framed malformed
+  packets reject with borrowed data, blank scratch and cleared controls checked.
+
+The six accepted full key invocations execute **5,348,850 binary actions**.
+The actual two caller invocations take 859,622 and 859,888 actions; the other
+four take 896,367–914,737. These observed counts do not establish the uniform
+bound; the block simulation does. The entire bounded verifier takes about
+three seconds locally, using one CPU and the standard library.
+
+The source caller facade decodes symbols for the **unlowered outer controller**.
+It never converts/copies an address or returned key at the service boundary:
+the service directly sees the facade's underlying bit tapes. Its key execution
+is wholly bit-level. Observer word decoding and oracle arithmetic are outside
+the executor. This package does not price outer control, full sorting/reinsertion,
+raw macro-S creation, ROM construction, variable-width parameters or E(p,ell).
+No full 2,944-call binary layer or historical suite was run.
+
+## Provenance and distinct scope
+
+Exact predecessor #4795 is
+`4e4cf7e47f3fc1c40e775d84fb2e7cd2603658cd`; it is retained unchanged on base
+`b91956876e5b4122fd89179f1b57557ff8378f15`. Its source proof, #4752 ROM program
+and original #4637 bridge/oracle, scanner increment, and original compact word
+are pinned in [SOURCES.json](SOURCES.json). Retention is not scientific approval.
+
+Current #4938 establishes evaluator/layout caps; #4942 and the reservoir-bill
+package price ordinary-interchange wrapper calls; #4946 audits the word-census
+prune; #4965 studies complex stopped recursion. Those do not supply this literal
+binary key executor. [TASK.json](TASK.json) records the refined question and
+bounded stop rule. Canonical coordination is
+[Discussion #4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19138317).
+
+## Reproduce
+
+From the repository root, Python 3.12:
+
+```sh
+python3.12 scripts/research_package.py --package research/crt-binary-key-port --check-only
+python3.12 scripts/research_package.py --package research/crt-binary-key-port
+python3.12 -O -B research/crt-binary-key-port/verify.py
+```
+
+The registered command has a 30-second cap and authenticates all declared live
+inputs before executing. Direct replay compares the frozen result; only explicit
+`--write-result` changes it. Source-history/committed-byte checks and the standard
+exporter bind the published files. Direct verification works in a Git-free export;
+the generic provenance-aware package runner itself requires Git history.
+
+## Open next questions
+
+1. Lower a bounded actual sparse-repair consumer (for example one radix pass)
+   into literal bit control using the same 13-bit representation. The current
+   facade still performs outer symbol decoding; a complete invoice must include
+   its branching, routing and lifecycle rather than multiplying a cell count.
+2. Supply physical ROM construction and variable-width parameter handling at
+   the real CRT caller. The fixed-width program and its source theorem do not
+   provide those prerequisites. First establish an encoded producer/consumer
+   contract; a larger finite key census would not resolve it.
+
+## Credit
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0.
+Retain #4795/#4752 authorship and the #4637 scanner/repair lineage: Cinna Davis,
+ToikY, Hiroki KUMAZAKI, Ryanson Jonathan, unpaidmoon, Jose Manuel and the original
+[source-specific notice](../unconditional-batched-crt/NOTICE.md). All predecessor
+source files are reused unchanged. No independent human or proof-kernel review
+is claimed.
diff --git a/research/crt-binary-key-port/RESULT.json b/research/crt-binary-key-port/RESULT.json
new file mode 100644
index 0000000000..f5b62ae8ce
--- /dev/null
+++ b/research/crt-binary-key-port/RESULT.json
@@ -0,0 +1,162 @@
+{
+  "behavior_controls": [
+    "short_move",
+    "dirty_head",
+    "keep_control",
+    "drop_tag",
+    "marker_collision"
+  ],
+  "binary_sha256": "50a3dea7fc087715b4e605e85629566ed31903026540f916df6b8cbaa536182d",
+  "caller": {
+    "calls": [
+      {
+        "address": 0,
+        "binary_actions": 859622,
+        "key": "000000000000",
+        "payload": 0
+      },
+      {
+        "address": 1,
+        "binary_actions": 859888,
+        "key": "000000000001",
+        "payload": 1
+      }
+    ],
+    "consumer": "original one_pass on two completed captured pairs",
+    "continued_to_address": 2,
+    "full_layer_replayed": false,
+    "source_target": 2
+  },
+  "keys": [
+    {
+      "address": 892,
+      "audited_source_instructions": 44340,
+      "binary_actions": 907284,
+      "census": {
+        "and": 156,
+        "branch": 11205,
+        "copy": 24416,
+        "halt": 1,
+        "jump": 5077,
+        "move": 258756,
+        "not": 11205,
+        "or": 156940,
+        "read": 88738,
+        "set": 185535,
+        "write": 6682,
+        "write_reg": 1560,
+        "xor": 11483,
+        "xor_const": 145530
+      },
+      "key": "011101110100",
+      "target": 0
+    },
+    {
+      "address": 4095,
+      "audited_source_instructions": 0,
+      "binary_actions": 910952,
+      "census": {
+        "and": 152,
+        "branch": 11252,
+        "copy": 24430,
+        "halt": 1,
+        "jump": 5224,
+        "move": 260334,
+        "not": 11252,
+        "or": 157596,
+        "read": 89141,
+        "set": 185674,
+        "write": 6682,
+        "write_reg": 1547,
+        "xor": 11479,
+        "xor_const": 146188
+      },
+      "key": "111111110110",
+      "target": 0
+    },
+    {
+      "address": 1023,
+      "audited_source_instructions": 0,
+      "binary_actions": 896367,
+      "census": {
+        "and": 32,
+        "branch": 11180,
+        "copy": 24444,
+        "halt": 1,
+        "jump": 5270,
+        "move": 256358,
+        "not": 11180,
+        "or": 156528,
+        "read": 88036,
+        "set": 179337,
+        "write": 6682,
+        "write_reg": 780,
+        "xor": 11359,
+        "xor_const": 145180
+      },
+      "key": "001111111111",
+      "target": 1
+    },
+    {
+      "address": 4095,
+      "audited_source_instructions": 0,
+      "binary_actions": 914737,
+      "census": {
+        "and": 152,
+        "branch": 11262,
+        "copy": 24444,
+        "halt": 1,
+        "jump": 5330,
+        "move": 263182,
+        "not": 11262,
+        "or": 157736,
+        "read": 89882,
+        "set": 185437,
+        "write": 6682,
+        "write_reg": 1560,
+        "xor": 11479,
+        "xor_const": 146328
+      },
+      "key": "111111011111",
+      "target": 2
+    }
+  ],
+  "primitive": {
+    "boolean_cases": 172,
+    "read_write_cases": 8208,
+    "symbols": 4104
+  },
+  "programs": [
+    {
+      "binary_instructions": 106583,
+      "bit_registers": 492,
+      "lifecycle_actions": 984,
+      "max_core_block": 43,
+      "source_instructions": 5313,
+      "target": 0
+    },
+    {
+      "binary_instructions": 106713,
+      "bit_registers": 492,
+      "lifecycle_actions": 984,
+      "max_core_block": 43,
+      "source_instructions": 5323,
+      "target": 1
+    },
+    {
+      "binary_instructions": 106843,
+      "bit_registers": 492,
+      "lifecycle_actions": 984,
+      "max_core_block": 43,
+      "source_instructions": 5333,
+      "target": 2
+    }
+  ],
+  "proved_binary_actions_per_key": 141346714,
+  "rejected_packet_actions": [
+    17792,
+    18249,
+    12497
+  ],
+  "status": "PASS_LITERAL_BINARY_KEY_PORT"
+}
diff --git a/research/crt-binary-key-port/SOURCES.json b/research/crt-binary-key-port/SOURCES.json
new file mode 100644
index 0000000000..27b3e26f72
--- /dev/null
+++ b/research/crt-binary-key-port/SOURCES.json
@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/crt-dense-guard-scan/machine.py",
+      "usage": "input",
+      "git_blob": "ce763898bd7b4401bbab818c640a0593b65c9a82",
+      "sha256": "1cb27312932914eb631078bd56e85feb1dc6c4191e9d1962b2cc3a7e1cfb8df7"
+    },
+    {
+      "path": "research/crt-mask-repair-bridge/bridge.py",
+      "usage": "input",
+      "git_blob": "826d62adbb777ceec20974e600a6ea05e03b7828",
+      "sha256": "573451d94435b6096a88250ca2a9fb75f39bcfa6f0436ffe2363ee07381d8331"
+    },
+    {
+      "path": "research/crt-mask-repair-bridge/key_subroutine.py",
+      "usage": "input",
+      "git_blob": "5771ae55626dbc2a32a95d8c098bdd03d820833c",
+      "sha256": "ffdbb610be71ae20bf974946dac66b6c1b4d43739cbc3b1eb81cbbeab8784b44"
+    },
+    {
+      "path": "research/crt-paid-key-service/PROOF.md",
+      "usage": "input",
+      "git_blob": "a0b84e8d3bd80d760a1be9e801fc57939b6f24e9",
+      "sha256": "1a4ac02653eb6c1b20807033a910f27bf9484cc972bf2629941f589275a87325"
+    },
+    {
+      "path": "research/crt-paid-key-service/service.py",
+      "usage": "input",
+      "git_blob": "726d9523ab7dd4a16697f9201b0224f2da1f2517",
+      "sha256": "ff06c6305c9f650a694e5c42baa4c7d841decf844a4f44f6776acc10a8400083"
+    },
+    {
+      "path": "research/crt-uniform-rom-query/PROOF.md",
+      "usage": "input",
+      "git_blob": "63b0551a7715b9b67f2b13510183254401eb082f",
+      "sha256": "736be5e1af590f2195e8b56b958258f0babe5cd6d2cf6f4f5023410112f4d870"
+    },
+    {
+      "path": "research/crt-uniform-rom-query/machine.py",
+      "usage": "input",
+      "git_blob": "88292ce98d31d540c7dba6960bfe4c19f06a8077",
+      "sha256": "46ee6a635251e498ee9a5d4aff8c0e2a7f1ef2ff951e5b6a2a8953316e9cd02d"
+    },
+    {
+      "path": "research/unconditional-batched-crt/NOTICE.md",
+      "usage": "input",
+      "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f",
+      "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461"
+    },
+    {
+      "path": "research/unconditional-batched-crt/check_batched_crt.py",
+      "usage": "input",
+      "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc",
+      "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e"
+    }
+  ]
+}
diff --git a/research/crt-binary-key-port/TASK.json b/research/crt-binary-key-port/TASK.json
new file mode 100644
index 0000000000..65732fbb32
--- /dev/null
+++ b/research/crt-binary-key-port/TASK.json
@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "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_status": "refined",
+  "actual_scope": "Execute a literal binary lowering of the complete retained #4795 finite key service and bind its encoded address/opaque-payload port to the original repair caller continuation.",
+  "scope_change_reason": "The generic all-size audit is narrowed to #4795's explicit binary-encoding remainder. New layout/reservoir/complex results do not supply that program. This changes the executed alphabet and control lifecycle instead of repeating the previous key census.",
+  "bottleneck_link": "A paid marker-alphabet key is not yet the literal binary service its original opaque-payload caller would use. Per-block simulation and actual physical port continuation discharge this fixed-geometry implication while the outer controller and uniform ROM/parameter costs remain explicit.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after a valid binary program and scoped block proof, codec/Boolean and mutation checks, bounded actual first-hole caller continuation, and source/export validation; otherwise report a precise obstruction. No full 2944-call binary layer or unrelated suite.",
+  "outcome": "completed",
+  "evidence": "PROOF.md establishes at most 43 actions per core source instruction plus 984 explicitly executed control lifecycle actions, giving 141,346,714 per key. RESULT.json records 4,104 codec values, 8,208 read/write cases, 172 Boolean/alias cases, 44,340 independently observed source boundaries, six full binary keys, actual split continuation and projected original one_pass, five fault controls and three framed rejections.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance for implementation, independent semantics observer, proof, tests, packaging and separate-context code/proof review.",
+  "open_questions": [
+    {
+      "question": "Can one actual sparse-repair radix consumer be lowered into complete binary control on the same encoded port?",
+      "why_it_matters": "Outer symbol decoding and its Boolean/routing/lifecycle costs remain outside the literal key theorem.",
+      "first_step": "Lower the unchanged original one_pass control and match its whole encoded-payload boundary, counting every operation.",
+      "blocked_by": "Only the key executor is binary here; the outer caller uses a symbol facade."
+    },
+    {
+      "question": "Can physical ROM production and encoded variable-width parameters replace the fixed geometry?",
+      "why_it_matters": "The uniform CRT evaluator still needs its real source supplier and compiler costs.",
+      "first_step": "Specify and realize one caller-bound ROM/parameter producer contract rather than increasing finite fixtures.",
+      "blocked_by": "The 32-bit source ROM and u2,t2,y8 widths are supplied prerequisites."
+    }
+  ]
+}
diff --git a/research/crt-binary-key-port/VERIFY.json b/research/crt-binary-key-port/VERIFY.json
new file mode 100644
index 0000000000..b3f37063c0
--- /dev/null
+++ b/research/crt-binary-key-port/VERIFY.json
@@ -0,0 +1,28 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/crt-dense-guard-scan/machine.py",
+    "research/crt-mask-repair-bridge/bridge.py",
+    "research/crt-mask-repair-bridge/key_subroutine.py",
+    "research/crt-paid-key-service/PROOF.md",
+    "research/crt-paid-key-service/service.py",
+    "research/crt-uniform-rom-query/PROOF.md",
+    "research/crt-uniform-rom-query/machine.py",
+    "research/unconditional-batched-crt/NOTICE.md",
+    "research/unconditional-batched-crt/check_batched_crt.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Pinned-source authentication, complete alphabet/read/write checks, tagged Boolean alias cases, independent source-block observer, actual original caller continuation and radix consumer, five mutants, three framed rejection packets and frozen binary receipt."
+    }
+  ]
+}
diff --git a/research/crt-binary-key-port/binary.py b/research/crt-binary-key-port/binary.py
new file mode 100644
index 0000000000..ec574f26d6
--- /dev/null
+++ b/research/crt-binary-key-port/binary.py
@@ -0,0 +1,123 @@
+"""Literal binary lowering of the retained finite key program.
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+Assembly/packet construction is outside runtime; Machine only executes bit ops.
+"""
+from collections import Counter
+
+WIDTH = 13
+REGISTER_WIDTH = 14
+CODES = {'_':0, 'L':1, '0':2, '1':3, 'R':4, '<':5, '>':6, '=':7}
+
+
+def code(symbol):
+    if type(symbol) is tuple and symbol[0] == 'R' and 0 <= symbol[1] < 4096:
+        return 4096 + symbol[1]
+    return CODES[symbol]
+
+
+def bits(symbol):
+    n = code(symbol)
+    return tuple((n >> j) & 1 for j in range(WIDTH))
+
+
+def word(value):
+    if type(value) is bool: return (int(value),) + (0,)*12 + (1,)
+    return bits(value) + (0,)
+
+
+def compile_program(source, fault=None, lifecycle=False):
+    """Finite static compilation; no packet/address/ROM is an argument."""
+    out=[];starts=[];registers={}
+    def emit(*instruction): out.append(instruction)
+    def reg(name, bit):
+        key=(name,bit)
+        if key not in registers: registers[key]=len(registers)
+        return registers[key]
+    def set_word(name,value):
+        for j,bit in enumerate(word(value)):emit('set',reg(name,j),bit)
+    for instruction in source:
+        starts.append(len(out));op,*a=instruction
+        if op in ('read','write','write_reg'):
+            for j in range(WIDTH):
+                if op=='read':emit('read',a[0],reg(a[1],j))
+                elif op=='write':emit('write',a[0],bits(a[1])[j])
+                else:emit('write_reg',a[0],reg(a[1],j))
+                if j != WIDTH-1:emit('move',a[0],1)
+            for _ in range(WIDTH-1):emit('move',a[0],-1)
+            if op=='read':emit('set',reg(a[1],13),0)
+        elif op=='move':
+            for _ in range(WIDTH if fault!='short_move' else WIDTH-1):emit('move',a[0],a[1])
+        elif op=='set':set_word(a[0],a[1])
+        elif op=='copy':
+            for j in range(REGISTER_WIDTH):emit('copy',reg(a[0],j),reg(a[1],j))
+        elif op in ('eq','eq_reg'):
+            emit('set',reg('$different',0),0)
+            for j in range(13 if fault=='drop_tag' else REGISTER_WIDTH):
+                if op=='eq':emit('xor_const',reg(a[0],j),word(a[1])[j],reg('$xor',0))
+                else:emit('xor',reg(a[0],j),reg(a[1],j),reg('$xor',0))
+                emit('or',reg('$different',0),reg('$xor',0),reg('$different',0))
+            for j in range(1,REGISTER_WIDTH):emit('set',reg(a[2],j),int(j==13))
+            emit('not',reg('$different',0),reg(a[2],0))
+        elif op in ('xorbit','andbit','orbit'):
+            emit({'xorbit':'xor','andbit':'and','orbit':'or'}[op],reg(a[0],0),reg(a[1],0),reg(a[2],0))
+            for j in range(1,REGISTER_WIDTH):emit('set',reg(a[2],j),int(j==1))
+        elif op=='branch':emit('branch',reg(a[0],0),('label',a[1]),('label',a[2]))
+        elif op=='jump':emit('jump',('label',a[0]))
+        elif op=='halt':
+            if fault=='dirty_head':emit('move','rom',1)
+            if lifecycle and fault!='keep_control':emit('clear_control')
+            emit('halt',a[0])
+        else:raise ValueError('unknown source operation')
+    starts.append(len(out))
+    # Initialize and erase each physical finite-control bit explicitly when
+    # composing a complete service, rather than relying on host allocation.
+    offsets=[];at=len(registers) if lifecycle else 0
+    for instruction in out:
+        offsets.append(at);at+=len(registers) if instruction[0]=='clear_control' else 1
+    offsets.append(at);starts=[offsets[start] for start in starts]
+    program=[('set',j,0) for j in range(len(registers))] if lifecycle else []
+    for instruction in out:
+        if instruction[0]=='clear_control':program.extend(('set',j,0) for j in range(len(registers)))
+        else:program.append(tuple(starts[x[1]] if type(x) is tuple and x[0]=='label' else x for x in instruction))
+    return program,starts,registers
+
+
+class BitTape:
+    """Physical binary cells; head coordinates exist only in this emulator."""
+    def __init__(self,initial=(),head=0):
+        self.cells={i:b for i,b in enumerate(initial) if b};self.head=head;self.actions=Counter()
+    def read(self):self.actions['read']+=1;return self.cells.get(self.head,0)
+    def write(self,bit):
+        if bit not in (0,1):raise ValueError('nonbinary write')
+        self.actions['write']+=1
+        if bit:self.cells[self.head]=1
+        else:self.cells.pop(self.head,None)
+    def move(self,direction):
+        if direction not in (-1,1) or self.head+direction<0:raise ValueError('invalid physical move')
+        self.actions['move']+=1;self.head+=direction
+
+
+class Machine:
+    def __init__(self,program,register_count,tapes):
+        self.program=program;self.registers=[0]*register_count;self.tapes=tapes
+        self.pc=0;self.census=Counter();self.status=None
+    def step(self):
+        op,*a=self.program[self.pc];self.pc+=1;self.census[op]+=1;r=self.registers;t=self.tapes
+        if op=='read':r[a[1]]=t[a[0]].read()
+        elif op=='write':t[a[0]].write(a[1])
+        elif op=='write_reg':t[a[0]].write(r[a[1]])
+        elif op=='move':t[a[0]].move(a[1])
+        elif op=='set':r[a[0]]=a[1]
+        elif op=='copy':r[a[1]]=r[a[0]]
+        elif op in ('xor','xor_const'):r[a[2]]=r[a[0]]^(a[1] if op=='xor_const' else r[a[1]])
+        elif op=='and':r[a[2]]=r[a[0]]&r[a[1]]
+        elif op=='or':r[a[2]]=r[a[0]]|r[a[1]]
+        elif op=='not':r[a[1]]=r[a[0]]^1
+        elif op=='branch':self.pc=a[1] if r[a[0]] else a[2]
+        elif op=='jump':self.pc=a[0]
+        elif op=='halt':self.status=a[0]
+        else:raise ValueError('unknown binary operation')
+    def run(self):
+        while self.status is None:self.step()
+        return self.status
diff --git a/research/crt-binary-key-port/verify.py b/research/crt-binary-key-port/verify.py
new file mode 100644
index 0000000000..eb93b173a8
--- /dev/null
+++ b/research/crt-binary-key-port/verify.py
@@ -0,0 +1,289 @@
+"""Independent block semantics and actual caller continuation for the bit port.
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+All decoding and source arithmetic in this file are external verifier/outer control.
+"""
+import argparse
+from collections import Counter
+import hashlib
+import json
+from pathlib import Path
+import sys
+import types
+
+P=Path(__file__).resolve().parent
+ROOT=P.parents[1]
+
+
+def need(ok,message):
+    if not ok:raise ValueError(message)
+
+
+def load(name,path):
+    m=types.ModuleType(name);m.__file__=str(path);sys.modules[name]=m
+    exec(compile(path.read_bytes(),str(path),'exec'),m.__dict__);return m
+
+
+def modules():
+    for row in json.loads((P/'SOURCES.json').read_text())['files']:
+        if row['usage']!='input':continue
+        raw=(ROOT/row['path']).read_bytes()
+        need(hashlib.sha256(raw).hexdigest()==row['sha256'],'source SHA256 drift')
+        need(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest()==row['git_blob'],'source Git blob drift')
+    paths={'source':'crt-paid-key-service/service.py','query':'crt-uniform-rom-query/machine.py',
+           'bridge':'crt-mask-repair-bridge/bridge.py','oracle':'crt-mask-repair-bridge/key_subroutine.py',
+           'native':'crt-dense-guard-scan/machine.py','crt':'unconditional-batched-crt/check_batched_crt.py'}
+    result={k:load('binary_port_'+k,ROOT/'research'/path) for k,path in paths.items()}
+    result['binary']=load('binary_port_impl',P/'binary.py');return result
+
+
+# Independent representation (no compiler encoding helper).
+TABLE=['_','L','0','1','R','<','>','=']
+
+
+def encode(symbol):
+    number=TABLE.index(symbol) if type(symbol) is str else 4096+symbol[1]
+    return tuple(int(c) for c in format(number,'013b')[::-1])
+
+
+def encode_value(value):
+    return ((int(value),)+(0,)*12+(1,)) if type(value) is bool else encode(value)+(0,)
+
+
+def decode(block):
+    n=sum(v*2**i for i,v in enumerate(block))
+    if n<8:return TABLE[n]
+    need(n>=4096,'invalid symbol code');return ('R',n-4096)
+
+
+def packet(symbols):return [bit for symbol in symbols for bit in encode(symbol)]
+
+
+def physical_word(tape,cell):return tuple(tape.cells.get(13*cell+j,0) for j in range(13))
+
+
+def observe_register(machine,registers,name):
+    return tuple(machine.registers[registers[name,j]] for j in range(14))
+
+
+def primitive_checks(b):
+    values=TABLE+[('R',i) for i in range(4096)]
+    encodings=[encode(v) for v in values]
+    need(len(set(encodings))==4104,'injective complete caller alphabet')
+    need(all(b.bits(v)==encode(v) and decode(encode(v))==v for v in values),'independent encoding')
+    read,_,rr=b.compile_program([('read','x','a'),('halt','accept')])
+    write,_,wr=b.compile_program([('write_reg','x','a'),('halt','accept')])
+    for v in values:
+        tape=b.BitTape(encode(v));m=b.Machine(read,len(rr),{'x':tape});m.run()
+        need(observe_register(m,rr,'a')==encode_value(v) and tape.head==0,'all-symbol read')
+        tape=b.BitTape((1,)*13);m=b.Machine(write,len(wr),{'x':tape})
+        for j,x in enumerate(encode_value(v)):
+            if ('a',j) in wr:m.registers[wr['a',j]]=x
+        m.run();need(physical_word(tape,0)==encode(v) and tape.head==0,'all-symbol dirty overwrite')
+    tests=0
+    # The tagged cases distinguish True/L and False/blank; every pair differs
+    # in either a specific low/high position, a payload bit, or the Boolean tag.
+    pairs=[(x,y) for x in TABLE+[True,False] for y in TABLE+[True,False]]
+    pairs += [(('R',x),('R',x^(1<<j))) for x in (0,1,4095) for j in range(12)]
+    for x,y in pairs:
+        program,_,regs=b.compile_program([('eq_reg','a','b','z'),('halt','accept')])
+        m=b.Machine(program,len(regs),{})
+        for name,value in [('a',x),('b',y)]:
+            for j,bit in enumerate(encode_value(value)):
+                if (name,j) in regs:m.registers[regs[name,j]]=bit
+        m.run();need(observe_register(m,regs,'z')==encode_value(type(x)==type(y) and x==y),'tagged equality');tests+=1
+    for op in ('xorbit','andbit','orbit'):
+        for x in '01':
+            for y in '01':
+                for dst in ('a','b','z'):
+                    program,_,regs=b.compile_program([(op,'a','b',dst),('halt','accept')]);m=b.Machine(program,len(regs),{})
+                    for name,value in [('a',x),('b',y)]:
+                        for j,bit in enumerate(encode_value(value)):
+                            if (name,j) in regs:m.registers[regs[name,j]]=bit
+                    m.run();v=((x!=y) if op=='xorbit' else (x=='1' and y=='1') if op=='andbit' else (x=='1' or y=='1'))
+                    need(observe_register(m,regs,dst)==encode_value('1' if v else '0'),'bit arithmetic alias truth table');tests+=1
+    return dict(symbols=4104,read_write_cases=8208,boolean_cases=tests)
+
+
+def source_step(code,state):
+    """Independent marker-machine semantics, used only by the audit observer."""
+    pc,regs,cells,heads=state;op,*a=code[pc];pc+=1
+    if op=='read':regs[a[1]]=cells[a[0]].get(heads[a[0]],'_')
+    elif op in ('write','write_reg'):cells[a[0]][heads[a[0]]]=a[1] if op=='write' else regs[a[1]]
+    elif op=='move':heads[a[0]]+=a[1]
+    elif op=='set':regs[a[0]]=a[1]
+    elif op=='copy':regs[a[1]]=regs[a[0]]
+    elif op=='eq':regs[a[2]]=regs[a[0]]==a[1]
+    elif op=='eq_reg':regs[a[2]]=regs[a[0]]==regs[a[1]]
+    elif op in ('xorbit','andbit','orbit'):
+        x=regs[a[0]]=='1';y=regs[a[1]]=='1'
+        regs[a[2]]='1' if ((x!=y) if op=='xorbit' else x and y if op=='andbit' else x or y) else '0'
+    elif op=='branch':pc=a[1] if regs[a[0]] else a[2]
+    elif op=='jump':pc=a[0]
+    elif op=='halt':pass
+    else:raise ValueError('unknown source opcode')
+    return pc,regs,cells,heads
+
+
+def key_run(mod,target,table,address,audited=False,fault=None):
+    b=mod['binary'];source,_=mod['source'].assemble(mod['query'],target)
+    program,starts,regs=b.compile_program(source,fault,lifecycle=True)
+    initial={name:[] for name in mod['source'].OWNED_WIDTHS}
+    initial.update(counter=['<',*format(address,'012b'),'>'],rom=['L',*map(str,table),'R'],stream=['<',('R',4095),('R',0)])
+    tapes={role:b.BitTape(packet(cells),39 if role=='stream' else 0) for role,cells in initial.items()}
+    m=b.Machine(program,len(regs),tapes);m.registers[:]=[1]*len(regs);source_counts=Counter();charged=0
+    if audited:
+        for _ in range(starts[0]):m.step()
+        charged=starts[0]
+        state=(0,{}, {r:dict(enumerate(c)) for r,c in initial.items()}, {r:3 if r=='stream' else 0 for r in initial})
+        while m.status is None:
+            pc=state[0];need(m.pc==starts[pc],'source/micro control boundary')
+            op,*a=source[pc];state=source_step(source,state)
+            length=starts[pc+1]-starts[pc]
+            for _ in range(length):m.step()
+            charged+=length;source_counts[op]+=1
+            if op!='halt':need(m.pc==starts[state[0]],'relocated jump/branch')
+            for role in initial:need(tapes[role].head==13*state[3][role],'physical head scaling')
+            if op in ('write','write_reg'):
+                role=a[0];pos=state[3][role];need(physical_word(tapes[role],pos)==encode(state[2][role][pos]),'binary write simulation')
+            dest=(a[1] if op in ('read','copy') else a[0] if op=='set' else a[2] if op in ('eq','eq_reg','xorbit','andbit','orbit') else None)
+            if dest is not None:need(observe_register(m,regs,dest)==encode_value(state[1][dest]),'register simulation')
+        need(charged==sum(m.census.values()),'complete block instruction invoice')
+    else:m.run()
+    need(m.status=='accept' and not any(m.registers),'binary acceptance and control erasure')
+    expected=mod['oracle'].ReverseWordKey(target,table).key_of(format(address,'012b'))
+    actual=''.join(decode(physical_word(tapes['stream'],i)) for i in range(3,15))
+    need(actual==expected,'key equals independent retained word')
+    for r in ('counter','rom'):need(tapes[r].cells=={i:v for i,v in enumerate(packet(initial[r])) if v} and tapes[r].head==0,'borrowed restoration')
+    for r in mod['source'].OWNED_WIDTHS:need(not tapes[r].cells and tapes[r].head==0,'private bit erasure and return')
+    need(tapes['stream'].head==195 and all(physical_word(tapes['stream'],i)==encode(c) for i,c in enumerate(initial['stream'])),'opaque prefix and 156-bit append')
+    need(sum(m.census.values())<=43*3_287_110+2*len(regs),'binary static bound')
+    return dict(target=target,address=address,key=actual,binary_actions=sum(m.census.values()),audited_source_instructions=sum(source_counts.values()),census=dict(sorted(m.census.items())))
+
+
+def rejection_checks(mod):
+    b=mod['binary'];source,_=mod['source'].assemble(mod['query'],2)
+    program,starts,regs=b.compile_program(source,lifecycle=True);rows=[]
+    for payload in ('0'*11,'0'*13,'00000_000000'):
+        tapes={name:b.BitTape() for name in mod['source'].OWNED_WIDTHS}
+        tapes.update(counter=b.BitTape(packet(['<',*payload,'>'])),rom=b.BitTape(packet(['L',*('0'*32),'R'])),stream=b.BitTape(packet(['<',('R',4095)]),26))
+        before={role:dict(tapes[role].cells) for role in ('counter','rom','stream')}
+        m=b.Machine(program,len(regs),tapes);m.registers[:]=[1]*len(regs);m.run()
+        need(m.status=='reject' and not any(m.registers),'framed binary rejection and control erase')
+        need(all(tapes[r].cells==before[r] and tapes[r].head==(26 if r=='stream' else 0) for r in before),'rejected borrowed/append port preserved')
+        need(all(not tapes[r].cells and tapes[r].head==0 for r in mod['source'].OWNED_WIDTHS),'rejected private bit cleanup')
+        rows.append(sum(m.census.values()))
+    return rows
+
+
+class Facade:
+    """Unlowered outer caller only. Its storage is the SAME physical bit tape."""
+    def __init__(self,b,symbols):self.raw=b.BitTape(packet(symbols))
+    def read(self):
+        data=[]
+        for j in range(13):
+            data.append(self.raw.read())
+            if j<12:self.raw.move(1)
+        for _ in range(12):self.raw.move(-1)
+        return decode(data)
+    def write(self,symbol):
+        for j,bit in enumerate(encode(symbol)):
+            self.raw.write(bit)
+            if j<12:self.raw.move(1)
+        for _ in range(12):self.raw.move(-1)
+    def move(self,d):
+        for _ in range(13):self.raw.move(d)
+
+
+class Captured(Exception):pass
+
+
+def caller_port(mod):
+    b=mod['binary'];crt=mod['crt'];bridge=mod['bridge'];target=2
+    nets=[crt.benes(crt.rotation(8,5,(2*a)%5 if a<3 else 0)) for a in range(4)]
+    table=[nets[a][2][1][v] for a in range(4) for v in range(8)]
+    raw=[None]*4096;mask=[]
+    for q in range(4096):
+        u,t,y=q>>10,(q>>8)&3,q&255
+        moved=crt.compact(u,t,y,lambda yy:(table[yy&31],),positions=(target,),ybits=8)
+        dest=(moved[0]<<10)|(moved[1]<<8)|moved[2];raw[dest]=('R',q)
+        mask.append('0' if crt.good(u,t,y,bits=2,positions=(target,),guard=6) else '1')
+    counter=Facade(b,['<',*('0'*12),'>']);data=Facade(b,['<',*raw,'>']);mt=Facade(b,['<',*mask,'>'])
+    good=Facade(b,['<']);bad=Facade(b,['<']);scratch=Facade(b,['<'])
+    rom=b.BitTape(packet(['L',*map(str,table),'R']));private={r:b.BitTape() for r in mod['source'].OWNED_WIDTHS}
+    source,_=mod['source'].assemble(mod['query'],target);program,starts,regs=b.compile_program(source,lifecycle=True)
+    calls=[];saved=bridge.evaluate_key;meter={'calls':0,'interface_actions':0};capture={}
+    def invoke(actual_counter,actual_bad,unused,meter):
+        need(actual_counter is counter and actual_bad is bad,'original caller objects')
+        address=int(''.join(decode(physical_word(counter.raw,i)) for i in range(1,13)),2)
+        if len(calls)==2:
+            capture.update(next_address=address,head=bad.raw.head);raise Captured()
+        start=bad.raw.head;prefix=dict(bad.raw.cells);counter_before=dict(counter.raw.cells);rom_before=dict(rom.cells)
+        tapes=dict(private,counter=counter.raw,stream=bad.raw,rom=rom)
+        machine=b.Machine(program,len(regs),tapes);machine.registers[:]=[1]*len(regs);machine.run()
+        expected=mod['oracle'].ReverseWordKey(target,table).key_of(format(address,'012b'))
+        result=''.join(decode(physical_word(bad.raw,start//13+j)) for j in range(12))
+        need(result==expected and machine.status=='accept' and not any(machine.registers),'actual caller key/control return')
+        need(all(bad.raw.cells.get(i,0)==value for i,value in prefix.items()) and all(bad.raw.cells.get(i,0)==prefix.get(i,0) for i in range(start)),'physical opaque prefix')
+        need(counter.raw.cells==counter_before and counter.raw.head==0 and rom.cells==rom_before and rom.head==0,'borrowed physical restore')
+        need(all(not t.cells and t.head==0 for t in private.values()) and bad.raw.head==start+156,'physical owned return/append')
+        calls.append(dict(address=address,key=result,payload=decode(physical_word(bad.raw,start//13-1))[1],binary_actions=sum(machine.census.values())))
+        meter['calls']+=1
+    bridge.evaluate_key=invoke
+    try:
+        bridge.split(mt,data,counter,good,bad,scratch,None,mod['native'].increment_and_return,meter,frozenset())
+    except Captured:pass
+    finally:bridge.evaluate_key=saved
+    holes=[i for i,v in enumerate(mask) if v=='1']
+    need([x['address'] for x in calls]==holes[:2] and capture['next_address']==holes[2],'actual mask calls and caller continuation')
+    need(bad.raw.head==13*(1+2*13+1),'caller next payload head after two complete returns')
+    # A projection of the two completed pairs is given to the original radix
+    # consumer. Closing the captured prefix is verifier setup, not a full layer.
+    first_next_record=1+2*13
+    bad.raw.head=13*first_next_record;bad.write('>');bad.raw.head=0
+    b0=Facade(b,['<']);b1=Facade(b,['<']);bridge.one_pass(bad,b0,b1,frozenset())
+    expected_order=sorted(calls,key=lambda r:r['key'][-1])
+    for i,row in enumerate(expected_order):
+        cell=1+13*i;need(decode(physical_word(bad.raw,cell))==('R',row['payload']),'actual radix consumer payload')
+        rotated=''.join(decode(physical_word(bad.raw,cell+j)) for j in range(1,13))
+        need(rotated==row['key'][-1]+row['key'][:-1],'actual radix consumer key')
+    need(all(x.raw.head==0 for x in (bad,b0,b1)),'consumer heads returned')
+    return dict(source_target=target,calls=calls,continued_to_address=capture['next_address'],consumer='original one_pass on two completed captured pairs',full_layer_replayed=False)
+
+
+def main():
+    ap=argparse.ArgumentParser();ap.add_argument('--write-result',action='store_true');args=ap.parse_args();mod=modules();b=mod['binary']
+    primitive=primitive_checks(b)
+    programs=[]
+    for target in (0,1,2):
+        source,_=mod['source'].assemble(mod['query'],target);micro,starts,regs=b.compile_program(source,lifecycle=True)
+        lengths=[starts[i+1]-starts[i] for i,inst in enumerate(source) if inst[0]!='halt'];need(max(lengths)==43,'proved core per-block maximum')
+        programs.append(dict(target=target,source_instructions=len(source),binary_instructions=len(micro),bit_registers=len(regs),max_core_block=43,lifecycle_actions=2*len(regs)))
+    parity=[(x>>1).bit_count()&1 for x in range(32)]
+    rows=[key_run(mod,0,parity,892,True),key_run(mod,0,parity,4095),key_run(mod,1,[0]*32,1023),key_run(mod,2,[0]*32,4095)]
+    controls=[]
+    for fault in ('short_move','dirty_head','keep_control'):
+        try:key_run(mod,0,parity,892,fault=fault)
+        except (ValueError,KeyError,IndexError):controls.append(fault)
+        else:raise ValueError('undetected physical mutant '+fault)
+    for fault in ('drop_tag',):
+        program,_,regs=b.compile_program([('eq_reg','a','b','z'),('halt','accept')],fault)
+        m=b.Machine(program,len(regs),{})
+        for name,value in [('a',True),('b','L')]:
+            for j,bit in enumerate(encode_value(value)):
+                if (name,j) in regs:m.registers[regs[name,j]]=bit
+        m.run();need(observe_register(m,regs,'z')!=encode_value(False),'tag mutant must differ');controls.append(fault)
+    previous=b.CODES['R'];b.CODES['R']=b.CODES['L']
+    try:
+        try:primitive_checks(b)
+        except ValueError:controls.append('marker_collision')
+        else:raise ValueError('marker collision not detected')
+    finally:b.CODES['R']=previous
+    rejected=rejection_checks(mod)
+    result=dict(status='PASS_LITERAL_BINARY_KEY_PORT',primitive=primitive,programs=programs,keys=rows,caller=caller_port(mod),behavior_controls=controls,rejected_packet_actions=rejected,
+                proved_binary_actions_per_key=43*3_287_110+984,binary_sha256=hashlib.sha256((P/'binary.py').read_bytes()).hexdigest())
+    if args.write_result:(P/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n')
+    else:need(result==json.loads((P/'RESULT.json').read_text()),'frozen result receipt')
+    print(json.dumps(result,sort_keys=True))
+
+if __name__=='__main__':main()