docs: de-conflate Tangle from KRL; drop two dead Jekyll Pages workflows (#78)

The tangle half of a coordinated two-repo de-conflation pass. The krl
half is hyperpolymath/krl#53 (merged) and hyperpolymath/krl#54.

## The three projects are separate

**Tangle** is a general language for knot mathematics — topological,
algebraic, geometric, logical. **QuandleDB** is a knot database. **KRL**
is QuandleDB's resolution language, developed jointly with it. They
share a subject matter, not an architecture.

Documentation here presented Tangle as the substrate of a KRL
compilation stack. That is false in both directions, and the connecting
layer does not exist:

> **`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 repos.

The relationship between the projects is left intact. What is removed is
a claimed architectural dependency that was never built.

## 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 line.
- Removed the `KRL → TangleIR → Tangle core → QuandleDB + Skein.jl`
ladder.
- Removed the `== KRL — Knot Resolution Language` section, which
restated KRL's four operations as though KRL were *this* project's
surface language.
- **Strengthened the formal core with a result rather than a claim**
(below).
- Added an explicit note that only the Lean proofs are CI-gated.

## The formal core is real — and now verified

I ran the repository's own documented oracle:

```console
$ cd proofs && lean Tangle.lean
$ echo $?
0
```

| Check | Result |
|---|---|
| `lean Tangle.lean` (pinned `leanprover/lean4:v4.14.0`) | **exit 0, no
errors** |
| `sorry` count | **0** |
| `axiom` count | **0** |
| `import` lines | **0** — self-contained, no Mathlib |
| `progress`, `preservation`, `determinism`, `type_safety`,
`infer_sound`, `infer_complete`, `infer_iff_hasType` | all present with
real proof terms |

This is worth stating precisely: an `axiom` stub compiles cleanly while
proving nothing, so *"the Lean build is green"* and *"the theorems are
proved"* are different claims in general. **Here they coincide, and that
was checked rather than assumed.** This is Tangle's strongest asset and
the README now leads with it.

## AFFIRMATION.adoc — erratum, not edit

An affirmation is a dated claim about a past state (`102499d`,
2026-06-19); amending it in place would falsify a record. So the
original text is untouched and an erratum is appended. It corrects the
*"maintainer-confirmed"* `KRL → TangleIR → VerisimCore →
Skein/QuandleDB` stack, and flags that the quotable one-line
characterisation shouldn't be quoted while it calls Tangle *"the …
TangleIR of the KRL stack"*.

It also **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 is now closed, with command and exit code recorded.

## READINESS.md — Grade C → D

Grade C means *self-validated in the home context*; the `D → C` trigger
is *"dogfood it hard in the home context."* The assessment cited
**exactly one** piece of dogfooding evidence:

> **Dogfooding:** Used internally as host for the KRL (Knot Resolution
Language) DSL

That is false — KRL is not built on Tangle. With it withdrawn, C is
unsupported. Two further corrections:

- **"CI: Clean" was false** — `main` was failing Governance and both
Jekyll workflows.
- **The test suites are not run by CI.** Eight OCaml test files exist
under `compiler/test/`, but **no workflow invokes `dune` or `cargo
test`**.

The cheapest available uplift is named explicitly: add a workflow
running `dune build && dune test`. Eight suites already exist and
nothing executes them.

## dialects/README.md

- Removed KRL from the dialect table — it was listed as a dialect that
had "graduated", and it was never a Tangle dialect.
- Replaced the dead absolute path `/var/mnt/eclipse/repos/krl` (another
machine) with the GitHub URL.
- Dropped "wire through to TangleIR" from the maturation pattern.

## Workflows — two deleted

`jekyll.yml` and `jekyll-gh-pages.yml` are GitHub's **sample** Jekyll
workflows. This repo has **no `_config.yml` and no `Gemfile`** — there
is no Jekyll site to build, so both fail on every push. `pages.yml`
(Ddraig SSG, #73) is the real one; three workflows were competing for
the same Pages deployment.

## ⚠️ Owner action — GitHub Pages is not enabled

`pages.yml` will **still** fail at the deploy step after this PR. Its
build succeeds and certifies a11y, but:

```
GET /repos/hyperpolymath/tangle/pages  ->  404 Not Found
```

which surfaces as `HttpError: Not Found / Creating Pages deployment
failed`. **The same is true of `hyperpolymath/krl`.** Pages needs
enabling with source = GitHub Actions on both. That publishes a public
site, so I've left it to you rather than doing it.

## Verified on this branch

`actionlint` 0 errors · `asciidoctor` renders `README.adoc` and
`AFFIRMATION.adoc` clean · `lean Tangle.lean` exit 0

Author: hyperpolymath

.github/workflows/governance.yml

@@ -13,4 +13,4 @@ permissions:
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e
+    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b

.github/workflows/hypatia-scan.yml

@@ -12,8 +12,11 @@ on:
 
 permissions:
   contents: read
-  security-events: read
+  # The reusable declares security-events: write (it uploads SARIF). A called
+  # workflow cannot escalate beyond the caller's grant, so `read` here makes the
+  # whole run a startup_failure with zero jobs and no log.
+  security-events: write
 
 jobs:
   scan:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e
+    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b

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

@@ -1,3 +1,5 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 name: GitHub Pages (Ddraig SSG)
 on:
   push:
@@ -18,9 +20,9 @@ jobs:
       image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff
     steps:
       - name: Checkout Site
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
       - name: Checkout Ddraig SSG
-        uses: actions/checkout@v7
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
         with:
           repository: hyperpolymath/ddraig-ssg
           path: .ddraig-ssg
@@ -37,7 +39,7 @@ jobs:
           fi
           ./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/}
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v5
+        uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5
         with:
           path: '_site'
   deploy:
@@ -50,4 +52,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v5
+        uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5

.github/workflows/jekyll.yml

@@ -13,7 +13,7 @@ permissions:
 
 jobs:
   scorecard:
-    uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e
+    uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b
     permissions:
       contents: read
       security-events: write

.github/workflows/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/scorecard.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.