docs: de-conflate KRL from Tangle, restate the readiness grade honestly

The three projects are distinct and were built for different purposes.
QuandleDB is the knot database. KRL is its resolution language, developed
alongside it. Tangle is a separate, general language for knot mathematics that
happens to share the subject matter. Documentation in this repository had fused
KRL and Tangle into a single compilation pipeline that does not exist.

README.md

* Removed the claim that KRL "lowers through TangleIR into Tangle-level
  computation", and the layer table presenting Tangle as KRL's substrate.
  `TangleIR` appears 0 times in the KRL implementation; the struct definitions
  the README documented as "the single hardest-designed artifact in the stack"
  correspond to no code.
* Removed `KRLAdapter.jl` as the named canonical implementation. It no longer
  exists. A short note records that both claims were false, so the correction
  is legible rather than silent.
* Removed the `TanglePL` usage example, which imports packages that do not
  exist.
* Restated what the repository actually holds, and what it does not: there is
  no parser here, so nothing in this tree can execute a KRL program.
* Added the known divergence between this repository's grammar and QuandleDB's
  — disjoint on core vocabulary, with `|` bound to opposite meanings.
* Restructured to a single <h1>. Ddraig SSG certifies pages against a decidable
  a11y predicate requiring exactly one <h1> and no heading-level skips; the old
  README had 8, which is why GitHub Pages was failing. Verified by compiling
  Ddraig locally and running it: old README FAIL (exit 1), new README ok
  (exit 0).

READINESS.md

* Grade D -> E. The entire evidence base for D was a parser, AST, lowering pass
  and 57-test matrix in `KRLAdapter.jl`, which no longer exists, so none of it
  can be checked. The CRG demotion table gives `D -> E` for "the scope narrows
  so far that the component barely does anything", which is what happened.
* Replaced the evidence section with checks that were executed on 2026-07-21:
  grammar smoke 20/20, zig build test 3/3, aspect 4/4, e2e 4/4.
* Documented the limitations plainly, including that no conformance suite
  exists, so "conforms to the KRL spec" is not currently a checkable claim.
* Removed the duplicated "Path to C"/"Path to B" sections.

ASSUMPTIONS.md

* Added a Status column. Seven DESIGN assumptions named code in
  `KRLAdapter.jl`. A DESIGN assumption is defined in this file as "true by
  construction in our code" — with the code gone there is no construction left
  to be true by.
* A-KR-1.1, 1.2, 2.1, 3.2, 4.1 marked UNANCHORED; A-KR-6.1 and 6.2 marked VOID
  (both presuppose two implementations, and only one exists).
* Verified that no re-anchoring is possible: `sigma`, `cup`, `cap`,
  `r1_simplify` and any pretty-printer appear 0 times in
  `quandledb/server/krl/`. The braid generators these assumptions describe are
  implemented nowhere.
* The four MATH assumptions are untouched — they rest on external theorems.

TOPOLOGY.md

* Was pure RSR-template residue describing the template itself, its dogfood
  gate, and "500+ RSR-based repositories" downstream. Replaced with KRL's
  actual topology: the three project boundaries, the ABI/FFI layering, and the
  spec/implementation seam that no conformance suite currently checks.
* States that this repository exposes no Groove service and has no
  `.well-known/groove/manifest.json`, rather than implying one exists.

Author: hyperpolymath

ASSUMPTIONS.md

@@ -17,19 +17,38 @@ Cross-references use `[[A-KR-N.M]]` syntax, resolved here.
 
 ---
 
