From 232b3916e6331222278f6edd5a4b9d56731667d9 Mon Sep 17 00:00:00 2001
From: Hiroki KUMAZAKI <hiroki.kumazaki@gmail.com>
Date: Sun, 18 Oct 2026 12:59:33 +0900
Subject: [PATCH] Implement least actual-body borrowing on fixed Count tapes

---
 .../encoded-body-depth-borrowing/PROOF.md     | 240 +++++++++++++++++
 .../encoded-body-depth-borrowing/README.md    | 131 +++++++++
 .../encoded-body-depth-borrowing/RESULT.json  | 149 +++++++++++
 .../encoded-body-depth-borrowing/SOURCES.json | 141 ++++++++++
 .../encoded-body-depth-borrowing/TASK.json    | 131 +++++++++
 .../encoded-body-depth-borrowing/VERIFY.json  |  40 +++
 .../independent.py                            | 144 ++++++++++
 .../predecessor/PR3486-PROOF.md               | 195 ++++++++++++++
 .../encoded-body-depth-borrowing/selector.py  | 222 ++++++++++++++++
 .../encoded-body-depth-borrowing/verify.py    | 248 ++++++++++++++++++
 10 files changed, 1641 insertions(+)
 create mode 100644 research/encoded-body-depth-borrowing/PROOF.md
 create mode 100644 research/encoded-body-depth-borrowing/README.md
 create mode 100644 research/encoded-body-depth-borrowing/RESULT.json
 create mode 100644 research/encoded-body-depth-borrowing/SOURCES.json
 create mode 100644 research/encoded-body-depth-borrowing/TASK.json
 create mode 100644 research/encoded-body-depth-borrowing/VERIFY.json
 create mode 100644 research/encoded-body-depth-borrowing/independent.py
 create mode 100644 research/encoded-body-depth-borrowing/predecessor/PR3486-PROOF.md
 create mode 100644 research/encoded-body-depth-borrowing/selector.py
 create mode 100644 research/encoded-body-depth-borrowing/verify.py

