From 1ea9a8554e96324aed5dd8b73dbb62a7bb91de17 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 14 Oct 2026 01:18:25 +0000
Subject: [PATCH 1/2] feat(rung-3): a region crossing is a cut; K-4 laws over
 TropicalNat

Marches/Cut.lean (new): a cut of the region DAG is a set of regions
closed under predecessors.
- 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
  composite trace crosses a cut holding the trace's start, not its end.
- DiscSys.trace_mem_back / trace_inside / no_reentry: a trace ending in a
  cut was inside it all along; a trace that leaves a cut never re-enters
  (no_back_cross lifted from one interface to every cut).
- DiscSys.composeCut: compose restricted to a cut prefix is a Discipline
  (prefix-closure); composeCut_trace_embed / composeCut_trace_reflect: its
  traces are exactly the composite's traces that end in the prefix.
- Two-region Interface: trace_cross_crosses_cut, trace_stays_in_B.
- CutExhibit: a concrete twoTropical trace, and a negative control.

Marches/Tropical.lean: TropicalGrade reads TropicalNat as a (min,+)
grade. seq_unitl and alt_idem are the two laws K-CUT-LOSS uses (K-4).
better_reverses_altLe, altLe_one and s3_witness record that marches'
`better` runs against its own induced order (S-3 / W-4 direction).

