feat(rung-3): a region crossing is a cut; K-4 laws over TropicalNat

[hyperpolymath]

Stack 2/3 for MRC-01 (rung 3). Stack 1/3, the toolchain move to v4.34.0, merged as #36. Next: …-docs (correspondence table, falsifier, STATE/ROADMAP), stacked on this branch.

Marches/Cut.lean (new)

A cut of the region DAG is a set of regions closed under predecessors: every region that can cross into the cut is in it. This is classical downward closure. It is not choreographic-types' party-indexed Consistent, which is a merge condition at choices; the next PR in the stack records that as a falsifier finding.

Theorem	Says
Cut.edge_crosses_past	In an acyclic graph every edge r → r' leaves the principal cut ↓r.
Cut.path_back_crosses_no_cut	Negative: an edge on a cycle crosses no cut. Acyclic 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, trace_inside	A trace that ends in a cut was inside it all along, and fired every label inside it.
DiscSys.no_reentry	A trace that leaves a cut never re-enters it. This is no_back_cross lifted from one interface to every cut.
DiscSys.composeCut	Prefix-closure: compose restricted to a cut prefix is a Discipline.
composeCut_trace_embed / composeCut_trace_reflect	Its traces are exactly the composite's traces that end in the prefix: the frontier's future is irrelevant to the prefix.
trace_cross_crosses_cut, trace_stays_in_B	The same results for the two-region Interface of Compose.lean, read as the 2-node DAG Reassembly.boolUp.
CutExhibit.*	A concrete twoTropical trace that instantiates the theorems, plus a negative control on a self-loop.

Marches/Tropical.lean: the grade at the crossing

TropicalGrade reads TropicalNat as a (min,+) grade: alt = min, seq = +, one = 0.

• K-4 laws: seq_unitl (𝟙 ⊗ x = x) and alt_idem (x ⊕ x = x).
• S-3 inside marches: better_reverses_altLe. better runs with cost, while the ⊕-induced order runs against it, as in resource-algebra's Loss and opposite to its MaxPlus. altLe_one puts 𝟙 at the top, as Loss's fin 0. s3_witness uses the same numbers as resource-algebra's S-3 (2 ≼ 1).
• The Agda side is not imported or re-declared. altLe is marches' own order, and the doc comment says so.

Evidence (local, Lean v4.34.0)

$ rm -rf .lake && 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)]

#print axioms over all 45 declarations added in Cut.lean and TropicalGrade: every one reports does not depend on any axioms. I re-proved three grade lemmas that had picked up propext through core Nat lemmas, to match the existing kernel, which is also axiom-free.

grep -ni converg Marches/Cut.lean → only the delimitation line (45).

CI: two red checks that are not this PR's

• CI (the lake build + no-sorries job) ends in startup_failure. This has happened on every run since the Dependabot bump chore(deps): bump the actions group with 2 updates #34 (runs 78–81, including on main). That bump moved ci.yml to leanprover/lean-action@v1.6.1 and codeql.yml to codeql-action@v4.38.2, but .github/workflows/actions.lock still pins @v1.6.0 / @v4.38.0. The lockfile is enforced at startup ("Using locked action versions from the workflow's lockfile"). Fix: re-run gh actions-lock on main, as chore(actions): relock drifted action pins #25 did. I have not hand-edited the machine-generated lockfile. Until that lands, the local gate output above is the build evidence.
• estate-audit fails at the Required Files Gate. This is red on main since at least run 41 (1 Oct). Reproduced locally against cicd-suite@5a10b72: the gate runs under bash -e -o pipefail, and for this repo's comment-only .github/CODEOWNERS, functional_lines=$(grep -vE '^\s*(#|//|;|$)' "$f" | wc -l) selects no lines. grep exits 1, pipefail fails the assignment, and the step exits with no ::error::. That is the very case the gate's "Rule 1" means to allow. The fix belongs in hyperpolymath/cicd-suite, e.g. { grep -vE … "$f" || true; } | wc -l.

Status rows

New README rows are PROVEN by lake build, and "conditional" where they consume Acyclic. No cross-prover claim is made in this PR. Rung 3 stays OPEN.

🤖 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 45 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: 47561225-a1fc-4bac-9763-850f24306666

📥 Commits

Reviewing files that changed from the base of the PR and between 1152b03 and 1ea9a85.

📒 Files selected for processing: 4

• Marches.lean
• Marches/Cut.lean
• Marches/Tropical.lean
• README.adoc

• 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.}