= ROADMAP — proof ladder

One rung per session. A rung is DONE when its gates pass and STATE.adoc
records the artifact. Do not start rung N+1 with rung N open.

== Rung 0 — kernel (THIS TAG, v0.1.0) ✅

Typed crossing judgment; positive theorems (worsening, empty cycles);
negative theorems (underivability); GR finite exhibit; DISAGREE pincer;
tropical instance. Gates: `lake build` green, zero `sorry`, `#eval orbit`
prints the period-2 cycle. All met 2026-07-07.

== Rung 1 — Gao–Rexford wired into Trace

* Generalise `CLabel.cross` to the three GR relations; `Trace` becomes
  the valley-freedom grammar.
* Formalise the acyclic customer→provider hierarchy as an explicit
  hypothesis; derive loop-freedom for GR *under that hypothesis*.
* Discharge falsifier F2: a non-inflationary instance with a well-typed
  returning trace (shows `hA`/`hB` load-bearing).
* Cite agda-routing in every statement that goes near convergence.

== Rung 2 — n regions and reassembly (TAG v0.3.0) ✅

* `Discipline` abstracts the shared invariant; loop-freedom proven once
  (`Discipline.no_loop`). `PathAlgebra.toDiscipline` makes the kernel an
  instance. `DiscSys.compose`: a finite acyclic DAG of disciplines is a
  discipline — composite obligation discharged from the componentwise
  ones + `Acyclic` (the by-construction counterpart of Kirigami's cut
  soundness); composites nest (`Reassembly.nestedComposed`).
* `Interface.strict` DELETED — rung 2 confirmed crossing-map
  order-preservation is never load-bearing. Met 2026-07-07.

== Rung 3 — tropical/estate integration (OPEN)

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. It lives in
hyperpolymath/tropical-types (lake package `tropical-resource-typing`) at
`e172f8a`, on Lean v4.13.0. Decided 2026-10-14: *depend, tracking latest*.
`lakefile` requires tropical-types at a pinned commit, and the weekly
re-pin bot keeps that commit current. Prerequisite, upstream in
tropical-types: build on marches' toolchain (hyperpolymath/tropical-types#65).
|`lakefile.toml` `require`; `Marches/TropicalAdapter.lean`;
`track-siblings.yml` moves the lake pin with the sibling pin
|it builds inside this repo on the pinned toolchain, unparaphrased
|met 2026-11-04 (pinned to tropical-types `168f09d`, the #65 merge
commit)

|3e. Path provenance as graded accumulation (echo-types bridge): what a
trace *carries* across an interface, not just where it may go.
|`Marches/Provenance.lean`; `docs/kcut-correspondence.adoc` KC-9 to KC-12;
echo-types pinned in `scripts/fetch-siblings.sh`
|shared Lean gates; `#print axioms` on the new declarations reports none;
`scripts/check-correspondence.sh` prints PASS with the echo-types pin
|met 2026-10-27 (bridge rows ASSUMED; F6 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)

* Announcements as attested claims: RPKI attests origin; this layer
  attests *policy*. `@record` anti-desync primitive for announcement
  provenance. Design doc first; no code before the doc.

== Rung 5 — deployment note + write-up

* Overlay/incremental-adoption note (no flag-day), IRTF-shaped paper
  skeleton in the consensus form; LIMITATIONS becomes the related-work
  section, statuses become the evaluation section.

== Handoff protocol (Opus and friends)

Every session: read `CLAUDE.md`, then `STATE.adoc`, then the current
rung here. Work only that rung. Before ending: update STATE.adoc
(what changed, what discharged, what broke), commit, and if gates pass,
tag. Statuses move only with named artifacts.