feat(provenance): rung 3e, path provenance as graded accumulation

.github/workflows/track-siblings.yml

@@ -2,7 +2,7 @@
 name: Track latest siblings
 
 # Weekly: for each sibling proof repository pinned in scripts/fetch-siblings.sh
-# (choreographic-types, resource-algebra, tropical-types), check
+# (choreographic-types, resource-algebra, tropical-types, echo-types), check
 # docs/kcut-correspondence.adoc against the sibling's current HEAD.
 #
 # - Every cited name still exists at HEAD → re-pin: one commit per sibling,
@@ -56,7 +56,8 @@ jobs:
           repinned=(); broken=()
           for spec in choreographic-types:CHOREOGRAPHIC_TYPES_COMMIT \
                       resource-algebra:RESOURCE_ALGEBRA_COMMIT \
-                      tropical-types:TROPICAL_TYPES_COMMIT; do
+                      tropical-types:TROPICAL_TYPES_COMMIT \
+                      echo-types:ECHO_TYPES_COMMIT; do
             repo="${spec%%:*}"; var="${spec#*:}"
             pinned=$(grep -E "^${var}=" scripts/fetch-siblings.sh | grep -oE '[0-9a-f]{40}')
             head=$(git ls-remote "https://github.com/hyperpolymath/$repo.git" HEAD | cut -f1)

FALSIFIERS.adoc

@@ -62,6 +62,11 @@ refused). It cannot check meaning. Read at choreographic-types `edb784a`
 marches has no parties, and its cut condition (downward closure,
 `Cut.closed`) is what Agda's `Cut` has by construction. The
 `Acyclic ↔ Consistent` pairing is withdrawn (KC-3). The rest stand
-ASSUMED until a port re-proves them.
+ASSUMED until a port re-proves them. Rung 3e (2026-10-27) adds the
+echo-types rows KC-9 and KC-10: `Echo` is the preimage fibre on both
+sides, so the shared content is small by construction, and echo-types'
+own claim (taxonomy, separation, residues on top of the fibre) is not
+paired. KC-12 records that accumulation needs the `⊗`-monoid, which K-4
+does not supply: a different law set, not a disagreement.
 |open (narrowed)
 |===

Marches.lean

@@ -10,3 +10,4 @@ import Marches.Tropical
 import Marches.Freewheel
 import Marches.Reassembly
 import Marches.Cut
+import Marches.Provenance

README.adoc

@@ -147,8 +147,33 @@ order
 |`Tropical.TropicalGrade.seq_unitl`, `alt_idem`, `better_reverses_altLe`,
 `altLe_one`, `s3_witness`
 
+|In one tropical region the end signature of a run is the start `⊗` the
+grade its word carried, and a non-empty word carries a non-unit grade
+|PROVEN
+|`Provenance.TropicalGrade.run_eq_seq_carried`, `carried_cons_ne_one`,
+`no_return_of_carried`
+
+|A well-typed two-region trace that crosses is an A-word, the crossing,
+then a B-word; what crosses is the A-signature at the crossing, which B
+sees only through `τ` (its fibre is `Interface.fibre`)
+|PROVEN
+|`Provenance.trace_cross_shape`, `Interface.carried`, `trace_cross_lands`
+
+|In the region DAG, the grade reaching a point inside a cut, or a crossing
+out of `↓r`, is accumulated by a trace of the cut prefix alone
+|PROVEN (conditional)
+|`Provenance.DiscSys.carried_in_cut`, `carried_to_cross_in_past`;
+conditional on `Acyclic`, as every `compose` theorem is
+
+|A collapsing crossing forgets the A-grade, and the fibre over the landing
+point still tells two such traces apart
+|PROVEN (finite)
+|`Provenance.ProvenanceExhibit.zero_forgets`, `zero_fibre_distinguishes`,
+`collapse₀`, `collapse₁`; `id_carries` for the identity crossing
+
 |marches' cuts and grade laws correspond to choreographic-types' K-CUT
-(`proj-cut`, `cut-projectable`, K-4)
+(`proj-cut`, `cut-projectable`, K-4), and its crossing fibre to
+echo-types' `Echo` and provenance theorems
 |ASSUMED (port-and-reprove)
 |`docs/kcut-correspondence.adoc`. A table of names, not a link. Names are
 checked at their pins by `scripts/check-correspondence.sh`. Falsifier F6
