feat(tropical): rung 3d, import TropicalAdapterPath unparaphrased

.github/workflows/track-siblings.yml

@@ -11,11 +11,17 @@ name: Track latest siblings
 # - A cited name is gone at HEAD → an issue with the check's output; the pin
 #   stays put.
 #
+# tropical-types is also a lake `require` (rung 3d): its re-pin moves
+# lakefile.toml and lake-manifest.json too, and the re-check's `lake build`
+# must pass against the new HEAD, or the pin stays and an issue is filed.
+#
 # Names only. Whether a re-pinned name still MEANS the same thing is falsifier
 # F6, and no script decides it: the PR asks for the sibling diff to be read.
 #
 # ⚠ NO `uses:` (see labels.yml): Lean comes from elan's installer.
-# Token: AUTOMATION_TOKEN if set (see actions-lock.yml), else GITHUB_TOKEN.
+# The check job has read-only permissions and no token in its environment.
+# Only publish uses AUTOMATION_TOKEN (see actions-lock.yml), else GITHUB_TOKEN.
+# Job outputs carry patches and issue text as data; publish never builds them.
 
 on:
   schedule:
@@ -30,30 +36,34 @@ concurrency:
   cancel-in-progress: false
 
 jobs:
-  repin:
+  check:
     runs-on: ubuntu-latest
     permissions:
-      contents: write
-      issues: write
-      pull-requests: write
+      contents: read
+    outputs:
+      base: ${{ steps.check.outputs.base }}
+      patches: ${{ steps.check.outputs.patches }}
+      repinned: ${{ steps.check.outputs.repinned }}
+      issues: ${{ steps.check.outputs.issues }}
     env:
-      GH_TOKEN: ${{ secrets.AUTOMATION_TOKEN || secrets.GITHUB_TOKEN }}
       BASE: main
       BRANCH: ci/track-siblings
     steps:
       - name: Check the correspondence against sibling HEADs and re-pin
+        id: check
         run: |
           set -euo pipefail
-          gh auth setup-git
-          gh repo clone "$GITHUB_REPOSITORY" repo -- --quiet --depth 1 --branch "$BASE"
+          git clone --quiet --depth 1 --branch "$BASE" "https://github.com/$GITHUB_REPOSITORY.git" repo
           cd repo
           curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
             | sh -s -- -y --default-toolchain none --no-modify-path
           export PATH="$HOME/.elan/bin:$PATH"
           run_url="$GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"
+          base=$(git rev-parse HEAD)
           git switch --quiet -c "$BRANCH"
-
-          repinned=(); broken=()
+          report=$(mktemp -d)
+          printf '[]\n' > "$report/issues.json"
+          printf '[]\n' > "$report/repinned.json"
           for spec in choreographic-types:CHOREOGRAPHIC_TYPES_COMMIT \
                       resource-algebra:RESOURCE_ALGEBRA_COMMIT \
                       tropical-types:TROPICAL_TYPES_COMMIT \
@@ -64,41 +74,107 @@ jobs:
             echo "$repo: pinned ${pinned:0:7}, HEAD ${head:0:7}"
             [ "$pinned" = "$head" ] && continue
 
-            out=$(mktemp)
+            out=$(mktemp); ok=0
             if env "$var=$head" scripts/check-correspondence.sh >"$out" 2>&1; then
-              sed -i "s/$pinned/$head/g" scripts/fetch-siblings.sh docs/kcut-correspondence.adoc
-              if ! scripts/check-correspondence.sh >"$out" 2>&1; then
-                echo "::error::$repo re-pin did not re-check"; cat "$out"; exit 1
-              fi
+              # tropical-types is also a lake `require` at the same commit
+              # (rung 3d): move the lakefile and manifest pins with it, so the
+              # re-check's `lake build` builds marches against the new HEAD.
+              # If that fails, restore the pins and report it like a lost name.
+              sed -i "s/$pinned/$head/g" scripts/fetch-siblings.sh docs/kcut-correspondence.adoc \
+                lakefile.toml lake-manifest.json
+              if scripts/check-correspondence.sh >"$out" 2>&1; then ok=1
+              else git checkout --quiet -- .; fi
+            fi
+            if [ "$ok" -eq 1 ]; then
               git -c user.name='github-actions[bot]' \
                   -c user.email='41898583+github-actions[bot]@users.noreply.github.com' \
                   commit --quiet -am "chore(siblings): re-pin $repo to ${head:0:7}" \
                   -m "Weekly track-siblings run: $run_url. $(tail -n 1 "$out")"
