diff --git a/research/nearest-even-walsh-error-audit/README.md b/research/nearest-even-walsh-error-audit/README.md
new file mode 100644
index 0000000000..7d5fbd0b62
--- /dev/null
+++ b/research/nearest-even-walsh-error-audit/README.md
@@ -0,0 +1,112 @@
+# Independent audit of #6129's nearest-even Walsh-stage bound
+
+**Audit of an open PR; no new κ, no selected-frontier change.**
+
+[PR #6129](https://github.com/CrocSwap/integer-mult-bounds/pull/6129)
+(Nick Petalas, head `f496734450c346468c66818c1c35521165b0cdda`) claims that J
+distinct normalized Walsh factors `H0=(1/2)[[1,1],[1,-1]]`, each followed by
+nearest-even rounding to a common grid h, have sharp sup-norm error
+
+    h a_J,   a_J = J/3 + (1-(-1/2)^J)/9,
+
+with sharp error `h a_(J-1)` on outputs whose stored value over h is odd. It
+also claims that CubeJerry's
+[PR #6119](https://github.com/CrocSwap/integer-mult-bounds/pull/6119) surrogate
+(head `bdfe5a10d488b5f774e906d8d4588dc8da25e7ba`) has exact global
+normalized error `3h/4`, which is 3/16 at h=1/4.
+
+**Verdict: no error found.** I checked PROOF.md step by step and reproduced
+every stated number with engines that share no code with #6129 or #6119.
+
+## Proof review (PR #6129 PROOF.md)
+
+| Step | Status |
+| --- | --- |
+| R is odd and `R(s+2k)=R(s)+2k`; signs absorbed into leaves | correct. Nearest-even is symmetric at ties. Negating a subtree's leaves negates every stored value in it. Distinct axes give disjoint leaves. |
+| Upper bound (3): even `u+v` is exact with equal child parities; odd `u+v` gives an even root, local error 1/2 and mixed parities | correct. `b_j <= max(a,b)` needs `b_(j-1) <= a_(j-1)`. The `d_j` induction supplies it without circularity. |
+| `d_j=(1-d_(j-1))/2`, `1/4<=d_j<=1/2` | correct. The second line of (3) dominates the exact branch because `d_(j-1)<=1`. |
+| Witnesses (4): E_j children are (0, a), (-1, b), and the root `R(-1/2)=0` adds +1/2. O_j children are (0, a), (2, a), and the root 1 is exact | correct; all signed errors are positive. |
+| Closed form and `a_J<J/2` for J>=2, ratio → 2/3 | correct |
+| Period `2^(J+1)` per input | correct. After k<=J stages the exact displacement is divisible by `2^(J+1-k)`, which is even. |
+| #6119 application | correct. `a=4` is an integer, so upper and inverse are exact on the grid. The lower inverse leaves `h(R(k/2)-k/2)` in {0, ±h/2}, and that rounds to 0 under ties-to-even. |
+
+Two clarifications for readers. They are not errors.
+
+1. The Walsh law depends on parity tie-breaking, not on ties-to-even itself.
+   Ties-to-odd gives the same a_J (engine D). The #6119 application does need
+   ties-to-even: under ties-to-odd, the echo temporary is left at ±h for every
+   odd k, so the echo would not be the identity.
+2. Nearest rounding alone does not give the saving. Floor rounding attains
+   the stagewise bound J/2 at every J<=5. Ties-away-from-zero already reaches
+   J/2=1 at J=2. Every rule here obeys `R(s+2t)=R(s)+2t` except ties-away.
+
+The same integer sequence, `2^J a_J = ((3J+1)2^J-(-1)^J)/9` (0, 1, 3, 9, 23,
+57, ...), is the sharp dyadic rotation switch tariff in
+`research/dyadic-rotation-switch-tariff` (also Nick Petalas). Both proofs
+reduce to the slope recurrence `d_j=(1-d_(j-1))/2`. This is a structural
+remark only. Neither result is used here.
+
+## Independent engines (`verify.py`, stdlib, about 50 s)
+
+- **A. Residue-tracking tree sets.** For one output tree with sign pattern
+  σ, I enumerate every leaf residue mod `2^(J+1)`. After each stage I keep
+  the complete set of (stored value mod `2^(J+1-k)`, exact signed error). By
+  `R(s+2t)=R(s)+2t`, the root residue mod M/2 is determined by the child
+  residues mod M when M>=4. This needs only the period lemma, not #6129's
+  "children can be shifted by any even amount" step. The engine covers every
+  sign pattern for J<=4, the all-plus pattern for J<=7, and both output
+  parities. The even-output maximum equals a_J and the odd-output maximum
+  equals a_(J-1) for every J<=7 (for example, 313/128 at J=7). For J<=4, the
+  (parity, |error|) set is identical across all 2^J sign patterns.
+- **B. Literal network.** This is an exhaustive check of the 8-point network
+  (J=3) on `[-3,0]^8` (65,536 inputs) in three stage orders, over every
+  output coordinate. The maximum is exactly 9/8, and no input exceeds it.
+- **C. #6119 surrogate.** I rebuilt the 12-wire surrogate (exposure, pad,
+  echo m=1/2 and a=4, active H0, unpad, restore, tail H0, six rounded maps) in
+  integer units of h/8. I checked it exhaustively over each spectator fiber
+  modulo 8h (8,192 inputs), plus 300 random period-8h shifts. The sup is
+  exactly 3h/4. #6129's original-coordinate witness (0,0,-1/4,0,-1/2,0,0,0)
+  attains it. *Local-only cross-check, not in the verifier:* on 3,000 random
+  grid inputs, my rebuild agrees exactly with #6119's own `program()`/`forward(rounding=True)`
+  at the head above.
+- **D. Controls.** Ties-to-odd gives the same law. Floor gives exactly J/2.
+  Ties-away-from-zero reaches 1 at J=2. Under ties-to-odd, the echo is dirty
+  on odd residues.
+
+Engine A uses the period lemma. Its proof is short and is given above and in
+#6129. The verifier only samples it, on 400 random literal J=3 networks. So
+engine A is a complete check *given* that lemma, not a proof-free
+exhaustion. Engine B is literal for J=3 on a box only. All-J correctness rests
+on the written proof, which I found correct.
+
+## Reproduce
+
+```sh
+python3 scripts/research_package.py --package research/nearest-even-walsh-error-audit --check-only
+python3.12 scripts/research_package.py --package research/nearest-even-walsh-error-audit
+```
+
+## Not covered
+
+This audit makes no claim about #6119's arbitrary-defect theorem or its
+mutation checks. It also does not cover bit costs, range guards, reversible
+history or any PR6030 child or supplier. These remain separate obligations
+of #6129 and #6119.
+
+## Open next questions
+
+- Whether a rounded echo is clean depends on the tie rule (engine D). Which
+  native rounded compilers on main rely on a ties-to-even cancellation like
+  #6119's lower inverse? A first step is to grep the retained rounded
+  shear/echo packages and look for `m=1/2` half-tie cancellations.
+- Does the sharp law survive when a non-Walsh gate sits between two rounded
+  stages (for example a grid shear)? #6129 excludes this case. A first step
+  is to put one intervening shear into engine A and enumerate it.
+
+## Credit
+
+The theorem, proof and witnesses are Nick Petalas's (#6129). The surrogate and
+the deferred-row context are CubeJerry's (#6119, with OpenAI Codex assistance)
+and Vlado Vojdanovski's (PR1673), with the lineage credited in #6129. This
+audit and its engines were prepared by Josie Elliston with Claude Opus 5.5
+(Anthropic) assistance. Apache-2.0.
diff --git a/research/nearest-even-walsh-error-audit/SOURCES.json b/research/nearest-even-walsh-error-audit/SOURCES.json
new file mode 100644
index 0000000000..40f96c767a
--- /dev/null
+++ b/research/nearest-even-walsh-error-audit/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}
diff --git a/research/nearest-even-walsh-error-audit/TASK.json b/research/nearest-even-walsh-error-audit/TASK.json
new file mode 100644
index 0000000000..3c9b918328
--- /dev/null
+++ b/research/nearest-even-walsh-error-audit/TASK.json
@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "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_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Independent adversarial audit of open PR #6129 (head f496734450c346468c66818c1c35521165b0cdda): sharp nearest-even normalized Walsh-stage error h(J/3+(1-(-1/2)^J)/9), its odd-output refinement, and its all-grid 3h/4 application to PR #6119 (head bdfe5a10d488b5f774e906d8d4588dc8da25e7ba).",
+  "scope_change_reason": "The card asks for a proof of an inherited assumption; #6129 claims one precision implication under this card, and a fresh, unreviewed proof is most useful checked independently before anyone relies on it.",
+  "bottleneck_link": "Side result for precision obligations: confirms (or would refute) a deterministic rounding budget that a deferred-row/Walsh supplier could cite. No supplier, invoice or kappa changes.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop after a step-by-step proof review plus independent exact engines reproduce or refute each stated number; report any gap found rather than repairing #6129.",
+  "outcome": "completed",
+  "evidence": "PROOF.md reviewed step by step: no error. verify.py: residue-tracking tree sets J<=7 (all 2^J sign patterns for J<=4) give even/odd maxima a_J/a_(J-1); literal 8-point network exhaustive on [-3,0]^8 in three orders gives 9/8; rebuilt #6119 surrogate exhaustive per fiber mod 8h gives 3h/4 with #6129's witness; controls: ties-to-odd same law, floor and ties-away reach J/2, ties-to-odd leaves #6119's echo dirty. Local-only: rebuild agrees with #6119 forward() on 3000 random grid inputs.",
+  "author": "Josie Elliston with Claude Opus 5.5 (Anthropic) assistance",
+  "ai_assistance": "Claude Opus 5.5 (Anthropic) wrote the review and verifier under Josie Elliston's donated session; no code from #6129 or #6119 is imported.",
+  "open_questions": [
+    {
+      "question": "Which retained rounded compilers rely on a ties-to-even half-tie cancellation like #6119's m=1/2 lower inverse?",
+      "why_it_matters": "Engine D shows the cancellation fails under ties-to-odd although the Walsh law does not; a tie-rule change would silently dirty such echoes.",
+      "first_step": "Search retained rounded shear/echo packages for m=1/2 cancellations and test each under ties-to-odd.",
+      "blocked_by": "none"
+    },
+    {
+      "question": "Does the sharp a_J law survive one intervening grid shear between rounded Walsh stages?",
+      "why_it_matters": "#6129 excludes intervening gates; real suppliers interleave them.",
+      "first_step": "Add one integer shear stage to engine A's residue-tracking enumeration.",
+      "blocked_by": "none"
+    }
+  ]
+}
diff --git a/research/nearest-even-walsh-error-audit/VERIFY.json b/research/nearest-even-walsh-error-audit/VERIFY.json
new file mode 100644
index 0000000000..a4f4263262
--- /dev/null
+++ b/research/nearest-even-walsh-error-audit/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Engines A-D: residue-tracking tree sets J<=7 (all sign patterns J<=4), literal J=3 box exhaustion in three stage orders, #6119 surrogate fiber exhaustion mod 8h with period samples, rounding-rule controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "The same exact checks with assertions disabled (the verifier uses explicit raises)."
+    }
+  ]
+}
diff --git a/research/nearest-even-walsh-error-audit/verify.py b/research/nearest-even-walsh-error-audit/verify.py
new file mode 100644
index 0000000000..bc3900c3ae
--- /dev/null
+++ b/research/nearest-even-walsh-error-audit/verify.py
@@ -0,0 +1,274 @@
+#!/usr/bin/env python3
+"""Independent audit engine for PR #6129's nearest-even Walsh-stage bound.
+
+Session 51 (JosieElliston fork, Claude Opus 5.5 assistance). Apache-2.0.
+Stdlib only. Nothing is imported from PR #6129 or PR #6119.
+
+Engines, all exact (Fraction / int):
+  A. residue-tracking tree sets: for every output sign pattern, the complete
+     set of (stored value mod 2^(J+1-k), error) after k stages, started from
+     every leaf residue mod 2^(J+1). Unlike #6129's parity-only recurrence it
+     does not use the "children can be shifted by any even amount" step; it
+     uses only R(s + 2t) = R(s) + 2t and the period-2^(J+1) lemma.
+  B. literal array exhaustion of the 8-point network (J=3) on the box
+     [-3,0]^8, both stage orders, every output coordinate.
+  C. a re-implementation of #6119's 12-wire echo surrogate in integer units
+     of h/8, exhaustive over one spectator fiber modulo 8h.
+  D. controls: ties-to-odd gives the same law (only parity tie-breaking
+     matters); floor gives the stagewise J/2 exactly and ties-away-from-zero
+     already reaches J/2 at J=2, so the saving needs parity tie-breaking.
+"""
+
+from fractions import Fraction
+from itertools import product
+import json
+import sys
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def r_even(q):
+    """Nearest integer to Fraction q, ties to even (independent of round())."""
+    fl = q.numerator // q.denominator
+    rem = q - fl
+    if rem < Fraction(1, 2):
+        return fl
+    if rem > Fraction(1, 2):
+        return fl + 1
+    return fl if fl % 2 == 0 else fl + 1
+
+
+def r_odd(q):
+    fl = q.numerator // q.denominator
+    rem = q - fl
+    if rem != Fraction(1, 2):
+        return r_even(q)
+    return fl if fl % 2 else fl + 1
+
+
+def r_floor(q):
+    return q.numerator // q.denominator
+
+
+def claimed(j):
+    return Fraction(j, 3) + (1 - Fraction(-1, 2) ** j) / 9
+
+
+# ---------------------------------------------------------------- engine A
+def tree_states(depth, signs, rnd):
+    """States (stored mod M, signed error) for one output tree.
+
+    signs[k] = +1 or -1 is the combination used at stage k+1. Valid for any
+    rounding rule with rnd(q + 2t) = rnd(q) + 2t (all three rules here).
+    """
+    mod = 1 << (depth + 1)
+    states = {(r, Fraction(0)) for r in range(mod)}
+    for sigma in signs:
+        need(mod >= 4, "modulus stays >= 4 before each combination")
+        nxt = set()
+        lst = sorted(states)
+        for (u, eu) in lst:
+            for (v, ev) in lst:
+                s = (u + sigma * v) % mod
+                stored = rnd(Fraction(s, 2))
+                local = stored - Fraction(s, 2)
+                nxt.add((stored % (mod // 2), local + (eu + sigma * ev) / 2))
+        states, mod = nxt, mod // 2
+    return states, mod
+
+
+def engine_a(max_all_signs=4, max_depth=7):
+    rows = []
+    for depth in range(0, max_depth + 1):
+        patterns = (list(product((1, -1), repeat=depth)) if depth <= max_all_signs
+                    else [(1,) * depth])
+        seen = None
+        for signs in patterns:
+            states, mod = tree_states(depth, signs, r_even)
+            need(mod == 2, "final modulus is two: output parity is determined")
+            even = [abs(e) for r, e in states if r == 0]
+            odd = [abs(e) for r, e in states if r == 1]
+            errs = sorted({e for _, e in states})
+            need(max(even) == claimed(depth), "even-output sharp error a_J")
+            need(max(odd) == (claimed(depth - 1) if depth else 0), "odd-output sharp a_(J-1)")
+            need(errs == sorted({-e for e in errs}), "error set symmetric")
+            if seen is None:
+                seen = states
+            need({(r, abs(e)) for r, e in states} == {(r, abs(e)) for r, e in seen},
+                 "all sign patterns give the same parity/|error| set")
+        rows.append({"J": depth, "sign_patterns": len(patterns),
+                     "sup_error": str(claimed(depth)),
+                     "odd_output_sup": str(claimed(depth - 1) if depth else 0),
+                     "distinct_errors": len(errs)})
+    return rows
+
+
+def engine_a_period(depth=3, trials=400):
+    """Sample the period lemma used by engine A on literal networks.
+
+    The lemma itself is proved in README.md (and #6129 PROOF.md); this is a
+    consistency control, not its proof."""
+    import random
+    rng = random.Random(6129)
+    n = 1 << depth
+    for _ in range(trials):
+        x = [rng.randrange(-50, 50) for _ in range(n)]
+        z = [rng.randrange(-5, 6) for _ in range(n)]
+        y = [a + (2 * n) * b for a, b in zip(x, z)]
+        need(errors(x, list(range(depth))) == errors(y, list(range(depth))),
+             "period 2^(J+1) per input")
+    return trials
+
+
+# ---------------------------------------------------------------- engine B
+def network(x, order, rnd=r_even):
+    vals = [Fraction(v) for v in x]
+    n = len(vals)
+    for bit in order:
+        w = 1 << bit
+        out = list(vals)
+        for i in range(n):
+            if not i & w:
+                a, b = vals[i], vals[i | w]
+                out[i] = (a + b) / 2
+                out[i | w] = (a - b) / 2
+                if rnd is not None:
+                    out[i], out[i | w] = Fraction(rnd(out[i])), Fraction(rnd(out[i | w]))
+        vals = out
+    return vals
+
+
+def errors(x, order, rnd=r_even):
+    exact = network(x, order, None)
+    got = network(x, order, rnd)
+    return [g - e for g, e in zip(got, exact)]
+
+
+def engine_b():
+    depth, n = 3, 8
+    best = {}
+    for order in ([0, 1, 2], [2, 1, 0], [1, 0, 2]):
+        top = Fraction(0)
+        for x in product(range(-3, 1), repeat=n):
+            e = max(abs(v) for v in errors(x, order))
+            need(e <= claimed(depth), "box input exceeds a_3")
+            top = max(top, e)
+        need(top == claimed(depth), "a_3 attained in [-3,0]^8")
+        best[str(order)] = str(top)
+    return {"inputs_per_order": 4 ** n, "orders": best}
+
+
+# ---------------------------------------------------------------- engine C
+def surrogate(x8, rule=r_even, strict=True):
+    """#6119 surrogate rebuilt from its definition; x8 in units of h, returns
+    the normalized error vector in units of h. Units of h/8 internally."""
+    unit = 8
+    q = [0] * 8
+    for old in range(8):  # exposure: original bit 1 becomes bit 0
+        q[(old & 4) | ((old & 1) << 1) | ((old & 2) >> 1)] = old
+
+    def rnd(vals):  # nearest-even to the h grid, values in h/8 units
+        return [rule(Fraction(v, unit)) * unit for v in vals]
+
+    v = [x8[q[i]] * unit for i in range(8)] + [0] * 4
+    m_num, m_den, a = 1, 2, 4
+    v = rnd([v[i] if i < 8 else v[i] + Fraction(m_num * v[i - 8], m_den) for i in range(12)])
+    v = rnd([v[i] + a * v[i + 8] if i < 4 else v[i] for i in range(12)])
+    v = rnd([v[i] - a * v[i + 8] if i < 4 else v[i] for i in range(12)])
+    v = rnd([v[i] if i < 8 else v[i] - Fraction(m_num * v[i - 8], m_den) for i in range(12)])
+    if not strict:
+        return v[8:]
+    need(v[8:] == [0] * 4, "echo temporaries return to zero on grid inputs")
+    w = list(v)
+    for i in range(0, 12, 2):
+        w[i], w[i + 1] = Fraction(v[i] + v[i + 1], 2), Fraction(v[i] - v[i + 1], 2)
+    v = rnd(w)
+    back = [0] * 8
+    for i in range(8):
+        back[q[i]] = v[i]
+    w = list(back)
+    for i in range(4):
+        w[i], w[i + 4] = Fraction(back[i] + back[i + 4], 2), Fraction(back[i] - back[i + 4], 2)
+    out = [Fraction(t, unit) for t in rnd(w)]
+    exact = [sum(Fraction((-1) ** bin(i & j & 6).count("1"), 4) * x8[j]
+                 for j in range(8) if not (i ^ j) & 1) for i in range(8)]
+    return [o - e for o, e in zip(out, exact)]
+
+
+def engine_c():
+    top, count = Fraction(0), 0
+    for spectator in (0, 1):
+        for vals in product(range(8), repeat=4):
+            x = [0] * 8
+            for k, idx in enumerate(i for i in range(8) if i & 1 == spectator):
+                x[idx] = vals[k]
+            e = max(abs(t) for t in surrogate(x))
+            top = max(top, e)
+            count += 1
+    need(top == Fraction(3, 4), "surrogate sharp normalized error 3h/4")
+    witness = [0, 0, -1, 0, -2, 0, 0, 0]  # (0,0,-1/4,0,-1/2,0,0,0) at h=1/4
+    need(max(abs(t) for t in surrogate(witness)) == Fraction(3, 4), "#6129 witness")
+    import random
+    rng = random.Random(6119)
+    for _ in range(300):
+        x = [rng.randrange(-40, 40) for _ in range(8)]
+        z = [rng.randrange(-4, 5) for _ in range(8)]
+        need(surrogate([a + 8 * b for a, b in zip(x, z)]) == surrogate(x),
+             "period 8h per input on the surrogate")
+    # Control: with ties-to-odd the lower inverse leaves +/-h on odd inputs,
+    # so the echo is not clean; the #6119 application needs ties-to-even.
+    dirty = [k for k in range(8) if surrogate([k] + [0] * 7, r_odd, strict=False) != [0] * 4]
+    need(dirty == [1, 3, 5, 7], "ties-to-odd leaves the echo temporary dirty exactly on odd k")
+    return {"fiber_inputs": count, "sup_over_h": str(top),
+            "ties_to_odd_dirty_residues": dirty,
+            "at_h_1_4": str(top / 4), "raw_recovery": str(top)}
+
+
+# ---------------------------------------------------------------- engine D
+def r_away(q):
+    """Nearest integer, ties away from zero (not 2-periodic near 0)."""
+    fl = q.numerator // q.denominator
+    if q - fl != Fraction(1, 2):
+        return r_even(q)
+    return fl + 1 if q > 0 else fl
+
+
+def engine_d(max_depth=5):
+    out = {}
+    for name, rule in (("ties_to_odd", r_odd), ("floor", r_floor)):
+        vals = []
+        for depth in range(max_depth + 1):
+            states, _ = tree_states(depth, (1,) * depth, rule)
+            vals.append(max(abs(e) for _, e in states))
+        out[name] = [str(t) for t in vals]
+        if name == "ties_to_odd":
+            need(vals == [claimed(d) for d in range(max_depth + 1)],
+                 "ties-to-odd has the same sharp law")
+        else:
+            need(vals == [Fraction(d, 2) for d in range(max_depth + 1)],
+                 "floor attains the stagewise J/2")
+    away = max(max(abs(t) for t in errors(x, [0, 1], r_away))
+               for x in product(range(-8, 8), repeat=4))
+    need(away == 1, "ties-away-from-zero attains J/2 at J=2 on [-8,8)^4")
+    out["ties_away_J2_box_lower_bound"] = str(away)
+    return out
+
+
+def main():
+    result = {
+        "engine_A_residue_tree_sets": engine_a(),
+        "engine_A_period_lemma_samples": engine_a_period(),
+        "engine_B_literal_J3_box": engine_b(),
+        "engine_C_pr6119_surrogate": engine_c(),
+        "engine_D_controls_sup_error_by_J": engine_d(),
+        "conclusion": "PASS: PR6129 formula, parity split and #6119 3h/4 application reproduced",
+    }
+    json.dump(result, sys.stdout, indent=1)
+    print()
+
+
+if __name__ == "__main__":
+    main()