hyperpolymath · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026
@@ -4,6 +4,9 @@
 # direction + I3 shared-ABI drift) that keep this repo composable with the rest
 # of the stack. See CONTRACT.adoc. Self-contained (no reusable); runnable
 # locally as tools/check-contract.sh.
+# Also gates the grade kernel (I2, extend don't redefine, applied to grades):
+# tools/check-grade-kernel.sh and tools/check-kernel-proofs.sh, both runnable
+# locally.
 name: Contract Gate
 on:
   pull_request:
@@ -25,3 +28,51 @@ jobs:
         uses: actions/checkout@v7.0.1
       - name: Run contract gate
         run: bash tools/check-contract.sh
+
+  # Grade kernel (PWL-01): the one definition of min-plus and of max-plus.
+  # 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
+  # regenerated, and this one already holds the only action it needs.
+  grade-kernel:
+    name: Grade kernel (one min-plus, one max-plus)
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+      - name: Gate self-test (negative control — seeded duplicates must be caught)
+        run: bash tools/check-grade-kernel.sh --self-test
+      - name: Grep gate
+        run: bash tools/check-grade-kernel.sh
+
+  # 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)
+  # 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 its tag with Chez Scheme.
+  kernel-proofs:
+    name: Grade kernel proofs (Idris2 0.8.0 + Agda)
+    runs-on: ubuntu-latest
+    timeout-minutes: 40
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+      - name: Install Chez Scheme, GMP and Agda
+        run: |
+          sudo apt-get update -qq
+          sudo apt-get install -y -qq chezscheme libgmp-dev agda-bin
+          agda --version
+      - name: Build Idris2 0.8.0 from source
+        run: |
+          git clone --quiet --depth 1 --branch v0.8.0 https://github.com/idris-lang/Idris2 "$RUNNER_TEMP/idris2-src"
+          make -C "$RUNNER_TEMP/idris2-src" bootstrap SCHEME=scheme -j"$(nproc)" > "$RUNNER_TEMP/idris2-build.log" 2>&1 \
+            || { tail -60 "$RUNNER_TEMP/idris2-build.log"; exit 1; }
+          make -C "$RUNNER_TEMP/idris2-src" install > "$RUNNER_TEMP/idris2-install.log" 2>&1 \
+            || { tail -60 "$RUNNER_TEMP/idris2-install.log"; exit 1; }
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+      - name: Fetch siblings at their pins
+        run: bash scripts/fetch-siblings.sh
+      - name: Kernel proofs
+        run: bash tools/check-kernel-proofs.sh
@@ -8,6 +8,32 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== 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,
+MaxPlus,HWM,Separation}.idr` transcribe hyperpolymath/resource-algebra @
+`cf9235c` (Agda `--safe --without-K`): the `ResourceAlgebra` / `IsOrdered` /
+`IsDioid` / `IsAnnihilating` interfaces, the Loss (min-plus), MaxPlus
+(max-plus) and HWM (occupancy) instances, and the S-1..S-3 separation
+witnesses.
+
+* `Tropical.TropCost` is now the kernel's Loss carrier; the twelve semiring
+  axioms and the dioid-order layer are derived from the kernel, and the local
+  `tropMin` / `natMax` copies are deleted. Every public name is kept.
+* `Echo.EchoGrade` names the same Loss carrier.
+* `tools/check-grade-kernel.sh` (with `--self-test`) enforces one min-plus and
+  one max-plus in the tree. `tools/check-kernel-proofs.sh` runs the
+  falsifiers: the Idris2 0.8.0 build, `tests/reject/*.idr` refused for the
+  intended reason, and a 172-row operation table accepted by Agda `refl` against
+  the pinned sources and by Idris2 `Refl` against the port, with wrong rows
+  refused by both. Both run in `contract-gate.yml`.
+* Correction: `Tropical.idr` was never max-plus. Its cost is min-plus and its
+  bottleneck is min-max (`tests/reject/TropicalIsNotMaxPlus.idr`).
+
+No level changes status; L11 and L12 stay draft. `contract.abi.sha256` is
+unchanged: the I3 anchors cover the wire format in `section.rs`, not
+`src/abi/`.
+
 ==== Machine-readable substrate: retired `6a2` layout migrated to `descriptiles` (2026-10-10)
 
 `0-canon/CANONICAL-NAMES.adoc` (owner mandate of 2026-06-30) deprecates the

@@ -91,6 +91,18 @@ and runnable locally / as a pre-commit step):
   `section.rs` against sealed digests in `contract.abi.sha256`; any change fails
   until you bump `abi_version`, cite an ADR, and `--reseal`.
 - *I4 (advisory):* role-purity greps (none for a target).
+- *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 mechanical falsifiers behind it (Idris2 build, `tests/reject`,
+  the Agda/Idris2 transcription table). Both run in `contract-gate.yml`.
+
+The I3 digests cover only the anchored wire-format regions of `section.rs`.
+The Idris2 level proofs under `src/abi/` are not anchors: changing them never
+re-seals `contract.abi.sha256`, and re-sealing to "record" such a change would
+be wrong (`--reseal` is for an `abi_version` bump only).
 
 To change the ABI (the *only* correct way): open a coordinated ADR across
 typed-wasm + AffineScript + ephapax, bump `CONTRACT_ABI_VERSION`, edit the

@@ -142,7 +142,10 @@ proof-term, behavioural lemmas `+loadSafeOffset+` and
 
 |11 |Tropical cost-tracking |Tropical.idr |Not yet |None |*In package
 (A1, 2026-04-18). Commutative-semiring closure PROVEN (A2, 2026-04-18):
-all 12 axioms. Uses structural `+tropMin+` (007-lang template). Zero
+all 12 axioms. PWL-01 (2026-10-14): the algebra is the grade kernel's
+Loss instance (`+TropCost = LossGrade+`, `+ResourceAlgebra/Loss.idr+`);
+the 12 axioms and the order layer are derived from it, and the local
+`+tropMin+` / `+natMax+` copies are deleted (`+tools/check-grade-kernel.sh+`). Zero
 dangerous patterns. A16 (2026-06-16) estate accommodation: added the
 canonical dioid ORDER layer (`+tropLe+` refl/trans + add/mul
 monotonicity, mirrors `+tropical-resource-typing+`
@@ -187,7 +190,7 @@ L16-C (payload primitive/declared region ref), L16-D (exact
 *[sfap]* = "`so far as possible`" — proofs are machine-checked in Idris2
 with zero dangerous patterns. They are as complete as the Idris2 type
 checker can verify. Full mechanical verification against a formal Wasm
-operational semantics (e.g. WasmCert-Isabelle) remains future work.
+operational semantics (e.g. WasmCert-Isabelle) remains future work.
 
 === What "`proven, erased`" means
 
@@ -322,7 +325,11 @@ witness-carrying levels, `+witnessToLegacy+` bridge, `+composeWitness+`
 mirror, `+composeWitnessLegacyAgree+` compat lemma, `+WitnessAchieved+`
 predicate.
 
-|Tropical.idr |0 |0 |0 |In package (A1, 2026-04-18)
+|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+`.
 
 |Epistemic.idr |0 |0 |0 |In package (A1, 2026-04-18). A10 (2026-05-26):
 propagation theorems added — `+freshImpliesEqual+`, `+staleImpliesLT+`,
@@ -350,6 +357,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
+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+`);
+correspondence to the Agda source ASSUMED (transcription) and TESTED
+on a 172-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
+(computed). Negative controls `+tests/reject/{HWMAnnihilates,
+LossWorstCase, DriftExceedsPeak, TropicalIsNotMaxPlus}.idr+` refused
+for the intended reason.
+
 |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+` /
@@ -561,3 +583,41 @@ comonad claims). `+--safe+`, closed.
 
 Nothing pushed or PR’d — drafts are for owner review per the stop-first
 rule.
+
+=== Grade kernel (PWL-01 — 2026-10-14)
+
+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
+(`+--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
+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
+  (`+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.
+  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
+  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
+  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.
+
+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.
+
+No level changes status here: L11 and L12 stay draft.
@@ -0,0 +1,39 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Fetch the sibling proof repositories at their pinned commits
+# (pattern: residual-evidence-types / choreographic-types).
+#
+# typed-wasm consumes these by pin, never by re-declaring their definitions:
+#   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.
+#
+# 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
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+
+RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}"
+
+fetch() { # fetch <name> <commit>
+  local name="$1" commit="$2" dir="_build/dependencies/$1"
+  mkdir -p _build/dependencies
+  if [ ! -d "$dir/.git" ]; then
+    git clone --quiet "https://github.com/hyperpolymath/${name}.git" "$dir"
+  fi
+  if ! git -C "$dir" cat-file -e "${commit}^{commit}" 2>/dev/null; then
+    git -C "$dir" fetch --quiet origin
+  fi
+  git -C "$dir" checkout --quiet --detach "$commit"
+  local got
+  got="$(git -C "$dir" rev-parse HEAD)"
+  case "$got" in
+    "$commit"*) echo "${name} at ${got}" ;;
+    *) echo "ERROR: ${name} resolved to ${got}, expected ${commit}" >&2; exit 1 ;;
+  esac
+}
+
+fetch resource-algebra "$RESOURCE_ALGEBRA_COMMIT"
@@ -76,11 +76,14 @@ _reference_ level.
 **Levels 11-12** (Frontier) are unique to typed-wasm:
 
 * **Level 11 — Tropical Cost-Tracking**: Memory access operations carry
-  semiring costs (min-plus for latency, max-plus for throughput). The
-  type checker proves that any access path through shared memory has
-  bounded total cost. Uses the tropical semiring algebra formalised in
-  007's `TropicalSemiring.idr`. This is the "how expensive is this
-  access pattern?" question answered at compile time.
+  semiring costs (min-plus for latency and cheapest path, min-max for the
+  bottleneck step; a max-plus worst-case grade is available but not yet
+  used). The type checker proves that any access path through shared
+  memory has bounded total cost. The grades come from the ABI's grade
+  kernel (`ResourceAlgebra`, transcribed from hyperpolymath/resource-algebra;
+  007's `TropicalSemiring.idr` is the provenance of the first port). This
+  is the "how expensive is this access pattern?" question answered at
+  compile time.
 
 * **Level 12 — Epistemic Safety**: Tracks which module _knows_ what about
   shared memory state. Module A writes field X; Module B's knowledge of

@@ -37,9 +37,13 @@
 -- Estate cross-reference (audit 2026-06-16) — canonical axis: Agda
 -- hyperpolymath/echo-types @ 2bbdb49 (proofs/agda/{Echo,EchoResidue,EchoGraded,
 -- EchoGradedComonadInterface}.agda; experimental/ for the R0-R4 variance line).
--- The min-plus grade IS the sibling TypedWasm.ABI.Tropical.TropCost; the loss
--- of an echo residue is MEASURED into it via Tropical.ResidueMeasure
--- (accumulation mu = tropMul = +).
+-- The loss grade is the grade kernel's Loss instance (min-plus on ℕ ∪ {∞},
+-- TypedWasm.ABI.ResourceAlgebra.Loss, transcribed from resource-algebra
+-- Instances/Loss.agda @ cf9235c, which is itself echo-types'
+-- experimental/echo-additive/Grade.agda).  `EchoGrade` below names it;
+-- TypedWasm.ABI.Tropical.TropCost is the same carrier, so the loss of an echo
+-- residue is MEASURED into it via Tropical.ResidueMeasure (accumulation
+-- mu = lossSeq = +).  This module defines no grade operation of its own.
 --
 -- WHAT THIS FILE MIRRORS (the SETTLED, machine-checked core):
 --   * the exact-on-a-fiber recoverable subobject: Echo (= Sigma-fiber),
@@ -49,7 +53,9 @@
 --   * the irreversible-relegation step: EchoR + echoToResidue
 --     (~ EchoResidue.agda EchoR / echo-to-residue) — an attestation is exactly
 --     a retained residue of a forgotten witness.
--- WHAT IT DEFERS: the numeric min-plus graded CARRIER and the (co)monad /
+-- WHAT IT NAMES: the numeric min-plus graded CARRIER, as the kernel's Loss
+--   instance (`EchoGrade`, `echoKeep`, `echoCollapse` at the end of this file).
+-- WHAT IT DEFERS: the graded modality D_r itself and its (co)monad /
 --   adjunction laws are live research in echo-types/experimental and are NOT
 --   reproduced here (deferring per caveat 2; do not bake in a variance).
 --
@@ -69,6 +75,9 @@
 
 module TypedWasm.ABI.Echo
 
+import TypedWasm.ABI.ResourceAlgebra
+import public TypedWasm.ABI.ResourceAlgebra.Loss
+
 %default total
 
 -- Shadow the prelude's trans with a definition that reduces on the first
@@ -295,3 +304,38 @@ echoToResidue :
   -> Echo f y -> EchoR C Cert y
 echoToResidue f kappa sound (MkEcho x pf) =
   MkEchoR (kappa x) (replace {p = \v => Cert (kappa x) v} pf (sound x))
+
+-- ============================================================================
+-- The loss grade — the kernel's Loss instance
+-- ============================================================================
+--
+-- echo-types grades loss by ℕ ∪ {∞}: `Finite 0` is `keep` (nothing lost),
+-- `Infinity` is total collapse; sequence adds loss, alternatives keep the
+-- less lossy branch.  That algebra is TypedWasm.ABI.ResourceAlgebra.Loss; it
+-- is named here, not redefined.
+
+||| The echo loss grade.  The kernel's Loss carrier.
+public export
+EchoGrade : Type
+EchoGrade = LossGrade
+
+||| `keep`: no information lost.  The unit of sequence.
+public export
+echoKeep : EchoGrade
+echoKeep = oneG
+
+||| Total collapse: nothing recoverable.  The unit of alternatives.
+public export
+echoCollapse : EchoGrade
+echoCollapse = zeroG
+
+||| Losing nothing then losing `r` loses `r`.  Kernel `seqUnitL`.
+public export
+echoKeepThen : (r : EchoGrade) -> otimes Echo.echoKeep r = r
+echoKeepThen r = seqUnitL r
+
+||| Total collapse absorbs every later loss.  Kernel `annihilL`
+||| (IsAnnihilating LossGrade).
+public export
+echoCollapseAbsorbs : (r : EchoGrade) -> otimes Echo.echoCollapse r = Echo.echoCollapse
+echoCollapseAbsorbs r = annihilL r