diff --git a/.github/workflows/push-email-notify.yml b/.github/workflows/push-email-notify.yml
index f4765e1..438d01a 100644
--- a/.github/workflows/push-email-notify.yml
+++ b/.github/workflows/push-email-notify.yml
@@ -40,7 +40,7 @@ jobs:
     timeout-minutes: 5
     steps:
       - name: Send push notification email
-        uses: hyperpolymath/smtp-notify-action@v0.5.0
+        uses: hyperpolymath/smtp-notify-action@v0.3.0
         with:
           server_address: ${{ secrets.SMTP_HOST }}
           server_port: ${{ secrets.SMTP_PORT }}
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 63fa599..356a2c7 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -1,3 +1,4 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
 == Changelog
 
 All notable changes to this project will be documented in this file.
@@ -8,6 +9,28 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== 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
+  `Finite n ≼ c`, and path bounds compose by the kernel's `otimesMono`
+  (`costBoundedSeq`). New `Level11WorstCaseProof` grades a branching access
+  plan in MaxPlus (`worstCaseThen`, `worstCaseOneOf`). It is DESIGNED: no
+  surface syntax or attestation uses it. The bottleneck stays MinMax.
+* *L12.* `stalenessGrade` is the reader's lag as a Loss grade: fresh = 𝟙,
+  stale ≠ 𝟙, never synced = 𝟘, and relayed lag = ⊗ (`stalenessRelay`).
+  `syncGrade` now carries a note that its number is a version, not a loss.
+* *L13.* New `Occupancy.idr` ports occupancy-types @ `af95728` R-1..R-5
+  (reclamation law, occupancy ≤ cost, strict reclamation, the 4-vs-7 witness)
+  over the kernel's HWM. It binds them to `private_memory` (an HWM grade within
+  the declared maximum) and to `boundary` (the cut that frees peak − drift).
+  The binding is DESIGNED.
+* Kernel additions: each instance's order read in ℕ (`lossLeOfLTE`,
+  `maxPlusLeOfLTE` and inverses); `ResourceAlgebra/Nat.idr` gains `maxLub`
+  and min/max-vs-`LTE` lemmas. These are typed-wasm's own, labelled as such.
+* New rejects: `CostIsOccupancy`, `DriftIsPeak` (occupancy-types R-6) and
+  `WorstCaseIsCheapest`. `tools/check-kernel-proofs.sh` also runs
+  occupancy-types' own Agda check at its pin.
+
 ==== Grade kernel: resource-algebra ported as the ABI's one source of grades (PWL-01, 2026-10-14)
 
 `src/abi/TypedWasm/ABI/ResourceAlgebra.idr` and `ResourceAlgebra/{Nat,Loss,
diff --git a/Cargo.lock b/Cargo.lock
index 447e750..1f6077d 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -224,7 +224,7 @@ version = "0.1.0"
 dependencies = [
  "thiserror",
  "wasm-encoder 0.256.0",
- "wasmparser 0.255.0",
+ "wasmparser 0.256.0",
 ]
 
 [[package]]
@@ -320,17 +320,6 @@ dependencies = [
  "indexmap",
 ]
 
-[[package]]
-name = "wasmparser"
-version = "0.255.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e8e329ef4b5d46e73b91d3ac6924417cad55a8cbbf869c199283383427c3320b"
-dependencies = [
- "bitflags",
- "indexmap",
- "semver",
-]
-
 [[package]]
 name = "wasmparser"
 version = "0.256.0"
@@ -344,17 +333,6 @@ dependencies = [
  "serde",
 ]
 
-[[package]]
-name = "wasmparser"
-version = "0.256.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "60bd825ffedc6cba8a642924ba7ae424afbc47811cffbcb7b92031ec24e59b4c"
-dependencies = [
- "bitflags",
- "indexmap",
- "semver",
-]
-
 [[package]]
 name = "wasmprinter"
 version = "0.256.0"
diff --git a/LEVEL-STATUS.adoc b/LEVEL-STATUS.adoc
index 88868f6..aa243e8 100644
--- a/LEVEL-STATUS.adoc
+++ b/LEVEL-STATUS.adoc
@@ -154,7 +154,16 @@ monotonicity, mirrors `+tropical-resource-typing+`
 `+Bridge.hub_ceiling_le+`), `+ResidueMeasure+` (E→R, mirrors
 `+Resource.EchoBridge+`), and `+Level11BottleneckProof+` +
 `+bottleneckCeilsEdges+` wired into
-`+Proofs.attestL11_Bottleneck+`/`+_Sound+`.*
+`+Proofs.attestL11_Bottleneck+`/`+_Sound+`. PWL-01 step 2: the
+obligations read through the kernel — `+CostBounded c n+` IS the Loss
+order `+Finite n ≼ c+` (`+costBoundedIsLossOrder+` /
+`+lossOrderIsCostBounded+`, PROVEN) and path bounds compose by the
+kernel's `+otimesMono+` (`+costBoundedSeq+`, PROVEN);
+`+Level11WorstCaseProof+` grades a branching plan in MaxPlus with
+`+worstCaseThen+` / `+worstCaseOneOf+` from `+otimesMono+` /
+`+oplusMono+` (PROVEN; the obligation itself DESIGNED — no surface or
+attestation uses it). `+Level11BottleneckProof+` is MinMax, not MaxPlus,
+and stays as it is (`+tests/reject/TropicalIsNotMaxPlus.idr+`).*
 
 |12 |Epistemic safety |Epistemic.idr |Not yet |None |*In package (A1,
 2026-04-18); A10 (2026-05-26) closes the "`freshness propagation under
@@ -165,11 +174,28 @@ sibling `+Tropical.TropCost+` (∞ = never-synced) +
 `+neverSyncedInfeasible+`/`+observedFeasible+`/`+observedNotInfeasible+`
 — extant Nat-indexed proofs untouched. Header IS-NOT note: this
 read-consistency model is a DIFFERENT problem from canonical
