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

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

AFFIRMATION.adoc

@@ -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.

READINESS.md

@@ -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.