docs: de-conflate Tangle from KRL; drop two dead Jekyll Pages workflows

Tangle, KRL and QuandleDB are three separate projects that share a subject
matter. Documentation here presented Tangle as the substrate of a KRL
compilation stack, which is not true in either direction.

README.adoc

* Retitled from "Tangle / KRL — Topological Programming Language" to
  "Tangle — a general language for knot mathematics". Removed "Tangle (via
  KRL — Knot Resolution Language) is ..." from the opening sentence and the
  "Tangle/KRL" framing from the status and summary sections.
* Removed the architecture ladder KRL -> TangleIR -> Tangle core ->
  QuandleDB + Skein.jl. `TangleIR` appears in NO source file in this
  repository (0 hits across .rs, .zig and .lean) and in NO source file in the
  KRL implementation. It existed only in prose, in both repositories.
* Removed the "== KRL — Knot Resolution Language" section, which restated
  KRL's four operations as though KRL were this project's surface language.
  Replaced with a "Relationship to KRL and QuandleDB" section stating the
  three projects' actual boundaries. The relationship is left intact — what
  is removed is a claimed architectural dependency that does not exist.
* Strengthened the formal-core section with a result rather than a claim: the
  repository's own oracle, `cd proofs && lean Tangle.lean`, was executed on
  2026-07-21 and exits 0. The proofs are self-contained (Tangle.lean has no
  import lines, so no Mathlib) and contain 0 `sorry` and 0 `axiom` across
  2,128 lines, with progress, preservation, determinism, type_safety,
  infer_sound, infer_complete and infer_iff_hasType all carrying real proof
  terms. "Builds" and "proved" coincide here, which is not automatic.
* Added an explicit note that only the Lean proofs are CI-gated: the OCaml
  compiler, the Rust components and the Zig components are built by no
  workflow.

AFFIRMATION.adoc

* Appended an erratum rather than editing the text. An affirmation is a dated
  claim about a past state; amending it in place would falsify a record.
* Corrects the "maintainer-confirmed" stack KRL -> TangleIR -> VerisimCore ->
  Skein/QuandleDB, and flags that the quotable one-line characterisation
  should not be quoted while it describes Tangle as "the ... TangleIR of the
  KRL stack".
* Discharges one of the affirmation's own acknowledged gaps. It recorded
  "OCaml + Lean not run (absent)" and concluded "structure + the repo's proof
  records are confirmed, not a fresh green build". The Lean half of that gap
  is now closed, with the command and exit code recorded.

READINESS.md — grade C -> D

* Grade C means self-validated in the home context, and the D -> C trigger is
  "dogfood it hard in the home context". The assessment cited exactly one
  piece of dogfooding evidence: "Used internally as host for the KRL DSL".
  That is false, so C is unsupported.
* "CI: Clean" was also false — main was failing Governance and both Jekyll
  Pages workflows.
* The 8 OCaml test suites under compiler/test/ are real but are run by no
  workflow, so their passing state is unverified by this repo's own CI.
* Recorded the verified Lean result as the evidence that does hold, and named
  the cheapest uplift: add a workflow that runs `dune build && dune test`.

dialects/README.md

* Removed KRL from the dialect table. It was listed as a dialect that had
  "graduated" to its own repo; it was never a Tangle dialect.
* Replaced the dead absolute path /var/mnt/eclipse/repos/krl with the GitHub
  URL.
* Dropped "wire through to TangleIR" from the maturation pattern, and noted
  that no dialect has yet made that journey, so there is no precedent.
* Softened the multi-DSL-host claim: the sketches set out what such a host
  would cover, but nothing is implemented and nothing is built on Tangle, so
  they do not yet evidence it.

Workflows

