docs(rung-3): K-CUT correspondence table, falsifier F6, ROADMAP by gates

.gitignore

@@ -1 +1,2 @@
 /.lake/
+/_build/

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
 

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)
 |===

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

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

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`.

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)
 

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.