docs: de-conflate KRL from Tangle, restate the readiness grade honestly (#54)

Follows #53. Same Part 1 remit: make `main` green **and honest**. This
half is the documentation de-conflation.

## The three projects are distinct

QuandleDB is the knot database. KRL is its resolution language,
developed alongside it. **Tangle is a separate project** — a general
language for knot mathematics (topological, algebraic, geometric,
logical) that happens to share the subject matter. Documentation here
had fused KRL and Tangle into a single compilation pipeline that does
not exist.

The relationship between KRL and QuandleDB is left intact — it is real
and deliberate. What is removed is the false *identity* with Tangle, not
the shared domain.

## 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.
- Removed the `TanglePL` usage example, which imports packages that
don't exist.
- Added the **known divergence**: this repo's grammar and QuandleDB's
are disjoint on core vocabulary, and `|` is bound to opposite meanings
(tensor here, pipeline there).
- A short note records that these claims were false, so the correction
is legible rather than silent.

### This also fixes the GitHub Pages failure

Root cause was **not** generic: Ddraig SSG certifies pages against a
decidable a11y predicate requiring exactly one `<h1>` and no
heading-level skips. The old README had **8** `<h1>`s:

```
+ index.md -> index.html  [a11y FAIL]
  a11y: exactly one <h1> required (found 8)
```

Verified by compiling Ddraig locally (Idris2) and running the real
certifier:

| README | Result |
|---|---|
| `origin/main` (old) | `[a11y FAIL]` — exit 1 |
| this branch | `[a11y ok]` — exit 0 |

## READINESS.md — Grade D → E

The **entire** evidence base for Grade D was a parser, AST, lowering
pass and 57-test matrix in `KRLAdapter.jl`. That repository 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 exactly what happened.

Replaced with evidence executed on 2026-07-21: grammar smoke 20/20, `zig
build test` 3/3, aspect 4/4, e2e 4/4. Limitations stated plainly,
including that **no conformance suite exists**, so "conforms to the KRL
spec" is not currently a checkable claim.

This is a correction to the record, not a regression in the work.

## ASSUMPTIONS.md

Seven DESIGN assumptions named code in `KRLAdapter.jl`. The file defines
a DESIGN assumption 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 → **UNANCHORED** (statement stands as
intent, names no live code)
- A-KR-6.1, 6.2 → **VOID** (both presuppose two implementations; 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 repo exposes **no** Groove service and has no
`.well-known/groove/manifest.json`, rather than implying one exists.

## Verified on this branch

`actionlint` 0 errors · aspect 4/4 · e2e 4/4 · smoke 20/20 · Ddraig a11y
ok

The matching de-conflation pass on `hyperpolymath/tangle` (whose README
is titled *"Tangle / KRL"*) follows separately.

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.