From d4d0c92513720da38087f34a899da9a14c2107d5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Tue, 27 Oct 2026 05:49:18 +0000 Subject: [PATCH] feat(provenance): rung 3e, path provenance as graded accumulation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Marches/Provenance.lean answers what a well-typed trace carries, as Cut.lean answered where it may go. Words accumulate a grade in a ⊗-monoid (accum_append: a monoid homomorphism). In one tropical region the end signature of a run is the start ⊗ the carried grade (run_eq_seq_carried), and a non-empty word carries a non-unit grade. A two-region trace that crosses is an A-word, the crossing, a B-word (trace_cross_shape, typing alone); what crosses is the A-signature at the crossing, which B sees only through τ, so Interface.fibre (the preimage fibre of τ) is what was carried and cannot be seen. In the region DAG the grade reaching a cut, or a crossing out of ↓r, is accumulated by a trace of the prefix alone. Exhibits: an identity crossing carries the grade intact; a collapsing one forgets it while the fibre still distinguishes. echo-types is pinned at 1073d60 as a fourth sibling (fetch-siblings.sh, check-correspondence.sh, track-siblings.yml); KC-9 to KC-12 pair the fibre and the law set, all ASSUMED under F6. Nothing Agda is imported. Gates: lake build green (16 jobs); grep -rnw sorry empty; #eval orbit unchanged; #print axioms none on all 20 new declarations; check-correspondence.sh PASS (24 Lean, 21 sibling names). Rung 3 stays open on 3d and 3f; no tag. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- .github/workflows/track-siblings.yml | 5 +- FALSIFIERS.adoc | 7 +- Marches.lean | 1 + Marches/Provenance.lean | 391 +++++++++++++++++++++++++++ README.adoc | 32 ++- ROADMAP.adoc | 8 +- STATE.adoc | 65 ++++- docs/kcut-correspondence.adoc | 58 +++- scripts/check-correspondence.sh | 2 +- scripts/fetch-siblings.sh | 2 + 10 files changed, 560 insertions(+), 11 deletions(-) create mode 100644 Marches/Provenance.lean diff --git a/.github/workflows/track-siblings.yml b/.github/workflows/track-siblings.yml index 0beb54d..bfb902f 100644 --- a/.github/workflows/track-siblings.yml +++ b/.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) diff --git a/FALSIFIERS.adoc b/FALSIFIERS.adoc index e079dd3..84e63e1 100644 --- a/FALSIFIERS.adoc +++ b/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) |=== diff --git a/Marches.lean b/Marches.lean index 24ff9a1..d6a55d5 100644 --- a/Marches.lean +++ b/Marches.lean @@ -10,3 +10,4 @@ import Marches.Tropical import Marches.Freewheel import Marches.Reassembly import Marches.Cut +import Marches.Provenance diff --git a/Marches/Provenance.lean b/Marches/Provenance.lean new file mode 100644 index 0000000..6c54fa2 --- /dev/null +++ b/Marches/Provenance.lean @@ -0,0 +1,391 @@ +/- + Marches — path provenance as graded accumulation (rung 3e). + + `Cut.lean` answers WHERE a well-typed trace may go: every crossing + crosses a cut, and a trace never re-enters a cut it has left. This file + answers WHAT a trace carries. A word of labels accumulates a grade + (`Grade.accum`: `𝟙` for the empty word, `⊗` along the word), and: + + • TropicalGrade.run_eq_seq_carried : in one tropical region the end + signature is `start ⊗ carried(word)`. + The signature IS the accumulated grade. + • TropicalGrade.carried_cons_ne_one : a non-empty word carries a + non-unit grade — strict inflation, + read as provenance. `no_return` follows. + • trace_cross_shape : a well-typed two-region trace that + crosses has one shape: an A-word from + an A-start, the crossing, a B-word. + Typing alone; no strictness needed. + • Interface.fibre, Interface.carried : what crosses is the A-signature + at the crossing; the B side sees it only + through `τ`. The fibre of `τ` over the + landing point is what was carried and + cannot be seen from B. + • DiscSys.carried_to_cross_in_past : in the region DAG, the grade that + reaches a crossing `r → r'` was + accumulated by a trace of the cut + prefix `↓r` alone. + • DiscSys.carried_in_cut : the grade that reaches a point inside + a cut was accumulated by a trace of the + prefix alone — the graded reading of + `composeCut_trace_reflect`. + + Provenance of the bridge. echo-types (pinned in scripts/fetch-siblings.sh) + proves, in Agda, that a forgetful projection collapses records that differ + in a provenance tag while the fibre `Echo f y := Σ x, f x ≡ y` keeps them + apart (`EchoProvenance.agda`). `Interface.fibre` is that fibre for the + crossing map, stated here in marches' own terms; nothing in this file + imports or re-declares the Agda. The pairing is a table row + (docs/kcut-correspondence.adoc), ASSUMED, port-and-reprove, under + falsifier F6. + + On the laws. Accumulation is a monoid homomorphism from label words, so + it uses `⊗`-associativity and BOTH units. K-4 (`𝟙 ⊗ x ≡ x`, `x ⊕ x ≡ x`, + the two laws K-CUT-LOSS uses) does not supply those: provenance needs the + `⊗`-monoid, not `⊕`-idempotence. `TropicalGrade.grade` has all three. + + Delimitation unchanged: nothing here is protocol convergence; that ground + is agda-routing's (LIMITATIONS.adoc). +-/ + +import Marches.Basic +import Marches.Kernel +import Marches.Compose +import Marches.Tropical +import Marches.Cut + +namespace Marches + +/-! ### Grades: what a word of labels accumulates -/ + +/-- A grade monoid: `seq` is `⊗`, `one` is `𝟙`. Three laws, not K-4's two. -/ +structure Grade where + G : Type + seq : G → G → G + one : G + seq_assoc : ∀ a b c : G, seq (seq a b) c = seq a (seq b c) + seq_unitl : ∀ a : G, seq one a = a + seq_unitr : ∀ a : G, seq a one = a + +namespace Grade + +/-- The grade a word of labels accumulates, label by label from the left. -/ +def accum (g : Grade) {L : Type} (cost : L → g.G) : List L → g.G + | [] => g.one + | l :: ls => g.seq (cost l) (accum g cost ls) + +theorem accum_nil (g : Grade) {L : Type} (cost : L → g.G) : g.accum cost [] = g.one := rfl + +theorem accum_cons (g : Grade) {L : Type} (cost : L → g.G) (l : L) (ls : List L) : + g.accum cost (l :: ls) = g.seq (cost l) (g.accum cost ls) := rfl + +theorem accum_singleton (g : Grade) {L : Type} (cost : L → g.G) (l : L) : + g.accum cost [l] = cost l := + g.seq_unitr (cost l) + +/-- Accumulation is a monoid homomorphism from label words: the grade of a + concatenation is the sequencing of the grades. Uses `seq_assoc` and + `seq_unitl`. -/ +theorem accum_append (g : Grade) {L : Type} (cost : L → g.G) : + ∀ ls₁ ls₂ : List L, g.accum cost (ls₁ ++ ls₂) = g.seq (g.accum cost ls₁) (g.accum cost ls₂) + | [], _ => (g.seq_unitl _).symm + | l :: ls₁, ls₂ => + (congrArg (g.seq (cost l)) (accum_append g cost ls₁ ls₂)).trans + (g.seq_assoc (cost l) (g.accum cost ls₁) (g.accum cost ls₂)).symm + +/-- Accumulation reads through a relabelling: grading the image of a word + is grading the word by the composed cost. -/ +theorem accum_map (g : Grade) {L L' : Type} (cost : L → g.G) (f : L' → L) : + ∀ ls : List L', g.accum cost (ls.map f) = g.accum (fun l => cost (f l)) ls + | [] => rfl + | l :: ls => congrArg (g.seq (cost (f l))) (accum_map g cost f ls) + +end Grade + +/-! ### The tropical grade: provenance in one region -/ + +namespace TropicalGrade + +/-- The (min, +) grade as a monoid: `⊗` is `+`, `𝟙` is `0`. Associativity + and the right unit are beyond K-4; accumulation needs them. -/ +def grade : Grade where + G := Nat + seq := seq + one := one + seq_assoc := Nat.add_assoc + seq_unitl := seq_unitl + seq_unitr := Nat.add_zero + +/-- The cost a label carries: `w + 1`, as `ext_eq_seq` reads extension. -/ +def cost (w : Nat) : Nat := w + 1 + +/-- The grade a tropical word carries. -/ +def carried (ls : List Nat) : Nat := grade.accum cost ls + +theorem carried_nil : carried [] = one := rfl + +theorem carried_cons (w : Nat) (ls : List Nat) : carried (w :: ls) = seq (cost w) (carried ls) := rfl + +theorem carried_append (ls₁ ls₂ : List Nat) : + carried (ls₁ ++ ls₂) = seq (carried ls₁) (carried ls₂) := + grade.accum_append cost ls₁ ls₂ + +/-- PROVENANCE, one region: running a word from `a` lands at + `a ⊗ carried(word)`. The end signature is the start plus what the word + carried, and nothing else. -/ +theorem run_eq_seq_carried : ∀ (ls : List Nat) (a : Nat), run TropicalNat ls a = seq a (carried ls) + | [], a => (Nat.add_zero a).symm + | w :: ls, a => + (run_eq_seq_carried ls (a + (w + 1))).trans (Nat.add_assoc a (w + 1) (carried ls)) + +/-- A non-empty word carries a non-unit grade: strict inflation, read as + provenance. `label_cost_ne_one` lifted from one label to a word. -/ +theorem carried_cons_ne_one (w : Nat) (ls : List Nat) : carried (w :: ls) ≠ one := + Nat.ne_of_gt (Nat.lt_of_lt_of_le (Nat.succ_pos w) (Nat.le_add_right (w + 1) (carried ls))) + +/-- Loop-freedom recovered from provenance: a word returning to its start + carries the unit, and a non-empty word does not. The same statement as + `tropical_no_return`, reached through the grade. -/ +theorem no_return_of_carried (w : Nat) (ls : List Nat) (a : Nat) : + run TropicalNat (w :: ls) a ≠ a := + fun h => + Nat.ne_of_gt + (Nat.lt_of_lt_of_le (Nat.lt_succ_self a) + (Nat.add_le_add_left + (Nat.succ_le_of_lt + (Nat.lt_of_lt_of_le (Nat.succ_pos w) (Nat.le_add_right (w + 1) (carried ls)))) + a)) + ((run_eq_seq_carried (w :: ls) a).symm.trans h) + +end TropicalGrade + +/-! ### What crosses the interface: the shape of a crossing trace -/ + +/-- A trace that starts in B is a B-word, and ends where that word runs to. -/ +theorem trace_from_B (A B : PathAlgebra) (I : Interface A B) : + ∀ {p : Pos A B} {ls : List (CLabel A B)} {q : Pos A B}, Trace A B I p ls q → + ∀ x : B.Carrier, p = .inB x → + ∃ bs : List B.Label, ls = bs.map CLabel.lb ∧ q = .inB (run B bs x) := by + intro p ls q ht + induction ht with + | nil => intro x hx; exact ⟨[], rfl, hx⟩ + | cons hs _ ih => + intro x hx + cases hs with + | la => cases hx + | @lb l x' => + cases hx + obtain ⟨bs, hls, hq⟩ := ih _ rfl + exact ⟨l :: bs, by rw [hls]; rfl, hq⟩ + | cross => cases hx + +/-- SHAPE: a well-typed two-region trace that crosses is an A-word from an + A-start, the crossing, then a B-word; it ends where the B-word runs to + from `τ` of where the A-word ran to. Typing alone gives this; no + strictness is used. What the trace carries across the interface is + `run A as a₀`, and the B side sees it only through `τ`. -/ +theorem trace_cross_shape (A B : PathAlgebra) (I : Interface A B) : + ∀ {p : Pos A B} {ls : List (CLabel A B)} {q : Pos A B}, Trace A B I p ls q → + CLabel.cross ∈ ls → + ∃ (a₀ : A.Carrier) (as : List A.Label) (bs : List B.Label), + p = .inA a₀ ∧ ls = as.map CLabel.la ++ CLabel.cross :: bs.map CLabel.lb ∧ + q = .inB (run B bs (I.τ (run A as a₀))) := by + intro p ls q ht + induction ht with + | nil => intro hl; cases hl + | cons hs ht' ih => + intro hl + cases hs with + | @la l x => + cases hl with + | tail _ hl' => + obtain ⟨a₀, as, bs, hp, hls, hq⟩ := ih hl' + cases hp + exact ⟨x, l :: as, bs, rfl, by rw [hls]; rfl, hq⟩ + | lb => + cases hl with + | tail _ hl' => + obtain ⟨_, _, _, hp, _, _⟩ := ih hl' + cases hp + | @cross x => + obtain ⟨bs, hls, hq⟩ := trace_from_B A B I ht' _ rfl + exact ⟨x, [], bs, rfl, by rw [hls]; rfl, hq⟩ + +/-! ### The fibre of the crossing map (echo-types bridge) -/ + +/-- The fibre of the crossing map over a B-signature: the A-signatures that + cross to it. This is the preimage fibre — what echo-types writes + `Echo τ y := Σ x, τ x ≡ y` — in marches' own terms. The B side cannot + tell its points apart; a trace's provenance lives here. -/ +def Interface.fibre {A B : PathAlgebra} (I : Interface A B) (y : B.Carrier) : Type := + {x : A.Carrier // I.τ x = y} + +/-- What a crossing trace carries: the A-signature at the crossing, as a + point of the fibre over where it lands. (echo-types' `echo-intro`, + applied to `run A as a₀`.) -/ +def Interface.carried {A B : PathAlgebra} (I : Interface A B) (a₀ : A.Carrier) (as : List A.Label) : + I.fibre (I.τ (run A as a₀)) := + ⟨run A as a₀, rfl⟩ + +/-- Every crossing trace lands in the image of `τ`, at the point its + carried signature crosses to — the shape theorem, read on the fibre. -/ +theorem trace_cross_lands (A B : PathAlgebra) (I : Interface A B) + {p : Pos A B} {ls : List (CLabel A B)} {q : Pos A B} + (ht : Trace A B I p ls q) (hl : CLabel.cross ∈ ls) : + ∃ (a₀ : A.Carrier) (as : List A.Label) (bs : List B.Label), + q = .inB (run B bs (I.τ (I.carried a₀ as).1)) := by + obtain ⟨a₀, as, bs, _, _, hq⟩ := trace_cross_shape A B I ht hl + exact ⟨a₀, as, bs, hq⟩ + +/-! ### Cuts of the region DAG: what reaches a crossing is accumulated in the prefix -/ + +namespace DiscSys + +variable (S : DiscSys) + +/-- The grade that reaches a point inside a cut was accumulated by a trace + of the cut prefix alone, label for label: the graded reading of + `composeCut_trace_reflect`. Whatever lies beyond the frontier + contributes nothing to it. -/ +theorem carried_in_cut (hacyc : Acyclic S.E) (C : Cut S.E) (g : Grade) (cost : S.Lab → g.G) + {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos} + (ht : Discipline.Trace (S.compose hacyc) p ls q) (hq : C.mem q.1) : + ∃ ls' : List (S.restrict C).Lab, + ls'.map (S.labEmb C) = ls ∧ + g.accum cost ls = g.accum (fun l => cost (S.labEmb C l)) ls' ∧ + Discipline.Trace (S.composeCut hacyc C) + ⟨⟨p.1, S.trace_mem_back hacyc C ht hq⟩, p.2⟩ ls' ⟨⟨q.1, hq⟩, q.2⟩ := by + obtain ⟨ls', hmap, ht'⟩ := S.composeCut_trace_reflect hacyc C ht hq + exact ⟨ls', hmap, by rw [← hmap, g.accum_map], ht'⟩ + +/-- The grade that reaches a crossing `r → r'` was accumulated inside the + principal cut `↓r`: the word splits as prefix, crossing, suffix; its + grade factors the same way; and the prefix is a trace of + `composeCut (past r)` from the trace's start, ending in `r`. -/ +theorem carried_to_cross_in_past (hacyc : Acyclic S.E) (g : Grade) (cost : S.Lab → g.G) + {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos} + (ht : Discipline.Trace (S.compose hacyc) p ls q) + {r r' : S.R} {e : S.E r r'} (hl : Lab.cross r r' e ∈ ls) : + ∃ ls₁ ls₂ : List S.Lab, + ls = ls₁ ++ Lab.cross r r' e :: ls₂ ∧ + g.accum cost ls = g.seq (g.accum cost ls₁) (g.seq (cost (.cross r r' e)) (g.accum cost ls₂)) ∧ + ∃ (ls₁' : List (S.restrict (Cut.past r)).Lab) + (p' m' : (S.composeCut hacyc (Cut.past r)).Pos), + S.posEmb (Cut.past r) p' = p ∧ (S.posEmb (Cut.past r) m').1 = r ∧ + ls₁'.map (S.labEmb (Cut.past r)) = ls₁ ∧ + g.accum cost ls₁ = g.accum (fun l => cost (S.labEmb (Cut.past r) l)) ls₁' ∧ + Discipline.Trace (S.composeCut hacyc (Cut.past r)) p' ls₁' m' := by + obtain ⟨ls₁, ls₂, m, _, he, h₁, hm, _⟩ := Discipline.trace_split _ ht hl + obtain ⟨hmr, _⟩ := S.cross_step_regions hm + have hmC : (Cut.past (E := S.E) r).mem m.1 := Or.inl hmr + have hp : (Cut.past (E := S.E) r).mem p.1 := S.trace_mem_back hacyc (Cut.past r) h₁ hmC + obtain ⟨ls₁', hmap, ht'⟩ := S.composeCut_trace_reflect_of hacyc (Cut.past r) h₁ hp hmC + subst he + refine ⟨ls₁, ls₂, rfl, g.accum_append cost ls₁ (Lab.cross r r' e :: ls₂), + ls₁', ⟨⟨p.1, hp⟩, p.2⟩, ⟨⟨m.1, hmC⟩, m.2⟩, rfl, hmr, hmap, ?_, ht'⟩ + rw [← hmap, g.accum_map] + +end DiscSys + +/-! ### Concrete exhibits: the theorems are not vacuous -/ + +namespace ProvenanceExhibit + +open TropicalGrade + +/-- One region: the word `[2, 0]` carries `3 + 1 = 4`, and running it from + cost `0` lands at `4`. -/ +example : carried [2, 0] = 4 ∧ + run TropicalNat ([2, 0] : List Nat) (0 : Nat) = seq 0 (carried [2, 0]) := + ⟨rfl, run_eq_seq_carried [2, 0] 0⟩ + +/-- The identity crossing between two tropical regions (the interface form + of `Reassembly.twoTropical`). -/ +def idI : Interface TropicalNat TropicalNat where + τ := fun x => x + +/-- A collapsing crossing: every A-signature crosses to cost `0`. -/ +def zeroI : Interface TropicalNat TropicalNat where + τ := fun _ => (0 : Nat) + +/-- Under the identity crossing the grade crosses intact: the end cost is + the start plus what BOTH words carried, as one word. -/ +theorem id_carries (a₀ : Nat) (as bs : List Nat) : + run TropicalNat bs (idI.τ (run TropicalNat as a₀)) = seq a₀ (carried (as ++ bs)) := by + show run TropicalNat bs (run TropicalNat as a₀) = seq a₀ (carried (as ++ bs)) + rw [run_eq_seq_carried, run_eq_seq_carried, carried_append] + exact Nat.add_assoc a₀ (carried as) (carried bs) + +/-- Under the collapsing crossing the A-grade is forgotten: the end cost does + not depend on the A-word at all. (echo-types' `provenance-collapses-at`, + in marches' terms.) -/ +theorem zero_forgets (a₀ : Nat) (as as' bs : List Nat) : + run TropicalNat bs (zeroI.τ (run TropicalNat as a₀)) = + run TropicalNat bs (zeroI.τ (run TropicalNat as' a₀)) := + rfl + +/-- ...and the fibre over the landing point still tells the two apart: the + words `[0]` and `[1]` carry `1` and `2`. (echo-types' + `echoes-distinguish-tag`.) -/ +theorem zero_fibre_distinguishes : + (zeroI.carried (0 : Nat) [(0 : Nat)]).1 ≠ (zeroI.carried (0 : Nat) [(1 : Nat)]).1 := by + show (1 : Nat) ≠ 2 + decide + +/-- Two well-typed traces over the collapsing crossing, from the same start, + with different A-words, to the SAME end: the B side cannot tell them + apart. -/ +theorem collapse₀ : + Trace TropicalNat TropicalNat zeroI (.inA (0 : Nat)) [.la (0 : Nat), .cross, .lb (0 : Nat)] + (.inB (1 : Nat)) := + .cons .la (.cons .cross (.cons .lb .nil)) + +theorem collapse₁ : + Trace TropicalNat TropicalNat zeroI (.inA (0 : Nat)) [.la (1 : Nat), .cross, .lb (0 : Nat)] + (.inB (1 : Nat)) := + .cons .la (.cons .cross (.cons .lb .nil)) + +/-- The shape theorem on `collapse₀`: it is `[0]`, the crossing, `[0]`. -/ +example : ∃ (a₀ : TropicalNat.Carrier) (as bs : List TropicalNat.Label), + Pos.inA (A := TropicalNat) (B := TropicalNat) (0 : Nat) = .inA a₀ ∧ + [CLabel.la (A := TropicalNat) (B := TropicalNat) (0 : Nat), .cross, .lb (0 : Nat)] = + as.map CLabel.la ++ CLabel.cross :: bs.map CLabel.lb ∧ + Pos.inB (A := TropicalNat) (B := TropicalNat) (1 : Nat) = + .inB (run TropicalNat bs (zeroI.τ (run TropicalNat as a₀))) := + trace_cross_shape TropicalNat TropicalNat zeroI collapse₀ (.tail _ (.head _)) + +/-- The composite exhibit of `Cut.lean`, graded: local labels cost `w + 1`, + the crossing costs `𝟙`. -/ +def cost₀ : Reassembly.twoTropical.Lab → Nat + | .loc _ w => cost w + | .cross _ _ _ => one + +/-- The word of `CutExhibit.trace₀`: a hop of weight 2 in region `false`, + the crossing, a hop of weight 0 in region `true`. -/ +def word₀ : List Reassembly.twoTropical.Lab := + [.loc false (2 : Nat), .cross false true CutExhibit.e₀, .loc true (0 : Nat)] + +/-- `trace₀` runs cost 0 → 4, and its word carries `3 + 0 + 1 = 4`. -/ +example : grade.accum cost₀ word₀ = (4 : Nat) := rfl + +/-- `carried_to_cross_in_past` on `trace₀`: the grade before the crossing is + accumulated by a trace of `↓false` alone. -/ +example : ∃ ls₁ ls₂ : List Reassembly.twoTropical.Lab, + word₀ = ls₁ ++ .cross false true CutExhibit.e₀ :: ls₂ ∧ + grade.accum cost₀ word₀ = + seq (grade.accum cost₀ ls₁) (seq (cost₀ (.cross false true CutExhibit.e₀)) (grade.accum cost₀ ls₂)) ∧ + ∃ (ls₁' : List (Reassembly.twoTropical.restrict (Cut.past false)).Lab) + (p' m' : (Reassembly.twoTropical.composeCut Reassembly.boolUp_acyclic (Cut.past false)).Pos), + Reassembly.twoTropical.posEmb (Cut.past false) p' = ⟨false, (0 : Nat)⟩ ∧ + (Reassembly.twoTropical.posEmb (Cut.past false) m').1 = false ∧ + ls₁'.map (Reassembly.twoTropical.labEmb (Cut.past false)) = ls₁ ∧ + grade.accum cost₀ ls₁ = + grade.accum (fun l => cost₀ (Reassembly.twoTropical.labEmb (Cut.past false) l)) ls₁' ∧ + Discipline.Trace (Reassembly.twoTropical.composeCut Reassembly.boolUp_acyclic (Cut.past false)) + p' ls₁' m' := + Reassembly.twoTropical.carried_to_cross_in_past Reassembly.boolUp_acyclic grade cost₀ + CutExhibit.trace₀ (.tail _ (.head _)) + +end ProvenanceExhibit + +end Marches diff --git a/README.adoc b/README.adoc index e08fd43..d74c1e8 100644 --- a/README.adoc +++ b/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 diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 5bb0902..c750251 100644 --- a/ROADMAP.adoc +++ b/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` diff --git a/STATE.adoc b/STATE.adoc index 246b44e..352e7f7 100644 --- a/STATE.adoc +++ b/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. diff --git a/docs/kcut-correspondence.adoc b/docs/kcut-correspondence.adoc index f94d407..197b6e2 100644 --- a/docs/kcut-correspondence.adoc +++ b/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. diff --git a/scripts/check-correspondence.sh b/scripts/check-correspondence.sh index 80dd10b..916edcf 100755 --- a/scripts/check-correspondence.sh +++ b/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 diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh index 2a27c3d..46da36d 100755 --- a/scripts/fetch-siblings.sh +++ b/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"