* Deleted .github/workflows/jekyll.yml and .github/workflows/jekyll-gh-pages.yml.
  Both are GitHub's sample Jekyll workflows; this repository has no _config.yml
  and no Gemfile, so there is no Jekyll site to build and both fail on every
  push to main. pages.yml (Ddraig SSG, landed in #73) is the real one, and
  three workflows were competing for the same Pages deployment.

NOTE: pages.yml will still fail at the deploy step. Its build succeeds and
certifies a11y, but GitHub Pages is not enabled for this repository —
/repos/hyperpolymath/tangle/pages returns 404, which surfaces as
"HttpError: Not Found / Creating Pages deployment failed". That is a repository
setting, not a code change, and is left for the owner.

Author: hyperpolymath

.github/workflows/jekyll-gh-pages.yml

@@ -220,3 +220,67 @@ un-run toolchains stated rather than implied.
   `-S`; the signed git commit over this content, at the SHA above, is the
   authoritative form.
 * *Signed-off-date:* (fill on signing)
+
+'''
+
+== Erratum — 2026-07-21
+
+This section corrects the affirmation above. The original text is left intact:
+an affirmation is a dated claim about a past state, and amending it in place
+would falsify a record. Two of its claims have since been shown to be wrong,
+and one of its acknowledged gaps has since been closed.
+
+=== Correction 1 — the stack does not exist
+
+The affirmation records, as *maintainer-confirmed*, the ladder:
+
+[literal]
+KRL -> TangleIR -> VerisimCore -> Skein/QuandleDB
+
+`TangleIR` does not exist. The identifier appears in *no source file* in this
+repository (0 hits across `.rs`, `.zig` and `.lean`) and in *no source file* in
+the KRL implementation at `quandledb/server/krl/`. It existed only in prose, in
+both repositories, and has been removed from `README.adoc`.
+
+Nor is KRL a surface language for Tangle. KRL is QuandleDB's resolution
+language, developed jointly with QuandleDB; it neither compiles to nor depends
+on Tangle. The three projects share a subject matter, not an architecture.
+
+The confirmation recorded on 2026-06-19 was a confirmation of the README's
+diagram, and that diagram was wrong. Nothing here suggests bad faith — the
+affirmation is careful, and states plainly which of its checks were not run.
+
+=== Correction 2 — the "one-line characterisation" should not be quoted as-is
+
+The characterisation invites quotation. It should not be quoted while it
+describes Tangle as "the proven type-safe small-step core + TangleIR of the KRL
+stack". Everything else in that sentence survives: the OCaml compiler, the Rust
+LSP/WASM targets, the Lean 4 proofs and the five dialects are all real.
+
+=== Discharge — the Lean proofs have now been run
+
+The affirmation states: *"OCaml + Lean not run (absent)"*, and concludes that
+*"structure + the repo's proof records are confirmed, not a fresh green build"*.
+
+That gap is now closed for Lean. On 2026-07-21 the repository's own documented
+oracle was executed:
+
+[source,console]
+----
+$ cd proofs && lean Tangle.lean
+$ echo $?
+0
+----
+
+Exit 0, no errors, using the pinned toolchain from `proofs/lean-toolchain`
+(`leanprover/lean4:v4.14.0`). The proofs are self-contained — `Tangle.lean` has
+no `import` lines at all, so no Mathlib — and contain *zero* occurrences of
+`sorry` and *zero* `axiom` declarations across 2,128 lines. `progress`,
+`preservation`, `determinism`, `type_safety`, `infer_sound`, `infer_complete`
+and `infer_iff_hasType` are all present with real proof terms.
+
+This matters because "the Lean build is green" and "the theorems are proved" are
+not the same claim in general: an `axiom` stub compiles cleanly while proving
+nothing. Here they coincide, and that was checked rather than assumed.
+
+The OCaml compiler remains unbuilt — no workflow in this repository builds it.

.github/workflows/jekyll.yml

@@ -6,45 +6,116 @@ Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 # Component Readiness — Tangle (language)
 
-**Current Grade:** C
-**Assessed:** 2026-04-05
+**Current Grade:** D
+**Assessed:** 2026-07-21 (demoted C → D)
 **Standard:** [CRG v2.0 STRICT](../standards/component-readiness-grades/)
 
-## Grade rationale (evidence for C)
+## Why the grade moved C → D
 
-Works reliably on own project + annotated. Tangle is a Turing-complete
-topological programming language with a compiler, LSP, and wasm backend.
+Grade C means *self-validated in the home context*; the D → C promotion trigger
+is *"dogfood it hard in the home context."* The previous assessment cited
+exactly one piece of dogfooding evidence:
 
-### Evidence
+> **Dogfooding:** Used internally as host for the KRL (Knot Resolution Language) DSL
 
-- **Tests:** 6 dune test suites (parser, typecheck, eval, e2e, property, compositional)
-- **Annotation:** 8 per-directory READMEs across compiler/, lib/, examples/, docs/
-- **Dogfooding:** Used internally as host for the KRL (Knot Resolution Language) DSL
-- **RSR compliance:** 0-AI-MANIFEST.a2ml, `.machine_readable/6a2/`, 14+ workflows, SECURITY/CONTRIBUTING/CODE_OF_CONDUCT, EXPLAINME.adoc, TEST-NEEDS.md, PROOF-NEEDS.md
-- **Formal proofs:** Lean 4 proofs for progress, preservation, determinism
-- **WASM backend:** Compositional PD compiler with wasm codegen
-- **CI:** Clean; panic-attack assail 0 findings
+**That is not true.** KRL is not built on Tangle. KRL is QuandleDB's resolution
+language, developed jointly with QuandleDB; it neither compiles to nor depends
+on Tangle, and the `TangleIR` layer that was supposed to connect them does not
+exist in any source file in either repository. See the erratum in
+`AFFIRMATION.adoc`.
+
+With that claim withdrawn there is no dogfooding evidence, so C is not
+supported. Two further corrections to the previous assessment:
+
+- **"CI: Clean" was false.** At the time of this assessment `main` was failing
+  Governance and both Jekyll Pages workflows.
+- **The test suites are not run by CI.** Eight OCaml test files exist under
+  `compiler/test/`, but no workflow in this repository invokes `dune` or
+  `cargo test`. Their passing state is unverified by this repository's own CI.
+
+This is a correction to the record, not a regression in the work. The formal
+core in particular got *stronger* this cycle — see below.
+
+---
+
+## Grade rationale (evidence for D)
+
+Grade D: *"works on some inputs, some cases, or some configurations, but not
+systematically … either needs to be narrowed in scope so that its documented
+capabilities match its actual capabilities, or needs the inconsistencies
+fixed."* Narrowing the documented scope is exactly what this revision does.
+
+### Verified evidence
+
+| Artefact | Check | Result |
+|---|---|---|
+| `proofs/Tangle.lean` | `cd proofs && lean Tangle.lean` (the repo's own documented oracle) | **exit 0, no errors** |
+| `proofs/Tangle.lean` | `sorry` count | **0** |
+| `proofs/Tangle.lean` | `axiom` count | **0** |
+| Theorems | `progress`, `preservation`, `determinism`, `type_safety`, `infer_sound`, `infer_complete`, `infer_iff_hasType` | all present with real proof terms |
+| Dependencies | `import` lines in `Tangle.lean` | **0** — self-contained, no Mathlib |
+
+Run on 2026-07-21 with the pinned toolchain (`leanprover/lean4:v4.14.0`). This
+is worth stating precisely: a Lean file full of `axiom` stubs compiles cleanly
+while proving nothing, so "the build is green" and "the theorems are proved" are
+different claims. Here they coincide, and that was checked.
+
+### Present but unverified
+
+- **OCaml compiler** (`compiler/`) — lexer, parser, AST, typechecker, evaluator,
+  pretty-printer, REPL, braid equivalence, LSP and WASM targets. Not built by
+  any workflow.
+- **Test suites** — 8 files under `compiler/test/` (`test_parser`,
+  `test_typecheck`, `test_eval`, `test_e2e`, `test_property`,
+  `test_compositional`, `test_check`, `test_roundtrip`) plus `tg3`/`tg5`/`tg7`/
+  `tg8` directories. Not run by any workflow.
+- **Rust / Zig components** — 18 `.rs`, 3 `.zig`. Not built by any workflow.
+- **Five dialects** — grammar sketches only.
+
+### Structural evidence
+
+- Per-directory README annotation across `compiler/`, `dialects/`, `docs/`.
+- RSR compliance: `0-AI-MANIFEST.a2ml`, `.machine_readable/6a2/`, workflows,
+  SECURITY / CONTRIBUTING / CODE_OF_CONDUCT, `EXPLAINME.adoc`, `TEST-NEEDS.md`,
+  `PROOF-NEEDS.md`.
+
+---
 
 ## Gaps preventing higher grades
 
+### Blocks C (self-validated in the home context)
+
+1. **No CI gate on the implementation.** The OCaml compiler, its 8 test suites,
+   and the Rust and Zig components are not built or run by any workflow. Until
+   they are, "works reliably" is not an evidenced claim. This is the single
+   highest-value fix available to this repository.
+2. **No dogfooding.** Nothing is currently built on Tangle. The previous claim
+   to the contrary was false.
+
 ### Blocks B (6+ diverse external targets)
+
 - No external language users outside hyperpolymath.
-- KRL is the only DSL built on Tangle so far — need 5 more distinct domain DSLs
-  to demonstrate the host-language claim.
 - No external submissions to language research venues confirming the phase
   separation or compositional PD model.
 
 ### Blocks A
+
 - Requires B first.
 
-## What to do for B
+---
+
+## What to do next
 
-1. Build 5 more DSLs on top of Tangle (not just KRL) — e.g. a braid-group
-   calculus, a category-theory calculus, a quantum-circuit calculus.
-2. Get external feedback on the surface syntax and compiler from language
-   researchers.
-3. Track the 6 targets here.
+1. **Add a workflow that runs `dune build && dune test`.** Eight test suites
+   already exist; nothing executes them. This is the cheapest available uplift
+   and is a precondition for any claim above D.
+2. Add a workflow that builds the Rust and Zig components.
+3. Build something real on Tangle, in its own right — a braid-group calculus, a
+   category-theory calculus, a quantum-circuit calculus. The five dialects are
+   the natural candidates and currently exist only as grammar sketches.
+   Note that this must be genuine dogfooding of *Tangle*; KRL does not count and
+   never did.
 
 ## Review cycle
 
-Reassess per release. Next review: on any compiler/LSP/wasm behavioural change.
+Reassess when the compiler is built and its tests are run by CI.