-              repinned+=("$repo ${pinned:0:7} → ${head:0:7} (https://github.com/hyperpolymath/$repo/compare/$pinned...$head)")
+              jq --arg entry "$repo ${pinned:0:7} → ${head:0:7} (https://github.com/hyperpolymath/$repo/compare/$pinned...$head)" \
+                '. + [$entry]' "$report/repinned.json" > "$report/next.json"
+              mv "$report/next.json" "$report/repinned.json"
             else
               title="Sibling $repo at HEAD breaks the K-CUT correspondence names"
               # shellcheck disable=SC2016  # literal Markdown backticks
-              body=$(printf 'Weekly check (%s): docs/kcut-correspondence.adoc against hyperpolymath/%s HEAD `%s` (pinned: `%s`). The pin stays put.\n\n```\n%s\n```\n' \
+              body=$(printf 'Weekly check (%s): docs/kcut-correspondence.adoc (and, for tropical-types, `lake build`) against hyperpolymath/%s HEAD `%s` (pinned: `%s`). The pin stays put.\n\n```\n%s\n```\n' \
                 "$run_url" "$repo" "$head" "$pinned" "$(tail -n 40 "$out")")
-              existing=$(gh issue list --state open --search "in:title \"$title\"" --json number --jq '.[0].number // empty')
-              if [ -n "$existing" ]; then gh issue comment "$existing" --body "$body"
-              else gh issue create --title "$title" --body "$body"; fi
-              broken+=("$repo")
+              jq --arg title "$title" --arg body "$body" --arg repo "$repo" \
+                '. + [{title: $title, body: $body, repo: $repo}]' \
+                "$report/issues.json" > "$report/next.json"
+              mv "$report/next.json" "$report/issues.json"
             fi
           done
 
-          if [ "${#repinned[@]}" -gt 0 ]; then
+          # No candidate code runs in the later job. Transfer only commit
+          # patches and JSON reports, without actions that need a lock entry.
+          git format-patch --stdout "$base..HEAD" > "$report/patches"
+          {
+            printf 'base=%s\n' "$base"
+            printf 'patches=%s\n' "$(base64 -w0 < "$report/patches")"
+            printf 'repinned=%s\n' "$(jq -c . "$report/repinned.json")"
+            printf 'issues=%s\n' "$(jq -c . "$report/issues.json")"
+          } >> "$GITHUB_OUTPUT"
+
+  publish:
+    needs: check
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+      issues: write
+      pull-requests: write
+    env:
+      GH_TOKEN: ${{ secrets.AUTOMATION_TOKEN || secrets.GITHUB_TOKEN }}
+      BASE: main
+      BRANCH: ci/track-siblings
+      CHECKED_BASE: ${{ needs.check.outputs.base }}
+      PATCHES: ${{ needs.check.outputs.patches }}
+      REPINNED: ${{ needs.check.outputs.repinned }}
+      ISSUES: ${{ needs.check.outputs.issues }}
+    steps:
+      - name: Publish correspondence issues and re-pin PR
+        run: |
+          set -euo pipefail
+          gh auth setup-git
+          gh repo clone "$GITHUB_REPOSITORY" repo -- --quiet --depth 1 --branch "$BASE"
+          cd repo
+          run_url="$GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID"
+
+          # Treat the read-only job's outputs as data, never shell commands.
+          while IFS= read -r issue; do
+            title=$(jq -r '.title' <<< "$issue")
+            body=$(jq -r '.body' <<< "$issue")
+            existing=$(gh issue list --state open --search "in:title \"$title\"" --json number --jq '.[0].number // empty')
+            if [ -n "$existing" ]; then gh issue comment "$existing" --body "$body"
+            else gh issue create --title "$title" --body "$body"; fi
+          done < <(jq -c '.[]' <<< "$ISSUES")
+
+          if [ "$(jq 'length' <<< "$REPINNED")" -gt 0 ]; then
+            [[ "$CHECKED_BASE" =~ ^[0-9a-f]{40}$ ]]
+            git fetch --quiet origin "$CHECKED_BASE"
+            git switch --quiet -c "$BRANCH" "$CHECKED_BASE"
+            printf '%s' "$PATCHES" | base64 --decode > "$RUNNER_TEMP/repin.patch"
+            git -c core.hooksPath=/dev/null \
+                -c user.name='github-actions[bot]' \
+                -c user.email='41898583+github-actions[bot]@users.noreply.github.com' \
+                am --quiet "$RUNNER_TEMP/repin.patch"
+            # Refuse patches outside the four files used for re-pinning.
+            while IFS= read -r -d '' path; do
+              case "$path" in
+                scripts/fetch-siblings.sh|docs/kcut-correspondence.adoc|lakefile.toml|lake-manifest.json) ;;
+                *) echo "::error::Unexpected re-pin path: $path"; exit 1 ;;
+              esac
+            done < <(git diff --name-only -z "$CHECKED_BASE" HEAD)
             git push --quiet --force origin "$BRANCH"
             # shellcheck disable=SC2016  # literal Markdown backticks
             body=$(printf 'Weekly re-pin (%s). Every name docs/kcut-correspondence.adoc cites still exists at the new pins, and both negative controls are refused (`scripts/check-correspondence.sh`).\n\n%s\n\n**Names only.** Read each sibling diff above before merging: whether a name still means the same thing is falsifier F6.\n' \
-              "$run_url" "$(printf -- '- %s\n' "${repinned[@]}")")
+              "$run_url" "$(jq -r '.[] | "- " + .' <<< "$REPINNED")")
             if [ -n "$(gh pr list --head "$BRANCH" --state open --json number --jq '.[].number')" ]; then
               gh pr edit "$BRANCH" --body "$body"
             else
               gh pr create --base "$BASE" --head "$BRANCH" --title "chore(siblings): re-pin to latest" --body "$body"
             fi
           fi
