diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index de76b0e..cc6e307 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -3,6 +3,7 @@
 # Docs: https://gh.io/actions-lockfile
 version: 'v0.0.2'
 workflows:
+    '.github/workflows/documentation-integrity.yml': []
     '.github/workflows/label-triage.yml': []
     '.github/workflows/labels.yml': []
     '.github/workflows/push-email-notify.yml':
diff --git a/.github/workflows/documentation-integrity.yml b/.github/workflows/documentation-integrity.yml
new file mode 100644
index 0000000..9ff86c2
--- /dev/null
+++ b/.github/workflows/documentation-integrity.yml
@@ -0,0 +1,33 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Documentation Integrity
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: documentation-${{ github.ref }}
+  cancel-in-progress: true
+jobs:
+  documentation:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 5
+    steps:
+      # No marketplace actions: this guard must not depend on the allow-list
+      # it helps document. Fetch the event SHA, never an untrusted branch name.
+      - name: Fetch event revision
+        env:
+          GH_TOKEN: ${{ github.token }}
+          REPOSITORY: ${{ github.repository }}
+          REVISION: ${{ github.sha }}
+        run: |
+          set -euo pipefail
+          gh api "repos/$REPOSITORY/tarball/$REVISION" > "$RUNNER_TEMP/source.tar.gz"
+          tar -xzf "$RUNNER_TEMP/source.tar.gz" --strip-components=1
+      - name: Check documentation and regression tests
+        run: |
+          set -euo pipefail
+          node --version
+          node scripts/check-repository.mjs
+          node --test tests/*.test.mjs
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
deleted file mode 100644
index 88cf4c2..0000000
--- a/.machine_readable/6a2/STATE.a2ml
+++ /dev/null
@@ -1,166 +0,0 @@
-# SPDX-License-Identifier: MPL-2.0
-# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-#
-# STATE.a2ml — choreographic-types project state (PRE-REGISTRATION)
-#
-# Format: TOML-A2ML (estate convention). Sibling of echo-types' STATE.a2ml.
-# PURPOSE: pre-registration written BEFORE any Agda and BEFORE git init, to pin the single
-# load-bearing claim (K-CUT) and the borrowed-vs-new ledger up front so the contribution
-# claim is survivable from the first commit. Nothing here is PROVEN in this repo yet; the
-# only PROVEN entries are imported base cases verified in their home repos this session.
-# Provenance CORRECTED 2026-06-16 vs the original "cut-calculus" working-title draft.
-
-[metadata]
-project        = "choreographic-types"   # was working-title "cut-calculus"
-repository     = "https://github.com/hyperpolymath/choreographic-types"  # NOT YET CREATED
-canonical-host = "github"
-mirrors        = ["gitlab", "codeberg"]
-version-target = "0.0.0"
-license        = "OWNER-TO-SET"          # MPL-2.0 expected (owner-sole); owner establishes manually
-created-at     = "2026-06-16"
-last-updated   = "2026-06-16"
-status         = "pre-registration (repo not yet created)"
-phase          = "space-setting: keystone + corrected provenance ledger before any code"
-family         = ["echo-types", "epistemic-types", "tropical-types", "choreographic-types"]
-
-[context-notes]
-note = """
-A choreographic fusion of echo grades (structural loss, the ℕ∪{∞} tropical semiring) and
-epistemic transport (standpoint warrant) over a global type G read as a partial causal
-order. The choreography is the clock; cuts (consistent frontiers / antichains) are the
-time points; the branch tree is the modality (∇ contingent vs △ non-contingent loss);
-ordinal rank of a cut is the temporal index. The whole reason to exist is one theorem
-(see [keystone]). It DEPENDS ON, and does not re-prove, machinery in echo-types,
-epistemic-types and tropical-types. NOT invented mathematics: it stands on multiparty
-session types (Honda-Yoshida-Carbone), choreographic programming (Montesi; Hirsch-Garg),
-timed session types (Bocchi-Yoshida) and secure/IFC session types; the ASSEMBLY + K-CUT
-are the contribution. See docs / dev-notes what-choreographic-is.
-"""
-
-[keystone]
-id       = "K-CUT"
-name     = "grading-and-transport / projection cut-coherence"
-status   = "OPEN"
-informal = """
-Projecting G onto party p and reading p's local (loss, warrant) timeline up to a cut c
-agrees with the global accumulation of (loss, warrant) over G up to c, restricted to p.
-Slogan: grading and transport commute with projection across a cut.
-"""
-
-[keystone.loss-component]
-id     = "K-CUT-LOSS"
-status = "OPEN"   # target: EQUALITY (loss is type-determined)
-
-[keystone.warrant-component]
-id             = "K-CUT-WARRANT"
-status         = "OPEN"   # target: BOUND under SoundWarrant (type upper-bounds, cannot determine)
-side-condition = "SoundWarrant at the receiver (ASSUMED local soundness, not type-determined)"
-
-# ---- Provenance ledger (CORRECTED 2026-06-16) ----
-
-[[imported-proven]]
-id        = "imp-001"
-name      = "choreo-grade-commute"
-home      = "echo-types : proofs/agda/characteristic/RoleGraded.agda:193"
-status    = "PROVEN (--safe --without-K, postulate-free; verified 2026-06-16; 18 cases / 1 non-trivial)"
-role-here = "Degenerate STATIC base case of K-CUT (single edge, no time). Import; do NOT restate as open."
-
-[[imported-proven]]
-id        = "imp-002"
-name      = "echo grade dioid ℕ∪{∞} under (min,+)"
-home      = "echo-types : proofs/agda/experimental/echo-additive/Grade.agda"
-status    = "PROVEN-but-UNWIRED (compiles --safe standalone; absent from All.agda; gated R-2026-05-18)"
-role-here = "Loss algebra. A consumer MUST wire/vendor it; it does NOT travel with echo-types' green closure."
-
-[[depends-on-sibling]]
-id     = "dep-001a"
-name   = "epistemic standpoint-warrant (PROOF HOME)"
-home   = "epistemic-types : src/EpistemicTypes/{Warrant,ProofTransport}.agda"
-status = "PROOF DEPENDENCY (Agda --safe). Non-factive Warrant + SoundWarrant; transmit / proofNeedsChecker."
-note   = "K-CUT-WARRANT's determine-vs-bound gap lives HERE. CORRECTION: the original draft misattributed this to proven-epistemic."
-
-[[depends-on-sibling]]
-id     = "dep-001b"
-name   = "proven-epistemic disclosure server (RUNTIME WITNESS only)"
-home   = "proven-servers : protocols/proven-epistemic (Idris2)"
-status = "RUNTIME WITNESS, NOT a proof source. decideDisclosable is a TOTAL Dec (it determines — opposite posture). Flawed / redesign pending."
-note   = "Cite only as the enforcement-gap instance at the BEAM/JS boundary. Never load-bearing."
-
-[[depends-on-sibling]]
-id     = "dep-002"
-name   = "tropical resource-dioid"
-home   = "tropical-types (tropical-resource-typing) : Resource.* (Lean 4)"
-status = "DEPEND-ON-SIBLING via in-site PORT (no Agda<->Lean import path). Re-axiomatise ResourceAlgebra in Agda; cite the Lean proof as warrant of inhabitation."
-note   = "Dioid fork RESOLVED-BY-PARAMETRICITY upstream: MaxPlus/MinPlus/MinMax are instances of one ResourceAlgebra; parametric_resource_transport proven on no axioms."
-
-[[standing-decisions]]
-id     = "sd-001"
-title  = "Dioid fork — RESOLVED by parametricity (NOT an open ratification)"
-status = "resolved"
-note   = "Write K-CUT-LOSS against [ResourceAlgebra R]; holds at min-plus / max-plus / min-max at once. The real residual is the cross-prover bridge (in-site port), not the carrier."
-
-[[standing-decisions]]
-id     = "sd-002"
-title  = "Standalone repo, registered in nextgen-typing (an edge, NOT a subdir)"
-status = "accepted"
-
-[[standing-decisions]]
-id     = "sd-003"
-title  = "GitHub canonical, hub-and-spoke mirror; name = choreographic-types (in the -types family)"
-status = "accepted"
-
-[[claims]]
-id = "c-cut-coherence"
-status = "OPEN"
-text = "K-CUT + its loss/warrant split. The single falsifier."
-
-[[claims]]
-id = "c-soundwarrant"
-status = "ASSUMED"
-text = "Receiver-local checker soundness; K-CUT-WARRANT is conditional on it. Never to be claimed PROVEN here."
-
-[cross-prover]
-note = """
-echo + epistemic = Agda (same kernel — genuine imports). tropical = Lean 4 (NO import path).
-Host choreographic-types in Agda; import echo+epistemic; re-prove the dioid in-site with an
-explicit NAMED prover-bridge obligation citing tropical-types' Lean proof. Never call it 'import'.
-Precedent: typed-wasm/src/abi/TypedWasm/ABI/Tropical.idr ports tropical-types in Idris.
-"""
-
-[[next-actions]]
-id = "na-001"
-title = "git init + owner sets LICENSE/SPDX + gh repo create + signed (-S) push"
-status = "open"
-priority = "high"
-
-[[next-actions]]
-id = "na-002"
-title = "Register in nextgen-typing (5-surface change set, like tropical-types)"
-status = "open"
-priority = "medium"
-
-[[next-actions]]
-id = "na-003"
-title = "State K-CUT-LOSS as the first Agda signature, against [ResourceAlgebra R]"
-status = "open"
-priority = "high"
-
-# ---- Application proof targets (added after pre-registration) ----
-
-[[application-targets]]
-id = "app-rapidnj-002"
-name = "two-thread RapidNJ K-CUT-LOSS square"
-status = "OPEN TARGET (not a proof; application note only)"
-frontier = "two selected events e1/e2 with Independent₂ witness"
-minimum-lemma = "localGrade p (localStep p e2 (localStep p e1 (project p s))) ≡ transportLoss p (globalGrade (step e2 (step e1 s)))"
-prerequisite = "canonical state diamond for disjoint read/write footprints"
-non-claim = "Does not assert upstream RapidNJ exposes this batch interface; does not address K-CUT-WARRANT"
-
-[[application-targets]]
-id = "app-rapidnj-001"
-name = "two-thread RapidNJ canonical state diamond"
-status = "OPEN TARGET (algorithmic prerequisite, not K-CUT)"
-statement = "step e2 (step e1 s) ~= step e1 (step e2 s) under Independent₂"
-
-[blockers]
-note = "K-CUT cannot be typed until the repo is git-init'd + licensed by the owner. Everything below na-001 waits on that."
diff --git a/EXPLAINME-new.adoc b/EXPLAINME-new.adoc
index 764fb4c..6b33e52 100644
--- a/EXPLAINME-new.adoc
+++ b/EXPLAINME-new.adoc
@@ -17,7 +17,7 @@ A global choreographic type G is read as a partial causal order. It is projected
 ____
 
 How this is intended to be implemented::
-The planned `link:src/ChoreographicTypes/[]` tree will define `GlobalType`, the
+The planned canonical source tree will define `GlobalType`, the
 partial causal order structure, the grading by `EchoGrade` (imported from
 `echo-types`) and `EpiGrade` (imported from `epistemic-types`), and the
 `EndpointProjection` mapping.
@@ -67,17 +67,19 @@ How this is implemented::
 `link:applications/rapidnj-two-thread.adoc[]` defines the application boundary and records the target in `link:applications/rapidnj-two-thread.agda[]`. The target names global and local reduction steps, projection, loss grading, transport, and an `Independent₂` witness. `Independent₂` is deliberately stronger than antichain membership: it must cover read/write disjointness, phase safety, and deterministic tie handling.
 
 Caveat::
-The accompanying Agda file contains open interfaces and postulated target signatures so that the proof obligation has a stable shape. It is not imported into the build and proves nothing. The RapidNJ state diamond (serialising two independent updates in either order) is an algorithmic prerequisite, separate from K-CUT-LOSS. No claim is made about the upstream implementation exposing this exact batch interface.
+The accompanying Agda file contains open interfaces and postulated target signatures so that the proof obligation has a stable shape. There is no canonical Agda build, and it proves nothing. The RapidNJ state diamond (serialising two independent updates in either order) is an algorithmic prerequisite, separate from K-CUT-LOSS. No claim is made about the upstream implementation exposing this exact batch interface.
 
-=== The tropical resource-dioid is re-proved in-site
+=== The tropical resource-dioid is planned to be re-proved in-site
 
 [quote, README.adoc]
 ____
-The tropical resource-dioid is re-proved in-site rather than imported across kernels. This follows the estate's port-and-reprove pattern.
+The tropical resource-dioid is planned to be re-proved in-site rather than imported across kernels. This follows the estate's port-and-reprove pattern.
 ____
 
 How this is implemented::
-The dioid structure and laws are proved directly in `link:src/ChoreographicTypes/ResourceDioid.agda[]` (or equivalent), without importing `tropical-resource-typing` (which is Lean 4, making a direct import impossible anyway; the port-and-reprove pattern ensures logical consistency across language boundaries).
+No local dioid implementation or proof exists. The plan is to re-prove its
+laws in Agda, with an explicit bridge obligation to the Lean 4 definitions.
+A port does not automatically establish cross-kernel consistency.
 
 Caveat::
 This is a duplication by design. It must be kept in sync manually if the Lean 4 definition changes. The precedent is `typed-wasm/…/Tropical.idr`.
@@ -86,7 +88,7 @@ This is a duplication by design. It must be kept in sync manually if the Lean 4
 
 [cols="1,2,2", options="header"]
 |===
-| Technology / Pattern | Used here | Also used in
+| Technology / Pattern | Planned use here | Also used in
 
 | Echo loss-grades
 | Global type grading
@@ -120,7 +122,7 @@ This is a duplication by design. It must be kept in sync manually if the Lean 4
 
 [CAUTION]
 ====
-**The RapidNJ target is not a proof.** `applications/rapidnj-two-thread.agda` is a standalone typed target with open interfaces and postulates. It is not imported into `All.agda`; the two-thread state diamond, projection square, and K-CUT-LOSS equality remain to be proved.
+**The RapidNJ target is not a proof.** `applications/rapidnj-two-thread.agda` is an illustrative target with open interfaces and postulates. There is no canonical Agda build; the two-thread state diamond, projection square, and K-CUT-LOSS equality remain to be proved.
 ====
 
 [CAUTION]
@@ -132,9 +134,9 @@ This is a duplication by design. It must be kept in sync manually if the Lean 4
 
 [cols="2,3", options="header"]
 |===
-| Path | Proves
+| Path | Evidence or intent
 
-| `src/ChoreographicTypes/`
+| Canonical source tree (not yet implemented)
 | Planned definitions of global types, projection, grades, cuts, K-CUT statements
 
 | `applications/rapidnj-two-thread.adoc`
@@ -149,6 +151,6 @@ This is a duplication by design. It must be kept in sync manually if the Lean 4
 | `ChoreoInjective` (sibling)
 | Degenerate single-static-edge base case
 
-| `.machine_readable/6a2/STATE.a2ml`
+| link:docs/pre-registration.adoc[Pre-registration record]
 | Pre-registration state and provenance ledger
 |===
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
index 8e5c545..d3cba3c 100644
--- a/EXPLAINME.adoc
+++ b/EXPLAINME.adoc
@@ -5,7 +5,13 @@
 :icons: font
 :doctype: article
 
-This file backs every factual claim in link:README.adoc[README.adoc] with code paths and honest caveats. Read it if you are doing due diligence on whether the story matches the code.
+[WARNING]
+====
+Historical, misplaced tropical-resource-typing document. It does NOT describe
+this repository, its files, its build or its proven results. Its claims below
+are retained only as historical context and have not been verified here.
+For current status use link:EXPLAINME-new.adoc[the choreographic claim map].
+====
 
 == Claim-to-implementation map
 
@@ -17,7 +23,7 @@ The max-plus semiring (⊕ = max, ⊗ = +) grading speculative session types: so
 ____
 
 How this is implemented::
-`link:TropicalSessionTypes.lean[]` defines the max-plus semiring on grades, the grading of session types, and proves soundness and `tropical_grade_le_sequentialTotal`. Depends only on `Init`. No `sorry`, no `Classical.choice`.
+`TropicalSessionTypes.lean (historical external path)` defines the max-plus semiring on grades, the grading of session types, and proves soundness and `tropical_grade_le_sequentialTotal`. Depends only on `Init`. No `sorry`, no `Classical.choice`.
 
 Caveat::
 The max-plus semiring is standard mathematics. The contribution is the *application* to speculative session types and the mechanised QTT refinement. Soundness holds under the assumption that dynamic cost matches the static grade structure — this is the standard assumption for any resource-aware type system.
@@ -30,7 +36,7 @@ The min-max / bottleneck semiring (⊕ = min, ⊗ = max) grading adapter paths.
 ____
 
 How this is implemented::
-`link:TropicalAdapterPath.lean[]` defines the min-max semiring, the grading of adapter paths, and proves `hub_ceiling`. Depends only on `Init`. No `sorry`, no `Classical.choice`. The provenance of the refuted claim is the frozen archive in `protocol-squisher` (left unchanged there).
+`TropicalAdapterPath.lean (historical external path)` defines the min-max semiring, the grading of adapter paths, and proves `hub_ceiling`. Depends only on `Init`. No `sorry`, no `Classical.choice`. The provenance of the refuted claim is the frozen archive in `protocol-squisher` (left unchanged there).
 
 Caveat::
 This is the strongest result in the repo. Proving a no-go theorem (an interoperability bound) is rigorous, defensive work that closes a specific overclaim. No known gap.
@@ -56,7 +62,7 @@ ResourceSemiring (ops + semiring laws) and the ordered ResourceAlgebra (preorder
 ____
 
 How this is implemented::
-`link:Resource/Algebra/[]` defines the interfaces and proves `parametric_resource_transport` (aliased as `resource_laws_sufficient_for_consumers`). The theorem states that satisfying the `ConsumerLawBundle` is sufficient to transport resource laws from the abstract algebra to a concrete consumer.
+`Resource/Algebra/ (historical external path)` defines the interfaces and proves `parametric_resource_transport` (aliased as `resource_laws_sufficient_for_consumers`). The theorem states that satisfying the `ConsumerLawBundle` is sufficient to transport resource laws from the abstract algebra to a concrete consumer.
 
 Caveat::
 The parametricity is over the `ConsumerLawBundle` record, not over an arbitrary universe. Downstream languages must instantiate this record. This is a design choice bounding the abstraction level.
@@ -69,7 +75,7 @@ Concrete instances all satisfying the one interface: Linear and Affine ({0,1,ω}
 ____
 
 How this is implemented::
-`link:Resource/Instances/[]` provides the five instances. Each proves the `ResourceAlgebra` laws. `Linear` and `Affine` share the same carrier `{0, 1, ω}` but differ in their preorder, demonstrating that the interface captures order-theoretic distinctions.
+`Resource/Instances/ (historical external path)` provides the five instances. Each proves the `ResourceAlgebra` laws. `Linear` and `Affine` share the same carrier `{0, 1, ω}` but differ in their preorder, demonstrating that the interface captures order-theoretic distinctions.
 
 Caveat::
 None currently known. The instances are small and mechanically verified.
@@ -82,7 +88,7 @@ Proves the tropical carriers are infinite — the stress test that the abstracti
 ____
 
 How this is implemented::
-`link:Resource/Stress.lean[]` proves that the `MaxPlus` and `MinPlus` carriers are infinite, distinguishing them from the finite `{0, 1, ω}` instances.
+`Resource/Stress.lean (historical external path)` proves that the `MaxPlus` and `MinPlus` carriers are infinite, distinguishing them from the finite `{0, 1, ω}` instances.
 
 Caveat::
 This is a separation proof in the same spirit as echo-types' matched-negatives: it proves the tropical abstraction is not a trivial finite reification. No known gap.
@@ -95,7 +101,7 @@ A resource algebra may measure Echo residues (direction E → R); Echo is not a
 ____
 
 How this is implemented::
-`link:Resource/EchoBridge.lean[]` defines the measurement direction (E → R) and proves that Echo is not a resource instance. The bridge does not import the `echo-types` Agda library; it establishes the vocabulary boundary in Lean.
+`Resource/EchoBridge.lean (historical external path)` defines the measurement direction (E → R) and proves that Echo is not a resource instance. The bridge does not import the `echo-types` Agda library; it establishes the vocabulary boundary in Lean.
 
 Caveat::
 This matches the `Echo.Separation.NotResourceInstance` result in `echo-types` but is proved independently in Lean without importing Agda artifacts. The two results should be consistent; cross-checking is a manual obligation.
@@ -108,7 +114,7 @@ Every headline theorem depends only on propext (+ Quot.sound) — no sorry, no C
 ____
 
 How this is implemented::
-`lake build` is green. `lean-toolchain` pins Lean 4.13.0. Imports are only `Init`. Grep for `sorry` and `Classical.choice` returns no hits in proof terms. Full provenance in `link:docs/LEAN-FORMALIZATION.adoc[]`.
+`lake build` is green. `lean-toolchain` pins Lean 4.13.0. Imports are only `Init`. Grep for `sorry` and `Classical.choice` returns no hits in proof terms. Full provenance in `docs/LEAN-FORMALIZATION.adoc (historical external path)`.
 
 Caveat::
 The dependence on `propext` and `Quot.sound` is the standard foundational commitment for Lean 4 mathematics using quotients. This is not constructively neutral; a user working in a strict cubical setting would need to re-derive these results.
diff --git a/README.adoc b/README.adoc
index 4d5b813..5ed54c8 100644
--- a/README.adoc
+++ b/README.adoc
@@ -5,10 +5,9 @@
 :icons: font
 :doctype: article
 
-image:https://img.shields.io/badge/OpenSSF-BestPractices-green[link="https://www.bestpractices.dev/projects/XXXX"]
-
-Agda formalisation target for a graded multiparty-session and choreographic
-type theory, combining echo loss-grades and epistemic standpoint-warrants.
+A pre-registration and research notebook for a graded multiparty-session and
+choreographic type theory, combining echo loss-grades and epistemic
+standpoint-warrants. Agda is the intended prover, not a completed formalisation.
 The central artefact is the open keystone K-CUT: the conjecture that grading
 and transport commute with projection across a consistent frontier.
 
@@ -112,21 +111,21 @@ deferred.
 
 == Dependencies and the port-and-reprove pattern
 
-The intended repository imports from the estate's Agda kernel:
+The planned formalisation will import from the estate's Agda kernel:
 
 * `echo-types` — the `ℕ ∪ {∞}` loss-dioid and the `choreo-grade-commute`
   base case.
 * `epistemic-types` — the non-factive `Warrant` / `SoundWarrant` interface
   (the proof home for the warrant gap in K-CUT-WARRANT).
 
-The tropical resource-dioid is **re-proved in-site** rather than imported
+The tropical resource-dioid is planned to be **re-proved in-site** rather than imported
 across kernels. This follows the estate's port-and-reprove pattern (precedent:
-`typed-wasm/…/Tropical.idr`), ensuring that the resource-algebra layer can be
-self-contained while maintaining logical consistency with
-`tropical-resource-typing`.
+`typed-wasm/…/Tropical.idr`). The goal is a self-contained resource-algebra
+layer; consistency with `tropical-resource-typing` remains an explicit
+bridge obligation, not an automatic consequence of porting.
 
-The full cited borrowed-vs-ours statement is planned for
-`dev-notes/2026-06-16-choreographic-types-what-it-is.adoc`.
+The research intent, borrowed-vs-ours ledger and outstanding obligations are
+preserved in link:docs/pre-registration.adoc[the pre-registration record].
 
 == What this is not
 
@@ -145,32 +144,39 @@ The full cited borrowed-vs-ours statement is planned for
 |===
 | Path | Purpose
 
-| `src/ChoreographicTypes/`
-| Planned Agda formalisation (definitions, projection, K-CUT statement)
-
 | `applications/`
-| Application notes and explicitly open Agda targets
+| Application notes and explicitly postulated Agda targets (not proofs)
+
+| `docs/pre-registration.adoc`
+| Research state, provenance and outstanding proof obligations
 
-| `dev-notes/`
-| Planned design notes and borrowed-vs-ours statement
+| `docs/actions-policy.adoc`
+| Owner-only Actions policy repair and verification
 
-| `.machine_readable/6a2/STATE.a2ml`
-| Pre-registration state (keystone, provenance, decisions)
+| `scripts/` and `tests/`
+| Documentation integrity and regression checks (not proof checking)
 |===
 
-== Build
+== Validation
 
-The current checkout is a documentation and proof-target scaffold; the
-planned `src/` tree is not present yet. Once it is added, the intended
-standalone build is:
+There is no canonical Agda build in this checkout. The application target is
+an illustrative collection of postulates, not a checked proof or a substitute
+for the planned definitions. Do not treat successful documentation checks as
+mathematical verification.
+
+With Node.js 22 or newer:
 
 [source,bash]
 ----
-agda --no-libraries -i src src/ChoreographicTypes/All.agda
+node scripts/check-repository.mjs
+node --test tests/*.test.mjs
 ----
 
-The application target under `applications/` is intentionally not part of
-that command until its interfaces are connected to the canonical definitions.
+== Planned formalisation
+
+Canonical definitions, endpoint projection, a parametric resource algebra,
+and the K-CUT statements must be developed before a prover build can be
+published. No placeholder source tree is provided to imply otherwise.
 
 == Documentation
 
diff --git a/docs/actions-policy.adoc b/docs/actions-policy.adoc
new file mode 100644
index 0000000..f891402
--- /dev/null
+++ b/docs/actions-policy.adoc
@@ -0,0 +1,103 @@
+// SPDX-License-Identifier: MPL-2.0
+= Actions policy: owner repair and verification
+
+== Boundaries and observations (2026-09-27)
+
+Issue https://github.com/hyperpolymath/choreographic-types/issues/16[#16]
+reported `selected` with an empty third-party allow-list. This is server-side
+configuration: a repository commit cannot repair it. The issue explicitly
+reserves the PUT for the owner. Do not widen policy to `all`, disable scanning,
+or change `verified_allowed` to work around this.
+
+This session's GitHub integration returns HTTP 403 for Actions permissions
+GETs and for updating the repository description. The current policy is
+therefore UNKNOWN, not confirmed empty and not verified repaired. The owner
+must use an appropriately authorised GitHub connection; no credentials belong
+in this repository or in an issue comment.
+
+The repository is now public. Secret Scanner runs 36287047076 and 36286986239
+succeeded; run 35478897141 also now reports success. The historical billing
+refusal in issue #15 is not evidence of a current billing failure. A green
+scanner does not prove that arbitrary third-party actions are admitted.
+
+== Canonical payload, not a remembered pattern count
+
+Prerequisites: Node.js 22+, `gh`, and an owner-authorised GitHub connection.
+Review the current standards policy and its rollout/pruning conditions first.
+Resolve it to one immutable commit so payload preparation and comparison use
+exactly the same revision. These commands only read remote settings:
+
+[source,bash]
+----
+set -euo pipefail
+ref=$(gh api repos/hyperpolymath/standards/commits/HEAD --jq .sha)
+work=$(mktemp -d)
+node scripts/actions-policy.mjs payload "$ref" > "$work/payload.json"
+cat "$work/payload.json"
+node scripts/actions-policy.mjs audit "$ref"
+----
+
+The audit checks both this repository and `echo-types` in the same invocation.
+It requires enabled Actions, the `selected` posture, both boolean flags, and
+exact pattern membership (order-independent), not merely matching counts.
+Access failures are UNKNOWN and exit nonzero. Payload generation rejects an
+empty/malformed list and excludes the canon's descriptive metadata from the
+API request. There is deliberately no automated write mode.
+
+If the audit reports drift, the owner reviews the payload, confirms that the
+live repository is still in `selected` mode, and executes the following
+owner-only repair. Refreshing `echo-types` is a separate owner decision in
+that repository, required for the issue's positive control:
+
+[source,bash]
+----
+# OWNER ONLY; use the same ref and work directory from above.
+gh api -X PUT repos/hyperpolymath/choreographic-types/actions/permissions/selected-actions --input "$work/payload.json"
+gh api -X PUT repos/hyperpolymath/echo-types/actions/permissions/selected-actions --input "$work/payload.json"
+node scripts/actions-policy.mjs audit "$ref"
+----
+
+Record the canonical SHA, payload count and successful read-back for BOTH
+repositories in #16 before closing it. Re-run the read-only audit whenever
+standards changes its policy or before adding a new third-party workflow.
+If the posture is disabled or not `selected`, stop for an owner decision
+rather than silently rewriting the broader permission settings.
+
+== Repository description (issue #15)
+
+The local documentation now describes the pre-registration honestly. The
+remote description still needs the following owner-authorised update:
+
+[source,bash]
+----
+gh repo edit hyperpolymath/choreographic-types --description 'Pre-registration and research notes for a graded multiparty-session theory combining echo loss-grades and epistemic warrants. K-CUT remains an open conjecture; application targets are not proofs.'
+gh repo view hyperpolymath/choreographic-types --json description
+----
+
+Do not restore an unqualified “Agda formalisation” description until a checked
+canonical module exists. Postulated application targets are not sufficient.
+
+== What automated validation means
+
+`Documentation Integrity` runs local link/status checks and their regression
+tests on pushes and pull requests. It uses no marketplace actions and requires
+only read access to repository contents. It does not type-check Agda, prove
+K-CUT, or inspect server-side policy. The allow-list audit remains an explicit
+owner-side check because ordinary Actions tokens cannot read admin settings.
+
+== Validation evidence for this repair
+
+* Canon fetched at `2479cf769ed5f0481ccf64860a2ab954514c2b59`:
+  payload preparation succeeded with 93 patterns. This is an observation,
+  not a count hard-coded into the audit.
+* Read-back audit: both repositories UNKNOWN (HTTP 403); neither is marked
+  repaired. The description update also returned HTTP 403.
+* Local documentation integrity check and all 12 regression tests passed.
+* The new workflow has not run remotely from this working branch. Its empty
+  dependency entry was added to `actions.lock`; the extension was unavailable
+  and its installation failed, so automatic lock regeneration was not run.
+* Label Triage run 35779001180 had a billing-refusal annotation before its
+  first step. No speculative classifier rewrite was made for that failure.
+
+Issues #15 and #16 must remain open until the repository changes are merged
+and the remaining owner-side acceptance checks pass.
diff --git a/docs/pre-registration.adoc b/docs/pre-registration.adoc
new file mode 100644
index 0000000..d28492d
--- /dev/null
+++ b/docs/pre-registration.adoc
@@ -0,0 +1,251 @@
+// SPDX-License-Identifier: MPL-2.0
+= Pre-registration, provenance and research obligations
+:toc:
+
+== Current status (2026-09-27)
+
+This repository exists and is licensed under MPL-2.0 (see link:../LICENSE[]).
+It is a pre-registration and research notebook, not a checked formalisation.
+K-CUT-LOSS and K-CUT-WARRANT remain OPEN. `SoundWarrant` is an assumed
+receiver-local side-condition, not a result established here.
+The application Agda file contains postulates, not proofs.
+
+This document retires the former machine-readable state format. The ledger
+below preserves the 2026-06-16 research intent and later application targets.
+Sibling proof claims are historical provenance, not independently rechecked
+by this repository's validation. Paths into sibling repositories are not
+local dependencies or evidence of a working local build.
+
+The old creation/licensing blocker is discharged: git initialisation,
+repository creation and licensing have happened. A signed push and sibling
+hub registration are not verified here. The actual research blockers are
+canonical definitions, dependency wiring, the named cross-prover bridge,
+and proofs of the projection/grade obligations.
+
+== Historical research ledger
+
+=== context-notes
+
+note::
+A choreographic fusion of echo grades (structural loss, the ℕ∪{∞} tropical semiring) and
+epistemic transport (standpoint warrant) over a global type G read as a partial causal
+order. The choreography is the clock; cuts (consistent frontiers / antichains) are the
+time points; the branch tree is the modality (∇ contingent vs △ non-contingent loss);
+ordinal rank of a cut is the temporal index. The whole reason to exist is one theorem
+(see [keystone]). It DEPENDS ON, and does not re-prove, machinery in echo-types,
+epistemic-types and tropical-types. NOT invented mathematics: it stands on multiparty
+session types (Honda-Yoshida-Carbone), choreographic programming (Montesi; Hirsch-Garg),
+timed session types (Bocchi-Yoshida) and secure/IFC session types; the ASSEMBLY + K-CUT
+are the contribution. See docs / dev-notes what-choreographic-is.
+
+=== keystone
+
+id::
+K-CUT
+
+name::
+grading-and-transport / projection cut-coherence
+
+status::
+OPEN
+
+informal::
+Projecting G onto party p and reading p's local (loss, warrant) timeline up to a cut c
+agrees with the global accumulation of (loss, warrant) over G up to c, restricted to p.
+Slogan: grading and transport commute with projection across a cut.
+
+loss-component::
+* id: K-CUT-LOSS
+* status: OPEN
+
+warrant-component::
+* id: K-CUT-WARRANT
+* status: OPEN
+* side-condition: SoundWarrant at the receiver (ASSUMED local soundness, not type-determined)
+
+=== imported-proven
+
+id::
+imp-001
+
+name::
+choreo-grade-commute
+
+home::
+echo-types : proofs/agda/characteristic/RoleGraded.agda:193
+
+status::
+PROVEN (--safe --without-K, postulate-free; verified 2026-06-16; 18 cases / 1 non-trivial)
+
+role-here::
+Degenerate STATIC base case of K-CUT (single edge, no time). Import; do NOT restate as open.
+
+id::
+imp-002
+
+name::
+echo grade dioid ℕ∪{∞} under (min,+)
+
+home::
+echo-types : proofs/agda/experimental/echo-additive/Grade.agda
+
+status::
+PROVEN-but-UNWIRED (compiles --safe standalone; absent from All.agda; gated R-2026-05-18)
+
+role-here::
+Loss algebra. A consumer MUST wire/vendor it; it does NOT travel with echo-types' green closure.
+
+=== depends-on-sibling
+
+id::
+dep-001a
+
+name::
+epistemic standpoint-warrant (PROOF HOME)
+
+home::
+epistemic-types : src/EpistemicTypes/{Warrant,ProofTransport}.agda
+
+status::
+PROOF DEPENDENCY (Agda --safe). Non-factive Warrant + SoundWarrant; transmit / proofNeedsChecker.
+
+note::
+K-CUT-WARRANT's determine-vs-bound gap lives HERE. CORRECTION: the original draft misattributed this to proven-epistemic.
+
+id::
+dep-001b
+
+name::
+proven-epistemic disclosure server (RUNTIME WITNESS only)
+
+home::
+proven-servers : protocols/proven-epistemic (Idris2)
+
+status::
+RUNTIME WITNESS, NOT a proof source. decideDisclosable is a TOTAL Dec (it determines — opposite posture). Flawed / redesign pending.
+
+note::
+Cite only as the enforcement-gap instance at the BEAM/JS boundary. Never load-bearing.
+
+id::
+dep-002
+
+name::
+tropical resource-dioid
+
+home::
+tropical-types (tropical-resource-typing) : Resource.* (Lean 4)
+
+status::
+DEPEND-ON-SIBLING via in-site PORT (no Agda<->Lean import path). Re-axiomatise ResourceAlgebra in Agda; cite the Lean proof as warrant of inhabitation.
+
+note::
+Dioid fork RESOLVED-BY-PARAMETRICITY upstream: MaxPlus/MinPlus/MinMax are instances of one ResourceAlgebra; parametric_resource_transport proven on no axioms.
+
+=== standing-decisions
+
+id::
+sd-001
+
+title::
+Dioid fork — RESOLVED by parametricity (NOT an open ratification)
+
+status::
+resolved
+
+note::
+Write K-CUT-LOSS against [ResourceAlgebra R]; holds at min-plus / max-plus / min-max at once. The real residual is the cross-prover bridge (in-site port), not the carrier.
+
+id::
+sd-002
+
+title::
+Standalone repo, registered in nextgen-typing (an edge, NOT a subdir)
+
+status::
+accepted
+
+id::
+sd-003
+
+title::
+GitHub canonical, hub-and-spoke mirror; name = choreographic-types (in the -types family)
+
+status::
+accepted
+
+=== claims
+
+id::
+c-cut-coherence
+
+status::
+OPEN
+
+text::
+K-CUT + its loss/warrant split. The single falsifier.
+
+id::
+c-soundwarrant
+
+status::
+ASSUMED
+
+text::
+Receiver-local checker soundness; K-CUT-WARRANT is conditional on it. Never to be claimed PROVEN here.
+
+=== cross-prover
+
+note::
+echo + epistemic = Agda (same kernel — genuine imports). tropical = Lean 4 (NO import path).
+Host choreographic-types in Agda; import echo+epistemic; re-prove the dioid in-site with an
+explicit NAMED prover-bridge obligation citing tropical-types' Lean proof. Never call it 'import'.
+Precedent: typed-wasm/src/abi/TypedWasm/ABI/Tropical.idr ports tropical-types in Idris.
+
+=== application-targets
+
+id::
+app-rapidnj-002
+
+name::
+two-thread RapidNJ K-CUT-LOSS square
+
+status::
+OPEN TARGET (not a proof; application note only)
+
+frontier::
+two selected events e1/e2 with Independent₂ witness
+
+minimum-lemma::
+localGrade p (localStep p e2 (localStep p e1 (project p s))) ≡ transportLoss p (globalGrade (step e2 (step e1 s)))
+
+prerequisite::
+canonical state diamond for disjoint read/write footprints
+
+non-claim::
+Does not assert upstream RapidNJ exposes this batch interface; does not address K-CUT-WARRANT
+
+id::
+app-rapidnj-001
+
+name::
+two-thread RapidNJ canonical state diamond
+
+status::
+OPEN TARGET (algorithmic prerequisite, not K-CUT)
+
+statement::
+step e2 (step e1 s) ~= step e1 (step e2 s) under Independent₂
+
+== Remaining work
+
+* Confirm registration in `nextgen-typing`; do not assume it has happened.
+* Define canonical global/local types, projection and `ResourceAlgebra`.
+* State K-CUT-LOSS against the parametric algebra; keep equality separate
+  from the conditional K-CUT-WARRANT bound.
+* Wire or vendor the echo loss algebra explicitly; a sibling green build
+  does not establish inclusion of its experimental module.
+* Re-prove the tropical algebra in Agda and discharge a named bridge
+  obligation. A Lean theorem is provenance, not an Agda import.
+* Discharge the RapidNJ state diamond and projection square separately;
+  do not promote a postulated signature to evidence of a theorem.
diff --git a/mise.toml b/mise.toml
index 6dd983f..d9efb0e 100644
--- a/mise.toml
+++ b/mise.toml
@@ -1,57 +1,13 @@
+# SPDX-License-Identifier: MPL-2.0
+# Only the runtime used by this pre-registration's integrity checks.
+# There is no Agda, Cargo, npm-package or Go build to invoke.
 [tools]
-# Language runtimes
-node = "latest"
-python = "latest"
-rust = "latest"
-go = "latest"
-zig = "latest"
-java = "latest"
-bun = "latest"
-denojs = "latest"
+node = "22"
 
-# Package managers
-npm = "latest"
-yarn = "latest"
-pnpm = "latest"
-pip = "latest"
-cargo = "latest"
-go-task = "latest"
+[tasks.check]
+description = "Check documentation integrity (not mathematical proofs)"
+run = "node scripts/check-repository.mjs"
 
-# Formatting & Linting
-gofmt = "latest"
-black = "latest"
-isort = "latest"
-ruff = "latest"
-prettier = "latest"
-shfmt = "latest"
-stylua = "latest"
-
-# Build tools
-cmake = "latest"
-make = "latest"
-ninja = "latest"
-
-# Shell tools
-git = "latest"
-gnu-sed = "latest"
-gnu-tar = "latest"
-gnu-grep = "latest"
-
-# Testing
-vitest = "latest"
-pytest = "latest"
-jest = "latest"
-
-[env]
-# Common environment variables
-NODE_ENV = "development"
-PYTHONDONTWRITEBYTECODE = "1"
-PYTHONUNBUFFERED = "1"
-
-# Task runner alias
-[alias]
-task = "go-task"
-build = "cargo build --release || npm run build || go build"
-test = "cargo test || npm test || go test ./..."
-lint = "ruff check . || prettier --check . || black --check ."
-fmt = "ruff format . || prettier --write . || black ."
+[tasks.test]
+description = "Run integrity and policy regression tests"
+run = "node --test tests/*.test.mjs"
diff --git a/scripts/actions-policy.mjs b/scripts/actions-policy.mjs
new file mode 100644
index 0000000..a01a2a4
--- /dev/null
+++ b/scripts/actions-policy.mjs
@@ -0,0 +1,60 @@
+// SPDX-License-Identifier: MPL-2.0
+// Read-only audit / payload preparation. Intentionally has no PUT mode.
+import { execFileSync } from 'node:child_process';
+import { resolve } from 'node:path';
+import { fileURLToPath } from 'node:url';
+
+export function payloadFrom(canon) {
+  const { github_owned_allowed, verified_allowed, patterns_allowed } = canon;
+  if (typeof github_owned_allowed !== 'boolean' || typeof verified_allowed !== 'boolean' ||
+      !Array.isArray(patterns_allowed) || !patterns_allowed.length ||
+      patterns_allowed.some(p => typeof p !== 'string' || !p.trim()) ||
+      new Set(patterns_allowed).size !== patterns_allowed.length) {
+    throw new Error('Invalid or empty canonical allow-list; refusing to prepare a payload');
+  }
+  return { github_owned_allowed, verified_allowed, patterns_allowed };
+}
+
+export function samePolicy(actual, expected) {
+  return actual.github_owned_allowed === expected.github_owned_allowed &&
+    actual.verified_allowed === expected.verified_allowed &&
+    Array.isArray(actual.patterns_allowed) &&
+    JSON.stringify([...actual.patterns_allowed].sort()) === JSON.stringify([...expected.patterns_allowed].sort());
+}
+
+function api(endpoint) {
+  return JSON.parse(execFileSync('gh', ['api', endpoint], { encoding: 'utf8', stdio: ['ignore', 'pipe', 'inherit'] }));
+}
+
+function main() {
+  const [mode, ref] = process.argv.slice(2);
+  if (!['payload', 'audit'].includes(mode) || !/^[a-f0-9]{40}$/.test(ref ?? '') || process.argv.length !== 4) {
+    throw new Error('Usage: node scripts/actions-policy.mjs <payload|audit> <standards full commit SHA>');
+  }
+  const file = api(`repos/hyperpolymath/standards/contents/config/settings/actions-allowlist.json?ref=${ref}`);
+  const expected = payloadFrom(JSON.parse(Buffer.from(file.content, 'base64').toString('utf8')));
+  console.error(`Canon ${ref}: ${expected.patterns_allowed.length} patterns`);
+  if (mode === 'payload') {
+    console.log(JSON.stringify(expected, null, 2));
+    return;
+  }
+  let failed = false;
+  for (const repo of ['choreographic-types', 'echo-types']) {
+    try {
+      const base = `repos/hyperpolymath/${repo}/actions/permissions`;
+      const permissions = api(base);
+      const actual = api(`${base}/selected-actions`);
+      const matches = permissions.enabled === true && permissions.allowed_actions === 'selected' && samePolicy(actual, expected);
+      console.log(`${repo}: ${matches ? 'MATCH' : 'DRIFT'}; live patterns=${actual.patterns_allowed?.length}; expected=${expected.patterns_allowed.length}`);
+      failed ||= !matches;
+    } catch (error) {
+      console.error(`${repo}: UNKNOWN (API access failed); not a policy pass`);
+      failed = true;
+    }
+  }
+  if (failed) process.exitCode = 1;
+}
+
+if (process.argv[1] && resolve(process.argv[1]) === fileURLToPath(import.meta.url)) {
+  try { main(); } catch (error) { console.error(error.message); process.exitCode = 1; }
+}
diff --git a/scripts/check-repository.mjs b/scripts/check-repository.mjs
new file mode 100644
index 0000000..0fca418
--- /dev/null
+++ b/scripts/check-repository.mjs
@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: MPL-2.0
+// Documentation checks only: never evidence that K-CUT is proved.
+import { existsSync, readdirSync, readFileSync } from 'node:fs';
+import { dirname, resolve } from 'node:path';
+import { fileURLToPath } from 'node:url';
+
+export function checkRepository(root) {
+  const errors = [];
+  function walk(dir) {
+    for (const entry of readdirSync(dir, { withFileTypes: true })) {
+      if (['.git', 'node_modules', '.cache'].includes(entry.name)) continue;
+      const path = resolve(dir, entry.name);
+      if (entry.isDirectory()) walk(path);
+      else if (entry.isFile()) {
+        if (entry.name.endsWith('.a2ml')) errors.push(`Retired state format: ${path}`);
+        if (!entry.name.endsWith('.adoc')) continue;
+        const text = readFileSync(path, 'utf8');
+        for (const [, target] of text.matchAll(/link:([^\s\[]+)\[/g)) {
+          if (/^[a-z][a-z\d+.-]*:/i.test(target) || target.startsWith('#')) continue;
+          const local = target.split('#')[0];
+          if (!existsSync(resolve(dirname(path), local))) errors.push(`Broken local link in ${path}: ${target}`);
+        }
+        if (/dev-notes\/2026-06-16-choreographic-types-what-it-is\.adoc/.test(text)) {
+          errors.push(`Retired nonexistent design-note reference: ${path}`);
+        }
+        if (/bestpractices\.dev\/projects\/XXXX/.test(text)) errors.push(`Placeholder certification badge: ${path}`);
+      }
+    }
+  }
+  walk(root);
+  const readme = readFileSync(resolve(root, 'README.adoc'), 'utf8');
+  if (!/pre-registration/i.test(readme)) errors.push('README must disclose pre-registration status');
+  if (!readme.includes('Nothing in this repo is proven yet.')) errors.push('README must disclose proof status');
+  for (const [, source] of readme.matchAll(/\bagda\b[^\n]*?([\w./-]+\.agda)/g)) {
+    if (!existsSync(resolve(root, source))) errors.push(`Nonexistent Agda build target: ${source}`);
+  }
+  return errors;
+}
+
+if (process.argv[1] && resolve(process.argv[1]) === fileURLToPath(import.meta.url)) {
+  const errors = checkRepository(resolve(dirname(fileURLToPath(import.meta.url)), '..'));
+  errors.forEach(error => console.error(error));
+  if (errors.length) process.exitCode = 1;
+  else console.log('Documentation integrity passed (not an Agda proof check).');
+}
diff --git a/tests/repository.test.mjs b/tests/repository.test.mjs
new file mode 100644
index 0000000..3f88c20
--- /dev/null
+++ b/tests/repository.test.mjs
@@ -0,0 +1,43 @@
+// SPDX-License-Identifier: MPL-2.0
+import { test } from 'node:test';
+import assert from 'node:assert/strict';
+import { mkdtempSync, writeFileSync, rmSync } from 'node:fs';
+import { tmpdir } from 'node:os';
+import { join } from 'node:path';
+import { checkRepository } from '../scripts/check-repository.mjs';
+import { payloadFrom, samePolicy } from '../scripts/actions-policy.mjs';
+
+const status = 'A pre-registration. Nothing in this repo is proven yet.\n';
+function fixture(t, files = {}) {
+  const root = mkdtempSync(join(tmpdir(), 'choreo-check-'));
+  t.after(() => rmSync(root, { recursive: true, force: true }));
+  for (const [name, text] of Object.entries({ 'README.adoc': status, ...files })) writeFileSync(join(root, name), text);
+  return root;
+}
+test('honest pre-registration passes', t => assert.deepEqual(checkRepository(fixture(t)), []));
+test('existing local and external links pass', t => {
+  const root = fixture(t, { 'README.adoc': status + 'link:note.adoc#heading[note] link:https://example.org/[web]', 'note.adoc': 'note' });
+  assert.deepEqual(checkRepository(root), []);
+});
+for (const [name, files, expected] of [
+  ['broken link', { 'note.adoc': 'link:absent.agda[]' }, /Broken local link/],
+  ['retired state', { 'STATE.a2ml': 'stale' }, /Retired state format/],
+  ['missing build', { 'README.adoc': status + 'agda --no-libraries -i src src/ChoreographicTypes/All.agda' }, /Nonexistent Agda build/],
+  ['missing note', { 'note.adoc': '`dev-notes/2026-06-16-choreographic-types-what-it-is.adoc`' }, /nonexistent design-note/],
+  ['false badge', { 'note.adoc': 'https://www.bestpractices.dev/projects/XXXX' }, /Placeholder/],
+  ['lost proof disclosure', { 'README.adoc': 'pre-registration' }, /proof status/],
+  ['lost project disclosure', { 'README.adoc': 'Nothing in this repo is proven yet.' }, /pre-registration status/],
+]) test(`regression: ${name}`, t => assert.match(checkRepository(fixture(t, files)).join('\n'), expected));
+
+const canon = { github_owned_allowed: true, verified_allowed: true, patterns_allowed: ['owner/a@*', 'owner/b@*'] };
+test('payload strips non-API metadata', () => assert.deepEqual(payloadFrom({ ...canon, version: 1 }), canon));
+test('empty, malformed and duplicate patterns fail closed', () => {
+  for (const patterns_allowed of [[], null, [''], [3], ['a', 'a']]) assert.throws(() => payloadFrom({ ...canon, patterns_allowed }));
+  assert.throws(() => payloadFrom({ ...canon, verified_allowed: 'true' }));
+});
+test('comparison ignores ordering but detects same-count drift and flags', () => {
+  assert.ok(samePolicy({ ...canon, patterns_allowed: [...canon.patterns_allowed].reverse() }, canon));
+  assert.ok(!samePolicy({ ...canon, patterns_allowed: ['owner/a@*', 'other/c@*'] }, canon));
+  assert.ok(!samePolicy({ ...canon, verified_allowed: false }, canon));
+  assert.ok(!samePolicy({ ...canon, patterns_allowed: [] }, canon));
+});