-`+epistemic-types+`’ standpoint-indexed modality.*
-
-|13 |Module isolation |ModuleIsolation.idr |(per-module handles, future)
+`+epistemic-types+`’ standpoint-indexed modality. PWL-01 step 2:
+staleness graded in the kernel's Loss — `+stalenessGrade+` is the lag;
+fresh is 𝟙 (`+freshHasNoStaleness+`), stale is not (`+staleHasStaleness+`),
+never-synced is 𝟘 (`+neverSyncedIsCollapse+`), and a relayed lag is the
+kernel's ⊗ (`+stalenessRelay+`), all PROVEN. `+syncGrade+` is kept but
+holds a version, not a loss: ordering it with the kernel order would rank
+older versions higher.*
+
+|13 |Module isolation |ModuleIsolation.idr + Occupancy.idr |(per-module handles, future)
 |12 parser/Checker tests |*v1.2 — Idris2 proof + surface checker live;
-007 lowering DONE (task #5)*
+007 lowering DONE (task #5). PWL-01 step 3: occupancy graded in the
+kernel's HWM — R-1..R-5 of occupancy-types @ `+af95728+` re-proved in
+Idris2 (`+cutFactor+`, `+reclaimLaw+`, `+occupancyAtCut+`,
+`+occupancyLeCost+`, `+noReclaim+`, `+reclaimed+`, `+witness*+`: PROVEN;
+statement correspondence ASSUMED, port-and-reprove), R-6 as
+`+tests/reject/{CostIsOccupancy,DriftIsPeak}.idr+` (TESTED). The L13
+binding — an HWM grade per `+private_memory+` within its declared
+maximum (`+OccupancyGradedMemory+`), a declared `+boundary+` as the cut
+that frees peak − drift (`+BoundaryCut+`, `+boundaryOccupancy+`,
+`+fitsAcrossBoundary+`) — is DESIGNED: nothing links the grade to
+`+memory.grow+` and no checker emits it. `+striated+` occupancy OPEN
+(surface-only construct).*
 
 |14 |Session protocols |SessionProtocol.idr |(typed-state handles,
 future) |13 parser/Checker tests |*v1.3 — Idris2 proof + surface checker
@@ -372,6 +398,12 @@ pinned sources and by Idris2 `+Refl+` against the port, with a
 LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus}.idr+` refused
 for the intended reason.
 
+|Occupancy.idr |0 |0 |0 |In package (PWL-01 step 3, 2026-10-14). L13
+occupancy over the kernel's HWM grade: occupancy-types
+(`+Reclaim.agda+` / `+Timeline.agda+` / `+Witness.agda+` @ `+af95728+`)
+R-1..R-5 ported and re-proved; L13 binding (`+OccupancyGradedMemory+`,
+`+BoundaryCut+`, `+boundaryFrees+`, `+fitsAcrossBoundary+`) DESIGNED.
+
 |VerifierSpec.idr |0 |0 |0 |Introduced A13 (2026-05-26, PR #72) as
 statement-level spec-of-record for post-A10 items 7+8. *Promoted to
 total bodies 2026-05-27 (PR #79)*: same `+ModuleSummary+` /
diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh
index 20704dc..5d2b313 100755
--- a/scripts/fetch-siblings.sh
+++ b/scripts/fetch-siblings.sh
@@ -9,14 +9,17 @@
 #   resource-algebra  — the grade kernel; src/abi/TypedWasm/ABI/ResourceAlgebra*
 #                       is its Idris2 transcription, and tests/transcription
 #                       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.
 #
 # 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> scripts/fetch-siblings.sh
+#   RESOURCE_ALGEBRA_COMMIT=<sha> OCCUPANCY_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}"
 
 fetch() { # fetch <name> <commit>
   local name="$1" commit="$2" dir="_build/dependencies/$1"
@@ -37,3 +40,4 @@ fetch() { # fetch <name> <commit>
 }
 
 fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT"
+fetch occupancy-types "$OCCUPANCY_TYPES_COMMIT"
diff --git a/src/abi/TypedWasm/ABI/Epistemic.idr b/src/abi/TypedWasm/ABI/Epistemic.idr
index 76e2d3a..57753ab 100644
--- a/src/abi/TypedWasm/ABI/Epistemic.idr
+++ b/src/abi/TypedWasm/ABI/Epistemic.idr
@@ -397,6 +397,10 @@ observedHasProvenance (Observed {oldVer} sync) = Just (oldVer ** sync)
 -- indexed modality.  Adopting the shared grade is vocabulary alignment, NOT a
 -- claim that this layer instantiates the canonical AccessibleModality.
 
+||| NOTE (PWL-01): the number in `syncGrade` is a VERSION, not a loss.  Under the
+||| kernel's Loss order (`LeG`, smaller is higher) comparing two syncGrades
+||| ranks the OLDER version higher, so do not order them with `LeG`.  The
+||| Loss reading of staleness is `stalenessGrade` below (the lag).
 ||| The tropical sync-grade of a knowledge state, read as irrecoverability:
 ||| never-observed (`Unknown`) relegates to `Infinity` (infeasible / unreachable
 ||| knowledge); knowledge observed at version `v` has finite grade `Finite v`.
@@ -422,3 +426,86 @@ public export
 observedNotInfeasible : (s : Sync mod field old ver) ->
                         Not (syncGrade (Observed {oldVer = old} s) = Infinity)
 observedNotInfeasible _ Refl impossible
+
+-- ============================================================================
+-- Staleness as a Loss grade (PWL-01 step 2, 2026-10-14 — ADDITIVE)
+-- ============================================================================
+--
+-- L12 staleness, graded in the kernel's Loss instance
+-- (TypedWasm.ABI.ResourceAlgebra.Loss): a reader's loss is its LAG, the
+-- number of versions it is behind.  Fresh knowledge loses nothing (𝟙 =
+-- Finite 0, the top of the Loss order); never-synced knowledge is total
+-- collapse (𝟘 = Infinity, the bottom).  Lag accumulates along a relay of
+-- readers by the kernel's sequence (⊗ = +), `stalenessRelay`.  Nothing
+-- above is re-indexed; the A10–A14 proofs are untouched.
+
+||| Staleness of knowing version `known` when the field is at `current`:
+||| the lag, as a Loss grade.
+public export
+stalenessGrade : (known, current : Nat) -> LossGrade
+stalenessGrade known current = Finite (minus current known)
+
+||| Staleness of a knowledge state against the field's current version.
+||| Never observed is total collapse.
+public export
+knowledgeStaleness : {0 m : ModuleId} -> {0 f : String} -> {ver : Nat} ->
+                     Knowledge m f ver -> (current : Nat) -> LossGrade
+knowledgeStaleness {ver} (Observed _) current = stalenessGrade ver current
+knowledgeStaleness Unknown            _       = Infinity
+
+||| Fresh knowledge loses nothing: its staleness is the kernel's 𝟙.
+public export
+freshHasNoStaleness : {0 m : ModuleId} -> {0 f : String} -> {known, current : Nat} ->
+                      Fresh m f known current ->
+                      stalenessGrade known current = oneG {g = LossGrade}
+freshHasNoStaleness (MkFresh _ _ _ eq) =
+  rewrite eq in cong Finite (sym (minusZeroN current))
+
+||| Stale knowledge loses something: its staleness is not 𝟙.
+public export
+staleHasStaleness : {0 m : ModuleId} -> {0 f : String} -> {known, current : Nat} ->
+                    Stale m f known current ->
+                    Not (stalenessGrade known current = oneG {g = LossGrade})
+staleHasStaleness (MkStale lt) prf =
+  succNotLTEzero (replace {p = \x => LT 0 x} (finiteInjective prf) (minusPos lt))
+
+||| Never-synced knowledge is the kernel's 𝟘 (total collapse).
+public export
+neverSyncedIsCollapse : {0 m : ModuleId} -> {0 f : String} -> (current : Nat) ->
+                        knowledgeStaleness {m} {f} Unknown current = zeroG {g = LossGrade}
+neverSyncedIsCollapse _ = Refl
+
+||| Every staleness is at or below fresh in the Loss order: 𝟙 is the top.
+public export
+freshIsTop : (known, current : Nat) -> LeG (stalenessGrade known current) (oneG {g = LossGrade})
+freshIsTop known current = lossLeOne (stalenessGrade known current)
+
+||| A Level-12 proof is a proof of zero staleness.
+public export
+level12NoStaleness : (p : Level12Proof) ->
+                     stalenessGrade p.knownVersion p.currentVersion = oneG {g = LossGrade}
+level12NoStaleness p = freshHasNoStaleness p.freshness
+
+private
+minusPlusCancel : (x, r : Nat) -> minus (x + r) r = x
+minusPlusCancel x r = rewrite plusCommutative x r in minusPlus r
+
+private
+lagSplits : {r, i, t : Nat} -> LTE r i -> LTE i t ->
+            minus t r = minus t i + minus i r
+lagSplits {r} {i} {t} ri it =
+  -- t = ((t − i) + (i − r)) + r, by (t − i) + i = t and (i − r) + r = i;
+  -- subtract r from both sides.
+  trans (cong (\z => minus z r)
+          (trans (sym (plusMinusLte i t it))
+          (trans (cong (\z => minus t i + z) (sym (plusMinusLte r i ri)))
+                 (plusAssociative (minus t i) (minus i r) r))))
+        (minusPlusCancel (minus t i + minus i r) r)
+
+||| Relayed knowledge: a reader at version r who learned from a reader at i,
+||| itself behind the truth t, lags t by the SEQUENCE of the two lags — the
+||| kernel's ⊗ in Loss.  (r ≤ i ≤ t: knowledge only flows forward.)
+public export
+stalenessRelay : {r, i, t : Nat} -> LTE r i -> LTE i t ->
+                 stalenessGrade r t = otimes (stalenessGrade i t) (stalenessGrade r i)
+stalenessRelay ri it = cong Finite (lagSplits ri it)
diff --git a/src/abi/TypedWasm/ABI/Occupancy.idr b/src/abi/TypedWasm/ABI/Occupancy.idr
new file mode 100644
index 0000000..e47e53c
--- /dev/null
+++ b/src/abi/TypedWasm/ABI/Occupancy.idr
@@ -0,0 +1,243 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- Occupancy.idr — L13 occupancy: the high-water-mark grade of private memory
+-- and what a module-isolation boundary reclaims.
+--
+-- L13 (ModuleIsolation.idr) proves ACCESS isolation.  This module adds the
+-- OCCUPANCY reading: a private memory's run is graded in the kernel's HWM
+-- instance (peak live state, drift still held at the end), and a declared
+-- boundary is a cut in that run.  The reclamation law says what the cut
+-- frees: the suffix after it starts from the prefix's DRIFT, not its PEAK,
+-- so peak − drift is reclaimed at the boundary.
+--
+-- PROVENANCE.  Ported and re-proved from hyperpolymath/occupancy-types
+--   src/OccupancyTypes/{Order,Timeline,Reclaim,Witness}.agda @ af957280075699c659de0abd9a3b0defade77309
+-- (fetched by scripts/fetch-siblings.sh), which states them over
+-- resource-algebra's Instances/HWM.agda, the source of
+-- TypedWasm.ABI.ResourceAlgebra.HWM.  Agda is the proof kernel; these Idris2
+-- proofs are the ABI layer's own.  Statement correspondence: ASSUMED
+-- (port-and-reprove).  Map: Timeline (Agda data) -> List; grade -> timelineGrade;
+-- cut-factor -> cutFactor (R-1); reclaim-law / occupancy-at-cut ->
+-- reclaimLaw / occupancyAtCut (R-2); occupancy≤cost / protocol-occupancy≤cost
+-- -> occupancyLeCost / protocolOccupancyLeCost (R-3); no-reclaim / reclaimed
+-- -> noReclaim / reclaimed (R-4); Witness -> witness* (R-5); the R-6 rejects
+-- are tests/reject/{CostIsOccupancy,DriftIsPeak}.idr.
+--
+-- WHAT IS DESIGNED, NOT PROVED.  That the HWM unit is a WebAssembly page of
+-- the private memory, that a module's run is the sequence of its phases, and
+-- that a declared L13 boundary is where the run is cut: no operational
+-- semantics links the grade to `memory.grow` or to actual frees, and no
+-- surface checker emits these grades.  `striated` regions are surface syntax
+-- only (no ABI type), so their occupancy is OPEN.
+--
+-- NO believe_me, NO postulate, NO assert_total.  %default total.
+
+module TypedWasm.ABI.Occupancy
+
+import Data.List
+import Data.List.Elem
+import Data.Nat
+
+import TypedWasm.ABI.ResourceAlgebra
+import public TypedWasm.ABI.ResourceAlgebra.HWM
+import TypedWasm.ABI.ResourceAlgebra.MaxPlus
+import TypedWasm.ABI.ModuleIsolation
+
+%default total
+
+-- ============================================================================
+-- Order lemmas — occupancy-types Order.agda (beyond what base provides)
+-- ============================================================================
+
+||| Agda `<-+ʳ`: a positive summand makes the sum strictly bigger.
+private
+ltPlusPositive : (m : Nat) -> {n : Nat} -> LT 0 n -> LT m (m + n)
+ltPlusPositive m {n = S k} _ =
+  rewrite sym (plusSuccRightSucc m k) in LTESucc (lteAddRight m)
+
+-- ============================================================================
+-- R-1  A run as the sequence of its phases; the grade factors at every cut
+--      (occupancy-types Timeline.agda, parametric in the algebra)
+-- ============================================================================
+
+||| The grade of a run: its phases in sequence.  Agda `Timeline.grade`.
+public export
+timelineGrade : ResourceAlgebra g => List g -> g
+timelineGrade []        = oneG
+timelineGrade (x :: xs) = otimes x (timelineGrade xs)
+
+||| Cutting a run anywhere factors its grade, in any resource algebra.
+||| Agda `cut-factor` (R-1).
+public export
+cutFactor : ResourceAlgebra g => (xs, ys : List g) ->
+            timelineGrade (xs ++ ys) = otimes (timelineGrade xs) (timelineGrade ys)
+cutFactor []        ys = sym (seqUnitL (timelineGrade ys))
+cutFactor (x :: xs) ys =
+  trans (cong (otimes x) (cutFactor xs ys))
+        (sym (seqAssoc x (timelineGrade xs) (timelineGrade ys)))
+
+-- ============================================================================
+-- R-2 .. R-4  Reclamation at a cut — occupancy-types Reclaim.agda
+-- ============================================================================
+
+||| The reclamation law: the suffix sees the prefix's drift.  Agda
+||| `reclaim-law` (R-2).
+public export
+reclaimLaw : (a, b : HWMGrade) ->
+             peak (hwmSeq a b) = maximum (peak a) (drift a + peak b)
+reclaimLaw (MkHWM _ _ _) (MkHWM _ _ _) = Refl
+
+||| Occupancy never exceeds cost.  Agda `occupancy≤cost` (R-3).
+public export
+occupancyLeCost : (a, b : HWMGrade) -> LTE (peak (hwmSeq a b)) (peak a + peak b)
+occupancyLeCost (MkHWM p1 n1 b1) (MkHWM p2 n2 b2) =
+  maxLub (lteAddRight p1) (plusLteMonotoneRight p2 n1 p1 b1)
+
+||| Nothing reclaimed (drift = peak): occupancy IS cost.  Agda `no-reclaim` (R-4).
+public export
+noReclaim : (a : HWMGrade) -> peak a = drift a -> (c : HWMGrade) ->
+            peak (hwmSeq a c) = peak a + peak c
+noReclaim (MkHWM p n b) eq (MkHWM p2 n2 b2) =
+  rewrite sym eq in
+  trans (maximumCommutative p (p + p2)) (maxAbsorbLTE (lteAddRight p))
+
+||| Strict reclamation: something is released at the cut and the suffix does
+||| something, so occupancy is strictly below cost.  Agda `reclaimed` (R-4).
+public export
+reclaimed : (a, c : HWMGrade) -> LT (drift a) (peak a) -> LT 0 (peak c) ->
+            LT (peak (hwmSeq a c)) (peak a + peak c)
+reclaimed (MkHWM p1 n1 b1) (MkHWM p2 n2 b2) lt pos =
+  maxLub (ltPlusPositive p1 pos) (plusLteMonotoneRight p2 (S n1) p1 lt)
+
+||| At the level of runs: the cut factorisation plus the law.  Agda
+||| `occupancy-at-cut` (R-2).
+public export
+occupancyAtCut : (xs, ys : List HWMGrade) ->
+                 peak (timelineGrade (xs ++ ys))
+               = maximum (peak (timelineGrade xs))
+                         (drift (timelineGrade xs) + peak (timelineGrade ys))
+occupancyAtCut xs ys =
+  trans (cong peak (cutFactor xs ys)) (reclaimLaw (timelineGrade xs) (timelineGrade ys))
+
+||| Agda `protocol-occupancy≤cost` (R-3).
+public export
+protocolOccupancyLeCost : (xs, ys : List HWMGrade) ->
+                          LTE (peak (timelineGrade (xs ++ ys)))
+                              (peak (timelineGrade xs) + peak (timelineGrade ys))
+protocolOccupancyLeCost xs ys =
+  rewrite cutFactor xs ys in occupancyLeCost (timelineGrade xs) (timelineGrade ys)
+
+-- ============================================================================
+-- R-5  Two readings of one run — occupancy-types Witness.agda (computed)
+-- ============================================================================
+--
+-- Phase 1 allocates 4 and releases 3 (drift 1); phase 2 allocates 3 and
+-- holds it.  Occupancy 4 (3 reclaimed at the cut), cost 7.
+
+public export
+witnessA : HWMGrade
+witnessA = MkHWM 4 1 (LTESucc LTEZero)
+
+public export
+witnessB : HWMGrade
+witnessB = MkHWM 3 3 (LTESucc (LTESucc (LTESucc LTEZero)))
+
+||| Agda `Witness.occupancy`.
+public export
+witnessOccupancy : peak (timelineGrade [Occupancy.witnessA, Occupancy.witnessB]) = 4
+witnessOccupancy = Refl
+
+||| Agda `Witness.cost`.
+public export
+witnessCost : timelineGrade [Val 4, Val 3] = Val 7
+witnessCost = Refl
+
+||| Agda `Witness.strict`.
+public export
+witnessStrict : LT (peak (hwmSeq Occupancy.witnessA Occupancy.witnessB))
+                   (peak Occupancy.witnessA + peak Occupancy.witnessB)
+witnessStrict =
+  reclaimed witnessA witnessB (LTESucc (LTESucc LTEZero)) (LTESucc LTEZero)
+
+-- ============================================================================
+-- L13 binding — private memory and boundaries (DESIGNED; see header)
+-- ============================================================================
+
+||| What a cut reclaims: peak − drift.
+public export
+reclaimedAt : HWMGrade -> Nat
+reclaimedAt g = minus (peak g) (drift g)
+
+||| What is reclaimed and what is still held make up the peak exactly.
+public export
+reclaimedPlusDrift : (g : HWMGrade) -> reclaimedAt g + drift g = peak g
+reclaimedPlusDrift (MkHWM p n b) = plusMinusLte n p b
+
+||| A private memory's run stays within its declared maximum (in pages).
+public export
+data WithinMaximum : PrivateMemory -> HWMGrade -> Type where
+  ||| No maximum declared.
+  NoMaximum    : {pm : PrivateMemory} -> {g : HWMGrade} ->
+                 pm.maximum = Nothing -> WithinMaximum pm g
+  ||| The peak does not exceed the declared maximum.
+  UnderMaximum : {pm : PrivateMemory} -> {g : HWMGrade} -> {m : Nat} ->
+                 pm.maximum = Just m -> LTE (peak g) m -> WithinMaximum pm g
+
+||| A private memory graded by occupancy: its run, phase by phase, and the
+||| proof that the run's high-water mark fits the declaration.
+public export
+record OccupancyGradedMemory where
+  constructor MkOccupancyGraded
+  ||| The L13 private memory.
+  memory : PrivateMemory
+  ||| Its run, as consecutive phases.
+  phases : List HWMGrade
+  ||| The run's peak fits the declared maximum.
+  fits   : WithinMaximum memory (timelineGrade phases)
+
+||| A run of an isolated module, cut at one of its declared boundaries.
+public export
+record BoundaryCut (m : IsolatedModule) where
+  constructor MkBoundaryCut
+  ||| The boundary the run crosses.
+  boundary : Boundary
+  ||| It is one the module declared (L13 well-formedness applies to it).
+  declared : Elem boundary m.boundaries
+  ||| Phases before the boundary.
+  before   : List HWMGrade
+  ||| Phases after it.
+  after    : List HWMGrade
+
+||| What the boundary frees: the prefix's peak − drift.
+public export
+boundaryFrees : BoundaryCut m -> Nat
+boundaryFrees c = reclaimedAt (timelineGrade c.before)
+
+||| R-2 at an L13 boundary: the run after the boundary starts from what the
+||| run before it still holds.
+public export
+boundaryOccupancy : (c : BoundaryCut m) ->
+                    peak (timelineGrade (c.before ++ c.after))
+                  = maximum (peak (timelineGrade c.before))
+                            (drift (timelineGrade c.before) + peak (timelineGrade c.after))
+boundaryOccupancy c = occupancyAtCut c.before c.after
+
+||| R-3 at an L13 boundary: occupancy across a boundary never exceeds the
+||| cost of the two sides.
+public export
+boundaryOccupancyLeCost : (c : BoundaryCut m) ->
+                          LTE (peak (timelineGrade (c.before ++ c.after)))
+                              (peak (timelineGrade c.before) + peak (timelineGrade c.after))
+boundaryOccupancyLeCost c = protocolOccupancyLeCost c.before c.after
+
+||| The budget rule a checker would apply at a boundary: if the run before
+||| fits in `m`, and the run after fits in what the boundary left (m minus
+||| the drift), the whole run fits in `m`.
+public export
+fitsAcrossBoundary : {m : Nat} -> (xs, ys : List HWMGrade) ->
+                     LTE (peak (timelineGrade xs)) m ->
+                     LTE (drift (timelineGrade xs) + peak (timelineGrade ys)) m ->
+                     LTE (peak (timelineGrade (xs ++ ys))) m
+fitsAcrossBoundary xs ys before after =
+  rewrite occupancyAtCut xs ys in maxLub before after
diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr
index 8d97bca..4cf0917 100644
--- a/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr
+++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Loss.idr
@@ -175,3 +175,39 @@ public export
 IsAnnihilating LossGrade where
   annihilL = \_ => Refl
   annihilR = lossAnnihilR
+
+-- ============================================================================
+-- typed-wasm additions (NOT in the Agda source): the order, read in ℕ
+-- ============================================================================
+--
+-- Separation S-3 says the Loss order runs opposite to ℕ's.  Precisely:
+--   Finite n ≼ Finite k   iff   k ≤ n,
+-- and Infinity (𝟘) is below everything, Finite 0 (𝟙) above everything.
+-- L11 uses this to read a numeric cost bound as the kernel order.
+
+||| `Finite` is never `Infinity`.
+public export
+finiteNotInfinity : {n : Nat} -> Not (Finite n = Infinity)
+finiteNotInfinity Refl impossible
+
+||| k ≤ n gives Finite n ≼ Finite k.
+public export
+lossLeOfLTE : {k, n : Nat} -> LTE k n -> LeG (Finite n) (Finite k)
+lossLeOfLTE le = cong Finite (minimumOfLTE le)
+
+||| Finite n ≼ Finite k gives k ≤ n.
+public export
+lteOfLossLe : (n, k : Nat) -> LeG (Finite n) (Finite k) -> LTE k n
+lteOfLossLe n k prf = lteOfMinimum n k (finiteInjective prf)
+
+||| Infinity is the least grade, so no finite grade sits below it:
+||| Finite n ≼ Infinity is false.
+public export
+finiteNotLeInfinity : {n : Nat} -> Not (LeG (Finite n) Infinity)
+finiteNotLeInfinity prf = finiteNotInfinity prf
+
+||| 𝟙 (= Finite 0, no loss) is the top of the Loss order.
+public export
+lossLeOne : (g : LossGrade) -> LeG g (Finite 0)
+lossLeOne (Finite n) = cong Finite (minimumZeroZeroLeft n)
+lossLeOne Infinity   = Refl
diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr
index 5a85c42..f921103 100644
--- a/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr
+++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/MaxPlus.idr
@@ -176,3 +176,20 @@ public export
 IsAnnihilating MaxPlusGrade where
   annihilL = \_ => Refl
   annihilR = maxPlusAnnihilR
+
+-- ============================================================================
+-- typed-wasm additions (NOT in the Agda source): the order, read in ℕ
+-- ============================================================================
+--
+-- The MaxPlus order IS ℕ's on finite grades:  Val m ≼ Val n  iff  m ≤ n.
+-- L11's worst-case bound uses it to read a numeric bound as the kernel order.
+
+||| m ≤ n gives Val m ≼ Val n.
+public export
+maxPlusLeOfLTE : {m, n : Nat} -> LTE m n -> LeG (Val m) (Val n)
+maxPlusLeOfLTE le = cong Val (maximumOfLTE le)
+
+||| Val m ≼ Val n gives m ≤ n.
+public export
+lteOfMaxPlusLe : (m, n : Nat) -> LeG (Val m) (Val n) -> LTE m n
+lteOfMaxPlusLe m n prf = lteOfMaximum m n (valInjective prf)
diff --git a/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr b/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr
index 85d5761..b1d64ec 100644
--- a/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr
+++ b/src/abi/TypedWasm/ABI/ResourceAlgebra/Nat.idr
@@ -152,3 +152,48 @@ plusDistribRMin a b c =
 public export
 plusAssoc : (m, n, p : Nat) -> (m + n) + p = m + (n + p)
 plusAssoc m n p = sym (plusAssociative m n p)
+
+-- ============================================================================
+-- typed-wasm additions (NOT in the Agda source): min / max against ℕ's order
+-- ============================================================================
+--
+-- Used to read the instances' induced orders as ℕ's order (Loss.idr,
+-- MaxPlus.idr) and by the occupancy theorems (TypedWasm.ABI.Occupancy).
+
+||| `S` is injective.
+public export
+succInj : {m, n : Nat} -> S m = S n -> m = n
+succInj Refl = Refl
+
+||| A bounded argument is what min returns.
+public export
+minimumOfLTE : {k, n : Nat} -> LTE k n -> minimum n k = k
+minimumOfLTE {n} LTEZero     = minimumZeroZeroLeft n
+minimumOfLTE     (LTESucc q) = cong S (minimumOfLTE q)
+
+||| If min returns its right argument, that argument is the smaller.
+public export
+lteOfMinimum : (n, k : Nat) -> minimum n k = k -> LTE k n
+lteOfMinimum n     Z     _   = LTEZero
+lteOfMinimum Z     (S k) prf = absurd prf
+lteOfMinimum (S n) (S k) prf = LTESucc (lteOfMinimum n k (succInj prf))
+
+||| A smaller argument is absorbed by max.
+public export
+maximumOfLTE : {m, n : Nat} -> LTE m n -> maximum m n = n
+maximumOfLTE LTEZero     = Refl
+maximumOfLTE (LTESucc q) = cong S (maximumOfLTE q)
+
+||| If max returns its right argument, the left one is the smaller.
+public export
+lteOfMaximum : (m, n : Nat) -> maximum m n = n -> LTE m n
+lteOfMaximum Z     n     _   = LTEZero
+lteOfMaximum (S m) Z     prf = absurd prf
+lteOfMaximum (S m) (S n) prf = LTESucc (lteOfMaximum m n (succInj prf))
+
+||| max is the least upper bound.  occupancy-types `max-lub` (Order.agda).
+public export
+maxLub : {a, b, c : Nat} -> LTE a c -> LTE b c -> LTE (maximum a b) c
+maxLub LTEZero     q           = q
+maxLub (LTESucc p) LTEZero     = LTESucc p
+maxLub (LTESucc p) (LTESucc q) = LTESucc (maxLub p q)
diff --git a/src/abi/TypedWasm/ABI/Tropical.idr b/src/abi/TypedWasm/ABI/Tropical.idr
index e803bde..bdb4062 100644
--- a/src/abi/TypedWasm/ABI/Tropical.idr
+++ b/src/abi/TypedWasm/ABI/Tropical.idr
@@ -47,6 +47,7 @@ import TypedWasm.ABI.Region
 import TypedWasm.ABI.Levels
 import public TypedWasm.ABI.ResourceAlgebra
 import public TypedWasm.ABI.ResourceAlgebra.Loss
+import public TypedWasm.ABI.ResourceAlgebra.MaxPlus
 import Data.Nat
 import Data.Fin
 import Data.List
@@ -577,3 +578,117 @@ public export
 bottleneckCeilsEdges : (p : Level11BottleneckProof) -> (e : TropCost) ->
                        Elem e p.edges -> tropLe p.bottleneck e
 bottleneckCeilsEdges p e el = rewrite p.isBottleneck in hubCeiling e el
+
+-- ============================================================================
+-- Level 11 obligations as kernel instantiations (PWL-01 step 2)
+-- ============================================================================
+--
+-- Each L11 obligation below is read through the grade kernel, so promoting
+-- L11 is a matter of instantiating kernel lemmas, not of a new algebra:
+--
+--   Level11Proof / Level11KleeneProof   Loss (min-plus).  The numeric bound
+--       `CostBounded c n` IS the kernel order `Finite n ≼ c` (Loss's order is
+--       ℕ's reversed: the cost sits above its bound), and bounds compose
+--       along a path by the kernel's `otimesMono` (IsOrdered LossGrade).
+--   Level11WorstCaseProof               MaxPlus (max-plus).  A branching
+--       access plan's worst case: max over alternatives, sum along a
+--       sequence; the bound is `worstCase plan ≼ Val bound`, which is ℕ's ≤.
+--       DESIGNED as an obligation: no surface syntax, checker or attestation
+--       uses it yet.
+--   Level11BottleneckProof              MinMax.  Not a kernel instance and
+--       NOT MaxPlus (tests/reject/TropicalIsNotMaxPlus.idr; see the header).
+--       Left as it is.
+
+||| The L11 numeric bound is the kernel's Loss order: `c ≤ n` as a cost is
+||| `Finite n ≼ c` as a grade.
+public export
+costBoundedIsLossOrder : {c : TropCost} -> {n : Nat} -> CostBounded c n -> LeG (Finite n) c
+costBoundedIsLossOrder (BoundedFinite le) = lossLeOfLTE le
+
+||| ...and back: a grade above `Finite n` in the Loss order is a cost
+||| bounded by n (in particular it is finite).
+public export
+lossOrderIsCostBounded : {n : Nat} -> (c : TropCost) -> LeG (Finite n) c -> CostBounded c n
+lossOrderIsCostBounded (Finite k) prf = BoundedFinite (lteOfLossLe n k prf)
+lossOrderIsCostBounded Infinity   prf = absurd (finiteNotLeInfinity prf)
+
+||| Path bounds compose: bounded steps give a bounded path, with the bounds
+||| added.  Kernel `otimesMono` (IsOrdered LossGrade), not a new proof.
+public export
+costBoundedSeq : {c1, c2 : TropCost} -> {n1, n2 : Nat} ->
+                 CostBounded c1 n1 -> CostBounded c2 n2 ->
+                 CostBounded (tropMul c1 c2) (n1 + n2)
+costBoundedSeq b1 b2 =
+  lossOrderIsCostBounded (tropMul c1 c2)
+    (otimesMono (costBoundedIsLossOrder b1) (costBoundedIsLossOrder b2))
+
+-- ---- MaxPlus: the worst case over alternatives ----
+
+||| A branching access plan: a single access of known cost, one plan after
+||| another, or one of two plans (which one runs is not known statically).
+public export
+data AccessPlan : Type where
+  ||| One access of the given cost.
+  Step  : (cost : Nat) -> AccessPlan
+  ||| `p` then `q`.
+  Then  : AccessPlan -> AccessPlan -> AccessPlan
+  ||| Either `p` or `q`.
+  OneOf : AccessPlan -> AccessPlan -> AccessPlan
+
+||| The worst-case cost of a plan, graded in the kernel's MaxPlus instance:
+||| costs add along `Then`, the dearer branch counts at `OneOf`.
+public export
+worstCase : AccessPlan -> MaxPlusGrade
+worstCase (Step c)    = Val c
+worstCase (Then p q)  = maxPlusSeq (worstCase p) (worstCase q)
+worstCase (OneOf p q) = maxPlusAlt (worstCase p) (worstCase q)
+
+||| A plan's worst case is always finite (never −∞): every plan does at
+||| least its cheapest branch.
+public export
+worstCaseFinite : (p : AccessPlan) -> (w : Nat ** worstCase p = Val w)
+worstCaseFinite (Step c)    = (c ** Refl)
+worstCaseFinite (Then p q)  =
+  let (a ** pa) = worstCaseFinite p
+      (b ** qb) = worstCaseFinite q
+  in (a + b ** rewrite pa in rewrite qb in Refl)
+worstCaseFinite (OneOf p q) =
+  let (a ** pa) = worstCaseFinite p
+      (b ** qb) = worstCaseFinite q
+  in (maximum a b ** rewrite pa in rewrite qb in Refl)
+
+||| Level 11 worst-case obligation: the plan's worst case is within
+||| `planBound` in the MaxPlus order (ℕ's ≤ on finite grades).
+public export
+record Level11WorstCaseProof where
+  constructor MkLevel11WorstCase
+  ||| The branching access plan.
+  plan        : AccessPlan
+  ||| The declared worst-case bound.
+  planBound   : Nat
+  ||| The plan's worst case does not exceed the bound.
+  planBounded : LeG (worstCase plan) (Val planBound)
+
+||| The bound read as a number: the worst case is `Val w` with w ≤ bound.
+public export
+worstCaseWithin : (prf : Level11WorstCaseProof) ->
+                  (w : Nat ** (worstCase prf.plan = Val w, LTE w prf.planBound))
+worstCaseWithin prf =
+  let (w ** eq) = worstCaseFinite prf.plan
+  in (w ** (eq, lteOfMaxPlusLe w prf.planBound
+                  (replace {p = \g => LeG g (Val prf.planBound)} eq prf.planBounded)))
+
+||| Sequenced plans: the bounds add.  Kernel `otimesMono` (IsOrdered
+||| MaxPlusGrade).
+public export
+worstCaseThen : {p, q : AccessPlan} -> {a, b : Nat} ->
+                LeG (worstCase p) (Val a) -> LeG (worstCase q) (Val b) ->
+                LeG (worstCase (Then p q)) (Val (a + b))
+worstCaseThen pa qb = otimesMono pa qb
+
+||| Alternative plans: the larger bound covers both.  Kernel `oplusMono`.
+public export
+worstCaseOneOf : {p, q : AccessPlan} -> {a, b : Nat} ->
+                 LeG (worstCase p) (Val a) -> LeG (worstCase q) (Val b) ->
+                 LeG (worstCase (OneOf p q)) (Val (maximum a b))
+worstCaseOneOf pa qb = oplusMono pa qb
diff --git a/src/abi/typed-wasm.ipkg b/src/abi/typed-wasm.ipkg
index 9b52812..101afcb 100644
--- a/src/abi/typed-wasm.ipkg
+++ b/src/abi/typed-wasm.ipkg
@@ -29,6 +29,8 @@ modules = TypedWasm.ABI.Region
         , TypedWasm.ABI.ResourceAlgebra.MaxPlus
         , TypedWasm.ABI.ResourceAlgebra.HWM
         , TypedWasm.ABI.ResourceAlgebra.Separation
+        -- L13 occupancy (PWL-01 step 3): R-1..R-5 ported from occupancy-types @ af95728
+        , TypedWasm.ABI.Occupancy
         , TypedWasm.ABI.Echo
         , TypedWasm.ABI.Tropical
         , TypedWasm.ABI.Epistemic
diff --git a/tests/proof/regression.mjs b/tests/proof/regression.mjs
index 1e6c794..6a0c52d 100644
--- a/tests/proof/regression.mjs
+++ b/tests/proof/regression.mjs
@@ -239,6 +239,26 @@ const EXPECTED = [
   ["Echo.idr", /^EchoGrade\s*:/m, "Echo loss grade = the kernel's Loss carrier"],
   ["Echo.idr", /^echoCollapseAbsorbs\s*:/m, "Total collapse absorbs later loss (kernel annihilL)"],
 
+  // PWL-01 step 2-3: L11 / L12 obligations read through the kernel, L13 occupancy.
+  ["Tropical.idr", /^costBoundedIsLossOrder\s*:/m, "L11 bound = kernel Loss order"],
+  ["Tropical.idr", /^lossOrderIsCostBounded\s*:/m, "L11 kernel Loss order = bound"],
+  ["Tropical.idr", /^costBoundedSeq\s*:/m, "L11 path bounds compose (kernel otimesMono)"],
+  ["Tropical.idr", /^record\s+Level11WorstCaseProof/m, "L11 MaxPlus worst-case obligation"],
+  ["Tropical.idr", /^worstCaseThen\s*:/m, "L11 worst case: sequence bounds add"],
+  ["Tropical.idr", /^worstCaseOneOf\s*:/m, "L11 worst case: choice takes the larger bound"],
+  ["Epistemic.idr", /^stalenessGrade\s*:/m, "L12 staleness as a Loss grade"],
+  ["Epistemic.idr", /^freshHasNoStaleness\s*:/m, "L12 fresh = kernel 𝟙"],
+  ["Epistemic.idr", /^staleHasStaleness\s*:/m, "L12 stale ≠ kernel 𝟙"],
+  ["Epistemic.idr", /^stalenessRelay\s*:/m, "L12 relayed lag = kernel ⊗"],
+  ["Occupancy.idr", /^cutFactor\s*:/m, "R-1 grade factors at every cut"],
+  ["Occupancy.idr", /^reclaimLaw\s*:/m, "R-2 reclamation law"],
+  ["Occupancy.idr", /^occupancyAtCut\s*:/m, "R-2 at the level of runs"],
+  ["Occupancy.idr", /^occupancyLeCost\s*:/m, "R-3 occupancy ≤ cost"],
+  ["Occupancy.idr", /^reclaimed\s*:/m, "R-4 strict reclamation"],
+  ["Occupancy.idr", /^witnessOccupancy\s*:/m, "R-5 occupancy 4 / cost 7"],
+  ["Occupancy.idr", /^boundaryOccupancy\s*:/m, "L13 boundary frees peak − drift"],
+  ["Occupancy.idr", /^fitsAcrossBoundary\s*:/m, "L13 budget rule across a boundary"],
+
   // 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/CostIsOccupancy.idr b/tests/reject/CostIsOccupancy.idr
new file mode 100644
index 0000000..8fd9afc
--- /dev/null
+++ b/tests/reject/CostIsOccupancy.idr
@@ -0,0 +1,17 @@
+-- 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 occupancy-types
+-- tests/reject/CostIsOccupancy.agda @ af95728 (R-6).
+--
+-- Occupancy of a sequence is not the sum of the peaks.  Reading it as cost
+-- would charge an L13 run for memory its boundary has already reclaimed.
+-- EXPECT: Can't solve constraint between: plus .* and maximum p \(n \+ p'\)
+module CostIsOccupancy
+
+import TypedWasm.ABI.ResourceAlgebra.HWM
+
+%default total
+
+invalid : (a, c : HWMGrade) -> peak (hwmSeq a c) = peak a + peak c
+invalid (MkHWM p n b) (MkHWM p' n' b') = Refl
diff --git a/tests/reject/DriftIsPeak.idr b/tests/reject/DriftIsPeak.idr
new file mode 100644
index 0000000..82f10ef
--- /dev/null
+++ b/tests/reject/DriftIsPeak.idr
@@ -0,0 +1,17 @@
+-- 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 occupancy-types
+-- tests/reject/DriftIsPeak.agda @ af95728 (R-6).
+--
+-- What is live at a cut is not the peak reached before it; identifying them
+-- is exactly "an L13 boundary never reclaims anything".
+-- EXPECT: Mismatch between: p and n
+module DriftIsPeak
+
+import TypedWasm.ABI.ResourceAlgebra.HWM
+
+%default total
+
+invalid : (a : HWMGrade) -> drift a = peak a
+invalid (MkHWM p n b) = Refl
diff --git a/tests/reject/README.adoc b/tests/reject/README.adoc
index 6f508ba..be1dd71 100644
--- a/tests/reject/README.adoc
+++ b/tests/reject/README.adoc
@@ -15,7 +15,12 @@ because then the control proves nothing.
 | `LossWorstCase` | echo's alternatives read as max, i.e. loss treated as cost (S-2)
 | `DriftExceedsPeak` | a run ending with more live state than its peak
 | `TropicalIsNotMaxPlus` | L11's `TropCost` read as max-plus (it is min-plus)
+| `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
 |===
 
-The first three mirror resource-algebra `tests/reject/*.agda` at the pin in
+`HWMAnnihilates`, `LossWorstCase` and `DriftExceedsPeak` mirror resource-algebra
+`tests/reject/*.agda`; `CostIsOccupancy` and `DriftIsPeak` mirror occupancy-types
+`tests/reject/*.agda`, both at the pins in
 `scripts/fetch-siblings.sh`.
diff --git a/tests/reject/WorstCaseIsCheapest.idr b/tests/reject/WorstCaseIsCheapest.idr
new file mode 100644
index 0000000..bf9c1c4
--- /dev/null
+++ b/tests/reject/WorstCaseIsCheapest.idr
@@ -0,0 +1,17 @@
+-- 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).  typed-wasm's own control.
+--
+-- L11's worst-case grade (MaxPlus) charges the DEARER branch of a choice.
+-- If this were accepted, `Level11WorstCaseProof` would bound the cheapest
+-- path, which is what the min-plus Kleene closure already does.
+-- EXPECT: Mismatch between: 0 and 1
+module WorstCaseIsCheapest
+
+import TypedWasm.ABI.Tropical
+
+%default total
+
+invalid : worstCase (OneOf (Step 2) (Step 3)) = Val 2
+invalid = Refl
diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh
index 2257d5f..b112a7f 100755
--- a/tools/check-kernel-proofs.sh
+++ b/tools/check-kernel-proofs.sh
@@ -4,8 +4,8 @@
 #
 # check-kernel-proofs.sh — the mechanical falsifiers behind the grade kernel.
 #
