diff --git a/research/compact-switch-sharp-two-target/README.md b/research/compact-switch-sharp-two-target/README.md
new file mode 100644
index 0000000000..49285fa257
--- /dev/null
+++ b/research/compact-switch-sharp-two-target/README.md
@@ -0,0 +1,85 @@
+# Sharp-window two-target macro
+
+**Scoped finite check. No new κ.** The selected conditional exponent stays
+60403/20000000. This does not accept PR #4100.
+
+## Result
+
+CRT.md §4 restores every good address at once when the guard windows lie
+in the published margin `2B ≤ W < 2^m − 2B` and the `K`-bit blocks are
+disjoint. The isolated post-increment step also holds on the larger range
+`0 ≤ W ≤ 2^m − B + 1`. PR #4646 substituted that range into the density
+term and left the two-target macro itself open on the extra windows.
+
+The live macro is two post-increment steps with a load of `f` between
+them and an unload after. Positions are `(0, K)` with `K = m + 1`, so
+each window occupies the `m` bits above its target and stops before the
+other target. Digits of both control words stay in `0, ..., B − 2`.
+Sources are constant bits, or, in one family, bits inside the restored
+windows. They do not read either target bit.
+
+On these inputs both control words return to their start, and the data
+word ends as the XOR of the two source bits into the two target positions.
+The tested edges `W = 0` and `W = 2^m − B + 1` sit outside the published
+margin.
+
+| Row | Edges | Restorations |
+| --- | --- | --- |
+| `B = 4`, `m = 5`, `K = 6`, the two edges chosen independently | `0` and `29` | 5,184 |
+| `B = 2`, `m = 5`, `K = 6`, both targets on the same edge | `0` and `31` | 32 |
+| `B = 8`, `m = 6`, `K = 7`, both targets on the same edge | `0` and `57` | 76,832 |
+| `B = 4`, `m = 5`, source reads window bits 3 and `K + 2` | both targets on `0`, and both on `29` | 648 |
+
+One step past the sharp edge does not restore the switch digit. With
+`B = 4`, `m = 5`, first window `W = 30`, second window `0`, and
+`(u, t, y) = (1, 2, 60)`, the macro ends at `(1, 10, 60)` rather than
+`(1, 2, 60)`. A source that reads the two target bits on `(1, 0, 0)`
+ends at `(1, 0, 1)`. The overlapping positions `(0, 1)` on
+`(u, t, y) = (0, 1, 80)` still end at `(0, 5, 81)` rather than
+`(0, 1, 81)`.
+
+## Scope
+
+Card `formal-interface-lemma`, scope **refined**. This is the first open
+question of the sharp-density comparison, PR #4646. The live-digit
+identity and the published-margin pair sweep are PR #4321. This package
+does not repeat that sweep.
+
+The check is finite. It does not prove the macro for every base and every
+placement, and it does not move CRT.md's simultaneous argument off the
+`2B` margin. The twelve paid `H`-bit exchanges, the reservoir shuttle, and
+the tape repair are not replayed. No Lean proof and no multiplication
+theorem are claimed.
+
+Canonical main fetched 2026-10-22T23:23:25Z at
+`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B research/compact-switch-sharp-two-target/verify.py
+python3.12 -B scripts/research_package.py --package research/compact-switch-sharp-two-target
+```
+
+The direct command prints `PASS_COMPACT_SWITCH_SHARP_TWO_TARGET`.
+
+## Open next questions
+
+1. Is `L ≤ p` true for a real #4174 placement, or only a sufficient
+   hypothesis inherited from #4328? The constant `1/6400` in the
+   sharp-density comparison uses that hypothesis. First step: read one
+   production plan's address length against its `p`. Blocker: reservoir
+   placement is not an input here.
+
+## Credit
+
+Cinna Davis, PR #4100, for CRT.md. The live-digit lemma, the sharp window,
+and the published-margin pair sweep are PR #4321. The density comparison
+that left this macro open is PR #4646. The published density identity and
+the `L ≤ p` hypothesis are PR #4328.
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance.
+Apache-2.0. No independent human review and no formal-kernel acceptance
+are claimed.
diff --git a/research/compact-switch-sharp-two-target/SOURCES.json b/research/compact-switch-sharp-two-target/SOURCES.json
new file mode 100644
index 0000000000..95b2d7afb1
--- /dev/null
+++ b/research/compact-switch-sharp-two-target/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/unconditional-batched-crt/CRT.md",
+      "usage": "input",
+      "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6",
+      "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b"
+    }
+  ]
+}
diff --git a/research/compact-switch-sharp-two-target/TASK.json b/research/compact-switch-sharp-two-target/TASK.json
new file mode 100644
index 0000000000..cea8fdcabb
--- /dev/null
+++ b/research/compact-switch-sharp-two-target/TASK.json
@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Run the live two-target compact-switch macro at the sharp window edges W=0 and W=2^m-B+1 on one pair of K-separated positions, and record whether both control words return.",
+  "scope_change_reason": "PR #4646 compared the sharp-window density with CRT.md's repair room and left the two-target macro on windows outside the published 2B margin open. The successive sixteenth walks are closed. This package runs that named macro. It does not formalize the lemma in a proof assistant, does not accept the all-size repair, and does not claim a new kappa.",
+  "bottleneck_link": "PR #4100's simultaneous carry argument still assumes the stricter 2B margin. These finite restorations say the live macro also returns both control words on the two sharp edges for the tested guards. The selected frontier is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the named edge windows, the three parameter rows, and the three failure controls. Do not replay the twelve paid H-bit exchanges, the tape repair, or Lean.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/compact-switch-sharp-two-target",
+  "author": "James Reed",
+  "ai_assistance": "Substantial assistance from Cursor Grok 4.7.",
+  "open_questions": [
+    {
+      "question": "Is L <= p true for a real #4174 placement, or only a sufficient hypothesis inherited from #4328?",
+      "why_it_matters": "The constant 1/6400 in the sharp-density comparison uses L <= p. A larger address length needs its own constant.",
+      "first_step": "Read one production plan's address length against its p.",
+      "blocked_by": "Reservoir placement is not an input to this package."
+    }
+  ]
+}
diff --git a/research/compact-switch-sharp-two-target/VERIFY.json b/research/compact-switch-sharp-two-target/VERIFY.json
new file mode 100644
index 0000000000..3c2bc4e6d1
--- /dev/null
+++ b/research/compact-switch-sharp-two-target/VERIFY.json
@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/unconditional-batched-crt/CRT.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Live two-target macro at W=0 and W=2^m-B+1 on K-separated positions restores both control words for B=4,m=5 (independent edges), B=2,m=5 and B=8,m=6 (matched edges), including window-bit sources on B=4. Failure controls reject one past-sharp window, a target-reading source, and overlapping positions (0, 1)."
+    }
+  ]
+}
diff --git a/research/compact-switch-sharp-two-target/verify.py b/research/compact-switch-sharp-two-target/verify.py
new file mode 100644
index 0000000000..7b8427782b
--- /dev/null
+++ b/research/compact-switch-sharp-two-target/verify.py
@@ -0,0 +1,207 @@
+#!/usr/bin/env python3
+"""Live two-target compact switch on the sharp window edges.
+
+CRT.md's simultaneous argument assumes the published 2B margin. PR #4646
+left open whether one K-separated pair still restores both control words
+on a window that is sharp-good and outside that margin. This verifier runs
+that macro at W=0 and at W=2^m-B+1. It does not replay the twelve paid
+H-bit exchanges, and it claims no new kappa.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = ROOT / "research" / "compact-switch-sharp-two-target"
+
+PHRASES = (
+    "y additions then have total z(1-2b)2^j",
+    "2B margins keep every intermediate carry inside its own guard interval",
+    "Color targets by current position modulo K, so guard intervals are disjoint.",
+    "r [2/B + 8B/2^K] <= C p 2^-G.",
+)
+
+
+def need(condition: bool, message: str) -> None:
+    if not condition:
+        raise SystemExit("FAIL: " + message)
+
+
+def pins_and_phrases() -> None:
+    sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8"))
+    for row in sources["files"]:
+        if row["usage"] == "input":
+            digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest()
+            need(digest == row["sha256"], row["path"])
+    crt = (ROOT / "research/unconditional-batched-crt/CRT.md").read_text(encoding="utf-8")
+    for phrase in PHRASES:
+        need(phrase in crt, phrase)
+    selected = json.loads(
+        (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")
+    )
+    need(selected["kappa"] == "60403/20000000", "selected kappa")
+
+
+def live_macro(u: int, t: int, y: int, sources, bits: int, positions: tuple[int, int]):
+    """Two live-digit steps with a load of f between them and an unload after."""
+    base = 1 << bits
+    count = len(positions)
+
+    def one_f(u0: int, t0: int, y0: int):
+        parity = [(u0 >> (bits * i)) & 1 for i in range(count)]
+        digits = [(t0 >> (bits * i)) & (base - 1) for i in range(count)]
+        y1 = y0
+        for i in range(count):
+            y1 += 2 * parity[i] * digits[i] * (1 << positions[i])
+        t1 = t0
+        for i in range(count):
+            t1 += ((y1 >> positions[i]) & 1) << (bits * i)
+        live = [(t1 >> (bits * i)) & (base - 1) for i in range(count)]
+        y2 = y1
+        for i in range(count):
+            y2 += parity[i] * (1 - 2 * live[i]) * (1 << positions[i])
+        t2 = t1
+        for i in range(count):
+            t2 -= (((y2 >> positions[i]) & 1) ^ parity[i]) << (bits * i)
+        return u0, t2, y2
+
+    u, t, y = one_f(u, t, y)
+    loaded = sources(y)
+    for i, value in enumerate(loaded):
+        u += value << (bits * i)
+    u, t, y = one_f(u, t, y)
+    unloaded = sources(y)
+    for i, value in enumerate(unloaded):
+        u -= value << (bits * i)
+    return u, t, y
+
+
+def ideal_y(y: int, values: tuple[int, int], positions: tuple[int, int]) -> int:
+    for value, pos in zip(values, positions):
+        y ^= value << pos
+    return y
+
+
+def pack(b0: int, w0: int, b1: int, w1: int, gap: int) -> int:
+    return b0 + (w0 << 1) + (b1 << gap) + (w1 << (gap + 1))
+
+
+def edge_pair(bits: int, width: int, independent: bool) -> int:
+    """Both targets sit on a sharp edge outside the published 2B margin."""
+    base = 1 << bits
+    limit = 1 << width
+    gap = width + 1
+    upper = limit - base + 1
+    published_hi = limit - 2 * base
+    for window in (0, upper):
+        need(not (2 * base <= window < published_hi), "edge is outside the published margin")
+        need(0 <= window <= upper, "edge is sharp-good")
+    positions = (0, gap)
+    passes = 0
+    windows = ((0, 0), (upper, upper))
+    if independent:
+        windows = ((0, 0), (0, upper), (upper, 0), (upper, upper))
+    legal = range(base - 1)
+    for w0, w1 in windows:
+        for b0 in (0, 1):
+            for b1 in (0, 1):
+                for s0 in (0, 1):
+                    for s1 in (0, 1):
+                        values = (s0, s1)
+                        source = lambda word, values=values: values
+                        for d0 in legal:
+                            for d1 in legal:
+                                for e0 in legal:
+                                    for e1 in legal:
+                                        y = pack(b0, w0, b1, w1, gap)
+                                        u = e0 + (e1 << bits)
+                                        t = d0 + (d1 << bits)
+                                        end = live_macro(u, t, y, source, bits, positions)
+                                        need(end == (u, t, ideal_y(y, values, positions)),
+                                             "sharp edge restores both controls")
+                                        passes += 1
+    return passes
+
+
+def window_sources() -> int:
+    """A source may read a restored window bit. It must not read a target."""
+    bits = 2
+    width = 5
+    base = 1 << bits
+    gap = width + 1
+    upper = (1 << width) - base + 1
+    positions = (0, gap)
+    passes = 0
+
+    def source(word: int) -> tuple[int, int]:
+        return (word >> 3) & 1, (word >> (gap + 2)) & 1
+
+    for window in (0, upper):
+        for b0 in (0, 1):
+            for b1 in (0, 1):
+                for d0 in range(base - 1):
+                    for d1 in range(base - 1):
+                        for e0 in range(base - 1):
+                            for e1 in range(base - 1):
+                                y = pack(b0, window, b1, window, gap)
+                                u = e0 + (e1 << bits)
+                                t = d0 + (d1 << bits)
+                                values = source(y)
+                                end = live_macro(u, t, y, source, bits, positions)
+                                need(end == (u, t, ideal_y(y, values, positions)),
+                                     "window-bit source restores both controls")
+                                passes += 1
+    return passes
+
+
+def failure_controls() -> None:
+    bits = 2
+    width = 5
+    base = 1 << bits
+    gap = width + 1
+    positions = (0, gap)
+    # One past the sharp upper edge. The first window spills onto the next target.
+    spilled = (1 << width) - (base - 2)
+    y = pack(0, spilled, 0, 0, gap)
+    need(y == 60, "past-sharp witness address")
+    end = live_macro(1, 2, y, lambda word: (0, 0), bits, positions)
+    need(end == (1, 10, 60), "past-sharp window does not restore t")
+    need(end != (1, 2, ideal_y(y, (0, 0), positions)), "past-sharp witness is not ideal")
+
+    def reads_targets(word: int) -> tuple[int, int]:
+        return word & 1, (word >> gap) & 1
+
+    leaked = live_macro(1, 0, 0, reads_targets, bits, positions)
+    need(leaked == (1, 0, 1), "target-reading source changes y")
+    need(leaked != (1, 0, 0), "target-reading source is not the ideal switch")
+
+    # The published overlapping pair. Each window meets the 2B margin; t does not return.
+    overlap_positions = (0, 1)
+
+    def overlap_source(word: int) -> tuple[int, int]:
+        return (word >> 4) & 1, (word >> 5) & 1
+
+    overlap = live_macro(0, 1, 80, overlap_source, bits, overlap_positions)
+    need(overlap == (0, 5, 81), "overlapping targets do not restore t")
+    need(overlap != (0, 1, 81), "overlap witness is not the ideal switch")
+
+
+def main() -> None:
+    pins_and_phrases()
+    b4 = edge_pair(2, 5, True)
+    b2 = edge_pair(1, 5, False)
+    b8 = edge_pair(3, 6, False)
+    windows = window_sources()
+    failure_controls()
+    need(b4 == 5184 and b2 == 32 and b8 == 76832 and windows == 648, "unexpected counts")
+    print(
+        "PASS_COMPACT_SWITCH_SHARP_TWO_TARGET "
+        f"b4_m5={b4} b2_m5={b2} b8_m6={b8} window_sources={windows}"
+    )
+
+
+if __name__ == "__main__":
+    main()