diff --git a/research/crt-multitarget-row-audit/PROOF.md b/research/crt-multitarget-row-audit/PROOF.md
new file mode 100644
index 0000000000..77adf1bcd4
--- /dev/null
+++ b/research/crt-multitarget-row-audit/PROOF.md
@@ -0,0 +1,302 @@
+# Multi-target composition at the current CRT row boundary
+
+This is an independent, source-relative audit of JoyboyBrian's PR #5496,
+head `a99afd7e0024af8367d5a2f6f4d2da57a1d13dd5`. The unchanged program and
+the exact claim audited are retained in `vendor/`. We found no defect in
+the implication below. The inherited numerical and ROM-producer theorems
+remain hypotheses; this is not an independent acceptance of those theorems,
+of #4100, or of a complete multiplication algorithm.
+
+## Statement and inherited contracts
+
+Let `d` be a power of two, `ell >= 2`, and `h_i in {ell-1,ell}`. At every
+axis let `2 <= s_i < 2^h_i`, with all moduli pairwise coprime, and let
+`0 <= x_i < 2^h_i`. Fix an admitted tree node `[a,a+n)`, `n=2^level >= 2`,
+with `b=a+n/2`, and a global row `0 <= g < 2ell-1`. Put
+
+    P = 1 + sum_{a <= i < a+n} h_i.
+
+Use the sequential axis-record format of PR5353, eight distinct protected
+numerical ports, the fixed compiled topology, and initially blank new
+owned backing. The source and all ports have their specified entry heads.
+Assume these two source contracts:
+
+1. **Numerical Entry.** PR5353/PR5219/PR5053 produce one P-bit `(c_i,v_i)`
+   record for **every** right axis `b <= i < a+n`, including idle axes.
+   If the left coordinates are valid, their current child is the unique
+   `k in [0,M)`, `M=product_{a <= j < b} s_j`, satisfying
+
+       k = x_i product_{a <= j < i} s_j (mod s_i),  a <= i < b.
+
+   If any left coordinate is padded, `k=0`. Each offset is
+
+       c_i = k (product_{a <= j < i} s_j)^(-1) mod s_i.
+
+   `v_i` is the complete-rotation output, not the micro-row output.
+   Entry supplies its stated input preservation, numerical ownership and
+   retirement guarantees.
+2. **ROM producer.** PR5092 accepts its encoded headers with `W>=h+3`,
+   legal modulus, selector and offsets; it returns the canonical complete
+   Beneš layers and selected row on the supplied output backings. It
+   preserves its headers, returns all heads to zero, and erases private
+   work. Blank tails beyond the current records are permitted. Its literal
+   loops terminate at their record markers, rather than the allocated list
+   length. This last fact is also directly visible in `microcode.py`.
+
+The conclusion is the original #5496 multi-target interface: if at least
+one right axis is active, `RowQuery` returns the exact current micro-row
+output for every right axis in order, copying idle axes unchanged. It
+uses one producer bank throughout that row, returns the borrowed bytes
+and heads, and retires all joined owned work on `close`. An all-idle row
+performs no tape work and allocates no numerical or ROM bank.
+
+This quantifies over all admitted parameters and padded current values,
+conditional on the two contracts. The finite executions below corroborate
+the implication; they are not the reason the quantifier holds.
+
+## Width and synchronized-row checks
+
+Admissibility forces every `h_i >= 2`: there is no integer `s_i` with
+`2 <= s_i < 2^1`. A node contains another axis besides any chosen target,
+so `P >= h_i+3`. Thus `W=P` meets the unchanged ROM producer's guard,
+including the minimum case `P=5,h_i=2`. The encoded constants `h_i` and
+the local row fit P bits. Offsets are in `[0,s_i)` by the Entry contract.
+
+For a long axis the local row is `g`. For a short axis the two global
+rows `ell-1,ell` are idle; the remaining local rows are `g` before that
+gap and `g-2` afterward. This lists `0,...,2h_i-2` exactly once. On every
+active row the target bit
+
+    min(local, 2h_i-2-local)
+
+equals the corresponding global schedule bit `min(g,2ell-2-g)`. These
+are the exact predicates and formulas used by the source loop.
+
+## Induction over the literal axis loop
+
+Immediately before parsing axis j, maintain these facts:
+
+* The borrowed source head is at that axis's ROOT, with all bytes unchanged.
+  The unary guide is back at its initial head.
+* The numerical result head is at the first unconsumed right-axis record.
+  Exactly one record has been consumed for each earlier **right** axis,
+  whether active or idle. Axes outside the node consume no result record.
+* The open output stream consists of exactly the processed right-axis
+  outputs, each in its declared `h_i` bits and followed by `|`; its head
+  is at the next blank output position.
+* Coordinate/countdown scratch and all four headers are blank at origin.
+  After every completed active target, the same physical producer roles
+  are blank at origin, including both outputs and every previously exposed
+  tail. The numerical result remains live until the entire loop ends.
+
+The first state follows from Entry's return and the fresh joined ports.
+There are three induction steps.
+
+**An axis outside the right half.** The loop reads its declared width,
+modulus and coordinate once, changes no source byte, and advances to the
+next ROOT. It consumes no numerical record and emits nothing.
+
+**An idle right axis.** The loop copies its h-bit coordinate to the
+coordinate port, skips exactly P offset bits and their delimiter, then
+skips exactly P complete-rotation bits and their delimiter. It checks and
+crosses RECORD_END. The coordinate is appended unchanged to the output,
+followed by `|`, and its scratch is erased. In particular, skipping the
+ROM call does **not** skip the numerical record. This is the boundary a
+single-target/all-idle test does not exercise: there can be a later active
+axis whose record must still be aligned.
+
+**An active right axis.** The loop copies the current modulus, offset,
+and compiled row/width to the producer's four headers, padded against the
+same unary P guide. It separately copies the current coordinate into the
+coordinate and countdown ports. The preceding width argument establishes
+the producer's complete header domain. The private bank and output roles
+are blank by the invariant, so the producer contract applies on the
+original backing objects.
+
+The selected ROM contains exactly `2^h_i` row bits. At ROM position j,
+until selection, the countdown equals `x_i-j`. A nonzero word is
+decremented with ordinary borrow propagation; zero selects the current
+row bit and disables further countdown changes. Since `x_i<2^h_i`,
+selection occurs exactly once before the ROM end marker. Both heads
+return, and countdown scratch is erased. XOR at the compiled target bit
+therefore gives exactly this micro-row's output. There is no `x_i<s_i`
+guard: intermediate padded coordinates must still be queried.
+
+The complete-layer output, selected ROM and all four headers are erased
+before the next axis. An erase crosses the current R and returns to L;
+all previously exposed cells beyond that R were blank at entry and are
+unchanged. The producer's private roles already returned blank. Thus the
+whole old backing, rather than just the shorter new prefix, is again
+blank. The complete-rotation field is consumed without supplying the
+micro-row answer. Output emission and coordinate erasure reestablish the
+invariant. Growing and shrinking target widths make no change to this
+argument; P is fixed for the node.
+
+At termination, both source and numerical result have their final end
+marker. Their rewinds restore the required heads, and the output receives
+R. The output stream contains every right target exactly once, in order.
+`close` erases this stream and invokes the original Entry retirement once.
+The all-idle branch has no Entry context and returns before tape access;
+its `close` is also empty. This proves the stated implication.
+
+Offsets depend on the current **left** child and all preceding moduli.
+The right target loop neither changes that child nor needs an offset
+recomputed from a changed right coordinate. This does not authorize
+reusing an offset across the three distinct current-left states of an
+exceptional reverse key; PR4716's stale-offset objection remains intact.
+
+## Cost and ownership boundary
+
+Retain the entire original invoice: one Entry invocation/retirement,
+one complete ROM production for each active axis, and all adapter work.
+No full-layer output is dropped merely because the consumer selects one
+row. With A the active right axes and
+
+    L = 2 + sum_i (3h_i+4),
+    F = L + (n+1)(P+2)
+        + sum_{i in A} [(2^h_i+1)(h_i+1)
+                       + 2^h_i(2h_i-1) + 2h_i+4],
+
+the literal loops have O(F) adapter tape work: one source scan and rewind,
+O(P) headers/result consumption per target, O(2^h_i h_i) countdown scans,
+and disposal of both outputs. The checker isolates adapter cell actions
+from Entry and ROM work and compares them with the source's `4096F`
+allowance. This is stronger finite diagnostic coverage than checking only
+the much larger combined bound. We do not independently certify the
+source's full finite-control constant or its inherited arithmetic tariff.
+
+## Exact retained footprint of this shared ROM bank
+
+The literal source permits a sharper statement than #5496's conservative
+sum of per-invocation storage bounds. For a nonempty active set, let
+`H=max_{i in A} h_i`, `N=2^H`. The exact retained cell count of its 52-role
+ROM service bank, including the four caller-owned headers, is
+
+    B(P,H) = 5 P 2^H (H^2+3H+1)
+             + 2^H(4H-1) + 48P + 2H + 104.                 (1)
+
+This is a count of finite-symbol **tape cells** of the pinned source
+program. It excludes the numerical Entry, the three other joined ports,
+borrowed axis/dirty words, interpreter metadata and any externally supplied
+blank reserve. It is not a bit-space theorem for an unbuilt binary compiler.
+
+Here is a derivation from the actual producer, rather than an inference
+from its output contract alone. At tree depth k there are `2^k` nodes of
+size `2^(h-k)` and height `t=h-k`. Each node has three scalar arrays and
+`2t-1` layer arrays, hence `2^(h-k)(2t+2)` arena records. Summing over
+`t=1,...,h`, and adding the shared N-slot stack, gives exactly
+
+    J = N [sum_{t=1}^h(2t+2)+1] = N(h^2+3h+1).
+
+This arena inventory is already part of ToikY's PR4192 lineage and
+PR5092's proof. The new footprint statement assembles all literal roles,
+markers and serializations and proves their repeated-bank maximum; it
+does not claim the arena count or the general rolewise-maximum principle
+(already in Ross Richardson's retained-backing audits) as new discoveries.
+
+The successful singleton-offset call has the following retained extents:
+
+| Role(s) | Number | Cells in each role |
+|---|---:|---:|
+| Scalar roles in the literal REGS tuple | 44 | `P+2` |
+| Arena, five P-bit words per record | 1 | `5PJ+2` |
+| Offset-major spool | 1 | `N(2h-1)+2` |
+| Complete layers with one separator per layer | 1 | `(N+1)(2h-1)+2` |
+| Selected row ROM | 1 | `N+2` |
+| Width, modulus, selected-layer headers | 3 | `P+2` |
+| Singleton offset header | 1 | `P+3` |
+
+Every listed extent is attained: initialization writes every scalar role
+and every arena record, and serialization writes every spool, layer and
+ROM bit plus its markers. None depends on the offset value or on the
+canonical network's particular bits. Conversely, no admitted execution
+visits beyond these extents. Scalar `each`, copy, comparison, carry/borrow,
+shift and erase routines stop at their fixed-width markers. Arena accesses
+scan complete five-word records through R and return; their indices
+select records without moving to a computed physical address. Initializers
+append the displayed counts. Spool scans end immediately after the last
+network bit; output appends end at their R slots. No routine steps past
+those slots on a successful path. `execute` only extends a backing when
+a unit movement first reaches its next cell, and never shortens a list.
+This proves the table's exact high-water counts for fresh one-cell blank
+private/output roles, the initialization used by RowQuery.
+
+At fixed P each row of this table is nondecreasing in h. For a sequence
+of target widths, each physical role therefore has exactly its extent at
+the largest width seen. This **componentwise monotonicity**, together with
+the reuse invariant, proves (1) by summing the table at H. Simply taking
+the maximum of arbitrary aggregate storage bounds would be invalid; that
+general shortcut is not used. An all-idle row allocates no service bank
+and has count zero, not (1).
+
+The other three joined ports have the exact total
+
+    X = 2(H+2) + sum_{b <= i < a+n} h_i + n/2 + 2.        (2)
+
+Coordinate and countdown each attain H bits plus two markers. With a
+nonempty active set, the largest right-axis width is also active: long
+axes are always active, and if all axes are short they are either all
+active or all idle. This uses the retained two-width family. The returned
+stream has one L, all right-coordinate bits, one separator per right
+axis and one R. These three backings are disjoint from the service bank;
+the header and ROM observer wrappers alias it and are counted once.
+Thus `B+X` is exact for the joined non-numerical backing. Erasure returns
+blank cells but does not reduce either quantity.
+
+The h=3 -> h=2 fixture at P=11 retains **9,086 bank cells** after its
+second call. Charging only the last target's fresh requirement, 3,084,
+omits 6,002 retained cells. The reverse order grows 3,084 -> 9,086.
+At P=5,h=2 the exact bank is 1,476 cells. The checker verifies every role's
+extent at every actual invocation, (1), (2), the disjoint storage partition
+and these rejecting controls. The numerical Entry remains separately
+charged. Arbitrary changing-precision numerical histories (JoyboyBrian's #5505) and
+separately allocated later RowQuery instances are outside this lemma.
+
+## Independent finite oracle and controls
+
+No #5496 verifier, retained Caller oracle, `decode_group` or source Beneš
+routine is executed. The finite CRT oracle enumerates k satisfying the
+displayed congruences, and enumerates the unique permitted offset. For
+each small permutation, the network oracle exhausts all binary color
+tuples and takes the lexicographically least tuple satisfying both input
+and output perfect matchings. Each component has two complementary
+colorings, so this is exactly color zero at its least vertex, independently
+of the source DFS's order. Recursing on the two matched children therefore
+reconstructs the canonical layers by a separate code path. All small
+oracle layers are also composed directly and checked against the rotation.
+
+Read-only observers decode actual producer headers and inspect its actual
+outputs before disposal. They check complete layers, selected row, header
+preservation, returned heads, private blanking, identical backing objects,
+and historical tails. They never provide a successful execution's values,
+tables or branches. Input serialization belongs to the test harness and
+is not billed as a new machine implementation.
+
+The actual cases cover two active targets, growing and shrinking widths,
+an idle axis before/after an active one, invalid left padding, current
+padded targets, all-idle behavior, and a nonroot node at `W=h+3` equality.
+Seven execution mutations distinguish stale offsets, wrong row, suppressed
+padded queries, missing full-layer disposal, missing result retirement,
+skipping an idle offset record and replacement backing. Two algebraic
+discriminators separate current-child semantics and the full right prefix;
+two storage controls reject last-width-only and omitted-spool bills;
+one receipt control separates JSON booleans from integers.
+
+The exact values and counts are frozen in RESULT.json. No h=4 pipeline,
+uninterrupted whole level, production-size geometry, raw compact S,
+three-epoch key, binary numerical compiler, full E(p,ell) tariff, native
+supplier, outer theorem or formal-kernel check is established here.
+
+## Credit
+
+The theorem being audited and the joined implementation are JoyboyBrian's
+#5496. Ali Romman supplies #5353's RowEntry. JoyboyBrian supplies #5092's
+ROM producer and #5053/#5219's numerical producer/entry. Hiroki KUMAZAKI
+supplies the current-state CRT contract (#4716) and the #4169/#4174 audits;
+ToikY supplies the explicit-width mixed caller (#4195) and the arena
+refinement (#4192); Cinna Davis supplies #4100's CRT/Beneš construction.
+The retained physical/repair lineage includes Tekalign, Jose Manuel,
+Ryanson Jonathan, unpaidmoon, Douglas Colkitt and John-Michael Smith.
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex
+assistance. Apache-2.0. No independent human or formal-kernel review is claimed.
diff --git a/research/crt-multitarget-row-audit/README.md b/research/crt-multitarget-row-audit/README.md
new file mode 100644
index 0000000000..fd052021bd
--- /dev/null
+++ b/research/crt-multitarget-row-audit/README.md
@@ -0,0 +1,153 @@
+# Independent audit of the multi-target CRT row join
+
+**Scoped positive proof audit with finite exact corroboration; no new κ.**
+PR #5496's current-row join composes across multiple right targets, including
+mixed active/idle axes and a producer bank reused at growing or shrinking
+widths, conditional on its inherited numerical Entry and ROM-producer
+contracts. No defect was found in that implication. This is a separate
+AI-assisted audit, not independent human or formal-kernel acceptance.
+
+The audited source is JoyboyBrian's [PR #5496](https://github.com/CrocSwap/integer-mult-bounds/pull/5496)
+at `a99afd7e0024af8367d5a2f6f4d2da57a1d13dd5`. Its published complete
+joined fixtures have one active target at a time, and its h=4 four-axis
+attempt did not complete. This audit adds the explicit target-loop
+invariant, an exact retained-bank footprint, and executed multi-target
+coverage. It does not redo the construction or present a larger parameter
+sample as a universal proof.
+
+[PROOF.md](PROOF.md) derives the all-admitted-parameter composition from
+the two named source contracts. An idle target still consumes its entire
+numerical record; the next active target therefore receives its own
+offset. Every producer call returns to the same bank, with all old tails
+blank, before the next target starts. Current padded coordinates are
+queried, and the numerical whole-rotation field is never substituted for
+one micro-row. The scope is one successful row invocation and its retirement.
+
+For the unchanged producer's 52-role bank, including all four headers,
+let P be the node's guide width and H its largest active target width.
+The exact retained count is
+
+```text
+B(P,H) = 5 P 2^H (H^2+3H+1) + 2^H(4H-1) + 48P + 2H + 104.
+```
+
+Every role's extent is nondecreasing in h at fixed P; that proved property
+allows a widest-target bound for this specific bank. The h=3 -> h=2 case
+at P=11 still retains 9,086 cells; billing just the final target would count
+3,084 and omit 6,002. The three other joined ports are counted separately
+and exactly in the proof. These are finite-symbol tape cells, excluding
+the numerical Entry and interpreter metadata. No program or recursive
+invoice is changed.
+
+## Evidence
+
+[verify.py](verify.py) executes the unchanged join and unchanged numerical
+and encoded-ROM producers. Its independent oracle searches the small CRT
+congruences and exhausts the two-matching color constraints to reconstruct
+canonical Beneš layers. It imports neither #5496's verifier nor the
+retained Caller/CRT/Beneš reference implementations. Read-only observers
+check the actual headers, every produced layer, selected ROM, bank identity,
+heads, private work and historical tails before the caller disposes of them.
+
+The frozen [RESULT.json](RESULT.json) contains nine actual caller cases and
+13 complete producer invocations. Representative root-node results are:
+
+| Case | Moduli; declared widths | Current state; global row | Right output |
+|---|---|---|---|
+| Two distinct offsets | `(5,7,3,2); (3,3,2,2)` | `(3,2,1,1); 4` | `(1,0)` |
+| Shrinking bank | `(2,5,7,3); (2,3,3,2)` | `(1,4,7,3); 4` | `(6,3)` |
+| Growing bank | `(2,5,3,7); (2,3,2,3)` | `(1,4,3,7); 4` | `(3,6)` |
+| Leading idle target | `(2,5,3,7); (2,3,2,3)` | `(1,4,3,7); 2` | `(3,7)` |
+| Trailing idle target | `(2,5,7,3); (2,3,3,2)` | `(1,4,7,3); 2` | `(3,3)` |
+
+Other cases cover invalid left padding, an all-idle row with zero tape
+work, and a nonroot node at the minimum guide `W=P=h+3=5`. All 63
+numerical owned ports retire. The finite oracle independently checks 32
+networks at all 236 input addresses. Seven execution mutations, two
+algebraic discriminators, two storage controls and one typed-receipt control
+pass. They detect stale offsets, wrong row selection, suppressed padded queries, omitted
+layer/result disposal, skipped idle records, replacement backing, omitted
+right prefixes, original/current-coordinate confusion, and boolean/integer
+receipt confusion. The storage controls reject a last-target-only bill
+and omission of the retained spool.
+
+The adapter's tape actions are measured separately from the expensive
+Entry and ROM calls and remain within the inherited `4096F` allowance.
+This does not independently certify its full control-instruction constant
+or the inherited arithmetic bill. Distinct backing identities and an
+independent bank-plus-three-extras partition prevent alias double counting
+and omitted producer storage.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B scripts/research_package.py --package research/crt-multitarget-row-audit --check-only
+python3 -B scripts/research_package.py --package research/crt-multitarget-row-audit
+```
+
+The registered replay runs normal and optimized Python serially, with a
+300-second limit for each. Each concludes:
+
+```text
+PASS_CRT_MULTITARGET_ROW_AUDIT cases=9 producer_calls=13 controls=12 no_new_kappa=true
+```
+
+The normal replay compares the existing receipt and writes no evidence.
+`--write-result` explicitly regenerates it. `--case growing_bank` selects
+one diagnostic without claiming the complete package pass.
+
+The audited pending source is vendored byte-for-byte, with its original
+credit, paths, commit, Git blobs and hashes in [VENDORED.json](VENDORED.json).
+The twelve scientific main-branch inputs are pinned in [SOURCES.json](SOURCES.json)
+and declared in [VERIFY.json](VERIFY.json). The export also retains the
+repository license and three original source notices. No pending Git object
+or live GitHub access is required for direct replay. Generic provenance validation
+still requires the package's main-branch Git history.
+
+## Scope and remaining obligations
+
+The base is `32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority revision 7;
+the task is `uniform-transfer-audit`, refined to this actual CRT caller.
+[TASK.json](TASK.json) records selection and overlap. Coordination is in
+[Discussion #4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709),
+following #5496's comment 19173182. JoyboyBrian's #5505 (cross-session
+numerical bank reuse) and #5486 (fixed repair binary lowering) are
+separate work.
+
+The numerical and producer theorems, initial encoded input production,
+uninterrupted whole-level updates, three-epoch key transport, production
+geometry, binary numerical compilation, complete E(p,ell), native/outer
+admission and the full multiplication theorem are not independently
+validated here. No h=4 joined replay, Lean build or selected replay is run.
+The selected record and all frozen predecessor files are unchanged.
+
+## Open next questions
+
+1. Connect this returned coordinate stream to a paid update of the actual
+   axis-record source, then invoke the next row without host serialization.
+   This would test the next physical caller boundary. Start with the
+   five-row mixed h=3/h=2 example; the source ownership/update contract is
+   the missing premise. PR5496 already identifies this task; it remains open.
+2. Join one complete three-epoch exceptional key to these actual current-row
+   inputs. Start with PR4716's two stale-offset discriminators and explicitly
+   price each source-coordinate conversion and restoration. A proved
+   single-row loop does not supply those changing-left-state descriptors.
+
+The family decision is to stop after this audit; neither a larger ROM
+sample nor a complete ordinary/outer run is justified by this result alone.
+
+## Credit
+
+Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance.
+
+JoyboyBrian supplies #5496's join, #5092's ROM producer and #5053/#5219's
+numerical components. Ali Romman supplies #5353's actual RowEntry.
+Hiroki KUMAZAKI supplies the current-state CRT contract (#4716) and the
+#4169/#4174 repair and mixed-width reservoir audits; Cinna Davis supplies
+#4100's construction; ToikY supplies the explicit-width mixed caller
+(#4195) and the Beneš arena refinement (#4192). Tekalign, Jose Manuel, Ryanson Jonathan, unpaidmoon, Douglas
+Colkitt, John-Michael Smith and the retained source notices preserve the
+physical/repair lineage. [vendor/NOTICE.md](vendor/NOTICE.md) identifies
+the copied material. Apache-2.0. No independent human review is claimed.
diff --git a/research/crt-multitarget-row-audit/RESULT.json b/research/crt-multitarget-row-audit/RESULT.json
new file mode 100644
index 0000000000..ed91a218b6
--- /dev/null
+++ b/research/crt-multitarget-row-audit/RESULT.json
@@ -0,0 +1,1835 @@
+{
+  "status": "PASS_CRT_MULTITARGET_ROW_AUDIT",
+  "sources": {
+    "research/crt-encoded-benes-rom-producer/PROOF.md": "93bd340ac9b77f8f781926aeb7327325789b331863b3088fed1809eefb789bd2",
+    "research/crt-encoded-benes-rom-producer/microcode.py": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7",
+    "research/crt-mixed-row-entry/PROOF.md": "8a529ece497c62d5225261cdacebfd88979322b3a8886d1a31eb6295f1989e4b",
+    "research/crt-mixed-row-entry/bridge.py": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9",
+    "research/crt-mixed-width-caller/verify.py": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45",
+    "research/encoded-crt-entry-lifecycle/PROOF.md": "a619be48c8c85749ea5411929aa6ff3986443b467133d32d19d543250b0054b0",
+    "research/encoded-crt-entry-lifecycle/entry.py": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7",
+    "research/encoded-current-crt/PROOF.md": "7da614e737414a373c8716158f2c02a52666620ea1f114fac7ca09b3b38489bc",
+    "research/encoded-current-crt/producer.py": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76",
+    "research/r437-preparation-composition/predecessor4025/source/records.py": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372",
+    "research/r437-preparation-composition/predecessor4025/source/words.py": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9",
+    "research/unconditional-batched-crt/CRT.md": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b",
+    "vendor/pr5496-join.py": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35",
+    "vendor/pr5496-PROOF.md": "6aaa6253bf5f64f07cbfbf0a98a7c464e5a78cfa05c398f7eb41a27f03a7379c",
+    "vendor/pr5496-README.md": "41a14eb0d72c1ecce16a791b8f32d84f8c0b4e089c5e66a19067218e56d48db0"
+  },
+  "oracle": {
+    "networks": 32,
+    "addresses": 236
+  },
+  "cases": [
+    {
+      "name": "two_short_first",
+      "idle": false,
+      "lower": 11,
+      "precision": 11,
+      "offsets": [
+        1,
+        1
+      ],
+      "output": [
+        3,
+        1
+      ],
+      "calls": [
+        {
+          "axis": 2,
+          "headers": {
+            "h": 2,
+            "modulus": 3,
+            "selected_layer": 0,
+            "offsets": 1
+          },
+          "instructions": 4841091,
+          "before_extents": {
+            "zero": 1,
+            "one": 1,
+            "two": 1,
+            "root": 1,
+            "n": 1,
+            "remaining": 1,
+            "depth": 1,
+            "height": 1,
+            "low": 1,
+            "high": 1,
+            "size": 1,
+            "cur_node": 1,
+            "init_kind": 1,
+            "init_layer": 1,
+            "init_index": 1,
+            "init_value": 1,
+            "limit": 1,
+            "xloop": 1,
+            "yloop": 1,
+            "px": 1,
+            "py": 1,
+            "node": 1,
+            "kind": 1,
+            "layer": 1,
+            "index": 1,
+            "value": 1,
+            "x": 1,
+            "other": 1,
+            "opposite": 1,
+            "color": 1,
+            "initial": 1,
+            "top": 1,
+            "off": 1,
+            "permuted": 1,
+            "addition": 1,
+            "child": 1,
+            "child_index": 1,
+            "inverse": 1,
+            "last": 1,
+            "outlayer": 1,
+            "layloop": 1,
+            "layers_count": 1,
+            "column": 1,
+            "check": 1,
+            "arena": 1,
+            "spool": 1,
+            "layers": 1,
+            "rom": 1,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "dde2ad20159724d288bd6145d77bd8e8bec7db9a36ceb42ebc2c6d3c045d46b1"
+        },
+        {
+          "axis": 3,
+          "headers": {
+            "h": 2,
+            "modulus": 2,
+            "selected_layer": 0,
+            "offsets": 1
+          },
+          "instructions": 4840616,
+          "before_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "93e452c83710ef6b736c4defcb57da7a2d7c46f9c143051960441230c2bccba4"
+        }
+      ],
+      "adapter_tape_actions": 2421,
+      "adapter_bound": 749568,
+      "owned_retained_cells": 4052,
+      "numerical_owned_roles": 63,
+      "producer_retained_cells": 3084,
+      "extra_retained_cells": 16,
+      "expected_query_coordinates": [
+        2,
+        1
+      ]
+    },
+    {
+      "name": "two_short_distinct_offsets",
+      "idle": false,
+      "lower": 3,
+      "precision": 11,
+      "offsets": [
+        0,
+        1
+      ],
+      "output": [
+        1,
+        0
+      ],
+      "calls": [
+        {
+          "axis": 2,
+          "headers": {
+            "h": 2,
+            "modulus": 3,
+            "selected_layer": 2,
+            "offsets": 0
+          },
+          "instructions": 4840097,
+          "before_extents": {
+            "zero": 1,
+            "one": 1,
+            "two": 1,
+            "root": 1,
+            "n": 1,
+            "remaining": 1,
+            "depth": 1,
+            "height": 1,
+            "low": 1,
+            "high": 1,
+            "size": 1,
+            "cur_node": 1,
+            "init_kind": 1,
+            "init_layer": 1,
+            "init_index": 1,
+            "init_value": 1,
+            "limit": 1,
+            "xloop": 1,
+            "yloop": 1,
+            "px": 1,
+            "py": 1,
+            "node": 1,
+            "kind": 1,
+            "layer": 1,
+            "index": 1,
+            "value": 1,
+            "x": 1,
+            "other": 1,
+            "opposite": 1,
+            "color": 1,
+            "initial": 1,
+            "top": 1,
+            "off": 1,
+            "permuted": 1,
+            "addition": 1,
+            "child": 1,
+            "child_index": 1,
+            "inverse": 1,
+            "last": 1,
+            "outlayer": 1,
+            "layloop": 1,
+            "layers_count": 1,
+            "column": 1,
+            "check": 1,
+            "arena": 1,
+            "spool": 1,
+            "layers": 1,
+            "rom": 1,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "93e452c83710ef6b736c4defcb57da7a2d7c46f9c143051960441230c2bccba4"
+        },
+        {
+          "axis": 3,
+          "headers": {
+            "h": 2,
+            "modulus": 2,
+            "selected_layer": 2,
+            "offsets": 1
+          },
+          "instructions": 4840617,
+          "before_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "5017425c34a54778a5b1aad8170a2c8f8ef83f00aa88b1e49c00774e5fe73e33"
+        }
+      ],
+      "adapter_tape_actions": 2394,
+      "adapter_bound": 749568,
+      "owned_retained_cells": 4051,
+      "numerical_owned_roles": 63,
+      "producer_retained_cells": 3084,
+      "extra_retained_cells": 16,
+      "expected_query_coordinates": [
+        1,
+        1
+      ]
+    },
+    {
+      "name": "shrinking_bank",
+      "idle": false,
+      "lower": 3,
+      "precision": 11,
+      "offsets": [
+        1,
+        0
+      ],
+      "output": [
+        6,
+        3
+      ],
+      "calls": [
+        {
+          "axis": 2,
+          "headers": {
+            "h": 3,
+            "modulus": 7,
+            "selected_layer": 4,
+            "offsets": 1
+          },
+          "instructions": 64964341,
+          "before_extents": {
+            "zero": 1,
+            "one": 1,
+            "two": 1,
+            "root": 1,
+            "n": 1,
+            "remaining": 1,
+            "depth": 1,
+            "height": 1,
+            "low": 1,
+            "high": 1,
+            "size": 1,
+            "cur_node": 1,
+            "init_kind": 1,
+            "init_layer": 1,
+            "init_index": 1,
+            "init_value": 1,
+            "limit": 1,
+            "xloop": 1,
+            "yloop": 1,
+            "px": 1,
+            "py": 1,
+            "node": 1,
+            "kind": 1,
+            "layer": 1,
+            "index": 1,
+            "value": 1,
+            "x": 1,
+            "other": 1,
+            "opposite": 1,
+            "color": 1,
+            "initial": 1,
+            "top": 1,
+            "off": 1,
+            "permuted": 1,
+            "addition": 1,
+            "child": 1,
+            "child_index": 1,
+            "inverse": 1,
+            "last": 1,
+            "outlayer": 1,
+            "layloop": 1,
+            "layers_count": 1,
+            "column": 1,
+            "check": 1,
+            "arena": 1,
+            "spool": 1,
+            "layers": 1,
+            "rom": 1,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 8362,
+            "spool": 42,
+            "layers": 47,
+            "rom": 10,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "09fd8e4e5c2c1c30bdd3d930b7874ec4c272a610da1058565b4c8e3d228b6865"
+        },
+        {
+          "axis": 3,
+          "headers": {
+            "h": 2,
+            "modulus": 3,
+            "selected_layer": 2,
+            "offsets": 0
+          },
+          "instructions": 4840097,
+          "before_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 8362,
+            "spool": 42,
+            "layers": 47,
+            "rom": 10,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 8362,
+            "spool": 42,
+            "layers": 47,
+            "rom": 10,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "37631d3c52ba6f3c5bd563f6018a099d730314a2dcb08d1403d9ad92fc68ec00"
+        }
+      ],
+      "adapter_tape_actions": 2847,
+      "adapter_bound": 958464,
+      "owned_retained_cells": 10059,
+      "numerical_owned_roles": 63,
+      "producer_retained_cells": 9086,
+      "extra_retained_cells": 19,
+      "expected_query_coordinates": [
+        7,
+        3
+      ]
+    },
+    {
+      "name": "growing_bank",
+      "idle": false,
+      "lower": 3,
+      "precision": 11,
+      "offsets": [
+        0,
+        5
+      ],
+      "output": [
+        3,
+        6
+      ],
+      "calls": [
+        {
+          "axis": 2,
+          "headers": {
+            "h": 2,
+            "modulus": 3,
+            "selected_layer": 2,
+            "offsets": 0
+          },
+          "instructions": 4840097,
+          "before_extents": {
+            "zero": 1,
+            "one": 1,
+            "two": 1,
+            "root": 1,
+            "n": 1,
+            "remaining": 1,
+            "depth": 1,
+            "height": 1,
+            "low": 1,
+            "high": 1,
+            "size": 1,
+            "cur_node": 1,
+            "init_kind": 1,
+            "init_layer": 1,
+            "init_index": 1,
+            "init_value": 1,
+            "limit": 1,
+            "xloop": 1,
+            "yloop": 1,
+            "px": 1,
+            "py": 1,
+            "node": 1,
+            "kind": 1,
+            "layer": 1,
+            "index": 1,
+            "value": 1,
+            "x": 1,
+            "other": 1,
+            "opposite": 1,
+            "color": 1,
+            "initial": 1,
+            "top": 1,
+            "off": 1,
+            "permuted": 1,
+            "addition": 1,
+            "child": 1,
+            "child_index": 1,
+            "inverse": 1,
+            "last": 1,
+            "outlayer": 1,
+            "layloop": 1,
+            "layers_count": 1,
+            "column": 1,
+            "check": 1,
+            "arena": 1,
+            "spool": 1,
+            "layers": 1,
+            "rom": 1,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "93e452c83710ef6b736c4defcb57da7a2d7c46f9c143051960441230c2bccba4"
+        },
+        {
+          "axis": 3,
+          "headers": {
+            "h": 3,
+            "modulus": 7,
+            "selected_layer": 4,
+            "offsets": 5
+          },
+          "instructions": 64975266,
+          "before_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 8362,
+            "spool": 42,
+            "layers": 47,
+            "rom": 10,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "f03d7eaeeab75bb49b3652cdf9353617e0b7f27d7e4c24dcdb91985803687417"
+        }
+      ],
+      "adapter_tape_actions": 2847,
+      "adapter_bound": 958464,
+      "owned_retained_cells": 10059,
+      "numerical_owned_roles": 63,
+      "producer_retained_cells": 9086,
+      "extra_retained_cells": 19,
+      "expected_query_coordinates": [
+        3,
+        7
+      ]
+    },
+    {
+      "name": "leading_idle",
+      "idle": false,
+      "lower": 3,
+      "precision": 11,
+      "offsets": [
+        0,
+        5
+      ],
+      "output": [
+        3,
+        7
+      ],
+      "calls": [
+        {
+          "axis": 3,
+          "headers": {
+            "h": 3,
+            "modulus": 7,
+            "selected_layer": 2,
+            "offsets": 5
+          },
+          "instructions": 64975266,
+          "before_extents": {
+            "zero": 1,
+            "one": 1,
+            "two": 1,
+            "root": 1,
+            "n": 1,
+            "remaining": 1,
+            "depth": 1,
+            "height": 1,
+            "low": 1,
+            "high": 1,
+            "size": 1,
+            "cur_node": 1,
+            "init_kind": 1,
+            "init_layer": 1,
+            "init_index": 1,
+            "init_value": 1,
+            "limit": 1,
+            "xloop": 1,
+            "yloop": 1,
+            "px": 1,
+            "py": 1,
+            "node": 1,
+            "kind": 1,
+            "layer": 1,
+            "index": 1,
+            "value": 1,
+            "x": 1,
+            "other": 1,
+            "opposite": 1,
+            "color": 1,
+            "initial": 1,
+            "top": 1,
+            "off": 1,
+            "permuted": 1,
+            "addition": 1,
+            "child": 1,
+            "child_index": 1,
+            "inverse": 1,
+            "last": 1,
+            "outlayer": 1,
+            "layloop": 1,
+            "layers_count": 1,
+            "column": 1,
+            "check": 1,
+            "arena": 1,
+            "spool": 1,
+            "layers": 1,
+            "rom": 1,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 8362,
+            "spool": 42,
+            "layers": 47,
+            "rom": 10,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "83d33e46490d16971097885c682fa255bbd966a99e738744fdc000718af3e8bb"
+        }
+      ],
+      "adapter_tape_actions": 1987,
+      "adapter_bound": 815104,
+      "owned_retained_cells": 10059,
+      "numerical_owned_roles": 63,
+      "producer_retained_cells": 9086,
+      "extra_retained_cells": 19,
+      "expected_query_coordinates": [
+        7
+      ]
+    },
+    {
+      "name": "trailing_idle",
+      "idle": false,
+      "lower": 3,
+      "precision": 11,
+      "offsets": [
+        1,
+        0
+      ],
+      "output": [
+        3,
+        3
+      ],
+      "calls": [
+        {
+          "axis": 2,
+          "headers": {
+            "h": 3,
+            "modulus": 7,
+            "selected_layer": 2,
+            "offsets": 1
+          },
+          "instructions": 64964341,
+          "before_extents": {
+            "zero": 1,
+            "one": 1,
+            "two": 1,
+            "root": 1,
+            "n": 1,
+            "remaining": 1,
+            "depth": 1,
+            "height": 1,
+            "low": 1,
+            "high": 1,
+            "size": 1,
+            "cur_node": 1,
+            "init_kind": 1,
+            "init_layer": 1,
+            "init_index": 1,
+            "init_value": 1,
+            "limit": 1,
+            "xloop": 1,
+            "yloop": 1,
+            "px": 1,
+            "py": 1,
+            "node": 1,
+            "kind": 1,
+            "layer": 1,
+            "index": 1,
+            "value": 1,
+            "x": 1,
+            "other": 1,
+            "opposite": 1,
+            "color": 1,
+            "initial": 1,
+            "top": 1,
+            "off": 1,
+            "permuted": 1,
+            "addition": 1,
+            "child": 1,
+            "child_index": 1,
+            "inverse": 1,
+            "last": 1,
+            "outlayer": 1,
+            "layloop": 1,
+            "layers_count": 1,
+            "column": 1,
+            "check": 1,
+            "arena": 1,
+            "spool": 1,
+            "layers": 1,
+            "rom": 1,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 8362,
+            "spool": 42,
+            "layers": 47,
+            "rom": 10,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "0679f9b24e701db7288294c7921ca619aa90e1e22aabf1dfd2c29b01d4892b60"
+        }
+      ],
+      "adapter_tape_actions": 1987,
+      "adapter_bound": 815104,
+      "owned_retained_cells": 10059,
+      "numerical_owned_roles": 63,
+      "producer_retained_cells": 9086,
+      "extra_retained_cells": 19,
+      "expected_query_coordinates": [
+        7
+      ]
+    },
+    {
+      "name": "invalid_left",
+      "idle": false,
+      "lower": 0,
+      "precision": 11,
+      "offsets": [
+        0,
+        0
+      ],
+      "output": [
+        3,
+        1
+      ],
+      "calls": [
+        {
+          "axis": 2,
+          "headers": {
+            "h": 2,
+            "modulus": 3,
+            "selected_layer": 2,
+            "offsets": 0
+          },
+          "instructions": 4840097,
+          "before_extents": {
+            "zero": 1,
+            "one": 1,
+            "two": 1,
+            "root": 1,
+            "n": 1,
+            "remaining": 1,
+            "depth": 1,
+            "height": 1,
+            "low": 1,
+            "high": 1,
+            "size": 1,
+            "cur_node": 1,
+            "init_kind": 1,
+            "init_layer": 1,
+            "init_index": 1,
+            "init_value": 1,
+            "limit": 1,
+            "xloop": 1,
+            "yloop": 1,
+            "px": 1,
+            "py": 1,
+            "node": 1,
+            "kind": 1,
+            "layer": 1,
+            "index": 1,
+            "value": 1,
+            "x": 1,
+            "other": 1,
+            "opposite": 1,
+            "color": 1,
+            "initial": 1,
+            "top": 1,
+            "off": 1,
+            "permuted": 1,
+            "addition": 1,
+            "child": 1,
+            "child_index": 1,
+            "inverse": 1,
+            "last": 1,
+            "outlayer": 1,
+            "layloop": 1,
+            "layers_count": 1,
+            "column": 1,
+            "check": 1,
+            "arena": 1,
+            "spool": 1,
+            "layers": 1,
+            "rom": 1,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "93e452c83710ef6b736c4defcb57da7a2d7c46f9c143051960441230c2bccba4"
+        },
+        {
+          "axis": 3,
+          "headers": {
+            "h": 2,
+            "modulus": 2,
+            "selected_layer": 2,
+            "offsets": 0
+          },
+          "instructions": 4839788,
+          "before_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "after_extents": {
+            "zero": 13,
+            "one": 13,
+            "two": 13,
+            "root": 13,
+            "n": 13,
+            "remaining": 13,
+            "depth": 13,
+            "height": 13,
+            "low": 13,
+            "high": 13,
+            "size": 13,
+            "cur_node": 13,
+            "init_kind": 13,
+            "init_layer": 13,
+            "init_index": 13,
+            "init_value": 13,
+            "limit": 13,
+            "xloop": 13,
+            "yloop": 13,
+            "px": 13,
+            "py": 13,
+            "node": 13,
+            "kind": 13,
+            "layer": 13,
+            "index": 13,
+            "value": 13,
+            "x": 13,
+            "other": 13,
+            "opposite": 13,
+            "color": 13,
+            "initial": 13,
+            "top": 13,
+            "off": 13,
+            "permuted": 13,
+            "addition": 13,
+            "child": 13,
+            "child_index": 13,
+            "inverse": 13,
+            "last": 13,
+            "outlayer": 13,
+            "layloop": 13,
+            "layers_count": 13,
+            "column": 13,
+            "check": 13,
+            "arena": 2422,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 13,
+            "modulus": 13,
+            "selected_layer": 13,
+            "offsets": 14
+          },
+          "rom_sha256": "93e452c83710ef6b736c4defcb57da7a2d7c46f9c143051960441230c2bccba4"
+        }
+      ],
+      "adapter_tape_actions": 2442,
+      "adapter_bound": 749568,
+      "owned_retained_cells": 4054,
+      "numerical_owned_roles": 63,
+      "producer_retained_cells": 3084,
+      "extra_retained_cells": 16,
+      "expected_query_coordinates": [
+        3,
+        1
+      ]
+    },
+    {
+      "name": "all_idle",
+      "idle": true,
+      "calls": [],
+      "lower": 11
+    },
+    {
+      "name": "nonroot_minimum_guide",
+      "idle": false,
+      "lower": 1,
+      "precision": 5,
+      "offsets": [
+        1
+      ],
+      "output": [
+        0
+      ],
+      "calls": [
+        {
+          "axis": 3,
+          "headers": {
+            "h": 2,
+            "modulus": 2,
+            "selected_layer": 2,
+            "offsets": 1
+          },
+          "instructions": 2363817,
+          "before_extents": {
+            "zero": 1,
+            "one": 1,
+            "two": 1,
+            "root": 1,
+            "n": 1,
+            "remaining": 1,
+            "depth": 1,
+            "height": 1,
+            "low": 1,
+            "high": 1,
+            "size": 1,
+            "cur_node": 1,
+            "init_kind": 1,
+            "init_layer": 1,
+            "init_index": 1,
+            "init_value": 1,
+            "limit": 1,
+            "xloop": 1,
+            "yloop": 1,
+            "px": 1,
+            "py": 1,
+            "node": 1,
+            "kind": 1,
+            "layer": 1,
+            "index": 1,
+            "value": 1,
+            "x": 1,
+            "other": 1,
+            "opposite": 1,
+            "color": 1,
+            "initial": 1,
+            "top": 1,
+            "off": 1,
+            "permuted": 1,
+            "addition": 1,
+            "child": 1,
+            "child_index": 1,
+            "inverse": 1,
+            "last": 1,
+            "outlayer": 1,
+            "layloop": 1,
+            "layers_count": 1,
+            "column": 1,
+            "check": 1,
+            "arena": 1,
+            "spool": 1,
+            "layers": 1,
+            "rom": 1,
+            "h": 7,
+            "modulus": 7,
+            "selected_layer": 7,
+            "offsets": 8
+          },
+          "after_extents": {
+            "zero": 7,
+            "one": 7,
+            "two": 7,
+            "root": 7,
+            "n": 7,
+            "remaining": 7,
+            "depth": 7,
+            "height": 7,
+            "low": 7,
+            "high": 7,
+            "size": 7,
+            "cur_node": 7,
+            "init_kind": 7,
+            "init_layer": 7,
+            "init_index": 7,
+            "init_value": 7,
+            "limit": 7,
+            "xloop": 7,
+            "yloop": 7,
+            "px": 7,
+            "py": 7,
+            "node": 7,
+            "kind": 7,
+            "layer": 7,
+            "index": 7,
+            "value": 7,
+            "x": 7,
+            "other": 7,
+            "opposite": 7,
+            "color": 7,
+            "initial": 7,
+            "top": 7,
+            "off": 7,
+            "permuted": 7,
+            "addition": 7,
+            "child": 7,
+            "child_index": 7,
+            "inverse": 7,
+            "last": 7,
+            "outlayer": 7,
+            "layloop": 7,
+            "layers_count": 7,
+            "column": 7,
+            "check": 7,
+            "arena": 1102,
+            "spool": 14,
+            "layers": 17,
+            "rom": 6,
+            "h": 7,
+            "modulus": 7,
+            "selected_layer": 7,
+            "offsets": 8
+          },
+          "rom_sha256": "5017425c34a54778a5b1aad8170a2c8f8ef83f00aa88b1e49c00774e5fe73e33"
+        }
+      ],
+      "adapter_tape_actions": 916,
+      "adapter_bound": 425984,
+      "owned_retained_cells": 1960,
+      "numerical_owned_roles": 63,
+      "producer_retained_cells": 1476,
+      "extra_retained_cells": 13,
+      "expected_query_coordinates": [
+        1
+      ]
+    }
+  ],
+  "controls": [
+    {
+      "name": "stale_zero_offset",
+      "rejected_by": "current target header correspondence"
+    },
+    {
+      "name": "wrong_local_row",
+      "rejected_by": "current target header correspondence"
+    },
+    {
+      "name": "suppress_padded_query",
+      "rejected_by": "independent micro-row endpoint"
+    },
+    {
+      "name": "omit_layers_disposal",
+      "rejected_by": "blank producer reentry including old tails"
+    },
+    {
+      "name": "omit_result_retirement",
+      "rejected_by": "joined retirement including result"
+    },
+    {
+      "name": "skip_idle_offset_record",
+      "rejected_by": "offset record end"
+    },
+    {
+      "name": "replace_bank_between_targets",
+      "rejected_by": "same producer bank at next target"
+    },
+    {
+      "name": "omit_preceding_right_modulus",
+      "correct": 5,
+      "wrong": 1
+    },
+    {
+      "name": "treat_current_as_original_digits",
+      "correct": 11,
+      "wrong": 26
+    },
+    {
+      "name": "bill_only_final_smaller_target",
+      "rejected_by": "exact shared-bank footprint"
+    },
+    {
+      "name": "omit_retained_spool",
+      "rejected_by": "complete bank includes spool"
+    },
+    {
+      "name": "boolean_integer_receipt_collision",
+      "rejected": true
+    }
+  ],
+  "producer_calls": 13
+}
diff --git a/research/crt-multitarget-row-audit/SOURCES.json b/research/crt-multitarget-row-audit/SOURCES.json
new file mode 100644
index 0000000000..3c998361ff
--- /dev/null
+++ b/research/crt-multitarget-row-audit/SOURCES.json
@@ -0,0 +1,114 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/crt-encoded-benes-rom-producer/PROOF.md",
+      "usage": "input",
+      "git_blob": "cdd530c668254558bb1ef8a6c6af9a5660f8f9c2",
+      "sha256": "93bd340ac9b77f8f781926aeb7327325789b331863b3088fed1809eefb789bd2"
+    },
+    {
+      "path": "research/crt-encoded-benes-rom-producer/microcode.py",
+      "usage": "input",
+      "git_blob": "052b01a83bc910c176b83a012b9f46f0e9525b9d",
+      "sha256": "d4af5350854a87b67484840800b94e1e53cff82c78ec0f2a91753fed9ea70af7"
+    },
+    {
+      "path": "research/crt-mixed-row-entry/PROOF.md",
+      "usage": "input",
+      "git_blob": "76e75e002b5c5860a43b2fe6313ba4339efcc3ff",
+      "sha256": "8a529ece497c62d5225261cdacebfd88979322b3a8886d1a31eb6295f1989e4b"
+    },
+    {
+      "path": "research/crt-mixed-row-entry/bridge.py",
+      "usage": "input",
+      "git_blob": "57f6853e262a6136bc616f1e47a31d0ace28495c",
+      "sha256": "89c38638c0d66da731566c903c32e7fa1ad31088d29cfd2634fce823dd07c1f9"
+    },
+    {
+      "path": "research/crt-mixed-width-caller/verify.py",
+      "usage": "input",
+      "git_blob": "7980582b86e8d20269ae32252ad03896eff1131b",
+      "sha256": "5e62787f3c4a8f1175ca7dea6c6b8ceff7863a3f879abd6245faf6aeb272fd45"
+    },
+    {
+      "path": "research/encoded-crt-entry-lifecycle/PROOF.md",
+      "usage": "input",
+      "git_blob": "8c9d971a3d3e5a75637e3279ed8f7f89b0c6a566",
+      "sha256": "a619be48c8c85749ea5411929aa6ff3986443b467133d32d19d543250b0054b0"
+    },
+    {
+      "path": "research/encoded-crt-entry-lifecycle/entry.py",
+      "usage": "input",
+      "git_blob": "1fa2b0cb88320d4f5b623554bb0fc6de332b773c",
+      "sha256": "0537ec98f306270c8ff6a424841886cf53f675d9947029347090c7dc779616d7"
+    },
+    {
+      "path": "research/encoded-current-crt/PROOF.md",
+      "usage": "input",
+      "git_blob": "286ab05ba7ab500e5b86268384545dcec8862d1c",
+      "sha256": "7da614e737414a373c8716158f2c02a52666620ea1f114fac7ca09b3b38489bc"
+    },
+    {
+      "path": "research/encoded-current-crt/producer.py",
+      "usage": "input",
+      "git_blob": "a327b0161eca57a1cc44ec2aa8e3defed2167ddc",
+      "sha256": "88dab4ca02a92164a67826db361214fa1405e4b4a588f8c4279a21bcee95ab76"
+    },
+    {
+      "path": "research/r437-preparation-composition/predecessor4025/source/records.py",
+      "usage": "input",
+      "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3",
+      "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372"
+    },
+    {
+      "path": "research/r437-preparation-composition/predecessor4025/source/words.py",
+      "usage": "input",
+      "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50",
+      "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9"
+    },
+    {
+      "path": "research/unconditional-batched-crt/CRT.md",
+      "usage": "input",
+      "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6",
+      "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b"
+    },
+    {
+      "path": "LICENSE",
+      "usage": "provenance",
+      "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64",
+      "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4"
+    },
+    {
+      "path": "research/unconditional-batched-crt/NOTICE.md",
+      "usage": "provenance",
+      "git_blob": "886a8fdee275f01b459cbd68ae2815dc9269502f",
+      "sha256": "924109837e71c52392191710d49c9deb42780878d1094f0b01e8690dbe799461"
+    },
+    {
+      "path": "research/r437-preparation-composition/predecessor4025/source/NOTICE.md",
+      "usage": "provenance",
+      "git_blob": "ef9f81510db86eaf2f0a7191d85e92a6db30ddc0",
+      "sha256": "c446b32b8a621844fb2fbe654810c8122035bdd43fed2132f1137d98cb6f9943"
+    },
+    {
+      "path": "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md",
+      "usage": "provenance",
+      "git_blob": "6ca47019de7e58edf93c4278a6a8251625d37477",
+      "sha256": "b886589be7c8b87bcf12b14ce4db6827299b7cec93836ed22cff81aed37623dc"
+    }
+  ]
+}
diff --git a/research/crt-multitarget-row-audit/TASK.json b/research/crt-multitarget-row-audit/TASK.json
new file mode 100644
index 0000000000..8442871d9e
--- /dev/null
+++ b/research/crt-multitarget-row-audit/TASK.json
@@ -0,0 +1,139 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "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": "Independently audit PR5496 RowQuery multi-target stream consumption, mixed active/idle targets, physical ROM-bank reuse and successful retirement, under the retained numerical Entry and producer contracts. Derive the exact fixed-P singleton-ROM shared-bank footprint and its three disjoint extra ports.",
+  "scope_change_reason": "The revision-7 card names one actual caller-bound CRT implication. Successor PR5496 supplies the concrete join; its completed fixtures have one active target, so this audit derives the target-loop invariant and adds independently checked multi-target boundary executions. The same rolewise reuse audit sharpens the bank storage accounting without changing the implementation or recursive invoice.",
+  "bottleneck_link": "CRT total repair needs correct current-state physical queries. This audits one necessary composition implication without treating it as complete all-size transfer or supplier admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at a source-relative proof or exact counterexample for this one loop, with h<=3 producer executions and no full native, ordinary, outer or production-size replay.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the quantified conditional audit; RESULT.json freezes nine caller cases, thirteen complete producer invocations, 32 independent oracle networks/236 addresses and twelve control groups. No defect found in the audited implication; inherited theorems remain hypotheses. The bank footprint B(P,H)=5P*2^H*(H^2+3H+1)+2^H*(4H-1)+48P+2H+104 follows from the literal arena/serialization loops and componentwise monotonicity at fixed P.",
+  "author": "commdata2338",
+  "ai_assistance": "Substantial OpenAI Codex (GPT-6 Astra) assistance in derivation, implementation, checking and writing. No independent human or formal-kernel review is claimed.",
+  "open_questions": [
+    {
+      "question": "Update the actual encoded axis source with the returned coordinate stream and execute the next row without host serialization.",
+      "why_it_matters": "This is the next physical whole-level composition boundary after the audited single-row service.",
+      "first_step": "Use the five-row mixed h=3/h=2 example and price an in-place coordinate splice with input/ownership invariants.",
+      "blocked_by": "A caller update/ownership contract and its paid implementation; the row output itself is available."
+    },
+    {
+      "question": "Compose the service at all three current-state epochs of an exceptional reverse key.",
+      "why_it_matters": "A current-row audit does not close CRT total repair or justify freezing the left-state offset.",
+      "first_step": "Bind actual encoded source descriptors at PR4716's two stale-offset discriminator states and retain all conversions/restorations.",
+      "blocked_by": "Physical current-state descriptor production and complete key/caller tariff."
+    }
+  ],
+  "scope_key": "ce7411fb7cf6f3460bfc",
+  "scope_refinement": "pr5496-multi-target-current-row-bank-invariant",
+  "selection": {
+    "seed": "44f05f574fc586d49962b167a149c6d8",
+    "track": "adversarial-audit",
+    "chosen_suggestion": 2,
+    "priority_revision": 7,
+    "alternatives": [
+      {
+        "task": "census-pruning-audit",
+        "reason": "Earlier account PR3215 audits that family; the concrete CRT implication is a current central question."
+      },
+      {
+        "task": "supplier-boundary-audit",
+        "reason": "Complete mixed admission exceeds this scoped session; current source-sensitive successor work is separate."
+      }
+    ],
+    "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19173182",
+    "existing_checks": "PR4100 author construction; PR5496 complete single-active-target h=2 pipeline and four controls. Its h=4 four-axis attempt was incomplete. This audit does not reuse its verifier.",
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19173680"
+  },
+  "dependency_heads": {
+    "PR5496": "a99afd7e0024af8367d5a2f6f4d2da57a1d13dd5",
+    "PR5353": "07a135eee3a8da9392c4a1e01d4b89db05b4ac03",
+    "main_input_pin": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+    "PR4100": "337d04939571a637aeab54a0f58f54fde811663a"
+  },
+  "boundary": {
+    "inputs": "One sequential padded-axis source, eight protected numerical ports, compiled node/row/width topology and blank new owned backing.",
+    "output": "Ordered right-axis micro-row stream; idle targets unchanged; source and protected ports restored.",
+    "cleanup": "Full produced layers, selected ROM, headers, coordinate/countdown scratch and all numerical owned ports; caller retires returned stream with close.",
+    "inherited": "Numerical Entry and encoded ROM producer success theorems and their stated tariffs.",
+    "not_claimed": "Whole-level input update, three-epoch key, full E(p,ell), binary numerical compiler, supplier admission or new kappa.",
+    "storage": "Exact 52-role ROM-bank and three-extra-port cell counts for one fresh RowQuery, including retained old tails; numerical Entry and any external initial blank reserve remain separate."
+  },
+  "family_decision": "Narrow and stop after this independent audit. All consumer/whole-key costs remain explicit; no larger dependent search.",
+  "overlap": {
+    "open_prs_fetched_at": "2026-10-25T05:11:23.081429+00:00",
+    "discussions_fetched_at": "2026-10-25T05:12:32.988336+00:00",
+    "local_head_records": 7402,
+    "nearest": [
+      "PR5496 (construction and single-active-target tests; audited here)",
+      "PR5353 (numerical row entry; inherited)",
+      "PR5092 (ROM producer; inherited)",
+      "PR5505 (cross-session numerical bank history; distinct)",
+      "PR5486 (fixed repair binary lowering; distinct)"
+    ],
+    "limits": "Complete snapshot pagination and full local note inventory; arbitrary code diffs and unpublished work outside coverage. No novelty guarantee.",
+    "footprint_check": {
+      "open_prs_fetched_at": "2026-10-25T05:31:21.052548+00:00",
+      "discussions_fetched_at": "2026-10-25T05:33:05.370314+00:00",
+      "queries": [
+        "ROM bank",
+        "producer footprint",
+        "48P"
+      ],
+      "distinction": "PR5505 concerns changing-precision numerical Entry histories, not the fixed-P singleton-ROM service bank. No matching exact bank formula found in the checked main notes and snapshot."
+    }
+  }
+}
diff --git a/research/crt-multitarget-row-audit/VENDORED.json b/research/crt-multitarget-row-audit/VENDORED.json
new file mode 100644
index 0000000000..e836c8fa64
--- /dev/null
+++ b/research/crt-multitarget-row-audit/VENDORED.json
@@ -0,0 +1,27 @@
+{
+  "source_pr": 5496,
+  "source_head": "a99afd7e0024af8367d5a2f6f4d2da57a1d13dd5",
+  "files": [
+    {
+      "path": "vendor/pr5496-join.py",
+      "source_path": "research/crt-current-row-query/join.py",
+      "source_commit": "a99afd7e0024af8367d5a2f6f4d2da57a1d13dd5",
+      "git_blob": "676582b4a376db375237ec52df84a3ddaf231827",
+      "sha256": "11c9ac1175a45edae80869b22c041e31a1b5cc75f4389ec2e073de37e547bf35"
+    },
+    {
+      "path": "vendor/pr5496-PROOF.md",
+      "source_path": "research/crt-current-row-query/PROOF.md",
+      "source_commit": "a99afd7e0024af8367d5a2f6f4d2da57a1d13dd5",
+      "git_blob": "0449d47c5027b4b5a6b6b5b2a87219069d4ad91c",
+      "sha256": "6aaa6253bf5f64f07cbfbf0a98a7c464e5a78cfa05c398f7eb41a27f03a7379c"
+    },
+    {
+      "path": "vendor/pr5496-README.md",
+      "source_path": "research/crt-current-row-query/README.md",
+      "source_commit": "a99afd7e0024af8367d5a2f6f4d2da57a1d13dd5",
+      "git_blob": "f5c66d745aaabb0b7ac8becaf8fda1ccfc004856",
+      "sha256": "41a14eb0d72c1ecce16a791b8f32d84f8c0b4e089c5e66a19067218e56d48db0"
+    }
+  ]
+}
diff --git a/research/crt-multitarget-row-audit/VERIFY.json b/research/crt-multitarget-row-audit/VERIFY.json
new file mode 100644
index 0000000000..25c3cc3067
--- /dev/null
+++ b/research/crt-multitarget-row-audit/VERIFY.json
@@ -0,0 +1,45 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "LICENSE",
+    "research/crt-encoded-benes-rom-producer/PROOF.md",
+    "research/crt-encoded-benes-rom-producer/microcode.py",
+    "research/crt-encoded-benes-rom-producer/vendor/pr4192-NOTICE.md",
+    "research/crt-mixed-row-entry/PROOF.md",
+    "research/crt-mixed-row-entry/bridge.py",
+    "research/crt-mixed-width-caller/verify.py",
+    "research/encoded-crt-entry-lifecycle/PROOF.md",
+    "research/encoded-crt-entry-lifecycle/entry.py",
+    "research/encoded-current-crt/PROOF.md",
+    "research/encoded-current-crt/producer.py",
+    "research/r437-preparation-composition/predecessor4025/source/NOTICE.md",
+    "research/r437-preparation-composition/predecessor4025/source/records.py",
+    "research/r437-preparation-composition/predecessor4025/source/words.py",
+    "research/unconditional-batched-crt/CRT.md",
+    "research/unconditional-batched-crt/NOTICE.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Independent multi-target current-row theorem corroboration: all actual producer tables, stream alignment, same-bank history, ownership, oracle calibration and twelve controls, exact rolewise extents and the sharp fixed-P bank footprint."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Same complete scientific checks with Python assertions disabled; typed receipt comparison and explicit failures remain active."
+    }
+  ]
+}
diff --git a/research/crt-multitarget-row-audit/vendor/NOTICE.md b/research/crt-multitarget-row-audit/vendor/NOTICE.md
new file mode 100644
index 0000000000..34cf4b6135
--- /dev/null
+++ b/research/crt-multitarget-row-audit/vendor/NOTICE.md
@@ -0,0 +1,14 @@
+# Retained source credit
+
+`pr5496-join.py`, `pr5496-PROOF.md` and `pr5496-README.md` are byte-identical
+copies from JoyboyBrian's PR #5496 at
+`a99afd7e0024af8367d5a2f6f4d2da57a1d13dd5`, under the repository's
+Apache-2.0 license. VENDORED.json records original paths, Git blobs and
+SHA256. Their original authorship and AI-assistance notices are retained.
+They are audited inputs, not new implementation by this package.
+
+The implementation's inherited credits include Ali Romman (#5353),
+Hiroki KUMAZAKI, Cinna Davis (#4100), ToikY, Tekalign, Jose Manuel,
+Ryanson Jonathan, unpaidmoon, Douglas Colkitt and John-Michael Smith.
+Their algorithms and proofs are explicit premises of this scoped audit.
+No pending Git object is needed for replay: the audited bytes are here.
diff --git a/research/crt-multitarget-row-audit/vendor/pr5496-PROOF.md b/research/crt-multitarget-row-audit/vendor/pr5496-PROOF.md
new file mode 100644
index 0000000000..0449d47c50
--- /dev/null
+++ b/research/crt-multitarget-row-audit/vendor/pr5496-PROOF.md
@@ -0,0 +1,226 @@
+# Current numerical offsets to a physical CRT micro-row
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## The exact boundary
+
+Use the admitted `RowEntry` domain of Ali Romman's PR5353: a power-of-two
+axis count d, declared h_i in {ell-1,ell}, ell>=2, pairwise coprime moduli
+2<=s_i<2^h_i, arbitrary padded current coordinates 0<=x_i<2^h_i, one
+compiled tree node [a,a+n) and one global row. The source is its literal
+sequential padded-axis tape, not a host list of numeric values. Eight
+distinct protected numerical words are supplied with the retained legal
+heads. Fixed topology, input ownership and the source numerical-operation
+model remain predecessor premises.
+
+Let b=a+n/2, P=1+sum_{i=a}^{a+n-1}h_i, and A be the non-idle right axes
+of this global row. The result is an owned stream containing, in axis
+order, the h_i bits of the **micro-row output** for every right axis
+b<=i<a+n. Delimiters are L, then one coordinate followed by `|` per axis,
+then R. No active axis means no allocation or tape work and no output;
+the original source already represents the identity row. When some axes
+are idle, their coordinates are copied into the returned stream unchanged.
+
+All borrowed source/dirty words and entry heads return unchanged. The
+numerical outputs, new descriptors, produced ROM and complete unselected
+layer output, producer workspace and query countdown are retired. The
+owned coordinate result remains until `close`, which erases it and closes
+the original Entry. Successful calls leave every new physical head at
+zero; the inherited numerical ports have their retained head-one exit.
+Failure rollback and arbitrary dirty backing acquisition are not claimed.
+
+This theorem closes an actual encoded-numerical-output to physical-query
+boundary. It is not the full three-epoch exceptional key, a full CRT row
+permutation of all payload addresses, or a complete multiplication theorem.
+
+## Numerical input and encoded descriptor compatibility
+
+The unchanged PR5353 RowEntry and PR5053 producer reconstruct the actual
+current left child. On a valid left child they return k_A; an invalid left
+child disables it by k_A=0. For each right axis i, their sequential output
+contains
+
+    c_i = k_A * (product_{j=a}^{i-1}s_j)^(-1) mod s_i,
+
+followed by a whole-rotation updated value. The inverse exists by pairwise
+coprimality. All preceding right moduli are included. We consume the offset
+word and **discard the updated-value word by a charged scan**: a complete
+cyclic rotation is not one Beneš micro-row.
+
+For an active axis, the join reads its original modulus directly from the
+borrowed source, translates each numeric bit to the producer's finite bit
+symbol, and pads with zeros against the actual unary P guide. It similarly
+copies exactly P bits from the actual numerical offset stream, enforcing
+the guide and field delimiters. This creates a singleton offset list
+`L [P bits] | R`; no decoded integer or host-built offset list is used.
+Compiled h_i and the selected local-row constant are written in binary and
+zero-padded through that same guide. The finite topology is the only source
+of those constants. The ROM program itself is precompiled without any
+input values and passed to the join.
+
+The existing PR5092 producer requires W>=h_i+3. A node has at least two
+axes, and every modulus is at least two, hence every admitted h_j>=2.
+Consequently P>=h_i+2+1=h_i+3. Taking W=P meets its width contract; its
+modulus and singleton-offset guards follow from the numerical theorem.
+The local row is g for a long axis, and g or g-2 on the two active pieces
+of a short axis, with global rows ell-1 and ell idle. This is exactly the
+pinned `local_row` function, and lies in [0,2h_i-2].
+
+Thus the unchanged encoded producer emits the exact canonical Beneš
+network for the rotation x->x+c_i mod s_i on x<s_i, fixing padded wires.
+Its selected `rom` is L followed by exactly N_i=2^h_i bits and R. Its
+`layers` output contains all 2h_i-1 layers; the join pays to erase it even
+though the query needs only one selected layer. Both producer outputs are
+consumed on their original backing lists, through local tape operations.
+There is no verifier-supplied row or source table lookup in execution.
+
+## Physical query and the current-coordinate convention
+
+The query copies the actual current h_i-bit coordinate to an owned
+little-endian countdown and a separate output coordinate. The ROM scan
+visits every produced row bit in order. Until selection, a zero test scans
+the countdown, returning its head, and a nonzero countdown is decremented
+by ordinary borrow propagation and head return. At scan position j, while
+selection is enabled, the countdown represents x_i-j. Hence precisely
+position x_i sees zero and selects its row bit. Since 0<=x_i<N_i, selection
+always occurs before R. After selection, the scan continues to R without
+changing the chosen bit. The countdown is then erased.
+
+If the local row is r, its source target bit is min(r,2h_i-2-r). The join
+moves to that compiled bit position in the owned coordinate, XORs the
+selected bit and returns the head. This is exactly `Caller.row`'s table
+action. No check x_i<s_i suppresses a query. A Beneš implementation of a
+padded permutation can pass through padded coordinates at intermediate
+rows; the queried coordinate must be the current one.
+
+At a fixed node, the left child is unchanged throughout its micro-rows.
+Right offsets depend on the successive modulus prefixes, not on the
+current right coordinate values. The numerical producer's current-child
+convention therefore gives the same offsets as the source caller at each
+row. Each active right axis receives its proper current-coordinate query;
+idle axes retain their coordinate. These facts prove the whole returned
+right-node row stream equals the corresponding slice of `Caller.row` for
+every admitted source state, not merely the verifier examples.
+
+## Ownership and a reused producer bank
+
+The numerical producer and RowEntry stay unchanged and retain their full
+63-port lifecycle. New header, coordinate, countdown and output ports are
+distinct from all borrowed roles. The join allocates one fixed PR5092
+service bank, then invokes the same program for each active axis on the
+same bank. Its private tapes return blank with heads zero by the producer
+theorem. The join erases both generated output roles and all four headers
+before the next invocation. These steps establish the next call's entry
+premises without constructing a new ROM or replacing the bank backing.
+Restoring the emulator's initial head configuration represents those
+already returned physical heads, not a free head jump.
+
+The finite producer register configuration is fixed control. Reentering
+its fixed start state has constant cost, included in the conservative
+adapter allowance below; it is not an input-sized store reset. Initial
+blank owned backing remains an explicit storage premise. Erasing cells
+does not release or subtract their retained capacity.
+
+The source and numerical output heads rewind by local movement. Numerical
+results are retired only after every offset has been consumed, so no
+output lifetime is silently shortened. `close` disposes of the coordinate
+result and calls the original Entry close exactly once. All malformed
+or rejected executions remain outside the successful cleanup theorem.
+
+## Complete local time and retained-storage invoice
+
+Let L=2+sum_{i=0}^{d-1}(3h_i+4), N_i=2^h_i, and
+
+    F = L + (n+1)(P+2)
+        + sum_{i in A}[(N_i+1)(h_i+1)
+                      + N_i(2h_i-1) + 2h_i+4].
+
+The inherited Entry, including numerical computation and retirement, costs
+
+    T_entry = 2^20(P+2)^4 + 2^16(P+2)^2 + 128(L+P+n+1).
+
+The complete producer is charged once per active axis at m=1, W=P:
+
+    T_rom(i) = 2*10^6 P^2 (N_i+1)^3 (h_i+1)^4.
+
+The new serialization, current-coordinate query, updates, returned-stream
+emission, every header/ROM/layer erase and every added rewind cost at most
+4096F source-tape/control operations. One direct count is: each additional
+source symbol is scanned a fixed number of times; each header/offset/skip
+word uses O(P) charged reads/writes/moves; each row query visits at most
+N_i positions, with at most two h_i-bit scans plus head returns at a
+position; disposal scans both output lengths N_i and N_i(2h_i-1)+O(h_i).
+The displayed routines use fewer than 64 primitive tape operations per
+unit represented in F. Between these charged accesses there are fewer
+than 64 finite tests, assignments and compiled-loop transitions, including
+fixed-role dispatch and the per-invocation fixed control reset. Thus 4096F
+is a deliberately loose complete bound, not a timing extrapolation.
+Compiled topology/ROM-program creation and supplied-input serialization
+are external setup, explicitly not runtime numeric decoding.
+Activity uses the fixed compiled node/width/row predicate, not a linear
+membership scan of all active axes. The emulator watchdog is the displayed
+T_rom(i), computed from compiled P and h_i; no fixed finite watchdog limits
+the admitted all-size successful execution theorem. External resource
+timeouts remain test limits, not machine rejection.
+
+The full invoice is
+
+    T_join <= T_entry + sum_{i in A} T_rom(i) + 4096F.
+
+This adds compatible fixed-alphabet source-operation bounds. It is not a
+claim that all numerical control was lowered to one binary transition table.
+
+Let J_i=N_i(h_i^2+3h_i+1). Use the predecessor Entry retained-backing bound
+
+    B_entry = 57(P+2)+3(P-2)(2P+4)+6+3P+4n+4,
+
+and, including the four producer inputs of total length 4P+9,
+
+    B_rom(i) = 100(P+2)+5P J_i+N_i(4h_i-1)+10(h_i+1)+4P+9.
+
+The single bank's sum of per-role historical maxima during this finite
+row is at most sum_i B_rom(i). We deliberately use this conservative sum,
+not the unjustified maximum of aggregate bounds. The two coordinate/
+countdown ports and returned stream add at most
+
+    B_extra = 2(max_{b<=i<a+n}h_i+3)
+              + sum_{b<=i<a+n}h_i + n/2 + 3.
+
+Hence total new owned retained backing is bounded by
+`B_entry + sum_i B_rom(i) + B_extra`. Input source L and protected numerical
+backing 8(P+2), plus any supplied exterior blank capacity, remain borrowed
+and separately charged. The verifier sums distinct physical backing
+identities, so ROM/header aliases in observer wrappers are not double
+counted. No arbitrary cross-session persistent-bank theorem is implied.
+
+## Evidence and limits
+
+The first source fixture is (7,3), widths (3,2), current state (1,1).
+Five separately encoded row invocations follow the actual state sequence
+(1,1), (1,1), (1,3), (1,3), (1,3), (1,2). The last query must run on
+padded coordinate 3. Test-harness serialization between invocations is
+explicit; this is not an uninterrupted physical whole-level execution.
+Invalid left padding disables the offset and returns identity. Four
+faults change the supplied offset, selected local row, required padded
+query or complete-layer disposal, and are detected at semantic or ownership
+checks. The source four-axis discriminator has preceding-right-modulus
+offset3 rather than the incorrect7, but the new full h=4 producer/query
+replay exceeded its180-second resource limit and produced no completion
+receipt. It is explicitly uncompleted; the executed new full pipeline
+evidence is h=2. The quantified argument is source-relative and does not
+depend on claiming that uncompleted test passed.
+
+Finite checks corroborate the written source-composition and countdown
+arguments. Initial axis-record production, a uniform binary compiler,
+full three-epoch exceptional key, global ROM reuse, full E(p,ell), native
+and outer multiplication admission remain unresolved. There is no new
+kappa or selected-frontier claim, human acceptance or formal-kernel proof.
+
+## Credit
+
+Ali Romman supplies PR5353's actual row-entry contract; JoyboyBrian supplies
+the retained PR5053/5219 numerical modules and PR5092 control producer.
+Retain Hiroki KUMAZAKI's current-coordinate and mixed-width caller,
+Cinna Davis's CRT/Beneš construction, ToikY's encoded arena/DFS proof,
+Tekalign's original-coordinate stream work, Jose Manuel, Ryanson Jonathan,
+unpaidmoon, Douglas Colkitt/John-Michael Smith and all pinned notices.
diff --git a/research/crt-multitarget-row-audit/vendor/pr5496-README.md b/research/crt-multitarget-row-audit/vendor/pr5496-README.md
new file mode 100644
index 0000000000..f5c66d745a
--- /dev/null
+++ b/research/crt-multitarget-row-audit/vendor/pr5496-README.md
@@ -0,0 +1,68 @@
+# Actual CRT offsets to a physical current-row query
+
+The sequential numerical result of Ali Romman's PR5353 now feeds the
+unchanged PR5092 encoded Beneš ROM producer. The join reads the produced
+ROM on its original backing, selects the current padded coordinate with
+an encoded countdown, and returns the actual micro-row coordinate stream.
+It pays for serialization, queries, rewinds and disposal of both the
+selected ROM and the unused complete-layer output.
+
+[PROOF.md](PROOF.md) gives the source-relative quantified interface theorem,
+admission W=P, current-coordinate convention, complete local time bound
+and retained-backing bound. [RESULT.json](RESULT.json) records the small
+actual producer/query cases and four falsifying controls. The h=2 checks
+exercise the complete encoded producer, not a verifier-supplied row table.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/crt-current-row-query
+```
+
+The registered normal and optimized runs authenticate every source input
+and compare typed deterministic receipts. The separate, expensive h=4
+four-axis test is explicitly opt-in:
+
+```sh
+python3.12 -B research/crt-current-row-query/verify.py --four-axis
+```
+
+This optional whole-ROM test is distinct from the small executed h=2 ABI
+checks. The author attempt exceeded180seconds without completion; no
+ACTUAL4 receipt exists and no h=4 joined result is claimed. See
+[ATTEMPT.json](ATTEMPT.json) for exact attempted bytes and the subsequent
+all-size repairs. A future completed optional run checks the caller and
+invoices even without a frozen receipt; `--write-result` records one.
+
+The small mixed-width case reaches padded coordinate3 before its last
+query. Suppressing that query gives the wrong endpoint. Mutating the
+offset, selected row or unused-layer disposal also fails. All source and
+protected words are restored; all63 numerical ports and every joined
+owned backing are retired. Separate row invocations use test-harness
+input serialization; no uninterrupted physical level execution is claimed.
+
+## Open next questions
+
+- Physically update the canonical axis input with the returned row stream,
+  so successive rows need no host serialization.
+- Compose the current query into the complete three-epoch exceptional key,
+  paying for all original/current coordinate conversions and restorations.
+- Resolve cross-session bank ownership and a complete binary numerical
+  lowering before claiming a global machine or outer multiplication bound.
+
+No new kappa, selected frontier, human acceptance or formal-kernel proof is
+claimed. Source models and initial blank owned backing remain explicit
+premises. This is one actual caller boundary, not full total repair.
+
+## Provenance and credit
+
+Base32890bc5de034ab8fc93ac88ead7279a6a416d04, priority7. The scope takes
+PR5353's explicit physical-query handoff, Discussion4709 comment19152738;
+the new claim is comment19173182. Fresh overlap covered352 open PRs and
+4747 fully paginated Discussion records through2026-10-25T04:14:44Z,
+plus exact local source packages. Unpublished work was not searched.
+[SOURCES.json](SOURCES.json) freezes the complete input closure.
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+Retain Ali Romman's actual RowEntry, Hiroki KUMAZAKI's mixed-width caller,
+JoyboyBrian's numerical entry and ROM producer, Cinna Davis's CRT/Beneš
+construction, ToikY's arena/DFS proof and all predecessor notices and
+credits listed in PROOF.md. No predecessor file is modified.
diff --git a/research/crt-multitarget-row-audit/vendor/pr5496-join.py b/research/crt-multitarget-row-audit/vendor/pr5496-join.py
new file mode 100644
index 0000000000..676582b4a3
--- /dev/null
+++ b/research/crt-multitarget-row-audit/vendor/pr5496-join.py
@@ -0,0 +1,224 @@
+"""Paid current-row numerical output -> existing ROM -> physical row query.
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+Topology is compiled data; runtime numeric values are never decoded.
+"""
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+class Tape:
+    def __init__(self, cells=None):
+        self.cells = ['_'] if cells is None else cells
+        self.head = 0
+        self.actions = 0
+
+    def read(self):
+        self.actions += 1
+        return self.cells[self.head]
+
+    def write(self, value):
+        need(value in ('_', 'L', 'R', '|', '0', '1'), 'fixed symbol')
+        self.actions += 1
+        self.cells[self.head] = value
+
+    def step(self, direction):
+        need(direction in (-1, 1) and self.head+direction >= 0, 'unit move')
+        self.actions += 1
+        self.head += direction
+        if self.head == len(self.cells):
+            self.cells.append('_')
+
+    def emit(self, value):
+        self.write(value)
+        self.step(1)
+
+    def rewind(self):
+        while self.read() != 'L':
+            self.step(-1)
+
+    def erase(self):
+        self.rewind()
+        self.step(1)
+        while self.read() != 'R':
+            self.write('_'); self.step(1)
+        self.write('_'); self.rewind(); self.write('_')
+
+
+def padded_constant(target, bits, guide, w):
+    target.emit('L')
+    for bit in bits:  # A compile-time constant, never an encoded input integer.
+        need(guide.read() == w.ONE, 'constant fits encoded width')
+        target.emit('1' if bit else '0'); guide.step(1)
+    while guide.read() == w.ONE:
+        target.emit('0'); guide.step(1)
+    need(guide.read() == w.BLANK, 'guide terminator')
+    target.write('R'); target.rewind(); guide.rewind()
+
+
+def copy_numeric_field(source, target, guide, w, delimiter, suffix='R'):
+    target.emit('L')
+    while guide.read() == w.ONE:
+        bit = source.read()
+        need(bit in (w.ZERO, w.ONE), 'numeric field bit')
+        target.emit('1' if bit == w.ONE else '0')
+        source.step(1); guide.step(1)
+    need(source.read() == delimiter and guide.read() == w.BLANK, 'exact P-bit field')
+    source.step(1); guide.rewind()
+    if suffix == '|':
+        target.emit('|')
+    target.write('R'); target.rewind()
+
+
+def skip_numeric_field(source, guide, w, delimiter):
+    while guide.read() == w.ONE:
+        need(source.read() in (w.ZERO, w.ONE), 'skipped numeric bit')
+        source.step(1); guide.step(1)
+    need(source.read() == delimiter and guide.read() == w.BLANK, 'skipped exact width')
+    source.step(1); guide.rewind()
+
+
+def select_row_bit(rom, countdown, fault=None):
+    """Scan the produced row; index is an encoded countdown, not a host cursor."""
+    enabled, answer, seen = True, '0', False
+    rom.step(1)
+    while rom.read() != 'R':
+        value = rom.read(); need(value in ('0', '1'), 'ROM row bit')
+        if enabled:
+            zero = True
+            countdown.step(1)
+            while countdown.read() != 'R':
+                zero = zero and countdown.read() == '0'
+                countdown.step(1)
+            countdown.rewind()
+            if zero:
+                answer, seen, enabled = value, True, False
+            else:
+                countdown.step(1)
+                while countdown.read() == '0':
+                    countdown.write('1'); countdown.step(1)
+                need(countdown.read() == '1', 'countdown underflow')
+                countdown.write('0'); countdown.rewind()
+        rom.step(1)
+    need(seen, 'current coordinate outside complete row')
+    rom.rewind(); countdown.erase()
+    return '0' if fault == 'suppress_query' else answer
+
+
+class RowQuery:
+    def __init__(self, w, records, entry_module, numeric, row_module, rom_module,
+                 program, source, dirty, widths, ell, level, start, row, fault=None):
+        self.w, self.records, self.source = w, records, source
+        self.fault = fault
+        self.entry = row_module.RowEntry(w, records, entry_module, numeric,
+                                        source, dirty, widths, ell, level, start, row)
+        self.output = None
+        self.ports = []
+        self.service = None
+        self.producer_steps = 0
+        self.invocations = 0
+        self.closed = False
+        if not self.entry.active:
+            return
+        # All variable-width initialization is driven by the existing unary guide.
+        guide = self.entry.guide
+        names = ('h', 'modulus', 'selected_layer', 'offsets')
+        headers = {name: Tape() for name in names}
+        coordinate, countdown, output = Tape(), Tape(), Tape()
+        self.ports = [*headers.values(), coordinate, countdown, output]
+        self.output = output
+        output.emit('L')
+        self.program = program
+        self.service = {name: ['_'] for name in rom_module.REGS+('arena','spool','layers','rom')}
+        self.service.update({name: headers[name].cells for name in names})
+        self.produced_rom = Tape(self.service['rom'])
+        self.produced_layers = Tape(self.service['layers'])
+        self.ports.extend((self.produced_rom, self.produced_layers))
+        result = self.entry.result['stream']
+        size = 1 << level
+        middle, stop = start+size//2, start+size
+        precision = 1 + sum(widths[start:stop])  # Compiled topology only.
+        for axis, h in enumerate(widths):
+            chosen = middle <= axis < stop
+            active = chosen and (h == ell or row not in (ell-1, ell))
+            need(source.read() == records.ROOT, 'axis tag'); source.step(1)
+            for _ in range(h):
+                need(source.read() == w.ONE, 'compiled axis width'); source.step(1)
+            need(source.read() == records.WORD_END, 'width delimiter'); source.step(1)
+            if active:
+                headers['modulus'].emit('L')
+            for _ in range(h):
+                bit=source.read(); need(bit in (w.ZERO,w.ONE), 'modulus bit')
+                if active:
+                    need(guide.read()==w.ONE,'modulus fits guide')
+                    headers['modulus'].emit('1' if bit==w.ONE else '0');guide.step(1)
+                source.step(1)
+            if active:
+                while guide.read()==w.ONE:
+                    headers['modulus'].emit('0');guide.step(1)
+                need(guide.read()==w.BLANK,'guide end');guide.rewind()
+                headers['modulus'].write('R');headers['modulus'].rewind()
+            need(source.read()==records.WORD_END,'modulus delimiter');source.step(1)
+            if chosen:
+                coordinate.emit('L')
+                if active:countdown.emit('L')
+            for _ in range(h):
+                bit=source.read();need(bit in (w.ZERO,w.ONE),'coordinate bit')
+                if chosen:
+                    symbol='1' if bit==w.ONE else '0';coordinate.emit(symbol)
+                    if active:countdown.emit(symbol)
+                source.step(1)
+            need(source.read()==records.RECORD_END,'axis end');source.step(1)
+            if not chosen:
+                continue
+            coordinate.write('R');coordinate.rewind()
+            need(result.read()==records.ROOT,'offset record');result.step(1)
+            if active:
+                countdown.write('R');countdown.rewind()
+                local=row if h==ell or row<ell-1 else row-2
+                selected=0 if fault=='wrong_local_row' else local
+                # These constants belong to the compiled topology.
+                hbits=tuple((h>>j)&1 for j in range(h.bit_length()))
+                rowbits=tuple((selected>>j)&1 for j in range(max(1,selected.bit_length())))
+                padded_constant(headers['h'],hbits,guide,w)
+                padded_constant(headers['selected_layer'],rowbits,guide,w)
+                copy_numeric_field(result,headers['offsets'],guide,w,records.WORD_END,'|')
+                if fault=='zero_offset':
+                    tape=headers['offsets'];tape.step(1)
+                    while tape.read()!='|':tape.write('0');tape.step(1)
+                    tape.rewind()
+                # Proven producer bound, compiled from topology, not input values.
+                budget=2*10**6*precision**2*((1<<h)+1)**3*(h+1)**4
+                run=rom_module.execute(self.program,self.service,max_steps=budget)
+                need(run['status']=='accept','unchanged ROM producer accepts')
+                need(all(head==0 for head in run['heads'].values()),'ROM heads returned')
+                self.producer_steps+=run['steps'];self.invocations+=1
+                bit=select_row_bit(self.produced_rom,countdown,fault)
+                target=min(local,2*h-2-local)
+                coordinate.step(1)
+                for _ in range(target):coordinate.step(1)
+                old=coordinate.read();coordinate.write('1' if (old=='1')!=(bit=='1') else '0')
+                coordinate.rewind()
+                if fault!='omit_layers_disposal':self.produced_layers.erase()
+                self.produced_rom.erase()
+                for tape in headers.values():tape.erase()
+            else:
+                skip_numeric_field(result,guide,w,records.WORD_END)
+            # The numerical whole-rotation field is consumed, never used as a row update.
+            skip_numeric_field(result,guide,w,records.WORD_END)
+            need(result.read()==records.RECORD_END,'offset record end');result.step(1)
+            coordinate.step(1)
+            while coordinate.read()!='R':
+                output.emit(coordinate.read());coordinate.step(1)
+            coordinate.rewind();coordinate.erase();output.emit('|')
+        need(source.read()==w.RIGHT and result.read()==w.RIGHT,'complete joined streams')
+        source.rewind();result.rewind();output.write('R');output.rewind()
+        need(all(tape.head==0 for tape in self.ports),'all physical heads returned')
+
+    def close(self):
+        need(not self.closed,'single retirement')
+        if self.output is not None:self.output.erase()
+        self.entry.close()
+        self.closed=True
diff --git a/research/crt-multitarget-row-audit/verify.py b/research/crt-multitarget-row-audit/verify.py
new file mode 100644
index 0000000000..81633db5c1
--- /dev/null
+++ b/research/crt-multitarget-row-audit/verify.py
@@ -0,0 +1,408 @@
+"""Independent boundary audit of the unchanged PR5496 multi-target join.
+
+Prepared for commdata2338 with substantial OpenAI Codex assistance.
+Apache-2.0. Observers never supply a successful execution's operands.
+"""
+import argparse
+from functools import lru_cache
+from hashlib import sha256
+import itertools
+import json
+import math
+from pathlib import Path
+import sys
+import types
+
+PACKAGE = Path(__file__).resolve().parent
+ROOT = PACKAGE.parents[1]
+
+
+class AuditError(ValueError):
+    pass
+
+
+def need(ok, reason):
+    if not ok:
+        raise AuditError(reason)
+
+
+def canonical(value):
+    """Preserve JSON types: True must not compare equal to 1 in a receipt."""
+    return json.dumps(value, sort_keys=True, separators=(',', ':'))
+
+
+def authenticate():
+    hashes = {}
+    for row in json.loads((PACKAGE / 'SOURCES.json').read_text())['files']:
+        if row['usage'] == 'input':
+            raw = (ROOT / row['path']).read_bytes()
+            need(sha256(raw).hexdigest() == row['sha256'], 'source hash: ' + row['path'])
+            hashes[row['path']] = row['sha256']
+    for row in json.loads((PACKAGE / 'VENDORED.json').read_text())['files']:
+        raw = (PACKAGE / row['path']).read_bytes()
+        need(sha256(raw).hexdigest() == row['sha256'], 'vendor hash: ' + row['path'])
+        hashes[row['path']] = row['sha256']
+    return hashes
+
+
+def load(name, path, raw=None):
+    module = types.ModuleType(name)
+    module.__file__ = str(path)
+    sys.modules[name] = module
+    exec(compile(path.read_bytes() if raw is None else raw, str(path), 'exec'), module.__dict__)
+    return module
+
+
+def modules():
+    base = ROOT / 'research/r437-preparation-composition/predecessor4025/source'
+    w = load('words', base / 'words.py')
+    r = load('audit_records', base / 'records.py')
+    e = load('audit_entry', ROOT / 'research/encoded-crt-entry-lifecycle/entry.py')
+    num = load('audit_numeric', ROOT / 'research/encoded-current-crt/producer.py')
+    row = load('audit_row_entry', ROOT / 'research/crt-mixed-row-entry/bridge.py')
+    rom = load('audit_rom', ROOT / 'research/crt-encoded-benes-rom-producer/microcode.py')
+    return w, r, e, num, row, rom, rom.producer_program()
+
+
+@lru_cache(None)
+def network(permutation):
+    """Exhaustive color oracle, independent of the source's DFS and arena.
+
+    The least satisfying tuple chooses zero at each component's minimum
+    vertex, the canonical source orientation. Only h<=3 is exercised.
+    """
+    n = len(permutation)
+    need(n >= 2 and n & (n - 1) == 0, 'oracle dyadic size')
+    need(sorted(permutation) == list(range(n)), 'oracle permutation')
+    if n == 2:
+        return ((0, (permutation[0], permutation[0])),)
+    inv = tuple(permutation.index(y) for y in range(n))
+    edges = [(x, x+1) for x in range(0,n,2)] + [(inv[y],inv[y+1]) for y in range(0,n,2)]
+    color = next((c for c in itertools.product((0,1), repeat=n)
+                  if all(c[x] != c[y] for x,y in edges)), None)
+    need(color is not None, 'oracle bipartite matchings')
+    children = []
+    for c in (0,1):
+        selected = [next(x for x in (2*j,2*j+1) if color[x] == c) for j in range(n//2)]
+        children.append(network(tuple(permutation[x]//2 for x in selected)))
+    layers = [(0,tuple(color[x] ^ (x%2) for x in range(n)))]
+    for k in range(len(children[0])):
+        layers.append((children[0][k][0]+1,
+                       tuple(children[x%2][k][1][x//2] for x in range(n))))
+    layers.append((0,tuple(color[inv[y]] ^ (y%2) for y in range(n))))
+    return tuple(layers)
+
+
+def rotation(h, modulus, offset):
+    return tuple((x+offset)%modulus if x<modulus else x for x in range(1<<h))
+
+
+def oracle(case):
+    """Bounded congruence search, not the retained CRT reconstruction."""
+    moduli, widths, state = case['moduli'],case['widths'],case['state']
+    start, size = case['start'],1<<case['level']
+    middle, stop = start+size//2,start+size
+    product = math.prod(moduli[start:middle])
+    if any(state[i]>=moduli[i] for i in range(start,middle)):
+        lower=0
+    else:
+        candidates=[k for k in range(product)
+                    if all((k-state[i]*math.prod(moduli[start:i]))%moduli[i]==0
+                           for i in range(start,middle))]
+        need(len(candidates)==1,'oracle unique current child')
+        lower=candidates[0]
+    rows=[]
+    for i in range(middle,stop):
+        h,s,g,ell=widths[i],moduli[i],case['row'],case['ell']
+        offsets=[c for c in range(s) if (product*c-lower)%s==0]
+        need(len(offsets)==1,'oracle unique offset')
+        c=offsets[0];product*=s
+        active=h==ell or g not in (ell-1,ell)
+        local=g if h==ell or g<ell-1 else g-2
+        layers=network(rotation(h,s,c));value=state[i]
+        if active:
+            bit,table=layers[local];value^=table[value]<<bit
+        rows.append(dict(axis=i,h=h,modulus=s,offset=c,active=active,
+                         local=local if active else None,input=state[i],output=value,layers=layers))
+    return lower,rows
+
+
+def port(w,e,symbols):
+    tape=e.Port(w)
+    for symbol in symbols:tape.append(symbol)
+    tape.rewind();return tape
+
+
+def bits(value,width):
+    return [(value>>j)&1 for j in range(width)]
+
+
+def snapshot(ports):
+    return [(bytes(p.cells),p.head) for p in ports]
+
+
+def traffic(ports):
+    return sum(p.meter.reads+p.meter.writes+p.meter.moves for p in ports)
+
+
+def read_header(cells,precision,offset=False):
+    ending=['|','R'] if offset else ['R']
+    need(cells[:1]==['L'] and cells[precision+1:precision+1+len(ending)]==ending,'header delimiters')
+    need(all(x in ('0','1') for x in cells[1:precision+1]),'header binary width')
+    need(all(x=='_' for x in cells[precision+1+len(ending):]),'header blank tail')
+    return sum(int(x)<<j for j,x in enumerate(cells[1:precision+1]))
+
+
+def body(cells,expected):
+    need(cells[:len(expected)]==expected and all(x=='_' for x in cells[len(expected):]),
+         'produced canonical table or blank tail')
+
+
+def bank_storage(precision,height):
+    """Derived in PROOF.md, including all four caller-owned headers."""
+    n=1<<height
+    return 5*precision*n*(height*height+3*height+1)+n*(4*height-1)+48*precision+2*height+104
+
+
+def fresh_extents(registers,precision,height):
+    need(len(registers)==44 and len(set(registers))==44,'fixed scalar role inventory')
+    n=1<<height
+    result={role:precision+2 for role in registers}
+    result.update(arena=5*precision*n*(height*height+3*height+1)+2,
+                  spool=n*(2*height-1)+2,layers=(n+1)*(2*height-1)+2,rom=n+2,
+                  h=precision+2,modulus=precision+2,selected_layer=precision+2,offsets=precision+3)
+    need(sum(result.values())==bank_storage(precision,height),'expanded bank formula')
+    return result
+
+
+class ObserveROM:
+    def __init__(self,rom,precision,expected):
+        self.execute_original=rom.execute
+        self.registers=rom.REGS
+        self.precision,self.expected=precision,expected
+        self.calls=[];self.identities=None;self.previous_extents=None
+        self.headers=('h','modulus','selected_layer','offsets')
+
+    def execute(self,program,tapes,max_steps):
+        index=len(self.calls)
+        need(index<len(self.expected),'too many producer invocations')
+        expected=self.expected[index]
+        ids={k:id(v) for k,v in tapes.items()}
+        need(len(set(ids.values()))==len(ids),'distinct producer backing roles')
+        if self.identities is None:self.identities=ids
+        else:need(ids==self.identities,'same producer bank at next target')
+        before={k:len(v) for k,v in tapes.items()}
+        if self.previous_extents is not None:
+            need(all(before[k]>=self.previous_extents[k] for k in before),'retained backing never shrinks')
+        need(all(all(x=='_' for x in v) for k,v in tapes.items() if k not in self.headers),
+             'blank producer reentry including old tails')
+        values={k:read_header(tapes[k],self.precision,k=='offsets') for k in self.headers}
+        wanted=dict(h=expected['h'],modulus=expected['modulus'],
+                    selected_layer=expected['local'],offsets=expected['offset'])
+        need(values==wanted,'current target header correspondence')
+        header_bytes={k:tuple(tapes[k]) for k in self.headers}
+        result=self.execute_original(program,tapes,max_steps=max_steps)
+        need(result['status']=='accept','actual producer acceptance')
+        need(all(h==0 for h in result['heads'].values()),'actual producer heads')
+        need(all(tuple(tapes[k])==header_bytes[k] for k in self.headers),'producer borrowed headers')
+        need(all(all(x=='_' for x in v) for k,v in tapes.items()
+                 if k not in self.headers+('rom','layers')),'producer private restoration')
+        table=expected['layers'][expected['local']][1]
+        body(tapes['rom'],['L',*map(str,table),'R'])
+        layers=['L']
+        for _,table in expected['layers']:layers += [*map(str,table),'|']
+        body(tapes['layers'],layers+['R'])
+        after={k:len(v) for k,v in tapes.items()}
+        fresh=fresh_extents(self.registers,self.precision,expected['h'])
+        need(set(before)==set(fresh),'complete bank role inventory')
+        need(after=={k:max(before[k],fresh[k]) for k in fresh},'exact rolewise retained extents')
+        self.previous_extents=after
+        self.calls.append(dict(axis=expected['axis'],headers=values,instructions=result['steps'],
+                               before_extents=before,after_extents=after,
+                               rom_sha256=sha256(''.join(tapes['rom']).encode()).hexdigest()))
+        return result
+
+
+CASES=[
+    dict(name='two_short_first',moduli=[5,7,3,2],widths=[3,3,2,2],state=[1,5,2,1],row=0),
+    dict(name='two_short_distinct_offsets',moduli=[5,7,3,2],widths=[3,3,2,2],state=[3,2,1,1],row=4),
+    dict(name='shrinking_bank',moduli=[2,5,7,3],widths=[2,3,3,2],state=[1,4,7,3],row=4),
+    dict(name='growing_bank',moduli=[2,5,3,7],widths=[2,3,2,3],state=[1,4,3,7],row=4),
+    dict(name='leading_idle',moduli=[2,5,3,7],widths=[2,3,2,3],state=[1,4,3,7],row=2),
+    dict(name='trailing_idle',moduli=[2,5,7,3],widths=[2,3,3,2],state=[1,4,7,3],row=2),
+    dict(name='invalid_left',moduli=[5,7,3,2],widths=[3,3,2,2],state=[5,5,3,1],row=4),
+    dict(name='all_idle',moduli=[5,7,3,2],widths=[3,3,2,2],state=[1,5,2,1],row=2),
+    dict(name='nonroot_minimum_guide',moduli=[5,7,3,2],widths=[3,3,2,2],state=[1,5,1,1],row=4,level=1,start=2),
+]
+for _case in CASES:
+    _case.setdefault('ell',3);_case.setdefault('level',2);_case.setdefault('start',0)
+
+
+def run_case(mod,case,mutation=None,fault=None):
+    w,r,e,num,row,rom,program=mod
+    raw=(PACKAGE/'vendor/pr5496-join.py').read_bytes()
+    if mutation:
+        old,new=mutation;need(raw.count(old)==1,'unique source mutation');raw=raw.replace(old,new)
+    join=load('audited_join',PACKAGE/'vendor/pr5496-join.py',raw)
+    source_data=[]
+    for s,h,x in zip(case['moduli'],case['widths'],case['state']):
+        source_data += [r.ROOT]+[w.ONE]*h+[r.WORD_END]+bits(s,h)+[r.WORD_END]+bits(x,h)+[r.RECORD_END]
+    source=port(w,e,source_data+[w.RIGHT])
+    n=1<<case['level'];precision=1+sum(case['widths'][case['start']:case['start']+n])
+    dirty=[port(w,e,bits((5*j+3)%(1<<precision),precision)+[w.RIGHT]) for j in range(8)]
+    for j,tape in enumerate(dirty):
+        for _ in range(j%3):tape.step(1)
+    borrowed=[source,*dirty]
+    before,initial_traffic=snapshot(borrowed),traffic(borrowed)
+    lower,expected=oracle(case);active=[x for x in expected if x['active']]
+    observer=ObserveROM(rom,precision,active)
+    entry_cut={}
+    class ObservedEntry(row.RowEntry):
+        def __init__(self,*args,**kwargs):
+            super().__init__(*args,**kwargs)
+            if self.context is not None:
+                entry_cut['ports']=[*borrowed,*self.inputs,*self.context.owned]
+                entry_cut['traffic']=traffic(entry_cut['ports'])
+    proxy_row=types.SimpleNamespace(RowEntry=ObservedEntry)
+    proxy_rom=types.SimpleNamespace(REGS=rom.REGS,execute=observer.execute)
+    query=join.RowQuery(w,r,e,num,proxy_row,proxy_rom,program,source,dirty,
+                        case['widths'],case['ell'],case['level'],case['start'],case['row'],fault)
+    need(snapshot(borrowed)==before,'borrowed input bytes and heads')
+    need(len(observer.calls)==len(active),'one producer call per active target')
+    if not active:
+        need(query.output is None and not query.ports and query.service is None,'idle no owned bank')
+        query.close();need(traffic(borrowed)==initial_traffic,'idle no tape work')
+        return dict(name=case['name'],idle=True,calls=[],lower=lower)
+    cells,at,actual=query.output.cells,1,[]
+    need(cells[0]=='L','output left marker')
+    for target in expected:
+        h=target['h'];need(all(x in ('0','1') for x in cells[at:at+h]),'output exact-width bits')
+        actual.append(sum(int(cells[at+j])<<j for j in range(h)));at+=h
+        need(cells[at]=='|','one output delimiter per target');at+=1
+    need(cells[at]=='R' and all(x=='_' for x in cells[at+1:]),'output right marker and blank tail')
+    need(actual==[x['output'] for x in expected],'independent micro-row endpoint')
+    need(all(p.head==0 for p in query.ports),'joined returned heads')
+    need({k:id(v) for k,v in query.service.items()}==observer.identities,'terminal same bank identities')
+    need(all(all(x=='_' for x in v) for v in query.service.values()),'terminal complete producer disposal')
+    adapter=sum(p.actions for p in query.ports)+traffic(entry_cut['ports'])-entry_cut['traffic']
+    length=2+sum(3*h+4 for h in case['widths'])
+    work=length+(n+1)*(precision+2)+sum(
+        (2**x['h']+1)*(x['h']+1)+2**x['h']*(2*x['h']-1)+2*x['h']+4 for x in active)
+    owned=[*query.entry.inputs,*query.entry.context.owned]
+    before_close=sum(p.actions for p in query.ports);query.close()
+    adapter+=sum(p.actions for p in query.ports)-before_close
+    need(adapter<=4096*work,'adapter-only tape-action allowance')
+    need(snapshot(borrowed)==before,'borrowed preservation after close')
+    need(all(p.head==1 and all(x==w.BLANK for x in p.cells) for p in owned),'numerical retirement')
+    need(all(p.head==0 and all(x=='_' for x in p.cells) for p in query.ports),'joined retirement including result')
+    unique={id(p.cells):p.cells for p in query.ports}
+    unique.update({id(v):v for v in query.service.values()})
+    # Independent partition: all service roles, plus exactly three other
+    # backings (coordinate, countdown and returned output). Headers and the
+    # two output observers alias service backings and are counted once.
+    bank_ids={id(v) for v in query.service.values()}
+    extras=[p.cells for p in query.ports if id(p.cells) not in bank_ids]
+    need(len(extras)==3 and len({id(v) for v in extras})==3,'three extra backings')
+    bank_retained=sum(len(v) for v in query.service.values())
+    extra_retained=sum(len(v) for v in extras)
+    largest=max(x['h'] for x in active)
+    need(bank_retained==bank_storage(precision,largest),'exact shared-bank footprint')
+    need(extra_retained==2*(largest+2)+sum(x['h'] for x in expected)+len(expected)+2,
+         'exact three-extra-port footprint')
+    need(sum(map(len,unique.values()))==bank_retained+extra_retained,'complete backing partition')
+    retained=sum(len(p.cells) for p in owned)+bank_retained+extra_retained
+    return dict(name=case['name'],idle=False,lower=lower,precision=precision,
+                offsets=[x['offset'] for x in expected],output=actual,calls=observer.calls,
+                adapter_tape_actions=adapter,adapter_bound=4096*work,
+                owned_retained_cells=retained,numerical_owned_roles=len(owned),
+                producer_retained_cells=bank_retained,extra_retained_cells=extra_retained,
+                expected_query_coordinates=[x['input'] for x in active])
+
+
+def rejected(label,fn,text):
+    try:fn()
+    except ValueError as exc:
+        need(text in str(exc),'wrong rejection for '+label+': '+str(exc))
+        return dict(name=label,rejected_by=str(exc))
+    raise AuditError('undetected control '+label)
+
+
+def controls(mod,results):
+    cases={x['name']:x for x in CASES};late=cases['two_short_distinct_offsets'];out=[]
+    out.append(rejected('stale_zero_offset',lambda:run_case(mod,late,fault='zero_offset'),
+                        'current target header correspondence'))
+    out.append(rejected('wrong_local_row',lambda:run_case(mod,late,fault='wrong_local_row'),
+                        'current target header correspondence'))
+    padded=dict(late,name='padded_control',state=[1,5,3,1])
+    out.append(rejected('suppress_padded_query',lambda:run_case(mod,padded,fault='suppress_query'),
+                        'independent micro-row endpoint'))
+    out.append(rejected('omit_layers_disposal',lambda:run_case(mod,late,fault='omit_layers_disposal'),
+                        'blank producer reentry including old tails'))
+    out.append(rejected('omit_result_retirement',lambda:run_case(mod,late,mutation=(
+        b'if self.output is not None:self.output.erase()',b'if self.output is not None:pass')),
+        'joined retirement including result'))
+    out.append(rejected('skip_idle_offset_record',lambda:run_case(mod,cases['leading_idle'],mutation=(
+        b'else:\n                skip_numeric_field(result,guide,w,records.WORD_END)',
+        b'else:\n                pass')),'offset record end'))
+    out.append(rejected('replace_bank_between_targets',lambda:run_case(mod,late,mutation=(
+        b'run=rom_module.execute(self.program,self.service,max_steps=budget)',
+        b'run=rom_module.execute(self.program,self.service if self.invocations==0 else {k:list(v) for k,v in self.service.items()},max_steps=budget)')),
+        'same producer bank at next target'))
+    k,targets=oracle(cases['growing_bank']);short_prefix=math.prod(cases['growing_bank']['moduli'][:2])
+    wrong=k*pow(short_prefix,-1,cases['growing_bank']['moduli'][3])%cases['growing_bank']['moduli'][3]
+    need(wrong!=targets[1]['offset'],'prefix omission discriminator')
+    out.append(dict(name='omit_preceding_right_modulus',correct=targets[1]['offset'],wrong=wrong))
+    k,_=oracle(cases['two_short_first']);raw_digits=1+5*5
+    need(k!=raw_digits,'current child versus original digits discriminator')
+    out.append(dict(name='treat_current_as_original_digits',correct=k,wrong=raw_digits))
+    shrinking=next(x for x in results if x['name']=='shrinking_bank')
+    actual=shrinking['producer_retained_cells']
+    last_height=shrinking['calls'][-1]['headers']['h']
+    wrong=bank_storage(shrinking['precision'],last_height)
+    out.append(rejected('bill_only_final_smaller_target',
+                        lambda:need(actual==wrong,'exact shared-bank footprint'),
+                        'exact shared-bank footprint'))
+    omitted_spool=actual-shrinking['calls'][-1]['after_extents']['spool']
+    out.append(rejected('omit_retained_spool',
+                        lambda:need(actual==omitted_spool,'complete bank includes spool'),
+                        'complete bank includes spool'))
+    need(canonical({'value':True})!=canonical({'value':1}),'typed receipt control')
+    out.append(dict(name='boolean_integer_receipt_collision',rejected=True))
+    return out
+
+
+def oracle_checks():
+    count=addresses=0
+    for h in (2,3):
+        for s in range(2,1<<h):
+            for offset in range(s):
+                perm=rotation(h,s,offset);layers=network(perm)
+                for bit,table in layers:
+                    need(all(table[x]==table[x^(1<<bit)] for x in range(1<<h)),'oracle switch involution')
+                for x in range(1<<h):
+                    y=x
+                    for bit,table in layers:y^=table[y]<<bit
+                    need(y==perm[x],'oracle composed rotation');addresses+=1
+                count+=1
+    return dict(networks=count,addresses=addresses)
+
+
+def main():
+    parser=argparse.ArgumentParser();parser.add_argument('--write-result',action='store_true')
+    parser.add_argument('--case',choices=[x['name'] for x in CASES]);args=parser.parse_args()
+    sources=authenticate();calibration=oracle_checks();mod=modules();results=[]
+    for case in CASES:
+        if args.case is None or args.case==case['name']:
+            results.append(run_case(mod,case));print('PASS_CASE',case['name'],flush=True)
+    if args.case:print(json.dumps(results,indent=2));return
+    negative=controls(mod,results)
+    result=dict(status='PASS_CRT_MULTITARGET_ROW_AUDIT',sources=sources,oracle=calibration,
+                cases=results,controls=negative,producer_calls=sum(len(x['calls']) for x in results))
+    receipt=PACKAGE/'RESULT.json'
+    if args.write_result:receipt.write_text(json.dumps(result,indent=2)+'\n')
+    else:need(canonical(json.loads(receipt.read_text()))==canonical(result),'typed receipt drift')
+    print(result['status'],'cases='+str(len(results)),'producer_calls='+str(result['producer_calls']),
+          'controls='+str(len(negative)),'no_new_kappa=true')
+
+
+if __name__=='__main__':main()