diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 356a2c7..cf8cc17 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -9,6 +9,23 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== L16 K-CUT-LOSS, parametric in the grade kernel (PWL-01 step 4, 2026-10-14)
+
+* New `KCut.idr` ports and re-proves choreographic-types `KCut.kcut-loss` @
+  `edb784a` over the kernel's `ResourceAlgebra` interface: graded global and
+  local types, cuts, projection with plain merge, consistency, and
+  `projCut` / `gradeProj` / `cutProjectable` / `kcutLoss` (K-1, K-2, K-3, K-5).
+  It is discharged at Loss, MaxPlus and HWM (K-6), and the upstream worked
+  broker protocol is evaluated in all three.
+* `Choreography.idr`: `GradedChoreography g` with `PartiesDeclared`, the
+  obligation `L16KCutLoss`, and its discharge `l16KCutLoss = kcutLoss`. Tying
+  the graded protocol to `messages` / `LegalTrace` is DESIGNED.
+* Rejects `UnprojectableChoice` and `InconsistentCut` (K-7), each refused on
+  the equality itself. `tools/check-kernel-proofs.sh` also checks upstream
+  `KCut.agda` and its two rejects at the pin.
+* `KCut` re-exports `Decidable.Equality` and the kernel interface, so
+  consumers can compute a concrete protocol's grades by evaluation.
+
 ==== L11 / L12 / L13 read through the grade kernel (PWL-01 steps 2–3, 2026-10-14)
 
 * *L11.* `CostBounded c n` is proved equal to the kernel's Loss order
diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc
index aa243e8..e0c839e 100644
--- a/LEVEL-STATUS.adoc
+++ b/LEVEL-STATUS.adoc
@@ -206,11 +206,21 @@ parser/Checker tests |*v1.4 — Idris2 proof + surface checker (L15-A +
 L15-B) live; L15-C call-graph check deferred to v1.4.x; 007 lowering
 DONE (task #9)*
 
-|16 |Agent choreography |Choreography.idr |(future) |12 parser/Checker
+|16 |Agent choreography |Choreography.idr + KCut.idr |(future) |12 parser/Checker
 tests |*v1.5 — composition proof over L13+L14+L15 live; surface checker
 enforces L16-A (role targets exist), L16-B (message endpoints declared),
 L16-C (payload primitive/declared region ref), L16-D (exact
-`+L13 + L14 + L15+` composition spec).*
+`+L13 + L14 + L15+` composition spec). PWL-01 step 4: grades drawn from
+the kernel — `+GradedChoreography g+` for any `+ResourceAlgebra g+`, with
+the K-CUT-LOSS obligation `+L16KCutLoss+` discharged by `+l16KCutLoss+` =
+`+KCut.kcutLoss+`, a port and re-proof of choreographic-types
+`+KCut.kcut-loss+` @ `+edb784a+` (K-1/K-2/K-3/K-5, and K-6 at Loss,
+MaxPlus, HWM: PROVEN in Idris2; correspondence ASSUMED; K-7 TESTED by
+`+tests/reject/{UnprojectableChoice,InconsistentCut}.idr+`; K-4 not
+re-checked here). Fragment: finite, binary choice, plain merge,
+synchronous. That the graded protocol IS the choreography's
+`+messages+` / `+LegalTrace+` is DESIGNED (only `+PartiesDeclared+` is
+checked); asynchrony OPEN upstream.*
 |===
 
 *[sfap]* = "`so far as possible`" — proofs are machine-checked in Idris2
@@ -315,7 +325,16 @@ envelope (via `+subsumeCompose+`) AND the combined L15 module envelope
 (via `+containedConcat+` + `+l15bSoundness+`). Closes post-A10 audit
 item 3.
 
-|Choreography.idr |0 |0 |0 |In package (v1.5 / L16)
+|Choreography.idr |0 |0 |0 |In package (v1.5 / L16). PWL-01 step 4:
+`+GradedChoreography+`, `+PartiesDeclared+`, `+L16KCutLoss+` /
+`+l16KCutLoss+`.
+
+|KCut.idr |0 |0 |0 |In package (PWL-01 step 4, 2026-10-14). K-CUT-LOSS
+parametric in the grade kernel: graded `+Global+` / `+Local+` types,
+`+Cut+` / `+LCut+`, projection with plain merge, `+Consistent+`;
+`+projCut+`, `+gradeProj+`, `+cutProjectable+`, `+kcutLoss+`, the three
+instance discharges and the worked broker protocol (computed readings
+TESTED). Port of choreographic-types @ `+edb784a+`.
 
 |Proofs.idr |0 |0 |0 |In package. Attestation API hardened A7
 (2026-04-18): every L1-L10 attestation now requires a witness from its
diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh
index 5d2b313..3833578 100755
--- a/scripts/fetch-siblings.sh
+++ b/scripts/fetch-siblings.sh
@@ -11,15 +11,19 @@
 #                       checks the operation tables against this tree in Agda.
 #   occupancy-types   — the reclamation law (R-1..R-6) that
 #                       src/abi/TypedWasm/ABI/Occupancy.idr ports for L13.
+#   choreographic-types — K-CUT-LOSS, which src/abi/TypedWasm/ABI/KCut.idr
+#                       ports for L16.
 #
 # Re-pin deliberately, one commit per pin, and update the module headers that
 # cite the pin in the same commit.  Override for a local experiment with
