hyperpolymath · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026
@@ -29,7 +29,7 @@ jobs:
       - name: Run contract gate
         run: bash tools/check-contract.sh
 
-  # Grade kernel (PWL-01): the one definition of min-plus and of max-plus.
+  # Grade kernel (PWL-01): the one definition of min-plus, max-plus and min-max.
   # Checkout-only and toolchain-free, so it runs on every PR in seconds.
   # It lives in this workflow because actions.lock is keyed by workflow path:
   # a new workflow file would be rejected at startup until the lock is
@@ -48,7 +48,7 @@ jobs:
 
   # The mechanical falsifiers behind the kernel: Idris2 0.8.0 builds the ABI,
   # refuses tests/reject/*.idr for the intended reasons, and agrees with the
-  # PINNED Agda kernel (resource-algebra @ cf9235c, Agda --safe --without-K)
+  # PINNED Agda kernel (resource-algebra at the fetch-siblings.sh pin, Agda --safe --without-K)
   # on tests/transcription/ops.tsv; both provers refuse the wrong rows.
   # Idris2 publishes no binaries and its release-tarball URL 404s (see
   # e2e.yml build-e2e), so 0.8.0 is built from source with Chez Scheme,

@@ -9,6 +9,28 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== MinMax joins the grade kernel (2026-10-14)
+
+* New `ResourceAlgebra/MinMax.idr` transcribes resource-algebra
+  `Instances/MinMax.agda` (hyperpolymath/resource-algebra#4): the bottleneck
+  sequence `minMaxSeq` (max, ∞ absorbing) on Loss's carrier, with Loss's
+  alternatives. The instance and its dioid, ordered and annihilating layers
+  are named implementations (`@{minMax}`, ...), because Idris2 resolves by
+  carrier and `ResourceAlgebra LossGrade` is Loss.
+* `Tropical.tropMax = minMaxSeq`. It was the one grade operation defined
+  outside the kernel, so `tools/grade-kernel.allow` is now empty and the gate
+  names a third single definition (min-max).
+* `ResourceAlgebra/Nat.idr`: `minOfLTE`, `maxDistribLMin`, `maxDistribRMin`
+  (upstream `min-≤`, `max-distribˡ-min`, `max-distribʳ-min`).
+* Separation S-4 `bottleneckIsNotSum`. New reject `MinMaxIsLoss`. The
+  transcription table gains the MinMax sequence: 197 rows, 269 equalities,
+  and a fourth wrong row.
+* resource-algebra pin `cf9235c` → `0b338c9`. Core, Loss, MaxPlus and HWM are
+  unchanged between the two; the kernel headers cite the new pin.
+  occupancy-types is checked against this pin and needs
+  hyperpolymath/occupancy-types#11 (its order lemmas now clash with the new
+  Prelude's); the occupancy-types pin moves when that merges.
+
 ==== Fixed (2026-10-14)
 
 * `Occupancy.WithinMaximum`: `UnderMaximum` now bounds a private memory's

@@ -94,8 +94,8 @@ and runnable locally / as a pre-commit step):
 - *I2 for grades (blocking):* `tools/check-grade-kernel.sh` — the grade kernel
   (`src/abi/TypedWasm/ABI/ResourceAlgebra*`, transcribed from
   hyperpolymath/resource-algebra at the pin in `scripts/fetch-siblings.sh`)
-  holds the one definition of min-plus and of max-plus; no other `.idr` file
-  may define a grade operation or a Nat min/max. `tools/check-kernel-proofs.sh`
+  holds the one definition of min-plus, of max-plus and of min-max; no other
+  `.idr` file may define a grade operation or a Nat min/max. `tools/check-kernel-proofs.sh`
   holds the mechanical falsifiers behind it (Idris2 build, `tests/reject`,
   the Agda/Idris2 transcription table). Both run in `contract-gate.yml`.
 

@@ -374,9 +374,10 @@ predicate.
 
 |Tropical.idr |0 |0 |0 |In package (A1, 2026-04-18). PWL-01 (2026-10-14):
 min-plus drawn from the grade kernel (`+TropCost = LossGrade+`); laws