-| ID | Class | Statement | Cited by | Where it lives |
-|----|-------|-----------|----------|----------------|
-| A-KR-1.1 | DESIGN | Every `KRLExpr` AST variant has a matching arm in `KRLAdapter.jl::lower.jl` | KR-1 | `KRLAdapter.jl/src/parser/lower.jl` |
-| A-KR-1.2 | DESIGN | `KRLAdapter.jl/src/parser/ast.jl` defines the only AST shapes the parser produces | KR-1 | `KRLAdapter.jl/src/parser/ast.jl` + `parser.jl` |
-| A-KR-2.1 | DESIGN | Generator arity is fixed: `sigma i / sigma_inv i : in=i+1, out=i+1`; `cup i : in=0, out=2`; `cap i : in=2, out=0` | KR-2 | KRL grammar definitions; `KRLAdapter.jl/src/operations.jl` |
-| A-KR-2.2 | MATH | `arity_in(a \| b) = arity_in(a) + arity_in(b)` and same for output (monoidal-category tensor) | KR-2 | Standard categorical tangle definition |
-| A-KR-3.1 | MATH | Reidemeister's theorem: R1+R2+R3 generate isotopy equivalence on tangle diagrams | KR-3 | Reidemeister 1927; Kauffman _Knots and Physics_ ch. 1 |
-| A-KR-3.2 | DESIGN | `KRLAdapter.jl::r1_simplify` / `r2_simplify` / `r3_simplify` implement those moves faithfully (R3 is a current GAP — see `quandledb/PROOF-NARRATIVE.md` QD-2) | KR-3 | `KRLAdapter.jl/src/operations.jl` |
-| A-KR-4.1 | DESIGN | KRL pretty-printer's bracketing is unambiguous: `;` only inside parens; tensor `\|` has lower precedence than compose `;` inside parens | KR-4 | `KRLAdapter.jl` pretty; `spec/grammar.ebnf` |
-| A-KR-6.1 | DESIGN | `KRLAdapter.jl::parse_krl` and `quandledb/server/krl/Parser.jl::parse_any` both target `spec/grammar.ebnf` v0.1.0 | KR-6 | `spec/grammar.ebnf` |
-| A-KR-6.2 | DESIGN | Both implementations share the same `Token` enumeration: keyword set, identifier shape, integer/string literal shapes | KR-6 | `KRLAdapter.jl/src/parser/lexer.jl` and `quandledb/server/krl/Lexer.jl` |
-| A-KR-8.1 | MATH (partial) | Fundamental-quandle functor is faithful on prime alternating knots; partial in general | KR-8 | Joyce 1982; for partial cases see Eisermann _The number of knot group representations_ |
-| A-KR-8.2 | MATH | Two non-isomorphic quandles have distinct canonical presentations (true by definition of "canonical") | KR-8 | Standard algebraic-presentation result |
+| ID | Class | Status | Statement | Cited by | Where it lives |
+|----|-------|--------|-----------|----------|----------------|
+| A-KR-1.1 | DESIGN | **UNANCHORED** | Every `KRLExpr` AST variant has a matching arm in the lowering pass | KR-1 | was `KRLAdapter.jl/src/parser/lower.jl` — gone; no lowering pass exists anywhere |
+| A-KR-1.2 | DESIGN | **UNANCHORED** | The AST module defines the only AST shapes the parser produces | KR-1 | was `KRLAdapter.jl/src/parser/ast.jl` — gone. `quandledb/server/krl/Ast.jl` exists but encodes a *different* language (see below) |
+| A-KR-2.1 | DESIGN | **UNANCHORED** | Generator arity is fixed: `sigma i / sigma_inv i : in=i+1, out=i+1`; `cup i : in=0, out=2`; `cap i : in=2, out=0` | KR-2 | `spec/grammar.ebnf` only. No implementation defines these generators — `sigma`, `cup` and `cap` appear 0 times in `quandledb/server/krl/` |
+| A-KR-2.2 | MATH | holds | `arity_in(a \| b) = arity_in(a) + arity_in(b)` and same for output (monoidal-category tensor) | KR-2 | Standard categorical tangle definition |
+| A-KR-3.1 | MATH | holds | Reidemeister's theorem: R1+R2+R3 generate isotopy equivalence on tangle diagrams | KR-3 | Reidemeister 1927; Kauffman _Knots and Physics_ ch. 1 |
+| A-KR-3.2 | DESIGN | **UNANCHORED** | `r1_simplify` / `r2_simplify` / `r3_simplify` implement those moves faithfully | KR-3 | was `KRLAdapter.jl/src/operations.jl` — gone. No Reidemeister simplification exists in `quandledb/server/krl/` |
+| A-KR-4.1 | DESIGN | **UNANCHORED** | The pretty-printer's bracketing is unambiguous: `;` only inside parens; tensor `\|` has lower precedence than compose `;` inside parens | KR-4 | No pretty-printer exists in any current implementation |
+| A-KR-6.1 | DESIGN | **VOID** | Two independent parsers both target `spec/grammar.ebnf` v0.1.0 | KR-6 | Only one parser now exists (`quandledb/server/krl/Parser.jl`), and it targets `quandledb/spec/grammar.ebnf`, not this one |
+| A-KR-6.2 | DESIGN | **VOID** | Both implementations share the same `Token` enumeration | KR-6 | Only one lexer now exists (`quandledb/server/krl/Lexer.jl`); there is nothing to share with |
+| A-KR-8.1 | MATH (partial) | holds | Fundamental-quandle functor is faithful on prime alternating knots; partial in general | KR-8 | Joyce 1982; for partial cases see Eisermann _The number of knot group representations_ |
+| A-KR-8.2 | MATH | holds | Two non-isomorphic quandles have distinct canonical presentations (true by definition of "canonical") | KR-8 | Standard algebraic-presentation result |
+
+### On the UNANCHORED and VOID rows
+
+A DESIGN assumption is defined above as *"true by construction in our code
+(must remain true; flag if you change the named code)"*. Seven rows named code
+in `KRLAdapter.jl`, which no longer exists, so there is no construction left to
+be true by. They are recorded here rather than deleted, because the statements
+are still the design intent — but none of them is currently checkable, and none
+may be cited as discharged.
+
+**UNANCHORED** means the statement stands as intent but names no live code.
+**VOID** means the statement presupposes two implementations, and only one
+exists.
+
+Re-anchoring is blocked on the specification itself. `spec/grammar.ebnf` (here)
+and `quandledb/spec/grammar.ebnf` are disjoint on core vocabulary: the braid
+generators these assumptions describe appear only in the former, and only the
+latter is implemented. Until the two are reconciled and a conformance suite
+exists, these rows cannot be re-anchored to anything. See `READINESS.md`.
 
 ---
 