-#   RESOURCE_ALGEBRA_COMMIT=<sha> OCCUPANCY_TYPES_COMMIT=<sha> scripts/fetch-siblings.sh
+#   RESOURCE_ALGEBRA_COMMIT=<sha> OCCUPANCY_TYPES_COMMIT=<sha> \
+#   CHOREOGRAPHIC_TYPES_COMMIT=<sha> scripts/fetch-siblings.sh
 set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 
 RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}"
 OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-af957280075699c659de0abd9a3b0defade77309}"
+CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-edb784a7d26c276c2abfa8399b773d346dbb101e}"
 
 fetch() { # fetch <name> <commit>
   local name="$1" commit="$2" dir="_build/dependencies/$1"
@@ -41,3 +45,4 @@ fetch() { # fetch <name> <commit>
 
 fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT"
 fetch occupancy-types "$OCCUPANCY_TYPES_COMMIT"
+fetch choreographic-types "$CHOREOGRAPHIC_TYPES_COMMIT"
diff --git a/src/abi/TypedWasm/ABI/Choreography.idr b/src/abi/TypedWasm/ABI/Choreography.idr
index ad30173..ba092ff 100644
--- a/src/abi/TypedWasm/ABI/Choreography.idr
+++ b/src/abi/TypedWasm/ABI/Choreography.idr
@@ -19,10 +19,13 @@ module TypedWasm.ABI.Choreography
 
 import Data.List
 import Data.List.Elem
+import Data.Nat
 
 import TypedWasm.ABI.ModuleIsolation
 import TypedWasm.ABI.SessionProtocol
 import TypedWasm.ABI.ResourceCapabilities
+import TypedWasm.ABI.ResourceAlgebra
+import public TypedWasm.ABI.KCut
 
 %default total
 
@@ -239,3 +242,58 @@ traceSoundness c tr legal =
     (collectIsolation c.realisations c.compositionWitness)
     (collectSessionLinearity c.realisations c.compositionWitness)
     (collectCapabilityContainment c.realisations c.compositionWitness)
+
+-- ============================================================================
+-- Graded choreographies and K-CUT-LOSS (PWL-01 step 4, 2026-10-14)
+-- ============================================================================
+--
+-- The composition theorem above says nothing about grades.  This section
+-- adds them: a choreography's protocol graded in ANY algebra of the grade
+-- kernel (TypedWasm.ABI.ResourceAlgebra), with the K-CUT-LOSS obligation
+-- stated for it and discharged by TypedWasm.ABI.KCut.kcutLoss — a port and
+-- re-proof of choreographic-types `KCut.kcut-loss` @ edb784a (correspondence
+-- ASSUMED; see KCut.idr).  Fragment: finite messages and binary choice,
+-- plain merge, synchronous.
+--
+-- DESIGNED, not proved: that the graded protocol is the choreography's own
+-- (its messages are the declared `messages`, its runs the `LegalTrace`s).
+-- `PartiesDeclared` only checks that every party index names a declared
+-- role.  Asynchrony (queues) is OPEN upstream.
+
+||| Every party index in a protocol is below `n` (here: names a declared role).
+public export
+data PartiesDeclared : (n : Nat) -> Global g -> Type where
+  DEnd    : PartiesDeclared n End
+  DMsg    : {s, r : Party} -> {x : g} -> {gl : Global g} ->
+            LT s n -> LT r n -> PartiesDeclared n gl ->
+            PartiesDeclared n (Msg s r x gl)
+  DChoice : {s, r : Party} -> {x : g} -> {l, k : Global g} ->
+            LT s n -> LT r n -> PartiesDeclared n l -> PartiesDeclared n k ->
+            PartiesDeclared n (Choice s r x l k)
+
+||| An L16 choreography with a graded protocol over its roles: party i is
+||| the i-th declared role.
+public export
+record GradedChoreography (g : Type) where
+  constructor MkGradedChoreography
+  ||| The L16 choreography (roles, messages, realisations, L13–L15 witness).
+  choreography : Choreography
+  ||| Its protocol, graded in the kernel algebra `g`.
+  protocol     : Global g
+  ||| Every party in the protocol is a declared role.
+  declared     : PartiesDeclared (length choreography.roles) protocol
+
+||| The L16 K-CUT-LOSS obligation: at every consistent cut, every party reads
+||| on its own timeline exactly its share of the global grade.
+public export
+L16KCutLoss : {g : Type} -> ResourceAlgebra g => GradedChoreography g -> Type
+L16KCutLoss gc =
+  (p : Party) -> (c : Cut gc.protocol) -> Consistent p c ->
+  gradeAt p (cutGlobal gc.protocol c) = lgrade (cutLocal (proj p gc.protocol) (cutproj p c))
+
+||| Discharged for every graded choreography, parametrically in the grade
+||| algebra: KCut.kcutLoss.  At Loss this is the echo-loss reading, at MaxPlus
+||| worst-case cost, at HWM occupancy (KCut.kcutLossLoss / MaxPlus / HWM).
+public export
+l16KCutLoss : {g : Type} -> ResourceAlgebra g => (gc : GradedChoreography g) -> L16KCutLoss gc
+l16KCutLoss gc p c k = kcutLoss p gc.protocol c k
diff --git a/src/abi/TypedWasm/ABI/KCut.idr b/src/abi/TypedWasm/ABI/KCut.idr
new file mode 100644
index 0000000..2c15342
--- /dev/null
+++ b/src/abi/TypedWasm/ABI/KCut.idr
@@ -0,0 +1,432 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- KCut.idr — K-CUT-LOSS for graded choreographies, parametric in the grade
+-- kernel's resource algebra.
+--
+--   kcutLoss : gradeAt p (cutGlobal gl c) = lgrade (cutLocal (proj p gl) (cutproj p c))
+--
+-- "The global accumulation over a protocol up to a consistent cut, restricted
+-- to party p, equals the grade p reads on its own local timeline up to the
+-- projected cut."  Assembled, as upstream, from three lemmas:
+--   projCut          projection commutes with cutting (no algebra laws)
+--   gradeProj        restricted global grade = grade of the projection, for
+--                    projectable protocols (uses only seqUnitL and altIdem)
+--   cutProjectable   a consistent cut of any protocol is projectable
+--
+-- PROVENANCE.  Ported and re-proved from hyperpolymath/choreographic-types
+--   src/Choreographic/{Party,Global,Local,Projection,KCut,Instances}.agda
+--   @ edb784a7d26c276c2abfa8399b773d346dbb101e
+-- (fetched by scripts/fetch-siblings.sh), there parametric in
+-- resource-algebra's record, here in TypedWasm.ABI.ResourceAlgebra's
+-- interface.  Agda is the proof kernel; these Idris2 proofs are the ABI
+-- layer's own.  Statement correspondence: ASSUMED (port-and-reprove).
+-- Upstream claim map: K-1 kcutLoss, K-2 projCut, K-3 gradeProj,
+-- K-5 cutProjectable, K-6 kcutLossLoss / kcutLossMaxPlus / kcutLossHWM,
+-- K-7 tests/reject/{UnprojectableChoice,InconsistentCut}.idr.
+-- K-4 (only the two laws are used) is checked upstream by
+-- scripts/minimal-laws.sh; it is NOT re-checked here.
+--
+-- Renaming: end/msg/choice -> End/Msg/Choice; local end/send/recv/select/
+-- branch -> LEnd/Send/Recv/Select/Branch; grade↾ -> gradeAt; _↾_ ->
+-- cutGlobal; _↾ₗ_ -> cutLocal; stop/cont-* -> Stop/Cont* (LStop/Cont* for
+-- local cuts); sender/receiver/outside -> Sender/Receiver/Outside.
+--
+-- FRAGMENT (as upstream): finite global types with messages and binary
+-- choice, plain merge, synchronous; no recursion, no full merge, no
+-- delegation, no queues.
+--
+-- NO believe_me, NO postulate, NO assert_total.  %default total.
+
+module TypedWasm.ABI.KCut
+
+import Data.Nat
+-- Re-exported so a consumer can REDUCE `role`, and with it any concrete
+-- protocol's grades, at type level (role unfolds to decEq on Nat).
+import public Decidable.Equality
+
+import public TypedWasm.ABI.ResourceAlgebra
+import TypedWasm.ABI.ResourceAlgebra.Loss
+import TypedWasm.ABI.ResourceAlgebra.MaxPlus
+import TypedWasm.ABI.ResourceAlgebra.HWM
+
+%default total
+
+-- ============================================================================
+-- Parties and roles — Party.agda
+-- ============================================================================
+
+||| A party, by number (decidable equality without primitives).
+public export
+Party : Type
+Party = Nat
+
+||| The role party p plays in an interaction s → r.
+public export
+data Role : (p, s, r : Party) -> Type where
+  Sender   : p = s -> Role p s r
+  Receiver : Not (p = s) -> p = r -> Role p s r
+  Outside  : Not (p = s) -> Not (p = r) -> Role p s r
+
+||| Classify p in the interaction s → r; sender takes precedence when s = r.
+public export
+role : (p, s, r : Party) -> Role p s r
+role p s r with (decEq p s)
+  role p s r | Yes e = Sender e
+  role p s r | No ne with (decEq p r)
+    role p s r | No ne | Yes e   = Receiver ne e
+    role p s r | No ne | No ne'  = Outside ne ne'
+
+-- ============================================================================
+-- Graded global types and cuts — Global.agda
+-- ============================================================================
+
+||| A graded global protocol.
+public export
+data Global : Type -> Type where
+  ||| Done.
+  End    : Global g
+  ||| s → r : x . continuation
+  Msg    : (s, r : Party) -> g -> Global g -> Global g
+  ||| s → r chooses between two continuations.
+  Choice : (s, r : Party) -> g -> Global g -> Global g -> Global g
+
+||| Global accumulation: sequence is ⊗, alternatives are ⊕.
+public export
+grade : ResourceAlgebra g => Global g -> g
+grade End                 = oneG
+grade (Msg _ _ x gl)      = otimes x (grade gl)
+grade (Choice _ _ x l r)  = otimes x (oplus (grade l) (grade r))
+
+||| The share of an interaction's grade that p experiences.
+public export
+at : ResourceAlgebra g => Role p s r -> g -> g
+at (Sender _)     x = x
+at (Receiver _ _) x = x
+at (Outside _ _)  _ = oneG
+
+||| Global accumulation restricted to p.  Agda `grade↾`.
+public export
+gradeAt : ResourceAlgebra g => Party -> Global g -> g
+gradeAt p End                = oneG
+gradeAt p (Msg s r x gl)     = otimes (at (role p s r) x) (gradeAt p gl)
+gradeAt p (Choice s r x l k) = otimes (at (role p s r) x) (oplus (gradeAt p l) (gradeAt p k))
+
+||| A frontier through a global protocol.
+public export
+data Cut : {g : Type} -> Global g -> Type where
+  ||| Cut everything below here.
+  Stop       : {gl : Global g} -> Cut gl
+  ||| Keep the message and continue.
+  ContMsg    : {s, r : Party} -> {x : g} -> {gl : Global g} ->
+               Cut gl -> Cut (Msg s r x gl)
+  ||| Keep the choice and continue into both branches.
+  ContChoice : {s, r : Party} -> {x : g} -> {l, k : Global g} ->
+               Cut l -> Cut k -> Cut (Choice s r x l k)
+
+||| Truncate a protocol at a frontier.  Agda `_↾_`.
+public export
+cutGlobal : (gl : Global g) -> Cut gl -> Global g
+cutGlobal _                  Stop             = End
+cutGlobal (Msg s r x gl)     (ContMsg c)      = Msg s r x (cutGlobal gl c)
+cutGlobal (Choice s r x l k) (ContChoice a b) = Choice s r x (cutGlobal l a) (cutGlobal k b)
+
+-- ============================================================================
+-- Graded local types and local cuts — Local.agda
+-- ============================================================================
+
+||| A graded endpoint type.
+public export
+data Local : Type -> Type where
+  LEnd   : Local g
+  Send   : Party -> g -> Local g -> Local g
+  Recv   : Party -> g -> Local g -> Local g
+  Select : Party -> g -> Local g -> Local g -> Local g
+  Branch : Party -> g -> Local g -> Local g -> Local g
+
+||| The endpoint's own timeline, graded.
+public export
+lgrade : ResourceAlgebra g => Local g -> g
+lgrade LEnd               = oneG
+lgrade (Send _ x l)       = otimes x (lgrade l)
+lgrade (Recv _ x l)       = otimes x (lgrade l)
+lgrade (Select _ x l k)   = otimes x (oplus (lgrade l) (lgrade k))
+lgrade (Branch _ x l k)   = otimes x (oplus (lgrade l) (lgrade k))
+
+||| A frontier through an endpoint type.
+public export
+data LCut : {g : Type} -> Local g -> Type where
+  LStop      : {l : Local g} -> LCut l
+  ContSend   : {q : Party} -> {x : g} -> {l : Local g} -> LCut l -> LCut (Send q x l)
+  ContRecv   : {q : Party} -> {x : g} -> {l : Local g} -> LCut l -> LCut (Recv q x l)
+  ContSelect : {q : Party} -> {x : g} -> {l, k : Local g} ->
+               LCut l -> LCut k -> LCut (Select q x l k)
+  ContBranch : {q : Party} -> {x : g} -> {l, k : Local g} ->
+               LCut l -> LCut k -> LCut (Branch q x l k)
+
+||| Truncate an endpoint at its frontier.  Agda `_↾ₗ_`.
+public export
+cutLocal : (l : Local g) -> LCut l -> Local g
+cutLocal _                LStop            = LEnd
+cutLocal (Send q x l)     (ContSend c)     = Send q x (cutLocal l c)
+cutLocal (Recv q x l)     (ContRecv c)     = Recv q x (cutLocal l c)
+cutLocal (Select q x l k) (ContSelect a b) = Select q x (cutLocal l a) (cutLocal k b)
+cutLocal (Branch q x l k) (ContBranch a b) = Branch q x (cutLocal l a) (cutLocal k b)
+
+-- ============================================================================
+-- Projection — Projection.agda
+-- ============================================================================
+
+||| Prepend a send or receive for a participant; an outsider's continuation
+||| is unchanged.
+public export
+projMsg : {s, r : Party} -> Role p s r -> g -> Local g -> Local g
+projMsg {r} (Sender _)     x l = Send r x l
+projMsg {s} (Receiver _ _) x l = Recv s x l
+projMsg     (Outside _ _)  _ l = l
+
+||| Form a selection or branch for a participant; an outsider takes the left
+||| continuation as representative.
+public export
+projChoice : {s, r : Party} -> Role p s r -> g -> Local g -> Local g -> Local g
+projChoice {r} (Sender _)     x l k = Select r x l k
+projChoice {s} (Receiver _ _) x l k = Branch s x l k
+projChoice     (Outside _ _)  _ l _ = l
+
+||| p's endpoint.
+public export
+proj : Party -> Global g -> Local g
+proj p End                = LEnd
+proj p (Msg s r x gl)     = projMsg (role p s r) x (proj p gl)
+proj p (Choice s r x l k) = projChoice (role p s r) x (proj p l) (proj p k)
+
+||| What a choice demands of p: nothing if p takes part; plain merge (the two
+||| branches project identically) if it does not.
+public export
+Merge : (p : Party) -> Role p s r -> Global g -> Global g -> Type
+Merge p (Sender _)     _ _ = ()
+Merge p (Receiver _ _) _ _ = ()
+Merge p (Outside _ _)  l k = proj p l = proj p k
+
+||| p's projection is well defined.
+public export
+data Projectable : (p : Party) -> Global g -> Type where
+  PEnd    : Projectable p End
+  PMsg    : {s, r : Party} -> {x : g} -> {gl : Global g} ->
+            Projectable p gl -> Projectable p (Msg s r x gl)
+  PChoice : {s, r : Party} -> {x : g} -> {l, k : Global g} ->
+            Projectable p l -> Projectable p k -> Merge p (role p s r) l k ->
+            Projectable p (Choice s r x l k)
+
+||| Project a message cut.
+public export
+cutprojMsg : {s, r : Party} -> {x : g} -> {l : Local g} ->
+             (rho : Role p s r) -> LCut l -> LCut (projMsg rho x l)
+cutprojMsg (Sender _)     c = ContSend c
+cutprojMsg (Receiver _ _) c = ContRecv c
+cutprojMsg (Outside _ _)  c = c
+
+||| Project a choice cut; an outsider keeps only the left cut.
+public export
+cutprojChoice : {s, r : Party} -> {x : g} -> {l, k : Local g} ->
+                (rho : Role p s r) -> LCut l -> LCut k -> LCut (projChoice rho x l k)
+cutprojChoice (Sender _)     a b = ContSelect a b
+cutprojChoice (Receiver _ _) a b = ContBranch a b
+cutprojChoice (Outside _ _)  a _ = a
+
+||| Map a global frontier to p's endpoint.
+public export
+cutproj : {gl : Global g} -> (p : Party) -> Cut gl -> LCut (proj p gl)
+cutproj                          p Stop             = LStop
+cutproj {gl = Msg s r x gl'}     p (ContMsg c)      = cutprojMsg (role p s r) (cutproj p c)
+cutproj {gl = Choice s r x l k}  p (ContChoice a b) =
+  cutprojChoice (role p s r) (cutproj p a) (cutproj p b)
+
+||| A cut is consistent for p when plain merge still holds on the truncated
+||| branches of every choice p does not take part in.
+public export
+data Consistent : (p : Party) -> {gl : Global g} -> Cut gl -> Type where
+  CStop   : {gl : Global g} -> Consistent p (Stop {gl})
+  CMsg    : {s, r : Party} -> {x : g} -> {gl : Global g} -> {c : Cut gl} ->
+            Consistent p c -> Consistent p (ContMsg {s} {r} {x} c)
+  CChoice : {s, r : Party} -> {x : g} -> {l, k : Global g} ->
+            {a : Cut l} -> {b : Cut k} ->
+            Consistent p a -> Consistent p b ->
+            Merge p (role p s r) (cutGlobal l a) (cutGlobal k b) ->
+            Consistent p (ContChoice {s} {r} {x} a b)
+
+-- ============================================================================
+-- K-CUT-LOSS — KCut.agda
+-- ============================================================================
+
+-- (A) Projection commutes with cutting (K-2).
+
+projCutMsg : {s, r : Party} -> (rho : Role p s r) -> (x : g) -> (l : Local g) -> (c : LCut l) ->
+             projMsg rho x (cutLocal l c) = cutLocal (projMsg rho x l) (cutprojMsg {x} rho c)
+projCutMsg (Sender _)     _ _ _ = Refl
+projCutMsg (Receiver _ _) _ _ _ = Refl
+projCutMsg (Outside _ _)  _ _ _ = Refl
+
+projCutChoice : {s, r : Party} -> (rho : Role p s r) -> (x : g) -> (l, k : Local g) ->
+                (a : LCut l) -> (b : LCut k) ->
+                projChoice rho x (cutLocal l a) (cutLocal k b)
+              = cutLocal (projChoice rho x l k) (cutprojChoice {x} rho a b)
+projCutChoice (Sender _)     _ _ _ _ _ = Refl
+projCutChoice (Receiver _ _) _ _ _ _ _ = Refl
+projCutChoice (Outside _ _)  _ _ _ _ _ = Refl
+
+||| Agda `proj-cut` (K-2): no side-conditions, no algebra laws.
+public export
+projCut : (p : Party) -> (gl : Global g) -> (c : Cut gl) ->
+          proj p (cutGlobal gl c) = cutLocal (proj p gl) (cutproj p c)
+projCut p _                  Stop             = Refl
+projCut p (Msg s r x gl)     (ContMsg c)      =
+  trans (cong (projMsg (role p s r) x) (projCut p gl c))
+        (projCutMsg (role p s r) x (proj p gl) (cutproj p c))
+projCut p (Choice s r x l k) (ContChoice a b) =
+  trans (cong2 (projChoice (role p s r) x) (projCut p l a) (projCut p k b))
+        (projCutChoice (role p s r) x (proj p l) (proj p k) (cutproj p a) (cutproj p b))
+
+-- (B) The restricted global grade is the grade of the projection (K-3).
+
+gradeProjMsg : ResourceAlgebra g => {s, r : Party} ->
+               (rho : Role p s r) -> (x : g) -> {y : g} -> {l : Local g} ->
+               y = lgrade l -> otimes (at rho x) y = lgrade (projMsg rho x l)
+gradeProjMsg (Sender _)         x e = cong (otimes x) e
+gradeProjMsg (Receiver _ _)     x e = cong (otimes x) e
+gradeProjMsg (Outside _ _) {y}  _ e = trans (seqUnitL y) e
+
+gradeProjChoice : ResourceAlgebra g => {p, s, r : Party} ->
+                  (rho : Role p s r) -> (x : g) -> {y1, y2 : g} -> {l, k : Global g} ->
+                  y1 = lgrade (proj p l) -> y2 = lgrade (proj p k) ->
+                  Merge p rho l k ->
+                  otimes (at rho x) (oplus y1 y2) = lgrade (projChoice rho x (proj p l) (proj p k))
+gradeProjChoice (Sender _)     x e1 e2 _ = cong (otimes x) (cong2 oplus e1 e2)
+gradeProjChoice (Receiver _ _) x e1 e2 _ = cong (otimes x) (cong2 oplus e1 e2)
+gradeProjChoice {p} (Outside _ _) _ {y1} {y2} {l} e1 e2 m =
+  trans (seqUnitL (oplus y1 y2))
+  (trans (cong2 oplus e1 e2)
+  (trans (cong (oplus (lgrade (proj p l))) (cong lgrade (sym m)))
+         (altIdem (lgrade (proj p l)))))
+
+||| Agda `grade-proj` (K-3).
+public export
+gradeProj : ResourceAlgebra g => (p : Party) -> (gl : Global g) -> Projectable p gl ->
+            gradeAt p gl = lgrade (proj p gl)
+gradeProj p End                PEnd               = Refl
+gradeProj p (Msg s r x gl)     (PMsg pr)          =
+  gradeProjMsg (role p s r) x (gradeProj p gl pr)
+gradeProj p (Choice s r x l k) (PChoice pl pk m)  =
+  gradeProjChoice (role p s r) x (gradeProj p l pl) (gradeProj p k pk) m
+
+-- (C) A consistent cut yields a projectable protocol (K-5).
+
+||| Agda `cut-projectable` (K-5).
+public export
+cutProjectable : (p : Party) -> (gl : Global g) -> (c : Cut gl) -> Consistent p c ->
+                 Projectable p (cutGlobal gl c)
+cutProjectable p _                  Stop             CStop             = PEnd
+cutProjectable p (Msg s r x gl)     (ContMsg c)      (CMsg kc)         =
+  PMsg (cutProjectable p gl c kc)
+cutProjectable p (Choice s r x l k) (ContChoice a b) (CChoice ka kb m) =
+  PChoice (cutProjectable p l a ka) (cutProjectable p k b kb) m
+
+||| K-CUT-LOSS (K-1).  Agda `kcut-loss`.
+public export
+kcutLoss : ResourceAlgebra g => (p : Party) -> (gl : Global g) -> (c : Cut gl) ->
+           Consistent p c ->
+           gradeAt p (cutGlobal gl c) = lgrade (cutLocal (proj p gl) (cutproj p c))
+kcutLoss p gl c k =
+  trans (gradeProj p (cutGlobal gl c) (cutProjectable p gl c k))
+        (cong lgrade (projCut p gl c))
+
+||| The uncut special case.  Agda `kcut-loss-full`.
+public export
+kcutLossFull : ResourceAlgebra g => (p : Party) -> (gl : Global g) -> Projectable p gl ->
+               gradeAt p gl = lgrade (proj p gl)
+kcutLossFull = gradeProj
+
+-- ============================================================================
+-- K-6  Discharged at the three kernel instances — Instances.agda
+-- ============================================================================
+
+||| K-CUT-LOSS for echo loss (min-plus).
+public export
+kcutLossLoss : (p : Party) -> (gl : Global LossGrade) -> (c : Cut gl) -> Consistent p c ->
+               gradeAt p (cutGlobal gl c) = lgrade (cutLocal (proj p gl) (cutproj p c))
+kcutLossLoss = kcutLoss
+
+||| K-CUT-LOSS for worst-case cost (max-plus).
+public export
+kcutLossMaxPlus : (p : Party) -> (gl : Global MaxPlusGrade) -> (c : Cut gl) -> Consistent p c ->
+                  gradeAt p (cutGlobal gl c) = lgrade (cutLocal (proj p gl) (cutproj p c))
+kcutLossMaxPlus = kcutLoss
+
+||| K-CUT-LOSS for occupancy (high-water mark).
+public export
+kcutLossHWM : (p : Party) -> (gl : Global HWMGrade) -> (c : Cut gl) -> Consistent p c ->
+              gradeAt p (cutGlobal gl c) = lgrade (cutLocal (proj p gl) (cutproj p c))
+kcutLossHWM = kcutLoss
+
+-- ============================================================================
+-- A worked protocol — Instances.agda `Worked` (computed readings: TESTED)
+-- ============================================================================
+--
+-- Parties 0 (client), 1 (broker), 2 (server):
+--   0 → 1 : a . 1 → 2 : b . 0 → 2 chooses { 2 → 1 : c . end | 2 → 1 : c . end }
+-- The broker is outside the choice and both branches project identically
+-- for it, so its projection is plain-mergeable.
+
+||| The worked protocol.
+public export
+worked : ResourceAlgebra g => (a, b, c : g) -> Global g
+worked a b c = Msg 0 1 a (Msg 1 2 b (Choice 0 2 oneG (Msg 2 1 c End) (Msg 2 1 c End)))
+
+||| Cut after the broker has forwarded, before the server answers.
+public export
+workedCut : ResourceAlgebra g => {a, b, c : g} -> Cut (worked a b c)
+workedCut = ContMsg (ContMsg (ContChoice Stop Stop))
+
+||| The broker's projection is well defined.
+public export
+workedProjectable : ResourceAlgebra g => {a, b, c : g} -> Projectable 1 (worked a b c)
+workedProjectable = PMsg (PMsg (PChoice (PMsg PEnd) (PMsg PEnd) Refl))
+
+||| The cut is consistent for the broker.
+public export
+workedConsistent : ResourceAlgebra g => {a, b, c : g} -> Consistent 1 (workedCut {a} {b} {c})
+workedConsistent = CMsg (CMsg (CChoice CStop CStop Refl))
+
+||| The keystone at that cut, for the broker, in any algebra.
+public export
+brokerCut : ResourceAlgebra g => (a, b, c : g) ->
+            gradeAt 1 (cutGlobal (worked a b c) (workedCut {a} {b} {c}))
+          = lgrade (cutLocal (proj 1 (worked a b c)) (cutproj 1 (workedCut {a} {b} {c})))
+brokerCut a b c = kcutLoss 1 (worked a b c) workedCut workedConsistent
+
+||| Loss: the broker's restricted grade over the whole protocol is 1 + 2 + 5.
+public export
+lossBroker : gradeAt 1 (worked (Finite 1) (Finite 2) (Finite 5)) = Finite 8
+lossBroker = Refl
+
+||| Loss: at the cut only a and b remain.
+public export
+lossBrokerCut : gradeAt 1 (cutGlobal (worked (Finite 1) (Finite 2) (Finite 5)) KCut.workedCut)
+              = Finite 3
+lossBrokerCut = Refl
+
+||| MaxPlus: the same protocol costs 8.
+public export
+maxPlusBroker : gradeAt 1 (worked (Val 1) (Val 2) (Val 5)) = Val 8
+maxPlusBroker = Refl
+
+||| HWM: peaks 1, 2 and 5 with nothing held between them reach 5, not 8.
+public export
+hwmBroker : peak (gradeAt 1 (worked (MkHWM 1 0 LTEZero) (MkHWM 2 0 LTEZero) (MkHWM 5 0 LTEZero))) = 5
+hwmBroker = Refl
+
+||| HWM: at the cut the peak is 2.
+public export
+hwmBrokerCut : peak (gradeAt 1 (cutGlobal (worked (MkHWM 1 0 LTEZero) (MkHWM 2 0 LTEZero) (MkHWM 5 0 LTEZero))
+                                          KCut.workedCut)) = 2
+hwmBrokerCut = Refl
diff --git a/src/abi/typed-wasm.ipkg b/src/abi/typed-wasm.ipkg
index 101afcb..34e5178 100644
--- a/src/abi/typed-wasm.ipkg
+++ b/src/abi/typed-wasm.ipkg
@@ -19,6 +19,8 @@ modules = TypedWasm.ABI.Region
         , TypedWasm.ABI.ModuleIsolation
         , TypedWasm.ABI.SessionProtocol
         , TypedWasm.ABI.ResourceCapabilities
+        -- K-CUT-LOSS (PWL-01 step 4): ported from choreographic-types @ edb784a
+        , TypedWasm.ABI.KCut
         , TypedWasm.ABI.Choreography
         -- Grade kernel (PWL-01): transcribed from hyperpolymath/resource-algebra
         -- @ cf9235c; the one definition of min-plus (Loss) and of max-plus
diff --git a/tests/proof/regression.mjs b/tests/proof/regression.mjs
index 6a0c52d..6752278 100644
--- a/tests/proof/regression.mjs
+++ b/tests/proof/regression.mjs
@@ -259,6 +259,20 @@ const EXPECTED = [
   ["Occupancy.idr", /^boundaryOccupancy\s*:/m, "L13 boundary frees peak − drift"],
   ["Occupancy.idr", /^fitsAcrossBoundary\s*:/m, "L13 budget rule across a boundary"],
 
+  // PWL-01 step 4: L16 K-CUT-LOSS, parametric in the grade kernel.
+  ["KCut.idr", /^data\s+Global/m, "Graded global protocol"],
+  ["KCut.idr", /^gradeAt\s*:/m, "Global grade restricted to a party (Agda grade↾)"],
+  ["KCut.idr", /^proj\s*:/m, "Endpoint projection"],
+  ["KCut.idr", /^data\s+Consistent/m, "Consistent cut"],
+  ["KCut.idr", /^projCut\s*:/m, "K-2 projection commutes with cutting"],
+  ["KCut.idr", /^gradeProj\s*:/m, "K-3 restricted grade = grade of projection"],
+  ["KCut.idr", /^cutProjectable\s*:/m, "K-5 consistent cut is projectable"],
+  ["KCut.idr", /^kcutLoss\s*:/m, "K-1 K-CUT-LOSS"],
+  ["KCut.idr", /^kcutLossHWM\s*:/m, "K-6 discharged at HWM"],
+  ["KCut.idr", /^lossBroker\s*:/m, "Worked broker protocol (computed)"],
+  ["Choreography.idr", /^record\s+GradedChoreography/m, "L16 graded choreography"],
+  ["Choreography.idr", /^l16KCutLoss\s*:/m, "L16 K-CUT-LOSS obligation discharged"],
+
   // Proofs.idr — LevelAttestationW (standards#130 long-tail closure):
   // witness-indexed attestation GADT with per-level smart ctors,
   // extractors ("entails-semantic-property" lemmas), legacy bridge,
diff --git a/tests/reject/InconsistentCut.idr b/tests/reject/InconsistentCut.idr
new file mode 100644
index 0000000..9e98042
--- /dev/null
+++ b/tests/reject/InconsistentCut.idr
@@ -0,0 +1,29 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (tools/check-kernel-proofs.sh).  Mirrors choreographic-types
+-- tests/reject/InconsistentCut.agda @ edb784a (K-7).
+--
+-- The protocol is projectable for party 2 (both branches identical), but
+-- the cut truncates the left branch after two messages and the right after
+-- one, so the frontier is inconsistent for 2.  Restricted global grade at
+-- the cut: Finite 1 (min 2 1); the local timeline cut (left representative)
+-- reads Finite 2.  The Consistent side-condition is load-bearing.
+-- EXPECT: Mismatch between: S \(plus 0 0\) and 0
+module InconsistentCut
+
+import TypedWasm.ABI.KCut
+import TypedWasm.ABI.ResourceAlgebra.Loss
+
+%default total
+
+gl : Global LossGrade
+gl = Choice 0 1 (Finite 0) (Msg 1 2 (Finite 1) (Msg 1 2 (Finite 1) End))
+                           (Msg 1 2 (Finite 1) (Msg 1 2 (Finite 1) End))
+
+c : Cut InconsistentCut.gl
+c = ContChoice (ContMsg (ContMsg Stop)) (ContMsg Stop)
+
+invalid : gradeAt 2 (cutGlobal InconsistentCut.gl InconsistentCut.c)
+        = lgrade (cutLocal (proj 2 InconsistentCut.gl) (cutproj 2 InconsistentCut.c))
+invalid = Refl
diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc
index be1dd71..d441962 100644
--- a/tests/reject/README.adoc
+++ b/tests/reject/README.adoc
@@ -18,9 +18,13 @@ because then the control proves nothing.
 | `CostIsOccupancy` | an L13 run charged the sum of its peaks, as if the boundary reclaimed nothing (occupancy-types R-6)
 | `DriftIsPeak` | drift identified with peak: "a boundary never reclaims" (occupancy-types R-6)
 | `WorstCaseIsCheapest` | L11's MaxPlus worst case charging the cheaper branch
+| `UnprojectableChoice` | K-CUT-LOSS without the Projectable side-condition (choreographic-types K-7)
+| `InconsistentCut` | K-CUT-LOSS without the Consistent side-condition (choreographic-types K-7)
 |===
 
 `HWMAnnihilates`, `LossWorstCase` and `DriftExceedsPeak` mirror resource-algebra
 `tests/reject/*.agda`; `CostIsOccupancy` and `DriftIsPeak` mirror occupancy-types
-`tests/reject/*.agda`, both at the pins in
+`tests/reject/*.agda`; `UnprojectableChoice` and `InconsistentCut` mirror
+choreographic-types
+`tests/reject/*.agda`, all at the pins in
 `scripts/fetch-siblings.sh`.
diff --git a/tests/reject/UnprojectableChoice.idr b/tests/reject/UnprojectableChoice.idr
new file mode 100644
index 0000000..422585d
--- /dev/null
+++ b/tests/reject/UnprojectableChoice.idr
@@ -0,0 +1,24 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- MUST FAIL (tools/check-kernel-proofs.sh).  Mirrors choreographic-types
+-- tests/reject/UnprojectableChoice.agda @ edb784a (K-7).
+--
+-- Party 2 is outside the choice 0 → 1, and the two branches project to
+-- different local types for it (recv at loss 2 vs recv at loss 1).  Plain
+-- merge fails, and the equality K-CUT-LOSS promises is false: restricted
+-- global grade Finite 1 (min of the branches), local grade Finite 2 (the
+-- left representative).  The Projectable side-condition is load-bearing.
+-- EXPECT: Mismatch between: S \(plus 0 0\) and 0
+module UnprojectableChoice
+
+import TypedWasm.ABI.KCut
+import TypedWasm.ABI.ResourceAlgebra.Loss
+
+%default total
+
+gl : Global LossGrade
+gl = Choice 0 1 (Finite 0) (Msg 1 2 (Finite 2) End) (Msg 1 2 (Finite 1) End)
+
+invalid : gradeAt 2 UnprojectableChoice.gl = lgrade (proj 2 UnprojectableChoice.gl)
+invalid = Refl
diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh
index b112a7f..9ce6e1b 100755
--- a/tools/check-kernel-proofs.sh
+++ b/tools/check-kernel-proofs.sh
@@ -4,7 +4,8 @@
 #
 # check-kernel-proofs.sh — the mechanical falsifiers behind the grade kernel.
 #
-#   1. upstream   resource-algebra's and occupancy-types' own checks at the pins (Agda --safe
+#   1. upstream   resource-algebra's and occupancy-types' own checks, and
+#                 choreographic-types' KCut slice, at the pins (Agda --safe
 #                 --without-K --no-libraries --double-check + their rejects)
 #   2. build      idris2 --build src/abi/typed-wasm.ipkg: exit 0 AND no
 #                 `Error:` line (idris2 can exit 0 while printing an error)
@@ -67,6 +68,29 @@ if (cd "$OCC" && AGDA=agda RESOURCE_ALGEBRA_SRC="$ROOT/$RA/src" bash scripts/che
 else
   cat "$OUT/upstream-occupancy.log"; err "upstream occupancy-types check failed at the pin"
 fi
+# choreographic-types: only the K-CUT-LOSS slice KCut.idr ports (KCut.agda and
+# its imports need resource-algebra alone; the rest of the repo also needs
+# epistemic-types), plus the two side-condition rejects (K-7), each of which
+# must be refused at its invalid declaration with upstream's "1 != 2".
+CT="_build/dependencies/choreographic-types"
+[ -d "$CT/src/Choreographic" ] || die "choreographic-types not fetched — run scripts/fetch-siblings.sh"
+echo "choreographic-types at $(git -C "$CT" rev-parse HEAD)"
+ct_flags=("${AGDA_FLAGS[@]}" -i "$RA/src" -i "$CT/src")
+if agda "${ct_flags[@]}" "$CT/src/Choreographic/KCut.agda" > "$OUT/upstream-kcut.log" 2>&1; then
+  pass "upstream choreographic-types: KCut.agda (K-1..K-5) checks against the resource-algebra pin"
+else
+  cat "$OUT/upstream-kcut.log"; err "upstream choreographic-types KCut.agda failed at the pin"
+fi
+for name in UnprojectableChoice InconsistentCut; do
+  log="$OUT/upstream-reject-$name.log"
+  if agda "${ct_flags[@]}" -i "$CT/tests/reject" "$CT/tests/reject/$name.agda" > "$log" 2>&1; then
+    err "upstream reject $name ACCEPTED"
+  elif grep -qE "$WRONG_REASON" "$log" || ! grep -q '1 != 2' "$log"; then
+    cat "$log"; err "upstream reject $name refused for the wrong reason"
+  else
+    pass "upstream choreographic-types: rejected $name (1 != 2)"
+  fi
+done
 
 # 2 — the ABI package ---------------------------------------------------------
 # From clean, so a stale TTC cannot mask an error.