-re-derived from `+ResourceAlgebra/Loss.idr+`; `+tropMax+` (MinMax
-bottleneck) is the one grade operation outside the kernel, allowlisted
-with its reason in `+tools/grade-kernel.allow+`.
+re-derived from `+ResourceAlgebra/Loss.idr+`. 2026-10-14: `+tropMax+`
+(the bottleneck) is the kernel's MinMax sequence (`+tropMax = minMaxSeq+`,
+`+ResourceAlgebra/MinMax.idr+`), so no grade operation is defined outside
+the kernel and `+tools/grade-kernel.allow+` is empty.
 
 |Epistemic.idr |0 |0 |0 |In package (A1, 2026-04-18). A10 (2026-05-26):
 propagation theorems added — `+freshImpliesEqual+`, `+staleImpliesLT+`,
@@ -404,20 +405,21 @@ RETRACTION R-2026-05-18 + experimental R0–R4). Added `+EchoR+` +
 attestation = a retained residue). Categorical base remains the settled
 fiber/slice structure.
 
-|ResourceAlgebra.idr + ResourceAlgebra/{Nat,Loss,MaxPlus,HWM,Separation}.idr |0 |0 |0 |In package (PWL-01, 2026-10-14). The *grade
+|ResourceAlgebra.idr + ResourceAlgebra/{Nat,Loss,MaxPlus,HWM,MinMax,Separation}.idr |0 |0 |0 |In package (PWL-01, 2026-10-14). The *grade
 kernel*: `+ResourceAlgebra+` / `+IsOrdered+` / `+IsDioid+` /
 `+IsAnnihilating+` interfaces and the Loss (min-plus), MaxPlus
-(max-plus) and HWM (high-water-mark) instances, transcribed from
-`+hyperpolymath/resource-algebra+` @ `+cf9235c+` (Agda `+--safe
---without-K+`). Laws re-proved in Idris2 (PROVEN, `+idris2 --build+`);
+(max-plus), HWM (high-water-mark) and MinMax (min-max, bottleneck; named
+implementations on Loss's carrier) instances, transcribed from
+`+hyperpolymath/resource-algebra+` @ `+0b338c9+` (Agda `+--safe
+--without-K+`; MinMax added 2026-10-14, the rest unchanged since `+cf9235c+`). Laws re-proved in Idris2 (PROVEN, `+idris2 --build+`);
 correspondence to the Agda source ASSUMED (transcription) and TESTED
-on a 172-row operation table, accepted by Agda `+refl+` against the
+on a 197-row operation table, accepted by Agda `+refl+` against the
 pinned sources and by Idris2 `+Refl+` against the port, with a
-3-row negative control refused by both
-(`+tools/check-kernel-proofs.sh+`). Separation S-1..S-3 TESTED
+4-row negative control refused by both
+(`+tools/check-kernel-proofs.sh+`). Separation S-1..S-4 TESTED
 (computed). Negative controls `+tests/reject/{HWMAnnihilates,
-LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus}.idr+` refused
-for the intended reason.
+LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus, MinMaxIsLoss}.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
@@ -641,36 +643,43 @@ rule.
 
 The "same object" above is now one definition. The grade kernel
 (`+src/abi/TypedWasm/ABI/ResourceAlgebra*+`) is the Idris2 transcription of
-`+hyperpolymath/resource-algebra+` @ `+cf9235c+`, the estate's Agda
+`+hyperpolymath/resource-algebra+` @ `+0b338c9+`, the estate's Agda
 (`+--safe --without-K+`) proof kernel for grades, fetched by
-`+scripts/fetch-siblings.sh+`. It holds the only min-plus (Loss) and the only
-max-plus (MaxPlus) in the tree, plus the high-water-mark occupancy grade
-(HWM). `+tools/check-grade-kernel.sh+` fails the build if anything else defines
+`+scripts/fetch-siblings.sh+`. It holds the only min-plus (Loss), the only
+max-plus (MaxPlus) and the only min-max (MinMax, the bottleneck) in the tree,
+plus the high-water-mark occupancy grade (HWM). `+tools/check-grade-kernel.sh+` fails the build if anything else defines
 one. `+Tropical.TropCost+`, `+Echo.EchoGrade+` and (through `+TropCost+`)
 `+Epistemic.syncGrade+` all draw their grade from Loss.
 
 What is proved, and how:
 
-* The interface laws and the three instances are re-proved in Idris2
+* The interface laws and the four instances are re-proved in Idris2
   (`+idris2 --build+`, zero dangerous patterns). PROVEN against the Idris2
   definitions.
 * That those definitions are the Agda ones is a transcription: ASSUMED. On a