@@ -65,3 +84,4 @@ file with the date and reason.
 | Date | Change | By |
 |------|--------|-----|
 | 2026-06-01 | Initial registry, scoped to KRL surface obligations | Audit |
+| 2026-07-21 | Added Status column. Marked A-KR-1.1, 1.2, 2.1, 3.2 and 4.1 UNANCHORED and A-KR-6.1, 6.2 VOID: all seven named code in `KRLAdapter.jl`, which no longer exists. Verified that no replacement exists — `sigma`, `cup`, `cap`, `r1_simplify` and any pretty-printer appear 0 times in `quandledb/server/krl/`. The four MATH rows are unaffected. | Audit |

READINESS.md

@@ -7,130 +7,117 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # Component Readiness — KRL
 
 **Standard:** [CRG v2.0 STRICT](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades)
-**Current Grade:** D
-**Assessed:** 2026-04-12 (promoted E → D after iteration 2)
+**Current Grade:** E
+**Assessed:** 2026-07-21 (demoted D → E)
 **Assessor:** Jonathan D.A. Jewell
 
 ---
 
-## Grade rationale (evidence for D — promoted from E)
+## Why the grade moved D → E
 
-Grade D criterion: "Works on some inputs, test matrix present."
+The previous assessment (2026-04-12) recorded Grade D on the strength of a
+parser, AST, recursive-descent implementation and a 57-test matrix, all of
+which lived in `KRLAdapter.jl`. **That repository no longer exists** — it was
+discarded, deliberately and not recoverably.
 
-### Evidence
+None of the D evidence can be checked. Under the CRG demotion table, `D → E`
+applies when *"the scope narrows so far that the component barely does
+anything"*, which is precisely what happened: with the adapter gone, nothing in
+this repository can parse or execute a KRL program.
 
