feat: MinMax instance and strict/lax morphisms between instances

.github/CODEOWNERS

@@ -2,14 +2,14 @@
 # CODEOWNERS - Define code review assignments
 # See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners
 #
-# Replace {{OWNER}} with your GitHub username or team
+# Repository owner: hyperpolymath
 
 # Default owners for everything
-* @{{OWNER}}
+* @hyperpolymath
 
 # Security-sensitive files require explicit review
-SECURITY.md @{{OWNER}}
-.github/workflows/ @{{OWNER}}
-.machine_readable/contractiles/trust/ @{{OWNER}}
-*_chora.deed @{{OWNER}}
-.machine_readable/ @{{OWNER}}
+SECURITY.md @hyperpolymath
+.github/workflows/ @hyperpolymath
+.machine_readable/contractiles/trust/ @hyperpolymath
+*_chora.deed @hyperpolymath
+.machine_readable/ @hyperpolymath

.github/workflows/actions.lock

@@ -57,6 +57,8 @@ workflows:
         - 'actions/deploy-pages@v5.0.1'
         - 'actions/upload-pages-artifact@v5.0.0'
         - 'haskell-actions/setup@v2.12.0'
+    '.github/workflows/proofs.yml':
+        - 'actions/checkout@v7.0.1'
     '.github/workflows/push-email-notify.yml':
         - 'hyperpolymath/smtp-notify-action@v0.3.0'
     '.github/workflows/quality.yml':

.github/workflows/proofs.yml

@@ -1,4 +1,4 @@
 # SPDX-License-Identifier: MPL-2.0
 name: Agda proofs
 # DESIGNED until its first green run. Pattern: residual-evidence-types
 # proofs.yml — the prover is the Debian agda-bin package at the pinned
@@ -11,17 +11,19 @@
 permissions:
   contents: read
 jobs:
   proofs:
     name: Core proofs and expected rejections
     runs-on: ubuntu-latest
     container: debian:trixie-slim
     steps:
       - name: Install the pinned prover
         run: |
           apt-get update
           apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2
-      - uses: actions/checkout@v6.0.3
+      - uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
       - name: Verify the checked Agda version
         run: test "$(agda --version)" = 'Agda version 2.6.4.3'
       - name: Core proofs and expected rejections
-        run: bash scripts/check.sh
+        run: bash scripts/check-agda.sh

.machine_readable/descriptiles/anchors/README.adoc

@@ -10,7 +10,7 @@ anchor file lives in this directory, and no `.a2ml` file may be created here.
 
 - `(anchor)` - Project recalibration, scope intervention, canonical authority
 
-Read a field with `scripts/deed-field.sh rsr-template-repo_chora.deed anchor <key>`.
+Read a field with `scripts/deed-field.sh resource-algebra_chora.deed anchor <key>`.
 
 ## Multiple Versions
 

.machine_readable/root-allow.txt

@@ -32,12 +32,13 @@ LICENSE
 LICENSES/                  # REUSE licence texts, dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0)
 CHANGELOG.adoc             # AsciiDoc is the estate-standard documentation format
 CITATION.cff               # citation metadata; GitHub reads it from the root of the default branch only
-rsr-template-repo_chora.deed # the repo deed: universal AI entry point; family-7 allocation manifest + ply tree folded in (standards#837 pilot). Filename carries the repo slug (deed dispatch <stem>_chora.deed), so repo-init renames it at mint
+resource-algebra_chora.deed # repository deed; Canon lockstep reads <repo>_chora.deed at the PR head
 CLAUDE.md                  # generated arrival pack; the generator, pre-commit and Claude Code all read it from the ROOT (do not hand-edit; edit the repo deed)
 ?GEMINI.md                # pointer to CLAUDE.md for repos without AGENTS.md yet
 Justfile                   # thin; delegates phases to build/just/*.just
 launcher.sh                # --setup/--doctor/--heal/--ai-setup (launcher-standard 0.6.0); the one file a newcomer runs first
 coordination.k9.ncl        # repo-local session binding (template-mandated)
+resource-algebra.agda-lib  # Agda library manifest; Agda discovers it at the library root and resolves src/ relative to it
 
 # ─── Conventional dotfiles (tool-required at root) ───────────────────────────
 .editorconfig

CHANGELOG.adoc

@@ -1,6 +1,29 @@
 == Changelog
 
 