@@ -217,6 +242,11 @@ A red result opens an issue instead of a PR.
 * `Marches/Cut.lean` — rung 3: cuts of the region DAG; every crossing
   crosses a cut, traces never re-enter a cut they have left, and
   `compose` restricted to a cut prefix is a discipline (prefix-closure).
+* `Marches/Provenance.lean` — rung 3e: what a trace carries. Words
+  accumulate a grade (a monoid homomorphism); a tropical run ends at
+  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.
 
 == Licence
 

ROADMAP.adoc

@@ -73,9 +73,11 @@ tropical-types: build on marches' toolchain.
 
 |3e. Path provenance as graded accumulation (echo-types bridge): what a
 trace *carries* across an interface, not just where it may go.
-|—
-|—
-|OPEN
+|`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`

STATE.adoc

@@ -1,5 +1,66 @@
 = STATE — cross-session log
 
+== 2026-10-27 — rung 3e: path provenance as graded accumulation (echo-types bridge)
+
+* New `Marches/Provenance.lean`, imported from `Marches.lean`. `Cut.lean`
+  said where a well-typed trace may go; this says what it carries.
+  - `Grade` (a `⊗`-monoid: associativity and both units) and
+    `Grade.accum`, the grade a word of labels accumulates. `accum_append`
+    (a monoid homomorphism from label words) and `accum_map` (reads
+    through a relabelling).
+  - One region, `TropicalGrade`: `run_eq_seq_carried`, the end signature
+    of a run is the start `⊗` the grade its word carried;
+    `carried_cons_ne_one`, a non-empty word carries a non-unit grade;
+    `no_return_of_carried` recovers `tropical_no_return` through the grade.
+  - Across the interface: `trace_cross_shape`, a well-typed two-region
+    trace that crosses is an A-word from an A-start, the crossing, a B-word
+    (typing alone; no strictness used). `Interface.fibre` is the preimage
+    fibre of `τ`; `Interface.carried` is the A-signature at the crossing as
+    a point of it; `trace_cross_lands`.
+  - Region DAG: `DiscSys.carried_in_cut` and `carried_to_cross_in_past`,
+    the grade reaching a point inside a cut, or a crossing out of `↓r`, is
+    accumulated by a trace of the cut prefix alone (conditional on
+    `Acyclic`, as every `compose` theorem is).
+  - Exhibits: `id_carries` (the identity crossing carries the grade
+    intact); `zero_forgets`, `zero_fibre_distinguishes`, `collapse₀`,
+    `collapse₁` (a collapsing crossing forgets the A-grade, and the fibre
+    still tells the two traces apart); `trace₀` of `Cut.lean` graded to 4.
+* echo-types read at `1073d60` (its HEAD on 2026-10-27, shallow clone). Its
+  `Echo f y := Σ x, f x ≡ y` is "the standard preimage fiber" by its own
+  README; `EchoProvenance.agda` gives the collapse and distinguish
+  theorems. Pinned in `scripts/fetch-siblings.sh` (`ECHO_TYPES_COMMIT`);
+  `check-correspondence.sh` now greps `echo-types:` refs too (a fabricated
+  echo-types name was run through it and refused); `track-siblings.yml`
+  re-pins it weekly. Nothing Agda is imported or re-declared.
+* `docs/kcut-correspondence.adoc`: KC-9 (fibre ↔ `Echo`, `echo-intro`),
+  KC-10 (the collapse exhibit ↔ `provenance-collapses-at`,
+  `echoes-distinguish-tag`), KC-11 (graded cut-locality, KC-4 again),
+  KC-12 (accumulation needs the `⊗`-monoid; K-4's two laws supply neither
+  associativity nor the right unit). All ASSUMED. F6 row updated.
+* Gates on v4.35.0, verbatim:
++
+----
+$ lake build
+Build completed successfully (16 jobs).
+$ grep -rnw sorry Marches/ Marches.lean  # empty
+$ lake env lean Marches/BadGadget.lean
+[(false, false), (true, true), (false, false), (true, true)]
+$ lake env lean Axioms.lean   # #print axioms, the 20 new declarations
+'Marches.Grade.accum_append' does not depend on any axioms
+  (all 20 lines read "does not depend on any axioms")
+$ scripts/check-correspondence.sh
+PASS: 24 Lean names and 21 sibling names exist at the pins; both negative controls refused
+----
++
+A first proof of `no_return_of_carried` through `Nat.add_left_cancel`
+picked up `propext`; it was reproved from `a < a + carried` and is
+axiom-free.
+* actionlint 1.7.7 clean on `track-siblings.yml`; shellcheck clean on both
+  scripts; Asciidoctor renders the edited `.adoc` files without warnings.
+  `grep -ni converg Marches/Provenance.lean` hits only the delimitation.
+* ROADMAP 3e: met 2026-10-27. Rung 3 stays OPEN: 3d and 3f are not done.
+  No tag.
+
 == 2026-10-19 — CI: estate audit pinned to cicd-suite b17ec1a (not a rung)
 
 * hyperpolymath/cicd-suite#55 merged as `b17ec1a`; the caller's pin moves