Every new declaration depends on no axioms (#print axioms) and nothing
re-declares an Agda definition.

Gates: lake build -> Build completed successfully (15 jobs);
grep -rnw sorry empty; #eval orbit unchanged.

Rung: 3 (rung stays OPEN)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
---
 Marches.lean          |   1 +
 Marches/Cut.lean      | 428 ++++++++++++++++++++++++++++++++++++++++++
 Marches/Tropical.lean |  63 +++++++
 README.adoc           |  36 +++-
 4 files changed, 526 insertions(+), 2 deletions(-)
 create mode 100644 Marches/Cut.lean

diff --git a/Marches.lean b/Marches.lean
index b6e0b65..24ff9a1 100644
--- a/Marches.lean
+++ b/Marches.lean
@@ -9,3 +9,4 @@ import Marches.BadGadget
 import Marches.Tropical
 import Marches.Freewheel
 import Marches.Reassembly
+import Marches.Cut
diff --git a/Marches/Cut.lean b/Marches/Cut.lean
new file mode 100644
index 0000000..5db7f54
--- /dev/null
+++ b/Marches/Cut.lean
@@ -0,0 +1,428 @@
+/-
+  Marches — cuts of the region DAG (rung 3).
+
+  A *cut* is a set of regions closed under DAG predecessors: if a region
+  is in the cut, so is every region that can cross into it. Read along the
+  causal order of announcements (a route is in a region before it crosses
+  out), a cut is a frontier, and its regions are the prefix before that
+  frontier. This is the classical downward-closure condition on a cut. It
+  is NOT the party-indexed `Consistent` of choreographic-types, a merge
+  condition at choices (see the correspondence table). Being a cut needs
+  no acyclicity; *crossing* one does (`edge_crosses_past`).
+
+  Headline theorems:
+    • Cut.edge_crosses_past        : in an acyclic graph every edge r → r'
+                                     leaves the principal cut ↓r.
+    • Cut.path_back_crosses_no_cut : an edge on a cycle crosses NO cut —
+                                     acyclicity is load-bearing.
+    • DiscSys.trace_cross_crosses_cut : every crossing in a well-typed
+                                     composite trace crosses a cut that
+                                     holds the trace's start and not its end.
+    • DiscSys.trace_mem_back       : a trace ending inside a cut was inside
+                                     it all along (`trace_inside`: every
+                                     label fired inside it).
+    • DiscSys.no_reentry           : a trace that has left a cut never
+                                     re-enters it — `no_back_cross`, lifted
+                                     from one interface to every cut.
+    • DiscSys.composeCut           : `compose` restricted to a cut prefix
+                                     is a `Discipline` (prefix-closure). Its
+                                     traces are exactly the composite traces
+                                     that end in the prefix
+                                     (`composeCut_trace_embed`,
+                                     `composeCut_trace_reflect`).
+    • trace_cross_crosses_cut      : the same, for the two-region
+                                     `Interface` of `Compose.lean` (the
+                                     2-node DAG `Reassembly.boolUp`).
+
+  Provenance. choreographic-types (pinned at edb784a) proves the cut side
+  for global choreographies in Agda: `Choreographic.Global.Cut`,
+  `KCut.proj-cut`, `KCut.cut-projectable`. The relation between those
+  names and these is a table, not a link (docs/kcut-correspondence.adoc).
+  No row there is more than ASSUMED (port-and-reprove). Nothing in this
+  file imports or re-declares the Agda definitions.
+
+  Delimitation: prefix-closure and loop-freedom of the typed judgment are
+  not protocol convergence; agda-routing owns that ground (LIMITATIONS.adoc).
+-/
+
+import Marches.Compose
+import Marches.Digraph
+import Marches.Reassembly
+
+namespace Marches
+
+/-- A cut of a region graph `E`: a set of regions closed under
+    predecessors. Every region that can cross into the cut is in it. -/
+structure Cut {R : Type} (E : R → R → Prop) where
+  mem    : R → Prop
+  closed : ∀ {r r' : R}, E r r' → mem r' → mem r
+
+namespace Cut
+
+variable {R : Type} {E : R → R → Prop}
+
+/-- An edge `r → r'` crosses the cut `C` when it leaves it. -/
+def Crosses (C : Cut E) (r r' : R) : Prop := C.mem r ∧ ¬ C.mem r'
+
+/-- Closure lifts from edges to paths. -/
+theorem closed_path (C : Cut E) :
+    ∀ {r r' : R}, RPath E r r' → C.mem r' → C.mem r := by
+  intro r r' h
+  induction h with
+  | single e => exact C.closed e
+  | cons e _ ih => intro hm; exact C.closed e (ih hm)
+
+/-- The principal cut below `r`: `r` and every region with a path to it. -/
+def past (r : R) : Cut E where
+  mem x := x = r ∨ RPath E x r
+  closed := by
+    intro x y e hy
+    cases hy with
+    | inl h => subst h; exact Or.inr (.single e)
+    | inr p => exact Or.inr (.cons e p)
+
+/-- In an acyclic graph every edge crosses the principal cut of its source:
+    the source is inside, the target outside. -/
+theorem edge_crosses_past (hacyc : Acyclic E) {r r' : R} (e : E r r') :
+    (past (E := E) r).Crosses r r' := by
+  refine ⟨Or.inl rfl, ?_⟩
+  intro h
+  cases h with
+  | inl h => subst h; exact hacyc _ (.single e)
+  | inr p => exact hacyc r (.cons e p)
+
+/-- Negative: if `r'` reaches back to `r`, no cut separates them. So an edge
+    `r → r'` on a cycle crosses no cut at all: without `Acyclic`,
+    `edge_crosses_past` fails, and so does every theorem below that uses it. -/
+theorem path_back_crosses_no_cut {r r' : R} (p : RPath E r' r) (C : Cut E) :
+    ¬ C.Crosses r r' :=
+  fun ⟨h, hn⟩ => hn (C.closed_path p h)
+
+end Cut
+
+/-! ### Traces of a discipline, split at a label -/
+
+/-- A trace containing a label splits into a prefix, that step, and a suffix. -/
+theorem Discipline.trace_split (D : Discipline) :
+    ∀ {p : D.Pos} {ls : List D.Lab} {q : D.Pos}, Discipline.Trace D p ls q →
+      ∀ {l : D.Lab}, l ∈ ls →
+        ∃ ls₁ ls₂ m m', ls = ls₁ ++ l :: ls₂ ∧ Discipline.Trace D p ls₁ m ∧
+          D.Step l m m' ∧ Discipline.Trace D m' ls₂ q := by
+  intro p ls q ht
+  induction ht with
+  | nil => intro l hl; cases hl
+  | @cons p q₀ _ l₀ ls hs ht' ih =>
+    intro l hl
+    cases hl with
+    | head => exact ⟨[], ls, p, q₀, rfl, .nil, hs, ht'⟩
+    | tail _ hl' =>
+      obtain ⟨ls₁, ls₂, m, m', he, h₁, hm, h₂⟩ := ih hl'
+      exact ⟨l₀ :: ls₁, ls₂, m, m', by rw [he]; rfl, .cons hs h₁, hm, h₂⟩
+
+/-! ### Cuts of a composed region DAG -/
+
+namespace DiscSys
+
+variable (S : DiscSys)
+
+/-- One composite step stays in its region or crosses one DAG edge. -/
+theorem step_region :
+    ∀ {l : S.Lab} {p q : S.Pos}, S.Step l p q → p.1 = q.1 ∨ S.E p.1 q.1 := by
+  intro l p q h
+  cases h with
+  | sloc _ => exact Or.inl rfl
+  | scross e => exact Or.inr e
+
+/-- A crossing step leaves exactly the edge's source for its target. -/
+theorem cross_step_regions {r r' : S.R} {e : S.E r r'} {m m' : S.Pos}
+    (h : S.Step (.cross r r' e) m m') : m.1 = r ∧ m'.1 = r' := by
+  cases h with
+  | scross _ => exact ⟨rfl, rfl⟩
+
+/-- A trace ends in its start region or downstream of it. -/
+theorem trace_region (hacyc : Acyclic S.E) :
+    ∀ {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos},
+      Discipline.Trace (S.compose hacyc) p ls q → p.1 = q.1 ∨ RPath S.E p.1 q.1 := by
+  intro p ls q ht
+  induction ht with
+  | nil => exact Or.inl rfl
+  | cons hs _ ih =>
+    cases S.step_region hs with
+    | inl h₁ =>
+      cases ih with
+      | inl h₂ => exact Or.inl (h₁.trans h₂)
+      | inr p₂ => exact Or.inr (by rw [h₁]; exact p₂)
+    | inr e =>
+      cases ih with
+      | inl h₂ => exact Or.inr (.single (by rw [← h₂]; exact e))
+      | inr p₂ => exact Or.inr (.cons e p₂)
+
+/-- PREFIX: a trace ending inside a cut started inside it. What happens
+    after the frontier cannot reach back into the prefix. -/
+theorem trace_mem_back (hacyc : Acyclic S.E) (C : Cut S.E)
+    {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos}
+    (ht : Discipline.Trace (S.compose hacyc) p ls q) (hq : C.mem q.1) : C.mem p.1 := by
+  cases S.trace_region hacyc ht with
+  | inl h => rw [h]; exact hq
+  | inr p => exact C.closed_path p hq
+
+/-- `no_back_cross`, lifted from one interface to every cut of the DAG:
+    a trace that starts outside a cut never enters it. -/
+theorem no_reentry (hacyc : Acyclic S.E) (C : Cut S.E)
+    {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos}
+    (ht : Discipline.Trace (S.compose hacyc) p ls q) (hp : ¬ C.mem p.1) :
+    ¬ C.mem q.1 :=
+  fun hq => hp (S.trace_mem_back hacyc C ht hq)
+
+/-- A composite label lies inside a cut when it fires from a region of the
+    cut and, if a crossing, lands in one. -/
+def LabInside (C : Cut S.E) : S.Lab → Prop
+  | .loc r _ => C.mem r
+  | .cross r r' _ => C.mem r ∧ C.mem r'
+
+/-- A trace ending inside a cut fires every one of its labels inside it. -/
+theorem trace_inside (hacyc : Acyclic S.E) (C : Cut S.E) :
+    ∀ {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos},
+      Discipline.Trace (S.compose hacyc) p ls q → C.mem q.1 →
+        ∀ l ∈ ls, S.LabInside C l := by
+  intro p ls q ht
+  induction ht with
+  | nil => intro _ l hl; cases hl
+  | cons hs ht' ih =>
+    intro hq l hl
+    have hq₀ := S.trace_mem_back hacyc C ht' hq
+    cases hl with
+    | head =>
+      cases hs with
+      | sloc _ => exact hq₀
+      | scross e => exact ⟨C.closed e hq₀, hq₀⟩
+    | tail _ hl' => exact ih hq l hl'
+
+/-- Every crossing in a well-typed composite trace crosses a cut — the
+    principal cut of its source — which holds the trace's start and not its
+    end: the trace leaves that cut at this step and never comes back. -/
+theorem trace_cross_crosses_cut (hacyc : Acyclic S.E)
+    {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos}
+    (ht : Discipline.Trace (S.compose hacyc) p ls q)
+    {r r' : S.R} {e : S.E r r'} (hl : Lab.cross r r' e ∈ ls) :
+    ∃ C : Cut S.E, C.Crosses r r' ∧ C.mem p.1 ∧ ¬ C.mem q.1 := by
+  obtain ⟨_, _, m, m', _, h₁, hm, h₂⟩ := Discipline.trace_split _ ht hl
+  obtain ⟨hmr, hmr'⟩ := S.cross_step_regions hm
+  have hc := Cut.edge_crosses_past hacyc e
+  refine ⟨Cut.past r, hc, ?_, ?_⟩
+  · cases S.trace_region hacyc h₁ with
+    | inl h => exact Or.inl (h.trans hmr)
+    | inr p => exact Or.inr (by rw [← hmr]; exact p)
+  · exact S.no_reentry hacyc (Cut.past r) h₂ (by rw [hmr']; exact hc.2)
+
+/-! ### Prefix-closure: `compose` restricted to a cut is a discipline -/
+
+/-- The system restricted to the regions of a cut. -/
+def restrict (C : Cut S.E) : DiscSys where
+  R := {r : S.R // C.mem r}
+  E := fun a b => S.E a.1 b.1
+  D := fun a => S.D a.1
+  τ := fun e x => S.τ e x
+
+/-- Paths in the restriction are paths in the system. -/
+theorem restrict_path (C : Cut S.E) :
+    ∀ {a b : (S.restrict C).R}, RPath (S.restrict C).E a b → RPath S.E a.1 b.1 := by
+  intro a b h
+  induction h with
+  | single e => exact .single e
+  | cons e _ ih => exact .cons e ih
+
+/-- The restriction of an acyclic DAG is acyclic. -/
+theorem restrict_acyclic (hacyc : Acyclic S.E) (C : Cut S.E) :
+    Acyclic (S.restrict C).E :=
+  fun a h => hacyc a.1 (S.restrict_path C h)
+
+/-- PREFIX-CLOSURE: `compose` restricted to a cut prefix is a `Discipline`.
+    Its loop-freedom is `Discipline.no_loop`, with no new proof. -/
+def composeCut (hacyc : Acyclic S.E) (C : Cut S.E) : Discipline :=
+  (S.restrict C).compose (S.restrict_acyclic hacyc C)
+
+/-- Positions of the prefix, read as positions of the whole system. -/
+def posEmb (C : Cut S.E) : (S.restrict C).Pos → S.Pos := fun p => ⟨p.1.1, p.2⟩
+
+/-- Labels of the prefix, read as labels of the whole system. -/
+def labEmb (C : Cut S.E) : (S.restrict C).Lab → S.Lab
+  | .loc a l => .loc a.1 l
+  | .cross a b e => .cross a.1 b.1 e
+
+theorem step_embed (C : Cut S.E) :
+    ∀ {l : (S.restrict C).Lab} {p q : (S.restrict C).Pos},
+      (S.restrict C).Step l p q → S.Step (S.labEmb C l) (S.posEmb C p) (S.posEmb C q) := by
+  intro l p q h
+  cases h with
+  | sloc hs => exact .sloc hs
+  | @scross a b e _ => exact DiscSys.Step.scross (S := S) (r := a.1) (r' := b.1) e
+
+/-- Every trace of the prefix is a trace of the whole composite. -/
+theorem composeCut_trace_embed (hacyc : Acyclic S.E) (C : Cut S.E) :
+    ∀ {p : (S.composeCut hacyc C).Pos} {ls : List (S.composeCut hacyc C).Lab}
+      {q : (S.composeCut hacyc C).Pos},
+      Discipline.Trace (S.composeCut hacyc C) p ls q →
+        Discipline.Trace (S.compose hacyc) (S.posEmb C p) (ls.map (S.labEmb C))
+          (S.posEmb C q) := by
+  intro p ls q ht
+  induction ht with
+  | nil => exact .nil
+  | cons hs _ ih => exact .cons (S.step_embed C hs) ih
+
+/-- Conversely, every composite trace that starts and ends in the prefix is
+    a trace of the prefix, label for label. -/
+theorem composeCut_trace_reflect_of (hacyc : Acyclic S.E) (C : Cut S.E) :
+    ∀ {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos},
+      Discipline.Trace (S.compose hacyc) p ls q →
+        ∀ (hp : C.mem p.1) (hq : C.mem q.1),
+          ∃ ls' : List (S.restrict C).Lab, ls'.map (S.labEmb C) = ls ∧
+            Discipline.Trace (S.composeCut hacyc C) ⟨⟨p.1, hp⟩, p.2⟩ ls'
+              ⟨⟨q.1, hq⟩, q.2⟩ := by
+  intro p ls q ht
+  induction ht with
+  | nil => intro _ _; exact ⟨[], rfl, .nil⟩
+  | cons hs ht' ih =>
+    intro hp hq
+    have hq₀ := S.trace_mem_back hacyc C ht' hq
+    obtain ⟨ls', hmap, ht''⟩ := ih hq₀ hq
+    cases hs with
+    | sloc hl =>
+      exact ⟨.loc ⟨_, hp⟩ _ :: ls', by rw [List.map_cons, hmap] <;> rfl,
+        .cons (.sloc hl) ht''⟩
+    | scross e =>
+      exact ⟨.cross ⟨_, hp⟩ ⟨_, hq₀⟩ e :: ls', by rw [List.map_cons, hmap] <;> rfl,
+        .cons (DiscSys.Step.scross (S := S.restrict C) (r := ⟨_, hp⟩) (r' := ⟨_, hq₀⟩) e)
+          ht''⟩
+
+/-- THE prefix-closure theorem: a composite trace that ENDS in a cut prefix
+    is a trace of the prefix alone — whatever lies beyond the frontier is
+    irrelevant to it. With `composeCut_trace_embed`, the prefix's traces
+    are exactly the composite's traces that end in the prefix. -/
+theorem composeCut_trace_reflect (hacyc : Acyclic S.E) (C : Cut S.E)
+    {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos}
+    (ht : Discipline.Trace (S.compose hacyc) p ls q) (hq : C.mem q.1) :
+    ∃ ls' : List (S.restrict C).Lab, ls'.map (S.labEmb C) = ls ∧
+      Discipline.Trace (S.composeCut hacyc C)
+        ⟨⟨p.1, S.trace_mem_back hacyc C ht hq⟩, p.2⟩ ls' ⟨⟨q.1, hq⟩, q.2⟩ :=
+  S.composeCut_trace_reflect_of hacyc C ht _ hq
+
+/-- The prefix has no well-typed loop: an instance of the generic theorem. -/
+theorem composeCut_no_loop (hacyc : Acyclic S.E) (C : Cut S.E)
+    {p : (S.composeCut hacyc C).Pos} {ls : List (S.composeCut hacyc C).Lab}
+    (ht : Discipline.Trace (S.composeCut hacyc C) p ls p) : ls = [] :=
+  Discipline.no_loop _ ht
+
+end DiscSys
+
+/-! ### The two-region interface of `Compose.lean` as a cut crossing
+
+  The interface `A → B` is the single edge of the 2-node DAG
+  `Reassembly.boolUp` (`false → true`); A is the region `false`, B is
+  `true`. Its crossing leaves the principal cut `↓false` = the A side. -/
+
+/-- The region of a two-region position: `false` for A, `true` for B. -/
+def Pos.region {A B : PathAlgebra} : Pos A B → Bool
+  | .inA _ => false
+  | .inB _ => true
+
+/-- The A side of the interface, as a cut of `boolUp`. -/
+abbrev aSide : Cut Reassembly.boolUp := Cut.past false
+
+/-- The interface crossing crosses the A-side cut. -/
+theorem cross_crosses_aSide (A B : PathAlgebra) (I : Interface A B)
+    {p q : Pos A B} (h : Step A B I .cross p q) :
+    aSide.Crosses p.region q.region := by
+  cases h with
+  | cross => exact Cut.edge_crosses_past Reassembly.boolUp_acyclic ⟨rfl, rfl⟩
+
+/-- A two-region trace containing a label splits at it. -/
+theorem trace_split (A B : PathAlgebra) (I : Interface A B) :
+    ∀ {p : Pos A B} {ls : List (CLabel A B)} {q : Pos A B}, Trace A B I p ls q →
+      ∀ {l : CLabel A B}, l ∈ ls →
+        ∃ ls₁ ls₂ m m', ls = ls₁ ++ l :: ls₂ ∧ Trace A B I p ls₁ m ∧
+          Step A B I l m m' ∧ Trace A B I m' ls₂ q := by
+  intro p ls q ht
+  induction ht with
+  | nil => intro l hl; cases hl
+  | @cons p q₀ _ l₀ ls hs ht' ih =>
+    intro l hl
+    cases hl with
+    | head => exact ⟨[], ls, p, q₀, rfl, .nil, hs, ht'⟩
+    | tail _ hl' =>
+      obtain ⟨ls₁, ls₂, m, m', he, h₁, hm, h₂⟩ := ih hl'
+      exact ⟨l₀ :: ls₁, ls₂, m, m', by rw [he]; rfl, .cons hs h₁, hm, h₂⟩
+
+/-- `no_back_cross`, lifted from one step to whole traces: a trace that
+    starts in B ends in B. -/
+theorem trace_stays_in_B (A B : PathAlgebra) (I : Interface A B) :
+    ∀ {p : Pos A B} {ls : List (CLabel A B)} {q : Pos A B},
+      Trace A B I p ls q → p.region = true → q.region = true := by
+  intro p ls q ht
+  induction ht with
+  | nil => exact id
+  | cons hs _ ih =>
+    intro hp
+    apply ih
+    cases hs with
+    | la => cases hp
+    | lb => rfl
+    | cross => cases hp
+
+/-- Every interface crossing in a well-typed two-region trace crosses the
+    A-side cut, which holds the trace's start and not its end. -/
+theorem trace_cross_crosses_cut (A B : PathAlgebra) (I : Interface A B)
+    {p q : Pos A B} {ls : List (CLabel A B)}
+    (ht : Trace A B I p ls q) (hl : CLabel.cross ∈ ls) :
+    aSide.Crosses false true ∧ aSide.mem p.region ∧ ¬ aSide.mem q.region := by
+  obtain ⟨_, _, m, m', _, h₁, hm, h₂⟩ := trace_split A B I ht hl
+  have hc :=
+    Cut.edge_crosses_past Reassembly.boolUp_acyclic (r := false) (r' := true) ⟨rfl, rfl⟩
+  refine ⟨hc, ?_, ?_⟩
+  · cases hm with
+    | cross =>
+      cases hpr : p.region with
+      | false => exact Or.inl rfl
+      | true => exact absurd (trace_stays_in_B A B I h₁ hpr) (fun h => by cases h)
+  · cases hm with
+    | cross =>
+      rw [trace_stays_in_B A B I h₂ rfl]
+      exact hc.2
+
+/-! ### Concrete exhibit: the theorems are not vacuous -/
+
+namespace CutExhibit
+
+open Reassembly
+
+/-- The one edge of `boolUp`. -/
+theorem e₀ : boolUp false true := ⟨rfl, rfl⟩
+
+/-- A concrete trace of `twoTropical`: a hop of weight 2 in region `false`
+    (cost 0 → 3), the crossing (identity on cost), a hop of weight 0 in
+    region `true` (cost 3 → 4). -/
+theorem trace₀ :
+    Discipline.Trace (twoTropical.compose boolUp_acyclic) ⟨false, (0 : Nat)⟩
+      [.loc false (2 : Nat), .cross false true e₀, .loc true (0 : Nat)] ⟨true, (4 : Nat)⟩ :=
+  .cons (.sloc rfl) (.cons (.scross e₀) (.cons (.sloc rfl) .nil))
+
+/-- Its crossing leaves a cut that holds the start region and not the end. -/
+example : ∃ C : Cut boolUp, C.Crosses false true ∧ C.mem false ∧ ¬ C.mem true :=
+  twoTropical.trace_cross_crosses_cut boolUp_acyclic trace₀ (.tail _ (.head _))
+
+/-- The prefix of `trace₀` that stays in region `false` is a trace of the
+    cut prefix `↓false` alone. -/
+example : ∃ ls' : List (twoTropical.restrict (Cut.past false)).Lab,
+    ls'.map (twoTropical.labEmb (Cut.past false)) = [.loc false (2 : Nat)] ∧
+    Discipline.Trace (twoTropical.composeCut boolUp_acyclic (Cut.past false))
+      ⟨⟨false, Or.inl rfl⟩, (0 : Nat)⟩ ls' ⟨⟨false, Or.inl rfl⟩, (3 : Nat)⟩ :=
+  twoTropical.composeCut_trace_reflect_of boolUp_acyclic (Cut.past false)
+    (.cons (.sloc rfl) .nil) (Or.inl rfl) (Or.inl rfl)
+
+/-- Negative control: on a self-loop no cut is crossed. -/
+example (C : Cut (fun _ _ : Unit => True)) : ¬ C.Crosses () () :=
+  Cut.path_back_crosses_no_cut (.single trivial) C
+
+end CutExhibit
+
+end Marches
diff --git a/Marches/Tropical.lean b/Marches/Tropical.lean
index f9686b1..d16851e 100644
--- a/Marches/Tropical.lean
+++ b/Marches/Tropical.lean
@@ -34,4 +34,67 @@ theorem tropical_no_return (l : Nat) (ls : List Nat) (a : Nat) :
     run TropicalNat (l :: ls) a ≠ a :=
   no_return TropicalNat tropical_strict l ls a
 
+/-! ### The grade at a crossing (rung 3)
+
+  `TropicalNat` read as a (min, +) grade, in the path algebra's own terms:
+  alternatives keep the cheaper route (`better` is `<`), sequencing adds
+  costs, and the unit of sequencing is cost `0`, the grade of the empty
+  word. choreographic-types (pinned at edb784a) records that K-CUT-LOSS
+  uses exactly two laws, `𝟙 ⊗ x ≡ x` and `x ⊕ x ≡ x` (K-4, TESTED there
+  by `scripts/minimal-laws.sh`). Both hold here. Whether this reading
+  agrees with any Agda instance is a cross-prover question: ASSUMED,
+  port-and-reprove (resource-algebra M-2 idiom). -/
+
+namespace TropicalGrade
+
+/-- Alternatives (`⊕`): keep the cheaper of two routes. -/
+def alt (a b : Nat) : Nat := min a b
+
+/-- Sequencing (`⊗`): costs add along a path. -/
+def seq (a b : Nat) : Nat := a + b
+
+/-- The unit of sequencing (`𝟙`): the cost of the empty word. -/
+def one : Nat := 0
+
+/-- K-4, first law: `𝟙 ⊗ x ≡ x`. -/
+theorem seq_unitl (x : Nat) : seq one x = x := Nat.zero_add x
+
+/-- K-4, second law: `x ⊕ x ≡ x`. -/
+theorem alt_idem (x : Nat) : alt x x = x := ite_self x
+
+/-- Extension is sequencing with the label's cost `w + 1`. -/
+theorem ext_eq_seq (w a : Nat) : TropicalNat.ext w a = seq a (w + 1) := rfl
+
+/-- The unit belongs to the empty word only: no label costs `𝟙`. This is
+    strict inflation, read as a grade. -/
+theorem label_cost_ne_one (w : Nat) : w + 1 ≠ one := fun h => Nat.noConfusion h
+
+/-- `alt` selects the `better` route. -/
+theorem alt_of_better {a b : Nat} (h : TropicalNat.better a b) : alt a b = a :=
+  Nat.min_eq_left (Nat.le_of_lt h)
+
+/-- The order `alt` induces, in resource-algebra's convention at cf9235c
+    (`a ≼ b` when `b` absorbs `a`). It is defined here for marches' own
+    grade; it is NOT the Agda `_≼_`, and no link between them is claimed. -/
+def altLe (a b : Nat) : Prop := alt a b = b
+
+/-- S-3 inside marches: `better` runs WITH cost, the induced order runs
+    AGAINST it. A better route sits ABOVE a worse one in `altLe`, as in
+    resource-algebra's Loss and opposite to its MaxPlus. Any K-CUT-WARRANT
+    bound ported here must be checked for direction (W-4). -/
+theorem better_reverses_altLe {a b : Nat} (h : TropicalNat.better a b) : altLe b a :=
+  ite_eq_right (Nat.not_le_of_gt h)
+
+/-- `𝟙` is the TOP of `altLe`: every grade is below it (as Loss's `fin 0`). -/
+theorem altLe_one : ∀ x : Nat, altLe x one
+  | 0 => rfl
+  | _ + 1 => rfl
+
+/-- Computed witness, the same numbers as resource-algebra's S-3:
+    `1` is better than `2`, and `2 ≼ 1`. -/
+theorem s3_witness : TropicalNat.better (1 : Nat) (2 : Nat) ∧ altLe 2 1 :=
+  ⟨Nat.lt_succ_self 1, rfl⟩
+
+end TropicalGrade
+
 end Marches
diff --git a/README.adoc b/README.adoc
index 33a2df6..469d5ef 100644
--- a/README.adoc
+++ b/README.adoc
@@ -32,6 +32,10 @@ no dependencies):
   discipline *and* demonstrably oscillates (`Marches/BadGadget.lean`;
   the `#eval` prints the period-2 orbit). The types reject exactly the
   policies that misbehave.
+* A region crossing is a cut: in an acyclic region DAG every crossing in
+  a well-typed trace leaves a cut and never re-enters it, and the
+  composite restricted to a cut prefix is itself a discipline whose traces
+  are exactly those ending in the prefix (`Marches/Cut.lean`).
 
 == What this is NOT
 
@@ -119,6 +123,30 @@ here (as in Gao–Rexford 2001)
 |`Marches.Acyclic` — hypothesis of `compose`, the SAME notion as the GR
 hierarchy's; never proven here
 
+|Every DAG edge crosses the principal cut of its source; an edge on a
+cycle crosses no cut
+|PROVEN (conditional)
+|`Cut.edge_crosses_past` — consumes `Acyclic`; `Cut.path_back_crosses_no_cut`
+
+|Every crossing in a well-typed trace crosses a cut that holds the trace's
+start and not its end; a trace that leaves a cut never re-enters it
+|PROVEN (conditional)
+|`Cut.DiscSys.trace_cross_crosses_cut`, `DiscSys.no_reentry`; two-region
+`Interface`: `trace_cross_crosses_cut`, `trace_stays_in_B`
+
+|`compose` restricted to a cut prefix is a discipline; its traces are
+exactly the composite's traces that end in the prefix
+|PROVEN (conditional)
+|`Cut.DiscSys.composeCut`, `composeCut_trace_embed`,
+`composeCut_trace_reflect`
+
+|`TropicalNat` as a (min,+) grade satisfies `𝟙 ⊗ x = x` and `x ⊕ x = x`
+(the two laws K-CUT-LOSS uses); its `better` runs against its ⊕-induced
+order
+|PROVEN
+|`Tropical.TropicalGrade.seq_unitl`, `alt_idem`, `better_reverses_altLe`,
+`altLe_one`, `s3_witness`
+
 |Tropical estate integration (`TropicalAdapterPath.lean`)
 |OPEN
 |rung 3
@@ -158,12 +186,16 @@ Zero dependencies; no mathlib. CI runs the same build.
 * `Marches/BadGadget.lean` — DISAGREE, the negative pincer.
 * `Marches/Freewheel.lean` — rung 1: falsifier F2 discharged; strictness
   is load-bearing.
-* `Marches/Tropical.lean` — (min,+) instance; seam for the estate's
-  tropical work.
+* `Marches/Tropical.lean` — (min,+) instance and its grade reading (the
+  two K-4 laws, the S-3 order direction); seam for the estate's tropical
+  work.
 * `Marches/Reassembly.lean` — *rung 2 headline*: `Discipline`, generic
   loop-freedom, `PathAlgebra.toDiscipline`, and `DiscSys.compose` — a
   finite acyclic DAG of disciplines is itself a discipline (reassembly
   as closure under composition).
+* `Marches/Cut.lean` — rung 3: cuts of the region DAG; every crossing
+  crosses a cut, traces never re-enter a cut they have left, and
+  `compose` restricted to a cut prefix is a discipline (prefix-closure).
 
 == Licence
 

From c10c64a1321797b8531e80b7daa3a17f5b554396 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Wed, 14 Oct 2026 01:26:41 +0000
Subject: [PATCH 2/2] docs(rung-3): K-CUT correspondence table, falsifier F6,
 ROADMAP by gates

docs/kcut-correspondence.adoc pairs marches' Lean names with
choreographic-types' Agda names, at pinned commits. It is a table, not a
link: every pairing is ASSUMED (port-and-reprove), in resource-algebra's
M-2 idiom.

scripts/fetch-siblings.sh clones choreographic-types (edb784a),
resource-algebra (cf9235c) and tropical-types (e172f8a) into
_build/dependencies. scripts/check-correspondence.sh checks that every
cited name exists (Lean in this build, Agda at its pin) and that every
pin appears in the table. Negative control: fabricated names are refused.
It checks names, not meanings.

FALSIFIERS F6 ("the correspondence is nominal") already fires on one
proposed row. Agda's `Consistent p c` is a party-indexed merge
condition, and marches has no parties, so the Acyclic <-> Consistent
pairing is withdrawn (KC-3). F6 stays open, narrowed.

Citation corrections from reading the pins:
- receiver-knows / sender-knows are in Instances.agda.
- TropicalAdapterPath.lean is in tropical-types (lake package
  tropical-resource-typing, Lean v4.13.0).
- TropicalNat is min-plus, so it is not an M-2 object.

The Tropical.lean seam note now points at M-2. ROADMAP rung 3 is a
gated table: 3a-3c met, 3d-3f OPEN. STATE.adoc records the session,
the pre-existing CI anomalies and the unreachable postern. README,
LIMITATIONS and ARCHITECTURE are updated to match.

Gates: lake build -> Build completed successfully (15 jobs);
grep -rnw sorry empty; #eval orbit unchanged;
check-correspondence.sh -> PASS (mutation test -> FAIL as expected);
shellcheck clean.

Rung: 3 (items 3a-3c met; rung stays OPEN, no tag)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
---
 .gitignore                      |   1 +
 ARCHITECTURE.adoc               |   4 +
 FALSIFIERS.adoc                 |  15 +++
 LIMITATIONS.adoc                |   5 +
 Marches/Tropical.lean           |  15 ++-
 README.adoc                     |  12 +++
 ROADMAP.adoc                    |  53 +++++++++--
 STATE.adoc                      |  78 +++++++++++++--
 docs/kcut-correspondence.adoc   | 163 ++++++++++++++++++++++++++++++++
 scripts/check-correspondence.sh |  81 ++++++++++++++++
 scripts/fetch-siblings.sh       |  28 ++++++
 11 files changed, 439 insertions(+), 16 deletions(-)
 create mode 100644 docs/kcut-correspondence.adoc
 create mode 100755 scripts/check-correspondence.sh
 create mode 100755 scripts/fetch-siblings.sh

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"