-          if [ "${#broken[@]}" -gt 0 ]; then
-            echo "::error::names broken at HEAD for: ${broken[*]} (issues filed)"
+          if [ "$(jq 'length' <<< "$ISSUES")" -gt 0 ]; then
+            echo "::error::names broken at HEAD for: $(jq -r 'map(.repo) | join(" ")' <<< "$ISSUES") (issues filed)"
             exit 1
           fi

Marches.lean

@@ -11,3 +11,4 @@ import Marches.Freewheel
 import Marches.Reassembly
 import Marches.Cut
 import Marches.Provenance
+import Marches.TropicalAdapter

Marches/Tropical.lean

@@ -6,11 +6,12 @@
   extension adds weight + 1 (positive weights ⇒ strictness).
 
   This file is the seam for integrating the estate's existing
-  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.
+  fully proved tropical work. `TropicalAdapterPath.lean` lives in
+  hyperpolymath/tropical-types (lake package `tropical-resource-typing`),
+  required in lakefile.toml at a pinned commit and imported unparaphrased
+  by `Marches/TropicalAdapter.lean` (rung 3d). Nothing in THIS file
+  depends on it: `TropicalNat` (min-plus) is not upstream's min-max
+  transport semiring.
 
   The cross-prover bridge is resource-algebra's M-2 (pinned in scripts/fetch-siblings.sh):
   Agda `MaxPlus` vs tropical-types' Lean `CommSemiring Tropical`, OPEN,

Marches/TropicalAdapter.lean