-#   1. upstream   resource-algebra's own check at the pin (Agda --safe
-#                 --without-K --no-libraries --double-check + its 3 rejects)
+#   1. upstream   resource-algebra's and occupancy-types' own checks 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)
 #   3. rejects    every tests/reject/*.idr must FAIL, at its `invalid`
@@ -57,6 +57,16 @@ if (cd "$RA" && AGDA=agda bash scripts/check-agda.sh) > "$OUT/upstream.log" 2>&1
 else
   cat "$OUT/upstream.log"; err "upstream resource-algebra check failed at the pin"
 fi
+# occupancy-types (L13's reclamation law), checked against OUR resource-algebra
+# pin: its own pin (b2c9f1f) differs from cf9235c only by a CI workflow file.
+OCC="_build/dependencies/occupancy-types"
+[ -d "$OCC/src/OccupancyTypes" ] || die "occupancy-types not fetched — run scripts/fetch-siblings.sh"
+echo "occupancy-types at $(git -C "$OCC" rev-parse HEAD)"
+if (cd "$OCC" && AGDA=agda RESOURCE_ALGEBRA_SRC="$ROOT/$RA/src" bash scripts/check-agda.sh) > "$OUT/upstream-occupancy.log" 2>&1; then
+  pass "upstream occupancy-types: $(tail -1 "$OUT/upstream-occupancy.log")"
+else
+  cat "$OUT/upstream-occupancy.log"; err "upstream occupancy-types check failed at the pin"
+fi
 
 # 2 — the ABI package ---------------------------------------------------------
 # From clean, so a stale TTC cannot mask an error.