@@ -283,6 +344,6 @@ lake package `tropical-resource-typing`, pinned `e172f8a`, Lean v4.13.0)
 behind the `Marches/Tropical.lean` seam — vendor or depend on it, do NOT
 paraphrase, and expect toolchain friction against the Lean marches pins
 (`lean-toolchain`; named there, not here, so a weekly bump cannot make
-this line stale). 3e: path provenance as graded accumulation (echo-types
-bridge). 3f: file the postern cross-issue once that repository exists.
+this line stale). 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.

docs/kcut-correspondence.adoc

@@ -37,9 +37,14 @@ ground (`LIMITATIONS.adoc`).
 |hyperpolymath/tropical-types
 |`e172f8abefd50fc40def4368fa60a155d130ff47`
 |`TropicalAdapterPath.lean`, `TropicalSessionTypes.lean` (the Lean side of M-2)
+
+|hyperpolymath/echo-types
+|`1073d600004d13f1aec7363baa0ee2e38d91568e`
+|`Echo`, `echo-intro` (the fibre); `Provenance`, `provenance-collapses-at`,
+`echoes-distinguish-tag` (the audience-facing provenance theorems)
 |===
 
-`scripts/fetch-siblings.sh` holds the same three commits. Re-pin one
+`scripts/fetch-siblings.sh` holds the same four commits. Re-pin one
 commit per change and update this table in the same commit.
 
 == The table
@@ -124,6 +129,54 @@ and it is OPEN there. marches' `TropicalNat` is min-plus on `Nat`, not
 max-plus: by KC-7 it sits with `Loss`, not with `MaxPlus`. No pairing
 with M-2's objects is proposed.
 |OPEN — not paired (order runs opposite)
