diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
index 264d05e..4f6eea7 100644
--- a/0-AI-MANIFEST.a2ml
+++ b/0-AI-MANIFEST.a2ml
@@ -14,7 +14,8 @@
(status "starred"))
(milestones
- (phase-a "COMPLETE" "2026-04-15" "Multi-root grounding, proptest, and benchmarks"))
+ (phase-a "COMPLETE" "2026-04-15" "Multi-root grounding, proptest, and benchmarks")
+ (adr-0001 "ACCEPTED" "2026-08-05" "Layer 3 ruled: the SORTAL layer; 3 of 5 counts against it broke"))
;; ==========================================================================
;; CORE IDEA — CANONICAL STATEMENT
@@ -91,14 +92,114 @@
(canonical-locations
(ai-manifest "0-AI-MANIFEST.a2ml" "THIS FILE")
- (launcher "invariant-path-launcher" "Standardized launcher"))
+ (launcher "invariant-path-launcher" "Standardized launcher")
+ (decisions "docs/decisions/" "ADRs — the layer rulings")
+ (architecture "ARCHITECTURE.md" "How the work is arranged")
+ (debt "docs/DEBT.md" "Live debt register"))
(structure
"invariant-path/
- ├── crates/ # Rust crates (CLI, core logic)
- ├── profiles/ # Scan profiles for different repos
- ├── schemas/ # JSON schemas for annotations
- └── scripts/ # Management and installation scripts")
+ ├── docs/decisions/ # ADRs — the LAYER RULINGS. Start at 0001.
+ ├── crates/invariant-path-core # extractor, classifier, model, annotations
+ ├── crates/invariant-path-cli # the binary (single main.rs)
+ ├── schemas/ # JSON schema for persisted annotations
+ ├── profiles/ # lenses onto corpora ELSEWHERE; vendor nothing
+ ├── proofs/ # SameCube.agda (the faces worked example)
+ ├── examples/same-cube/ # vendored corpus — violates profile-rule, issue #54
+ ├── scripts/ # verify-same-cube.sh, install-desktop.sh
+ ├── src/ui/ # AffineScript GUI SKETCH — in NO build
+ └── desktop/, assets/ # launcher entry and icons")
+
+ (architecture
+ (headline
+ "Two faces. (1) The GOVERNANCE FRONT-END for a three-layer claim checker —
+ this is where the layer architecture is decided and recorded, and where
+ most of the intellectual work lives. (2) A shipping Rust CLI that extracts
+ and classifies claim transitions. The second is NOT an implementation of
+ the first; keep that distinction visible.")
+
+ (layer-1 "type"
+ "Formal admissibility, checkable on FORM ALONE. Sub-layers: well-formedness;
+ continuity/through-line; temporality = 'the diode', a forward-only ordering
+ (evidence precedes conclusion, no backward edges) applied PER CLAIM-TYPE.
+ OPEN: the diode's clock must be EPISTEMIC not ontic or retrodiction fails
+ to type-check; epistemic time across sources is a PARTIAL order, so verdicts
+ need invariance across interleavings; per-type diodes glue into differently
+ clocked charts, so a path forward in every chart can reach backwards
+ globally (composition-forgery — holonomy).")
+
+ (layer-2 "trope"
+ "Particularity and warrant, PURPOSE-INDEXED, per strand. IMPLEMENTED
+ ELSEWHERE (trope-checker + hermeneia): a six-coordinate Grade, nine p-*
+ effects (three deceptive and absorbing), a Floor as partial demand vector,
+ and a verdict Sufficient|Insufficient CARRYING A WITNESS EDGE. p-sufficiency
+ is floor(U) [= acc(v). Resource discipline is AFFINE (at most once) WITH A
+ GUARDED CONTRACTION RULE — not plain affine logic.")
+
+ (layer-3 "sortal"
+ "Adjudicates IDENTITY OF AN ARGUMENT ACROSS PRESENTATIONS, issuing an
+ EQUIVALENCE CERTIFICATE (a move sequence whose every intermediate still
+ passes layers 1 and 2) or an OBSTRUCTION CERTIFICATE (an invariant
+ separating them under the same quotient). Detection and equivalence-
+ certification are DUAL. Named for the sortal of Locke/Strawson/Wiggins/Lowe:
+ a concept supplying a CRITERION OF IDENTITY and a PRINCIPLE OF COUNTING.
+ Ruled in docs/decisions/0001-the-sortal-layer.adoc after 3 of 5 counts
+ against the layer broke under adversarial review.")
+
+ (dependency-order
+ "Layer 1 --orientations--> Layer 3 --identities--> Layer 2.
+ Layer 3 is UPSTREAM of Layer 2's soundness. Overlapping presentations must
+ be recognised as the same argument BEFORE resource accounting, or Layer 2
+ double-counts. This arrow was missing from the original design.")
+
+ (killer-case "the doubling attack"
+ "One derivation presented TWICE, paraphrased, under distinct labels.
+ Label-honest (the diode is silent), well-founded, exogenously attested,
+ each copy individually warranted — and it has an IDENTICAL pass/fail profile
+ to genuine two-witness corroboration on EVERY subdiagram, so no layer-1 or
+ layer-2 sweep can see it, while corroboration weight is 2 versus 1.
+ It is NOT an illegal contraction; it is a contraction that was MANDATORY AND
+ NEVER TAKEN, to which the affine resource algebra is structurally blind.")
+
+ (status
+ "DECIDED, NOT BUILT. Nothing in this repository implements these layers.
+ Layer 1 has NO substrate anywhere in the estate. Layer 2 has real support
+ from tropical-types and echo-types. Layer 3 has ~a quarter, obstruction
+ side only, from echo-types' fibre. QuandleDB and absolute-zero's CNO were
+ both investigated as substrates and REFUTED WITH EVIDENCE — do not reopen
+ either without new evidence. See docs/DEBT.md sections A1-A3.")
+
+ (numbering-hazard
+ "NEVER write bare L1/L2/L3. Three unrelated L1-L10 schemes are live in
+ adjacent repositories (kategoria = language-feature ladder, typell/VCL =
+ query-safety scale), and BOTH neighbours put temporality at their L9 while
+ this architecture puts it at Layer 1c. Write 'Layer 1 (type)',
+ 'Layer 2 (trope)', 'Layer 3 (sortal)'; prefix foreign refs kat-L7, ty-L9."))
+
+ (debt
+ (register "docs/DEBT.md" "live; supersedes docs/tech-debt-2026-05-26.md")
+ (resolved "CI/CD: the lockfile epidemic is CURED (PR #56, 2026-08-05).
+ Until then ALL workflows were startup_failure on EVERY branch and
+ main had never been green. Now 10 green on main including Rust CI,
+ CodeQL and Secret Scanner — the gates are real. Residual: OSSF
+ Scorecard still startup_failure; Well-Known Standards and Workflow
+ Security Linter fail on content, untriaged. NOTE, because it will
+ recur: `gh pr checks` shows nothing wrong for a parse-rejected
+ workflow, since it emits no check run; use `gh run list`.")
+ (high "Architecture: layer 1 has no substrate; layer 3's equivalence side
+ (move relation, quotient, normal form) does not exist anywhere.")
+ (medium "Layer 2 VOCABULARY MISMATCH: of strength/consistency/coherence/
+ resemblance-warrant-on-merge/p-residue/p-sufficiency, only
+ p-sufficiency is real. p-residue exists in NO repository. Left
+ deliberately unreconciled; see docs/DEBT.md A3.")
+ (medium "Proof: proofs/SameCube.agda is real (--safe, zero postulates, zero
+ holes) but UNGATED — no workflow compiles it. verify-same-cube.sh
+ exits 0 on a missing compiler.")
+ (medium "Licence: GitHub reports NO licence — LICENSE deviated from canonical
+ MPL-2.0 (trailing space line 38, http vs https line 360). SPDX
+ identifiers sit on line 2-3 behind an opening comment, which the
+ estate linter (head -1 only) reads as missing. Do NOT fix by adding
+ headers — MOVE them; a blind sweep previously mis-licensed files."))
(format-meta
(version "2.1.0")
diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md
index 607e3d8..5e88e4f 100644
--- a/ARCHITECTURE.md
+++ b/ARCHITECTURE.md
@@ -1,47 +1,267 @@
+
+
# Architecture
-## Overview
+> **Read `0-AI-MANIFEST.a2ml` first.** Its `(core-idea …)` block is the canonical
+> statement of what this repository is for, and it is marked do-not-paraphrase.
+> This file describes how the work is arranged; it does not restate the idea.
+
+Invariant Path is a claim-path debugger, not a truth engine. It has two faces:
+
+1. **The governance front-end for a three-layer claim checker.** This is where
+ the layer architecture is decided and recorded. Most of the intellectual
+ work lives here.
+2. **A working extractor and classifier.** A Rust CLI that finds claim
+ transitions in repository artifacts and records what each one preserves and
+ loses. This is what currently ships.
+
+The second is not an implementation of the first. Keeping that distinction
+visible is the point of this document.
+
+---
+
+## Part I — The three-layer claim checker
+
+A claim is checked by three layers, each answering a question the others
+cannot. `nextgen-language-evangeliser` names this repository as the *governance
+front-end* for that architecture: rulings are recorded here as ADRs, and each
+equivalence claim is anchored to its code locations plus a witness,
+human-in-the-loop and editable.
+
+### Layer 1 — `type`: formal admissibility
+
+Checkable on **form alone**, with no judgement of evidence quality. Three
+sub-layers:
+
+- **Well-formedness** — is this a claim at all?
+- **Continuity / through-line** — does the argument connect end to end?
+- **Temporality — "the diode"** — a forward-only ordering constraint: evidence
+ must precede conclusion, no backward edges, applied **per claim-type**.
+
+The diode was sited in Layer 1 deliberately, so that anything downstream
+inherits strand orientations from a clean form-only rule rather than from Layer
+2's purpose-indexed judgements.
+
+**What is settled, and what is not.** The diode is correct but narrower than it
+looks: it rejects only *label-honest* backward edges. Three open problems are
+recorded in ADR-0001:
+
+- Its clock must be **epistemic** (when evidence was committed) rather than
+ ontic (when events happened), or retrodiction — history, forensics — falsely
+ fails to type-check.
+- Epistemic time across multiple sources is therefore a **partial order**, not
+ a scalar clock, so verdicts must be proved invariant across admissible
+ interleavings of causally incomparable commits.
+- Because the diode applies *per claim-type*, differently-clocked charts glue
+ together, and a composite path can run forward in every chart while its
+ endpoints reach backwards globally. ADR-0001 calls this **composition-forgery**;
+ it is a holonomy phenomenon — every chart flat, the twist in the gluing.
+
+### Layer 2 — `trope`: particularity and warrant
+
+**Purpose-indexed**, per strand: does individuated, context-bound evidence
+survive the leap to *this* conclusion for *this* use?
+
+This is the layer with a real implementation, and it lives in
+`trope-checker` and `hermeneia`, not here:
+
+- a six-coordinate **`Grade`** — four `Fate` fields plus `Bond` and `Merge`
+ (`Trope/Grade.idr`);
+- nine **`p-*` effects** in `trope-particularity-workbench/vocabulary/`, of
+ which three are *deceptive* and absorbing under composition;
+- a **`Floor`** — a use-model expressed as a partial demand vector
+ (`Checker/Ir.idr`);
+- a verdict `Sufficient | Insufficient` that **carries a witness edge** on
+ failure (`Checker/Check.idr`);
+- **p-sufficiency**, defined as `floor(U) ⊑ acc(v)` — the declared floor lies
+ below the accumulated grade in a componentwise retention order.
+
+Grades compose associatively along transformation paths, with the fidelity
+coordinate accumulating tropically.
+
+**Resource discipline: affine, with a guarded contraction rule.** At most once
+— weakening is free, contraction is not — but contraction *is* permitted when a
+resemblance warrant licenses it. That is not plain affine logic, and the
+distinction is load-bearing; see the doubling attack below.
+
+### Layer 3 — `sortal`: identity across presentations
+
+Ruled 2026-08-05 in `docs/decisions/0001-the-sortal-layer.adoc`, after a
+five-count case against the layer was built deliberately and **three of the
+five counts broke** under adversarial review.
+
+The layer adjudicates **identity of an argument across presentations**, and
+issues one of two things:
+
+- an **equivalence certificate** — a sequence of moves, every intermediate of
+ which still passes Layers 1 and 2, transforming one presentation into the
+ other;
+- an **obstruction certificate** — an invariant separating them under the same
+ quotient.
+
+Detection and equivalence-certification are **dual**, so "it is only an
+equivalence proof" is the job stated correctly, not a demotion.
+
+The name is from the same literature `trope` came from: a **sortal** supplies a
+*criterion of identity* and a *principle of counting* for its instances. Both
+halves do work — the criterion decides "same argument", the count decides
+whether two corroborating lines are two witnesses or one witness echoed.
-This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability.
+### The doubling attack, and why Layer 3 precedes Layer 2
-## Directory Structure
+Present one derivation **twice**, paraphrased, under distinct labels. Every
+node is label-honest, so the diode is silent. Every chain terminates in
+genuinely attested exogenous anchors, so attestation and well-foundedness both
+pass. Each copy individually passes Layer 2.
+
+The doubled web and an honestly-redundant two-witness web have **identical
+pass/fail profiles on every subdiagram** — yet corroboration weight is two
+versus one.
+
+This is not an illegal contraction. It is a contraction that was **mandatory
+and never taken**, and the affine resource algebra is structurally blind to it:
+nothing illegal happened, two distinct labels really were spent once each.
+Whether they were the same token is a fact about *identity*, which is not a
+resource property.
+
+Hence the dependency arrow that the original design was missing:
```
-.
-├── src/ # Source code
-├── tests/ # Test suites
-├── docs/ # Documentation
-├── scripts/ # Utility scripts
-├── config/ # Configuration files
-├── LICENSE # License file
-├── LICENSES/ # Full license texts
-└── README.adoc # Project documentation
+Layer 1 (type) ──orientations──▶ Layer 3 (sortal) ──identities──▶ Layer 2 (trope)
```
-## Design Principles
-
-- **Separation of Concerns**: Each module has a single responsibility
-- **Testability**: Code is written to be easily testable
-- **Documentation**: All public APIs are documented
-- **Configuration**: Environment-specific settings are externalized
+Overlapping presentations must be recognised as the same argument **before**
+resource accounting runs, or Layer 2 double-counts. Layer 3 is upstream of
+Layer 2's soundness, not decoration downstream of it.
-## Dependencies
+### Status: decided, not built
-- External dependencies are minimized and clearly declared
-- Version pinning is used for reproducibility
+**Nothing in this repository implements these layers.** ADR-0001 is a decision
+record about an architecture, and says so. A survey of existing formal work
+(recorded in the ADR) found:
-## Security Considerations
+- **Layer 1** — no substrate anywhere in the estate. No syntax of claims, no
+ ordering on evidence events. Must be built from scratch.
+- **Layer 2** — real support from `tropical-types` (the retention order derived
+ from one line of idempotence, axiom-free, behind a genuine CI gate) and
+ `echo-types` (path-independence of degradation holds precisely if the
+ retention order is propositional, with a countermodel).
+- **Layer 3** — roughly a quarter, obstruction side only. `echo-types` supplies
+ the fibre `Echo f y = Σ A (λ x → f x ≡ y)` — "which distinct presentations
+ collapsed to the same argument" — and "identified members count once". There
+ is **nothing** on the equivalence side: no move relation, no quotient, no
+ normal form, anywhere.
-- Sensitive data is never committed to the repository
-- Secrets are managed through environment variables or secure vaults
-- Regular dependency audits are performed
+Two candidate substrates were investigated and **refuted with evidence**:
+QuandleDB (a homonym — topological invariants are blind to labels, so a quandle
+fingerprint cannot see the doubling attack and would return false positives)
+and absolute-zero's CNO (machine-checked refutation against its own Coq).
-## Maintainability
+### Conventions
-- Code follows consistent style guidelines
-- Pull requests require review and CI checks
-- Issues and discussions are tracked transparently
+Do not write bare `L1` / `L2` / `L3`. Three unrelated L-numberings are live in
+adjacent repositories, and both neighbours put temporality at *their* L9 while
+this architecture puts it at Layer 1c. Write `Layer 1 (type)`,
+`Layer 2 (trope)`, `Layer 3 (sortal)`; prefix foreign references `kat-L7`,
+`ty-L9`.
---
-*Last updated: 2026-07-18*
+## Part II — The shipping tool
+
+What actually compiles and runs today: a pipeline from artifact text to a
+reviewable record.
+
+```
+artifact text
+ │
+ ▼
+ extractor candidate claim transitions, anchored by trigger phrase
+ │ and byte span
+ ▼
+ classifier invariant type; losses/preserved; break condition;
+ │ a Classification
+ ▼
+ annotations JSONL, upsert-on-write, visibility + status
+ │
+ ▼
+ CLI scan / accept / dismiss / clarify / add / update / overlay
+```
+
+Two commitments explain most of the code.
+
+**Heuristics are deliberately strict.** The extractor triggers on explicit
+transition markers and accepts false negatives to avoid annotation noise
+(`DESIGN.md`, 2026-04-10). A noisy suggester costs more trust than it saves.
+
+**The path is retained, never discarded.** A bare `Classification` cannot
+recover the claim-path that produced it, so `ClassificationOutcome` carries
+`losses` and `preserved` alongside the verdict — the `echo-types` fibre
+discipline applied to a classifier. See `docs/ECHO-TYPES.md`.
+
+### Domain model
+
+In `crates/invariant-path-core/src/model.rs`:
+
+- **`ClaimCandidate`** — source span, target text, matched trigger, path
+ description.
+- **`InvariantType`** — what is meant to be preserved: `CausalRelationship`,
+ `StatisticalRelationship`, `LogicalImplication`, `Mechanism`,
+ `RiskProbability`, `NormativeBridge`, `ResourceBudget`, `Provenance`.
+- **`Classification`** — `ValidPath`, `Overextended`, `Conflation`,
+ `Incomplete`, `Abstain`.
+- **`ClassificationOutcome`** — the verdict *plus* `losses`, `preserved`, break
+ condition. The retained echo.
+- **`Annotation`** — the persisted record, with `Visibility` and `Status`.
+
+The classifier is pure and offline: term lists in `classifier.rs`, no model, no
+network, no external state.
+
+### Profiles
+
+A profile is a **lens onto a corpus that lives elsewhere**. It names a target
+by path and **vendors nothing**. `pmpl.md` is the reference implementation.
+
+The rule exists because a profile carrying a copy of its target drifts from the
+real thing and then grounds a claim about a stale fixture *while reporting
+success* — this tool's own failure mode, turned inward. Profiles are named for
+their **target**, not for one claim about it.
+
+Six exist: `echidna`, `faces`, `hypatia`, `panll`, `pmpl`, `standards-docs`.
+
+`faces` is the one worked example that is fully grounded end to end: it checks
+that AffineScript's several surface syntaxes all lower to one canonical form,
+by compiling each to typed-wasm and comparing `sha256` hashes. It is a good
+demonstration of the whole idea in miniature — and it is *an example*, not the
+subject of this repository. It also violates the profile rule twice (it vendors
+its corpus, and it is named for a claim rather than a target), which is issue
+#54. Details in `profiles/faces.md`; its Agda companion is `proofs/SameCube.agda`.
+
+## Layout
+
+| Path | What lives there |
+|---|---|
+| `docs/decisions/` | **ADRs — the layer rulings. Start at ADR-0001.** |
+| `crates/invariant-path-core/` | The library: `extractor.rs`, `classifier.rs`, `model.rs`, `annotations.rs`, `doc_claims.rs`, `pipeline.rs`. |
+| `crates/invariant-path-cli/` | The binary. Single `main.rs`; parsing and output only. |
+| `schemas/annotation.schema.json` | The contract between this tool and anything reading its store. |
+| `profiles/` | One markdown file per target corpus. Vendors nothing. |
+| `proofs/`, `examples/same-cube/`, `scripts/verify-same-cube.sh` | The `faces` worked example and its grounding check. |
+| `docs/` | `ARCHITECTURE.md` (module contracts), `EXTENDING.md`, `ECHO-TYPES.md`, `DEBT.md`. |
+| `desktop/`, `assets/` | `.desktop` launcher entry and icons. |
+| `src/ui/` | `invariant_path_gui.affine` — an AffineScript GUI sketch. **Not in the Cargo workspace; built by nothing.** Design material, not code. |
+
+The Cargo workspace is exactly the two crates in `members`; nothing under
+`src/` is compiled.
+
+## What this is not
+
+- Not a truth engine. It never decides whether a claim is true.
+- Not an implementation of the three layers. Those are decided, not built.
+- Not a prover. `proofs/` grounds one claim in one worked example.
+- Not networked. No service, no telemetry, no model calls.
+- Not a general NLP pipeline. The classifier is term lists and pattern matches,
+ chosen so a reader can audit every decision it makes.
diff --git a/LICENSE b/LICENSE
index 14e2f77..d0a1fa1 100644
--- a/LICENSE
+++ b/LICENSE
@@ -35,7 +35,7 @@ Mozilla Public License Version 2.0
means any form of the work other than Source Code Form.
1.7. "Larger Work"
- means a work that combines Covered Software with other material, in
+ means a work that combines Covered Software with other material, in
a separate file or files, that is not Covered Software.
1.8. "License"
@@ -357,7 +357,7 @@ Exhibit A - Source Code Form License Notice
This Source Code Form is subject to the terms of the Mozilla Public
License, v. 2.0. If a copy of the MPL was not distributed with this
- file, You can obtain one at http://mozilla.org/MPL/2.0/.
+ file, You can obtain one at https://mozilla.org/MPL/2.0/.
If it is not possible or desirable to put the notice in a particular
file, then You may include the notice in a location (such as a LICENSE
diff --git a/README.md b/README.md
index 7eb45ba..c266541 100644
--- a/README.md
+++ b/README.md
@@ -52,9 +52,40 @@ one canonical form. Per-face snapshot tests catch drift *within* a face and
never compare face A's cube against face B's. **The cross-face equality is the
load-bearing claim**, and no per-face test can state it.
-Invariant Path grounds that claim: every face's `preview-*` lowering must
-normalise to the same canonical text, and when one breaks, the profile locates
-*which* face broke it.
+Invariant Path grounds that claim: each face is compiled to typed-wasm and the
+modules are compared by `sha256`, so the faces must land in **one wasm
+equivalence class**. The wasm *is* the cube, which makes this a far stronger
+bar than matching canonical text. When a face falls outside the class, a
+normalised text diff is printed to locate *where* — as a diagnostic, not as the
+check itself.
+
+This is one worked example, not the subject of the repository. See
+`profiles/faces.md` for its limits, including the two classes the `greet`
+corpus genuinely splits into.
+
+## The three-layer claim checker
+
+Invariant Path is the **governance front-end** for a layered checker. Each
+layer answers a question the others cannot:
+
+| Layer | Name | Question |
+|---|---|---|
+| 1 | **type** | Is this admissible *on form alone*? Well-formedness, through-line, and a forward-only ordering on evidence — "the diode". |
+| 2 | **trope** | Does this particular evidence survive the leap to this conclusion *for this use*? Purpose-indexed warrant. |
+| 3 | **sortal** | Are these two presentations *the same argument*? Identity, and therefore counting. |
+
+Layer 3 was ruled on in
+[ADR-0001](docs/decisions/0001-the-sortal-layer.adoc) after a five-count case
+against it was built deliberately and three of the five counts broke. Its
+killer case is the **doubling attack**: one derivation presented twice,
+paraphrased, under distinct labels is invisible to every Layer 1 and Layer 2
+check — identical pass/fail on every subdiagram — while corroboration weight is
+two instead of one. That is why Layer 3 runs *before* Layer 2: identity must be
+settled before resource accounting, or Layer 2 double-counts.
+
+**These layers are decided, not built.** The ADR is a decision record. What
+ships today is the extractor, classifier and annotation store described below.
+Open architectural gaps are tracked in [`docs/DEBT.md`](docs/DEBT.md).
## Its dual: 007 and hermeneutic semantics
diff --git a/docs/DEBT.md b/docs/DEBT.md
new file mode 100644
index 0000000..61f13ee
--- /dev/null
+++ b/docs/DEBT.md
@@ -0,0 +1,291 @@
+
+
+# Debt register — invariant-path
+
+**Audited 2026-08-05** by reading the tree and querying the GitHub API. This is
+the *live* register: findings stay until closed, and each carries the evidence
+that would prove it fixed.
+
+Supersedes `docs/tech-debt-2026-05-26.md`, whose "RESOLVED" banner overstates
+the proof item — see [P1](#p1).
+
+| | Dimension | Open | Worst |
+|---|---|---|---|
+| A | Architecture — the three layers | 3 | **HIGH** |
+| C | CI/CD | 3 | MEDIUM |
+| L | Licence | 3 | MEDIUM |
+| D | Docs | 3 | MEDIUM |
+| P | Proof | 2 | MEDIUM |
+| K | Code | 1 | LOW |
+
+---
+
+## Architecture debt
+
+This is where the substantial work is, and where the substantial gaps are.
+ADR-0001 settled Layer 3's charter and name; it did not build anything, and it
+was explicit about what remains.
+
+
+### A1 — Layer 1 has no substrate anywhere. `HIGH`
+
+A survey of `_TYPES _SET` and `_PROVER-SOLVER _SET` (recorded in ADR-0001)
+found **no syntax of claims, premises, steps or evidence in any repository**,
+and **no ordering on evidence events of any kind**. All three sub-layers —
+well-formedness, continuity, temporality — must be built from scratch.
+
+Two names promise otherwise and do not deliver: `choreographic-types` has never
+contained a line of source on any branch, and typell's "Level 9 Temporal
+safety" passes iff a named field is present, examining no event and no order.
+
+**Closed when:** a claim syntax and an evidence-event ordering exist, with the
+diode enforced on the latter.
+
+### A2 — Layer 3's equivalence side does not exist. `HIGH`
+
+`echo-types` supplies roughly a quarter of the layer, and only the
+*obstruction* half: the fibre `Echo f y = Σ A (λ x → f x ≡ y)`, an invariant
+separating two members of one fibre, and "identified members count once".
+
+There is **no move relation, no quotient, and no normal form anywhere** — which
+is the entire equivalence-certificate side. And the one piece most needed is
+`echo-types`' own unclosed debt: propositional truncation is *postulated* under
+`--safe` and constructed only in a `--cubical` island that Agda's flag rules
+forbid the main cone from importing. "Merely inhabited versus how many
+witnesses" is exactly what the doubling attack turns on.
+
+Two candidate substrates were investigated and **refuted with evidence** —
+QuandleDB and absolute-zero's CNO — so this is not a matter of wiring something
+up. Do not reopen either without new evidence; both refutations are in
+ADR-0001.
+
+**Recorded ruling:** mechanise in **Agda `--cubical`**, not Idris 2. The core
+construction is a quotient by admissible moves, and Idris 2's QTT cannot host
+quotients or higher inductive types.
+
+**Closed when:** a move relation and a quotient exist, and an equivalence
+certificate can be produced and checked for a worked pair.
+
+### A3 — Layer 2's vocabulary does not match its implementation. `MEDIUM`
+
+The terms in circulation — strength, consistency, coherence,
+resemblance-warrant-on-merge, p-residue, p-sufficiency — are not the terms in
+code. Only **p-sufficiency** is real (`floor(U) ⊑ acc(v)`). **`p-residue` does
+not exist in any repository in the estate.**
+
+What is built (`trope-checker`) is a six-coordinate `Grade`, nine `p-*`
+effects, a `Floor`, and a witness-carrying `Verdict`.
+
+This matters beyond tidiness: part of the ADR-0001 argument read p-residue as
+affine resource accounting — a term that could not be grounded — so the
+reachability result should be re-derived against the actual grade algebra.
+`trope-particularity-workbench/tests/check-vocabulary.sh` hard-fails on any
+vocabulary entry outside the nine effects, so introducing these terms as if
+established would break a live gate.
+
+Left deliberately unreconciled in ADR-0001 rather than quietly harmonised.
+
+**Closed when:** a ruling records whether the six terms are a new Layer 2
+design superseding the grade algebra, an informal gloss of it, or drift.
+
+---
+
+## CI/CD debt
+
+### C1 — The lockfile epidemic is CURED. `RESOLVED 2026-08-05`
+
+Until 2026-08-05 there was no Actions lockfile, and **every** workflow
+terminated as `startup_failure` before a single step ran, on every branch.
+`main` had never been green, which made every other gate decorative.
+
+Fixed by PR #56, which adopted `.github/workflows/actions.lock`. Re-measured on
+`main` the same day — latest run per workflow:
+
+```
+GREEN (10) Code Quality · CodeQL Security Analysis · Governance ·
+ Guix/Nix Package Policy · Hypatia Security Scan ·
+ RSR Anti-Pattern Check · Runtime Policy · Rust CI ·
+ Secret Scanner · Security Policy
+```
+
+The gates are now real: Rust CI, CodeQL and Secret Scanner actually execute and
+can actually fail. Three residual items remain, tracked below.
+
+> **Diagnosis trap, retained because it will recur.** `gh pr checks` shows
+> *nothing wrong* for a parse-rejected workflow — it emits no check run at all,
+> so a PR looks unchecked rather than broken. Use `gh run list --branch `;
+> a `?status=failure` query also **excludes** `startup_failure`.
+
+### C2 — OSSF Scorecard still fails to start. `MEDIUM`
+
+The one workflow the lockfile fix did not reach: `OSSF Scorecard` is still
+`startup_failure` on `main`, so it has never produced a result. PR #59 proposes
+making it periodic rather than per-push, which may or may not address the
+startup cause — the two are independent.
+
+**Closed when:** Scorecard produces a conclusion other than `startup_failure`.
+
+### C3 — Two workflows fail on content. `MEDIUM`
+
+Genuine failures, not startup problems — which means they are now doing their
+job and reporting something real:
+
+- `Well-Known Standards (RFC 9116 + RSR)`
+- `Workflow Security Linter`
+
+Both were invisible until the lockfile landed, because neither could start.
+Neither has been triaged.
+
+**Closed when:** each either passes or has its finding recorded here as
+accepted.
+
+### C4 — No proof gate. `MEDIUM`
+
+No workflow invokes Agda, and none runs `scripts/verify-same-cube.sh`. The CI
+half of [P1](#p1) and [P2](#p2). Unaffected by the lockfile fix.
+
+**Closed when:** a workflow compiles `proofs/SameCube.agda` and runs the
+verifier, and both can fail the build.
+
+---
+
+## Licence debt
+
+### L1 — GitHub reports **no licence** for this repository. `MEDIUM`
+
+`gh repo view --json licenseInfo` returns `null`, despite a 373-line MPL-2.0
+`LICENSE` at the root and `license = "MPL-2.0"` in `Cargo.toml`. The repository
+shows as unlicensed to anyone browsing it and to tooling reading the API.
+
+Cause: `LICENSE` deviates from canonical MPL-2.0 in two places — a **trailing
+space** at line 38, and `http://` rather than `https://` at line 360.
+`LICENSES/MPL-2.0.txt` is the clean copy.
+
+Fixed in this change by replacing `LICENSE` with the canonical text; detection
+is recomputed on push, so the API result must be re-checked after merge.
+
+**Closed when:** `gh repo view --json licenseInfo` reports `MPL-2.0`.
+
+### L2 — SPDX headers are not on line 1. `MEDIUM`
+
+Twelve of thirteen root-level documents open with `