From c6ffd9f450e041fbc423aaa75c9c167c3095002a Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:07:38 +0000 Subject: [PATCH 1/2] chore(toolchain): move to Lean v4.34.0 before rung 3 Maintainer decision on MRC-01's open question: adopt the estate's v4.34.0 floor (F-11) before any rung-3 module lands, as its own change. The tree at ea1920a was built on both toolchains before the switch: both completed with no warnings and the same `#eval orbit`, so no source change is needed. README's build line and STATE.adoc are updated to match. Gates (v4.34.0): lake build -> Build completed successfully (14 jobs); grep -rnw sorry empty; #eval orbit unchanged. Rung: 3 (preparation; rung stays OPEN) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- README.adoc | 4 ++-- STATE.adoc | 13 +++++++++++++ lean-toolchain | 2 +- 3 files changed, 16 insertions(+), 3 deletions(-) diff --git a/README.adoc b/README.adoc index 680e2a7..33a2df6 100644 --- a/README.adoc +++ b/README.adoc @@ -14,7 +14,7 @@ object*: region-crossing well-formedness is a typing judgment on traces (`Marches.Trace`), and ill-typed crossings are *unconstructible* — they have no derivation — rather than detected and filtered. -Machine-checked, in this repository, by `lake build` (Lean 4, v4.15.0, +Machine-checked, in this repository, by `lake build` (Lean 4, v4.34.0, no dependencies): * Every well-typed non-empty cross-region trace strictly worsens @@ -136,7 +136,7 @@ artifact for PROVEN rows. No fabricated identifiers. [source,shell] ---- -elan default leanprover/lean4:v4.15.0 # or let lake read lean-toolchain +elan default leanprover/lean4:v4.34.0 # or let lake read lean-toolchain lake build ---- diff --git a/STATE.adoc b/STATE.adoc index f09cffb..5a18bb3 100644 --- a/STATE.adoc +++ b/STATE.adoc @@ -1,5 +1,18 @@ = STATE — cross-session log +== 2026-10-14 — toolchain moved to v4.34.0 before rung 3 (Claude Code session) + +* Maintainer decision (MRC-01 open question): move `lean-toolchain` from + `v4.15.0` to the estate's `v4.34.0` floor (F-11) *before* any rung-3 + module is added, as its own change. +* No source change was needed: the tree at `ea1920a` was built on both + toolchains first, and both gave `Build completed successfully` with no + warnings and the same `#eval orbit`. +* Gates on v4.34.0: `lake build` → `Build completed successfully (14 jobs).`; + `grep -rnw sorry Marches/ Marches.lean` empty; `#eval orbit` unchanged + (`[(false, false), (true, true), (false, false), (true, true)]`). +* Rung 3 still OPEN; nothing else moved. + == 2026-07-07 — rung 2 built and verified (Claude Code session) * Digraph foundation lifted: `Marches/Digraph.lean` — `RPath`, diff --git a/lean-toolchain b/lean-toolchain index d0eb99f..12359f9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0 +leanprover/lean4:v4.34.0 From 70d58e2a2685b4d69256d60df0c400a1457a9051 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 01:18:25 +0000 Subject: [PATCH 2/2] feat(rung-3): a region crossing is a cut; K-4 laws over TropicalNat Marches/Cut.lean (new): a cut of the region DAG is a set of regions closed under predecessors. - Cut.edge_crosses_past: in an acyclic graph every edge leaves the principal cut of its source; Cut.path_back_crosses_no_cut: an edge on a cycle crosses no cut, so Acyclic is load-bearing. - DiscSys.trace_cross_crosses_cut: every crossing in a well-typed composite trace crosses a cut holding the trace's start, not its end. - DiscSys.trace_mem_back / trace_inside / no_reentry: a trace ending in a cut was inside it all along; a trace that leaves a cut never re-enters (no_back_cross lifted from one interface to every cut). - DiscSys.composeCut: compose restricted to a cut prefix is a Discipline (prefix-closure); composeCut_trace_embed / composeCut_trace_reflect: its traces are exactly the composite's traces that end in the prefix. - Two-region Interface: trace_cross_crosses_cut, trace_stays_in_B. - CutExhibit: a concrete twoTropical trace, and a negative control. Marches/Tropical.lean: TropicalGrade reads TropicalNat as a (min,+) grade. seq_unitl and alt_idem are the two laws K-CUT-LOSS uses (K-4). better_reverses_altLe, altLe_one and s3_witness record that marches' `better` runs against its own induced order (S-3 / W-4 direction). Every new declaration depends on no axioms (#print axioms) and nothing re-declares an Agda definition. Gates: lake build -> Build completed successfully (15 jobs); grep -rnw sorry empty; #eval orbit unchanged. Rung: 3 (rung stays OPEN) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- Marches.lean | 1 + Marches/Cut.lean | 428 ++++++++++++++++++++++++++++++++++++++++++ Marches/Tropical.lean | 63 +++++++ README.adoc | 36 +++- 4 files changed, 526 insertions(+), 2 deletions(-) create mode 100644 Marches/Cut.lean diff --git a/Marches.lean b/Marches.lean index b6e0b65..24ff9a1 100644 --- a/Marches.lean +++ b/Marches.lean @@ -9,3 +9,4 @@ import Marches.BadGadget import Marches.Tropical import Marches.Freewheel import Marches.Reassembly +import Marches.Cut diff --git a/Marches/Cut.lean b/Marches/Cut.lean new file mode 100644 index 0000000..5db7f54 --- /dev/null +++ b/Marches/Cut.lean @@ -0,0 +1,428 @@ +/- + Marches — cuts of the region DAG (rung 3). + + A *cut* is a set of regions closed under DAG predecessors: if a region + is in the cut, so is every region that can cross into it. Read along the + causal order of announcements (a route is in a region before it crosses + out), a cut is a frontier, and its regions are the prefix before that + frontier. This is the classical downward-closure condition on a cut. It + is NOT the party-indexed `Consistent` of choreographic-types, a merge + condition at choices (see the correspondence table). Being a cut needs + no acyclicity; *crossing* one does (`edge_crosses_past`). + + Headline theorems: + • Cut.edge_crosses_past : in an acyclic graph every edge r → r' + leaves the principal cut ↓r. + • Cut.path_back_crosses_no_cut : an edge on a cycle crosses NO cut — + acyclicity is load-bearing. + • DiscSys.trace_cross_crosses_cut : every crossing in a well-typed + composite trace crosses a cut that + holds the trace's start and not its end. + • DiscSys.trace_mem_back : a trace ending inside a cut was inside + it all along (`trace_inside`: every + label fired inside it). + • DiscSys.no_reentry : a trace that has left a cut never + re-enters it — `no_back_cross`, lifted + from one interface to every cut. + • DiscSys.composeCut : `compose` restricted to a cut prefix + is a `Discipline` (prefix-closure). Its + traces are exactly the composite traces + that end in the prefix + (`composeCut_trace_embed`, + `composeCut_trace_reflect`). + • trace_cross_crosses_cut : the same, for the two-region + `Interface` of `Compose.lean` (the + 2-node DAG `Reassembly.boolUp`). + + Provenance. choreographic-types (pinned at edb784a) proves the cut side + for global choreographies in Agda: `Choreographic.Global.Cut`, + `KCut.proj-cut`, `KCut.cut-projectable`. The relation between those + names and these is a table, not a link (docs/kcut-correspondence.adoc). + No row there is more than ASSUMED (port-and-reprove). Nothing in this + file imports or re-declares the Agda definitions. + + Delimitation: prefix-closure and loop-freedom of the typed judgment are + not protocol convergence; agda-routing owns that ground (LIMITATIONS.adoc). +-/ + +import Marches.Compose +import Marches.Digraph +import Marches.Reassembly + +namespace Marches + +/-- A cut of a region graph `E`: a set of regions closed under + predecessors. Every region that can cross into the cut is in it. -/ +structure Cut {R : Type} (E : R → R → Prop) where + mem : R → Prop + closed : ∀ {r r' : R}, E r r' → mem r' → mem r + +namespace Cut + +variable {R : Type} {E : R → R → Prop} + +/-- An edge `r → r'` crosses the cut `C` when it leaves it. -/ +def Crosses (C : Cut E) (r r' : R) : Prop := C.mem r ∧ ¬ C.mem r' + +/-- Closure lifts from edges to paths. -/ +theorem closed_path (C : Cut E) : + ∀ {r r' : R}, RPath E r r' → C.mem r' → C.mem r := by + intro r r' h + induction h with + | single e => exact C.closed e + | cons e _ ih => intro hm; exact C.closed e (ih hm) + +/-- The principal cut below `r`: `r` and every region with a path to it. -/ +def past (r : R) : Cut E where + mem x := x = r ∨ RPath E x r + closed := by + intro x y e hy + cases hy with + | inl h => subst h; exact Or.inr (.single e) + | inr p => exact Or.inr (.cons e p) + +/-- In an acyclic graph every edge crosses the principal cut of its source: + the source is inside, the target outside. -/ +theorem edge_crosses_past (hacyc : Acyclic E) {r r' : R} (e : E r r') : + (past (E := E) r).Crosses r r' := by + refine ⟨Or.inl rfl, ?_⟩ + intro h + cases h with + | inl h => subst h; exact hacyc _ (.single e) + | inr p => exact hacyc r (.cons e p) + +/-- Negative: if `r'` reaches back to `r`, no cut separates them. So an edge + `r → r'` on a cycle crosses no cut at all: without `Acyclic`, + `edge_crosses_past` fails, and so does every theorem below that uses it. -/ +theorem path_back_crosses_no_cut {r r' : R} (p : RPath E r' r) (C : Cut E) : + ¬ C.Crosses r r' := + fun ⟨h, hn⟩ => hn (C.closed_path p h) + +end Cut + +/-! ### Traces of a discipline, split at a label -/ + +/-- A trace containing a label splits into a prefix, that step, and a suffix. -/ +theorem Discipline.trace_split (D : Discipline) : + ∀ {p : D.Pos} {ls : List D.Lab} {q : D.Pos}, Discipline.Trace D p ls q → + ∀ {l : D.Lab}, l ∈ ls → + ∃ ls₁ ls₂ m m', ls = ls₁ ++ l :: ls₂ ∧ Discipline.Trace D p ls₁ m ∧ + D.Step l m m' ∧ Discipline.Trace D m' ls₂ q := by + intro p ls q ht + induction ht with + | nil => intro l hl; cases hl + | @cons p q₀ _ l₀ ls hs ht' ih => + intro l hl + cases hl with + | head => exact ⟨[], ls, p, q₀, rfl, .nil, hs, ht'⟩ + | tail _ hl' => + obtain ⟨ls₁, ls₂, m, m', he, h₁, hm, h₂⟩ := ih hl' + exact ⟨l₀ :: ls₁, ls₂, m, m', by rw [he]; rfl, .cons hs h₁, hm, h₂⟩ + +/-! ### Cuts of a composed region DAG -/ + +namespace DiscSys + +variable (S : DiscSys) + +/-- One composite step stays in its region or crosses one DAG edge. -/ +theorem step_region : + ∀ {l : S.Lab} {p q : S.Pos}, S.Step l p q → p.1 = q.1 ∨ S.E p.1 q.1 := by + intro l p q h + cases h with + | sloc _ => exact Or.inl rfl + | scross e => exact Or.inr e + +/-- A crossing step leaves exactly the edge's source for its target. -/ +theorem cross_step_regions {r r' : S.R} {e : S.E r r'} {m m' : S.Pos} + (h : S.Step (.cross r r' e) m m') : m.1 = r ∧ m'.1 = r' := by + cases h with + | scross _ => exact ⟨rfl, rfl⟩ + +/-- A trace ends in its start region or downstream of it. -/ +theorem trace_region (hacyc : Acyclic S.E) : + ∀ {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos}, + Discipline.Trace (S.compose hacyc) p ls q → p.1 = q.1 ∨ RPath S.E p.1 q.1 := by + intro p ls q ht + induction ht with + | nil => exact Or.inl rfl + | cons hs _ ih => + cases S.step_region hs with + | inl h₁ => + cases ih with + | inl h₂ => exact Or.inl (h₁.trans h₂) + | inr p₂ => exact Or.inr (by rw [h₁]; exact p₂) + | inr e => + cases ih with + | inl h₂ => exact Or.inr (.single (by rw [← h₂]; exact e)) + | inr p₂ => exact Or.inr (.cons e p₂) + +/-- PREFIX: a trace ending inside a cut started inside it. What happens + after the frontier cannot reach back into the prefix. -/ +theorem trace_mem_back (hacyc : Acyclic S.E) (C : Cut S.E) + {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) : C.mem p.1 := by + cases S.trace_region hacyc ht with + | inl h => rw [h]; exact hq + | inr p => exact C.closed_path p hq + +/-- `no_back_cross`, lifted from one interface to every cut of the DAG: + a trace that starts outside a cut never enters it. -/ +theorem no_reentry (hacyc : Acyclic S.E) (C : Cut S.E) + {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) (hp : ¬ C.mem p.1) : + ¬ C.mem q.1 := + fun hq => hp (S.trace_mem_back hacyc C ht hq) + +/-- A composite label lies inside a cut when it fires from a region of the + cut and, if a crossing, lands in one. -/ +def LabInside (C : Cut S.E) : S.Lab → Prop + | .loc r _ => C.mem r + | .cross r r' _ => C.mem r ∧ C.mem r' + +/-- A trace ending inside a cut fires every one of its labels inside it. -/ +theorem trace_inside (hacyc : Acyclic S.E) (C : Cut S.E) : + ∀ {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos}, + Discipline.Trace (S.compose hacyc) p ls q → C.mem q.1 → + ∀ l ∈ ls, S.LabInside C l := by + intro p ls q ht + induction ht with + | nil => intro _ l hl; cases hl + | cons hs ht' ih => + intro hq l hl + have hq₀ := S.trace_mem_back hacyc C ht' hq + cases hl with + | head => + cases hs with + | sloc _ => exact hq₀ + | scross e => exact ⟨C.closed e hq₀, hq₀⟩ + | tail _ hl' => exact ih hq l hl' + +/-- Every crossing in a well-typed composite trace crosses a cut — the + principal cut of its source — which holds the trace's start and not its + end: the trace leaves that cut at this step and never comes back. -/ +theorem trace_cross_crosses_cut (hacyc : Acyclic S.E) + {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) : + ∃ C : Cut S.E, C.Crosses r r' ∧ C.mem p.1 ∧ ¬ C.mem q.1 := by + obtain ⟨_, _, m, m', _, h₁, hm, h₂⟩ := Discipline.trace_split _ ht hl + obtain ⟨hmr, hmr'⟩ := S.cross_step_regions hm + have hc := Cut.edge_crosses_past hacyc e + refine ⟨Cut.past r, hc, ?_, ?_⟩ + · cases S.trace_region hacyc h₁ with + | inl h => exact Or.inl (h.trans hmr) + | inr p => exact Or.inr (by rw [← hmr]; exact p) + · exact S.no_reentry hacyc (Cut.past r) h₂ (by rw [hmr']; exact hc.2) + +/-! ### Prefix-closure: `compose` restricted to a cut is a discipline -/ + +/-- The system restricted to the regions of a cut. -/ +def restrict (C : Cut S.E) : DiscSys where + R := {r : S.R // C.mem r} + E := fun a b => S.E a.1 b.1 + D := fun a => S.D a.1 + τ := fun e x => S.τ e x + +/-- Paths in the restriction are paths in the system. -/ +theorem restrict_path (C : Cut S.E) : + ∀ {a b : (S.restrict C).R}, RPath (S.restrict C).E a b → RPath S.E a.1 b.1 := by + intro a b h + induction h with + | single e => exact .single e + | cons e _ ih => exact .cons e ih + +/-- The restriction of an acyclic DAG is acyclic. -/ +theorem restrict_acyclic (hacyc : Acyclic S.E) (C : Cut S.E) : + Acyclic (S.restrict C).E := + fun a h => hacyc a.1 (S.restrict_path C h) + +/-- PREFIX-CLOSURE: `compose` restricted to a cut prefix is a `Discipline`. + Its loop-freedom is `Discipline.no_loop`, with no new proof. -/ +def composeCut (hacyc : Acyclic S.E) (C : Cut S.E) : Discipline := + (S.restrict C).compose (S.restrict_acyclic hacyc C) + +/-- Positions of the prefix, read as positions of the whole system. -/ +def posEmb (C : Cut S.E) : (S.restrict C).Pos → S.Pos := fun p => ⟨p.1.1, p.2⟩ + +/-- Labels of the prefix, read as labels of the whole system. -/ +def labEmb (C : Cut S.E) : (S.restrict C).Lab → S.Lab + | .loc a l => .loc a.1 l + | .cross a b e => .cross a.1 b.1 e + +theorem step_embed (C : Cut S.E) : + ∀ {l : (S.restrict C).Lab} {p q : (S.restrict C).Pos}, + (S.restrict C).Step l p q → S.Step (S.labEmb C l) (S.posEmb C p) (S.posEmb C q) := by + intro l p q h + cases h with + | sloc hs => exact .sloc hs + | @scross a b e _ => exact DiscSys.Step.scross (S := S) (r := a.1) (r' := b.1) e + +/-- Every trace of the prefix is a trace of the whole composite. -/ +theorem composeCut_trace_embed (hacyc : Acyclic S.E) (C : Cut S.E) : + ∀ {p : (S.composeCut hacyc C).Pos} {ls : List (S.composeCut hacyc C).Lab} + {q : (S.composeCut hacyc C).Pos}, + Discipline.Trace (S.composeCut hacyc C) p ls q → + Discipline.Trace (S.compose hacyc) (S.posEmb C p) (ls.map (S.labEmb C)) + (S.posEmb C q) := by + intro p ls q ht + induction ht with + | nil => exact .nil + | cons hs _ ih => exact .cons (S.step_embed C hs) ih + +/-- Conversely, every composite trace that starts and ends in the prefix is + a trace of the prefix, label for label. -/ +theorem composeCut_trace_reflect_of (hacyc : Acyclic S.E) (C : Cut S.E) : + ∀ {p : (S.compose hacyc).Pos} {ls : List (S.compose hacyc).Lab} {q : (S.compose hacyc).Pos}, + Discipline.Trace (S.compose hacyc) p ls q → + ∀ (hp : C.mem p.1) (hq : C.mem q.1), + ∃ ls' : List (S.restrict C).Lab, ls'.map (S.labEmb C) = ls ∧ + Discipline.Trace (S.composeCut hacyc C) ⟨⟨p.1, hp⟩, p.2⟩ ls' + ⟨⟨q.1, hq⟩, q.2⟩ := by + intro p ls q ht + induction ht with + | nil => intro _ _; exact ⟨[], rfl, .nil⟩ + | cons hs ht' ih => + intro hp hq + have hq₀ := S.trace_mem_back hacyc C ht' hq + obtain ⟨ls', hmap, ht''⟩ := ih hq₀ hq + cases hs with + | sloc hl => + exact ⟨.loc ⟨_, hp⟩ _ :: ls', by rw [List.map_cons, hmap] <;> rfl, + .cons (.sloc hl) ht''⟩ + | scross e => + exact ⟨.cross ⟨_, hp⟩ ⟨_, hq₀⟩ e :: ls', by rw [List.map_cons, hmap] <;> rfl, + .cons (DiscSys.Step.scross (S := S.restrict C) (r := ⟨_, hp⟩) (r' := ⟨_, hq₀⟩) e) + ht''⟩ + +/-- THE prefix-closure theorem: a composite trace that ENDS in a cut prefix + is a trace of the prefix alone — whatever lies beyond the frontier is + irrelevant to it. With `composeCut_trace_embed`, the prefix's traces + are exactly the composite's traces that end in the prefix. -/ +theorem composeCut_trace_reflect (hacyc : Acyclic S.E) (C : Cut S.E) + {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 ∧ + Discipline.Trace (S.composeCut hacyc C) + ⟨⟨p.1, S.trace_mem_back hacyc C ht hq⟩, p.2⟩ ls' ⟨⟨q.1, hq⟩, q.2⟩ := + S.composeCut_trace_reflect_of hacyc C ht _ hq + +/-- The prefix has no well-typed loop: an instance of the generic theorem. -/ +theorem composeCut_no_loop (hacyc : Acyclic S.E) (C : Cut S.E) + {p : (S.composeCut hacyc C).Pos} {ls : List (S.composeCut hacyc C).Lab} + (ht : Discipline.Trace (S.composeCut hacyc C) p ls p) : ls = [] := + Discipline.no_loop _ ht + +end DiscSys + +/-! ### The two-region interface of `Compose.lean` as a cut crossing + + The interface `A → B` is the single edge of the 2-node DAG + `Reassembly.boolUp` (`false → true`); A is the region `false`, B is + `true`. Its crossing leaves the principal cut `↓false` = the A side. -/ + +/-- The region of a two-region position: `false` for A, `true` for B. -/ +def Pos.region {A B : PathAlgebra} : Pos A B → Bool + | .inA _ => false + | .inB _ => true + +/-- The A side of the interface, as a cut of `boolUp`. -/ +abbrev aSide : Cut Reassembly.boolUp := Cut.past false + +/-- The interface crossing crosses the A-side cut. -/ +theorem cross_crosses_aSide (A B : PathAlgebra) (I : Interface A B) + {p q : Pos A B} (h : Step A B I .cross p q) : + aSide.Crosses p.region q.region := by + cases h with + | cross => exact Cut.edge_crosses_past Reassembly.boolUp_acyclic ⟨rfl, rfl⟩ + +/-- A two-region trace containing a label splits at it. -/ +theorem trace_split (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 → + ∀ {l : CLabel A B}, l ∈ ls → + ∃ ls₁ ls₂ m m', ls = ls₁ ++ l :: ls₂ ∧ Trace A B I p ls₁ m ∧ + Step A B I l m m' ∧ Trace A B I m' ls₂ q := by + intro p ls q ht + induction ht with + | nil => intro l hl; cases hl + | @cons p q₀ _ l₀ ls hs ht' ih => + intro l hl + cases hl with + | head => exact ⟨[], ls, p, q₀, rfl, .nil, hs, ht'⟩ + | tail _ hl' => + obtain ⟨ls₁, ls₂, m, m', he, h₁, hm, h₂⟩ := ih hl' + exact ⟨l₀ :: ls₁, ls₂, m, m', by rw [he]; rfl, .cons hs h₁, hm, h₂⟩ + +/-- `no_back_cross`, lifted from one step to whole traces: a trace that + starts in B ends in B. -/ +theorem trace_stays_in_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 → p.region = true → q.region = true := by + intro p ls q ht + induction ht with + | nil => exact id + | cons hs _ ih => + intro hp + apply ih + cases hs with + | la => cases hp + | lb => rfl + | cross => cases hp + +/-- Every interface crossing in a well-typed two-region trace crosses the + A-side cut, which holds the trace's start and not its end. -/ +theorem trace_cross_crosses_cut (A B : PathAlgebra) (I : Interface A B) + {p q : Pos A B} {ls : List (CLabel A B)} + (ht : Trace A B I p ls q) (hl : CLabel.cross ∈ ls) : + aSide.Crosses false true ∧ aSide.mem p.region ∧ ¬ aSide.mem q.region := by + obtain ⟨_, _, m, m', _, h₁, hm, h₂⟩ := trace_split A B I ht hl + have hc := + Cut.edge_crosses_past Reassembly.boolUp_acyclic (r := false) (r' := true) ⟨rfl, rfl⟩ + refine ⟨hc, ?_, ?_⟩ + · cases hm with + | cross => + cases hpr : p.region with + | false => exact Or.inl rfl + | true => exact absurd (trace_stays_in_B A B I h₁ hpr) (fun h => by cases h) + · cases hm with + | cross => + rw [trace_stays_in_B A B I h₂ rfl] + exact hc.2 + +/-! ### Concrete exhibit: the theorems are not vacuous -/ + +namespace CutExhibit + +open Reassembly + +/-- The one edge of `boolUp`. -/ +theorem e₀ : boolUp false true := ⟨rfl, rfl⟩ + +/-- A concrete trace of `twoTropical`: a hop of weight 2 in region `false` + (cost 0 → 3), the crossing (identity on cost), a hop of weight 0 in + region `true` (cost 3 → 4). -/ +theorem trace₀ : + Discipline.Trace (twoTropical.compose boolUp_acyclic) ⟨false, (0 : Nat)⟩ + [.loc false (2 : Nat), .cross false true e₀, .loc true (0 : Nat)] ⟨true, (4 : Nat)⟩ := + .cons (.sloc rfl) (.cons (.scross e₀) (.cons (.sloc rfl) .nil)) + +/-- Its crossing leaves a cut that holds the start region and not the end. -/ +example : ∃ C : Cut boolUp, C.Crosses false true ∧ C.mem false ∧ ¬ C.mem true := + twoTropical.trace_cross_crosses_cut boolUp_acyclic trace₀ (.tail _ (.head _)) + +/-- The prefix of `trace₀` that stays in region `false` is a trace of the + cut prefix `↓false` alone. -/ +example : ∃ ls' : List (twoTropical.restrict (Cut.past false)).Lab, + ls'.map (twoTropical.labEmb (Cut.past false)) = [.loc false (2 : Nat)] ∧ + Discipline.Trace (twoTropical.composeCut boolUp_acyclic (Cut.past false)) + ⟨⟨false, Or.inl rfl⟩, (0 : Nat)⟩ ls' ⟨⟨false, Or.inl rfl⟩, (3 : Nat)⟩ := + twoTropical.composeCut_trace_reflect_of boolUp_acyclic (Cut.past false) + (.cons (.sloc rfl) .nil) (Or.inl rfl) (Or.inl rfl) + +/-- Negative control: on a self-loop no cut is crossed. -/ +example (C : Cut (fun _ _ : Unit => True)) : ¬ C.Crosses () () := + Cut.path_back_crosses_no_cut (.single trivial) C + +end CutExhibit + +end Marches diff --git a/Marches/Tropical.lean b/Marches/Tropical.lean index f9686b1..d16851e 100644 --- a/Marches/Tropical.lean +++ b/Marches/Tropical.lean @@ -34,4 +34,67 @@ theorem tropical_no_return (l : Nat) (ls : List Nat) (a : Nat) : run TropicalNat (l :: ls) a ≠ a := no_return TropicalNat tropical_strict l ls a +/-! ### The grade at a crossing (rung 3) + + `TropicalNat` read as a (min, +) grade, in the path algebra's own terms: + alternatives keep the cheaper route (`better` is `<`), sequencing adds + costs, and the unit of sequencing is cost `0`, the grade of the empty + word. choreographic-types (pinned at edb784a) records that K-CUT-LOSS + uses exactly two laws, `𝟙 ⊗ x ≡ x` and `x ⊕ x ≡ x` (K-4, TESTED there + by `scripts/minimal-laws.sh`). Both hold here. Whether this reading + agrees with any Agda instance is a cross-prover question: ASSUMED, + port-and-reprove (resource-algebra M-2 idiom). -/ + +namespace TropicalGrade + +/-- Alternatives (`⊕`): keep the cheaper of two routes. -/ +def alt (a b : Nat) : Nat := min a b + +/-- Sequencing (`⊗`): costs add along a path. -/ +def seq (a b : Nat) : Nat := a + b + +/-- The unit of sequencing (`𝟙`): the cost of the empty word. -/ +def one : Nat := 0 + +/-- K-4, first law: `𝟙 ⊗ x ≡ x`. -/ +theorem seq_unitl (x : Nat) : seq one x = x := Nat.zero_add x + +/-- K-4, second law: `x ⊕ x ≡ x`. -/ +theorem alt_idem (x : Nat) : alt x x = x := ite_self x + +/-- Extension is sequencing with the label's cost `w + 1`. -/ +theorem ext_eq_seq (w a : Nat) : TropicalNat.ext w a = seq a (w + 1) := rfl + +/-- The unit belongs to the empty word only: no label costs `𝟙`. This is + strict inflation, read as a grade. -/ +theorem label_cost_ne_one (w : Nat) : w + 1 ≠ one := fun h => Nat.noConfusion h + +/-- `alt` selects the `better` route. -/ +theorem alt_of_better {a b : Nat} (h : TropicalNat.better a b) : alt a b = a := + Nat.min_eq_left (Nat.le_of_lt h) + +/-- The order `alt` induces, in resource-algebra's convention at cf9235c + (`a ≼ b` when `b` absorbs `a`). It is defined here for marches' own + grade; it is NOT the Agda `_≼_`, and no link between them is claimed. -/ +def altLe (a b : Nat) : Prop := alt a b = b + +/-- S-3 inside marches: `better` runs WITH cost, the induced order runs + AGAINST it. A better route sits ABOVE a worse one in `altLe`, as in + resource-algebra's Loss and opposite to its MaxPlus. Any K-CUT-WARRANT + bound ported here must be checked for direction (W-4). -/ +theorem better_reverses_altLe {a b : Nat} (h : TropicalNat.better a b) : altLe b a := + ite_eq_right (Nat.not_le_of_gt h) + +/-- `𝟙` is the TOP of `altLe`: every grade is below it (as Loss's `fin 0`). -/ +theorem altLe_one : ∀ x : Nat, altLe x one + | 0 => rfl + | _ + 1 => rfl + +/-- Computed witness, the same numbers as resource-algebra's S-3: + `1` is better than `2`, and `2 ≼ 1`. -/ +theorem s3_witness : TropicalNat.better (1 : Nat) (2 : Nat) ∧ altLe 2 1 := + ⟨Nat.lt_succ_self 1, rfl⟩ + +end TropicalGrade + end Marches diff --git a/README.adoc b/README.adoc index 33a2df6..469d5ef 100644 --- a/README.adoc +++ b/README.adoc @@ -32,6 +32,10 @@ no dependencies): discipline *and* demonstrably oscillates (`Marches/BadGadget.lean`; the `#eval` prints the period-2 orbit). The types reject exactly the policies that misbehave. +* A region crossing is a cut: in an acyclic region DAG every crossing in + a well-typed trace leaves a cut and never re-enters it, and the + composite restricted to a cut prefix is itself a discipline whose traces + are exactly those ending in the prefix (`Marches/Cut.lean`). == What this is NOT @@ -119,6 +123,30 @@ here (as in Gao–Rexford 2001) |`Marches.Acyclic` — hypothesis of `compose`, the SAME notion as the GR hierarchy's; never proven here +|Every DAG edge crosses the principal cut of its source; an edge on a +cycle crosses no cut +|PROVEN (conditional) +|`Cut.edge_crosses_past` — consumes `Acyclic`; `Cut.path_back_crosses_no_cut` + +|Every crossing in a well-typed trace crosses a cut that holds the trace's +start and not its end; a trace that leaves a cut never re-enters it +|PROVEN (conditional) +|`Cut.DiscSys.trace_cross_crosses_cut`, `DiscSys.no_reentry`; two-region +`Interface`: `trace_cross_crosses_cut`, `trace_stays_in_B` + +|`compose` restricted to a cut prefix is a discipline; its traces are +exactly the composite's traces that end in the prefix +|PROVEN (conditional) +|`Cut.DiscSys.composeCut`, `composeCut_trace_embed`, +`composeCut_trace_reflect` + +|`TropicalNat` as a (min,+) grade satisfies `𝟙 ⊗ x = x` and `x ⊕ x = x` +(the two laws K-CUT-LOSS uses); its `better` runs against its ⊕-induced +order +|PROVEN +|`Tropical.TropicalGrade.seq_unitl`, `alt_idem`, `better_reverses_altLe`, +`altLe_one`, `s3_witness` + |Tropical estate integration (`TropicalAdapterPath.lean`) |OPEN |rung 3 @@ -158,12 +186,16 @@ Zero dependencies; no mathlib. CI runs the same build. * `Marches/BadGadget.lean` — DISAGREE, the negative pincer. * `Marches/Freewheel.lean` — rung 1: falsifier F2 discharged; strictness is load-bearing. -* `Marches/Tropical.lean` — (min,+) instance; seam for the estate's - tropical work. +* `Marches/Tropical.lean` — (min,+) instance and its grade reading (the + two K-4 laws, the S-3 order direction); seam for the estate's tropical + work. * `Marches/Reassembly.lean` — *rung 2 headline*: `Discipline`, generic loop-freedom, `PathAlgebra.toDiscipline`, and `DiscSys.compose` — a finite acyclic DAG of disciplines is itself a discipline (reassembly as closure under composition). +* `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). == Licence