+
+|KC-9
+|`Marches.Interface.fibre`, `Marches.Interface.carried`
+|`echo-types:proofs/agda/Echo.agda:Echo`, `echo-types:proofs/agda/Echo.agda:echo-intro`
+|Both are the preimage fibre of a map, `Σ x, f x ≡ y`, with its canonical
+inhabitant `(x, refl)`. Lean: the map is the crossing `τ` and the
+inhabitant is the A-signature a crossing trace carries (`run A as a₀`,
+by `trace_cross_shape`). Agda: any `f`; echo-types itself calls `Echo`
+"the standard preimage fiber, not a new construction". What marches adds
+is which map and which inhabitant. What echo-types adds on top of the
+fibre (its loss taxonomy, separation proofs, residues) is not paired.
+|ASSUMED (port-and-reprove)
+
+|KC-10
+|`Marches.ProvenanceExhibit.zero_forgets`, `Marches.ProvenanceExhibit.zero_fibre_distinguishes`
+|`echo-types:proofs/agda/EchoProvenance.agda:Provenance`, `echo-types:proofs/agda/EchoProvenance.agda:provenance-collapses-at`, `echo-types:proofs/agda/EchoProvenance.agda:echoes-distinguish-tag`
+|A forgetful map collapses two inputs that differ in what it forgets, and
+the fibre still tells them apart. Agda: the map is
+`project : Payload × Tag → Payload`, the two inputs differ in `Tag`,
+parametric in a `Provenance` record. Lean: the map is a collapsing
+crossing (`zeroI.τ`, every cost to `0`), the two inputs are the
+A-signatures of the traces `collapse₀` and `collapse₁`, whose words `[0]`
+and `[1]` carry grades `1` and `2`. The Agda is parametric; the Lean is one
+instance over `TropicalNat`, with no `Tag` type: the whole A-signature is
+what is forgotten.
+|ASSUMED (port-and-reprove)
+
+|KC-11
+|`Marches.DiscSys.carried_in_cut`, `Marches.DiscSys.carried_to_cross_in_past`
+|`choreographic-types:src/Choreographic/KCut.agda:cut-projectable` (K-5)
+|KC-4 again, for what a trace carries rather than where it goes: the grade
+reaching a point inside a cut, or a crossing out of `↓r`, is accumulated
+by a trace of the prefix alone. Agda's `cut-projectable` is about
+projectability of the prefix, not about a grade. The shared shape is
+cut-locality; the content differs.
+|ASSUMED (port-and-reprove)
+
+|KC-12
+|`Marches.Grade`, `Marches.Grade.accum_append`, `Marches.TropicalGrade.grade`
+|`choreographic-types:tests/minimal-laws/ResourceAlgebra/Core.agda:unitˡ`, `choreographic-types:tests/minimal-laws/ResourceAlgebra/Core.agda:idem`
+|KC-6 extended. Accumulation along a word is a monoid homomorphism and
+uses `⊗`-associativity and BOTH units. K-4's two laws (`unitˡ`, `idem`)
+supply neither associativity nor the right unit, so provenance by
+accumulation rests on more than K-CUT-LOSS needs. `TropicalGrade.grade`
+discharges all three for (min, +). A different law set for a different
+theorem, not a disagreement; no counterpart is proposed for `seq_assoc`
+or `seq_unitr`.
+|ASSUMED for `seq_unitl ↔ unitˡ` (as KC-6); the other two laws unpaired
 |===
 
 == Transport, for postern
@@ -160,4 +213,7 @@ postern's code. When the repository exists, the plan from MRC-01 is:
   own check.
 * Asynchronous K-CUT lands. Then postern's handshake is typed against the
   asynchronous fragment.
+* An Agda port of `Marches/Provenance.lean`'s fibre statements, or a Lean
+  port of `EchoProvenance`, lands. Then KC-9 and KC-10 move from ASSUMED to
+  a named port with its own check.
 * Rung 4 attestation lands. Then announcements carry the cut they were made at.

scripts/check-correspondence.sh

@@ -59,7 +59,7 @@ done < <(grep -oE '`Marches\.[A-Za-z0-9_.'"'"']+`' "$doc" | tr -d '`' | sort -u)
 while IFS= read -r ref; do
   nsib=$((nsib + 1))
   if ! sibling_exists "$ref"; then echo "MISSING (sibling): $ref"; fail=1; fi
-done < <(grep -oE '`(choreographic-types|resource-algebra|tropical-types):[^`]+`' "$doc" \
+done < <(grep -oE '`(choreographic-types|resource-algebra|tropical-types|echo-types):[^`]+`' "$doc" \
            | tr -d '`' | sort -u)
 
 while IFS= read -r pin; do

scripts/fetch-siblings.sh

@@ -11,6 +11,7 @@ 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:-e172f8abefd50fc40def4368fa60a155d130ff47}"
+ECHO_TYPES_COMMIT="${ECHO_TYPES_COMMIT:-1073d600004d13f1aec7363baa0ee2e38d91568e}"
 
 # Fetch a sibling repository and check out its pinned commit.
 # Arguments: $1 is the repository name under hyperpolymath; $2 is the commit.
@@ -31,3 +32,4 @@ mkdir -p _build/dependencies
 fetch choreographic-types "$CHOREOGRAPHIC_TYPES_COMMIT"
 fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT"
 fetch tropical-types "$TROPICAL_TYPES_COMMIT"
+fetch echo-types "$ECHO_TYPES_COMMIT"