@@ -0,0 +1,77 @@
+/-
+  Marches — the estate's tropical proofs, imported (rung 3d).
+
+  `TropicalAdapterPath` is hyperpolymath/tropical-types' fully proved
+  min-max ("bottleneck") transport semiring, required in `lakefile.toml`
+  at a pinned commit and imported here UNPARAPHRASED: nothing below
+  re-states or re-proves its contents. This file only connects it to
+  marches' own machinery, through upstream's own theorems.
+
+    • TropicalAdapter.bottleneck     : upstream's `⊗` (`tcMul` = max, unit
+                                       `tcOne` = 0) is a marches `Grade`; all
+                                       three laws are upstream's.
+    • TropicalAdapter.pathCost_eq_accum : upstream's `pathCost` IS marches'
+                                       `Grade.accum` of transport grades
+                                       under `bottleneck`.
+    • TropicalAdapter.carried_floor  : every step on a path floors the grade
+                                       the path carries (upstream's
+                                       `hub_ceiling`, read as provenance).
+    • TropicalAdapter.bottleneck_carries_unit : a NON-empty path can carry
+                                       the unit `𝟙` (one Concorde step). So
+                                       `bottleneck`, unlike `TropicalGrade`,
+                                       is not strictly inflationary as a
+                                       grade: `carried_cons_ne_one` has no
+                                       analogue, and no loop-freedom follows
+                                       from it (the F2 lesson, again).
+
+  The min-max semiring is neither marches' `TropicalNat` (min-plus) nor
+  M-2's max-plus; see docs/kcut-correspondence.adoc (KC-13). Delimitation
+  unchanged: nothing here is protocol convergence (LIMITATIONS.adoc).
+-/
+
+import TropicalAdapterPath
+import Marches.Provenance
+
+namespace Marches
+namespace TropicalAdapter
+
+open Hyperpolymath.ProtocolSquisher.Tropical
+
+/-- The bottleneck grade: upstream's min-max `⊗` as a marches `Grade`.
+    Every law is an upstream theorem. -/
+def bottleneck : Grade where
+  G := Nat
+  seq := tcMul
+  one := tcOne
+  seq_assoc := tcMul_assoc
+  seq_unitl := tcMul_one_left
+  seq_unitr := tcMul_one_right
+
+/-- Upstream's path cost is marches' accumulation: the bottleneck grade a
+    path of transport steps carries. -/
+theorem pathCost_eq_accum : ∀ p : AdapterPath, pathCost p = bottleneck.accum grade p
+  | [] => rfl
+  | c :: cs =>
+    (pathCost_cons c cs).trans (congrArg (Nat.max (grade c)) (pathCost_eq_accum cs))
+
+/-- Upstream's `pathCost_append`, recovered from marches' `accum_append`:
+    the two developments agree on concatenation. -/
+theorem pathCost_append_via_accum (p q : AdapterPath) :
+    pathCost (p ++ q) = tcMul (pathCost p) (pathCost q) := by
+  rw [pathCost_eq_accum, pathCost_eq_accum, pathCost_eq_accum]
+  exact bottleneck.accum_append grade p q
+
+/-- Every step on a path floors the grade the path carries: upstream's
+    `hub_ceiling`, read as provenance. -/
+theorem carried_floor (e : TransportClass) (p : AdapterPath) (h : e ∈ p) :
+    grade e ≤ bottleneck.accum grade p :=
+  pathCost_eq_accum p ▸ hub_ceiling e p h
+
+/-- A non-empty path can carry the unit: one Concorde step carries `𝟙`.
+    Contrast `TropicalGrade.carried_cons_ne_one`. -/
+theorem bottleneck_carries_unit :
+    bottleneck.accum grade [TransportClass.Concorde] = bottleneck.one :=
+  rfl
+
+end TropicalAdapter
+end Marches

README.adoc

@@ -179,9 +179,18 @@ echo-types' `Echo` and provenance theorems
 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
+|Tropical estate integration: tropical-types' `TropicalAdapterPath.lean`
+builds inside this repo, unparaphrased, and its `pathCost` is marches'
+grade accumulation under the bottleneck grade
+|PROVEN
+|`lake build` with the `lakefile.toml` `require`;
+`TropicalAdapter.pathCost_eq_accum`, `pathCost_append_via_accum`,
+`carried_floor`, `bottleneck_carries_unit`
+
+|The bottleneck grade gives no loop-freedom: a non-empty path can carry
+the unit
+|PROVEN (finite)
+|`TropicalAdapter.bottleneck_carries_unit`
 
 |Protocol-level asynchronous convergence
 |OUT OF SCOPE
@@ -247,6 +256,9 @@ A red result opens an issue instead of a PR.
   start `⊗` carried; a crossing trace is A-word, crossing, B-word, and
   carries the A-signature into the fibre of `τ`; in the DAG the grade
   reaching a cut or a crossing is accumulated inside the prefix.
+* `Marches/TropicalAdapter.lean` — rung 3d: imports tropical-types'
+  `TropicalAdapterPath` unparaphrased (a lake `require`); its min-max `⊗`
+  is a marches `Grade`, and its `pathCost` is that grade's accumulation.
 
 == Licence
 

ROADMAP.adoc

@@ -66,10 +66,12 @@ 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.
-|—
+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
-|OPEN
+|met on a PR-head pin 2026-10-27; re-pin to the tropical-types#65 merge
+commit closes it
 
 |3e. Path provenance as graded accumulation (echo-types bridge): what a
 trace *carries* across an interface, not just where it may go.