-  172-row operation table (every clause of every operation), it is TESTED.
+  197-row operation table (every clause of every operation), it is TESTED.
   Agda accepts each row by `+refl+` against the pinned sources and Idris2
-  accepts it by `+Refl+` against the port. Three wrong rows are refused by
+  accepts it by `+Refl+` against the port. Four wrong rows are refused by
   both (`+tools/check-kernel-proofs.sh+`, in CI as `+contract-gate.yml+` /
   `+kernel-proofs+`).
-* The three grades are not one: S-1 occupancy is not cost, S-2 echo
+* The grades are not one: S-1 occupancy is not cost, S-2 echo
   alternatives are min while tropical alternatives are max, S-3 the order runs
-  opposite ways (`+ResourceAlgebra/Separation.idr+`, computed). So L11's
-  latency cost (Loss carrier), a worst-case cost (MaxPlus) and L13's occupancy
-  (HWM) are kept apart.
+  opposite ways, S-4 a bottleneck is not a sum (`+ResourceAlgebra/Separation.idr+`,
+  computed). So L11's latency cost (Loss carrier), its bottleneck (MinMax), a
+  worst-case cost (MaxPlus) and L13's occupancy (HWM) are kept apart.
 
 One correction to earlier prose. `+Tropical.idr+` was never max-plus: its
 `+TropCost+` is min-plus (the Loss algebra), and its bottleneck layer
 (`+tropMax+`) is min-max, which is neither min-plus nor max-plus.