-- **Parser implemented:** `KRLAdapter.jl/src/parser/` (Julia, Option B decision 2026-04-12)
-  - `lexer.jl` — full lexer with position tracking, `KRLLexError`
-  - `ast.jl` — all AST node types (`KRLProgram`, `KRLBinding`, `KRLGenerator`,
-    `KRLCompose`, `KRLTensor`, `KRLPrefixOp`, `KRLParenExpr`, `KRLIdentifier`,
-    `KRLQuery`, `KRLFilter`, `KRLIntValue`, `KRLStrValue`, `KRLIdentValue`)
-  - `parser.jl` — recursive descent, full v0.1.0 grammar
-  - `lower.jl` — AST → TangleIR lowering with `KRLLowerError`
-- **Grammar ambiguity resolved:** `;` as sequential composition only fires
-  inside parenthesised expressions (`in_parens=true`); at statement level `;`
-  is the terminator.
-- **Test matrix:** `KRLAdapter.jl/test/parser_test.jl` — 5 testsets, 57 tests
-  - Lexer: keywords, identifiers, integers, strings, operators, punctuation,
-    comments stripped, position tracking, lex error, unterminated string
-  - Parser: 20 grammar cases including all generators, let bindings, sequential
-    compose (with parens), tensor product, prefix ops, queries with `and` chains
-  - Parser errors: missing `;`, unrecognised token, missing index, zero index
-  - Example .krl files: all 4 examples in `krl/examples/` parse without error
-  - Lowering: sigma/sigma_inv → TangleIR, compose, trefoil, mirror, let binding,
-    unbound identifier error, query → KRLQueryPlan
-- **5577 tests pass** (full KRLAdapter.jl suite including parser tests)
-
-### Grammar coverage
-
-The implemented grammar (v0.1.0):
-
-| Construct | Status |
-|-----------|--------|
-| `let` binding | ✅ |
-| `sigma`, `sigma_inv`, `cup`, `cap` generators | ✅ |
-| Sequential composition `(a ; b)` | ✅ |
-| Tensor product `a \| b` | ✅ |
-| `close`, `mirror`, `simplify`, `normalise`, `classify` | ✅ |
-| `find where` queries with `and` | ✅ |
-| Parenthesised sub-expressions | ✅ |
-| Identifier references (let-bound) | ✅ |
-| Line comments `--` | ✅ |
-| String, integer, identifier filter values | ✅ |
-
-### What is NOT yet implemented (documented gaps — D grade)
-
-- **No typechecker.** Port-arity compatibility (e.g. composing a 2-strand
-  braid with a 3-strand tangle) not verified at parse time.
-- **R2 simplification across compose() boundaries.** `simplify_ir` detects
-  R2 bigons by arc-index overlap, but `compose()` renumbers arcs so adjacent
-  sigma/sigma_inv pairs are not detected. Tracked in `KRLAdapter.jl` issues.
-- **No pretty-printer.** `KRLProgram → string` round-trip not yet implemented.
-- **No RESOLVE family.** `classify` is parsed and lowered (identity) but
-  not dispatched to the query layer.
+This is a correction to the record, not a regression in the work. The grade was
+restated rather than left standing on evidence nobody can inspect.
 
 ---
 
-## Grade E rationale (retained for history)
-
-Grade E criterion: "At least 1 test, documented failures."
-
-### Evidence (iteration 1)
-
-- Grammar drafted: `spec/grammar.ebnf`, `spec/grammar-overview.md`
-- 4 examples in `examples/`
-- Shell smoke test: `tests/smoke/grammar_smoke.sh` (16 lexical assertions)
+## Grade rationale (evidence for E)
 
----
+Grade E criterion: *"Does something slight … there is a kernel of value … at
+least one successful test case demonstrating the kernel of functionality, and
+documentation of known failures and limitations."*
 
-## Path to C (alpha-stable)
+Every item below was executed on 2026-07-21, not inferred from documentation.
 
-After D: typechecker (port-arity + generator index validity), deeper TangleIR
-compilation correctness, annotation per-directory, dogfooding by parsing 20+
-KRL programs from the knot table. Fix R2 simplification across compose()
-boundaries.
+### Evidence
 
-## Path to B (beta)
+| Artefact | Check | Result |
+|---|---|---|
+| `spec/grammar.ebnf` | 114-line EBNF, v0.1.0 | present |
+| `examples/*.krl` | 4 example programs | present |
+| `tests/smoke/grammar_smoke.sh` | lexical conformance of examples to the grammar | 20 checks, all pass |
+| `src/interface/ffi/` | `zig build test` | 3/3 pass |
+| `src/interface/ffi/` | `zig build` | produces `libkrl.a` |
+| `src/interface/Abi/` | `%foreign` declarations | 4, all covered by 11 Zig exports |
+| `tests/aspect_tests.sh` | SPDX, banned constructs, ABI/FFI correspondence | 4/4 pass |
+| `tests/e2e.sh` | full local pipeline | 4/4 pass, negative-controlled |
+
+The kernel of value is the specification plus a set of examples that provably
+conform to it at the lexical level, over a C ABI that compiles and is tested.
+
+### Known failures and limitations
+
+- **No parser, and therefore no execution.** Nothing in this repository can
+  read a `.krl` program and produce a result. `grammar_smoke.sh` is lexical
+  only and says so in its own header.
+- **The specification is contested.** `spec/grammar.ebnf` here and
+  `quandledb/spec/grammar.ebnf` both claim to be KRL v0.1.0 and are disjoint on
+  core vocabulary; `|` is bound to opposite meanings in the two. See README.
+- **No conformance suite.** There is no executable artefact that an
+  implementation can be tested against, so "conforms to the KRL spec" is not
+  currently a checkable claim.
+- **Proof obligations are unmet.** `PROOF-STATUS.md` records 0 of 8 obligations
+  proven, 2 partial.
+- **`rust-ci.yml` gates nothing** — it calls the shared Rust reusable, but this
+  repository contains no `Cargo.toml`.
 
