diff --git a/research/staged544-two-neighbour-invoice/README.md b/research/staged544-two-neighbour-invoice/README.md
new file mode 100644
index 0000000000..6319cf796b
--- /dev/null
+++ b/research/staged544-two-neighbour-invoice/README.md
@@ -0,0 +1,83 @@
+# Two-neighbour ADD moves do not improve the raw moment
+
+**No new κ.** Selected κ stays 0.001672660197076918.
+
+This is a scoped obstruction for one frame-path change left open by
+[PR #3942](https://github.com/CrocSwap/integer-mult-bounds/pull/3942).
+It is not a review of that paper's interaction or new-gap reduction, and it
+is not the radius-one theorem. The first displacement there is one neighbour.
+Here the first ADD crosses at least two scalar neighbours.
+
+## Result
+
+Fix either literal PR #3734 provider word carried by PR #3942. Consider an
+existing ADD, a cut in its commuting corridor that passes at least two gates,
+and any common frame dimension legal for the removed-gate interval at that
+cut. The raw rank-moment delta of that first move is nonnegative for every
+real `0 < a < 1`. The certificate is the predecessor curvature test: rank
+mass zero and nonnegative partial sums of `C_k = sum_r d_r min(r, k)`.
+The first-move price depends only on dimension, by the interval formula in
+PR #3942, PROOF.md §4, so this dimension census covers every subspace of
+the same dimension.
+
+Each provider has 5,501 ADD gates, 4,979 of them with a long cut, and
+1,761,760 dimension cases: 239,103 nonzero and 1,522,657 neutral. The two
+providers agree on these counts. None improves.
+
+One changed-frame witness on the base word is gate `A[595] = add 459 510`
+with coefficient `-1` and empty frame. Moving it to cut `1214` crosses 618
+gates, including both an ADD and a SCALE, and the only legal rank-1 frame
+is `span{85}`. The frame bill changes by `+3` rank-1 children and `-1`
+rank-3 child. Its caps are `[2, 1, 0, ...]`, so the move is strictly losing.
+After the coefficient update and rederived cleanup, the edited word passes
+the vendored frame auditor. Every one of the 1,767,681 single-ADD
+retimings of that edited word keeps the combined histogram certified
+nonnegative. This witness does not unlock a saving inside that single-move
+class.
+
+## What this does not show
+
+A second move that itself changes a frame interval of quotient rank greater
+than 1, or a second cut that is priced only after another long move, is
+outside the continuation census. Native phase, hosting, stock, precision,
+tape, all-size transfer and both supplier caps are not repriced. Unknown
+costs are not zero. The scalar crossing rule is the sufficient PR #3886
+condition, not every algebraic commutation. No 632-input free-operator
+replay was repeated. This is not a multiplication theorem.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B research/staged544-two-neighbour-invoice/verify.py
+python3 -B scripts/research_package.py --package research/staged544-two-neighbour-invoice
+```
+
+The expected first line starts
+`PASS_STAGED544_TWO_NEIGHBOUR_INVOICE` and ends with `improving=0 no_new_kappa`.
+The registered timeout is 180 seconds. A local run is well under that.
+
+`vendor/retiming.py` is byte-identical to PR #3942 at
+`1416f8cd6bfb2f2eb9aa5cc22f0388a85fdbac91`. `vendor/audit_core.py` and both
+`inputs/BORROW-WORD-43*.json.gz` files are the copies carried in that
+package. SHA256 values are checked before use.
+
+## Open next questions
+
+1. Does every long first move, not only `A[595]`, keep every single-ADD
+   continuation nonnegative? One witness cannot extend the radius-one
+   theorem. The first step is the same continuation census on a move whose
+   frame interval has quotient rank greater than 1.
+2. Can a second ADD that itself crosses two neighbours improve the combined
+   raw moment? Freeze one edited word and one such second cut before any
+   larger search.
+
+## Credit
+
+PR #3734 / dataisfire for the provider words. PR #3886 and PR #3942 /
+Chris R, Clear1nsight, for the retiming rules, curvature test and the open
+two-neighbour question. Sagar Thakrar for the frame auditor. The radius-one
+interaction reduction remains their argument; this package does not review
+it. New census and witness by unpaidmoon, with substantial Cursor Grok
+assistance. Apache-2.0.
diff --git a/research/staged544-two-neighbour-invoice/SOURCES.json b/research/staged544-two-neighbour-invoice/SOURCES.json
new file mode 100644
index 0000000000..a604c6a640
--- /dev/null
+++ b/research/staged544-two-neighbour-invoice/SOURCES.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}
diff --git a/research/staged544-two-neighbour-invoice/TASK.json b/research/staged544-two-neighbour-invoice/TASK.json
new file mode 100644
index 0000000000..e3a285227d
--- /dev/null
+++ b/research/staged544-two-neighbour-invoice/TASK.json
@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "scalar-to-moment",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "scalar-to-moment",
+    "question": "Can one known scalar simplification be converted into an actual paid-profile improvement?",
+    "starting_points": [
+      "research/r439-bsection-stars-seed01/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Derive the changed legal frame itinerary and exact child histogram.",
+      "Prove a scoped obstruction showing why that scalar gain cannot change the paid contract."
+    ],
+    "acceptance_gate": "An unchanged histogram is not a kappa gain; record any separate runtime or proof benefit explicitly.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/r439-bsection-stars-seed01/verify.py"
+      ],
+      "expected": "PASS_R439_BSECTION_STARS",
+      "inspect": "Observe that the positive control improves scalar counts while retaining the paid histogram.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Choose one simplification and derive the complete changed frame itinerary, or prove why it cannot change the histogram.",
+    "bottleneck_link": "A legal change to the histogram, not addition count alone, is the bridge to an exponent gain.",
+    "allowed_variations": [
+      "One existing scalar simplification and one proposed frame-path change."
+    ],
+    "scope_change_triggers": [
+      "Submitting only another scalar count as completion of a paid-profile task."
+    ],
+    "overlap_terms": [
+      "scalar simplification",
+      "paid profile",
+      "R439"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "On both pinned PR3734 staged544 providers, price every legal first ADD move that crosses at least two scalar neighbours, at every feasible common-frame dimension, and price every single-ADD continuation after one explicit changed-frame witness.",
+  "scope_change_reason": "The card allows one frame-path change. This is that change for the PR3942 radius-one contract: the first ADD crosses two or more neighbours and may change frame. It is not an R439 scalar-count reduction, and it does not review the radius-one interaction reduction.",
+  "bottleneck_link": "A negative raw-moment delta on this frame path would be a paid-histogram change. The certified nonnegative deltas show this path does not supply one. No kappa is claimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the dimension-complete long-first census on both providers and the single-move continuation census of one changed-frame witness. Do not search a second long move or review PROOF.md sections 2-3.",
+  "outcome": "negative-result",
+  "evidence": "Exact nonnegative S_j certificates for every long first-move dimension and for every single-move continuation of witness A/595/cut 1214/frame [85].",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok assisted the census script, packaging, and write-up. The predecessor trace and frame auditor are vendored unchanged.",
+  "open_questions": [
+    {
+      "question": "After every long first move, not only witness A/595, does every single-ADD continuation stay nonnegative?",
+      "why_it_matters": "One witness does not extend the radius-one theorem to the whole two-neighbour class.",
+      "first_step": "Repeat the continuation census on a long move whose feasible frame interval has quotient rank greater than 1.",
+      "blocked_by": "The pair of censuses is a different budget from this witness."
+    },
+    {
+      "question": "Can a second ADD that itself crosses two or more neighbours improve the combined raw moment?",
+      "why_it_matters": "The continuation census uses the single-move corridor, which prices every distance inside that corridor, but a second changed-frame long move can change geometry again.",
+      "first_step": "Freeze one edited word and one second cut that crosses two neighbours, then add the two histograms.",
+      "blocked_by": "No source-bound obstruction for that second long move is claimed here."
+    }
+  ]
+}
diff --git a/research/staged544-two-neighbour-invoice/VERIFY.json b/research/staged544-two-neighbour-invoice/VERIFY.json
new file mode 100644
index 0000000000..604af2c776
--- /dev/null
+++ b/research/staged544-two-neighbour-invoice/VERIFY.json
@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "SHA256 of the vendored trace, auditor and both provider words; dimension-complete long-first census on both providers; one changed-frame witness frame bill; every single-ADD continuation certificate; a negative curvature control."
+    }
+  ]
+}
diff --git a/research/staged544-two-neighbour-invoice/inputs/BORROW-WORD-43base.json.gz b/research/staged544-two-neighbour-invoice/inputs/BORROW-WORD-43base.json.gz
new file mode 100644
index 0000000000..674ea18ade
Binary files /dev/null and b/research/staged544-two-neighbour-invoice/inputs/BORROW-WORD-43base.json.gz differ
diff --git a/research/staged544-two-neighbour-invoice/inputs/BORROW-WORD-43extra.json.gz b/research/staged544-two-neighbour-invoice/inputs/BORROW-WORD-43extra.json.gz
new file mode 100644
index 0000000000..b17e2be67e
Binary files /dev/null and b/research/staged544-two-neighbour-invoice/inputs/BORROW-WORD-43extra.json.gz differ
diff --git a/research/staged544-two-neighbour-invoice/vendor/audit_core.py b/research/staged544-two-neighbour-invoice/vendor/audit_core.py
new file mode 100644
index 0000000000..8b5e1d5f2a
--- /dev/null
+++ b/research/staged544-two-neighbour-invoice/vendor/audit_core.py
@@ -0,0 +1,480 @@
+"""Independent exact semantics and binary-frame bill for the BORROW-WORD format.
+
+Standard library only. Nothing is imported from the audited authors' code
+(PR3133/PR3605 producers, cleanup generator, evaluator or frame solver); the word
+format and its semantic contract were read from those pinned sources and are
+credited there.  The frame-bill and free-word structure (point-set spans, warp
+frame and lifted-frame checks, target levels keyed by register, dual symbol
+naming) re-implements, without importing, Arham Tahir's
+research/coupled-carrier-independent-audit/verify.py (Apache-2.0) and shares its
+reading of the contract, so this module is not independent of that audit.
+
+Sagar Thakrar (thakrarsagar), with substantial AI assistance from Claude
+(Anthropic, Claude Opus 5.5). Apache-2.0.
+"""
+from collections import Counter
+from fractions import Fraction as Q
+
+V, N, H = 112, 704, 9          # sources 0..111, targets 112..223, helpers 224..703
+DUAL = 10 ** 6                  # offset naming the independent dual symbols D_k = K_k^(-T)
+
+
+class AuditFailure(Exception):
+    """Explicit failure; never disabled by python -O."""
+
+
+def need(ok, *why):
+    if not ok:
+        raise AuditFailure(' '.join(map(str, why)))
+
+
+def is_target(r):
+    return V <= r < 2 * V
+
+
+def touched(g):
+    return g[1:3] if g[0] == 'add' else g[1:2]
+
+
+# ----------------------------------------------------------------------------
+# Binary frames: a subspace of F_2^9 is stored as a 512-bit point-set mask
+# (bit x set iff x lies in the subspace).  Containment is mask inclusion.
+# ----------------------------------------------------------------------------
+_SPAN = {}
+
+
+def span(vectors):
+    key = tuple(vectors)
+    mask = _SPAN.get(key)
+    if mask is None:
+        points = {0}
+        for u in key:
+            need(type(u) is int and 0 <= u < 512, 'frame vector out of range', u)
+            if u not in points:
+                points |= {p ^ u for p in points}
+        mask = sum(1 << p for p in points)
+        _SPAN[key] = mask
+    return mask
+
+
+def points(mask):
+    return [x for x in range(512) if mask >> x & 1]
+
+
+def dim(mask):
+    size = bin(mask).count('1')
+    need(size and size & (size - 1) == 0, 'not a subspace point set')
+    return size.bit_length() - 1
+
+
+FULL = (1 << 512) - 1
+ZERO = 1
+
+
+def hyperplane(port):
+    return sum(1 << x for x in range(512) if bin(x & port).count('1') % 2 == 0)
+
+
+def warp_images(columns):
+    """Images of all 512 vectors under the F_2-linear map with columns G e_i."""
+    need(len(columns) == H and all(type(c) is int and 0 <= c < 512 for c in columns), 'warp columns')
+    images = [0] * 512
+    for x in range(1, 512):
+        low = x & -x
+        images[x] = images[x ^ low] ^ columns[low.bit_length() - 1]
+    need(len(set(images)) == 512, 'singular warp')
+    return images
+
+
+def image_mask(images, mask):
+    return sum(1 << images[x] for x in points(mask))
+
+
+def lagrangian_action_ok(images, U, E):
+    """K_G(x,z)=(Gx, Gx+G^{-T}(x+z)) is symplectic and maps L_U to L_E, L_0 and L_FULL to themselves.
+
+    L_U={(x,x+p): x in U, p in U^perp}.  This is the binary frame action only; it
+    is not a Clifford phase or Gaussian-product certificate.  For invertible G with
+    G(U)=E it is implied by the frame-map check (<G^-T p, Gu> = <p, u>), so it is a
+    consistency check of the implementation, not extra evidence.
+    """
+    inverse = [0] * 512
+    for x, y in enumerate(images):
+        inverse[y] = x
+    # G^{-T} z: bit j of the result is <G^{-1} e_j, z>.
+    git = lambda z: sum((bin(inverse[1 << j] & z).count('1') & 1) << j for j in range(H))
+    lift = lambda x, z: (images[x], images[x] ^ git(x ^ z))
+    pair = lambda a, b: (bin(a[0] & b[1]).count('1') + bin(a[1] & b[0]).count('1')) & 1
+    basis = [(1 << i, 0) for i in range(H)] + [(0, 1 << i) for i in range(H)]
+    lifted = [lift(*b) for b in basis]
+    if any(pair(lifted[i], lifted[j]) != pair(basis[i], basis[j]) for i in range(18) for j in range(i + 1, 18)):
+        return False
+
+    def frame(mask):
+        us = points(mask)
+        perp = [p for p in range(512) if all(bin(p & u).count('1') % 2 == 0 for u in us)]
+        return {(u, u ^ p) for u in us for p in perp}
+    return all({lift(*pt) for pt in frame(a)} == frame(b) for a, b in ((ZERO, ZERO), (FULL, FULL), (U, E)))
+
+
+# ----------------------------------------------------------------------------
+# Chronological binary-frame bill (BORROW-WORD contract)
+# ----------------------------------------------------------------------------
+def frame_bill(w, lagrangian=False):
+    rep = w['report']
+    need((rep['v'], 2 * rep['v'] + rep['R'], rep['h']) == (V, N, H), 'word geometry')
+    removed = set(w['removed'])
+    need(len(removed) == len(w['removed']) and all(2 * V <= r < N for r in removed), 'removed helpers')
+    live = [r for r in range(N) if r not in removed]
+    liveset = set(live)
+    B, warps = w['B'], w['warps']
+    for k, (pos, lender, cols, U, E) in enumerate(warps, 1):
+        need(0 <= pos <= len(B), 'warp position', k)
+        need(lender in liveset and not is_target(lender), 'warp lender', k)
+        images = warp_images(cols)
+        su, se = span(U), span(E)
+        need(dim(su) == len(U) == len(E) == dim(se), 'warp frame bases', k)
+        need(image_mask(images, su) == se, 'warp does not map its frame', k)
+        if lagrangian:
+            need(lagrangian_action_ok(images, su, se), 'lifted frame action', k)
+    for name in ('A', 'B', 'restore'):
+        for g in w[name]:
+            if g[0] != 'warp':
+                need(all(r in liveset for r in touched(g)), 'removed/out-of-range register', name, g)
+                if g[0] == 'add' and not is_target(g[1]):
+                    need(not is_target(g[2]), 'non-target reads a target', name, g)
+    need(all(g[-1] is None and is_target(g[1]) and g[0] == 'add' for g in w['cut']), 'cut gates')
+    need(all(g[-1] == [] and is_target(g[1]) for g in w['precondition'] + w['compensation']), 'zero-frame wrapper writes')
+    need(all(not is_target(g[1]) for g in w['restore']), 'restore writes a target')
+
+    ports = w['ports']
+    start, end = {}, {}
+    for r in live:
+        if r < V:
+            start[r], end[r] = span((ports[r],)), FULL
+        elif r < 2 * V:
+            start[r], end[r] = ZERO, hyperplane(ports[r - V])
+        else:
+            start[r], end[r] = ZERO, FULL
+    for q, U in w['start_extra'].items():
+        need(int(q) in liveset and int(q) >= 2 * V, 'entrance names a live helper', q)
+        start[int(q)] = span(U)
+    for q, U in w['helper_final'].items():
+        need(int(q) in liveset and int(q) >= 2 * V, 'terminal names a live helper', q)
+        end[int(q)] = span(U)
+
+    current, bill, chain = dict(start), Counter(), {}
+
+    def climb(r, mask, where):
+        need(current[r] & ~mask == 0, 'frame containment fails', where, r)
+        d = dim(mask) - dim(current[r])
+        if d:
+            bill[d] += 1
+        chain.setdefault(r, []).append((where, d, mask))
+        current[r] = mask
+
+    npre = w['prelude_events']
+    for i, g in enumerate(w['A']):
+        if g[0] == 'warp':
+            need(i < npre and len(g) == 5, 'warp outside the prelude', i)
+            _, r, op, fr, to = g
+            need(op != 0 and abs(op) <= len(warps) and warps[abs(op) - 1][1] == r, 'prelude warp lender', i)
+            images = warp_images(warps[abs(op) - 1][2])
+            if op < 0:
+                inverse = [0] * 512
+                for x, y in enumerate(images):
+                    inverse[y] = x
+                images = inverse
+            need(image_mask(images, span(fr)) == span(to), 'prelude warp frame action', i)
+            need(current[r] == span(fr), 'prelude warp entry frame', i, r)
+            current[r] = span(to)
+            chain.setdefault(r, []).append((('A', i), 'warp', span(to)))
+        else:
+            if i < npre:
+                need(is_target(g[1]), 'prelude scalar writes a non-target', i)
+            for r in touched(g):
+                climb(r, span(g[-1]), ('A', i))
+    levels = {V + int(t): span(U) for t, U in w['target_levels'].items()}
+    need(all(current[t] == levels.get(t, ZERO) for t in range(V, 2 * V)), 'target cut levels')
+    for q, U in zip(w['centers'], w['center_frames']):
+        U = span(U)
+        need(current[q] == U, 'centre entry frame', q)
+        served = {levels.get(g[1], ZERO) for g in w['cut'] if g[2] == q}
+        for T in sorted(served, key=lambda m: -dim(m)):
+            need(T & ~U == 0, 'centre descent not nested', q)
+            d = dim(U) - dim(T)
+            if d:
+                bill[d] += 1
+                chain.setdefault(q, []).append((('centre',), d, T))
+            U = T
+    at = {}
+    for k, rec in enumerate(warps, 1):
+        at.setdefault(rec[0], []).append(k)
+    for p in range(len(B) + 1):
+        for k in at.get(p, ()):
+            _, lender, _, U, E = warps[k - 1]
+            need(current[lender] == span(U), 'native warp entry frame', k, lender)
+            current[lender] = span(E)
+            chain.setdefault(lender, []).append((('warp', k), 'warp', span(E)))
+        if p < len(B):
+            for r in touched(B[p]):
+                climb(r, span(B[p][-1]), ('B', p))
+    for i, g in enumerate(w['restore']):
+        for r in touched(g):
+            climb(r, span(g[-1]), ('restore', i))
+    for r in live:
+        climb(r, end[r], ('end',))
+    restored = set(map(int, w['helper_final']))
+    need(all(end[r] == FULL for r in live if r not in restored and not is_target(r)), 'a FULL-cleanup register ends low')
+    widths = Counter(dim(end[r]) - dim(start[r]) for r in live if r >= 2 * V)
+    return dict(sorted(bill.items())), dict(sorted(widths.items())), chain, start, end
+
+
+def hygiene(w):
+    """Inherited structural contract: dyadic scalars, power-of-two scales, wrapper and correction access."""
+    entering = set(map(int, w['start_extra']))
+    restored = set(map(int, w['helper_final']))
+    live = set(range(N)) - set(w['removed'])
+    for name in ('precondition', 'compensation', 'A', 'cut', 'B', 'restore', 'cleanup'):
+        for g in w[name]:
+            if g[0] == 'warp':
+                continue
+            q = Q(g[3], g[4]) if g[0] == 'add' else Q(g[2], g[3])
+            need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'non-dyadic scalar', name, g)
+            if g[0] == 'scale':
+                need(abs(q.numerator) & (abs(q.numerator) - 1) == 0, 'non power-of-two scale', name, g)
+    for g in w['precondition'] + w['compensation']:
+        need(not any(r in entering | restored for r in touched(g)), 'wrapper touches an entering or restored helper', g)
+    for c in w['initial_corrections']:
+        word = c['operator_word']
+        need(is_target(c['target']) and c['source'] in live and c['source'] >= 2 * V
+             and c['source'] not in entering, 'correction access', c)
+        need(word and all(w['warps'][abs(o) - 1][1] == c['source'] for o in word), 'correction operator lender', c)
+        q = Q(c['coefficient'])
+        need(q != 0 and q.denominator & (q.denominator - 1) == 0, 'correction coefficient', c)
+    return True
+
+
+# ----------------------------------------------------------------------------
+# Literal inverse cleanup, derived from the contract
+# ----------------------------------------------------------------------------
+def ordinary_forward(w):
+    """Chronological non-wrapper actions whose inverse forms cleanup."""
+    out = [g for g in w['A'][w['prelude_events']:]]
+    at = {}
+    for k, rec in enumerate(w['warps'], 1):
+        at.setdefault(rec[0], []).append(['warp', rec[1], k])
+    for p in range(len(w['B']) + 1):
+        out += at.get(p, [])
+        if p < len(w['B']):
+            out.append(w['B'][p])
+    return out + list(w['restore'])
+
+
+def derive_cleanup(w):
+    restored = set(map(int, w['helper_final']))
+    buf = lambda r: r + N if r in restored else r
+    full = [256, 128, 64, 32, 16, 8, 4, 2, 1]
+    out = []
+    for g in reversed(ordinary_forward(w)):
+        if g[0] == 'warp':
+            out.append(['warp', buf(g[1]), -g[2], full])
+        elif is_target(g[1]):
+            continue
+        elif g[0] == 'add':
+            out.append(['add', buf(g[1]), buf(g[2]), -g[3], g[4], full])
+        else:
+            need(g[0] == 'scale', 'unknown primitive', g)
+            out.append(['scale', buf(g[1]), g[3], g[2], full])
+    return out
+
+
+def same_cleanup(a, b):
+    norm = lambda c: [(g[:-1], span(g[-1])) for g in c]
+    return len(a) == len(b) and norm(a) == norm(b)
+
+
+# ----------------------------------------------------------------------------
+# Exact free-operator semantics.  A value is a dict {(input, word): Fraction};
+# word is a reduced tuple of signed operator ids (leftmost = applied last).
+# ----------------------------------------------------------------------------
+def program(w, cleanup=None):
+    """Literal executed sequence: corrections, wrapper, A, cut, B+warps, restore | cleanup."""
+    items = [('corr', c['target'], c['source'], tuple(c['operator_word']), Q(c['coefficient']))
+             for c in w['initial_corrections']]
+    items += w['precondition'] + w['compensation'] + w['A'] + w['cut']
+    at = {}
+    for k, rec in enumerate(w['warps'], 1):
+        at.setdefault(rec[0], []).append(['warp', rec[1], k])
+    for p in range(len(w['B']) + 1):
+        items += at.get(p, [])
+        if p < len(w['B']):
+            items.append(w['B'][p])
+    items += w['restore']
+    return items, list(w['cleanup'] if cleanup is None else cleanup)
+
+
+def dual_op(op):
+    return (1 if op > 0 else -1) * (abs(op) + DUAL)
+
+
+def _left(op, word):
+    return word[1:] if word and word[0] == -op else (op,) + word
+
+
+def _right(word, op):
+    return word[:-1] if word and word[-1] == -op else word + (op,)
+
+
+def _axpy(dst, src, q):
+    for key, x in src.items():
+        y = dst.get(key, 0) + q * x
+        if y:
+            dst[key] = y
+        else:
+            dst.pop(key, None)
+
+
+def forward_rows(w, cleanup=None, dual=False, symbolic_buffers=True, snapshot=None):
+    """Schrodinger pass: every register's value as a combination of initial inputs.
+
+    Live inputs are independent symbols.  Private buffers are independent symbols
+    when symbolic_buffers is set (dirty), otherwise zero.  The optional snapshot
+    callback sees the rows at the cleanup boundary.
+    """
+    removed = set(w['removed'])
+    live = [r for r in range(N) if r not in removed]
+    restored = sorted(map(int, w['helper_final']))
+    rows = {r: {(r, ()): Q(1)} for r in live}
+    for c in restored:
+        rows[c + N] = {(c + N, ()): Q(1)} if symbolic_buffers else {}
+    prefix, tail = program(w, cleanup)
+
+    def apply(g):
+        kind = g[0]
+        if kind == 'add':
+            t, s, q = g[1], g[2], Q(g[3], g[4])
+            need(t != s and q, 'add gate', g)
+            if dual:
+                t, s, q = s, t, -q
+            _axpy(rows[t], rows[s], q)
+        elif kind == 'scale':
+            q = Q(g[2], g[3])
+            need(q != 0, 'zero scale', g)
+            if dual:
+                q = 1 / q
+            rows[g[1]] = {k: q * x for k, x in rows[g[1]].items()}
+        elif kind == 'warp':
+            op = dual_op(g[2]) if dual else g[2]
+            rows[g[1]] = {(var, _left(op, word)): x for (var, word), x in rows[g[1]].items()}
+        elif kind == 'corr':
+            _, t, s, word, c = g
+            if dual:
+                src, ops, dst, c = rows[t], [-dual_op(o) for o in word], s, -c
+            else:
+                src, ops, dst = rows[s], list(reversed(word)), t
+            moved = {}
+            for (var, wd), x in src.items():
+                for o in ops:
+                    wd = _left(o, wd)
+                moved[var, wd] = x
+            _axpy(rows[dst], moved, c)
+        else:
+            raise AuditFailure('unknown primitive ' + repr(g))
+
+    for g in prefix:
+        apply(g)
+    if snapshot is not None:
+        snapshot(rows)
+    for g in tail:
+        apply(g)
+    return rows
+
+
+def reverse_columns(w, cleanup=None, upto_cleanup=False):
+    """Heisenberg pull-back: process the forward program backwards.
+
+    cols[s] = {(output, word): coefficient}: the final output register 'output'
+    contains coefficient*word*x_s.  Words grow on the right.  Every live input and
+    every private buffer is an independent symbol.
+    """
+    removed = set(w['removed'])
+    live = [r for r in range(N) if r not in removed]
+    restored = sorted(map(int, w['helper_final']))
+    regs = live + [c + N for c in restored]
+    cols = {r: {(r, ()): Q(1)} for r in regs}
+    prefix, tail = program(w, cleanup)
+    seq = prefix if upto_cleanup else prefix + tail
+    for g in reversed(seq):
+        kind = g[0]
+        if kind == 'add':
+            t, s, q = g[1], g[2], Q(g[3], g[4])
+            need(t != s and q, 'add gate', g)
+            _axpy(cols[s], cols[t], q)
+        elif kind == 'scale':
+            q = Q(g[2], g[3])
+            need(q != 0, 'zero scale', g)
+            cols[g[1]] = {k: q * x for k, x in cols[g[1]].items()}
+        elif kind == 'warp':
+            op = g[2]
+            cols[g[1]] = {(out, _right(word, op)): x for (out, word), x in cols[g[1]].items()}
+        elif kind == 'corr':
+            _, t, s, word, c = g
+            moved = {}
+            for (out, wd), x in cols[t].items():
+                for o in word:
+                    wd = _right(wd, o)
+                moved[out, wd] = x
+            _axpy(cols[s], moved, c)
+        else:
+            raise AuditFailure('unknown primitive ' + repr(g))
+    return cols
+
+
+def transpose(cols):
+    rows = {}
+    for s, col in cols.items():
+        for (r, word), x in col.items():
+            rows.setdefault(r, {})[s, word] = x
+    return rows
+
+
+def endpoint_defects(w, rows, dual=False):
+    """Compare final rows with the contract on the zero-buffer (live-input) domain.
+
+    Returns (bad live registers, dirty buffers, buffer->live leaks, buffer self-map identity).
+    """
+    removed = set(w['removed'])
+    live = [r for r in range(N) if r not in removed]
+    restored = sorted(map(int, w['helper_final']))
+    bad = []
+    for r in live:
+        expect = {(r, ()): Q(1)}
+        if dual and r < V:
+            expect[r + V, ()] = Q(-1)
+        if not dual and is_target(r):
+            expect[r - V, ()] = Q(1)
+        got = {k: x for k, x in rows.get(r, {}).items() if k[0] < N}
+        if got != expect:
+            bad.append(r)
+    dirty = [c for c in restored if any(k[0] < N for k in rows.get(c + N, {}))]
+    leaks = sorted({r for r in live for k in rows.get(r, {}) if k[0] >= N})
+    buffer_identity = all({k: x for k, x in rows.get(c + N, {}).items() if k[0] >= N} == {(c + N, ()): Q(1)}
+                          for c in restored)
+    return bad, dirty, leaks, buffer_identity
+
+
+def boundary_defects(w, rows):
+    """Contract at the cleanup boundary (forward): targets sheared, restored helpers clean and isolated."""
+    restored = set(map(int, w['helper_final']))
+    out = []
+    for t in range(V, 2 * V):
+        if {k: x for k, x in rows[t].items() if k[0] < N} != {(t, ()): Q(1), (t - V, ()): Q(1)}:
+            out.append(('target', t))
+    for c in restored:
+        if rows[c] != {(c, ()): Q(1)}:
+            out.append(('restored', c))
+    for r, row in rows.items():
+        if r < N and r not in restored and any(k[0] in restored for k in row):
+            out.append(('restored input read', r))
+    return out
diff --git a/research/staged544-two-neighbour-invoice/vendor/retiming.py b/research/staged544-two-neighbour-invoice/vendor/retiming.py
new file mode 100644
index 0000000000..c33d7bbcdf
--- /dev/null
+++ b/research/staged544-two-neighbour-invoice/vendor/retiming.py
@@ -0,0 +1,269 @@
+# SPDX-License-Identifier: Apache-2.0
+"""Exact, fixed-neighbour single-ADD retiming relaxation.
+
+Chris R / Clear1nsight, with substantial OpenAI assistance. The BORROW-WORD
+frame contract and scalar-retiming mechanism are credited in README.md.
+This module does not import the retained auditor or a numerical optimiser.
+"""
+from bisect import bisect_left
+from collections import Counter
+from copy import deepcopy
+from fractions import Fraction
+from functools import lru_cache
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+@lru_cache(maxsize=None)
+def span(vectors):
+    points = {0}
+    for v in vectors:
+        need(type(v) is int and 0 <= v < 512, 'invalid frame vector')
+        points |= {x ^ v for x in tuple(points)}
+    return sum(1 << x for x in points)
+
+
+@lru_cache(maxsize=None)
+def basis(mask):
+    answer = []
+    have = 1
+    for v in range(1, 512):
+        if (mask >> v) & 1 and not (have >> v) & 1:
+            answer.append(v)
+            have = span(tuple(answer))
+    need(have == mask, 'not a binary subspace')
+    return tuple(answer)
+
+
+@lru_cache(maxsize=None)
+def join(a, b):
+    return span(basis(a) + basis(b))
+
+
+@lru_cache(maxsize=None)
+def rank(mask):
+    n = mask.bit_count()
+    need(n > 0 and n & (n - 1) == 0, 'invalid subspace cardinality')
+    return n.bit_length() - 1
+
+
+def contained(a, b):
+    return not a & ~b
+
+
+def touched(gate):
+    return gate[1:3] if gate[0] == 'add' else gate[1:2]
+
+
+def tracing(word):
+    """Own chronological trace; centre descent is NOT persistent state.
+
+    A check node is a fixed boundary, not a charged instruction. The census
+    relaxes it to a virtual climb. Every legal witness has zero such charge.
+    """
+    full = (1 << 512) - 1
+    live = set(range(704)) - set(word['removed'])
+    start, end = {}, {}
+    for r in live:
+        if r < 112:
+            start[r], end[r] = span((word['ports'][r],)), full
+        elif r < 224:
+            p = word['ports'][r - 112]
+            start[r] = 1
+            end[r] = sum(1 << x for x in range(512) if (x & p).bit_count() % 2 == 0)
+        else:
+            start[r], end[r] = 1, full
+    for r, fr in word['start_extra'].items():
+        start[int(r)] = span(tuple(fr))
+    for r, fr in word['helper_final'].items():
+        end[int(r)] = span(tuple(fr))
+    current = dict(start)
+    nodes = {r: [] for r in live}
+    where = {}
+    bill = Counter()
+
+    def event(r, frame, address, kind='climb'):
+        before = current[r]
+        if kind != 'map':
+            need(contained(before, frame), 'source frame containment')
+            d = rank(frame) - rank(before)
+            if kind == 'check':
+                need(d == 0, 'source fixed boundary')
+            elif d:
+                bill[d] += 1
+        if kind == 'climb':
+            where[(address, r)] = len(nodes[r])
+        nodes[r].append((address, kind, before, frame))
+        current[r] = frame
+
+    for i, gate in enumerate(word['A']):
+        if gate[0] == 'warp':
+            event(gate[1], span(tuple(gate[3])), ('check-A', i), 'check')
+            event(gate[1], span(tuple(gate[4])), ('map-A', i), 'map')
+        else:
+            for r in touched(gate):
+                event(r, span(tuple(gate[-1])), ('A', i))
+    levels = {112 + int(r): span(tuple(fr)) for r, fr in word['target_levels'].items()}
+    for r in range(112, 224):
+        event(r, levels.get(r, 1), ('target-cut', r), 'check')
+    for r, fr in zip(word['centers'], word['center_frames']):
+        u = span(tuple(fr))
+        event(r, u, ('centre-cut', r), 'check')
+        served = {levels.get(g[1], 1) for g in word['cut'] if g[2] == r}
+        for v in sorted(served, key=lambda x: -rank(x)):
+            need(contained(v, u), 'centre nesting')
+            if rank(u) > rank(v):
+                bill[rank(u) - rank(v)] += 1
+            u = v
+        # The main forward register remains at its declared centre entry.
+    warps = {}
+    for j, rec in enumerate(word['warps']):
+        warps.setdefault(rec[0], []).append((j, rec))
+    for i in range(len(word['B']) + 1):
+        for j, rec in warps.get(i, []):
+            event(rec[1], span(tuple(rec[3])), ('check-B', j), 'check')
+            event(rec[1], span(tuple(rec[4])), ('map-B', j), 'map')
+        if i < len(word['B']):
+            gate = word['B'][i]
+            for r in touched(gate):
+                event(r, span(tuple(gate[-1])), ('B', i))
+    for i, gate in enumerate(word['restore']):
+        for r in touched(gate):
+            event(r, span(tuple(gate[-1])), ('restore', i))
+    for r in live:
+        event(r, end[r], ('end',))
+    return nodes, where, dict(sorted(bill.items()))
+
+
+def crosses(g, h):
+    """Sufficient exact scalar normal form, not all algebraic commutations."""
+    if h[0] == 'add':
+        return g[1] != h[2] and h[1] != g[2]
+    return h[0] == 'scale' and h[2] != 0
+
+
+def segments(word, section):
+    if section == 'A':
+        cuts = [word['prelude_events'], len(word['A'])]
+    elif section == 'B':
+        cuts = sorted({0, len(word['B'])} | {rec[0] for rec in word['warps']})
+    else:
+        cuts = [0, len(word[section])]
+    return list(zip(cuts, cuts[1:]))
+
+
+def caps(delta):
+    return [sum(n * min(r, k) for r, n in enumerate(delta)) for k in range(1, 10)]
+
+
+def all_power_nonnegative(delta):
+    """Sufficient exact certificate using decreasing positive curvatures."""
+    values = caps(delta)
+    prefix = 0
+    for value in values[:-1]:
+        prefix += value
+        if prefix < 0:
+            return False
+    return values[-1] == 0
+
+
+def census(word):
+    nodes, where, bill = tracing(word)
+    deltas = Counter()
+    counts = {}
+    for section in ('A', 'B', 'restore'):
+        gates = word[section]
+        count = 0
+        for lo, hi in segments(word, section):
+            occurrences = {}
+            for i in range(lo, hi):
+                need(gates[i][0] in ('add', 'scale'), 'unexpected scalar segment')
+                for r in touched(gates[i]):
+                    occurrences.setdefault(r, []).append(i)
+            for i in range(lo, hi):
+                g = gates[i]
+                if g[0] != 'add':
+                    continue
+                lower = i
+                while lower > lo and crosses(g, gates[lower - 1]):
+                    lower -= 1
+                upper = i + 1
+                while upper < hi and crosses(g, gates[upper]):
+                    upper += 1
+                removal = [0] * 10
+                reduced, entries, exits = {}, {}, {}
+                for r in touched(g):
+                    seq = nodes[r]
+                    pos = where[((section, i), r)]
+                    _, _, p, u = seq[pos]
+                    need(pos + 1 < len(seq) and seq[pos + 1][1] != 'map', 'missing successor')
+                    q = seq[pos + 1][3]
+                    removal[rank(u) - rank(p)] -= 1
+                    removal[rank(q) - rank(u)] -= 1
+                    removal[rank(q) - rank(p)] += 1
+                    indices = occurrences[r]
+                    reduced[r] = [x for x in indices if x != i]
+                    entries[r] = seq[where[((section, indices[0]), r)]][2]
+                    last = where[((section, indices[-1]), r)]
+                    need(seq[last + 1][1] != 'map', 'missing exit check')
+                    exits[r] = seq[last + 1][3]
+                for cut in range(lower, upper + 1):
+                    if cut == i + 1:  # Same placement as cut i, counted once.
+                        continue
+                    boundaries = []
+                    for r in touched(g):
+                        indices = reduced[r]
+                        j = bisect_left(indices, cut)
+                        p = span(tuple(gates[indices[j - 1]][-1])) if j else entries[r]
+                        q = span(tuple(gates[indices[j]][-1])) if j < len(indices) else exits[r]
+                        boundaries.append((p, q))
+                    lower_frame = join(boundaries[0][0], boundaries[1][0])
+                    upper_frame = boundaries[0][1] & boundaries[1][1]
+                    if not contained(lower_frame, upper_frame):
+                        continue
+                    dims = [(rank(p), rank(q)) for p, q in boundaries]
+                    for d in range(rank(lower_frame), rank(upper_frame) + 1):
+                        delta = removal.copy()
+                        for p, q in dims:
+                            delta[q - p] -= 1
+                            delta[d - p] += 1
+                            delta[q - d] += 1
+                        delta[0] = 0
+                        need(sum(r * n for r, n in enumerate(delta)) == 0, 'rank mass drift')
+                        deltas[tuple(delta)] += 1
+                        count += 1
+        counts[section] = count
+    return {'per_section': counts, 'candidates': sum(counts.values()),
+            'source_profile': bill,
+            'deltas': [{'delta': {r: n for r, n in enumerate(d) if n}, 'count': n,
+                        'caps': caps(d), 'certificate': all_power_nonnegative(d)}
+                       for d, n in sorted(deltas.items())]}
+
+
+def apply_move(word, section, index, cut, frame):
+    """Apply one exact scalar retiming. Caller must rederive cleanup and audit."""
+    need(section in ('A', 'B', 'restore'), 'unknown section')
+    gates = word[section]
+    need(type(index) is int and 0 <= index < len(gates), 'bad source index')
+    need(type(cut) is int and 0 <= cut <= len(gates), 'bad insertion cut')
+    need(any(lo <= index < hi and lo <= cut <= hi for lo, hi in segments(word, section)),
+         'crosses prelude or native warp boundary')
+    g = deepcopy(gates[index])
+    need(g[0] == 'add', 'only ADD moves are covered')
+    crossed = gates[index + 1:cut] if cut > index else gates[cut:index]
+    need(all(crosses(g, h) for h in crossed), 'noncommuting scalar barrier')
+    coefficient = Fraction(g[3], g[4])
+    for h in crossed:
+        if h[0] == 'scale' and h[1] in touched(g):
+            power = (1 if h[1] == g[1] else -1) * (1 if cut > index else -1)
+            coefficient *= Fraction(h[2], h[3]) ** power
+    g[3:5] = [coefficient.numerator, coefficient.denominator]
+    g[-1] = list(basis(span(tuple(frame))))
+    result = deepcopy(word)
+    result[section].pop(index)
+    result[section].insert(cut - (cut > index), g)
+    # Segment length and all warp cuts are unchanged. No warp is crossed.
+    return result
diff --git a/research/staged544-two-neighbour-invoice/verify.py b/research/staged544-two-neighbour-invoice/verify.py
new file mode 100644
index 0000000000..814daa043b
--- /dev/null
+++ b/research/staged544-two-neighbour-invoice/verify.py
@@ -0,0 +1,262 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Long first-ADD retiming invoices on the two pinned staged544 providers.
+
+The first-move price depends only on dimension. Every legal cut that crosses
+at least two scalar neighbours is certified nonnegative for every feasible
+common-frame dimension. One changed-frame witness is then continued through
+every single-ADD retiming of the edited word.
+"""
+import gzip
+import hashlib
+import json
+from importlib.machinery import SourceFileLoader
+from pathlib import Path
+
+P = Path(__file__).resolve().parent
+HASHES = {
+    "vendor/retiming.py": "591d7278541ac4de9e9b6fc1e17aba23b205ac4b6c81824a28fc08294658ef0d",
+    "vendor/audit_core.py": "888679ca8502cdcb100420fe5382a052529a494bf76cb332928b86e62612b951",
+    "inputs/BORROW-WORD-43base.json.gz": "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699",
+    "inputs/BORROW-WORD-43extra.json.gz": "965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e",
+}
+WITNESS = {
+    "provider": "base",
+    "section": "A",
+    "index": 595,
+    "cut": 1214,
+    "frame": [85],
+    "gate_head": ["add", 459, 510, -1, 1],
+    "original_frame": [],
+    "crossed": 618,
+    "first_delta": [0, 3, 0, -1, 0, 0, 0, 0, 0, 0],
+    "first_caps": [2, 1, 0, 0, 0, 0, 0, 0, 0],
+    "second_candidates": 1767681,
+    "edited_profile": {1: 2443, 2: 725, 3: 223, 4: 102, 5: 20, 8: 8},
+    "original_profile": {1: 2440, 2: 725, 3: 224, 4: 102, 5: 20, 8: 8},
+}
+# Dimension-complete long-first censuses. Locked after the source-bound run.
+EXPECTED = {
+    "base": {"adds": 5501, "long_gates": 4979, "cases": 1761760, "nonzero": 239103, "neutral": 1522657, "improving": 0},
+    "extra": {"adds": 5501, "long_gates": 4979, "cases": 1761760, "nonzero": 239103, "neutral": 1522657, "improving": 0},
+}
+
+
+def need(ok, message):
+    if not ok:
+        raise SystemExit(message)
+
+
+def load(name, path):
+    return SourceFileLoader(name, str(path)).load_module()
+
+
+def authenticate():
+    for rel, digest in HASHES.items():
+        raw = (P / rel).read_bytes()
+        need(hashlib.sha256(raw).hexdigest() == digest, "sha256 mismatch: " + rel)
+
+
+def load_word(tag):
+    return json.loads(gzip.decompress((P / "inputs" / f"BORROW-WORD-43{tag}.json.gz").read_bytes()))
+
+
+def segment_bounds(R, word, section, index):
+    for lo, hi in R.segments(word, section):
+        if lo <= index < hi:
+            return lo, hi
+    raise SystemExit("index outside every segment")
+
+
+def long_cuts(R, gates, lo, hi, index):
+    gate = gates[index]
+    lower, upper = index, index + 1
+    while lower > lo and R.crosses(gate, gates[lower - 1]):
+        lower -= 1
+    while upper < hi and R.crosses(gate, gates[upper]):
+        upper += 1
+    cuts = []
+    for cut in range(lower, upper + 1):
+        if cut == index + 1:
+            continue
+        crossed = gates[index + 1:cut] if cut > index else gates[cut:index]
+        if len(crossed) >= 2:
+            cuts.append(cut)
+    return cuts
+
+
+def removal_histogram(R, word, nodes, where, section, index):
+    gate = word[section][index]
+    delta = [0] * 10
+    for register in R.touched(gate):
+        seq = nodes[register]
+        pos = where[((section, index), register)]
+        _, _, before, frame = seq[pos]
+        need(seq[pos + 1][1] != "map", "missing successor")
+        after = seq[pos + 1][3]
+        delta[R.rank(frame) - R.rank(before)] -= 1
+        delta[R.rank(after) - R.rank(frame)] -= 1
+        delta[R.rank(after) - R.rank(before)] += 1
+    return delta
+
+
+def cut_bounds(R, gates, occurrences, entries, exits, index, cut):
+    bounds = []
+    for register in R.touched(gates[index]):
+        indices = [x for x in occurrences[register] if x != index]
+        j = 0
+        while j < len(indices) and indices[j] < cut:
+            j += 1
+        before = R.span(tuple(gates[indices[j - 1]][-1])) if j else entries[register]
+        after = R.span(tuple(gates[indices[j]][-1])) if j < len(indices) else exits[register]
+        bounds.append((before, after))
+    low = R.join(bounds[0][0], bounds[1][0])
+    high = bounds[0][1] & bounds[1][1]
+    return low, high, bounds
+
+
+def insertion_delta(removal, dims, dimension):
+    delta = removal.copy()
+    for before, after in dims:
+        delta[after - before] -= 1
+        delta[dimension - before] += 1
+        delta[after - dimension] += 1
+    delta[0] = 0
+    return delta
+
+
+def long_first_census(R, word):
+    nodes, where, traced = R.tracing(word)
+    counts = {"adds": 0, "long_gates": 0, "cases": 0, "nonzero": 0, "neutral": 0, "improving": 0}
+    for section in ("A", "B", "restore"):
+        gates = word[section]
+        for lo, hi in R.segments(word, section):
+            occurrences = {}
+            for index in range(lo, hi):
+                for register in R.touched(gates[index]):
+                    occurrences.setdefault(register, []).append(index)
+            entries, exits = {}, {}
+            for register, indices in occurrences.items():
+                entries[register] = nodes[register][where[((section, indices[0]), register)]][2]
+                last = where[((section, indices[-1]), register)]
+                need(nodes[register][last + 1][1] != "map", "missing exit")
+                exits[register] = nodes[register][last + 1][3]
+            for index in range(lo, hi):
+                if gates[index][0] != "add":
+                    continue
+                counts["adds"] += 1
+                cuts = long_cuts(R, gates, lo, hi, index)
+                if not cuts:
+                    continue
+                counts["long_gates"] += 1
+                removal = removal_histogram(R, word, nodes, where, section, index)
+                for cut in cuts:
+                    low, high, bounds = cut_bounds(R, gates, occurrences, entries, exits, index, cut)
+                    if not R.contained(low, high):
+                        continue
+                    dims = [(R.rank(before), R.rank(after)) for before, after in bounds]
+                    for dimension in range(R.rank(low), R.rank(high) + 1):
+                        delta = insertion_delta(removal, dims, dimension)
+                        need(sum(rank * count for rank, count in enumerate(delta)) == 0, "rank mass drift")
+                        counts["cases"] += 1
+                        if any(delta):
+                            counts["nonzero"] += 1
+                        else:
+                            counts["neutral"] += 1
+                        if not R.all_power_nonnegative(delta):
+                            counts["improving"] += 1
+    need(traced == {int(rank): count for rank, count in word["report"]["local_profile"].items()}
+         or traced == word["report"]["local_profile"], "trace/profile disagreement")
+    # local_profile keys may already be ints
+    profile = {int(rank): count for rank, count in word["report"]["local_profile"].items()}
+    need(traced == profile, "trace bill differs from declared profile")
+    return counts, nodes, where
+
+
+def witness_invoice(R, C, word):
+    section = WITNESS["section"]
+    index = WITNESS["index"]
+    cut = WITNESS["cut"]
+    gates = word[section]
+    gate = gates[index]
+    need(gate[:5] == WITNESS["gate_head"], "witness gate changed")
+    need(gate[-1] == WITNESS["original_frame"], "witness original frame changed")
+    crossed = gates[index + 1:cut]
+    need(len(crossed) == WITNESS["crossed"], "witness crossing length changed")
+    need(any(item[0] == "add" for item in crossed) and any(item[0] == "scale" for item in crossed),
+         "witness must cross both an ADD and a SCALE")
+    nodes, where, _ = R.tracing(word)
+    lo, hi = segment_bounds(R, word, section, index)
+    occurrences = {}
+    for cursor in range(lo, hi):
+        for register in R.touched(gates[cursor]):
+            occurrences.setdefault(register, []).append(cursor)
+    entries, exits = {}, {}
+    for register, indices in occurrences.items():
+        entries[register] = nodes[register][where[((section, indices[0]), register)]][2]
+        last = where[((section, indices[-1]), register)]
+        exits[register] = nodes[register][last + 1][3]
+    low, high, bounds = cut_bounds(R, gates, occurrences, entries, exits, index, cut)
+    need(R.contained(low, high), "witness interval empty")
+    need(R.basis(high) == tuple(WITNESS["frame"]), "witness frame is not the unique upper line")
+    need(not R.contained(R.span((1,)), high), "control vector 1 must lie outside the witness line")
+    dims = [(R.rank(before), R.rank(after)) for before, after in bounds]
+    removal = removal_histogram(R, word, nodes, where, section, index)
+    delta = insertion_delta(removal, dims, 1)
+    need(delta == WITNESS["first_delta"], "witness first delta changed: " + str(delta))
+    need(R.caps(delta) == WITNESS["first_caps"], "witness caps changed")
+    need(R.all_power_nonnegative(delta), "witness first move lost its certificate")
+    edited = R.apply_move(word, section, index, cut, WITNESS["frame"])
+    C.hygiene(edited)
+    edited["cleanup"] = C.derive_cleanup(edited)
+    C.hygiene(edited)
+    original_bill, _widths, *_rest = C.frame_bill(word)
+    edited_bill, _widths, *_rest = C.frame_bill(edited)
+    need(original_bill == WITNESS["original_profile"], "original frame bill changed")
+    need(edited_bill == WITNESS["edited_profile"], "edited frame bill changed")
+    traced = R.tracing(edited)[2]
+    need(traced == edited_bill, "edited trace disagrees with frame bill")
+    second = R.census(edited)
+    need(second["candidates"] == WITNESS["second_candidates"], "second-move count changed")
+    first = WITNESS["first_delta"]
+    for row in second["deltas"]:
+        combined = first.copy()
+        for rank, count in row["delta"].items():
+            combined[int(rank)] += count
+        need(sum(rank * count for rank, count in enumerate(combined)) == 0, "combined rank mass")
+        need(R.all_power_nonnegative(combined), "combined continuation improves: " + str(combined))
+    return second["candidates"]
+
+
+def failure_controls(R):
+    losing = [0, -1, 0, 0, 0, 0, 0, 0, 0, 0]
+    need(not R.all_power_nonnegative(losing), "negative control was certified")
+    neutral = [0] * 10
+    need(R.all_power_nonnegative(neutral), "zero delta must be neutral")
+    need(R.rank(R.span(())) == 0, "empty frame rank")
+
+
+def main():
+    authenticate()
+    R = load("staged544_retiming", P / "vendor" / "retiming.py")
+    C = load("staged544_audit_core", P / "vendor" / "audit_core.py")
+    failure_controls(R)
+    summary = {}
+    for tag in ("base", "extra"):
+        word = load_word(tag)
+        counts, _nodes, _where = long_first_census(R, word)
+        need(counts["improving"] == 0, tag + " has an improving long first move")
+        need(counts["cases"] == counts["nonzero"] + counts["neutral"], tag + " case split")
+        expected = EXPECTED[tag]
+        if expected is not None:
+            need(counts == expected, tag + " counts changed: " + str(counts))
+        summary[tag] = counts
+        if tag == WITNESS["provider"]:
+            witness_invoice(R, C, word)
+    print("PASS_STAGED544_TWO_NEIGHBOUR_INVOICE "
+          + " ".join(f"{tag}_cases={summary[tag]['cases']}" for tag in summary)
+          + f" witness_second={WITNESS['second_candidates']} improving=0 no_new_kappa")
+
+
+if __name__ == "__main__":
+    main()