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

[hyperpolymath]

Stack 3/3 for MRC-01 (rung 3). 1/3 merged as #36 (toolchain) and 2/3 as #37 (Marches/Cut.lean + K-4 laws). This branch was cut from #37's head before its squash. main has since been merged in, without rewriting history. The squash tree is byte-identical to that head, so the diff against main is only this PR's docs and shell glue, plus one Lean comment (the Tropical.lean seam note).

What

• docs/kcut-correspondence.adoc: marches' Lean names paired 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. Rows KC-1…KC-8 cover cuts, downward closure, K-5 (cut-projectable), K-2 (proj-cut), the K-4 laws, the S-3/W-4 direction, and M-2.
• scripts/fetch-siblings.sh: clones the siblings at their pins into _build/dependencies (now git-ignored), using the choreographic-types pattern. Pins: choreographic-types edb784a, resource-algebra cf9235c, tropical-types e172f8a.
• scripts/check-correspondence.sh: the mechanical part. It checks that every Lean name cited exists in this build (#check), that every Agda name exists at its pin, and that every pin appears in the table. Negative control: a fabricated Lean name and a fabricated Agda name go through the same checks and must be refused. It checks names, not meanings.
• FALSIFIERS.adoc F6: "the correspondence is nominal." It fires on one proposed row. At edb784a, Agda's Consistent p c (Projection.agda:89) is a party-indexed merge condition at choices, and marches has no parties. So MRC-01's Acyclic ↔ Consistent pairing is withdrawn (KC-3, status OPEN). F6 stays open, narrowed.
• Marches/Tropical.lean seam note: now points at resource-algebra M-2, and records where TropicalAdapterPath.lean actually lives (below).
• ROADMAP.adoc rung 3: now a gated table. 3a–3c are met; 3d (TropicalAdapterPath import), 3e (echo-types bridge) and 3f (postern) are OPEN, so the rung stays OPEN and there is no tag.
• STATE.adoc: records the session. README gets one ASSUMED row and a note on the check script; LIMITATIONS gets one bullet; ARCHITECTURE lists docs/ and scripts/.

Citation corrections found while reading the pins

• T-2's receiver-knows / sender-knows are in src/Choreographic/Instances.agda (lines 172 and 177), not Transport.agda. Transport.agda holds the generic knows-local-cut.
• TropicalAdapterPath.lean is in hyperpolymath/tropical-types. Its lake package is named tropical-resource-typing, which is the name the ROADMAP used. It is pinned to Lean v4.13.0, so expect friction when 3d imports it into v4.34.0.
• marches' TropicalNat is min-plus, so it sits with Loss, not MaxPlus. It is not one of M-2's two (max-plus) objects (KC-8).

Evidence (this head)

$ lake build
Build completed successfully (15 jobs).
$ grep -rnw sorry Marches/ Marches.lean ; echo $?
1
$ lake env lean Marches/BadGadget.lean
[(false, false), (true, true), (false, false), (true, true)]
$ scripts/check-correspondence.sh
choreographic-types at edb784a
resource-algebra at cf9235c
tropical-types at e172f8a
PASS: 15 Lean names and 16 sibling names exist at the pins; both negative controls refused
$ shellcheck scripts/*.sh   # clean
$ grep -ni converg Marches/Cut.lean docs/kcut-correspondence.adoc scripts/*.sh
Marches/Cut.lean:45:  not protocol convergence; agda-routing owns that ground (LIMITATIONS.adoc).
docs/kcut-correspondence.adoc:20:Delimitation: nothing here is a convergence claim; agda-routing owns that

Mutation test: I renamed one Lean name, one Agda name and one pin in the doc. The script printed MISSING (Lean), MISSING (sibling) and PIN NOT IN TABLE, then FAIL with exit 1. Restoring the doc gives PASS again.

postern

Not reachable from this account on 2026-10-14 (add_repo: not found or no access; no list_repos match). No cross-issue was filed. The MRC-01 import plan is kept in the correspondence doc, ready to file.

CI

The same two pre-existing red checks as on main apply here, and neither is caused by this PR:

• CI ends in startup_failure: actions.lock has drifted since chore(deps): bump the actions group with 2 updates #34. The fix is gh actions-lock, as in chore(actions): relock drifted action pins #25.
• estate-audit fails because of a cicd-suite pipefail bug on a comment-only CODEOWNERS.

The full diagnosis is in #37. check-correspondence.sh needs network access, so it is not wired into CI here.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX

---

Generated by Claude Code

[coderabbitai]

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 36 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: 6987b939-e5bf-4cc5-a74c-3871bd6abd8a

📥 Commits

Reviewing files that changed from the base of the PR and between 3ca64b4 and 3600a07.

📒 Files selected for processing: 11

• .gitignore
• ARCHITECTURE.adoc
• FALSIFIERS.adoc
• LIMITATIONS.adoc
• Marches/Tropical.lean
• README.adoc
• ROADMAP.adoc
• STATE.adoc
• docs/kcut-correspondence.adoc
• scripts/check-correspondence.sh
• scripts/fetch-siblings.sh

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[hyperpolymath]

estate-audit is red, but not because of this PR. It fails the same way on main (runs 42, 44, 46) and on every recent PR. I reproduced it locally against the pinned hyperpolymath/cicd-suite@5a10b72. The Required Files Gate runs under bash -e -o pipefail. For this repo's comment-only .github/CODEOWNERS, functional_lines=$(grep -vE '^\s*(#|//|;|$)' "$f" | wc -l) selects no lines, so grep exits 1 and pipefail fails the assignment. The step then exits with no ::error:: line, which is the very case the gate's own "Rule 1" means to allow. No fix exists yet. It belongs in cicd-suite, e.g. functional_lines=$({ grep -vE '…' "$f" || true; } | wc -l). I haven't re-run it, because it fails the same way every time.

CI (lake build + no-sorries) ends in startup_failure here as on main. .github/workflows/actions.lock still pins lean-action@v1.6.0 / codeql-action@v4.38.0, while the workflows were bumped in #34. No fix PR exists. Running gh actions-lock on main (as #25 did) fixes it. Until then, the build evidence is the local gate output in the PR body.

---

Generated by Claude Code