diff --git a/.gitignore b/.gitignore
index 4080d07..8859dd2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 /.lake/
+/_build/
diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc
index 8b45cdf..e61c360 100644
--- a/ARCHITECTURE.adoc
+++ b/ARCHITECTURE.adoc
@@ -9,6 +9,10 @@ exists, per the estate Required Files gate (substance over presence).
 * `.machine_readable/` — .machine_readable — repository component
 * `LICENSES/` — LICENSES — repository component
 * `Marches/` — Marches — repository component
+* `docs/` — design notes; `kcut-correspondence.adoc` pairs Lean and Agda
+  names (a table, not a link)
+* `scripts/` — shell glue: `fetch-siblings.sh` (pinned sibling clones
+  into `_build/dependencies`, git-ignored) and `check-correspondence.sh`
 
 == Data flow
 
diff --git a/FALSIFIERS.adoc b/FALSIFIERS.adoc
index 12aa737..e079dd3 100644
--- a/FALSIFIERS.adoc
+++ b/FALSIFIERS.adoc
@@ -49,4 +49,19 @@ kernel theorems get applied where they do not hold.
 never silently discharged. The hypothesis itself remains ASSUMED
 about real topologies, as in Gao–Rexford 2001.
 |held
+
+|F6
+|The K-CUT correspondence is nominal: Lean's cut and Agda's cut disagree
+on what `Consistent` means, so the paired names share words, not content.
+|`docs/kcut-correspondence.adoc` pairs the names; every pairing is ASSUMED
+(port-and-reprove). `scripts/check-correspondence.sh` checks that every
+cited name exists at its pin (negative control: fabricated names
+refused). It cannot check meaning. Read at choreographic-types `edb784a`
+(2026-10-14), the falsifier already FIRES on one proposed row: Agda's
+`Consistent p c` is a party-indexed merge condition at choices, while
+marches has no parties, and its cut condition (downward closure,
+`Cut.closed`) is what Agda's `Cut` has by construction. The
+`Acyclic ↔ Consistent` pairing is withdrawn (KC-3). The rest stand
+ASSUMED until a port re-proves them.
+|open (narrowed)
 |===
