diff --git a/research/crt-uniform-evaluator/PROOF.md b/research/crt-uniform-evaluator/PROOF.md
new file mode 100644
index 000000000..7175c780b
--- /dev/null
+++ b/research/crt-uniform-evaluator/PROOF.md
@@ -0,0 +1,197 @@
+# Explicit constant for the uniform CRT evaluator
+
+This is a counting proof for one proposition in Cinna Davis's PR #4100,
+`CRT.md` §2 and the amortization display in §4. It is not an acceptance of
+that construction, and it does not change κ.
+
+## Proposition
+
+For every integer `p >= 2` and `ell >= 1`, there is a sequential evaluator
+that, from a CRT group of total bit length `W <= p` and a batch of at most
+`A <= 8(p+2)` target axes, returns the forward and inverse rotation-switch
+tables used by `CRT.md` and restores its work tapes, in at most
+
+```text
+E(p, ell) = 2^{4 ell} (p+2)^{16}
+```
+
+bit-steps. Thus the constant in the displayed bound
+
+```text
+E(p, ell) <= C 2^{4 ell} (p+2)^{16}
+```
+
+may be taken to be `C = 1` on this domain. The same bound implies the §4
+comparison
+
+```text
+2^{-G} E(p, ell) <= 2^{-60 ell} (p+2)^{-48}
+```
+
+with `G = 64 (ell + ceil(log2(p+2)))`, again with constant 1.
+
+The caller sizes in `research/unconditional-batched-crt/PROOF.md` meet
+`W <= p`. For `n < 4` that file uses elementary multiplication and does not
+call this evaluator. For `n >= 4`, `b = ceil(log2 n) >= 2` and the nominal
+parameter is `p = 6b`. The dyadic length `T` is a power of two in
+`[4n/b, 8n/b)`, so
+
+```text
+log2 T < log2(8n/b) = 3 + log2 n - log2 b <= b + 3 - log2 b.
+```
+
+For `b >= 2`, `log2 b >= 1`, hence `log2 T <= b + 1 <= p`. The split of
+`log2 T` is the sum of the axis widths, and every CRT group is a subset, so
+`W <= p`. The batch cap `A <= 8(p+2)` is the explicit reading of `CRT.md`'s
+"at most O(p) axis controls" used here. It is not a claim that every hidden
+factor inside an `O(p)` in that file has been extracted.
+
+## Bit-step model
+
+A bit-step is one head move, one bit read, one bit write, or one binary
+Boolean operation. Three tapes are used: input, work, and output. An indexed
+read of a table is a full sequential scan of that table and a return to its
+marker. No tape is allocated per recursion depth, axis, or input length.
+
+Schoolbook multiplication of an `a`-bit integer by a `b`-bit integer, for
+`a, b >= 1`, costs at most `8ab` bit-steps: each of the `a` rows ANDs `b`
+bits and adds them into a window of `b + 1` bits at 2 steps per bit, then
+the `a + b` product bits are written. That is `3ab + 3a + b`. For `a = 1`
+this is at most `5b`; for `b = 1` it is at most `5a`; for `a, b >= 2`,
+`3a + b <= 4ab`. In every case the total is at most `8ab`.
+
+Restoring division with quotient length `a` and divisor length `b` costs at
+most `8ab` bit-steps. Each of the `a` quotient bits subtracts and shifts a
+window of `b + 1` bits, at `3(b + 1)` steps, and the quotient is written:
+`3ab + 4a <= 8ab` because `4a <= 5ab` for `b >= 1`.
+
+A positive Euclidean algorithm halves the remainder at least every two
+steps: `r_i = q r_{i+1} + r_{i+2}` with `q >= 1` and `r_{i+1} > r_{i+2}`,
+so `r_i > 2 r_{i+2}`. A `b`-bit modulus therefore produces at most `2b`
+divisions. Each division and the two coefficient products cost at most
+`32 b^2` bit-steps, because `8b^2 + 16b^2 + 4b <= 32b^2` for `b >= 1`.
+The modular inverse therefore costs at most `64 b^3` bit-steps.
+
+## What one axis evaluates
+
+Fix a left group of `m <= 8(p+2)` moduli whose bit lengths sum to
+`W <= 8(p+2)`, and one target modulus of bit length at most `ell`. The
+offset is the one computed by the retained `balanced` step: reconstruct the
+left integer with `decode_group`, then multiply by the inverse of the
+growing right-child prefix modulo the target. One axis is charged for the
+whole reconstruction, whether or not several targets share it.
+
+That procedure uses at most `8m` multiplications of `W`-bit words, `4m`
+divisions of a `2W`-bit dividend by a `W`-bit divisor, `2m` inverses of
+`ell`-bit moduli, and `4m` additions of `W`-bit words at `4W` steps each.
+The resulting per-axis CRT bill is at most
+
+```text
+64 m W^2 + 64 m W^2 + 128 m ell^3 + 16 m W
+  = 128 m W^2 + 128 m ell^3 + 16 m W.
+```
+
+Substitute `m <= 8q` and `W <= 8q` with `q = p + 2`:
+
+```text
+65536 q^3 + 1024 q ell^3 + 1024 q^2.
+```
+
+Across `A <= 8q` axes this is `524288 q^4 + 8192 q^2 ell^3 + 8192 q^3`.
+
+Four networks are built from that offset and its negative: the forward
+rotation, the inverse rotation, and the same pair for the inverse macro.
+`CRT.md` describes a fixed number of forward and inverse gadget operations;
+four is the number priced here.
+
+For a network on `N = 2^h` wires, `1 <= h <= ell`:
+
+- Writing the rotation table costs at most `9(ell + 2)^2` bit-steps per
+  wire, hence at most `9(ell + 2)^2 2^ell` altogether. Each wire is one
+  addition and one restoring division of integers of at most `ell + 2` bits.
+- The Beneš tables are produced by the scan recurrence below, at most
+  `64 ell 2^{2 ell}` bit-steps.
+- The output is at most `2 ell` layers of `N` bits. Scanning it once and
+  returning the head costs at most `8 ell 2^ell` bit-steps.
+
+Per network this is at most `25(ell + 2)^2 2^ell + 64 ell 2^{2 ell}`.
+Four networks and `A <= 8q` axes contribute
+
+```text
+800 q (ell + 2)^2 2^ell + 2048 q ell 2^{2 ell}.
+```
+
+The input descriptor has at most `A W <= 64 q^2` bits and is scanned once,
+at `256 q^2` bit-steps. Adding the CRT bill for every axis gives the six
+quantities in `cost_terms` inside `verify.py`: setup `256 q^2`, CRT
+`524288 q^4` and `8192 q^3`, the inverse piece `8192 q^2 ell^3`, and the
+two network pieces.
+
+## Beneš scans
+
+At a dyadic node of size `n = 2^k`, `k >= 2`, the sequential procedure
+performs `7n + 1` full scans of `n` records of `k` bits: `n` scans to build
+the inverse, `4n` scans for the two neighbor lookups at every node, `2n`
+scans for the stack push and pop, and one scan to emit the child
+permutations. A scan of `n` records of `k` bits costs `4nk` bit-steps, so
+the local bill is `(7n + 1) 4 n k <= 32 k n^2`. The two children satisfy
+the inductive claim `T(n/2, k-1) <= 64 (k-1) (n/2)^2`, and
+
+```text
+2 T(n/2, k-1) + 32 k n^2 = 64 k n^2 - 32 n^2 <= 64 k n^2.
+```
+
+The `n = 2` node performs 13 scans and costs `104` bit-steps, at most
+`64 * 1 * 4 = 256`. Therefore `T(2^h, h) <= 64 h 2^{2h} <= 64 ell 2^{2 ell}`.
+The child permutations are the standard even-cycle coloring of the retained
+`benes` routine; the scans change the access mechanism, not the Boolean
+tables. `verify.py` checks those tables against
+`research/unconditional-batched-crt/check_batched_crt.py` on 90 rotation
+networks and checks that flipping one control bit changes the image.
+
+## Closing the inequality
+
+Let `B = 2^{4 ell} q^{16}` and let `q = p + 2 >= 4`. Every term has the
+shape `C(ell) q^a` with `a <= 4`. For an integer `q >= 5`,
+
+```text
+q^a / q^{16} < 4^a / 4^{16},
+```
+
+because `q^{12} > 4^{12}` and `x |-> x^{12}` is strictly increasing on the
+positive integers. The ratio of each term to `B` is therefore largest at
+`q = 4`.
+
+At `p = 2`, `ell = 1`, each of the six terms is at most `B/7`. Raising
+`ell` by one multiplies `B` by 16. It multiplies the quartic and cubic CRT
+terms by 1, the `ell^3` term by at most 8, the table term by at most
+`32/9`, and the network term by at most 8. Each of those factors is at most
+16, so `7 * term <= B` is preserved for every `ell >= 1`. The sum of six
+terms each at most `B/7` is at most `B`.
+
+## The guard amortization
+
+The bound just proved says `E <= 2^{4 ell} (p+2)^{16}`. With
+`G = 64 (ell + ceil(log2(p+2)))`,
+
+```text
+G - 60 ell = 4 ell + 64 ceil(log2(p+2)).
+```
+
+So `E (p+2)^{48} <= 2^{G - 60 ell}` follows from
+`(p+2)^{64} <= 2^{64 ceil(log2(p+2))}`, which is
+`p + 2 <= 2^{ceil(log2(p+2))}`. This is exactly the displayed comparison
+`2^{-G} E <= 2^{-60 ell} (p+2)^{-48}`. It prices only that comparison. It
+does not prove reservoir placement, the ordinary interchange callee, or the
+sparse repair program.
+
+## What was executed
+
+`verify.py` checks the integer comparisons in this argument, the scan
+recurrence, the schoolbook and division tariffs through bit lengths 16 and
+12, the Euclidean halving identity on the Fibonacci worst cases, 90
+agreements with the retained compiler, 44 CRT offset or direct-endpoint
+fixtures, rejection of a non-invertible prefix and of a non-permutation,
+and a direct grid `p = 2..30`, `ell = 1..12`. The executed compiler uses
+ordinary arrays. The bit-step count is the counting argument above, not a
+trace of a finite-state tape simulator.
diff --git a/research/crt-uniform-evaluator/README.md b/research/crt-uniform-evaluator/README.md
new file mode 100644
index 000000000..5b28a48bd
--- /dev/null
+++ b/research/crt-uniform-evaluator/README.md
@@ -0,0 +1,85 @@
+# Uniform CRT evaluator bound, with constant 1
+
+**Scoped counting proof. No new κ.** The selected conditional exponent is
+unchanged.
+
+## Scope and evidence
+
+Original card: `uniform-transfer-audit`, refined to one proposition. Cinna
+Davis's PR #4100 states
+
+```text
+E(p, ell) <= C 2^{4 ell} (p+2)^{16}
+```
+
+for the sequential Beneš and CRT control evaluator, and then uses
+
+```text
+2^{-G} E(p, ell) <= C 2^{-60 ell} (p+2)^{-48}.
+```
+
+The October 21 coverage map of #4100 still lists the full uniform `E(p, ell)`
+evaluator, starting from CRT data rather than from an encoded permutation, as
+unaudited. PR #4192 prices the Beneš component once a permutation is already
+encoded. This package prices the missing reconstruction and the four rotation
+networks together, and names the constant.
+
+For every integer `p >= 2` and `ell >= 1`, and for every CRT group whose bit
+length is at most `p` and every batch of at most `8(p+2)` axes, the procedure
+in [PROOF.md](PROOF.md) uses at most `2^{4 ell} (p+2)^{16}` bit-steps. The
+constant may be `C = 1`. The same inequality is exactly the displayed guard
+amortization. The size paragraph of #4100's `PROOF.md` gives group bit length
+at most `p`; the factor 8 is this package's explicit batch cap, not a new
+parameter of that construction.
+
+The executed checker agrees with the retained `benes` compiler on 90 rotation
+networks, checks 44 CRT offset fixtures, and rejects a non-invertible prefix
+and a non-permutation. The bit-step count itself is the counting argument, not
+a finite-state tape trace. Reservoir placement, the ordinary interchange
+callee, sparse repair, native execution, and the outer multiplication theorem
+are not proved here.
+
+Nearest open work, and why this is different: PR #4192 prices the Beneš
+component after the permutation is encoded and leaves CRT reconstruction open.
+PR #4187 assumes the uniform evaluator and prices only the last-K branch.
+PR #4321 compares a guard-density window with the printed `2^{-G} E` display
+and does not derive `E`. PR #4174 prices reservoir placement, not this
+evaluator.
+
+Source commits, Git blobs and SHA256 pins are in [SOURCES.json](SOURCES.json).
+The selected record and catalogue are historical provenance.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 scripts/research_package.py --package research/crt-uniform-evaluator --check-only
+python3.12 -B research/crt-uniform-evaluator/verify.py
+```
+
+The verifier prints `PASS_CRT_UNIFORM_EVALUATOR`.
+
+## Open next questions
+
+1. Replay one root-axis query on a single arena, in the sense of PR #4192,
+   where every logical access scans the whole arena rather than one table.
+   That schedule is more specific than the per-table scans priced here. The
+   first step is to feed this package's CRT offset into that arena and compare
+   the touch count with `2^{4 ell} (p+2)^{16}`. It is blocked because #4192
+   starts from an encoded permutation and is not replayed here.
+2. Use `C = 1` inside the reservoir and ordinary-callee argument of `CRT.md`
+   §3–§4, including the finite range that falls back to elementary
+   multiplication. The first step is the `H >= G` comparison at the stated
+   `G`. It is blocked because placement geometry is a separate obligation
+   (PR #4174) and is not an input to this evaluator.
+
+## Credit
+
+Cinna Davis supplies the CRT construction, the `E(p, ell)` shape, and the
+retained `benes` routine in PR #4100. ToikY's PR #4192 is the predecessor
+Beneš-scan audit and states this full-evaluator follow-up; this package does
+not depend on its unmerged bound. The coverage map in PR #4311 records that
+the evaluator was still open. Prepared by unpaidmoon with substantial Cursor
+Grok assistance. Apache-2.0. No independent human review or proof-assistant
+acceptance is claimed.
diff --git a/research/crt-uniform-evaluator/SOURCES.json b/research/crt-uniform-evaluator/SOURCES.json
new file mode 100644
index 000000000..d171e8035
--- /dev/null
+++ b/research/crt-uniform-evaluator/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/unconditional-batched-crt/check_batched_crt.py",
+      "usage": "input",
+      "git_blob": "1cf78abccd5e06beecc3ed21ba55f7c03b65fdbc",
+      "sha256": "681e2e3d71fa74c8b9b326f3860104fd9d89590a222e26ae6ee718d1fd40ff2e"
+    },
+    {
+      "path": "research/unconditional-batched-crt/CRT.md",
+      "usage": "provenance",
+      "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6",
+      "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b"
+    },
+    {
+      "path": "research/unconditional-batched-crt/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c",
+      "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060"
+    }
+  ]
+}
diff --git a/research/crt-uniform-evaluator/TASK.json b/research/crt-uniform-evaluator/TASK.json
new file mode 100644
index 000000000..9abf68d85
--- /dev/null
+++ b/research/crt-uniform-evaluator/TASK.json
@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "Does CRT.md's uniform evaluator satisfy E(p, ell) <= 2^{4 ell} (p+2)^{16} for every integer p >= 2 and ell >= 1, when the CRT group has bit length at most p and the batch has at most 8(p+2) axes?",
+  "scope_change_reason": "The card asks for one quantified implication of #4100 at its caller. CRT total repair, the free-algebra lift, and the main conditioning arguments already have open audits. This package takes only the still-unaudited uniform E(p, ell) evaluator that starts from CRT data, including the displayed 2^{-G} comparison that uses that bound. It does not audit placement, repair, or the outer theorem.",
+  "bottleneck_link": "PR #4100 proposes a conditional exponent above the selected kappa. Its CRT route pays E(p, ell) inside the bad-address amortization. An explicit constant for that evaluator is one caller-bound obligation of the proposed transfer; it does not by itself select a new exponent.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the evaluator inequality and the displayed 2^{-G} corollary. Do not price reservoir placement, the ordinary callee, or claim a new kappa.",
+  "outcome": "completed",
+  "evidence": "PROOF.md derives C=1. verify.py checks the comparisons, the Bene\u0161 recurrence, 90 retained-compiler agreements, 44 CRT fixtures, and the rejection controls. It prints PASS_CRT_UNIFORM_EVALUATOR.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok, substantial assistance with the proof writeup and the verifier.",
+  "open_questions": [
+    {
+      "question": "Does one root-axis query still fit 2^{4 ell}(p+2)^{16} when every logical access scans a single shared arena, as in PR #4192, after the CRT offset is included?",
+      "why_it_matters": "The per-table scans priced here are a different schedule from that arena. A shared arena can add a logarithmic factor. The proposed exponent uses E only through an amortization that has slack, but the schedules should not be silently identified.",
+      "first_step": "Encode this package's offset as the permutation input of the PR #4192 arena and compare its touch count with 2^{4 ell}(p+2)^{16} for one root axis.",
+      "blocked_by": "PR #4192 starts from an encoded permutation and is not replayed here. This package does not execute that arena."
+    },
+    {
+      "question": "With C=1, do the reservoir placement and ordinary interchange callee of CRT.md \u00a73\u2013\u00a74 still fit their stated O(V) and O(V p^{1-a} ell^2 polylog p) bills, including the finite elementary fallback?",
+      "why_it_matters": "The evaluator constant is only one factor in the CRT route. Placement and the callee can reintroduce an E-sized term if H < G on the actual parameters.",
+      "first_step": "Check H >= G at G = 64(ell + ceil(log2(p+2))) on the size family in #4100's PROOF.md, and price one ordinary H-bit interchange.",
+      "blocked_by": "Placement geometry is PR #4174's obligation and is not an input to this evaluator."
+    }
+  ]
+}
diff --git a/research/crt-uniform-evaluator/VERIFY.json b/research/crt-uniform-evaluator/VERIFY.json
new file mode 100644
index 000000000..0fac3f74a
--- /dev/null
+++ b/research/crt-uniform-evaluator/VERIFY.json
@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/check_batched_crt.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Integer comparisons for C=1, Bene\u0161 scan recurrence, schoolbook and division tariffs, 90 retained rotation-compiler agreements, 44 CRT offset fixtures, and rejection of a non-invertible prefix and a non-permutation."
+    }
+  ]
+}
diff --git a/research/crt-uniform-evaluator/verify.py b/research/crt-uniform-evaluator/verify.py
new file mode 100644
index 000000000..2673b156e
--- /dev/null
+++ b/research/crt-uniform-evaluator/verify.py
@@ -0,0 +1,426 @@
+#!/usr/bin/env python3
+"""Exact check of the uniform CRT evaluator bound.
+
+The proof is PROOF.md. This program checks every integer comparison used
+there, the Beneš scan recurrence, schoolbook and division tariffs on their
+stated domains, agreement with the retained rotation compiler, and the
+negative controls. It does not claim a new kappa.
+"""
+
+import importlib.util
+import json
+from pathlib import Path
+
+
+ROOT = Path(__file__).resolve().parents[2]
+SOURCE = ROOT / "research" / "unconditional-batched-crt" / "check_batched_crt.py"
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def load_source():
+    spec = importlib.util.spec_from_file_location("retained_batched_crt", SOURCE)
+    module = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(module)
+    return module
+
+
+def bit_length(value):
+    need(value >= 0, "nonnegative bit length")
+    return value.bit_length() or 1
+
+
+def prove_schoolbook_tariff():
+    """3ab + 3a + b <= 8ab for all integers a, b >= 1."""
+    # a = 1: 3 + b <= 5b iff 3 <= 4b, true for b >= 1.
+    # b = 1: 3a + 1 <= 5a iff 1 <= 2a, true for a >= 1.
+    # a >= 2, b >= 2: 3a + b <= 3ab + ab = 4ab <= 5ab, so 3ab+3a+b <= 8ab.
+    need(3 <= 4 * 1, "schoolbook a=1 corner")
+    need(1 <= 2 * 1, "schoolbook b=1 corner")
+    for a, b in ((2, 2), (2, 3), (5, 2)):
+        need(3 * a + b <= 4 * a * b <= 5 * a * b, "schoolbook interior")
+    for a in range(1, 17):
+        for b in range(1, 17):
+            touches = schoolbook_touches(a, b)
+            need(touches <= 8 * a * b, "schoolbook execution " + str((a, b)))
+
+
+def schoolbook_touches(a, b):
+    """Bit-steps of the schoolbook product described in PROOF.md."""
+    touches = 0
+    for _i in range(a):
+        touches += b  # AND the addend
+        touches += 2 * (b + 1)  # add into a (b+1)-bit window
+    touches += a + b  # write the product
+    return touches
+
+
+def prove_division_tariff():
+    """Restoring division: <= 8ab bit-steps, quotient length a, divisor length b."""
+    # Per quotient bit: 2(b+1) subtractor steps and (b+1) shifts = 3(b+1).
+    # Times a, plus a quotient writes: 3ab + 3a + a = 3ab + 4a.
+    # 4a <= 5ab for b >= 1, so 3ab + 4a <= 8ab.
+    need(4 <= 5 * 1, "division b=1")
+    for a in range(1, 13):
+        for b in range(1, 13):
+            touches = a * 3 * (b + 1) + a
+            need(touches <= 8 * a * b, "division tariff " + str((a, b)))
+
+
+def prove_euclid_tariff():
+    """Extended Euclid on a b-bit modulus costs <= 64 b^3 bit-steps for b >= 2.
+
+    Every two remainders the positive value is at least halved:
+    r_i = q r_{i+1} + r_{i+2} with q >= 1 and r_{i+1} > r_{i+2},
+    so r_i >= r_{i+1} + r_{i+2} > 2 r_{i+2}.
+    Hence at most 2b division steps. Each step's division and two coefficient
+    products are <= 32 b^2 bit-steps by the tariffs above.
+    """
+    # 8b^2 division + 16b^2 products + 4b subtractions <= 24b^2 + 4b <= 32b^2.
+    # 24b^2 + 4b <= 32b^2 iff 4b <= 8b^2 iff b >= 1.
+    need(4 <= 8, "Euclid step for every b >= 1")
+    for b in range(1, 9):
+        need(24 * b * b + 4 * b <= 32 * b * b, "Euclid step " + str(b))
+        need(2 * b * 32 * b * b == 64 * b ** 3, "Euclid total " + str(b))
+    # Structural halving on Fibonacci worst cases and on random-looking pairs.
+    samples = [1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597]
+    for modulus in samples:
+        for operand in range(1, modulus):
+            steps = euclid_steps(operand, modulus)
+            bits = bit_length(modulus)
+            need(steps <= 2 * bits, "Euclid steps " + str((operand, modulus)))
+
+
+def euclid_steps(operand, modulus):
+    steps = 0
+    left, right = operand, modulus
+    while left:
+        quotient = right // left
+        remainder = right - quotient * left
+        need(quotient >= 1 and left > remainder, "positive remainder drop")
+        need(right >= left + remainder > 2 * remainder, "strict halving inequality")
+        right, left = left, remainder
+        steps += 1
+        need(steps <= 4 * bit_length(modulus), "runaway Euclid")
+    return steps
+
+
+def prove_benes_recurrence():
+    """Local scan charge (7n+1)*4*n*k <= 32 k n^2, and T <= 64 k n^2."""
+    for k in range(2, 12):
+        n = 1 << k
+        local = (7 * n + 1) * 4 * n * k
+        need(local <= 32 * k * n * n, "local Beneš budget")
+        child = 64 * (k - 1) * (n // 2) ** 2
+        need(2 * child + 32 * k * n * n == 64 * k * n * n - 32 * n * n, "induction algebra")
+        need(2 * child + local <= 64 * k * n * n, "induction with the real local charge")
+    need(13 * 4 * 2 * 1 <= 64 * 1 * 4, "n=2 base charge")
+
+
+def bound(p, ell):
+    return 2 ** (4 * ell) * (p + 2) ** 16
+
+
+def prove_q_maximum():
+    """Every term is C(ell) q^a with a <= 4, so term/B is largest at q = 4.
+
+    For integers q >= 5 and a <= 4, q^a 4^{16} < 4^a q^{16} follows from
+    q^{12} > 4^{12}, and x |-> x^{12} is strictly increasing on the integers.
+    """
+    degrees = {
+        "setup": 2,
+        "crt_quartic": 4,
+        "crt_cubic": 3,
+        "crt_ell_cube": 2,
+        "tables": 1,
+        "networks": 1,
+    }
+    for name, degree in degrees.items():
+        need(degree <= 4, name)
+        need(4 ** (16 - degree) * 5 ** degree < 5 ** 16, "q=5 beats q=4 for " + name)
+    need(5 ** 12 > 4 ** 12, "twelfth powers increase past 4")
+
+
+def prove_master_inequality():
+    """Sum of cost terms <= 2^{4ell}(p+2)^{16} for every integer p >= 2, ell >= 1.
+
+    Each term has q-degree at most 3, so it is largest relative to the bound at
+    q = p+2 = 4. At that corner the ell = 1 value fits, and raising ell
+    multiplies the term by less than it multiplies the bound.
+    """
+    prove_q_maximum()
+    q = 4
+    ell = 1
+    terms = cost_terms(q - 2, ell)
+    limit = bound(q - 2, ell)
+    need(sum(terms.values()) <= limit, "corner sum")
+    need(all(7 * value <= limit for value in terms.values()), "corner sevenths")
+    # Step factors at q=4. B grows by 2^4 = 16 when ell increases by 1.
+    # The quartic and cubic CRT terms do not grow with ell.
+    need(1 <= 16, "ell-independent terms")
+    # 8192 q^2 ell^3 grows by ((ell+1)/ell)^3 <= 8.
+    need(8 <= 16, "ell-cube step")
+    # tables grow by ((ell+3)/(ell+2))^2 * 2 <= (4/3)^2 * 2 = 32/9 at ell=1.
+    need(32 * 16 <= 9 * 16 * 16, "table step 32/9 <= 16")
+    # networks grow by (ell+1)/ell * 4 <= 8.
+    need(8 <= 16, "network step")
+    for p in range(2, 31):
+        for width in range(1, 13):
+            values = cost_terms(p, width)
+            limit = bound(p, width)
+            need(sum(values.values()) <= limit, "grid " + str((p, width)))
+
+
+def cost_terms(p, ell):
+    """Bit-step terms for A<=8(p+2) axes and group width W<=8(p+2).
+
+    CRT allows 8m multiplications, 4m divisions and 2m inverses per axis,
+    with m<=8(p+2). Four rotation networks per axis use the Beneš recurrence.
+    """
+    q = p + 2
+    return {
+        "setup": 256 * q * q,
+        "crt_quartic": 524288 * q ** 4,
+        "crt_cubic": 8192 * q ** 3,
+        "crt_ell_cube": 8192 * q * q * ell ** 3,
+        "tables": 800 * q * (ell + 2) ** 2 * 2 ** ell,
+        "networks": 2048 * q * ell * 2 ** (2 * ell),
+    }
+
+
+def prove_amortization():
+    """E <= 2^{4ell}(p+2)^{16} implies the displayed 2^{-G} E comparison with C=1.
+
+    G = 64 (ell + ceil(log2(p+2))). The integer form is
+    E (p+2)^{48} <= 2^{G - 60 ell}.
+    """
+    for p in range(2, 65):
+        modulus = p + 2
+        ceiling = (modulus - 1).bit_length()  # ceil(log2(modulus))
+        need(2 ** ceiling >= modulus, "ceil log")
+        for ell in (1, 2, 5):
+            guard = 64 * (ell + ceiling)
+            evaluator = 2 ** (4 * ell) * modulus ** 16
+            need(evaluator * modulus ** 48 <= 2 ** (guard - 60 * ell), "amortization")
+    # Universal step: (p+2) <= 2^{ceil(log2(p+2))} gives
+    # 2^{4ell}(p+2)^{64} <= 2^{4ell + 64 ceil(log2(p+2))} = 2^{G - 60 ell}.
+    need(64 - 60 == 4, "exponent split")
+
+
+def independent_benes(permutation):
+    size = len(permutation)
+    need(size >= 2 and size & (size - 1) == 0, "dyadic size")
+    need(sorted(permutation) == list(range(size)), "permutation")
+    if size == 2:
+        return [(0, (permutation[0], permutation[0]))]
+    inverse = [0] * size
+    for position, image in enumerate(permutation):
+        inverse[image] = position
+    color = [-1] * size
+    for start in range(size):
+        if color[start] >= 0:
+            continue
+        color[start] = 0
+        stack = [start]
+        while stack:
+            node = stack.pop()
+            neighbors = (node ^ 1, inverse[permutation[node] ^ 1])
+            for other in neighbors:
+                if color[other] < 0:
+                    color[other] = color[node] ^ 1
+                    stack.append(other)
+                need(color[other] == color[node] ^ 1, "even cycle")
+    first = tuple(color[x] ^ (x & 1) for x in range(size))
+    last = tuple(color[inverse[y]] ^ (y & 1) for y in range(size))
+    children = []
+    for wanted in (0, 1):
+        child = [permutation[x] // 2 for x in range(size) if color[x] == wanted]
+        need(len(child) == size // 2, "child size")
+        children.append(independent_benes(child))
+    layers = [(0, first)]
+    for left, right in zip(*children):
+        need(left[0] == right[0], "aligned schedule")
+        table = tuple((left, right)[x & 1][1][x // 2] for x in range(size))
+        layers.append((left[0] + 1, table))
+    layers.append((0, last))
+    return layers
+
+
+def charged_local_scans(size):
+    """One recursive level's scan count under the procedure in PROOF.md."""
+    if size == 2:
+        return 13
+    scans = 0
+    scans += size  # inverse lookups
+    scans += 4 * size  # two neighbors, permutation and inverse, every node
+    scans += 2 * size  # stack push and pop
+    scans += 1  # emit the two child tables
+    need(scans == 7 * size + 1, "scan formula")
+    return scans
+
+
+def rotation(size, modulus, offset):
+    return tuple((value + offset) % modulus if value < modulus else value for value in range(size))
+
+
+def run_network(layers, value):
+    for bit, table in layers:
+        value ^= table[value] << bit
+    return value
+
+
+def counted_reconstruction(residues, moduli):
+    """Operation counts for the retained decode_group formula."""
+    counts = {"mul": 0, "div": 0, "inv": 0, "add": 0}
+    product = 1
+    for modulus in moduli:
+        if product != 1:
+            counts["mul"] += 1
+        product *= modulus
+    answer = 0
+    prefix = 1
+    for value, modulus in zip(residues, moduli):
+        counts["div"] += 1
+        complement = product // modulus
+        counts["mul"] += 1
+        counts["div"] += 1
+        residue = value * prefix % modulus
+        counts["inv"] += 1
+        inverse = pow(complement, -1, modulus)
+        counts["mul"] += 2
+        counts["add"] += 1
+        answer += residue * complement * inverse
+        counts["mul"] += 1
+        prefix *= modulus
+    return answer % product, counts
+
+
+def group_offset(residues, moduli, target):
+    """k_A * (running prefix)^{-1} mod target, prefix starting at the left product."""
+    product = 1
+    mixed = 0
+    for residue, modulus in zip(residues, moduli):
+        need(0 <= residue < modulus, "residue range")
+        mixed += residue * product
+        product *= modulus
+    prefix = product
+    # Caller passes the right-child moduli already folded into `target` only.
+    try:
+        inverse = pow(prefix, -1, target)
+    except ValueError as exc:
+        raise ValueError("prefix not invertible") from exc
+    return mixed * inverse % target, mixed, product
+
+
+def prove_outputs(source):
+    compared = 0
+    for bits in range(1, 5):
+        size = 1 << bits
+        charged_local_scans(size)
+        for modulus in range(2, size + 1):
+            for offset in range(0, modulus, max(1, modulus // 3)):
+                permutation = rotation(size, modulus, offset)
+                ours = independent_benes(permutation)
+                retained = source.benes(permutation)
+                need(ours == retained, "retained compiler agreement")
+                need(tuple(run_network(ours, value) for value in range(size)) == permutation,
+                     "rotation endpoint")
+                # A single flipped control bit is not the same permutation.
+                broken = [list(table) for _bit, table in ours]
+                broken[0][0] ^= 1
+                mutated = [(bit, tuple(table)) for (bit, _table), table in zip(ours, broken)]
+                mutated_images = tuple(run_network(mutated, value) for value in range(size))
+                need(mutated_images != permutation, "flipped control changes the map")
+                compared += 1
+    need(charged_local_scans(32) == 7 * 32 + 1, "larger level formula")
+    # One balanced step from a zero right child is the CRT offset.
+    checked_groups = 0
+    for moduli in ((3, 5), (5, 7), (4, 3), (8, 5), (9, 4), (11, 8)):
+        for residue in range(moduli[0]):
+            image = source.balanced((residue, 0), moduli)
+            lower = source.decode_group((residue,), (moduli[0],))
+            offset = lower * pow(moduli[0], -1, moduli[1]) % moduli[1]
+            need(image == (residue, offset), "zero right child receives the offset")
+            checked_groups += 1
+    for moduli in ((3, 5, 7, 11),):
+        for residues in ((0, 0), (1, 2), (2, 4), (1, 0)):
+            image = source.balanced(residues + (0, 0), moduli)
+            need(image == source.direct(residues + (0, 0), moduli), "retained direct endpoint")
+            checked_groups += 1
+    need(checked_groups > 20, "enough CRT fixtures")
+    for moduli, residues in (
+        ((3, 5, 7), (1, 2, 3)),
+        ((4, 3, 5, 7), (1, 2, 1, 3)),
+        ((8, 5, 7, 9), (3, 1, 2, 4)),
+    ):
+        got, counts = counted_reconstruction(residues, moduli)
+        need(got == source.decode_group(residues, moduli), "counted reconstruction")
+        modulus_count = len(moduli)
+        need(counts["mul"] <= 8 * modulus_count, "multiplication cap")
+        need(counts["div"] <= 4 * modulus_count, "division cap")
+        need(counts["inv"] <= 2 * modulus_count, "inverse cap")
+        need(counts["add"] <= 4 * modulus_count, "addition cap")
+    # Non-invertible prefix is rejected.
+    rejected = False
+    try:
+        group_offset((1,), (4,), 2)
+    except ValueError:
+        rejected = True
+    need(rejected, "non-invertible prefix must fail")
+    rejected = False
+    try:
+        independent_benes((0, 0))
+    except ValueError:
+        rejected = True
+    need(rejected, "non-permutation must fail")
+    rejected = False
+    try:
+        source.benes((0, 0))
+    except ValueError:
+        rejected = True
+    need(rejected, "retained compiler rejects a non-permutation")
+    return compared, checked_groups
+
+
+def prove_width_hypotheses_cover_theorem():
+    """The closed form already uses A<=8(p+2) and W<=8(p+2); record the slack."""
+    # Worst numeric ratio on a modest rectangle, as a witnessed margin.
+    worst = 0
+    for p in range(2, 25):
+        for ell in range(1, 13):
+            bound = 2 ** (4 * ell) * (p + 2) ** 16
+            ratio = sum(cost_terms(p, ell).values()) / bound
+            if ratio > worst:
+                worst = ratio
+    need(worst < 1 / 50, "uniform margin stronger than 50")
+    return worst
+
+
+def main():
+    prove_schoolbook_tariff()
+    prove_division_tariff()
+    prove_euclid_tariff()
+    prove_benes_recurrence()
+    prove_master_inequality()
+    prove_amortization()
+    source = load_source()
+    compared, groups = prove_outputs(source)
+    worst = prove_width_hypotheses_cover_theorem()
+    print(json.dumps({
+        "status": "PASS_CRT_UNIFORM_EVALUATOR",
+        "constant_C": 1,
+        "networks_per_axis": 4,
+        "axes_at_most": "8(p+2)",
+        "group_bits_at_most": "8(p+2)",
+        "compiler_agreements": compared,
+        "crt_groups": groups,
+        "worst_ratio_on_sample": worst,
+        "kappa_claimed": False,
+    }, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()