-After C: 6+ diverse external targets (knot researchers, DSL authors,
-topology educators) write KRL programs and report back.
+---
 
-## Path to C (alpha-stable)
+## Rework needed to reach D
 
-After D: typechecker (port-arity + generator index validity), compiler
-to TangleIR via KRLAdapter.jl, deep annotation per-directory, real
-dogfooding by parsing 20+ KRL programs representing knots from the
-knot table.
+Grade D requires a matrix of tested scenarios and at least one test per claimed
+capability. Concretely:
 
-## Path to B (beta)
+1. **Reconcile the two grammars** into one normative specification, resolving
+   the `|` collision.
+2. **Write an executable conformance suite** — programs plus expected results —
+   so that spec conformance becomes testable rather than asserted.
+3. **Run that suite against `quandledb/server/krl/`**, the actual
+   implementation (3,035 lines of Julia plus 1,732 lines of tests). One passing
+   test per claimed capability is the D bar.
 
-After C: 6+ diverse external targets (knot researchers, DSL authors,
-topology educators) write KRL programs and report back.
+Until at least (1) and (2) exist, this repository specifies a language nobody
+can be shown to implement.
 
 ---
 
 ## Iteration history
 
-### Iteration 0 (X grade — 2026-04-05 initial scaffold)
-Templated from rsr-template-repo. Zero KRL-specific content.
+### Iteration 0 — X (2026-04-05)
+Templated from `rsr-template-repo`. Zero KRL-specific content.
+
+### Iteration 1 — promoted to E (2026-04-05)
+- `spec/grammar.ebnf` (v0.1.0 EBNF) and `spec/grammar-overview.md`
+- 4 `examples/` programs
+- `tests/smoke/grammar_smoke.sh` (16 lexical assertions)
 
-### Iteration 1 (promoted to E — 2026-04-05)
-- spec/grammar.ebnf (v0.1.0 EBNF)
-- spec/grammar-overview.md
-- 4 examples/ programs
-- tests/smoke/grammar_smoke.sh (16 lexical assertions, all passing)
+### Iteration 2 — promoted to D (2026-04-12) — **evidence since lost**
+Decision "Option B — Julia in `KRLAdapter.jl`"; lexer, AST, recursive-descent
+parser and lowering implemented there, with 57 dedicated parser tests. The
+repository holding all of it has since been discarded, so none of this is
+verifiable. Retained here as history, not as evidence.
 
-### Iteration 2 (promoted to D — 2026-04-12)
-- Decision: Option B — Julia in KRLAdapter.jl
-- Implemented: lexer, AST, recursive-descent parser, lowering (KRLAdapter.jl)
-- Grammar ambiguity fixed: `;` as compose only inside parentheses
-- 57 dedicated parser tests + all 4 example files parse cleanly
-- 5577 total KRLAdapter.jl tests pass
+### Iteration 3 — demoted to E (2026-07-21)
+- Grade restated against what is actually present and runnable in this tree.
+- Zig FFI shim repaired: it had never compiled (`opaque` type with fields).
+- Three vacuous or false gates repaired (`aspect_tests.sh`, `e2e.sh`).
+- False `TangleIR` lowering claims and dead `KRLAdapter.jl` references removed
+  from the README.
 
 ## Review cycle
 
-Reassess on typechecker implementation or when 20+ knot-table programs
-have been parsed successfully.
+Reassess when a conformance suite exists and has been run against
+`quandledb/server/krl/`.
 
 ---
 
-## Run `just crg-badge` to generate the shields.io badge for your README.
+Run `just crg-badge` to generate the shields.io badge for the README.