+== 2026-10-14 — MinMax and morphisms (resource-algebra#3)
+
+* `Instances/MinMax.agda`: the min-max (bottleneck) instance on the Loss
+  carrier, with dioid, ordered and annihilating layers.
+* `Morphism.agda`: strict (`Hom`) and lax (`LaxHom`) morphisms with
+  identities and composition; `peak-lax` (HWM → MaxPlus); no strict
+  morphism out of HWM; exactly two strict morphisms Loss → MaxPlus and
+  exactly one MaxPlus → Loss; `loss-bottleneck` (Loss → MinMax, lax).
+* `Separation.agda`: S-4 (a bottleneck is not a sum).
+* Five more expected rejections: `MinMaxIsLoss`, `PeakIsStrict`,
+  `BottleneckBoundReversed`, `MinMaxInfinityIsIdentity`, `PeakPreservesZero`;
+  unit tests in `tests/unit/`.
+* `scripts/check-agda.sh` now requires each rejection to carry the message
+  its `-- EXPECT:` line names (a refusal for another reason fails), and
+  typechecks the unit tests.
+* The proof ledger moved to `docs/status/PROOF-STATUS.adoc`, the template's
+  home for it, replacing the unfilled template stub there (`just` read the
+  stub first). The root allowlist keeps only `resource-algebra.agda-lib`.
+* Fixed: `proofs.yml` called a non-existent `scripts/check.sh`, so CI had
+  never checked the proofs; it now runs `scripts/check-agda.sh`. The
+  workflow had no `actions.lock` key and an unlocked checkout ref (Lock Sync
+  Gate); it now uses the locked `actions/checkout@v7.0.1`.
+
 == 2026-10-12 — initial development
 
 * `ResourceAlgebra` record with `IsOrdered`, `IsDioid` (⇒ ordered) and

CITATION.cff

@@ -1,4 +1,5 @@
 cff-version: 1.2.0
+message: "If you use this software, please cite it using the metadata in this file."
 title: "resource-algebra: the parametric grade algebra of the hyperpolymath type family"
 type: software
 authors:

CLAUDE.md

@@ -6,7 +6,7 @@ SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 <!-- The region between the ARRIVAL-PACK markers is generated from this
      repo's deed by `just claude-md` — do not hand-edit it. -->
 
-<!-- ARRIVAL-PACK:BEGIN — estate-common @Manifesto:DRAFT-unratified · repo @deed:DEED@ab944221ee82 ANCHOR@51194a4e21e8 — generated by `just claude-md`, do not hand-edit -->
+<!-- ARRIVAL-PACK:BEGIN — estate-common @Manifesto:DRAFT-unratified · repo @deed:DEED@62a71111a313 ANCHOR@6f1c91b4155e — generated by `just claude-md`, do not hand-edit -->
 
 # You are in the hyperpolymath estate — orient before acting
 
@@ -38,7 +38,7 @@ The descriptive family (working name *descriptiles*) describes what-is; the **co
 
 | File | Answers |
 |---|---|
-| `rsr-template-repo_chora.deed` | **CHORA**, the repo deed. Its `(identity)` `(clade)` `(lineage)` clauses say what this repo IS (registers into `gv-clade-index`); `(meta)` the architecture axes; `(agentic)` *may I act now?*; `(ecosystem)` where it sits and what it is not; `(status)` and `(maturity)` where it is now. Read fields with `scripts/deed-field.sh`. |
+| `resource-algebra_chora.deed` | **CHORA**, the repo deed. Its `(identity)` `(clade)` `(lineage)` clauses say what this repo IS (registers into `gv-clade-index`); `(meta)` the architecture axes; `(agentic)` *may I act now?*; `(ecosystem)` where it sits and what it is not; `(status)` and `(maturity)` where it is now. Read fields with `scripts/deed-field.sh`. |
 | `(anchor)` | *Semantic authority + golden path* — what downstream may extend-not-redefine; if a recognised-drift / re-anchor marker is present, it **supersedes** accumulated context — read it first. |
 | `(neurosym)` | *Meaning* of operations — proof obligations. |
 | `(playbook)` | *How* permitted actions run. |
@@ -57,17 +57,17 @@ Use plain JavaScript when this tooling is needed. TypeScript and ReScript migrat
 
 ---
 
-# This repo: `rsr-template-repo`  ·  clade `rm-rsr-template-repo`
+# This repo: `resource-algebra`  ·  clade `UNASSIGNED-resource-algebra`
 
-- **Identity** — uuid `a5ea1382-a34c-5334-8a46-a2ebe904c810`; clade `rm` (secondary ``); born 2026-03-16; forge `hyperpolymath/rsr-template-repo`.
-- **IS** — Canonical RSR-compliant repository template: scaffolding (CI/CD, AI manifests, ABI/FFI standards, container ecosystem, governance) that new hyperpolymath projects are instantiated from.
-- **IS-NOT** — a project in its own right · Scaffoldia (the full-featured repo designer) · standards (the canon source this template operationalises)
-- **Where it sits** — pipeline position **foundation**; chain `standards → rsr-template-repo → (every estate repo)`; coordination = `standards`.
+- **Identity** — uuid `241f1c29-0838-5033-b654-7f4c5e279ebc`; clade `UNASSIGNED` (secondary ``); born 2026-10-12; forge `hyperpolymath/resource-algebra`.
+- **IS** — Parametric resource algebra in Agda, with Loss, MaxPlus, HWM and MinMax instances and strict/lax morphisms.
+- **IS-NOT** — a repository template · the K-CUT statement, which belongs in choreographic-types · occupancy-types' own algebra, for which HWM is a proposal
+- **Where it sits** — pipeline position **kernel**; chain `resource-algebra → hyperpolymath type family`; coordination = ``.
 - **Constraints here** (AGENTIC) — fail-closed; evidence-per-step; no-silent-skip; rerun-after-fix; release-claim-requires-hard-pass. Never: banned langs (above), secrets, state files in repo root, AGPL. Details: the deed's `(bot-directives (methodology) (coverage) (debt))` clauses.
 - **Golden path** (ANCHOR) — `just test && just quality` → Core tests pass; Quality gates pass; No unresolved critical security findings.
-- **State** — phase active; maturity production. Milestones and next actions: `docs/status/ROADMAP.adoc`.
+- **State** — phase active; maturity experimental. Milestones and next actions: `docs/status/ROADMAP.adoc`.
 
-<!-- ARRIVAL-PACK:END · provenance: DEED@ab944221ee82 ANCHOR@51194a4e21e8 · Manifesto@DRAFT-unratified · regenerate: `just claude-md` (k9 drift-detects; do not hand-edit above) -->
+<!-- ARRIVAL-PACK:END · provenance: DEED@62a71111a313 ANCHOR@6f1c91b4155e · Manifesto@DRAFT-unratified · regenerate: `just claude-md` (k9 drift-detects; do not hand-edit above) -->
 
 <!-- Hand-authored (owner, 2026-10-05): kept below the generated region so `just claude-md` does not overwrite it. -->
 ## Estate-Wide Format Migration Directives

README.adoc

@@ -4,10 +4,6 @@
 = resource-algebra — the parametric grade algebra shared by the type family
 :toc: left
 
-// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
-= Resource Algebra — the parametric grade algebra shared by the type family
-:toc: left
-
 == Overview
 
 One Agda record, `ResourceAlgebra`, states what a grade algebra is for the
@@ -17,21 +13,29 @@ monoid `(⊕, 𝟘)`, sequence forms a monoid `(⊗, 𝟙)`. Optional layers add
 (`IsDioid`, which yields `IsOrdered` by a proof, not a second obligation),
 and an annihilating zero (`IsAnnihilating`).
 
-Three instances are checked against it:
+Four instances are checked against it:
 
 [cols="1,2,2,1",options="header"]
 |===
 | Instance | Source of the definition | Alternatives / sequence | Status
 | `Instances.Loss` | echo-types `experimental/echo-additive/Grade.agda`, transcribed | min / + on ℕ ∪ {∞} | transcribed, PROVEN
 | `Instances.MaxPlus` | tropical-types `TropicalSessionTypes.lean`, transcribed | max / + on ℕ ∪ {−∞} | transcribed, PROVEN; Lean bridge OPEN
 | `Instances.HWM` | occupancy-types operational model, *proposed* (its R2–R3 algebra is not yet defined) | componentwise max / peak-and-drift | DESIGNED, PROVEN against this definition
+| `Instances.MinMax` | typed-wasm L11 bottleneck (`Tropical.tropMax`), which defined it locally | min / max on ℕ ∪ {∞} | PROVEN; typed-wasm adoption DESIGNED
 |===
 
 This repository is a kernel module of the family, not a family of its own.
 It exists so that K-CUT-LOSS (choreographic-types) can be stated once,
 parametrically, and discharged three times, instead of being proved against
 a single concrete algebra that bakes in one repo's vocabulary.
 
+`Morphism.agda` defines strict (`Hom`) and lax (`LaxHom`) maps between
+instances and says which exist: `peak` is lax HWM → MaxPlus and nothing
+strict leaves HWM; Loss → MaxPlus has exactly two strict maps and
+MaxPlus → Loss exactly one, and none of them separates two positive
+grades; the identity is lax Loss → MinMax. Transport of K-CUT-LOSS along these maps is
+not proved here (link:docs/status/PROOF-STATUS.adoc[], Open).
+
 == What is standard and what is ours
 
 *Standard:* idempotent semirings (dioids), the max-plus and min-plus
@@ -41,16 +45,16 @@ multiplication for the natural order.
 *Ours:* the layering (what K-CUT-LOSS needs versus what K-CUT-WARRANT
 needs), the three estate instances held against one record, the
 high-water-mark proposal, and the checked separation witnesses
-(`Separation.agda`) that turn three boundary sentences of the family map into
+(`Separation.agda`) that turn four boundary sentences into
 `refl`-plus-inequality facts: an occupancy bound is not a cost bound; echo
 alternatives are min while tropical alternatives are max; the induced order
-runs opposite ways in the two.
+runs opposite ways in the two; a bottleneck bound is not a loss bound.
 
 == What this is not
 
 * Not an import of echo-types or tropical-types. The instances are
   transcriptions; the correspondence is a review obligation recorded in
-  link:PROOF-STATUS.adoc[].
+  link:docs/status/PROOF-STATUS.adoc[].
 * Not the K-CUT statement. Global/local types, projection and cuts live in
   choreographic-types; this repository supplies the algebra they are
   parametric in.
@@ -61,29 +65,33 @@ runs opposite ways in the two.
 
 [source,bash]
 ----
-just check        # core proofs under --safe --without-K --double-check,
-                  # then every tests/reject/*.agda must be refused at its
-                  # invalid declaration
+just check-agda  # core proofs and unit tests under --safe --without-K
+                  # --double-check, then every tests/reject/*.agda must be
+                  # refused at its invalid declaration with the message
+                  # its `-- EXPECT:` line names
 ----
 
-Builtins only (`--no-libraries`): the development checks under the Debian
-`agda-bin` package the estate CI pins and under Ubuntu's 2.6.3.
+Builtins only (`--no-libraries`). It checks locally under Agda 2.6.3. CI
+(`proofs.yml`) pins the Debian `agda-bin` 2.6.4.3 package; until 2026-10-14
+that workflow called a script that does not exist, so a CI check is evidence
+only from its first green run.
 
 == Repository layout
 
 ----
 src/ResourceAlgebra/Prelude.agda      ℕ lemmas (+, max, min, ≤), proved here
 src/ResourceAlgebra/Core.agda         the record and its layers
-src/ResourceAlgebra/Instances/*.agda  Loss, MaxPlus, HWM
+src/ResourceAlgebra/Instances/*.agda  Loss, MaxPlus, HWM, MinMax
 src/ResourceAlgebra/Separation.agda   checked separation witnesses
+src/ResourceAlgebra/Morphism.agda     strict and lax morphisms, classifications
 tests/reject/*.agda                   expected rejections (must fail)
 docs/pre-registration.adoc            intent, provenance ledger, obligations
-PROOF-STATUS.adoc                     every claim with its status and artefact
+docs/status/PROOF-STATUS.adoc         every claim with its status and artefact
 ----
 
 == Documentation
 
-* link:PROOF-STATUS.adoc[Proof status]
+* link:docs/status/PROOF-STATUS.adoc[Proof status]
 * link:docs/pre-registration.adoc[Pre-registration and obligations]
 * Family map: `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`
 
@@ -209,7 +217,7 @@ maintainers can brief an AI with `just ai-warmup dev` / `just ai-warmup maintain
 * *Machine-readable metadata* (`.machine_readable/descriptiles/`) — `STATE`, `META`,
   `ECOSYSTEM`, `PLAYBOOK`, `AGENTIC`, `NEUROSYM`, `CLADE`, and `anchors/ANCHOR`,
   in deed, so tools and agents can read the project's state and boundaries.
-* *AI gatekeeper protocol* — `rsr-template-repo_chora.deed` (the repo deed) is the
+* *AI gatekeeper protocol* — `resource-algebra_chora.deed` (the repo deed) is the
   universal entry point that tells an AI agent how to work in this repo before it
   touches anything; it carries the AI allocation policy and the ply directory tree.
 * *Typed ABI/FFI seam* — `src/interface/Abi/` (Idris2 type + layout proofs) over

docs/MAINTAINERS.adoc

@@ -12,9 +12,9 @@ earlier duplicates at `.github/MAINTAINERS` and `docs/attribution/MAINTAINERS.ad
 |===
 | Name | Role | Contact
 
-| {{AUTHOR}}
+| Jonathan D.A. Jewell
 | Lead Maintainer
-| https://github.com/{{OWNER}}[@{{OWNER}}]
+| https://github.com/hyperpolymath[@hyperpolymath]
 |===
 
 == Responsibilities