chore(siblings): re-pin tropical-types to the #65 merge commit; close rung 3d

ROADMAP.adoc

@@ -70,8 +70,8 @@ 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 on a PR-head pin 2026-10-27; re-pin to the tropical-types#65 merge
-commit closes it
+|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.

STATE.adoc

@@ -1,5 +1,48 @@
 = STATE — cross-session log
 
+== 2026-11-04 — rung 3d closed: tropical-types re-pinned to the #65 merge commit
+
+* #52 merged before hyperpolymath/tropical-types#65, so `main` kept the
+  PR-head pin `226c9e1`. #65 squash-merged as `168f09d` and its branch was
+  deleted; `226c9e1` is then on no branch, and a fresh clone's
+  `git fetch origin` never brings it in. Reproduced:
+  `TROPICAL_TYPES_COMMIT=226c9e1… scripts/fetch-siblings.sh` on an empty
+  `_build/dependencies` → `fatal: reference is not a tree: 226c9e1…`.
+* That is why the 2026-11-02 `track-siblings` run filed #54
+  (choreographic-types) and #55 (resource-algebra): both checks died on
+  the tropical-types fetch, not on a lost name. With the fixed pin, both
+  siblings at their current HEADs (`8751c7d`, `e25d35d`) give PASS. The
+  next weekly run re-pins them.
+* The same run had already committed the right re-pins on
+  `ci/track-siblings` (tropical-types → `168f09d`, echo-types → `b0982c4`)
+  and failed only at `gh pr create` (Actions may not open PRs without
+  `AUTOMATION_TOKEN`). Those two commits are cherry-picked here with `-x`,
+  authorship kept. `168f09d` and `226c9e1` have identical Lean trees
+  (`git diff --stat` over `*.lean`, `lean-toolchain`, `lakefile.lean` is
+  empty).
+* F6, echo-types `1073d60..b0982c4`: one commit, and it touches neither
+  `proofs/agda/Echo.agda` nor `proofs/agda/EchoProvenance.agda`.
+* #52's squash also carries CodeRabbit's autofix of `track-siblings.yml`
+  (its Major finding: build candidate pins without the write token). Read
+  after the fact: a read-only `check` job builds and passes patches and
+  JSON as data; `publish` holds the token, applies only patches touching
+  the four pin files, and still exits red on broken names. shellcheck on
+  both extracted run blocks: clean except SC2153 (info, `BASE` comes from
+  `env:`), which actionlint 1.7.7 also reports.
+* Gates on v4.35.0 at `168f09d`, from an empty `_build/dependencies`:
++
+----
+$ lake build
+Build completed successfully (19 jobs).
+$ grep -rnw sorry Marches/ Marches.lean  # empty
+$ lake env lean Marches/BadGadget.lean
+[(false, false), (true, true), (false, false), (true, true)]
+$ scripts/check-correspondence.sh
+PASS: 28 Lean names and 22 sibling names exist at the pins; both negative controls refused
+----
+* ROADMAP 3d: met. Rung 3 stays OPEN on 3f only (postern: `list_repos`
+  query `postern` empty). No tag.
+
 == 2026-10-27 — rung 3d: TropicalAdapterPath imported, unparaphrased
 
 * Upstream prerequisite: hyperpolymath/tropical-types#65 moves that
@@ -389,11 +432,6 @@ $ lake env lean Marches/BadGadget.lean
 
 == Next action
 
-Rung 3 (see ROADMAP.adoc), the remaining items. 3d: once
-hyperpolymath/tropical-types#65 merges, re-pin `lakefile.toml`,
-`lake-manifest.json`, `scripts/fetch-siblings.sh` and the correspondence
-pin table to its merge commit (one sed of the SHA; then `lake build` and
-`scripts/check-correspondence.sh`). 3e: met 2026-10-27
-(`Marches/Provenance.lean`). 3f: file the postern cross-issue once that
-repository exists. Obtain the real files; never reconstruct from memory.
-One rung only.
+Rung 3 (see ROADMAP.adoc): only 3f remains. File the postern cross-issue
+once that repository exists (not found 2026-11-04). 3d and 3e are met.
+Obtain the real files; never reconstruct from memory. One rung only.

docs/kcut-correspondence.adoc

@@ -35,11 +35,11 @@ ground (`LIMITATIONS.adoc`).
 |`_≼_` convention, `Loss`, `MaxPlus`, S-3 witnesses, M-2 status
 
 |hyperpolymath/tropical-types
-|`226c9e191e0ab966f094a6394f0958cdc28254e0`
+|`168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5`
 |`TropicalAdapterPath.lean` (also IMPORTED: the lake `require` in `lakefile.toml` is at this same commit), `TropicalSessionTypes.lean` (the Lean side of M-2)
 
 |hyperpolymath/echo-types
-|`1073d600004d13f1aec7363baa0ee2e38d91568e`
+|`b0982c44f36133acd2d0e1d4e03cf031fff7a470`
 |`Echo`, `echo-intro` (the fibre); `Provenance`, `provenance-collapses-at`,
 `echoes-distinguish-tag` (the audience-facing provenance theorems)
 |===

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "226c9e191e0ab966f094a6394f0958cdc28254e0",
+   "rev": "168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5",
    "name": "«tropical-resource-typing»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "226c9e191e0ab966f094a6394f0958cdc28254e0",
+   "inputRev": "168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "marches",

lakefile.toml

@@ -11,4 +11,4 @@ name = "Marches"
 [[require]]
 name = "tropical-resource-typing"
 git = "https://github.com/hyperpolymath/tropical-types"
-rev = "226c9e191e0ab966f094a6394f0958cdc28254e0"
+rev = "168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5"

scripts/fetch-siblings.sh

@@ -13,8 +13,8 @@ cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 
 CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-f5a41772c2ca2345bd53579b73f064f4a3ab7ed7}"
 RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-e9482657aa791678e1d99996a18fb3e126e0d3c2}"
-TROPICAL_TYPES_COMMIT="${TROPICAL_TYPES_COMMIT:-226c9e191e0ab966f094a6394f0958cdc28254e0}"
-ECHO_TYPES_COMMIT="${ECHO_TYPES_COMMIT:-1073d600004d13f1aec7363baa0ee2e38d91568e}"
+TROPICAL_TYPES_COMMIT="${TROPICAL_TYPES_COMMIT:-168f09d1df8bc239d41bc0f9d9d18575b2c9c9d5}"
+ECHO_TYPES_COMMIT="${ECHO_TYPES_COMMIT:-b0982c44f36133acd2d0e1d4e03cf031fff7a470}"
 
 # Fetch a sibling repository and check out its pinned commit.
 # Arguments: $1 is the repository name under hyperpolymath; $2 is the commit.