-`+tests/reject/TropicalIsNotMaxPlus.idr+` is the checked statement. The
-kernel has no MinMax instance, so `+tropMax+` stays local, allowlisted with
-that reason. Whether to add MinMax upstream is an owner decision.
+`+tests/reject/TropicalIsNotMaxPlus.idr+` is the checked statement.
+
+*Resolved 2026-10-14.* The owner ruled to add MinMax upstream
+(hyperpolymath/resource-algebra#4, at the pin `+0b338c9+`).
+`+ResourceAlgebra/MinMax.idr+` transcribes it, `+tropMax+` is its sequence,
+`+tests/reject/MinMaxIsLoss.idr+` refuses reading it as a sum, and
+`+tools/grade-kernel.allow+` is empty. Upstream's strict and lax morphisms
+(`+Morphism.agda+`) are not ported. Level11BottleneckProof's status does not
+move: the bottleneck's laws were already proved; what changed is where its
+sequence is defined.
 
 No level changes status here: L11 and L12 stay draft.
@@ -21,8 +21,8 @@
 set -euo pipefail
 cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
 
-RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}"
-OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-af957280075699c659de0abd9a3b0defade77309}"
+RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe}"
+OCCUPANCY_TYPES_COMMIT="${OCCUPANCY_TYPES_COMMIT:-60134839efe2c6f51a31d977a72c1cf94457e71d}"
 CHOREOGRAPHIC_TYPES_COMMIT="${CHOREOGRAPHIC_TYPES_COMMIT:-edb784a7d26c276c2abfa8399b773d346dbb101e}"
 
 fetch() { # fetch <name> <commit>

@@ -10,7 +10,8 @@
 -- (tools/check-grade-kernel.sh enforces that).
 --
 -- PROVENANCE.  Transcribed from hyperpolymath/resource-algebra
---   src/ResourceAlgebra/Core.agda @ cf9235c532712a783a404c359a1055f40134794a
+--   src/ResourceAlgebra/Core.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe
+-- (unchanged since cf9235c, the pin it was first transcribed at)
 -- (fetched by scripts/fetch-siblings.sh).  Agda --safe --without-K is the
 -- proof kernel; this Idris2 module is the ABI layer and re-proves the same
 -- laws.  Correspondence status: ASSUMED (transcription).  The instance

@@ -7,7 +7,8 @@
 -- (resource-algebra H-2); PROVEN against the definition below.
 --
 -- Transcribed from hyperpolymath/resource-algebra
---   src/ResourceAlgebra/Instances/HWM.agda @ cf9235c532712a783a404c359a1055f40134794a
+--   src/ResourceAlgebra/Instances/HWM.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe
+-- (unchanged since cf9235c, the pin it was first transcribed at)
 -- Correspondence status: ASSUMED (transcription); operation table TESTED on
 -- both sides by tests/transcription.  occupancy-types @ af95728 builds its
 -- reclamation law (OccupancyTypes/Reclaim.agda) on that same Agda module.

@@ -8,7 +8,8 @@
 -- loss grade are this carrier, not copies of it.
 --
 -- Transcribed from hyperpolymath/resource-algebra
---   src/ResourceAlgebra/Instances/Loss.agda @ cf9235c532712a783a404c359a1055f40134794a
+--   src/ResourceAlgebra/Instances/Loss.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe
+-- (unchanged since cf9235c, the pin it was first transcribed at)
 -- which is itself the echo-types loss grade
 --   (echo-types experimental/echo-additive/Grade.agda).
 -- Correspondence status: ASSUMED (transcription); operation table TESTED on

@@ -6,7 +6,8 @@
 -- THE ONE DEFINITION OF MAX-PLUS IN THIS TREE (tools/check-grade-kernel.sh).
 --
 -- Transcribed from hyperpolymath/resource-algebra
---   src/ResourceAlgebra/Instances/MaxPlus.agda @ cf9235c532712a783a404c359a1055f40134794a
+--   src/ResourceAlgebra/Instances/MaxPlus.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe
+-- (unchanged since cf9235c, the pin it was first transcribed at)
 -- which is itself the tropical-types grade (TropicalSessionTypes.lean).
 -- Correspondence status: ASSUMED (transcription); operation table TESTED on
 -- both sides by tests/transcription.  The Lean bridge (resource-algebra M-2)

@@ -0,0 +1,139 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- ResourceAlgebra/MinMax.idr — the min-max (bottleneck) grade on ℕ ∪ {∞}.
+--
+-- THE ONE DEFINITION OF THE BOTTLENECK SEQUENCE IN THIS TREE.
+-- TypedWasm.ABI.Tropical's `tropMax` (the L11 bottleneck layer,
+-- Level11BottleneckProof) is `minMaxSeq`, not a copy of it.
+--
+-- Transcribed from hyperpolymath/resource-algebra
+--   src/ResourceAlgebra/Instances/MinMax.agda @ 0b338c9fc45cd04e7ee7d00b3855cd59d56a2afe
+-- Correspondence status: ASSUMED (transcription); the sequence's operation
+-- table is TESTED on both sides by tests/transcription.
+--
+-- Renaming (the only change from the Agda text): _⊔g_ is minMaxSeq; the
+-- carrier and the alternatives are Loss's own (Agda imports Loss's Grade,
+-- fin / inf and _⊓g_; here LossGrade, Finite / Infinity and lossAlt).
+-- Clause order is kept.
+--
+--   minMaxSeq = sequence     = MAX (the worst hop)       — the "⊗", unit Finite 0
+--   lossAlt   = alternatives = MIN (the better path)     — the "⊕", unit Infinity
+-- Infinity absorbs under sequence but is the identity for alternatives:
+-- and an unreachable alternative is never chosen.
+--
+-- The carrier is shared with Loss ON PURPOSE (upstream Morphism.agda,
+-- `loss-bottleneck`: the identity on the carrier is a lax morphism Loss →
+-- MinMax, because a bottleneck never exceeds the sum).  Idris2 resolves an
+-- interface by its carrier, and `ResourceAlgebra LossGrade` is already Loss,
+-- so this instance and its layers are NAMED implementations: use them with
+-- `@{minMax}`, `@{minMaxDioid}`, ... .  They never take part in search.
+--
+-- Neither min-plus (sequence is max, not +) nor max-plus (max is the
+-- sequence, not the alternatives, and 𝟘 is ∞, not −∞): Separation.idr S-4
+-- and tests/reject/MinMaxIsLoss.idr are the checked statements.
+--
+-- NO believe_me, NO postulate, NO assert_total.  %default total.
+
+module TypedWasm.ABI.ResourceAlgebra.MinMax
+
+import public Data.Nat
+import TypedWasm.ABI.ResourceAlgebra
+import TypedWasm.ABI.ResourceAlgebra.Nat
+import public TypedWasm.ABI.ResourceAlgebra.Loss
+
+%default total
+
+||| Sequence: the worst hop.  Agda `_⊔g_`.
+public export
+minMaxSeq : LossGrade -> LossGrade -> LossGrade
+minMaxSeq Infinity   _          = Infinity
+minMaxSeq (Finite m) Infinity   = Infinity
+minMaxSeq (Finite m) (Finite n) = Finite (maximum m n)
+
+-- ============================================================================
+-- Sequence: (minMaxSeq, Finite 0) is a monoid
+-- ============================================================================
+
+||| Agda `⊔g-assoc`.
+public export
+minMaxSeqAssoc : (a, b, c : LossGrade) ->
+                 minMaxSeq (minMaxSeq a b) c = minMaxSeq a (minMaxSeq b c)
+minMaxSeqAssoc (Finite a) (Finite b) (Finite c) = cong Finite (maxAssoc a b c)
+minMaxSeqAssoc (Finite a) (Finite b) Infinity   = Refl
+minMaxSeqAssoc (Finite a) Infinity   c          = Refl
+minMaxSeqAssoc Infinity   b          c          = Refl
+
+||| Agda `⊔g-unitˡ`.
+public export
+minMaxSeqUnitL : (a : LossGrade) -> minMaxSeq (Finite 0) a = a
+minMaxSeqUnitL (Finite a) = Refl
+minMaxSeqUnitL Infinity   = Refl
+
+||| Agda `⊔g-unitʳ`.
+public export
+minMaxSeqUnitR : (a : LossGrade) -> minMaxSeq a (Finite 0) = a
+minMaxSeqUnitR (Finite a) = cong Finite (maximumZeroNLeft a)
+minMaxSeqUnitR Infinity   = Refl
+
+-- ============================================================================
+-- The instance, and its layers
+-- ============================================================================
+
+||| Agda `MinMax : ResourceAlgebra`.  Named: the carrier is Loss's.
+public export
+[minMax] ResourceAlgebra LossGrade where
+  oplus    = lossAlt
+  otimes   = minMaxSeq
+  zeroG    = Infinity
+  oneG     = Finite 0
+  altAssoc = lossAltAssoc
+  altComm  = lossAltComm
+  altIdem  = lossAltIdem
+  altUnitL = \_ => Refl
+  seqAssoc = minMaxSeqAssoc
+  seqUnitL = minMaxSeqUnitL
+  seqUnitR = minMaxSeqUnitR
+
+||| Agda `MinMax-dioid` (distribˡ).
+public export
+minMaxDistribL : (a, b, c : LossGrade) ->
+                 minMaxSeq a (lossAlt b c) = lossAlt (minMaxSeq a b) (minMaxSeq a c)
+minMaxDistribL (Finite a) (Finite b) (Finite c) = cong Finite (maxDistribLMin a b c)
+minMaxDistribL (Finite a) (Finite b) Infinity   = Refl
+minMaxDistribL (Finite a) Infinity   c          = Refl
+minMaxDistribL Infinity   b          c          = Refl
+
+||| Agda `MinMax-dioid` (distribʳ).
+public export
+minMaxDistribR : (a, b, c : LossGrade) ->
+                 minMaxSeq (lossAlt a b) c = lossAlt (minMaxSeq a c) (minMaxSeq b c)
+minMaxDistribR (Finite a) (Finite b) (Finite c) = cong Finite (maxDistribRMin a b c)
+minMaxDistribR (Finite a) (Finite b) Infinity   = Refl
+minMaxDistribR (Finite a) Infinity   (Finite c) = Refl
+minMaxDistribR (Finite a) Infinity   Infinity   = Refl
+minMaxDistribR Infinity   b          c          = Refl
+
+||| Agda `MinMax-dioid`.
+public export
+[minMaxDioid] IsDioid LossGrade using minMax where
+  distribL = minMaxDistribL
+  distribR = minMaxDistribR
+
+||| Agda `MinMax-ordered = IsDioid.ordered MinMax-dioid`.
+public export
+[minMaxOrdered] IsOrdered LossGrade using minMax where
+  otimesMonoL = dioidMonoL @{minMaxDioid}
+  otimesMonoR = dioidMonoR @{minMaxDioid}
+
+||| Agda `MinMax-annihilating` (annihilʳ).
+public export
+minMaxAnnihilR : (a : LossGrade) -> minMaxSeq a Infinity = Infinity
+minMaxAnnihilR (Finite _) = Refl
+minMaxAnnihilR Infinity   = Refl
+
+||| Agda `MinMax-annihilating`.
+public export
+[minMaxAnnihilating] IsAnnihilating LossGrade using minMax where
+  annihilL = \_ => Refl
+  annihilR = minMaxAnnihilR