diff --git a/research/encoded-body-depth-borrowing/PROOF.md b/research/encoded-body-depth-borrowing/PROOF.md
new file mode 100644
index 0000000000..5d8a52f3f3
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/PROOF.md
@@ -0,0 +1,240 @@
+# Count-tape refinement of actual-body borrowing
+
+This result refines Nick Petalas's [PR3486](https://github.com/CrocSwap/integer-mult-bounds/pull/3486)
+at `991861d40a1ebdbbf35be9adc1726e6af5b71e49`. Its byte-pinned proof is
+retained in `predecessor/PR3486-PROOF.md`. The new contribution is the
+`selector.py` implementation, its setup and ownership invoice, and bounded
+checks against independent integer specifications. The monotonicity and
+inverse-depth arguments remain PR3486's work.
+
+The execution vocabulary is Jose Manuel's PR2899 Count selector and its
+retained PR2809/PR2753 source closure. The consumer contract is Tekalign's
+PR3264 ordinary one-factor adapter, using Nick Petalas's PR3246 NODE-guard
+reserve. Source access, completed children, pointwise fresh-row restoration,
+physical refinement and uniform caller costs remain inherited premises.
+
+## 1. Contract and arithmetic refinement
+
+Fix compiled integers `q>=2`, `m>r>=1`, `W>=1`, `Q>=1` and a fixed rational
+width exponent `alpha=A/C`, with `C>0` and `0<=A<=C`. The zero exponent is
+useful for reduced fixtures; the selected exponent is `17/10000`. For a
+positive canonical input Count `e`, define
+
+```
+w = ceil(e^alpha),
+N = product_(i=0)^(m-1) (q^m-q^i),
+b = W*N*q^(m*m*(w-1)),
+D(n) = 0                         if n<m,
+D(n) = 1+D(r*floor(n/m))          otherwise,
+S_0 = 1,  S_d = Q*b^d            for d>=1.
+```
+
+For a source-admissible prime `q`, `N=|GL_m(F_q)|`. Validation of the
+arithmetic selector only requires integer `q>=2`; this does not admit a
+composite radix to the selected finite-field construction.
+
+The retained `encoded.atom_width` computes the stated ceiling using exact
+integer powers and bisection. All subsequent values depending on `e` are
+Counts. The host expressions for `N`, `q^(m*m)`, `W*N`, and the profile are
+compiled source constants. Neither `e`, `w`, `k`, `D(n)` nor a stock value is
+decoded to a Python integer by the selector.
+
+The new `_power(base, exponent)` scans the canonical exponent from most
+significant bit to least significant bit. If the scanned prefix has value
+`p`, its invariant is `value=base^p`. Squaring and then multiplying by the
+base exactly when the next bit is one changes the exponent to `2p+bit`.
+The initial value is one, so this also handles zero. Count products copy
+their inputs, and the exponent is rewound on return. The two inputs retain
+their contents and origin positions. No recursion or list of exponent bits
+is required.
+
+For a trial `0<=k<=e`, `encoded.divide(e-k,w)` returns its exact quotient
+and remainder. Repeated small division by `m` followed by multiplication by
+`r` computes `D(n)`; this terminates because the child is strictly smaller
+than each positive internal width. `_power` then constructs the exact
+`stock=S_D(n)` and `rows=q^k`. At positive depth, `Q` is multiplied once.
+At depth zero, stock is one. Every trial's body, remainder, depth, stock and
+rows are recomputed from its own borrowing Count.
+
+## 2. Least feasible borrowing
+
+Let
+
+```
+n(k)=floor((e-k)/w),
+U=min(floor((e-1)/2), e-m*w).
+```
+
+Exactly the integers `k` in `[0,U]` satisfy both `2k<e` and `n(k)>=m`.
+PR3486 proves that, on this interval,
+
+```
+P(k): q^k >= S_D(n(k))
+```
+
+is monotone: `D` is nondecreasing, `n(k)` is nonincreasing, and the stock
+sequence is nondecreasing. This selector implements that same predicate by
+comparing its two exact Count values, without approximating logarithms.
+
+If `e<m*w`, it returns no fit. Otherwise it constructs the nonnegative `U`,
+tests zero, and then tests `U`. A successful zero is minimal. A failed `U`
+rules out every candidate. In the remaining case the maintained endpoints
+satisfy `0<=lower<upper<=U`, with `P(lower)` false and `P(upper)` true.
+Their integer midpoint is strictly between them when the gap exceeds one.
+Replacing the appropriate endpoint preserves the invariant and at least
+halves the gap, rounded up. Thus the loop takes `O(log(e+1))` trials and
+terminates at adjacent endpoints. Its upper endpoint is the least feasible
+borrowing. This nonnegative formulation needs no encoded negative sentinel.
+
+After bisection, a fresh final trial materializes all five dependent fields.
+Together with `width` and `borrowed`, the seven returned Counts describe
+exactly the accepted plan. They belong to the caller. A no-fit result has the
+true width, zero depth/borrowed/body/remainder, and unit stock/rows. Those
+sentinel fields describe no admitted recursive call. They cannot be reused
+as stale fields from a rejected trial. `close_plan` releases all seven Counts.
+
+Optimality is for this fixed width and the explicit covering constraint
+`q^k>=S_D(n)`. It does not optimize width or all possible padding budgets.
+In particular, the optimum need not satisfy `k=ceil(log_q S_D(n(k)))`;
+PR3486's discontinuous-depth example explains why fixed-point iteration
+would be incorrect.
+
+## 3. Complete setup invoice
+
+This invoice counts the retained sequential binary-tape operations, subject
+to their existing physical refinement. Constants below may depend on the
+fixed profile and radix. Put
+
+```
+h = 1+ceil(log_2(e+1)),
+B = e+w*h.
+```
+
+Since `w<=e` and `r/m<1`, trial depths are `O(h)`. The bitlengths of the
+input, geometric endpoints, body, remainder and depth are `O(h)`; the level
+`b` has `O(w)` bits; and a trial stock has `O(w*h)` bits. The full `q^k`
+may have `Theta(e)` bits even for a rejected trial with small `w`. It is
+therefore included in `B`. The bound does not charge only the final stock
+threshold or silently replace full radix powers by saturated comparisons.
+
+A copy, comparison, small fixed multiplication/division, increment,
+subtraction, normalization or clear costs `O(L)` at word length `L`.
+Retained binary long division and `Count.product` cost `O(L^2)` when all
+operands and results have `O(L)` bits. In the product, at most `O(L)` scanned
+multiplier bits each cause an `O(L)` shift/add scan. An MSB exponentiation
+with a `t`-bit exponent consequently costs `O(t*L^2)`. All intermediate
+exponents are prefixes of the final exponent, including the doubled prefix
+before a conditional multiply. Bases here are at least one, so no
+intermediate product exceeds its final power.
+
+The charges are as follows; they include the scans that rewind, normalize,
+copy and clear each temporary.
+
+| Stage | Bound in retained tape operations |
+| --- | --- |
+| Atom-width selection | `O(h^3)` |
+| Geometric bounds and endpoint setup | `O(h)` |
+| Construct `b` from the compiled `q^(m*m)` and Count exponent `w-1` | `O(h*w^2)` |
+| One trial's quotient/remainder and depth recurrence | `O(h^2)` |
+| One trial's stock power and one compatibility multiplication | `O((1+log(h+1))*(w*h)^2)` |
+| One trial's full radix power `q^k` | `O(h*e^2)` |
+| Endpoint tests, `O(h)` bisection trials and one final materialization | `O(h^2*B^2)` in total |
+| Final returned-plan disposal and other remaining cleanup | `O(B)` |
+
+For the first row, the fixed numerator gives an `O(h)`-bit target `e^A`.
+Width bisection has `O(h)` iterations. The fixed-denominator powers saturate
+at that target: an unsaturated product has at most twice its bitlength.
+There are a fixed number of products per fixed-exponent power, each costing
+`O(h^2)`. For the level row, there are at most `O(h)` exponent bits and
+`O(w)`-bit intermediate values. For the stock row, `D(n)=O(h)` has only
+`O(1+log(h+1))` bits. The conservative total also includes zero and upper
+endpoint trials, discarded plans and the final complete recomputation.
+
+The resulting bound is
+
+```
+T_setup = O(h^3 + h^2*(e+w*h)^2),
+S_setup = O(e+w*h) binary cells on a fixed number of roles.
+```
+
+There is an additional fixed compilation/initialization constant for the
+chosen `q,m,r,W,Q,A,C`; this is not uniform in these source parameters. For
+the selected fixed exponent `0<alpha<1`, `w*h=O(e)`, so setup is
+`O(e^2*h^2+h^3)` and uses `O(e)` cells. More generally `alpha<=1` gives the
+still polynomial bound `O(e^2*h^4+h^3)`. With the inherited relation
+`e=O_q(log V)`, either is a fixed polynomial in `1+log V`. Setup is charged
+in addition to the consumer's full payload bill. This proof supplies no
+numerical machine-step constant or new asymptotic multiplication exponent.
+
+## 4. Fixed roles and successful-return ownership
+
+Each `_Owned` dictionary has a fixed finite set of literal names; loop
+iterations replace existing slots. A trial is closed before the next one,
+and `_power` uses one replacement accumulator. Thus the Python bookkeeping
+does not encode an unbounded table or a growing recursion stack.
+
+The count includes the temporary tape used by `Count.literal`, not merely
+the returned Counts. A Count product has at most four simultaneous internal
+tapes: factor, scan, result, and either the result literal's temporary or the
+copy used by addition. A power retains one old accumulator while that
+product is constructed, so it needs at most five additional roles beyond
+its borrowed inputs.
+
+| Phase | Conservative simultaneous roles, excluding the borrowed input |
+| --- | --- |
+| Inherited width helper, before other selector fields exist | 10 |
+| Main scope plus active trial and power temporaries | 17 |
+| No-fit sentinel construction while the upper trial is still live | 19 |
+
+For the second row, the main scope has at most eight live Counts, including
+the midpoint. The trial retains at most four other Counts while creating
+its rows power, which adds at most five. Its division path uses fewer roles.
+For the last row there are seven main Counts, five completed trial Counts,
+six sentinel Counts and one literal-construction temporary. Including the
+borrowed input still leaves a conservative allowance of 24 roles. Width
+selection has already returned before the later main/trial scopes overlap.
+
+Under the retained fixed-role allocator these requests fit within the
+predecessor's 64 setup-role allowance. This is an analytic upper bound on
+successful well-formed executions, not an inference from a finite observed
+peak. The input Count is preserved and rewound. Every other result is either
+transferred once to the returned plan or closed by its scope; replacement
+closes the old value after the new value is computed. The caller closes the
+plan after use. This preserves the inherited successful-return marker and
+lease convention. It does not promise transactional recovery from arbitrary
+exceptions inside predecessor arithmetic or supply a new universal physical
+compiler proof.
+
+## 5. Conditional consumer implication and limits
+
+For an admitted plan let `d=D(n)`, `R=q^k` and
+`R'=ceil(R/S_d)*S_d`. The predicate proves `R>=S_d`, hence
+`R<=R'<2R`. PR3486 and PR3264 then give the same NODE-guard implication:
+the whole fresh quotient passes to children, completed siblings reuse it,
+and compatibility `Q` is not charged again at each ancestor. Both padded
+ordinary calls use this same reserve. The genuine other high field stays
+`R`, and each padded return is immediately restricted to its genuine rows.
+These implications retain the completed-callee, exact source, pointwise
+restoration, restriction and ownership hypotheses of those predecessors.
+
+No callback or default backend is changed here, and the verifier does not
+run a selected-parameter Boolean payload. The setup implementation can be
+passed to the existing plan hook only with its inherited consumer contracts.
+The older simultaneous full-depth-format contract remains a distinct,
+stronger requirement.
+
+If PR3264's old `D(e)` selector fits, its borrowing is feasible here because
+`D(n)<=D(e)` and the guard stock is nondecreasing. The new least borrowing
+is no greater. The existing sufficient fallback cutoff therefore remains
+sufficient, conditional on the same source contracts. This says neither that
+all inputs fit nor that a smaller borrowing is a runtime speed factor.
+
+Independent integer specifications and reduced literal Count replays are
+finite evidence for this refinement. They do not discharge full-cover,
+completed-leaf, source-access, uniform physical-cost, routing, precision,
+outer-transfer or complete multiplication-theorem obligations. All children,
+helpers, padding, restriction, output copies and cleanup remain charged in
+the inherited consumer recurrence. No selected-frontier change is claimed.
+
+Prepared by Hiroki Kumazaki with substantial OpenAI Codex assistance.
+Predecessor attribution above is retained. Apache-2.0.
diff --git a/research/encoded-body-depth-borrowing/README.md b/research/encoded-body-depth-borrowing/README.md
new file mode 100644
index 0000000000..7c4e749af3
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/README.md
@@ -0,0 +1,131 @@
+# Least actual-body borrowing on Count tapes
+
+This closes the encoded-selector and setup-invoice part of [PR3486's
+handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19010306)
+at `991861d40a1ebdbbf35be9adc1726e6af5b71e49`. The predecessor proves the
+threshold with host integers; this package computes it using the retained
+binary Count tapes and fixed physical roles. It is an opt-in setup component,
+not a selected supplier, default-backend change or new multiplication bound.
+
+## Result
+
+For compiled radix/profile constants, fix the atom width
+`w=ceil(e^(A/C))` before borrowing. The selector returns the least `k` with
+
+```
+2*k < e,
+n = floor((e-k)/w) >= m,
+q^k >= S_D(n),
+D(n) = 0 if n<m, otherwise 1+D(r*floor(n/m)),
+S_0 = 1, S_d = Q * (W*|GL_m(F_q)|*q^(m*m*(w-1)))^d for d>0.
+```
+
+`selector.select_body_stock` uses encoded bisection, actual-body depth at
+every trial, and MSB-scanned Count exponentiation. It accepts the same compiled
+profile vocabulary and returns the seven owned Count fields plus `fits` used
+by the existing ordinary plan hook. No host-decoded input or input-dependent
+depth table is used. On no fit, `width` is retained, `depth/borrowed/body/remainder`
+are zero and `stock/rows` are one; these are explicitly nonadmitted sentinels.
+The caller must close every plan with `close_plan`.
+
+For `h=1+ceil(log2(e+1))`, the complete setup invoice is
+
+```
+time  O(h^3 + h^2*(e+w*h)^2),
+space O(e+w*h), on at most 24 roles including the borrowed input.
+```
+
+Constants depend on the compiled radix/profile. This includes width selection,
+level construction, discarded trials, **full** trial radix powers, final-plan
+recomputation and cleanup. It fits within the inherited 64-role setup allowance.
+For the selected fixed exponent `17/10000`, the time is `O(e^2*h^2+h^3)`.
+The relation `e=O_q(log V)` makes this a fixed polynomial setup addition to the
+inherited full payload bill. These are conditional tape-operation bounds, not
+measured performance or a new universal physical compiler proof.
+
+## Discriminating examples
+
+Use `q=2,m=2,r=1,W=Q=1,w=1`:
+
+| Original width | Exact decision | What it checks |
+| --- | --- | --- |
+| 12 | No fit | `k=6` covers the stock but violates strict `2k<e`. |
+| 13 | `k=6,n=7,D=2,S=36,R=64` | Actual-body depth fits where the old `D(e)` choice needs `k=8` and fails. |
+| 24 | `k=9,n=15,D=3,S=216,R=512` | Required-stock substitution cycles `8 → 11 → 8`; the least admitted `k` exceeds its own required digit count of 8. |
+
+With width exponent `1/3`, `e=61` gives `w=4,k=30,n=7,remainder=3`.
+The literal tape tests also cross the ceiling-width boundaries `8/9` and
+`64/65`. These are reduced setup examples, not selected GL64 payload runs.
+
+## Verification and scope
+
+```sh
+python3.12 -B scripts/research_package.py --package research/encoded-body-depth-borrowing
+python3.12 -I -O -B research/encoded-body-depth-borrowing/verify.py
+```
+
+The standard-library replay authenticates 20 unchanged source inputs and the
+retained PR3486 proof. Runtime uses the predecessor's already-archived tape
+vocabulary; no executable or Git object from pending PR3486 is needed.
+`verify.py --emit` prints the deterministic receipt without overwriting it.
+
+- **171 literal Count cases**, 84 fitted, match independently written forward
+  enumeration and inverse-depth slab specifications. Physical constructors and
+  numerical decoding are disabled during selection. Borrowed inputs return
+  unchanged at their origin; all temporary/result leases close.
+- The independent integer methods agree on **5,760 cases**. All 1,139 admitted
+  plans satisfy the padded quotient and compatibility guards at every depth.
+- Twelve controls cover invalid contracts, zero input, a semantic failure after
+  complete trial construction, and executed mutants using old depth, omitting
+  Q, weakening strict fit, using the wrong radix exponent or returning the false
+  bisection endpoint. The five algorithm mutants reach the semantic oracle.
+- The observed peak is **19 setup roles**; the written 24-role bound comes from
+  a separate inventory of allocation sites, including constructor temporaries.
+
+The first literal replay exposed a scan-origin bug in the new exponentiation;
+the fixed code moves right from `LEFT` before using the retained rewind loop.
+The published tests exercise this path. Successful, fallback and the tested
+semantic-failure cleanup are covered; arbitrary interruption or allocation
+failure inside inherited arithmetic is not a transactional guarantee.
+
+The optimality, stock and inverse-depth theorems remain PR3486's results.
+[PROOF.md](PROOF.md) establishes their encoded refinement and setup invoice.
+It retains the NODE-guard covering constraint, fixed width, completed-callee,
+pointwise restoration, source, ordinary/C0 physical and uniform-cost premises.
+The simultaneous full-depth-format consumer needs its separate stronger
+contract. All children, helpers, padding, routing and consumer costs remain.
+No selected payload, full cold replay, human review or proof kernel is claimed.
+
+## Open next questions
+
+1. Bind this plan factory to one fully specified reduced completed ordinary
+   caller, checking both padded returns, all dirty spectators and fallback.
+   Start at the existing `execute_plan` hook; its physical caller contract must
+   be explicit. This package verifies setup and does not execute that payload.
+2. Can exact saturation reduce rejected-trial radix-power work? Start by capping
+   the comparison at the actual stock, proving the same threshold, and retaining
+   full materialization for the accepted plan. No faster implementation is
+   established here.
+
+## Attribution and coordination
+
+Hiroki Kumazaki with substantial OpenAI Codex assistance for analysis, code,
+execution, writing and separate same-session AI-agent checks. Apache-2.0.
+Credit Nick Petalas (PR3486 threshold and PR3246 one-factor reserve), Tekalign
+(PR3264 consumer), Jose Manuel (PR2899/2809 encoded arithmetic and physical
+setup), David Arias (PR2753 recursive caller), Ross Richardson (PR2420 format
+contract), and their retained BIT/geometry/compiler lineage. The byte-identical
+predecessor proof retains its source, hash and author attribution in SOURCES.json.
+
+Base: canonical main `6f100d4bb5083f8c35d96fd95a539811c62f245c`, priority
+revision 6. This changes the `selected-stock-envelope` card to the live encoded
+implementation handoff. Entry overlap covered 410 open PRs and 2,332 Discussion
+records with complete pagination, plus focused current-thread checks; it excludes
+unpublished work and exhaustive historical diffs. [Canonical claim/result](https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19010614).
+
+The publication refresh also found the concurrent [factor-two padding
+claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19010608).
+That work changes the covering premise to permit `S/2<R<S` and explicitly stops
+before a full encoded borrowing selector. This package keeps `R>=S` and supplies
+that selector only for the existing covering contract; no result is transferred
+between the two admission predicates.
diff --git a/research/encoded-body-depth-borrowing/RESULT.json b/research/encoded-body-depth-borrowing/RESULT.json
new file mode 100644
index 0000000000..661102d0a1
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/RESULT.json
@@ -0,0 +1,149 @@
+{
+  "encoded_cases": 171,
+  "fitted": 84,
+  "independent": {
+    "accepted": 1139,
+    "cases": 5760,
+    "records_sha256": "23e11481f74f42a9750e47e110dff39e4ea7868c65bb6b937613fc71a939cacb",
+    "rejected": 4621
+  },
+  "peak_setup_roles": 19,
+  "records_sha256": "9d1b5e8ad3aab75cbcf6236049cf19bd4de89372c6c38b4fccac3959b7252b3e",
+  "rejection_controls": [
+    "compiled-contract-0",
+    "compiled-contract-1",
+    "compiled-contract-2",
+    "compiled-contract-3",
+    "compiled-contract-4",
+    "zero-original",
+    "completed-trial-failure-cleanup",
+    "old-original-depth",
+    "missing-Q",
+    "nonstrict-fit",
+    "wrong-radix-exponent",
+    "false-final-endpoint"
+  ],
+  "runtime_boundary": "source inspection: no cells/head/physical/inspect/bit_length access; literal runtime also seals constructors and Word.inspect",
+  "source_inputs": 20,
+  "witnesses": [
+    {
+      "args": [
+        12,
+        2,
+        2,
+        1,
+        1,
+        1,
+        0,
+        1
+      ],
+      "guards": null,
+      "peak_roles": 19,
+      "plan": {
+        "body": 0,
+        "borrowed": 0,
+        "depth": 0,
+        "fits": false,
+        "remainder": 0,
+        "rows": 1,
+        "stock": 1,
+        "width": 1
+      },
+      "tape_steps": 14814
+    },
+    {
+      "args": [
+        13,
+        2,
+        2,
+        1,
+        1,
+        1,
+        0,
+        1
+      ],
+      "guards": {
+        "padded": 72,
+        "quotients": [
+          12,
+          2
+        ]
+      },
+      "peak_roles": 17,
+      "plan": {
+        "body": 7,
+        "borrowed": 6,
+        "depth": 2,
+        "fits": true,
+        "remainder": 0,
+        "rows": 64,
+        "stock": 36,
+        "width": 1
+      },
+      "tape_steps": 39770
+    },
+    {
+      "args": [
+        24,
+        2,
+        2,
+        1,
+        1,
+        1,
+        0,
+        1
+      ],
+      "guards": {
+        "padded": 648,
+        "quotients": [
+          108,
+          18,
+          3
+        ]
+      },
+      "peak_roles": 17,
+      "plan": {
+        "body": 15,
+        "borrowed": 9,
+        "depth": 3,
+        "fits": true,
+        "remainder": 0,
+        "rows": 512,
+        "stock": 216,
+        "width": 1
+      },
+      "tape_steps": 51198
+    },
+    {
+      "args": [
+        61,
+        2,
+        2,
+        1,
+        1,
+        1,
+        1,
+        3
+      ],
+      "guards": {
+        "padded": 1207959552,
+        "quotients": [
+          49152,
+          2
+        ]
+      },
+      "peak_roles": 17,
+      "plan": {
+        "body": 7,
+        "borrowed": 30,
+        "depth": 2,
+        "fits": true,
+        "remainder": 3,
+        "rows": 1073741824,
+        "stock": 603979776,
+        "width": 4
+      },
+      "tape_steps": 191126
+    }
+  ]
+}
diff --git a/research/encoded-body-depth-borrowing/SOURCES.json b/research/encoded-body-depth-borrowing/SOURCES.json
new file mode 100644
index 0000000000..4c4b74f1ec
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/SOURCES.json
@@ -0,0 +1,141 @@
+{
+  "schema_version": 1,
+  "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "research/bit2234-stock-threshold/README.md",
+      "usage": "input",
+      "git_blob": "ede0d322c477af91d4c2cc33db0fd10958f45eab",
+      "sha256": "1e050c9f963421d751d9208092f9a15321ed77810e03912df8eb5eb56bbb06e7"
+    },
+    {
+      "path": "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL-TEMPLATE.json.gz",
+      "usage": "input",
+      "git_blob": "9eafb8776cbf78c72124f833534469ddfa5e98ec",
+      "sha256": "0357b7cfbd7c29b4983982baf153c8a9f1e1e412690cd7fa9fc3d23d7963b20f"
+    },
+    {
+      "path": "research/community-hyperplane599-audit/pr589/bit589/v9/nine/GEOMETRY.json",
+      "usage": "input",
+      "git_blob": "44006542202ca6037533a754f0bcd00549d7e088",
+      "sha256": "0058c491d839142aa99ef86a5ec697ce99857632228531512ea3fa74fb24d734"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+      "usage": "input",
+      "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13",
+      "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4"
+    },
+    {
+      "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
+      "usage": "input",
+      "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a",
+      "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+    },
+    {
+      "path": "research/ordinary-one-factor-stock/PROOF.md",
+      "usage": "input",
+      "git_blob": "bcfe2e4ad694113967b0042059fd81d5d90afd44",
+      "sha256": "0ac52b1c1a237adf64dae8dafedad5c83f09f5392c057b510bc2a04faadcf4ed"
+    },
+    {
+      "path": "research/ordinary-one-factor-stock/selector.py",
+      "usage": "input",
+      "git_blob": "0a4c769610d72a6474b1d82ceb1c7182772bbd54",
+      "sha256": "b44a86e43b488e4e48a394e07429f16d09e87b6e4cbbc5e22a95ad29f56880f3"
+    },
+    {
+      "path": "research/physical-ordinary-interchange/PROOF.md",
+      "usage": "input",
+      "git_blob": "12be1f06062090fcc68e598bae250f185e3d8524",
+      "sha256": "8a1c2145cd8f080026488a571d95813c09679aa323f19aeaef0ea98030136e1c"
+    },
+    {
+      "path": "research/physical-ordinary-interchange/encoded.py",
+      "usage": "input",
+      "git_blob": "2280fa98ff5e4da7c4909814ce4a1c405605ada8",
+      "sha256": "10ad2fa5902a48d49cf2b89a30b3f2711d63a6a43b9512a6427affcdf07335a7"
+    },
+    {
+      "path": "research/physical-ordinary-interchange/inputs/pr2808.tar",
+      "usage": "input",
+      "git_blob": "191b0b3342d12a630d60643439afa3284641c2d5",
+      "sha256": "2ab59c6d0ad00c001ecbe44090b66871ec3d2c1fdc51daa503109e56f3285cab"
+    },
+    {
+      "path": "research/physical-ordinary-interchange/inputs/pr2809.tar",
+      "usage": "input",
+      "git_blob": "21ff4b5b9942dbc82b60b4546d39785daa22ba86",
+      "sha256": "ee1d4ec05e3c872d264be3b38f71a8c153acf37427f5d3ba87f8e15440c9ccf0"
+    },
+    {
+      "path": "research/physical-ordinary-interchange/session.py",
+      "usage": "input",
+      "git_blob": "09f645bbf0c6c3d41d0c03e8031adc4e81744ac1",
+      "sha256": "45ee809b27a69ca5576361922fd2760f568c9a98864d4c55c4fee3003ee3c9ad"
+    },
+    {
+      "path": "research/physical-ordinary-interchange/source.py",
+      "usage": "input",
+      "git_blob": "8594fc62cee8a111958561b75045c8ec16ebfa47",
+      "sha256": "4bd047a1272374880962d3074f1e50de717518a3a181f11607e820afe50dd4e5"
+    },
+    {
+      "path": "research/pr589-five-helper-hosting/PROOF.md",
+      "usage": "input",
+      "git_blob": "bbd3f12b9a32b3ad3cba85a2d5a1b3054214fa02",
+      "sha256": "59cae781bfbe1a01ed9e66a8efeeb5a2b995e5ecdf908586b23ecc39f2b8d647"
+    },
+    {
+      "path": "research/pr589-five-helper-hosting/verify.py",
+      "usage": "input",
+      "git_blob": "dbc71f56bb4205ebe378ada1f9f4ea88630d1d39",
+      "sha256": "cf90e19ae9991b0698be03d395a8cc29061ecb307eb7fea19adfb2d23c25a367"
+    },
+    {
+      "path": "research/recursive-parking-boundary/README.md",
+      "usage": "input",
+      "git_blob": "251f335ebaccc11d69393ee7aeb5a2e84526d0bb",
+      "sha256": "491aa208391ee4c2936510b1a5c5c018dd5509d9a0e88687c72ab8406cd77b18"
+    },
+    {
+      "path": "research/selected-bit-local-ring-sweeps/PROOF.md",
+      "usage": "input",
+      "git_blob": "4330de85dd9862ed15d84ab917887d249753df99",
+      "sha256": "846c59440cc99e28bae93ad2af99525bc769de29368080071b8427141215b4f7"
+    },
+    {
+      "path": "research/selected-bit-recursive-closure/PROOF.md",
+      "usage": "input",
+      "git_blob": "6c410cab5713979214a45835091fbeb9ee9b8531",
+      "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344"
+    },
+    {
+      "path": "upstream/build/sections/02-streams.tex",
+      "usage": "input",
+      "git_blob": "088fceea1867abc76271d7efe7532b779fee9039",
+      "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ],
+  "predecessor": {
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3486",
+    "commit": "991861d40a1ebdbbf35be9adc1726e6af5b71e49",
+    "original_path": "research/selected-body-depth-borrowing/PROOF.md",
+    "retained_path": "predecessor/PR3486-PROOF.md",
+    "sha256": "0671a0a1f4b31e18fb00ce7a3fbf13986fe61b45b3252a90212af491f815e671",
+    "git_blob": "5929215d66e47f30e08df224ce56bb2e925f4dd6",
+    "usage": "byte-identical proof reference; no predecessor executable imported"
+  }
+}
diff --git a/research/encoded-body-depth-borrowing/TASK.json b/research/encoded-body-depth-borrowing/TASK.json
new file mode 100644
index 0000000000..5c17bfe548
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/TASK.json
@@ -0,0 +1,131 @@
+{
+  "schema_version": 1,
+  "task_id": "selected-stock-envelope",
+  "scope_key": "pr3486-encoded-actual-body-selection",
+  "base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c",
+  "priority_revision": 6,
+  "scope_status": "changed",
+  "original_card": {
+    "id": "selected-stock-envelope",
+    "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?",
+    "starting_points": [
+      "research/selected-bootstrap-stock-audit/README.md",
+      "research/bootstrap-cutoff-time-space-split/README.md",
+      "certificates/selected-result.json",
+      "docs/research/community-efficient1000-review.md",
+      "research/stock-margin-chain/README.md"
+    ],
+    "methods": [
+      "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.",
+      "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope."
+    ],
+    "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.",
+      "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."
+    },
+    "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.",
+    "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.",
+    "allowed_variations": [
+      "One stage or one explicit reserve/depth implication.",
+      "An independently checked same-domain proof repair, retaining all remaining assumptions."
+    ],
+    "scope_change_triggers": [
+      "Importing the historical 57604 or 252 allowance without a selected-producer binding.",
+      "Calling a conditional fit lemma a full outer-proof adoption.",
+      "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality."
+    ],
+    "overlap_terms": [
+      "selected stock",
+      "stock envelope",
+      "bootstrap cutoff",
+      "1956",
+      "1965",
+      "1990",
+      "2972",
+      "stock-margin-chain",
+      "actual_stock_coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.",
+        "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation",
+        "remaining": "Derive one actual reserve/depth coefficient from the selected producer.",
+        "status": "reviewed",
+        "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "actual_scope": "Refine PR3486 least fixed-width actual-body borrowing to Count tapes with a fixed role bound and conditional setup invoice.",
+  "scope_change_reason": "The current live PR3486 handoff already proves the host-integer threshold and asks for encoded selection and setup charges; older coefficient/cutoff tasks have newer followups.",
+  "bottleneck_link": "Discharges the concrete encoded setup obligation between an actual-body stock theorem and the existing ordinary plan-factory interface, with complete physical callee costs still conditional.",
+  "stop_rule": "Stop at the encoded selector and setup proof; do not execute immense selected payloads, replace a default backend, treat runtime measurements as supplier admission, or change the frontier.",
+  "evidence": "171 literal Count plans with sealed constructors and no numerical decoding; 5760 independent forward/slab cases; 12 rejection controls; source-bound retained RESULT.json. Registered, optimized and committed-export checks recorded at publication.",
+  "author": "Hiroki Kumazaki",
+  "ai_assistance": "Substantial OpenAI Codex analysis, code, execution, writing and separate same-session AI-agent checks. No independent human or formal proof-kernel review claimed.",
+  "outcome": "completed",
+  "open_questions": [
+    {
+      "question": "Can an actual completed ordinary caller use this selector at its existing execute_plan hook and retain both padded returns and all dirty spectators?",
+      "why_it_matters": "The encoded plan is available, but this package executes no selected payload and does not discharge its physical consumer contracts.",
+      "first_step": "Run one fully specified reduced fitted ordinary packet with this plan factory; compare every output and restored spectator with a separate oracle, including no-fit fallback.",
+      "blocked_by": "The full selected GL64 payload and universal completed-callee/physical C0 premises remain outside this bounded setup package."
+    },
+    {
+      "question": "Can bounded saturation reduce rejected-trial q^k work without changing the exact returned plan?",
+      "why_it_matters": "The current setup intentionally materializes full radix powers, making their e-bit cost explicit.",
+      "first_step": "Cap trial comparisons at the exact stock while retaining final exact materialization; prove the monotone decision and add equality/one-below failure controls before claiming a lower invoice.",
+      "blocked_by": "No faster setup or measured runtime improvement is established here."
+    }
+  ],
+  "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19010614",
+  "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19010306",
+  "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129",
+  "overlap": {
+    "open_prs": {
+      "fetched_at": "2026-10-18T03:46:50.159026+00:00",
+      "complete_pagination": true,
+      "records": 410
+    },
+    "discussions": {
+      "fetched_at": "2026-10-18T03:49:39.151988+00:00",
+      "complete_pagination": true,
+      "records": 2332
+    }
+  },
+  "overlap_limits": "Complete open PR bodies and Discussion records, plus targeted current2319/handoff reads and local package notes. No exhaustive historical diffs or unpublished-work coverage. Offline targeted query reused the freshly completed online snapshot.",
+  "environment": {
+    "python": "3.12.13",
+    "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.43"
+  },
+  "review_corrections": [
+    "Initial MSB exponent scan failed to move right from LEFT before the retained rewind primitive; literal tape smoke exposed this and the published _power returns inside the record before rewind.",
+    "A missing-Q test mutant initially called multiply_small(1), which the retained primitive rejects; it was replaced by a genuine omitted multiplication, verified to reach the independent semantic oracle."
+  ],
+  "unrun": [
+    "Selected GL64 payload execution",
+    "Full selected cold replay",
+    "Universal physical C0/ordinary refinement",
+    "Independent human review",
+    "Formal proof-kernel check"
+  ],
+  "publication_refresh": {
+    "utc": "2026-10-18T03:59:33.413216+00:00",
+    "canonical_main": "6f100d4bb5083f8c35d96fd95a539811c62f245c",
+    "predecessor_head": "991861d40a1ebdbbf35be9adc1726e6af5b71e49",
+    "result": "Guidance and predecessor unchanged. Focused open PR search returned3486; latest12 canonical2319 comments and all their replies inspected. Concurrent factor-two padding claim19010608 changes R>=S to S/2<R<S and explicitly excludes full encoded borrowing. It is complementary and not adopted.",
+    "parallel_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19010608"
+  },
+  "verification": {
+    "normal_registered": "PASS_REGISTERED_RESEARCH_PACKAGE",
+    "isolated_optimized": "PASS_ENCODED_BODY_DEPTH ed69e292ef0e5c75ba5a993864b77e741ca603d2535e146f57abd27672d6ca7d",
+    "same_session_review": "Separate AI agents wrote primary selector, independent oracle and setup proof; independent final read-only review found no blocking issue. No human or proof-kernel review."
+  }
+}
diff --git a/research/encoded-body-depth-borrowing/VERIFY.json b/research/encoded-body-depth-borrowing/VERIFY.json
new file mode 100644
index 0000000000..b25ff99ee9
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/VERIFY.json
@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/bit2234-stock-threshold/README.md",
+    "research/community-hyperplane599-audit/pr589/bit589/v9/hosted/GLOBAL-TEMPLATE.json.gz",
+    "research/community-hyperplane599-audit/pr589/bit589/v9/nine/GEOMETRY.json",
+    "research/e8-bit-p111-tuned/tune/EXPECTED.json",
+    "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz",
+    "research/ordinary-one-factor-stock/PROOF.md",
+    "research/ordinary-one-factor-stock/selector.py",
+    "research/physical-ordinary-interchange/PROOF.md",
+    "research/physical-ordinary-interchange/encoded.py",
+    "research/physical-ordinary-interchange/inputs/pr2808.tar",
+    "research/physical-ordinary-interchange/inputs/pr2809.tar",
+    "research/physical-ordinary-interchange/session.py",
+    "research/physical-ordinary-interchange/source.py",
+    "research/pr589-five-helper-hosting/PROOF.md",
+    "research/pr589-five-helper-hosting/verify.py",
+    "research/recursive-parking-boundary/README.md",
+    "research/selected-bit-local-ring-sweeps/PROOF.md",
+    "research/selected-bit-recursive-closure/PROOF.md",
+    "upstream/build/sections/02-streams.tex"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Literal fixed-role Count plans against independent forward scan and inverse-depth slabs, source pins, ownership, rejection and algorithm mutations."
+    }
+  ]
+}
diff --git a/research/encoded-body-depth-borrowing/independent.py b/research/encoded-body-depth-borrowing/independent.py
new file mode 100644
index 0000000000..7684a46c3f
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/independent.py
@@ -0,0 +1,144 @@
+"""Host-integer specifications, independent of the Count-tape implementation.
+
+The linear scan evaluates every geometrically legal borrowing in increasing
+order. The second specification instead inverts the child-depth thresholds.
+Neither imports the selector, its tape runtime, or its generated receipt.
+Hiroki Kumazaki with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+
+import itertools
+import json
+from hashlib import sha256
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def parameters(e, q, dimension, child_rank, row_factor, compatibility,
+               numerator=0, denominator=1):
+    values = (e, q, dimension, child_rank, row_factor, compatibility,
+              numerator, denominator)
+    require(all(type(value) is int for value in values), "integer parameters")
+    require(e >= 1 and q >= 2 and 1 <= child_rank < dimension,
+            "positive width, radix, and contracting depth")
+    require(row_factor >= 1 and compatibility >= 1,
+            "positive stock factors")
+    require(denominator > 0 and 0 <= numerator <= denominator,
+            "width exponent in [0,1]")
+    width = 1
+    target = e ** numerator
+    while width ** denominator < target:
+        width += 1
+    group_order = 1
+    for column in range(dimension):
+        group_order *= q ** dimension - q ** column
+    level = row_factor * group_order * q ** (dimension * dimension * (width - 1))
+    return width, level
+
+
+def depth(body, dimension, child_rank):
+    result = 0
+    while body >= dimension:
+        body = child_rank * (body // dimension)
+        result += 1
+    return result
+
+
+def plan_at(e, q, width, dimension, child_rank, level, compatibility, borrowed):
+    body, remainder = divmod(e - borrowed, width)
+    actual_depth = depth(body, dimension, child_rank)
+    stock = 1 if actual_depth == 0 else compatibility * level ** actual_depth
+    return dict(fits=2 * borrowed < e and body >= dimension and q ** borrowed >= stock,
+                width=width, depth=actual_depth, stock=stock, rows=q ** borrowed,
+                borrowed=borrowed, body=body, remainder=remainder)
+
+
+def specification(e, q, dimension, child_rank, row_factor, compatibility,
+                  numerator=0, denominator=1):
+    """Return the first admitted plan or canonical fallback, by linear scan."""
+    width, level = parameters(e, q, dimension, child_rank, row_factor,
+                              compatibility, numerator, denominator)
+    for borrowed in range((e - 1) // 2 + 1):
+        candidate = plan_at(e, q, width, dimension, child_rank, level,
+                            compatibility, borrowed)
+        if candidate["fits"]:
+            return candidate
+    return fallback(width)
+
+
+def fallback(width):
+    return dict(fits=False, width=width, depth=0, stock=1, rows=1,
+                borrowed=0, body=0, remainder=0)
+
+
+def slab_specification(e, q, dimension, child_rank, row_factor, compatibility,
+                       numerator=0, denominator=1):
+    """Minimize inverse-depth intervals, with no forward depth recurrence."""
+    width, level = parameters(e, q, dimension, child_rank, row_factor,
+                              compatibility, numerator, denominator)
+    threshold = dimension
+    stock = compatibility
+    exponent, rows, level_number = 0, 1, 0
+    candidates = []
+    while threshold <= e // width:
+        level_number += 1
+        stock *= level
+        while rows < stock:
+            exponent += 1
+            rows *= q
+        following = dimension * ((threshold + child_rank - 1) // child_rank)
+        lower = max(0, exponent, e - width * following + 1)
+        upper = min((e - 1) // 2, e - width * threshold)
+        if lower <= upper:
+            body, remainder = divmod(e - lower, width)
+            candidates.append(dict(fits=True, width=width, depth=level_number,
+                                   stock=stock, rows=q ** lower, borrowed=lower,
+                                   body=body, remainder=remainder))
+        threshold = following
+    return min(candidates, key=lambda candidate: candidate["borrowed"]) if candidates else fallback(width)
+
+
+def padded_guards(plan, q, dimension, row_factor, compatibility):
+    """Check every literal child quotient and Q guard for a selected plan."""
+    require(plan["fits"], "admitted plan")
+    group_order = 1
+    for i in range(dimension):
+        group_order *= q ** dimension - q ** i
+    level = row_factor * group_order * q ** (dimension ** 2 * (plan["width"] - 1))
+    stock, genuine = plan["stock"], plan["rows"]
+    padded = ((genuine + stock - 1) // stock) * stock
+    require(genuine <= padded < 2 * genuine, "strict padding envelope")
+    remaining = padded
+    quotients = []
+    for _ in range(plan["depth"]):
+        remaining, residue = divmod(remaining, level)
+        require(residue == 0, "complete local stock quotient")
+        require(remaining % compatibility == 0, "compatibility guard")
+        quotients.append(remaining)
+    return dict(padded=padded, quotients=quotients)
+
+
+def check():
+    """Bounded arithmetic evidence; it is not an encoded runtime replay."""
+    records = []
+    accepted = 0
+    for q, (dimension, child_rank), row_factor, compatibility, exponent in itertools.product(
+            (2, 3), ((2, 1), (3, 1), (3, 2)), (1, 2), (1, 2, 5), ((0, 1), (1, 3))):
+        for e in range(1, 81):
+            args = (e, q, dimension, child_rank, row_factor, compatibility, *exponent)
+            forward = specification(*args)
+            inverse = slab_specification(*args)
+            require(forward == inverse, "forward scan equals inverse-depth slabs")
+            if forward["fits"]:
+                padded_guards(forward, q, dimension, row_factor, compatibility)
+                accepted += 1
+            records.append([list(args), forward])
+    serial = json.dumps(records, sort_keys=True, separators=(",", ":"))
+    return dict(cases=len(records), accepted=accepted, rejected=len(records) - accepted,
+                records_sha256=sha256(serial.encode()).hexdigest())
+
+
+if __name__ == "__main__":
+    print("PASS_INDEPENDENT_BODY_DEPTH", json.dumps(check(), sort_keys=True))
diff --git a/research/encoded-body-depth-borrowing/predecessor/PR3486-PROOF.md b/research/encoded-body-depth-borrowing/predecessor/PR3486-PROOF.md
new file mode 100644
index 0000000000..5929215d66
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/predecessor/PR3486-PROOF.md
@@ -0,0 +1,195 @@
+# Least borrowing at the actual body depth
+
+Fix integers q>=2, w>=1, m>r>=1, b>=1 and Q>=1. The atom width w is fixed
+before borrowing. Define
+
+```
+D(n)=0                              for 0<=n<m,
+D(n)=1+D(r floor(n/m))              for n>=m,
+S_0=1,   S_d=Q b^d                 for d>=1,
+L_d=min{j>=0 : q^j>=S_d}.
+```
+
+These statements concern this prescribed reserve and the current NODE guard
+contract. They do not assert a minimum for arbitrary implementations. A
+consumer requiring the older simultaneous full depth-d formats retains its
+stronger divisor.
+
+Optimality below retains the selector's explicit covering constraint
+q^k>=S_D(n). It does not optimize over alternative padding/volume budgets.
+For example, R<S can sometimes still give R'=S<2R. Such a relaxation is
+outside the stated predicate and is not ruled out by this result.
+
+## 1. The exact admissibility predicate
+
+For positive original width e and borrowed width k, put
+
+```
+n(k)=floor((e-k)/w),   ell(k)=(e-k) mod w,
+U=min(floor((e-1)/2), e-mw).
+```
+
+A fitted plan in this guard model exists exactly when some integer k in
+[0,U] satisfies
+
+```
+k >= F(k),   F(k)=L_D(n(k)).                         (1)
+```
+
+Indeed, k<=floor((e-1)/2) is precisely strict fit 2k<e. The condition
+k<=e-mw is precisely n(k)>=m. The reserve condition q^k>=S_D(n(k)) is
+equivalent to (1) by the definition of L. These are the three conditions
+being optimized. Complete physical execution has additional premises below.
+
+The child map is nondecreasing and strictly contracts positive internal
+widths. Thus D is finite and nondecreasing. The latter also follows by strong
+induction: for m<=x<=y, compare the two smaller child widths; if x<m its
+depth is zero. S_d and L_d are nondecreasing, including d=0, since b,Q>=1.
+As k increases, n(k), D(n(k)) and F(k) are nonincreasing. Therefore (1) is
+a monotone predicate on [0,U].
+
+If U<0 or U<F(U), there is no fitted plan. Otherwise bisection between the
+false sentinel -1 and true endpoint U returns the least k satisfying (1).
+Every tested midpoint is nonnegative; the sentinel is never passed to F.
+The integer interval length at least halves, rounded up, at each step.
+Thus ceil(log2(U+2)) steps suffice. The implementation allows
+e.bit_length()+1 steps. The theorem has no finite e cap; replay declares one.
+
+This is an inequality problem. The least k need not equal F(k). Replacing
+the predicate by k=F(k) can discard the optimum or fail to terminate, as
+section 4 demonstrates within the selected parameter domain.
+
+## 2. An independent inverse-depth formula
+
+The least n of depth at least d has thresholds
+
+```
+a_1=m,   a_(d+1)=m ceil(a_d/r).
+```
+
+Direct inversion of r floor(n/m)>=a_d proves this recurrence. Hence D(n)=d
+exactly when a_d<=n<a_(d+1), for d>=1. At a proposed depth d, the three
+admissibility conditions are equivalent to
+
+```
+max(0,L_d,e-w*a_(d+1)+1) <= k
+                         <= min(floor((e-1)/2),e-w*a_d).
+```
+
+Take the lower endpoint whenever this interval is nonempty, then minimize it
+over 1<=d<=D(floor(e/w)). This is a second exact characterization of the
+same optimum. It uses inverse thresholds and finitely many depth slabs,
+rather than the forward recurrence and bisection. independent.py implements
+this formula without importing the primary implementation or its receipt.
+
+## 3. Bind the result to the existing consumer
+
+David Arias's PR2753 source supplies m=64, r=42 and the completed recursive
+caller boundary. Jose Manuel's PR2899 encoded selector fixes
+w=ceil(e^(17/10000)) before borrowing and uses D(e) to choose stock.
+Tekalign's PR3264 opt-in selector retains that depth and substitutes Nick
+Petalas's PR3246 one-factor reserve. Its proof explicitly leaves actual-body
+depth and optimal borrowing open. These exact source files are inputs in
+SOURCES.json; their bytes and attribution remain unchanged.
+
+For the selected guard reserve, at fixed source-admissible prime q>2^80,
+
+```
+N=|GL_64(F_q)|,   H=q^(4096(w-1)),
+b=28416*N*H,      Q=9475.
+```
+
+At the optimum choose R=q^k and pad to
+R'=ceil(R/S_D(n))*S_D(n). Equation (1) gives R>=S_D(n), so R<=R'<2R.
+The callee receives n and all R' fresh rows. Its actual maximum child depth
+is D(n), so PR3246's unchanged guard induction supplies every quotient and
+Q check. The entire fresh quotient passes to children; completed siblings
+reuse it.
+
+PR3264's consumer argument then applies with d=D(n) in both padded calls,
+conditional on its existing completed-callee, source access, fresh-field,
+pointwise row/spectator restoration, restriction and ownership premises.
+The genuine other high field remains R rather than R'. Both restrictions
+occur immediately after their padded call. Sequential calls do not multiply
+stock. No child, helper, routing or cleanup charge disappears.
+
+If the existing D(e) selector fits, its k is a feasible candidate for (1),
+because D(n(k))<=D(e). The new optimum is no larger. It need not be smaller,
+and smaller k is not a measured runtime gain. This implication does not
+install a Count-tape selector or prove its setup cost. The artifact is a
+bounded exact host-integer selector and a source-bound conditional interface
+theorem. No default backend or selected frontier changes.
+
+## 4. Exact selected examples without enormous stocks
+
+Take q=2^127-1, a prime greater than 2^80. The replay checks primality of
+127 and the 125-step Lucas-Lehmer residue zero for q. The
+[GIMPS prime record](https://www.mersenne.org/primes/) also identifies this
+classical prime. This explanatory reference is not a network replay input.
+
+Put P(q)=product_(i=1)^64 (1-q^-i). Independent-column counting gives
+N=q^4096 P(q). The elementary product and Bernoulli inequalities give
+
+```
+1 > P(q) > 1-1/(q-1),
+P(q)^d > 1-d/(q-1)                         for d>=1.
+```
+
+Let C_d=9475*28416^d and h_d=min{j:q^j>=C_d}. Whenever
+
+```
+C_d*(q-1-d) > q^(h_d-1)*(q-1),                     (2)
+```
+
+the exact stock lies strictly between q^(4096wd+h_d-1) and
+q^(4096wd+h_d). Thus L_d=4096wd+h_d. Both implementations check (2)
+independently at every consumed depth. No floating logarithm, rounded group
+order or materialized GL64 reserve enters acceptance. The larger group and
+reserve retain their exact defining formulae.
+
+For e=250000, the exact inequality 1<e^17<=2^10000 certifies
+w=ceil(e^(17/10000))=2. The D(e)=18 choice has k=147459 and fails 2k<e.
+Even D(floor(e/w))=17 requires k=139267 and fails. The actual-body optimum is
+
+```
+k=122882, n=63559, ell=0, D(n)=15, L_15=122882,
+2k=245764<250000.
+```
+
+Feedback therefore supplies a fitted plan in the stated guard model where
+both coarser depths select fallback. This is selected-parameter arithmetic,
+not an execution of its immense Boolean payload or a changed asymptotic
+bootstrap cutoff.
+
+For e=970370, the same exact ceiling gives w=2, and
+
+```
+F(155651)=163843,   F(163843)=155651.
+```
+
+Both k values meet the geometric fit conditions. The exact threshold a_20
+is 405312. At k=159746 the body is 405312 of depth 20 and requires 163843
+digits. At k=159747 the body is 405311 of depth 19 and requires 155651.
+The least feasible k is therefore 159747, strictly greater than its own
+required digit count. Monotonicity proves minimality and shows no fixed point
+exists: below this k the predicate fails; at or above it,
+F(k)<=155651<159747<=k. Substitution can cycle between 155651 and 163843.
+It is not a valid general selection algorithm.
+
+## 5. Evidence and limits
+
+The primary and independent depth-slab implementations agree on 8192 bounded
+cases and five selected examples. A separate exhaustive scan over every
+geometrically legal k in those cases checks the least result and each
+accepted padded quotient/Q guard. The written proof supplies the universal
+claim; finite agreement does not replace it. The actual optimized CLI accepts
+its Git-free source closure and rejects seven malformed source, receipt and
+arithmetic producers. Contracts remain active under -O.
+
+The result optimizes k at fixed w for the prescribed guard stock. It does not
+optimize w, prove a smaller universal reserve, supply encoded tapes, execute
+the selected GL64 payload, discharge universal C0/physical refinement or
+uniform costs, or solve the complex m=73 reserve. Full-cover, completed
+leaves, fresh fields, pointwise restoration, routing, precision/tape and outer
+transfer obligations remain. No new kappa, supplier admission or complete
+multiplication theorem is asserted.
diff --git a/research/encoded-body-depth-borrowing/selector.py b/research/encoded-body-depth-borrowing/selector.py
new file mode 100644
index 0000000000..0b717794f9
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/selector.py
@@ -0,0 +1,222 @@
+# SPDX-License-Identifier: Apache-2.0
+"""Actual-body borrowing on the retained fixed-role Count-tape vocabulary.
+
+Hiroki Kumazaki, with substantial OpenAI Codex assistance.
+The threshold theorem is Nick Petalas's PR3486; Count arithmetic and the
+ordinary consumer are the credited PR2899/3264 predecessor interfaces.
+"""
+
+from contextlib import contextmanager
+
+import encoded
+from cardinal_counts import Count, positive
+from words import LEFT, ONE, ZERO, need
+
+
+class _Owned:
+    """Ownership bookkeeping for a fixed set of literal operand names.
+
+    The dictionary is host bookkeeping, not an integer tape or a data table.
+    Every call site uses a fixed name; loop iterations replace those slots.
+    """
+
+    def __init__(self):
+        self.values = {}
+
+    def put(self, name, value):
+        need(name not in self.values, "unused setup operand role")
+        self.values[name] = value
+        return value
+
+    def replace(self, name, value):
+        self.drop(name)
+        return self.put(name, value)
+
+    def get(self, name):
+        return self.values[name]
+
+    def take(self, name):
+        return self.values.pop(name)
+
+    def drop(self, name):
+        self.take(name).close()
+
+    def __enter__(self):
+        return self
+
+    def __exit__(self, *_exception):
+        while self.values:
+            self.values.popitem()[1].close()
+
+
+def _power(base, exponent):
+    """Encoded nonnegative exponent, scanned MSB first; preserve both inputs."""
+    with _Owned() as work:
+        work.put("value", Count.literal(1))
+        exponent.msb()
+        try:
+            while exponent.read() != LEFT:
+                bit = exponent.read()
+                need(bit in (ZERO, ONE), "binary setup exponent")
+                value = work.get("value")
+                work.replace("value", Count.product(value, value))
+                if bit == ONE:
+                    work.replace("value", Count.product(work.get("value"), base))
+                exponent.step(-1)
+            return work.take("value")
+        finally:
+            if exponent.read() == LEFT:
+                exponent.step(1)
+            exponent.rewind()
+
+
+@contextmanager
+def _trial(original, width, borrowed, dimension, level, radix, profile,
+           compatibility):
+    """Compute the complete trial plan from the candidate borrowing tape."""
+    with _Owned() as work:
+        remaining = work.put("remaining", encoded.subtract(original, borrowed))
+        body, remainder = encoded.divide(remaining, width)
+        work.put("body", body)
+        work.put("remainder", remainder)
+        work.drop("remaining")
+        cursor = work.put("cursor", Count(body))
+        depth = work.put("depth", Count.literal(0))
+        while encoded.compare(cursor, dimension) >= 0:
+            cursor.divide_small(profile.dimension)
+            if profile.child_rank != 1:
+                cursor.multiply_small(profile.child_rank)
+            depth.increment()
+        work.drop("cursor")
+        stock = work.put("stock", _power(level, depth))
+        if not depth.zero() and compatibility != 1:
+            stock.multiply_small(compatibility)
+        work.put("rows", _power(radix, borrowed))
+        yield work
+
+
+def _fits(trial):
+    return encoded.compare(trial.get("rows"), trial.get("stock")) >= 0
+
+
+def _plan(work, trial, borrowed_name):
+    """Transfer owned results out of the two bounded temporary scopes."""
+    result = {name: trial.take(name)
+              for name in ("depth", "stock", "rows", "body", "remainder")}
+    result["width"] = work.take("width")
+    result["borrowed"] = work.take(borrowed_name)
+    result["fits"] = True
+    return result
+
+
+def _no_fit(work):
+    """Return a documented nonadmitted sentinel, never stale trial fields."""
+    for name in ("depth", "borrowed", "body", "remainder"):
+        work.put("fallback_" + name, Count.literal(0))
+    for name in ("stock", "rows"):
+        work.put("fallback_" + name, Count.literal(1))
+    result = {name: work.take("fallback_" + name)
+              for name in ("depth", "borrowed", "body", "remainder", "stock", "rows")}
+    result["width"] = work.take("width")
+    result["fits"] = False
+    return result
+
+
+def select_body_stock(original, q, profile=encoded.Profile(row_factor=28416),
+                      compatibility=9475):
+    """Return the least admitted actual-body borrowing, using Count tapes.
+
+    The radix and profile are compiled constants. The caller retains
+    ``original`` and owns every returned Count. Successful plans satisfy
+    2*k<e, n=floor((e-k)/w)>=m and q**k>=Q*b**D(n), with fixed
+    w=ceil(e**(numerator/denominator)) and
+    b=W*|GL_m(F_q)|*q**(m*m*(w-1)).
+
+    A no-fit plan has the true width, zero depth/borrowed/body/remainder and
+    unit stock/rows. Its fields are a sentinel, not an admitted invocation.
+    This function does not change a backend callback or execute a payload.
+    """
+    need(type(q) is int and q >= 2, "compiled radix at least two")
+    need(type(compatibility) is int and compatibility >= 1,
+         "positive compiled compatibility factor")
+    need(type(profile.row_factor) is int and profile.row_factor >= 1,
+         "positive compiled live-family factor")
+    need(type(profile.dimension) is int and type(profile.child_rank) is int
+         and 1 <= profile.child_rank < profile.dimension,
+         "contracting compiled depth profile")
+    need(type(profile.numerator) is int and type(profile.denominator) is int
+         and profile.denominator > 0
+         and 0 <= profile.numerator <= profile.denominator,
+         "compiled width exponent between zero and one")
+    positive(original)
+    with _Owned() as work:
+        width = work.put("width", encoded.atom_width(
+            original, profile.numerator, profile.denominator))
+        dimension = work.put("dimension", Count.literal(profile.dimension))
+        one = work.put("one", Count.literal(1))
+        minimum_body = work.put("minimum_body", Count(width))
+        minimum_body.multiply_small(profile.dimension)
+        if encoded.compare(original, minimum_body) < 0:
+            return _no_fit(work)
+
+        strict = work.put("strict", encoded.subtract(original, one))
+        strict.divide_small(2)
+        body_limit = work.put("body_limit", encoded.subtract(original, minimum_body))
+        work.drop("minimum_body")
+        if encoded.compare(strict, body_limit) <= 0:
+            work.put("upper", work.take("strict"))
+            work.drop("body_limit")
+        else:
+            work.put("upper", work.take("body_limit"))
+            work.drop("strict")
+
+        # Only compiled source constants use host arithmetic. Width-dependent
+        # high-field multiplicities and every trial reserve remain encoded.
+        order = 1
+        for position in range(profile.dimension):
+            order *= q ** profile.dimension - q ** position
+        atom = work.put("atom", Count.literal(q ** (profile.dimension ** 2)))
+        exponent = work.put("exponent", encoded.subtract(width, one))
+        level = work.put("level", _power(atom, exponent))
+        level.multiply_small(profile.row_factor * order)
+        work.drop("atom")
+        work.drop("exponent")
+        radix = work.put("radix", Count.literal(q))
+        work.put("lower", Count.literal(0))
+
+        with _trial(original, width, work.get("lower"), dimension, level, radix,
+                    profile, compatibility) as trial:
+            if _fits(trial):
+                return _plan(work, trial, "lower")
+        with _trial(original, width, work.get("upper"), dimension, level, radix,
+                    profile, compatibility) as trial:
+            if not _fits(trial):
+                return _no_fit(work)
+
+        # The lower endpoint is false and the upper endpoint is true. A
+        # nonnegative encoded interval avoids a negative sentinel tape.
+        while True:
+            gap = work.put("gap", encoded.subtract(work.get("upper"), work.get("lower")))
+            adjacent = encoded.compare(gap, one) == 0
+            work.drop("gap")
+            if adjacent:
+                break
+            middle = work.put("middle", Count(work.get("lower")))
+            middle.add(work.get("upper"))
+            middle.divide_small(2)
+            with _trial(original, width, middle, dimension, level, radix,
+                        profile, compatibility) as trial:
+                destination = "upper" if _fits(trial) else "lower"
+            work.replace(destination, work.take("middle"))
+
+        with _trial(original, width, work.get("upper"), dimension, level, radix,
+                    profile, compatibility) as trial:
+            need(_fits(trial), "admitted final stock")
+            return _plan(work, trial, "upper")
+
+
+def close_plan(plan):
+    """Release all seven owned Count results, including no-fit sentinels."""
+    for key, value in plan.items():
+        if key != "fits":
+            value.close()
diff --git a/research/encoded-body-depth-borrowing/verify.py b/research/encoded-body-depth-borrowing/verify.py
new file mode 100644
index 0000000000..874bae1bc0
--- /dev/null
+++ b/research/encoded-body-depth-borrowing/verify.py
@@ -0,0 +1,248 @@
+"""Replay source-bound literal Count selection and independent failure controls.
+
+Hiroki Kumazaki with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+import ast
+from contextlib import contextmanager
+from hashlib import sha256
+import json
+from pathlib import Path
+import sys
+import tempfile
+from types import ModuleType
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def canonical(value):
+    return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False)
+
+
+def authenticate():
+    sources = json.loads((HERE / "SOURCES.json").read_text())
+    checked = 0
+    for row in sources["files"]:
+        if row["usage"] == "input":
+            require(sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"],
+                    "source pin: " + row["path"])
+            checked += 1
+    predecessor = sources["predecessor"]
+    require(sha256((HERE / predecessor["retained_path"]).read_bytes()).hexdigest()
+            == predecessor["sha256"], "retained PR3486 proof")
+    return checked
+
+
+@contextmanager
+def activate():
+    # Direct execution also avoids stale bytecode from an earlier source tree.
+    with tempfile.TemporaryDirectory(prefix="body-depth-bytecode-") as cache:
+        sys.pycache_prefix = cache
+        sys.path.insert(0, str(ROOT / "research/physical-ordinary-interchange"))
+        import source
+        source.activate()
+        sys.path.insert(0, str(HERE))
+        yield
+
+
+def observe(count):
+    """Checker only: no observer is called while the selector is running."""
+    from words import RIGHT
+    tape = count.tape
+    cells = tape.cells if hasattr(tape, "cells") else tape.physical.cells
+    end = cells.index(RIGHT, 1)
+    digits = cells[1:end]
+    require(bool(digits) and all(type(bit) is int and bit in (0, 1) for bit in digits),
+            "canonical binary observation")
+    require(len(digits) == 1 or digits[-1] == 1, "no leading zero")
+    return sum(bit << position for position, bit in enumerate(digits))
+
+
+def run_case(args, implementation=None):
+    import encoded
+    import selector
+    from cardinal_counts import Count
+    from check_support import no_decode
+    from scratch_pool import ScratchPool
+    from session import sealed_constructors
+    from independent import specification, slab_specification, padded_guards
+    e, q, m, r, w_factor, compatibility, numerator, denominator = args
+    profile = encoded.Profile(numerator=numerator, denominator=denominator,
+                              dimension=m, child_rank=r, row_factor=w_factor)
+    original = Count.literal(e)
+    before = bytes(original.tape.cells)
+    pool = ScratchPool(24)
+    candidate = None
+    try:
+        with no_decode(), sealed_constructors(), pool.install():
+            try:
+                candidate = (implementation or selector.select_body_stock)(
+                    original, q, profile, compatibility)
+                observed = {key: value if key == "fits" else observe(value)
+                            for key, value in candidate.items()}
+            finally:
+                if candidate is not None:
+                    selector.close_plan(candidate)
+            pool.empty()
+        require(bytes(original.tape.cells) == before and original.tape.head == 1,
+                "borrowed original restored")
+        expected = specification(*args)
+        require(expected == slab_specification(*args), "independent inverse-depth agreement")
+        require(canonical(observed) == canonical(expected), "literal Count plan equals independent specification")
+        guard = padded_guards(observed, q, m, w_factor, compatibility) if observed["fits"] else None
+        return dict(args=list(args), plan=observed, guards=guard, peak_roles=pool.peak,
+                    tape_steps=sum(t.meter.reads + t.meter.writes + t.meter.moves for t in pool.tapes))
+    finally:
+        original.close()
+
+
+def cases():
+    # Complete reduced strict-fit/depth-jump range, then changed width, rank,
+    # radix, compatibility and live-family factors. No random nomination.
+    result = [(e, 2, 2, 1, 1, 1, 0, 1) for e in range(1, 81)]
+    for q, m, r, factor, compatibility, a, b in (
+            (2, 2, 1, 1, 2, 0, 1), (3, 2, 1, 2, 5, 0, 1),
+            (2, 3, 2, 1, 1, 0, 1), (3, 3, 1, 1, 2, 1, 3),
+            (2, 2, 1, 1, 1, 1, 3), (2, 2, 1, 1, 9475, 0, 1),
+            (2, 2, 1, 1, 1, 1, 1)):
+        for e in (1, 2, 8, 9, 12, 13, 24, 32, 61, 64, 65, 80, 127):
+            result.append((e, q, m, r, factor, compatibility, a, b))
+    return list(dict.fromkeys(result))
+
+
+def source_boundary():
+    tree = ast.parse((HERE / "selector.py").read_text())
+    forbidden = {"cells", "physical", "head", "inspect", "inspect_count", "bit_length"}
+    bad = [node.attr for node in ast.walk(tree)
+           if isinstance(node, ast.Attribute) and node.attr in forbidden]
+    require(not bad, "selector has no host tape observation")
+    return "source inspection: no cells/head/physical/inspect/bit_length access; literal runtime also seals constructors and Word.inspect"
+
+
+def controls():
+    import encoded
+    import selector
+    from cardinal_counts import Count
+    from check_support import no_decode
+    from scratch_pool import ScratchPool
+    from session import sealed_constructors
+    rejected = []
+    base = encoded.Profile(numerator=0, denominator=1, dimension=2, child_rank=1, row_factor=1)
+    invalid = [(True, base, 1), (1, base, 1), (2, base, 0),
+               (2, encoded.Profile(dimension=2, child_rank=2), 1),
+               (2, encoded.Profile(numerator=2, denominator=1), 1)]
+    for index, (q, profile, compatibility) in enumerate(invalid):
+        original, pool = Count.literal(13), ScratchPool(24)
+        try:
+            with no_decode(), sealed_constructors(), pool.install():
+                try:
+                    selector.select_body_stock(original, q, profile, compatibility)
+                except ValueError:
+                    rejected.append("compiled-contract-" + str(index))
+                else:
+                    raise ValueError("invalid compiled contract accepted")
+                pool.empty()
+        finally:
+            original.close()
+    original, pool = Count.literal(0), ScratchPool(24)
+    try:
+        with no_decode(), sealed_constructors(), pool.install():
+            try:
+                selector.select_body_stock(original, 2, base, 1)
+            except ValueError:
+                rejected.append("zero-original")
+            else:
+                raise ValueError("zero original accepted")
+            pool.empty()
+    finally:
+        original.close()
+
+    # A semantic failure after all trial fields exist must unwind both scopes.
+    original, pool = Count.literal(24), ScratchPool(24)
+    snapshot = bytes(original.tape.cells)
+    saved = selector._fits
+    def injected(_trial):
+        raise ValueError("injected completed-trial failure")
+    selector._fits = injected
+    try:
+        with no_decode(), sealed_constructors(), pool.install():
+            try:
+                selector.select_body_stock(original, 2, base, 1)
+            except ValueError as error:
+                require(str(error) == "injected completed-trial failure", "failure reached trial boundary")
+            else:
+                raise ValueError("injected semantic failure accepted")
+            pool.empty()
+        require(bytes(original.tape.cells) == snapshot and original.tape.head == 1,
+                "semantic failure preserves borrowed input")
+        rejected.append("completed-trial-failure-cleanup")
+    finally:
+        selector._fits = saved
+        original.close()
+
+    text = (HERE / "selector.py").read_text()
+    mutations = (
+        ("old-original-depth", 'Count(body)', 'Count(original)', (13, 2, 2, 1, 1, 1, 0, 1)),
+        ("missing-Q", 'stock.multiply_small(compatibility)', 'pass',
+         (32, 2, 2, 1, 1, 5, 0, 1)),
+        ("nonstrict-fit", 'strict.divide_small(2)', 'strict.increment(); strict.divide_small(2)',
+         (12, 2, 2, 1, 1, 1, 0, 1)),
+        ("wrong-radix-exponent", '_power(radix, borrowed)', '_power(radix, depth)',
+         (13, 2, 2, 1, 1, 1, 0, 1)),
+        ("false-final-endpoint", '_plan(work, trial, "upper")', '_plan(work, trial, "lower")',
+         (24, 2, 2, 1, 1, 1, 0, 1)),
+    )
+    for name, old, new, args in mutations:
+        require(text.count(old) == 1, "unique executed mutation target: " + name)
+        module = ModuleType("mutant_" + name.replace("-", "_"))
+        exec(compile(text.replace(old, new), name, "exec"), module.__dict__)
+        try:
+            run_case(args, module.select_body_stock)
+        except ValueError as error:
+            require(str(error) == "literal Count plan equals independent specification", "mutation reached oracle: " + name)
+            rejected.append(name)
+        else:
+            raise ValueError("algorithm mutation accepted: " + name)
+    return rejected
+
+
+def replay():
+    inputs = authenticate()
+    with activate():
+        from independent import check
+        boundary = source_boundary()
+        records = [run_case(args) for args in cases()]
+        failures = controls()
+        arithmetic = check()
+    witnesses = [row for row in records if row["args"] in (
+        [12, 2, 2, 1, 1, 1, 0, 1], [13, 2, 2, 1, 1, 1, 0, 1],
+        [24, 2, 2, 1, 1, 1, 0, 1], [61, 2, 2, 1, 1, 1, 1, 3])]
+    return dict(source_inputs=inputs, encoded_cases=len(records),
+                fitted=sum(row["plan"]["fits"] for row in records),
+                peak_setup_roles=max(row["peak_roles"] for row in records),
+                records_sha256=sha256(canonical(records).encode()).hexdigest(),
+                independent=arithmetic, rejection_controls=failures,
+                runtime_boundary=boundary, witnesses=witnesses)
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument("--emit", action="store_true")
+    args = parser.parse_args()
+    result = replay()
+    if args.emit:
+        print(json.dumps(result, indent=2, sort_keys=True))
+    else:
+        require(canonical(result) == canonical(json.loads((HERE / "RESULT.json").read_text())),
+                "complete typed retained result")
+        print("PASS_ENCODED_BODY_DEPTH", sha256(canonical(result).encode()).hexdigest())
+
+
+if __name__ == "__main__":
+    main()