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

[hyperpolymath]

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:

$ 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