diff --git a/LIMITATIONS.adoc b/LIMITATIONS.adoc
index 717ee07..9c2d0c1 100644
--- a/LIMITATIONS.adoc
+++ b/LIMITATIONS.adoc
@@ -68,6 +68,11 @@ violations are underivable, not a property checked afterwards.
   (`Marches.Acyclic`) — `gr_loop_free` is conditional on it, and
   loop-freedom of the typed judgment is *not* protocol convergence
   (agda-routing's ground).
+* The K-CUT correspondence (rung 3, `docs/kcut-correspondence.adoc`)
+  pairs marches' Lean names with choreographic-types' Agda names. It is
+  a table, not a link: every pairing is ASSUMED (port-and-reprove), and
+  only name existence is checked mechanically. Falsifier F6 has already
+  withdrawn the proposed `Acyclic ↔ Consistent` pairing.
 * The region DAG (rung 2, `DiscSys.compose`) consumes the SAME
   `Marches.Acyclic` as the GR hierarchy: an acyclic region DAG is an
   ASSUMED property of a deployment, never proven here. Composite
diff --git a/Marches/Tropical.lean b/Marches/Tropical.lean
index d16851e..5ad5b74 100644
--- a/Marches/Tropical.lean
+++ b/Marches/Tropical.lean
@@ -6,10 +6,17 @@
   extension adds weight + 1 (positive weights ⇒ strictness).
 
   This file is the seam for integrating the estate's existing
-  fully proved tropical work (TropicalAdapterPath.lean in
-  tropical-resource-typing). Status of that integration: OPEN
-  (rung 3 in ROADMAP.adoc). Nothing here fabricates or depends on
-  that file's contents.
+  fully proved tropical work. Read 2026-10-14: `TropicalAdapterPath.lean`
+  lives in hyperpolymath/tropical-types (whose lake package is named
+  `tropical-resource-typing`) at e172f8a, on Lean v4.13.0. Status of the
+  import: OPEN (rung 3 in ROADMAP.adoc). Nothing here fabricates or
+  depends on that file's contents.
+
+  The cross-prover bridge is resource-algebra's M-2 (pinned at cf9235c):
+  Agda `MaxPlus` vs tropical-types' Lean `CommSemiring Tropical`, OPEN,
+  port-and-reprove, with no mechanical link. `TropicalNat` below is
+  min-plus, not max-plus, so it is not one of M-2's two objects; see
+  docs/kcut-correspondence.adoc (KC-7, KC-8).
 -/
 
 import Marches.Basic
diff --git a/README.adoc b/README.adoc
index 469d5ef..3e6506e 100644
--- a/README.adoc
+++ b/README.adoc
@@ -147,6 +147,13 @@ order
 |`Tropical.TropicalGrade.seq_unitl`, `alt_idem`, `better_reverses_altLe`,
 `altLe_one`, `s3_witness`
 
+|marches' cuts and grade laws correspond to choreographic-types' K-CUT
+(`proj-cut`, `cut-projectable`, K-4)
+|ASSUMED (port-and-reprove)
+|`docs/kcut-correspondence.adoc`. A table of names, not a link. Names are
+checked at their pins by `scripts/check-correspondence.sh`. Falsifier F6
+is open and has already withdrawn one proposed pairing.
+
 |Tropical estate integration (`TropicalAdapterPath.lean`)
 |OPEN
 |rung 3
@@ -170,6 +177,11 @@ lake build
 
 Zero dependencies; no mathlib. CI runs the same build.
 
+`scripts/check-correspondence.sh` fetches the sibling proof repositories
+at their pinned commits (into `_build/dependencies`). It checks that every
+name `docs/kcut-correspondence.adoc` cites exists, and it needs network
+access.
+
 == Module map
 
 * `Marches/Basic.lean` — path algebras, strict/non-strict inflation, `run`.
diff --git a/ROADMAP.adoc b/ROADMAP.adoc
index 849c6c1..07ea5c3 100644
--- a/ROADMAP.adoc
+++ b/ROADMAP.adoc
@@ -31,13 +31,54 @@ prints the period-2 cycle. All met 2026-07-07.
 * `Interface.strict` DELETED — rung 2 confirmed crossing-map
   order-preservation is never load-bearing. Met 2026-07-07.
 
-== Rung 3 — tropical/estate integration
+== Rung 3 — tropical/estate integration (OPEN)
 
-* Import the estate's fully proved `TropicalAdapterPath.lean`
-  (tropical-resource-typing) behind the `Marches/Tropical.lean` seam.
-  Do NOT paraphrase it; vendor or depend on it.
-* Path provenance as graded accumulation (echo-types bridge): what a
-  trace *carries* across an interface, not just where it may go.
+Each item is marked by its gate, not by prose. The rung is DONE when every
+row's gate passes. Shared gates for Lean rows: `lake build` green,
+`grep -rnw sorry Marches/ Marches.lean` empty, `#eval orbit` unchanged.
+
+[cols="3,3,3,1",options="header"]
+|===
+|Item |Artefact |Gate |Status
+
+|3a. A region crossing is a cut (MRC-01): every crossing crosses a cut;
+no re-entry; `compose` restricted to a cut prefix is a discipline
+|`Marches/Cut.lean`
+|shared Lean gates; `#print axioms` on the new declarations reports none
+|met 2026-10-14
+
+|3b. The grade at the crossing: the two K-4 laws over `TropicalNat`; S-3
+direction recorded
+|`Marches/Tropical.lean` (`TropicalGrade`)
+|shared Lean gates
+|met 2026-10-14
+
+|3c. K-CUT correspondence as a table of names (rows ASSUMED, M-2 idiom);
+falsifier F6 added
+|`docs/kcut-correspondence.adoc`, `FALSIFIERS.adoc` F6
+|`scripts/check-correspondence.sh` prints PASS, and both negative controls
+are refused
+|met 2026-10-14 (names only; F6 open)
+
+|3d. Import the estate's fully proved `TropicalAdapterPath.lean` behind
+the `Marches/Tropical.lean` seam. Do NOT paraphrase it; vendor or depend
+on it. It lives in hyperpolymath/tropical-types (lake package
+`tropical-resource-typing`) at `e172f8a`, on Lean v4.13.0.
+|—
+|it builds inside this repo on the pinned toolchain, unparaphrased
+|OPEN
+
+|3e. Path provenance as graded accumulation (echo-types bridge): what a
+trace *carries* across an interface, not just where it may go.
+|—
+|—
+|OPEN
+
+|3f. postern consumes `no_back_cross` (cross-issue)
+|import plan in `docs/kcut-correspondence.adoc`
+|issue filed on postern
+|OPEN — postern not reachable 2026-10-14
+|===
 
 == Rung 4 — attestation (A2ML bridge)
 
diff --git a/STATE.adoc b/STATE.adoc
index 5a18bb3..d93b08a 100644
--- a/STATE.adoc
+++ b/STATE.adoc
@@ -1,5 +1,69 @@
 = STATE — cross-session log
 
+== 2026-10-14 — rung 3, items 3a–3c: a region crossing is a cut (Claude Code session, MRC-01)
+
+* `Marches/Cut.lean` (3a). A cut is a predecessor-closed set of regions.
+  - `Cut.edge_crosses_past`: in an acyclic graph every edge leaves the
+    principal cut of its source.
+  - `Cut.path_back_crosses_no_cut`: an edge on a cycle crosses no cut, so
+    `Acyclic` is load-bearing.
+  - `DiscSys.trace_cross_crosses_cut`: every crossing in a well-typed trace
+    crosses a cut holding the start, not the end.
+  - `DiscSys.trace_mem_back`, `trace_inside`, `no_reentry`: no re-entry,
+    i.e. `no_back_cross` lifted to every cut.
+  - `DiscSys.composeCut`: prefix-closure. Its traces are exactly the
+    composite's traces that end in the prefix
+    (`composeCut_trace_embed` / `_reflect`).
+  - The two-region `Interface` versions are `trace_cross_crosses_cut` and
+    `trace_stays_in_B`. `CutExhibit` holds a concrete trace and a negative
+    control.
+* `Marches/Tropical.lean` `TropicalGrade` (3b). K-4's two laws over
+  `TropicalNat` (`seq_unitl`, `alt_idem`). S-3 inside marches:
+  `better_reverses_altLe`, `altLe_one` (𝟙 on top, as Loss), `s3_witness`.
+* `docs/kcut-correspondence.adoc` + `scripts/check-correspondence.sh` (3c).
+  Lean ↔ Agda names, each pairing ASSUMED (M-2 idiom). The script fetches
+  siblings at pins (`scripts/fetch-siblings.sh`, `_build/dependencies`)
+  and checks names only. Pins: choreographic-types `edb784a`,
+  resource-algebra `cf9235c`, tropical-types `e172f8a`.
+* F6 added (`FALSIFIERS.adoc`), and it FIRED on reading. MRC-01's proposed
+  `Acyclic ↔ Consistent` pairing is withdrawn: Agda's `Consistent p c` is a
+  party-indexed merge condition, and marches has no parties. F6 stays open
+  (narrowed).
+* Citation corrections found while reading the pins:
+  - T-2's `receiver-knows` / `sender-knows` are in `Instances.agda`, not
+    `Transport.agda`.
+  - `TropicalAdapterPath.lean` is in hyperpolymath/tropical-types, whose
+    lake package is `tropical-resource-typing`, on Lean v4.13.0.
+  - marches' `TropicalNat` is min-plus, so it is not one of M-2's two
+    (max-plus) objects.
+* Gates:
+  - `lake build` → `Build completed successfully (15 jobs).`
+  - `grep -rnw sorry Marches/ Marches.lean` is empty.
+  - `#eval orbit` is unchanged
+    (`[(false, false), (true, true), (false, false), (true, true)]`).
+  - `#print axioms`: every declaration added in 3a/3b depends on no axioms.
+  - `scripts/check-correspondence.sh` → `PASS: 15 Lean names and 16
+    sibling names exist at the pins; both negative controls refused`. A
+    mutation test (one bad Lean name, one bad Agda name, one wrong pin)
+    → `FAIL`, as it should.
+* CI anomalies, pre-existing on `main`, not caused by this rung:
+  - `CI` has ended in `startup_failure` since #34. Dependabot moved
+    `lean-action` to v1.6.1 and `codeql-action` to v4.38.2 without
+    relocking `actions.lock`. Fix: `gh actions-lock`, as in #25.
+  - `estate-audit` fails at cicd-suite's Required Files Gate. Under
+    `-e -o pipefail`, a comment-only CODEOWNERS makes `grep -v | wc -l`
+    exit 1 silently. The fix belongs in cicd-suite.
+* postern was not reachable (`add_repo`: not found or no access; no
+  `list_repos` match). No cross-issue was filed. The import plan is kept in
+  the correspondence doc.
+* Status rows moved:
+  - New PROVEN rows (README) for 3a/3b.
+  - One ASSUMED row for the K-CUT correspondence.
+  - No convergence claim (`grep -ni converg` on new files hits only the
+    disclaimers).
+* Rung 3 stays OPEN: 3d (TropicalAdapterPath import), 3e (echo-types
+  bridge) and 3f (postern) are not done. No tag.
+
 == 2026-10-14 — toolchain moved to v4.34.0 before rung 3 (Claude Code session)
 
 * Maintainer decision (MRC-01 open question): move `lean-toolchain` from
@@ -86,9 +150,11 @@
 
 == Next action
 
-Rung 3 (see ROADMAP.adoc): tropical/estate integration. Import the
-estate's fully proved `TropicalAdapterPath.lean`
-(tropical-resource-typing) behind the `Marches/Tropical.lean` seam —
-vendor or depend on it, do NOT paraphrase. Path provenance as graded
-accumulation (echo-types bridge). Obtain the real file; never
-reconstruct from memory. One rung only.
+Rung 3 (see ROADMAP.adoc), the remaining items. 3d: import the estate's
+fully proved `TropicalAdapterPath.lean` (hyperpolymath/tropical-types,
+lake package `tropical-resource-typing`, pinned `e172f8a`, Lean v4.13.0)
+behind the `Marches/Tropical.lean` seam — vendor or depend on it, do NOT
+paraphrase, and expect toolchain friction against v4.34.0. 3e: path
+provenance as graded accumulation (echo-types bridge). 3f: file the
+postern cross-issue once that repository exists. Obtain the real files;
+never reconstruct from memory. One rung only.
diff --git a/docs/kcut-correspondence.adoc b/docs/kcut-correspondence.adoc
new file mode 100644
index 0000000..052afa4
--- /dev/null
+++ b/docs/kcut-correspondence.adoc
@@ -0,0 +1,163 @@
+= K-CUT correspondence — a table of names, not a link
+:revdate: 2026-10-14
+
+marches (Lean 4, kept as provenance) proves that a region crossing is a
+cut (`Marches/Cut.lean`). choreographic-types (Agda, the proof kernel)
+proves the cut side of K-CUT for global choreographies. This page pairs
+the names. It does not link the proofs: no row is more than ASSUMED, in
+the idiom of resource-algebra's M-2 — cross-prover, port-and-reprove, a
+named obligation, no mechanical link exists or is claimed.
+
+What IS mechanical: `scripts/check-correspondence.sh` fetches the
+siblings at the pins below and checks that every name cited on this page
+exists — Lean names in this build, sibling names at their pinned commits —
+and that every pin appears here. A fabricated Lean name and a fabricated
+Agda name are run through the same checks as a negative control and must
+be refused. The script checks names only. Whether two paired names mean
+the same thing is falsifier F6 (`FALSIFIERS.adoc`), and one proposed row
+below already fails it.
+
+Delimitation: nothing here is a convergence claim; agda-routing owns that
+ground (`LIMITATIONS.adoc`).
+
+== Pins
+
+[cols="2,3,3",options="header"]
+|===
+|Repository |Commit |Read for
+
+|hyperpolymath/choreographic-types
+|`edb784a7d26c276c2abfa8399b773d346dbb101e`
+|`Cut`, `_↾_`, `Consistent`, `proj-cut`, `cut-projectable`, K-4 minimal laws, `Bound`, T-2
+
+|hyperpolymath/resource-algebra
+|`cf9235c532712a783a404c359a1055f40134794a`
+|`_≼_` convention, `Loss`, `MaxPlus`, S-3 witnesses, M-2 status
+
+|hyperpolymath/tropical-types
+|`e172f8abefd50fc40def4368fa60a155d130ff47`
+|`TropicalAdapterPath.lean`, `TropicalSessionTypes.lean` (the Lean side of M-2)
+|===
+
+`scripts/fetch-siblings.sh` holds the same three commits. Re-pin one
+commit per change and update this table in the same commit.
+
+== The table
+
+Every Lean name below is PROVEN by `lake build` in this repository, and
+every Agda name has the status its own repository gives it. The *Status*
+column is the status of the PAIRING.
+
+[cols="1,3,3,4,2",options="header"]
+|===
+|ID |marches (Lean) |sibling (Agda, at pin) |Reading |Status of the pairing
+
+|KC-1
+|`Marches.Cut`
+|`choreographic-types:src/Choreographic/Global.agda:Cut`, `choreographic-types:src/Choreographic/Global.agda:_↾_`
+|Both are frontiers whose inside is a prefix. Lean: a predecessor-closed
+set of regions of a DAG. Agda: a frontier through a finite global type;
+`G ↾ c` is the prefix.
+|ASSUMED (port-and-reprove)
+
+|KC-2
+|`Marches.Cut.closed`
+|`choreographic-types:src/Choreographic/Global.agda:Cut`
+|Downward closure is marches' cut condition and must be stated. In Agda it
+holds by construction: a `Cut G` is built along the tree (`stop`,
+`cont-msg`, `cont-choice`) and cannot skip a node.
+|ASSUMED (port-and-reprove)
+
+|KC-3
+|`Marches.Acyclic` (as proposed in MRC-01)
+|`choreographic-types:src/Choreographic/Projection.agda:Consistent` (as proposed)
+|*Fails on reading* (F6). `Consistent p c` is indexed by a party: at each
+choice `p` takes no part in, the two truncated branches must merge for
+`p`. marches has no parties and no choices. Its `Acyclic` is a hypothesis
+on the region relation; Agda needs none, because `Global` is an inductive
+tree. Neither name has a counterpart on the other side.
+|OPEN — no counterpart; the proposed pairing is withdrawn
+
+|KC-4
+|`Marches.DiscSys.composeCut_trace_reflect`, `Marches.DiscSys.trace_mem_back`, `Marches.DiscSys.no_reentry`, `Marches.no_back_cross`
+|`choreographic-types:src/Choreographic/KCut.agda:cut-projectable` (K-5)
+|"What happens after the frontier is irrelevant." Lean: a trace that ends
+in the prefix lies in it throughout and is a trace of the prefix alone;
+a trace that leaves a cut never returns. `no_back_cross` (one interface)
+is the special case. Agda: `Consistent p c` alone makes the prefix
+projectable. MRC-01 paired `no_back_cross` with K-5. The closer Lean
+statement is `composeCut_trace_reflect`, and `no_back_cross` /
+`no_reentry` are the ingredient it rests on.
+|ASSUMED (port-and-reprove)
+
+|KC-5
+|`Marches.DiscSys.composeCut`, `Marches.DiscSys.composeCut_trace_embed`
+|`choreographic-types:src/Choreographic/KCut.agda:proj-cut` (K-2)
+|An operation commutes with cutting. Agda: projecting then cutting equals
+cutting then projecting, with no side-conditions. Lean: composing the
+cut prefix gives exactly the composite's traces that end in the prefix
+(embed + reflect). The operations differ (projection vs composition);
+only the commuting shape is shared.
+|ASSUMED (port-and-reprove)
+
+|KC-6
+|`Marches.TropicalGrade.seq_unitl`, `Marches.TropicalGrade.alt_idem`
+|`choreographic-types:tests/minimal-laws/ResourceAlgebra/Core.agda:unitˡ`, `choreographic-types:tests/minimal-laws/ResourceAlgebra/Core.agda:idem`, `choreographic-types:scripts/minimal-laws.sh`
+|K-4 (TESTED there): K-CUT-LOSS uses only `𝟙 ⊗ x ≡ x` and `x ⊕ x ≡ x`.
+Both hold for marches' (min,+) reading of `TropicalNat`.
+|ASSUMED (port-and-reprove)
+
+|KC-7
+|`Marches.TropicalGrade.better_reverses_altLe`, `Marches.TropicalGrade.altLe_one`, `Marches.TropicalGrade.s3_witness`
+|`resource-algebra:src/ResourceAlgebra/Separation.agda:loss-order-reversed`, `resource-algebra:src/ResourceAlgebra/Instances/Loss.agda:Loss`, `choreographic-types:src/Choreographic/Bound.agda:grade-≼↾`
+|S-3 and W-4. marches' `better` runs with cost, and its ⊕-induced order
+runs against cost with `𝟙` on top, as in `Loss` (`fin 2 ≼ fin 1`, same
+numbers). So a ported K-CUT-WARRANT bound would take the `grade-≼↾`
+(upper) form, not `grade↾-≼`. Any port must re-check the direction.
+|ASSUMED (port-and-reprove)
+
+|KC-8
+|`Marches.TropicalNat`
+|`resource-algebra:src/ResourceAlgebra/Instances/MaxPlus.agda:MaxPlus`, `tropical-types:TropicalSessionTypes.lean`
+|M-2 pairs `MaxPlus` with tropical-types' Lean `CommSemiring Tropical`,
+and it is OPEN there. marches' `TropicalNat` is min-plus on `Nat`, not
+max-plus: by KC-7 it sits with `Loss`, not with `MaxPlus`. No pairing
+with M-2's objects is proposed.
+|OPEN — not paired (order runs opposite)
+|===
+
+== Transport, for postern
+
+T-2 (choreographic-types, PROVEN for the synchronous fragment): receiving
+is knowing (`choreographic-types:src/Choreographic/Instances.agda:receiver-knows`);
+synchronously, so is sending
+(`choreographic-types:src/Choreographic/Instances.agda:sender-knows`). Both
+instantiate the generic
+`choreographic-types:src/Choreographic/Transport.agda:knows-local-cut`.
+MRC-01 cited `Transport.agda` for the two named lemmas. At the pin they
+are in `Instances.agda`. Under asynchrony, `sender-knows` is expected to
+FAIL (PROOF-STATUS, "Open: Asynchrony"). That is OPEN, and it is the
+property an ACK-based containment boundary relies on: a sender without
+receipt cannot know.
+
+== postern import plan (not filed)
+
+postern was not reachable on 2026-10-14 (not found, or no access, from
+this account), so no cross-issue was filed and nothing here describes
+postern's code. When the repository exists, the plan from MRC-01 is:
+
+. State the containment boundary as an `Interface` and import
+  `Marches.no_back_cross`. The crossing map never returns.
+. Model TCP-ACK-as-proof as a `Trace` whose well-typedness is the ACK.
+. Model `guardEmit` as unconstructibility of emission before the ACK.
+. Cite the sender's ignorance under asynchrony as OPEN on
+  choreographic-types (above). Do not claim it.
+
+== As the proofs progress
+
+* M-2 closes, or an Agda port of `Marches/Cut.lean` lands. Then KC-1, KC-2,
+  KC-4, KC-5 and KC-6 can each move from ASSUMED to a named port with its
+  own check.
+* Asynchronous K-CUT lands. Then postern's handshake is typed against the
+  asynchronous fragment.
+* Rung 4 attestation lands. Then announcements carry the cut they were made at.
diff --git a/scripts/check-correspondence.sh b/scripts/check-correspondence.sh
new file mode 100755
index 0000000..80dd10b
--- /dev/null
+++ b/scripts/check-correspondence.sh
@@ -0,0 +1,81 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Mechanical check on docs/kcut-correspondence.adoc. It checks NAMES, not
+# meanings:
+#   1. every Lean identifier the table cites (`Marches.…`) exists in this
+#      build (`#check` under `lake env lean`);
+#   2. every sibling identifier it cites (`repo:path` or `repo:path:name`)
+#      exists in that repository at the commit pinned in
+#      scripts/fetch-siblings.sh;
+#   3. every pinned commit appears in the table, so prose and pin agree.
+# Negative control: one fabricated Lean name and one fabricated Agda name
+# are run through the same checks and must be refused, or the run fails.
+# Whether the paired names MEAN the same thing is falsifier F6, and no
+# script decides it.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+export LC_ALL="${LC_ALL:-C.UTF-8}"
+
+doc=docs/kcut-correspondence.adoc
+deps=_build/dependencies
+scripts/fetch-siblings.sh
+lake build >/dev/null
+
+tmp="$(mktemp -d)"; trap 'rm -rf "$tmp"' EXIT
+
+lean_exists() {
+  printf 'import Marches\n#check @%s\n' "$1" > "$tmp/Check.lean"
+  lake env lean "$tmp/Check.lean" >/dev/null 2>&1
+}
+
+# `repo:path` names a file; `repo:path:name` needs a line of that file, at
+# the pinned commit, that begins with the name and a space (after any
+# indentation and an optional data/record/field keyword). That is where
+# Agda declares a name; it is a name check, not a type check.
+sibling_exists() {
+  local repo="${1%%:*}" rest="${1#*:}" path name
+  case "$rest" in
+    *:*) path="${rest%%:*}"; name="${rest#*:}" ;;
+    *)   path="$rest"; name="" ;;
+  esac
+  [ -d "$deps/$repo" ] || return 1
+  git -C "$deps/$repo" cat-file -e "HEAD:$path" 2>/dev/null || return 1
+  [ -z "$name" ] && return 0
+  git -C "$deps/$repo" show "HEAD:$path" | awk -v n="$name" '
+      { sub(/^[ \t]+/, ""); sub(/^(data|record|field)[ \t]+/, "") }
+      index($0, n " ") == 1 { found = 1 }
+      END { exit found ? 0 : 1 }'
+}
+
+fail=0
+nlean=0; nsib=0
+
+while IFS= read -r name; do
+  nlean=$((nlean + 1))
+  if ! lean_exists "$name"; then echo "MISSING (Lean): $name"; fail=1; fi
+done < <(grep -oE '`Marches\.[A-Za-z0-9_.'"'"']+`' "$doc" | tr -d '`' | sort -u)
+
+# shellcheck disable=SC2016  # the backticks are literal AsciiDoc markup
+while IFS= read -r ref; do
+  nsib=$((nsib + 1))
+  if ! sibling_exists "$ref"; then echo "MISSING (sibling): $ref"; fail=1; fi
+done < <(grep -oE '`(choreographic-types|resource-algebra|tropical-types):[^`]+`' "$doc" \
+           | tr -d '`' | sort -u)
+
+while IFS= read -r pin; do
+  if ! grep -qF "$pin" "$doc"; then echo "PIN NOT IN TABLE: $pin"; fail=1; fi
+done < <(grep -oE '_COMMIT:-[0-9a-f]{40}' scripts/fetch-siblings.sh | cut -d- -f2)
+
+# Negative control: the checks must refuse names that do not exist.
+if lean_exists "Marches.Cut.no_such_lemma_negative_control"; then
+  echo "NEGATIVE CONTROL FAILED: a fabricated Lean name was accepted"; fail=1
+fi
+if sibling_exists "choreographic-types:src/Choreographic/KCut.agda:no-such-lemma-negative-control"; then
+  echo "NEGATIVE CONTROL FAILED: a fabricated Agda name was accepted"; fail=1
+fi
+
+if [ "$fail" -ne 0 ]; then
+  echo "FAIL: docs/kcut-correspondence.adoc cites a name or pin that does not check"
+  exit 1
+fi
+echo "PASS: $nlean Lean names and $nsib sibling names exist at the pins; both negative controls refused"
diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh
new file mode 100755
index 0000000..844725e
--- /dev/null
+++ b/scripts/fetch-siblings.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Fetch the sibling proof repositories marches cites, each at a pinned
+# commit, into _build/dependencies (pattern: choreographic-types,
+# residual-evidence-types). Nothing here is imported into the Lean build:
+# the siblings are read, never re-declared. Re-pin deliberately, one
+# commit per pin, and update docs/kcut-correspondence.adoc to match.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+
+CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-edb784a7d26c276c2abfa8399b773d346dbb101e}"
+RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}"
+TROPICAL_TYPES_COMMIT="${TROPICAL_TYPES_COMMIT:-e172f8abefd50fc40def4368fa60a155d130ff47}"
+
+fetch() {
+  local name="$1" commit="$2" dir="_build/dependencies/$1"
+  if [ ! -d "$dir" ]; then
+    git clone --quiet "https://github.com/hyperpolymath/$name.git" "$dir"
+  fi
+  git -C "$dir" fetch --quiet origin
+  git -C "$dir" checkout --quiet "$commit"
+  echo "$name at $(git -C "$dir" rev-parse --short HEAD)"
+}
+
+mkdir -p _build/dependencies
+fetch choreographic-types "$CHOREOGRAPHIC_TYPES_COMMIT"
+fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT"
+fetch tropical-types "$TROPICAL_TYPES_COMMIT"