diff --git a/research/complex-stopped-recursion-cost/PROOF.md b/research/complex-stopped-recursion-cost/PROOF.md
new file mode 100644
index 0000000000..a6162a3a56
--- /dev/null
+++ b/research/complex-stopped-recursion-cost/PROOF.md
@@ -0,0 +1,146 @@
+# The stopped complex recursion bill of #4100 COMPLEX.md
+
+JoyboyBrian, with substantial assistance from Anthropic Claude (Claude Code).
+Apache-2.0. This is an author-submitted scoped proof, not an accepted theorem.
+
+## Object and caller
+
+Cinna Davis's #4100 `research/unconditional-batched-crt/COMPLEX.md` (retained
+head `337d04939571a637aeab54a0f58f54fde811663a`, pinned here at canonical main
+`cef4b52f2a59009865bf8eabde1be3f159063703`), section "Time", states:
+
+> Stop at width max(73,h^eta). At each internal node, all adapters, monomials,
+> packet scans and parking cost O(V e^(1-a2) polylog(p)) [...] Hence the
+> complete layer costs O(V h^(1-q) polylog(p)).
+
+Its constants are the PR4088 mixed histogram
+`H = {1:8060060, 2:2310120, 3:751813, 4:327210, 5:66425, 8:25920, 48:138492}`,
+`W = 322560`, `b = .001730979115670792472760579929302792893760378764`,
+`q = b - 10^-28`, `a_eff = (b+q)/2`, `tau = 1 - a_eff`, `eta = 10^-32`, and
+`a2 = .001733394791695384296` from PROOF.md. Write
+
+    mu_x = sum_r (H_r / W) (r/73)^x.
+
+The callers are PROOF.md's synthetic-transform layers (`h` = active axis bits at
+one FFT level, `1 <= h <= d-1`, at most `ell` levels per transform) and
+GAUSSIAN.md's compiled layers (`h = O(p^beta)` or `O(p^epsilon)`).
+
+## Premises kept explicit
+
+These are COMPLEX.md's own premises. This package does not verify them.
+`Lambda = Lambda(p) >= 1` is the polylog factor, uniform in `e`, `v` and `h`;
+`c_N`, `c_L`, `c_P` are fixed constants. Fix the root width `h >= 1` and the
+stop width `s = max(73, h^eta)`; every descendant uses the root's `s`.
+
+- **(N) internal node.** A call of width `e > s` on volume `v` puts
+  `f = floor(e/73)` and performs only: (i) its own adapters, monomials, packet
+  scans and parking, at cost at most `c_N Lambda v e^(1-a2)`; (ii) the
+  `e - 73f <= 72` remainder bits by elementary passes, at most `c_L v` each;
+  (iii) for each rank `r`, children of width `r f` whose total volume is
+  `(H_r/W) v`. This is COMPLEX.md's one-child reading of a rank-`r` transition;
+  #4375 shows that the factorwise reading (`f` scalar copies) breaks the moment.
+- **(L) leaf.** A call with `e <= s` costs at most `c_L v e`.
+- **(P) root placement.** Placement and inverse cost at most
+  `c_P Lambda V (h^(1-a2) + 1)`.
+- **(A) additivity.** Costs of the listed parts add, and every child obeys
+  (N), (L) with the same constants.
+
+## Exact and certified facts
+
+1. `a_eff < a2`, `q < a_eff`, `q > 0` and `eta*b < b - q` hold exactly over the
+   rationals. Hence `1-a2 < tau < 1-q` and `1 - b + eta*b < 1 - q`.
+2. `a_eff < 1/200` and `74^199 >= 72^200`, so `e^tau >= 74^(199/200) >= 72`
+   for every integer `e >= 74`.
+3. Certified outward-rounded rational enclosures give
+   `1 - mu_(1-b) = 1.804257...e-48 > 0` and
+   `1 - mu_tau = 1.417734591407...e-28 > 0`, so
+   `1/(1 - mu_tau)` lies in `(7.0535e27, 7.0536e27)`.
+
+`verify.py` checks all three with the standard library.
+
+## Lemma (all root widths)
+
+Under (N), (L), (A), every call of width `e >= 1` on volume `v` costs at most
+
+    v [ K1 e^tau + c_L s^b e^(1-b) ],     K1 = (c_N Lambda + c_L) / (1 - mu_tau).
+
+*Proof.* Strong induction on `e`. The recursion is well founded: an internal
+width satisfies `e >= 74`, so `f >= 1`, and every child width satisfies
+`1 <= r f <= 48 e / 73 < e`.
+
+*Leaf* (`e <= s`): `c_L v e = c_L v e^(1-b) e^b <= c_L v s^b e^(1-b)`.
+
+*Internal* (`e > s >= 73`): parts (i) and (ii) cost at most
+`c_N Lambda v e^(1-a2) + 72 c_L v`. Since `e >= 1` and `1-a2 < tau`,
+`e^(1-a2) <= e^tau`; by fact 2, `72 <= e^tau`. So (i)+(ii) cost at most
+`(c_N Lambda + c_L) v e^tau`. For (iii), `73 f <= e` and the exponents are
+positive, so `(r f)^x <= (r/73)^x e^x` for `x = tau, 1-b`. The induction
+hypothesis, applied to each child and summed by (A), bounds (iii) by
+
+    v [ K1 mu_tau e^tau + c_L s^b mu_(1-b) e^(1-b) ]
+      <= v [ K1 mu_tau e^tau + c_L s^b e^(1-b) ],
+
+using `mu_(1-b) <= 1` (fact 3). Adding, the coefficient of `v e^tau` is
+`c_N Lambda + c_L + K1 mu_tau = K1`. This closes the induction. QED.
+
+No monotonicity of the cost in `e` is used, and floors enter only through
+`73 floor(e/73) <= e`.
+
+## Theorem (COMPLEX.md's layer bill)
+
+Under (N), (L), (P), (A), for every `h >= 1` the complete layer of volume `V`
+costs at most
+
+    V Lambda h^(1-q) [ (c_N + c_L)/(1 - mu_tau) + 73^b c_L + 2 c_P ].
+
+*Proof.* Apply the lemma at `e = h`, `v = V`, and add (P). Since `h >= 1`,
+`s^b = max(73^b, h^(eta b)) <= 73^b h^(eta b)`. The four exponents `tau`,
+`1-b+eta*b`, `1-a2` and `0` are all at most `1-q` (fact 1), so each power of
+`h` is at most `h^(1-q)`. Finally use `Lambda >= 1`. QED.
+
+The constant is independent of `h`, `p` and the coefficient values. It is
+effective but large, since `1/(1-mu_tau) > 7.05e27`.
+
+## Binding to the callers
+
+- **PROOF.md synthetic transforms.** One FFT level is one layer with
+  `1 <= h <= d-1`; there are at most `ell` levels. Since `h^(1-q)` increases
+  with `h`, levels with fewer active axes are covered. One transform costs at
+  most `ell V Lambda K d^(1-q)`, which is PROOF.md's
+  `O(V ell d^(1-q) polylog(p))`.
+- **GAUSSIAN.md compiled layers.** `h = O(p^beta)` or `O(p^epsilon)` gives
+  `O(V h^(1-q) polylog(p))` with the same constant.
+
+## What the argument does and does not use
+
+- `mu_(1-b) <= 1` suffices for the leaf term. Strictness is not needed. Its
+  certified margin is only `1.8e-48`, and one extra rank-48 child per `W`
+  makes `mu_(1-b) > 1` (control).
+- The stop width enters only through `s >= 73`. The lemma holds for every
+  fixed `s >= 73`. The `h^eta` stop costs the factor `h^(eta b)` and is not
+  needed for this bill. It may serve other premises, such as control
+  payloads; this package does not decide that.
+- The floor is necessary. With `r ceil(e/73)` instead, a width-74 node has a
+  rank-48 child of width 96, so the recursion is not well founded and the
+  comparison `(r f)^x <= (r/73)^x e^x` fails (control).
+- **Size of the constant.** The per-level contraction `1 - mu_tau` is only
+  `1.4e-28`, so the uniform constant exceeds `7e27 (c_N Lambda + c_L)`. On
+  complete finite trees with unit node costs, the internal `tau`-sum divided
+  by `h^tau` is at most 8.8 for `h <= 10^12`. It grows roughly like the
+  depth. The huge constant is therefore a worst-case geometric-series artifact
+  and not a defect.
+
+## Finite corroboration
+
+`verify.py` evaluates complete recursion trees with unit costs
+(`c_N = c_L = Lambda = 1`) at 60-digit Decimal precision. It covers every
+`h = 75, 112, ..., 1497`, plus `h` in
+`{74, 100, 146, 1000, 5329, 10^4, 389017, 10^6, 10^9, 10^12}`, with stop widths
+73, 500 and 5000. It checks three things:
+
+- the frontier sum `sum_leaves (v_l/V) e_l^(1-b)` is at most `h^(1-b)`;
+- the internal sum `sum_internal (v/V) e^tau` is at most `h^tau/(1-mu_tau)`;
+- the unit-cost total is below the lemma's bound.
+
+This is numerical corroboration. It does not certify anything and does not
+replace the proof.
diff --git a/research/complex-stopped-recursion-cost/README.md b/research/complex-stopped-recursion-cost/README.md
new file mode 100644
index 0000000000..b9672294f7
--- /dev/null
+++ b/research/complex-stopped-recursion-cost/README.md
@@ -0,0 +1,118 @@
+# COMPLEX.md's stopped complex recursion meets its layer bill
+
+**Scoped proof under COMPLEX.md's own node premises. No new κ.** This does not
+accept #4100, and it changes nothing in it or in the selected record.
+
+## Object and caller
+
+The object is Cinna Davis's #4100 [COMPLEX.md](../unconditional-batched-crt/COMPLEX.md),
+section "Time", at retained head `337d04939571a637aeab54a0f58f54fde811663a`
+(pinned at canonical main `cef4b52f2a59009865bf8eabde1be3f159063703`). It
+claims that the stopped complex recursion costs `O(V h^(1-q) polylog(p))`.
+The recursion has the PR4088 mixed histogram over `W = 322560`, children of
+width `r floor(e/73)`, and stop width `max(73, h^eta)`.
+
+The callers are PROOF.md's synthetic-transform layers (`1 <= h <= d-1`, at
+most `ell` levels) and GAUSSIAN.md's compiled layers (`h = O(p^beta)` or
+`O(p^epsilon)`). The [#4100 coverage map](../../docs/research/pr4100-audit-coverage-map.md)
+lists the stopped-moment proof outside #4178's caller as still open.
+
+## Result
+
+[PROOF.md](PROOF.md) proves the following by strong induction, for every root
+width `h >= 1`. It keeps COMPLEX.md's premises explicit: (N) node cost, the
+remainder bits and the child volumes; (L) leaves; (P) root placement;
+(A) additivity. The layer then costs at most
+
+    V Lambda h^(1-q) [ (c_N + c_L)/(1 - mu_tau) + 73^b c_L + 2 c_P ].
+
+Here `mu_x = sum_r (H_r/W)(r/73)^x`. The proof handles floors, the
+`e mod 73` remainder bits and every stop width `s >= 73` directly. It assumes
+no monotonicity in `e`. The certified facts are:
+
+| Fact | Value |
+| --- | --- |
+| `1 - mu_(1-b)` | `1.804257...e-48 > 0` (only `<= 1` is needed) |
+| `1 - mu_tau` | `1.417734591407...e-28 > 0` |
+| `1/(1 - mu_tau)` | in `(7.0535e27, 7.0536e27)` |
+| exponent order | `1-a2 < tau < 1-q`, `1-b+eta*b < 1-q`, `72 <= 74^tau` (exact) |
+
+**Callers.** For the synthetic transforms this gives PROOF.md's
+`O(V ell d^(1-q) polylog(p))`, including levels with fewer active axes. For the
+GAUSSIAN.md compiled layers it gives `O(V h^(1-q) polylog(p))`.
+
+**Notes.** None of these changes a downstream bound.
+
+- The leaf term needs only `mu_(1-b) <= 1`.
+- The `h^eta` stop is not used by this bill. Any fixed stop `s >= 73` works.
+- The floor is necessary. With a ceiling, a width-74 node has a width-96
+  child.
+- The uniform constant exceeds `7e27 (c_N Lambda + c_L)`. On finite trees
+  with unit costs, the internal `tau`-sum over `h^tau` is only 8.8 at
+  `h = 10^12`. The constant is a worst-case artifact, not a defect.
+
+## Not covered
+
+- Premise (N)(i): that the node's adapters, monomials, the `Gamma`-fold cover
+  gathers and parking cost `O(V e^(1-a2) polylog p)`.
+- Premise (N)(iii): that the actual packets realize total child volume
+  `(H_r/W) v` at width `r floor(e/73)`. #4375 shows that the factorwise
+  reading breaks the moment.
+- The free-word lift (#4184), the cover and stock arithmetic (#4424), the
+  height and precision chain (#4178, #4371, #4415), and all of CRT.md.
+
+## Reproduce
+
+From the repository root, with Python 3.12 (standard library only, about 7 s):
+
+```sh
+python3 scripts/research_package.py --package research/complex-stopped-recursion-cost --check-only
+python3.12 -B scripts/research_package.py --package research/complex-stopped-recursion-cost
+python3.12 -B research/complex-stopped-recursion-cost/verify.py
+```
+
+`verify.py` reads the constants from the pinned COMPLEX.md and PROOF.md. It
+checks the exact exponent order and the certified outward-rounded enclosures
+of `mu_tau` and `mu_(1-b)`. It runs three rejection controls:
+
+- a root above the bracket, `b + 1e-47`, gives `mu > 1`;
+- one extra rank-48 child per `W` breaks both moments;
+- the ceiling child rule grows width 74 to 96.
+
+It also corroborates numerically, at 60 digits, complete recursion trees for
+stop widths 73, 500 and 5000. That check is corroboration, not a certificate.
+It imports no code from #4100, #4171 or #4178.
+
+## Open next questions
+
+The structured versions are in [TASK.json](TASK.json).
+
+1. **Node-cost premise.** Do the adapters, the F2 row-addition monomials, the
+   `Gamma`-fold common-cover packet gathers and parking cost
+   `O(V e^(1-a2) polylog p)` at the actual node? First step: write a per-node
+   invoice from COMPLEX.md's "Common cover" section, PR2250 §5–6 and #4424's
+   row-stock layout.
+2. **Child volume premise.** Do the actual child packets realize
+   `Gamma H_r` rank-`r` calls of volume `V/(W Gamma)` each? First step: bind
+   PR4088's owner fill and the `W`-family split to per-child packet volumes on
+   one cover value.
+
+## Task and overlap
+
+- **Card:** `uniform-transfer-audit`, refined to one native/complex-family
+  implication.
+- **Claim:** https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19137702
+- **Overlap:** the nearest work is #4178 (height recurrence at the Gaussian
+  caller), #4171 and #4330 (root and ledger numbers), #4424 (cover and stock
+  arithmetic), and #4375 (frame-child reading). None writes this cost
+  induction.
+
+## Credit
+
+The construction and every audited statement are Cinna Davis's (#4100). The
+histogram and words are PR4088's. The ledger cross-check is Nick Petalas's
+(#4171), the height recurrence is Jose Manuel's (jmbarrancoml, #4178), the cover
+audit is Matarener's (#4424), the frame-child separation is unpaidmoon's (#4375),
+and the coverage map is Ryanson Jonathan's (pinterbanget, #4311). Prepared by JoyboyBrian with
+substantial assistance from Anthropic Claude (Claude Code). New work is
+Apache-2.0.
diff --git a/research/complex-stopped-recursion-cost/SOURCES.json b/research/complex-stopped-recursion-cost/SOURCES.json
new file mode 100644
index 0000000000..6866aff1af
--- /dev/null
+++ b/research/complex-stopped-recursion-cost/SOURCES.json
@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/unconditional-batched-crt/COMPLEX.md",
+      "usage": "input",
+      "git_blob": "c3be56fbfdb4fb29c1ace88cbcdfa7475fb6e343",
+      "sha256": "853e1295850862752e4f854aa9e8b28f9ca6eaa9306e2af110b7b77526d1b5e1"
+    },
+    {
+      "path": "research/unconditional-batched-crt/PROOF.md",
+      "usage": "input",
+      "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c",
+      "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060"
+    }
+  ]
+}
diff --git a/research/complex-stopped-recursion-cost/TASK.json b/research/complex-stopped-recursion-cost/TASK.json
new file mode 100644
index 0000000000..562c1a470f
--- /dev/null
+++ b/research/complex-stopped-recursion-cost/TASK.json
@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "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": "Prove, for every root width h>=1, that COMPLEX.md's stopped complex recursion (children r*floor(e/73) with the PR4088 mixed histogram over W=322560, stop width max(73,h^eta), node cost O(V e^(1-a2) polylog p), elementary remainders and leaves, root placement) costs at most V Lambda h^(1-q) [(c_N+c_L)/(1-mu_tau)+73^b c_L+2c_P], with certified mu_tau<1 and mu_(1-b)<=1, and bind it to PROOF.md's synthetic-transform layers and GAUSSIAN.md's compiled layers. The node-cost, child-volume and leaf premises stay explicit.",
+  "scope_change_reason": "The card asks for one quantified #4100 implication at its actual caller. This package takes the native/complex-family obligation that docs/research/pr4100-audit-coverage-map.md lists as open after #4178: COMPLEX.md's stopped-recursion time bill, at the PR4088 mixed histogram and the PROOF.md and GAUSSIAN.md layer callers. It avoids CRT.md and the precision chain (#4371, #4415, #4178).",
+  "bottleneck_link": "Side result for the #4100 audit: it closes one transfer implication, the stopped complex moment, under COMPLEX.md's own node premises. It does not change any kappa or the selected frontier.",
+  "budget_minutes": 150,
+  "stop_rule": "Stop after the all-size lemma and theorem, the certified moment enclosures, three rejection controls and bounded tree corroboration. Do not audit the node-cost premise, the free-word lift, CRT.md or the precision chain.",
+  "outcome": "completed",
+  "evidence": "PROOF.md: written strong induction over all widths, with floors, remainders and an arbitrary stop width s>=73. verify.py: exact exponent order, certified rational enclosures of mu_tau and mu_(1-b), rejection controls, and 60-digit numerical tree corroboration. The tree check is corroboration, not a certificate.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5)",
+  "open_questions": [
+    {
+      "question": "Is COMPLEX.md's node-cost premise true at the actual node: adapters, F2 row-addition monomials through the compact primitive, the Gamma-fold common-cover packet gathers and parking all cost O(V e^(1-a2) polylog p), uniformly in e?",
+      "why_it_matters": "The theorem here is conditional on it. Whether the per-cover-value gathers scan only the cover's own rows or the whole node volume changes only a constant, but a per-node term not bounded by V e^(1-a2) polylog p would break the bill.",
+      "first_step": "Write a per-node invoice from COMPLEX.md's 'Common cover, fresh rows and fixed tapes' section and PR2250 sections 5-6, with the row-field layout of #4424.",
+      "blocked_by": "A literal node-level tape layout for the Gamma cover field is not written in #4100."
+    },
+    {
+      "question": "Do the actual child packets realize the moment's volume normalization: Gamma*H_r rank-r child calls of volume V/(W Gamma) each, at width r*floor(e/73)?",
+      "why_it_matters": "mu_x uses H_r/W as the total child volume per unit parent volume. #4375 shows that the factorwise reading breaks the moment, so this premise carries the whole stopped bill.",
+      "first_step": "Bind PR4088's owner fill (3240*408 roles) and the W-family split to per-child packet volumes on one cover value.",
+      "blocked_by": "No external blocker."
+    }
+  ]
+}
diff --git a/research/complex-stopped-recursion-cost/VERIFY.json b/research/complex-stopped-recursion-cost/VERIFY.json
new file mode 100644
index 0000000000..b395afdfdf
--- /dev/null
+++ b/research/complex-stopped-recursion-cost/VERIFY.json
@@ -0,0 +1,31 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/COMPLEX.md",
+    "research/unconditional-batched-crt/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Bind the histogram, W, b, q, a_eff, eta, stop and child rules from COMPLEX.md and a2 from PROOF.md; exact exponent order 1-a2<tau<1-q, 1-b+eta*b<1-q and 72<=74^tau; certified outward-rounded enclosures 1-mu_(1-b)=1.804e-48>0 and 1-mu_tau=1.4177e-28>0 with 1/(1-mu_tau) in (7.0535e27,7.0536e27); controls: root b+1e-47 gives mu>1, one extra rank-48 child breaks both moments, ceiling child rule grows width 74 to 96; 60-digit numerical tree corroboration for stop widths 73, 500, 5000."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same checks with Python optimization enabled; no check relies on assert."
+    }
+  ]
+}
diff --git a/research/complex-stopped-recursion-cost/verify.py b/research/complex-stopped-recursion-cost/verify.py
new file mode 100644
index 0000000000..771fa158a9
--- /dev/null
+++ b/research/complex-stopped-recursion-cost/verify.py
@@ -0,0 +1,244 @@
+#!/usr/bin/env python3
+"""Verifier for the #4100 COMPLEX.md stopped-recursion cost audit.
+
+JoyboyBrian, with substantial assistance from Anthropic Claude (Claude Code).
+Apache-2.0. Python 3.12 standard library only.
+
+Checks, in order:
+  1. Source binding: the histogram, W, root b, q, a_eff, eta, stop rule and
+     child rule are read from the pinned COMPLEX.md; a2 from PROOF.md.
+  2. Exponent order used by PROOF.md section 1: 1-a2 < tau < 1-q and
+     1-b+eta*b < 1-q, exactly over the rationals.
+  3. Certified rational enclosures of mu_tau and mu_(1-b) (outward-rounded
+     atanh/exp series), giving mu_(1-b) < 1, mu_tau < 1 and an enclosure of
+     the uniform constant 1/(1-mu_tau).
+  4. Rejection controls: a root above the certified bracket, one extra
+     rank-48 child per W, and the ceiling child rule all fail.
+  5. Finite numerical corroboration (Decimal, 60 digits) of the two tree
+     sums that the written induction bounds, on complete recursion trees.
+The all-size statement is the written proof in PROOF.md; items 3-5 do not
+replace it.
+"""
+from decimal import Decimal, getcontext
+from fractions import Fraction as F
+from pathlib import Path
+import re
+import sys
+
+ROOT = Path(__file__).resolve().parents[2]
+SRC = ROOT / 'research' / 'unconditional-batched-crt'
+GRID = 10 ** 110
+
+
+def fail(message):
+    print('FAIL_COMPLEX_STOPPED_RECURSION_COST: ' + message)
+    sys.exit(1)
+
+
+def check(condition, message):
+    if not condition:
+        fail(message)
+
+
+def flat(path):
+    return ' '.join(path.read_text(encoding='utf-8').split())
+
+
+# ---------------------------------------------------------------- sources
+complex_md = flat(SRC / 'COMPLEX.md')
+proof_md = flat(SRC / 'PROOF.md')
+
+hist_match = re.search(r'exact paid histogram is \{([0-9:,]+)\}', complex_md)
+check(hist_match is not None, 'histogram sentence not found in COMPLEX.md')
+HIST = {int(k): int(v) for k, v in (item.split(':') for item in hist_match.group(1).split(','))}
+check(HIST == {1: 8060060, 2: 2310120, 3: 751813, 4: 327210, 5: 66425, 8: 25920, 48: 138492},
+      'unexpected histogram')
+w_match = re.search(r'Set W=(\d+) and', complex_md)
+check(w_match is not None, 'W not found')
+W = int(w_match.group(1))
+check(W == 322560, 'unexpected W')
+b_match = re.search(r'Let b=\.(\d+);', complex_md)
+check(b_match is not None, 'root b not found')
+B_ROOT = F(int(b_match.group(1)), 10 ** len(b_match.group(1)))
+a2_match = re.search(r'a2=\.(\d+)\.', proof_md)
+check(a2_match is not None, 'a2 not found in PROOF.md')
+A2 = F(int(a2_match.group(1)), 10 ** len(a2_match.group(1)))
+for sentence in ('Put q=b-10^-28, a_eff=(b+q)/2, eta=10^-32 and tau=1-a_eff.',
+                 'Stop at width max(73,h^eta).',
+                 'Every child r floor(e/73), r<=48, decreases D',
+                 'all adapters, monomials, packet scans and parking cost O(V e^(1-a2) polylog(p))',
+                 'O(V h^(1-q) polylog(p))',
+                 'The placement and its inverse cost O(V h^(1-a2) polylog(p)+V polylog(p)).'):
+    check(sentence in complex_md, 'COMPLEX.md sentence missing: ' + sentence)
+check('Each transform costs O(V ell d^(1-q) polylog(p)).' in proof_md, 'PROOF.md caller sentence missing')
+
+Q = B_ROOT - F(1, 10 ** 28)
+A_EFF = (B_ROOT + Q) / 2
+ETA = F(1, 10 ** 32)
+TAU = 1 - A_EFF
+
+# ------------------------------------------------------- exponent order
+check(A_EFF < A2, 'need a_eff < a2, so that e^(1-a2) <= e^tau')
+check(Q < A_EFF, 'need q < a_eff, so that tau < 1-q')
+check(ETA * B_ROOT < B_ROOT - Q, 'need 1-b+eta*b < 1-q')
+check(0 < Q, 'need q > 0')
+# remainder absorption: 72 <= 74^tau, via a_eff < 1/200 and 74^199 >= 72^200
+check(A_EFF < F(1, 200) and 74 ** 199 >= 72 ** 200, 'need 72 <= e^tau for every internal width e >= 74')
+
+
+# ---------------------------------------------- certified enclosures
+def down(x):
+    return F((x.numerator * GRID) // x.denominator, GRID)
+
+
+def up(x):
+    return F(-((-x.numerator * GRID) // x.denominator), GRID)
+
+
+def atanh_inv(m):
+    """Enclosure of atanh(1/m) for an integer m >= 3."""
+    lo = hi = F(0)
+    power, k = F(1, m), 0        # power = m^-(2k+1), exact (denominator is a power of m)
+    while power > F(10 ** 10, GRID):
+        lo += down(power / (2 * k + 1))
+        hi += up(power / (2 * k + 1))
+        power /= m * m
+        k += 1
+    return lo, up(hi + power / ((2 * k + 1) * (1 - F(1, m * m))))
+
+
+def iadd(x, y):
+    return (x[0] + y[0], x[1] + y[1])
+
+
+def iscale(c, x):
+    return (c * x[0], c * x[1]) if c >= 0 else (c * x[1], c * x[0])
+
+
+def two_atanh(m):
+    return iscale(2, atanh_inv(m))
+
+
+LN2 = two_atanh(3)            # ln 2
+LN32 = two_atanh(5)           # ln 3/2
+LN54 = two_atanh(9)           # ln 5/4
+LN7372 = two_atanh(145)       # ln 73/72
+LN3 = iadd(LN2, LN32)
+LN = {1: (F(0), F(0)), 2: LN2, 3: LN3, 4: iscale(2, LN2), 5: iadd(iscale(2, LN2), LN54),
+      8: iscale(3, LN2), 48: iadd(iscale(4, LN2), LN3)}
+LN73 = iadd(iadd(iscale(3, LN2), iscale(2, LN3)), LN7372)
+L73 = {r: (LN73[0] - LN[r][1], LN73[1] - LN[r][0]) for r in LN}   # ln(73/r) > 0
+
+
+def exp_bounds(y):
+    """Enclosure of exp(y) for 0 <= y <= 8 (positive Taylor terms)."""
+    lo = hi = F(0)
+    t_lo = t_hi = F(1)           # outward-rounded n-th Taylor terms y^n/n!
+    n = 0
+    while t_hi > F(10 ** 10, GRID) or n < 2 * int(y) + 4:
+        lo += t_lo
+        hi += t_hi
+        n += 1
+        t_lo, t_hi = down(t_lo * y / n), up(t_hi * y / n)
+    # remaining tail <= t_hi / (1 - y/(n+1)) once n+1 > 2y
+    return lo, up(hi + t_hi / (1 - y / (n + 1)))
+
+
+def power_ratio(r, x):
+    """Enclosure of (r/73)^x = exp(-x ln(73/r)) for rational x > 0."""
+    if r == 73:
+        return F(1), F(1)
+    lo_y, hi_y = x * L73[r][0], x * L73[r][1]
+    return down(1 / exp_bounds(up(hi_y))[1]), up(1 / exp_bounds(down(lo_y))[0])
+
+
+def mu(x, hist=None):
+    hist = HIST if hist is None else hist
+    lo, hi = F(0), F(0)
+    for r, count in hist.items():
+        p_lo, p_hi = power_ratio(r, x)
+        lo += F(count, W) * p_lo
+        hi += F(count, W) * p_hi
+    return lo, hi
+
+
+MU_EDGE = mu(1 - B_ROOT)
+check(MU_EDGE[1] < 1, 'mu_(1-b) < 1 not certified')
+MU_TAU = mu(TAU)
+check(MU_TAU[1] < 1, 'mu_tau < 1 not certified')
+GAP = (1 - MU_TAU[1], 1 - MU_TAU[0])
+check(GAP[1] - GAP[0] < GAP[0] / 10 ** 12, 'enclosure of 1-mu_tau is not sharp enough')
+K_LO, K_HI = 1 / GAP[1], 1 / GAP[0]
+K_WINDOW = (F(70535 * 10 ** 23), F(70536 * 10 ** 23))   # PROOF.md fact 3
+check(K_WINDOW[0] < K_LO and K_HI < K_WINDOW[1], '1/(1-mu_tau) outside the stated window')
+
+# ------------------------------------------------------- controls
+BAD_ROOT = B_ROOT + F(1, 10 ** 47)
+check(mu(1 - BAD_ROOT)[0] > 1, 'control: a root above the bracket should make mu_(1-b) > 1')
+extra = dict(HIST)
+extra[48] += 1
+check(mu(TAU, extra)[0] > 1, 'control: one extra rank-48 child per W should break mu_tau < 1')
+check(mu(1 - B_ROOT, extra)[0] > 1, 'control: one extra rank-48 child per W should break mu_(1-b) <= 1')
+ceil_bad = [e for e in range(74, 2000) if 48 * (-(-e // 73)) >= e]
+check(ceil_bad and ceil_bad[0] == 74 and 48 * 2 == 96, 'control: ceiling child rule should grow width 74 to 96')
+check(all(48 * (e // 73) < e and e // 73 >= 1 for e in range(74, 200000)),
+      'floor child rule must shrink every internal width')
+
+# ------------------------------------- finite numerical corroboration
+getcontext().prec = 60
+D_TAU = Decimal(TAU.numerator) / Decimal(TAU.denominator)
+D_EDGE = 1 - Decimal(B_ROOT.numerator) / Decimal(B_ROOT.denominator)
+D_A2 = 1 - Decimal(A2.numerator) / Decimal(A2.denominator)
+WEIGHTS = [(r, Decimal(c) / Decimal(W)) for r, c in sorted(HIST.items())]
+
+
+def tree_sums(h, stop):
+    """Return (internal tau-sum, frontier (1-b)-sum, unit-cost total) per unit root volume.
+
+    Unit-cost model: internal node own cost e^(1-a2) + (e mod 73), leaf cost e.
+    """
+    memo = {}
+
+    def walk(e):
+        if e in memo:
+            return memo[e]
+        de = Decimal(e)
+        if e <= stop:
+            out = (Decimal(0), de ** D_EDGE, de)
+        else:
+            f = e // 73
+            internal, frontier, cost = de ** D_TAU, Decimal(0), de ** D_A2 + (e - 73 * f)
+            for r, weight in WEIGHTS:
+                ci, cf, cc = walk(r * f)
+                internal += weight * ci
+                frontier += weight * cf
+                cost += weight * cc
+            out = (internal, frontier, cost)
+        memo[e] = out
+        return out
+
+    return walk(h)
+
+
+SAMPLES = [74, 100, 146, 1000, 5329, 10 ** 4, 389017, 10 ** 6, 10 ** 9, 10 ** 12]
+rows = []
+for stop in (73, 500, 5000):
+    for h in (SAMPLES if stop == 73 else SAMPLES[:8]) + list(range(75, 1500, 37)):
+        internal, frontier, cost = tree_sums(h, stop)
+        dh = Decimal(h)
+        check(frontier <= dh ** D_EDGE * (1 + Decimal(10) ** -40), 'frontier (1-b)-sum exceeds h^(1-b)')
+        k1 = Decimal(K_HI.numerator) / Decimal(K_HI.denominator)
+        bound = 2 * k1 * dh ** D_TAU + dh ** D_EDGE * Decimal(max(stop, 1)) ** (1 - D_EDGE)
+        check(cost <= bound, 'unit-cost total exceeds the written bound')
+        check(internal <= k1 * dh ** D_TAU, 'internal tau-sum exceeds h^tau/(1-mu_tau)')
+        if stop == 73 and h in SAMPLES and h not in [row[0] for row in rows]:
+            rows.append((h, float(internal / dh ** D_TAU), float(frontier / dh ** D_EDGE),
+                         float(cost / dh ** (1 - Decimal(Q.numerator) / Decimal(Q.denominator)))))
+
+print('mu_(1-b) in [1-%.6e, 1-%.6e]' % (float(1 - MU_EDGE[0]), float(1 - MU_EDGE[1])))
+print('1-mu_tau in [%.12e, %.12e]; 1/(1-mu_tau) in [%.6e, %.6e]'
+      % (float(GAP[0]), float(GAP[1]), float(K_LO), float(K_HI)))
+print('h, internal/h^tau, frontier/h^(1-b), unit cost/h^(1-q) at stop 73:')
+for row in rows:
+    print('  %-26d %10.4f %10.6f %10.4f' % row)
+print('PASS_COMPLEX_STOPPED_RECURSION_COST')