diff --git a/ASSUMPTIONS.adoc b/ASSUMPTIONS.adoc
new file mode 100644
index 0000000..b234f00
--- /dev/null
+++ b/ASSUMPTIONS.adoc
@@ -0,0 +1,182 @@
+== Assumptions Registry — QuandleDB
+
+Every load-bearing *unproven* assumption used in this repo, with an ID,
+classification, and the obligation it supports.
+
+Classifications: - *MATH* — true by an external mathematical theorem
+(cite it) - *DESIGN* — true by construction in our code (must remain
+true; flag if you change the named code) - *EMPIRICAL* — believed from
+testing; not formally verified - *CRYPTO* — standard
+cryptographic-primitive assumption
+
+Cross-references use `+[[A-QD-N.M]]+` syntax, resolved here.
+
+'''''
+
+=== Presentation extraction (QD-1, QD-9, QD-10, QD-11)
+
+[width="100%",cols="11%,14%,22%,20%,33%",options="header",]
+|===
+|ID |Class |Statement |Cited by |Where it lives
+|A-QD-1.1 |DESIGN |PD codes are well-formed: each crossing has exactly 4
+arcs in PD-positions `+(a, b, c, d)+` |QD-1
+|`+KnotTheory.PlanarDiagram+` struct contract
+
+|A-QD-1.2 |DESIGN |Connectedness (or per-component handling) is checked
+by the caller; `+extract_presentation+` does not validate |QD-1
+|`+server/quandle_semantic.jl::extract_presentation+`
+
+|A-QD-9.1 |MATH |Path compression in union-find preserves equivalence
+classes |QD-9 |Tarjan 1975
+
+|A-QD-9.2 |DESIGN |Iteration order of `+pd.crossings+` (a
+`+Vector{Crossing}+`) is deterministic at the Julia level |QD-9 |Julia
+language guarantee
+
+|A-QD-10.1 |DESIGN |`+spec/grammar.ebnf+` v0.1.0 (in KRL repo) is
+unambiguous |QD-10 |`+hyperpolymath/krl/spec/grammar.ebnf+`
+
+|A-QD-10.2 |DESIGN |Grammar references in KRL repo and
+quandledb/server/krl/ are kept in lock-step (currently manual; CI gate
+is owed) |QD-10 |Both Parser.jl files
+
+|A-QD-11.1 |DESIGN |The SQL subset supported by `+SqlFrontend.jl+` is
+well-defined: no joins, no subqueries, equality + comparison filters
+only |QD-11 |`+server/krl/SqlFrontend.jl+`
+
+|A-QD-11.2 |MATH (effective) |`+KnotTheory.jl+`’s notion of
+`+crossing_number+`, `+writhe+`, `+genus+` is stable across
+implementations (standard knot-theoretic definitions) |QD-11
+|KnotTheory.jl upstream
+|===
+
+=== Canonical form and fingerprinting (QD-3, QD-4, QD-7, QD-8)
+
+[width="100%",cols="11%,14%,22%,20%,33%",options="header",]
+|===
+|ID |Class |Statement |Cited by |Where it lives
+|A-QD-3.1 |MATH |The number of quandle homomorphisms from a quandle
+`+Q+` to a fixed finite quandle `+T+` is a class invariant of `+Q+`
+|QD-3 |Joyce 1982; standard algebraic result
+
+|A-QD-3.2 |DESIGN |`+_dihedral_colouring_count+`’s matrix `+M+`
+correctly encodes the dihedral relations: row for relation `+(a, b, c)+`
+(positive) is `+M[i, a] += 1; M[i, c] += 1; M[i, b] -= 2+` mod `+p+`
+|QD-3 |`+server/quandle_semantic.jl:253-270+`
+
+|A-QD-4.1 |CRYPTO |BLAKE3 produces identical output for identical input
+bytes |QD-4 |BLAKE3 specification
+
+|A-QD-4.2 |MATH |Julia’s `+string(...)+` interpolation of `+Int+` is
+identical across platforms (base-10 ASCII, no locale dependence) |QD-4
+|Julia language guarantee
+
+|A-QD-4.3 |DESIGN
+|`+sort(...; by = r -> (r.lhs, r.rhs, r.out, r.is_inverse ? 1 : 0))+` is
+stable and order-preserving across Julia implementations |QD-4 |Julia
+`+Base.sort+` contract
+
+|A-QD-7.1 |DESIGN |No relation field outside
+`+(lhs, rhs, out, is_inverse)+` affects quandle equality (the
+`+QuandleRelation+` struct has only these four fields) |QD-7
+|`+server/quandle_semantic.jl::QuandleRelation+`
+
+|A-QD-8.1 |DESIGN |`+_rank_mod_p!+` correctly computes matrix rank over
+`+Z_p+` for prime `+p+` |QD-8 |`+server/quandle_semantic.jl:207-251+`
+
+|A-QD-8.2 |MATH |For a homogeneous linear system over `+Z_p+` (prime)
+with `+g+` unknowns and rank `+r+`, the solution count is `+p^(g - r)+`
+|QD-8 |Standard linear algebra
+|===
+
+=== Reidemeister invariance (QD-2, QD-12)
+
+[width="100%",cols="11%,14%,22%,20%,33%",options="header",]
+|===
+|ID |Class |Statement |Cited by |Where it lives
+|A-QD-2.1 |MATH |R1 + R2 + R3 generate isotopy on classical knot
+diagrams (Reidemeister 1927) |QD-2, QD-3 |Standard
+
+|A-QD-2.2 |MATH |R3 acts on the fundamental quandle as a permutation of
+generators, leaving the quandle isomorphism class invariant |QD-2
+|Standard quandle-theoretic result
+
+|A-QD-12.1 |DESIGN |All Skein.jl mutating operations are identifiable by
+name suffix (e.g. `+store!+`, `+delete!+`, `+update!+` — Julia
+convention) |QD-12 |Skein.jl upstream + Julia convention
+|===
+
+=== FFI / ABI (QD-5, QD-6)
+
+[width="100%",cols="11%,14%,22%,20%,33%",options="header",]
+|===
+|ID |Class |Statement |Cited by |Where it lives
+|A-QD-5.1 |DESIGN |Idris2’s `+HasSize+` / `+HasAlignment+` instances are
+correct for the platforms targeted |QD-5 |Idris2 stdlib + per-platform
+overrides
+
+|A-QD-5.2 |DESIGN |Zig’s `+extern struct+` layout is C-ABI compatible
+(no field reordering, padding per platform) |QD-5 |Zig language
+guarantee
+
+|A-QD-6.1 |DESIGN |Zig’s safety guarantees (no UB on well-typed code in
+Release-Safe) hold for the NIF code paths in
+`+beam/native/quandle_db_nif.zig+` |QD-6 |Zig language guarantee + audit
+of the file
+
+|A-QD-6.2 |DESIGN |Elixir-side input types are validated by Dialyzer
+typespecs before the NIF call |QD-6
+|`+beam/lib/quandle_db_nif/native.ex+` typespecs
+|===
+
+=== Cryptographic primitives
+
+[width="100%",cols="13%,17%,28%,25%,17%",options="header",]
+|===
+|ID |Class |Statement |Cited by |Notes
+|A-QD-4.1 |CRYPTO |BLAKE3 produces identical output for identical input
+bytes |QD-4 |(see above)
+
+|_(implicit)_ |CRYPTO |SHA-256 collision resistance (used as backup
+digest in `+quandle_descriptor+`) |QD-4 (extended) |Standard
+|===
+
+'''''
+
+=== How to use this file
+
+* *Reading code.* When you see a function whose correctness depends on
+something not enforced by the local types — _that’s an assumption_. Find
+or add the entry here and reference it by ID.
+* *Writing a proof.* Every proof obligation in PROOF-NARRATIVE.md names
+its assumptions by ID. Before discharging the proof, audit the
+assumptions.
+* *Modifying load-bearing code.* Each DESIGN assumption names a
+file/component. If you edit that file, re-validate the assumption (or
+update the obligation if the design changed intentionally).
+
+=== Promoting / demoting assumptions
+
+[cols=",,",options="header",]
+|===
+|From |To |Trigger
+|EMPIRICAL → MATH |discharge with a citation |
+|EMPIRICAL → DESIGN |refactor to make it a structural invariant |
+|MATH → (delete) |obligation has been re-cast not to need it |
+|DESIGN → MATH (rare) |the design encodes a known theorem |
+|any → CRYPTO |only for cryptographic primitives |
+|===
+
+When you change a row, leave a one-line note in the changelog with the
+date and reason.
+
+'''''
+
+=== Changelog
+
+[width="100%",cols="32%,42%,26%",options="header",]
+|===
+|Date |Change |By
+|2026-06-01 |Initial registry, scoped to QuandleDB obligations
+QD-1..QD-12 |Audit
+|===
diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md
deleted file mode 100644
index 9c9fa22..0000000
--- a/ASSUMPTIONS.md
+++ /dev/null
@@ -1,103 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
-# Assumptions Registry — QuandleDB
-
-Every load-bearing **unproven** assumption used in this repo, with an
-ID, classification, and the obligation it supports.
-
-Classifications:
-- **MATH** — true by an external mathematical theorem (cite it)
-- **DESIGN** — true by construction in our code (must remain true; flag if you change the named code)
-- **EMPIRICAL** — believed from testing; not formally verified
-- **CRYPTO** — standard cryptographic-primitive assumption
-
-Cross-references use `[[A-QD-N.M]]` syntax, resolved here.
-
----
-
-## Presentation extraction (QD-1, QD-9, QD-10, QD-11)
-
-| ID | Class | Statement | Cited by | Where it lives |
-|----|-------|-----------|----------|----------------|
-| A-QD-1.1 | DESIGN | PD codes are well-formed: each crossing has exactly 4 arcs in PD-positions `(a, b, c, d)` | QD-1 | `KnotTheory.PlanarDiagram` struct contract |
-| A-QD-1.2 | DESIGN | Connectedness (or per-component handling) is checked by the caller; `extract_presentation` does not validate | QD-1 | `server/quandle_semantic.jl::extract_presentation` |
-| A-QD-9.1 | MATH | Path compression in union-find preserves equivalence classes | QD-9 | Tarjan 1975 |
-| A-QD-9.2 | DESIGN | Iteration order of `pd.crossings` (a `Vector{Crossing}`) is deterministic at the Julia level | QD-9 | Julia language guarantee |
-| A-QD-10.1 | DESIGN | `spec/grammar.ebnf` v0.1.0 (in KRL repo) is unambiguous | QD-10 | `hyperpolymath/krl/spec/grammar.ebnf` |
-| A-QD-10.2 | DESIGN | Grammar references in KRL repo and quandledb/server/krl/ are kept in lock-step (currently manual; CI gate is owed) | QD-10 | Both Parser.jl files |
-| A-QD-11.1 | DESIGN | The SQL subset supported by `SqlFrontend.jl` is well-defined: no joins, no subqueries, equality + comparison filters only | QD-11 | `server/krl/SqlFrontend.jl` |
-| A-QD-11.2 | MATH (effective) | `KnotTheory.jl`'s notion of `crossing_number`, `writhe`, `genus` is stable across implementations (standard knot-theoretic definitions) | QD-11 | KnotTheory.jl upstream |
-
-## Canonical form and fingerprinting (QD-3, QD-4, QD-7, QD-8)
-
-| ID | Class | Statement | Cited by | Where it lives |
-|----|-------|-----------|----------|----------------|
-| A-QD-3.1 | MATH | The number of quandle homomorphisms from a quandle `Q` to a fixed finite quandle `T` is a class invariant of `Q` | QD-3 | Joyce 1982; standard algebraic result |
-| A-QD-3.2 | DESIGN | `_dihedral_colouring_count`'s matrix `M` correctly encodes the dihedral relations: row for relation `(a, b, c)` (positive) is `M[i, a] += 1; M[i, c] += 1; M[i, b] -= 2` mod `p` | QD-3 | `server/quandle_semantic.jl:253-270` |
-| A-QD-4.1 | CRYPTO | BLAKE3 produces identical output for identical input bytes | QD-4 | BLAKE3 specification |
-| A-QD-4.2 | MATH | Julia's `string(...)` interpolation of `Int` is identical across platforms (base-10 ASCII, no locale dependence) | QD-4 | Julia language guarantee |
-| A-QD-4.3 | DESIGN | `sort(...; by = r -> (r.lhs, r.rhs, r.out, r.is_inverse ? 1 : 0))` is stable and order-preserving across Julia implementations | QD-4 | Julia `Base.sort` contract |
-| A-QD-7.1 | DESIGN | No relation field outside `(lhs, rhs, out, is_inverse)` affects quandle equality (the `QuandleRelation` struct has only these four fields) | QD-7 | `server/quandle_semantic.jl::QuandleRelation` |
-| A-QD-8.1 | DESIGN | `_rank_mod_p!` correctly computes matrix rank over `Z_p` for prime `p` | QD-8 | `server/quandle_semantic.jl:207-251` |
-| A-QD-8.2 | MATH | For a homogeneous linear system over `Z_p` (prime) with `g` unknowns and rank `r`, the solution count is `p^(g - r)` | QD-8 | Standard linear algebra |
-
-## Reidemeister invariance (QD-2, QD-12)
-
-| ID | Class | Statement | Cited by | Where it lives |
-|----|-------|-----------|----------|----------------|
-| A-QD-2.1 | MATH | R1 + R2 + R3 generate isotopy on classical knot diagrams (Reidemeister 1927) | QD-2, QD-3 | Standard |
-| A-QD-2.2 | MATH | R3 acts on the fundamental quandle as a permutation of generators, leaving the quandle isomorphism class invariant | QD-2 | Standard quandle-theoretic result |
-| A-QD-12.1 | DESIGN | All Skein.jl mutating operations are identifiable by name suffix (e.g. `store!`, `delete!`, `update!` — Julia convention) | QD-12 | Skein.jl upstream + Julia convention |
-
-## FFI / ABI (QD-5, QD-6)
-
-| ID | Class | Statement | Cited by | Where it lives |
-|----|-------|-----------|----------|----------------|
-| A-QD-5.1 | DESIGN | Idris2's `HasSize` / `HasAlignment` instances are correct for the platforms targeted | QD-5 | Idris2 stdlib + per-platform overrides |
-| A-QD-5.2 | DESIGN | Zig's `extern struct` layout is C-ABI compatible (no field reordering, padding per platform) | QD-5 | Zig language guarantee |
-| A-QD-6.1 | DESIGN | Zig's safety guarantees (no UB on well-typed code in Release-Safe) hold for the NIF code paths in `beam/native/quandle_db_nif.zig` | QD-6 | Zig language guarantee + audit of the file |
-| A-QD-6.2 | DESIGN | Elixir-side input types are validated by Dialyzer typespecs before the NIF call | QD-6 | `beam/lib/quandle_db_nif/native.ex` typespecs |
-
-## Cryptographic primitives
-
-| ID | Class | Statement | Cited by | Notes |
-|----|-------|-----------|----------|-------|
-| A-QD-4.1 | CRYPTO | BLAKE3 produces identical output for identical input bytes | QD-4 | (see above) |
-| _(implicit)_ | CRYPTO | SHA-256 collision resistance (used as backup digest in `quandle_descriptor`) | QD-4 (extended) | Standard |
-
----
-
-## How to use this file
-
-- **Reading code.** When you see a function whose correctness depends
-  on something not enforced by the local types — _that's an
-  assumption_. Find or add the entry here and reference it by ID.
-- **Writing a proof.** Every proof obligation in
-  [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md) names its assumptions by ID.
-  Before discharging the proof, audit the assumptions.
-- **Modifying load-bearing code.** Each DESIGN assumption names a
-  file/component. If you edit that file, re-validate the assumption
-  (or update the obligation if the design changed intentionally).
-
-## Promoting / demoting assumptions
-
-| From | To | Trigger |
-|------|-----|---------|
-| EMPIRICAL → MATH | discharge with a citation |
-| EMPIRICAL → DESIGN | refactor to make it a structural invariant |
-| MATH → (delete) | obligation has been re-cast not to need it |
-| DESIGN → MATH (rare) | the design encodes a known theorem |
-| any → CRYPTO | only for cryptographic primitives |
-
-When you change a row, leave a one-line note in the changelog with the
-date and reason.
-
----
-
-## Changelog
-
-| Date | Change | By |
-|------|--------|-----|
-| 2026-06-01 | Initial registry, scoped to QuandleDB obligations QD-1..QD-12 | Audit |
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
new file mode 100644
index 0000000..f219008
--- /dev/null
+++ b/CHANGELOG.adoc
@@ -0,0 +1,51 @@
+== Changelog — QuandleDB
+
+All notable changes to this project will be documented in this file.
+
+The format is based on https://keepachangelog.com/en/1.1.0/[Keep a
+Changelog].
+
+=== [Unreleased]
+
+==== Added
+
+* EXPLAINME.adoc: honest scope, invariants, boundaries, polyglot stack
+map
+* TEST-NEEDS.md: 21 assertions today, gaps documented per test category
+* PROOF-NEEDS.md: 4 mathematical obligations (quandle axioms,
+Reidemeister invariance, canonicalisation idempotence, colouring
+well-definedness)
+** 3 systems obligations (cross-platform determinism, ABI-FFI layout,
+NIF safety)
+* CRG v2 READINESS.md (grade D)
+
+==== Changed
+
+* Absorbed into `+nextgen-databases/+` monorepo (removed nested .git
+dir)
+* KRL → renamed reference to align with KRL stack naming
+
+=== [Absorbed into monorepo] 2026-04-05
+
+Previously lived as a nested git repo under nextgen-databases/.
+Flattened into the parent monorepo per the "`no .git dirs in monorepo
+subdirs`" rule. History preserved in the absorption commit message.
+
+==== Included in absorption
+
+* `+server/serve.jl+`: HTTP server with quandle_semantic_index SQLite
+sidecar
+* `+server/quandle_semantic.jl+`: QuandleSemantic module — presentation
+extraction, canonicalisation, descriptor hashing (SHA-256)
+* `+src/abi/Types.idr+`: Idris2 ABI type layer
+* `+src/ffi/semantic_ffi.zig+`: Zig FFI layer
+* `+src/api/*.v+`: zig API triples
+* `+beam/+`: Elixir BEAM client with NIFs
+
+==== Prior history (pre-absorption)
+
+* fix: replace Obj.magic with typed Fetch API bindings in Api.res
+* chore: batch RSR compliance
+* docs: KRL safety model — two-tier architecture with TypeLL levels
+* feat: KRL resolution language design — SQL compat + dependent type
+variants
diff --git a/CHANGELOG.md b/CHANGELOG.md
deleted file mode 100644
index 6be0ef6..0000000
--- a/CHANGELOG.md
+++ /dev/null
@@ -1,44 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
-
-# Changelog — QuandleDB
-
-All notable changes to this project will be documented in this file.
-
-The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
-
-## [Unreleased]
-
-### Added
-- EXPLAINME.adoc: honest scope, invariants, boundaries, polyglot stack map
-- TEST-NEEDS.md: 21 assertions today, gaps documented per test category
-- PROOF-NEEDS.md: 4 mathematical obligations (quandle axioms, Reidemeister
-  invariance, canonicalisation idempotence, colouring well-definedness)
-  + 3 systems obligations (cross-platform determinism, ABI-FFI layout,
-  NIF safety)
-- CRG v2 READINESS.md (grade D)
-
-### Changed
-- Absorbed into `nextgen-databases/` monorepo (removed nested .git dir)
-- KRL → renamed reference to align with KRL stack naming
-
-## [Absorbed into monorepo] 2026-04-05
-
-Previously lived as a nested git repo under nextgen-databases/. Flattened
-into the parent monorepo per the "no .git dirs in monorepo subdirs" rule.
-History preserved in the absorption commit message.
-
-### Included in absorption
-- `server/serve.jl`: HTTP server with quandle_semantic_index SQLite sidecar
-- `server/quandle_semantic.jl`: QuandleSemantic module — presentation
-  extraction, canonicalisation, descriptor hashing (SHA-256)
-- `src/abi/Types.idr`: Idris2 ABI type layer
-- `src/ffi/semantic_ffi.zig`: Zig FFI layer
-- `src/api/*.v`: zig API triples
-- `beam/`: Elixir BEAM client with NIFs
-
-### Prior history (pre-absorption)
-- fix: replace Obj.magic with typed Fetch API bindings in Api.res
-- chore: batch RSR compliance
-- docs: KRL safety model — two-tier architecture with TypeLL levels
-- feat: KRL resolution language design — SQL compat + dependent type variants
diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc
new file mode 100644
index 0000000..8ec13e1
--- /dev/null
+++ b/CODE_OF_CONDUCT.adoc
@@ -0,0 +1,339 @@
+== Code of Conduct
+
+=== Our Pledge
+
+We as members, contributors, and leaders pledge to make participation in
+QuandleDB a harassment-free experience for everyone, regardless of age,
+body size, visible or invisible disability, ethnicity, sex
+characteristics, gender identity and expression, level of experience,
+education, socio-economic status, nationality, personal appearance,
+race, caste, colour, religion, or sexual identity and orientation.
+
+We pledge to act and interact in ways that contribute to an open,
+welcoming, diverse, inclusive, and healthy community.
+
+We recognise that a thriving open source community requires
+*psychological safety* — an environment where people can contribute, ask
+questions, make mistakes, and learn without fear of ridicule or
+retaliation.
+
+'''''
+
+=== Our Standards
+
+==== Expected Behaviour
+
+The following behaviours contribute to a positive environment:
+
+*Communication* - Using welcoming and inclusive language - Being
+respectful of differing viewpoints and experiences - Giving and
+gracefully accepting constructive feedback - Assuming good intent while
+addressing impact - Communicating clearly and patiently, especially with
+newcomers
+
+*Collaboration* - Focusing on what is best for the community - Showing
+empathy and kindness toward other community members - Being
+collaborative rather than competitive - Mentoring and supporting less
+experienced contributors - Celebrating others’ contributions and
+successes
+
+*Professionalism* - Accepting responsibility and apologising to those
+affected by our mistakes - Learning from the experience and avoiding
+repetition - Respecting others’ time and attention - Staying on topic in
+project spaces - Following project guidelines and conventions
+
+*Accessibility* - Using plain language and avoiding unnecessary jargon -
+Providing alt text for images and transcripts for audio/video - Being
+patient with those using assistive technologies - Accommodating
+different communication styles and needs - Recognising that not everyone
+communicates the same way
+
+==== Unacceptable Behaviour
+
+The following behaviours are considered harassment and are unacceptable:
+
+*Harassment* - The use of sexualised language or imagery, and sexual
+attention or advances of any kind - Trolling, insulting or derogatory
+comments, and personal or political attacks - Public or private
+harassment - Deliberate intimidation, stalking, or following (online or
+in-person) - Unwelcome physical contact or simulated physical contact
+(e.g., emoji) - Sustained disruption of talks, events, or online
+discussions
+
+*Discrimination* - Discriminatory jokes and language - Posting or
+threatening to post others’ personally identifying information
+("`doxing`") - Advocating for, or encouraging, any of the above
+behaviour - Microaggressions — subtle, often unintentional,
+discriminatory comments or actions
+
+*Professional Misconduct* - Publishing others’ private information
+without explicit permission - Misrepresenting affiliation or
+contributions - Plagiarism or claiming credit for others’ work -
+Retaliating against anyone who reports a Code of Conduct violation -
+Other conduct which could reasonably be considered inappropriate in a
+professional setting
+
+==== Grey Areas
+
+Some situations require judgement. When uncertain:
+
+* *Intent vs Impact*: Good intentions do not excuse harmful impact.
+Focus on making things right.
+* *Power Dynamics*: Those with more power (maintainers, employers,
+experienced contributors) must be especially mindful of their impact.
+* *Cultural Differences*: What’s acceptable varies by culture. When in
+doubt, err on the side of caution and ask.
+* *Humour*: Jokes at others’ expense are rarely funny to everyone. Punch
+up, not down.
+
+'''''
+
+=== Scope
+
+This Code of Conduct applies within all community spaces, including:
+
+*Online Spaces* - Repository discussions, issues, and pull/merge
+requests - Project chat channels (Matrix, Discord, Slack, IRC) - Mailing
+lists and forums - Social media when representing the project - Video
+calls and virtual meetings
+
+*In-Person Spaces* - Conferences, meetups, and events - Workshops and
+training sessions - Any gathering where you represent the project
+
+*Representation* This Code of Conduct also applies when an individual is
+officially representing the community in public spaces. Examples
+include:
+
+* Using an official project email address
+* Posting via an official social media account
+* Acting as an appointed representative at an event
+* Speaking on behalf of the project
+
+'''''
+
+=== Enforcement
+
+==== Reporting
+
+If you experience or witness unacceptable behaviour, or have any other
+concerns, please report it as soon as possible.
+
+*How to Report*
+
+[width="99%",cols="30%,33%,37%",options="header",]
+|===
+|Method |Details |Best For
+|*Email* |j.d.a.jewell@open.ac.uk |Detailed reports, sensitive matters
+
+|*Private Message* |Contact any maintainer directly |Quick questions,
+minor issues
+
+|*Anonymous Form* |[Link to form if available] |When you need anonymity
+|===
+
+*What to Include*
+
+* Your contact information (unless anonymous)
+* Names/usernames of those involved
+* Description of what happened
+* When and where it occurred
+* Any witnesses
+* Any supporting evidence (screenshots, links)
+* How you would like us to respond (if you have a preference)
+
+*What Happens Next*
+
+[arabic]
+. You will receive acknowledgment within *5 working days*
+. The conduct team will review the report
+. We may ask for additional information
+. We will determine appropriate action
+. We will inform you of the outcome (respecting others’ privacy)
+
+==== Confidentiality
+
+All reports will be handled with discretion:
+
+* Reporter identity is protected by default
+* Details are shared only with those who need to know
+* We will ask before naming you in any communication
+* Anonymous reports are accepted and investigated
+
+==== Conflicts of Interest
+
+If a conduct team member is involved in an incident:
+
+* They will recuse themselves from the process
+* Another maintainer or external party will handle the report
+* We will disclose any potential conflicts
+
+'''''
+
+=== Enforcement Guidelines
+
+The conduct team will follow these guidelines in determining
+consequences:
+
+==== 1. Correction
+
+*Community Impact*: Use of inappropriate language or other behaviour
+deemed unprofessional or unwelcome.
+
+*Consequence*: A private, written warning providing clarity around the
+nature of the violation and an explanation of why the behaviour was
+inappropriate. A public apology may be requested.
+
+*Duration*: Immediate
+
+==== 2. Warning
+
+*Community Impact*: A violation through a single incident or series of
+actions.
+
+*Consequence*: A warning with consequences for continued behaviour. No
+interaction with the people involved, including unsolicited interaction
+with those enforcing the Code of Conduct, for a specified period. This
+includes avoiding interactions in community spaces as well as external
+channels like social media. Violating these terms may lead to a
+temporary or permanent ban.
+
+*Duration*: 1-4 weeks
+
+==== 3. Temporary Ban
+
+*Community Impact*: A serious violation of community standards,
+including sustained inappropriate behaviour.
+
+*Consequence*: A temporary ban from any sort of interaction or public
+communication with the community for a specified period. No public or
+private interaction with the people involved, including unsolicited
+interaction with those enforcing the Code of Conduct, is allowed during
+this period. Violating these terms may lead to a permanent ban.
+
+*Duration*: 1-6 months
+
+==== 4. Permanent Ban
+
+*Community Impact*: Demonstrating a pattern of violation of community
+standards, including sustained inappropriate behaviour, harassment of an
+individual, or aggression toward or disparagement of classes of
+individuals.
+
+*Consequence*: A permanent ban from any sort of public interaction
+within the community.
+
+*Duration*: Permanent (with appeal rights after 12 months)
+
+==== Enforcement Across Perimeters
+
+For contributors with elevated access (Perimeter 2 or 1):
+
+[cols=",",options="header",]
+|===
+|Level |Additional Consequence
+|Correction |Noted in contributor record
+|Warning |Access privileges may be temporarily reduced
+|Temporary Ban |Access reduced to Perimeter 3 for ban duration
+|Permanent Ban |All access revoked
+|===
+
+'''''
+
+=== Appeals
+
+If you believe an enforcement decision was made in error:
+
+[arabic]
+. *Wait 7 days* after the decision (cooling-off period)
+. *Email* j.d.a.jewell@open.ac.uk with subject line "`Appeal: [Original
+Report ID]`"
+. *Explain* why you believe the decision should be reconsidered
+. *Provide* any new information not previously available
+
+*Appeals Process*
+
+* Appeals are reviewed by a different conduct team member than the
+original
+* You will receive a response within 14 days
+* The appeals decision is final
+* You may only appeal once per incident
+
+*Grounds for Appeal*
+
+* Procedural errors in the original investigation
+* New evidence not previously available
+* Disproportionate response to the violation
+* Misunderstanding of facts
+
+'''''
+
+=== Supporting Those Who Report
+
+We are committed to supporting those who report violations:
+
+*We Will* - Believe and take all reports seriously - Respect your
+privacy and confidentiality preferences - Keep you informed of progress
+(if you wish) - Take steps to protect you from retaliation - Provide
+resources if you need support
+
+*We Will Not* - Require you to confront the person directly - Dismiss
+reports without investigation - Reveal your identity without consent -
+Tolerate retaliation against reporters - Rush you to make decisions
+
+'''''
+
+=== Prevention
+
+Beyond enforcement, we actively work to prevent issues:
+
+*Onboarding* - All contributors are expected to read this Code of
+Conduct - Perimeter 2 applicants must confirm they’ve read and
+understood it - Maintainers receive additional training on enforcement
+
+*Culture* - We model the behaviour we expect - We intervene early when
+we see potential issues - We thank people for positive contributions -
+We create opportunities for diverse voices
+
+*Review* - This Code of Conduct is reviewed annually - Community
+feedback is welcomed - Changes are communicated clearly
+
+'''''
+
+=== Acknowledgments
+
+This Code of Conduct is adapted from:
+
+* https://www.contributor-covenant.org/[Contributor Covenant], version
+2.1
+* https://www.djangoproject.com/conduct/[Django Code of Conduct]
+* https://www.rust-lang.org/policies/code-of-conduct[Rust Code of
+Conduct]
+* https://www.python.org/psf/conduct/[Python Community Code of Conduct]
+
+We thank these communities for their leadership in creating welcoming
+spaces.
+
+'''''
+
+=== Questions?
+
+If you have questions about this Code of Conduct:
+
+* Open a
+https://github.com/hyperpolymath/quandledb/discussions[Discussion] (for
+general questions)
+* Email j.d.a.jewell@open.ac.uk (for private questions)
+* Contact any maintainer directly
+
+'''''
+
+=== Summary
+
+*Be kind. Be respectful. Be collaborative.*
+
+We’re all here because we care about this project. Let’s make it a place
+where everyone can do their best work.
+
+'''''
+
+Last updated: 2026 · Based on Contributor Covenant 2.1
diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
deleted file mode 100644
index d4ebd24..0000000
--- a/CODE_OF_CONDUCT.md
+++ /dev/null
@@ -1,307 +0,0 @@
-# Code of Conduct
-
-## Our Pledge
-
-We as members, contributors, and leaders pledge to make participation in QuandleDB a harassment-free experience for everyone, regardless of age, body size, visible or invisible disability, ethnicity, sex characteristics, gender identity and expression, level of experience, education, socio-economic status, nationality, personal appearance, race, caste, colour, religion, or sexual identity and orientation.
-
-We pledge to act and interact in ways that contribute to an open, welcoming, diverse, inclusive, and healthy community.
-
-We recognise that a thriving open source community requires **psychological safety** — an environment where people can contribute, ask questions, make mistakes, and learn without fear of ridicule or retaliation.
-
----
-
-## Our Standards
-
-### Expected Behaviour
-
-The following behaviours contribute to a positive environment:
-
-**Communication**
-- Using welcoming and inclusive language
-- Being respectful of differing viewpoints and experiences
-- Giving and gracefully accepting constructive feedback
-- Assuming good intent while addressing impact
-- Communicating clearly and patiently, especially with newcomers
-
-**Collaboration**
-- Focusing on what is best for the community
-- Showing empathy and kindness toward other community members
-- Being collaborative rather than competitive
-- Mentoring and supporting less experienced contributors
-- Celebrating others' contributions and successes
-
-**Professionalism**
-- Accepting responsibility and apologising to those affected by our mistakes
-- Learning from the experience and avoiding repetition
-- Respecting others' time and attention
-- Staying on topic in project spaces
-- Following project guidelines and conventions
-
-**Accessibility**
-- Using plain language and avoiding unnecessary jargon
-- Providing alt text for images and transcripts for audio/video
-- Being patient with those using assistive technologies
-- Accommodating different communication styles and needs
-- Recognising that not everyone communicates the same way
-
-### Unacceptable Behaviour
-
-The following behaviours are considered harassment and are unacceptable:
-
-**Harassment**
-- The use of sexualised language or imagery, and sexual attention or advances of any kind
-- Trolling, insulting or derogatory comments, and personal or political attacks
-- Public or private harassment
-- Deliberate intimidation, stalking, or following (online or in-person)
-- Unwelcome physical contact or simulated physical contact (e.g., emoji)
-- Sustained disruption of talks, events, or online discussions
-
-**Discrimination**
-- Discriminatory jokes and language
-- Posting or threatening to post others' personally identifying information ("doxing")
-- Advocating for, or encouraging, any of the above behaviour
-- Microaggressions — subtle, often unintentional, discriminatory comments or actions
-
-**Professional Misconduct**
-- Publishing others' private information without explicit permission
-- Misrepresenting affiliation or contributions
-- Plagiarism or claiming credit for others' work
-- Retaliating against anyone who reports a Code of Conduct violation
-- Other conduct which could reasonably be considered inappropriate in a professional setting
-
-### Grey Areas
-
-Some situations require judgement. When uncertain:
-
-- **Intent vs Impact**: Good intentions do not excuse harmful impact. Focus on making things right.
-- **Power Dynamics**: Those with more power (maintainers, employers, experienced contributors) must be especially mindful of their impact.
-- **Cultural Differences**: What's acceptable varies by culture. When in doubt, err on the side of caution and ask.
-- **Humour**: Jokes at others' expense are rarely funny to everyone. Punch up, not down.
-
----
-
-## Scope
-
-This Code of Conduct applies within all community spaces, including:
-
-**Online Spaces**
-- Repository discussions, issues, and pull/merge requests
-- Project chat channels (Matrix, Discord, Slack, IRC)
-- Mailing lists and forums
-- Social media when representing the project
-- Video calls and virtual meetings
-
-**In-Person Spaces**
-- Conferences, meetups, and events
-- Workshops and training sessions
-- Any gathering where you represent the project
-
-**Representation**
-This Code of Conduct also applies when an individual is officially representing the community in public spaces. Examples include:
-
-- Using an official project email address
-- Posting via an official social media account
-- Acting as an appointed representative at an event
-- Speaking on behalf of the project
-
----
-
-## Enforcement
-
-### Reporting
-
-If you experience or witness unacceptable behaviour, or have any other concerns, please report it as soon as possible.
-
-**How to Report**
-
-| Method | Details | Best For |
-|--------|---------|----------|
-| **Email** | j.d.a.jewell@open.ac.uk | Detailed reports, sensitive matters |
-| **Private Message** | Contact any maintainer directly | Quick questions, minor issues |
-| **Anonymous Form** | [Link to form if available] | When you need anonymity |
-
-**What to Include**
-
-- Your contact information (unless anonymous)
-- Names/usernames of those involved
-- Description of what happened
-- When and where it occurred
-- Any witnesses
-- Any supporting evidence (screenshots, links)
-- How you would like us to respond (if you have a preference)
-
-**What Happens Next**
-
-1. You will receive acknowledgment within **5 working days**
-2. The conduct team will review the report
-3. We may ask for additional information
-4. We will determine appropriate action
-5. We will inform you of the outcome (respecting others' privacy)
-
-### Confidentiality
-
-All reports will be handled with discretion:
-
-- Reporter identity is protected by default
-- Details are shared only with those who need to know
-- We will ask before naming you in any communication
-- Anonymous reports are accepted and investigated
-
-### Conflicts of Interest
-
-If a conduct team member is involved in an incident:
-
-- They will recuse themselves from the process
-- Another maintainer or external party will handle the report
-- We will disclose any potential conflicts
-
----
-
-## Enforcement Guidelines
-
-The conduct team will follow these guidelines in determining consequences:
-
-### 1. Correction
-
-**Community Impact**: Use of inappropriate language or other behaviour deemed unprofessional or unwelcome.
-
-**Consequence**: A private, written warning providing clarity around the nature of the violation and an explanation of why the behaviour was inappropriate. A public apology may be requested.
-
-**Duration**: Immediate
-
-### 2. Warning
-
-**Community Impact**: A violation through a single incident or series of actions.
-
-**Consequence**: A warning with consequences for continued behaviour. No interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, for a specified period. This includes avoiding interactions in community spaces as well as external channels like social media. Violating these terms may lead to a temporary or permanent ban.
-
-**Duration**: 1-4 weeks
-
-### 3. Temporary Ban
-
-**Community Impact**: A serious violation of community standards, including sustained inappropriate behaviour.
-
-**Consequence**: A temporary ban from any sort of interaction or public communication with the community for a specified period. No public or private interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, is allowed during this period. Violating these terms may lead to a permanent ban.
-
-**Duration**: 1-6 months
-
-### 4. Permanent Ban
-
-**Community Impact**: Demonstrating a pattern of violation of community standards, including sustained inappropriate behaviour, harassment of an individual, or aggression toward or disparagement of classes of individuals.
-
-**Consequence**: A permanent ban from any sort of public interaction within the community.
-
-**Duration**: Permanent (with appeal rights after 12 months)
-
-### Enforcement Across Perimeters
-
-For contributors with elevated access (Perimeter 2 or 1):
-
-| Level | Additional Consequence |
-|-------|----------------------|
-| Correction | Noted in contributor record |
-| Warning | Access privileges may be temporarily reduced |
-| Temporary Ban | Access reduced to Perimeter 3 for ban duration |
-| Permanent Ban | All access revoked |
-
----
-
-## Appeals
-
-If you believe an enforcement decision was made in error:
-
-1. **Wait 7 days** after the decision (cooling-off period)
-2. **Email** j.d.a.jewell@open.ac.uk with subject line "Appeal: [Original Report ID]"
-3. **Explain** why you believe the decision should be reconsidered
-4. **Provide** any new information not previously available
-
-**Appeals Process**
-
-- Appeals are reviewed by a different conduct team member than the original
-- You will receive a response within 14 days
-- The appeals decision is final
-- You may only appeal once per incident
-
-**Grounds for Appeal**
-
-- Procedural errors in the original investigation
-- New evidence not previously available
-- Disproportionate response to the violation
-- Misunderstanding of facts
-
----
-
-## Supporting Those Who Report
-
-We are committed to supporting those who report violations:
-
-**We Will**
-- Believe and take all reports seriously
-- Respect your privacy and confidentiality preferences
-- Keep you informed of progress (if you wish)
-- Take steps to protect you from retaliation
-- Provide resources if you need support
-
-**We Will Not**
-- Require you to confront the person directly
-- Dismiss reports without investigation
-- Reveal your identity without consent
-- Tolerate retaliation against reporters
-- Rush you to make decisions
-
----
-
-## Prevention
-
-Beyond enforcement, we actively work to prevent issues:
-
-**Onboarding**
-- All contributors are expected to read this Code of Conduct
-- Perimeter 2 applicants must confirm they've read and understood it
-- Maintainers receive additional training on enforcement
-
-**Culture**
-- We model the behaviour we expect
-- We intervene early when we see potential issues
-- We thank people for positive contributions
-- We create opportunities for diverse voices
-
-**Review**
-- This Code of Conduct is reviewed annually
-- Community feedback is welcomed
-- Changes are communicated clearly
-
----
-
-## Acknowledgments
-
-This Code of Conduct is adapted from:
-
-- [Contributor Covenant](https://www.contributor-covenant.org/), version 2.1
-- [Django Code of Conduct](https://www.djangoproject.com/conduct/)
-- [Rust Code of Conduct](https://www.rust-lang.org/policies/code-of-conduct)
-- [Python Community Code of Conduct](https://www.python.org/psf/conduct/)
-
-We thank these communities for their leadership in creating welcoming spaces.
-
----
-
-## Questions?
-
-If you have questions about this Code of Conduct:
-
-- Open a [Discussion](https://github.com/hyperpolymath/quandledb/discussions) (for general questions)
-- Email j.d.a.jewell@open.ac.uk (for private questions)
-- Contact any maintainer directly
-
----
-
-## Summary
-
-**Be kind. Be respectful. Be collaborative.**
-
-We're all here because we care about this project. Let's make it a place where everyone can do their best work.
-
----
-
-<sub>Last updated: 2026 · Based on Contributor Covenant 2.1</sub>
diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc
new file mode 100644
index 0000000..be58be8
--- /dev/null
+++ b/CONTRIBUTING.adoc
@@ -0,0 +1,108 @@
+== Clone the repository
+
+git clone https://github.com/hyperpolymath/quandledb.git cd quandledb
+
+== Using Nix (recommended for reproducibility)
+
+nix develop
+
+== Or using toolbox/distrobox
+
+toolbox create quandledb-dev toolbox enter quandledb-dev # Install
+dependencies manually
+
+== Verify setup
+
+just check # or: cargo check / mix compile / etc. just test # Run test
+suite
+
+....
+
+### Repository Structure
+....
+
+quandledb/ ├── src/ # Source code (Perimeter 1-2) ├── lib/ # Library
+code (Perimeter 1-2) ├── extensions/ # Extensions (Perimeter 2) ├──
+plugins/ # Plugins (Perimeter 2) ├── tools/ # Tooling (Perimeter 2) ├──
+docs/ # Documentation (Perimeter 3) │ ├── architecture/ # ADRs, specs
+(Perimeter 2) │ └── proposals/ # RFCs (Perimeter 3) ├── examples/ #
+Examples (Perimeter 3) ├── spec/ # Spec tests (Perimeter 3) ├── tests/ #
+Test suite (Perimeter 2-3) ├── .well-known/ # Protocol files (Perimeter
+1-3) ├── .github/ # GitHub config (Perimeter 1) │ ├── ISSUE_TEMPLATE/ │
+└── workflows/ ├── CHANGELOG.md ├── CODE_OF_CONDUCT.md ├──
+CONTRIBUTING.md # This file ├── GOVERNANCE.md ├── LICENSE ├──
+MAINTAINERS.md ├── README.adoc ├── SECURITY.md ├── flake.nix # Nix flake
+(Perimeter 1) └── Justfile # Task runner (Perimeter 1)
+
+....
+
+---
+
+## How to Contribute
+
+### Reporting Bugs
+
+**Before reporting**:
+1. Search existing issues
+2. Check if it's already fixed in `main`
+3. Determine which perimeter the bug affects
+
+**When reporting**:
+
+Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include:
+
+- Clear, descriptive title
+- Environment details (OS, versions, toolchain)
+- Steps to reproduce
+- Expected vs actual behaviour
+- Logs, screenshots, or minimal reproduction
+
+### Suggesting Features
+
+**Before suggesting**:
+1. Check the [roadmap](ROADMAP.md) if available
+2. Search existing issues and discussions
+3. Consider which perimeter the feature belongs to
+
+**When suggesting**:
+
+Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include:
+
+- Problem statement (what pain point does this solve?)
+- Proposed solution
+- Alternatives considered
+- Which perimeter this affects
+
+### Your First Contribution
+
+Look for issues labelled:
+
+- [`good first issue`](https://github.com/hyperpolymath/quandledb/labels/good%20first%20issue) — Simple Perimeter 3 tasks
+- [`help wanted`](https://github.com/hyperpolymath/quandledb/labels/help%20wanted) — Community help needed
+- [`documentation`](https://github.com/hyperpolymath/quandledb/labels/documentation) — Docs improvements
+- [`perimeter-3`](https://github.com/hyperpolymath/quandledb/labels/perimeter-3) — Community sandbox scope
+
+---
+
+## Development Workflow
+
+### Branch Naming
+....
+
+docs/short-description # Documentation (P3) test/what-added # Test
+additions (P3) feat/short-description # New features (P2)
+fix/issue-number-description # Bug fixes (P2) refactor/what-changed #
+Code improvements (P2) security/what-fixed # Security fixes (P1-2)
+
+....
+
+### Commit Messages
+
+We follow [Conventional Commits](https://www.conventionalcommits.org/):
+....
+
+():
+
+{empty}[optional body]
+
+{empty}[optional footer]
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
deleted file mode 100644
index 7e5fb33..0000000
--- a/CONTRIBUTING.md
+++ /dev/null
@@ -1,116 +0,0 @@
-# Clone the repository
-git clone https://github.com/hyperpolymath/quandledb.git
-cd quandledb
-
-# Using Nix (recommended for reproducibility)
-nix develop
-
-# Or using toolbox/distrobox
-toolbox create quandledb-dev
-toolbox enter quandledb-dev
-# Install dependencies manually
-
-# Verify setup
-just check   # or: cargo check / mix compile / etc.
-just test    # Run test suite
-```
-
-### Repository Structure
-```
-quandledb/
-├── src/                 # Source code (Perimeter 1-2)
-├── lib/                 # Library code (Perimeter 1-2)
-├── extensions/          # Extensions (Perimeter 2)
-├── plugins/             # Plugins (Perimeter 2)
-├── tools/               # Tooling (Perimeter 2)
-├── docs/                # Documentation (Perimeter 3)
-│   ├── architecture/    # ADRs, specs (Perimeter 2)
-│   └── proposals/       # RFCs (Perimeter 3)
-├── examples/            # Examples (Perimeter 3)
-├── spec/                # Spec tests (Perimeter 3)
-├── tests/               # Test suite (Perimeter 2-3)
-├── .well-known/         # Protocol files (Perimeter 1-3)
-├── .github/             # GitHub config (Perimeter 1)
-│   ├── ISSUE_TEMPLATE/
-│   └── workflows/
-├── CHANGELOG.md
-├── CODE_OF_CONDUCT.md
-├── CONTRIBUTING.md      # This file
-├── GOVERNANCE.md
-├── LICENSE
-├── MAINTAINERS.md
-├── README.adoc
-├── SECURITY.md
-├── flake.nix            # Nix flake (Perimeter 1)
-└── Justfile             # Task runner (Perimeter 1)
-```
-
----
-
-## How to Contribute
-
-### Reporting Bugs
-
-**Before reporting**:
-1. Search existing issues
-2. Check if it's already fixed in `main`
-3. Determine which perimeter the bug affects
-
-**When reporting**:
-
-Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include:
-
-- Clear, descriptive title
-- Environment details (OS, versions, toolchain)
-- Steps to reproduce
-- Expected vs actual behaviour
-- Logs, screenshots, or minimal reproduction
-
-### Suggesting Features
-
-**Before suggesting**:
-1. Check the [roadmap](ROADMAP.md) if available
-2. Search existing issues and discussions
-3. Consider which perimeter the feature belongs to
-
-**When suggesting**:
-
-Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include:
-
-- Problem statement (what pain point does this solve?)
-- Proposed solution
-- Alternatives considered
-- Which perimeter this affects
-
-### Your First Contribution
-
-Look for issues labelled:
-
-- [`good first issue`](https://github.com/hyperpolymath/quandledb/labels/good%20first%20issue) — Simple Perimeter 3 tasks
-- [`help wanted`](https://github.com/hyperpolymath/quandledb/labels/help%20wanted) — Community help needed
-- [`documentation`](https://github.com/hyperpolymath/quandledb/labels/documentation) — Docs improvements
-- [`perimeter-3`](https://github.com/hyperpolymath/quandledb/labels/perimeter-3) — Community sandbox scope
-
----
-
-## Development Workflow
-
-### Branch Naming
-```
-docs/short-description       # Documentation (P3)
-test/what-added              # Test additions (P3)
-feat/short-description       # New features (P2)
-fix/issue-number-description # Bug fixes (P2)
-refactor/what-changed        # Code improvements (P2)
-security/what-fixed          # Security fixes (P1-2)
-```
-
-### Commit Messages
-
-We follow [Conventional Commits](https://www.conventionalcommits.org/):
-```
-<type>(<scope>): <description>
-
-[optional body]
-
-[optional footer]
diff --git a/PROOF-NARRATIVE.adoc b/PROOF-NARRATIVE.adoc
new file mode 100644
index 0000000..854b4d3
--- /dev/null
+++ b/PROOF-NARRATIVE.adoc
@@ -0,0 +1,408 @@
+== Proof Narrative — QuandleDB
+
+This file is the *single coherent story* of what QuandleDB proves, what
+it assumes, and what it has left to prove.
+
+For the per-obligation checklist with status/prover/effort, see
+PROOF-NEEDS.md. For the registry of every load-bearing unproven
+assumption, see ASSUMPTIONS.md.
+
+'''''
+
+=== 1. Position in the stack
+
+QuandleDB is the *semantic identity layer* of the KRL stack:
+
+....
+┌─────────────────────────────────────────────────────────┐
+│  KRL surface language     (hyperpolymath/krl)           │
+└─────────────────┬───────────────────────────────────────┘
+                  │ compiles to
+                  ▼
+┌─────────────────────────────────────────────────────────┐
+│  TangleIR                                                │
+└─────────────────┬───────────────────────────────────────┘
+                  │ extract_presentation(ir)
+                  ▼
+┌─────────────────────────────────────────────────────────┐
+│  QuandlePresentation  (THIS REPO)                        │
+│    server/quandle_semantic.jl — Julia core               │
+│    canonicalize_presentation → BLAKE3 fingerprint        │
+│    _dihedral_colouring_count → integer invariants        │
+└─────────────────┬───────────────────────────────────────┘
+                  │ fingerprint, key
+                  ▼
+┌─────────────────────────────────────────────────────────┐
+│  Skein.jl       — invariants table, query layer          │
+└─────────────────────────────────────────────────────────┘
+....
+
+Consequence: QuandleDB owes correctness of the *functor*
+`+Q : Tang → Quand+` and of the *canonical-form* that makes fingerprints
+meaningful as equality-witnesses.
+
+=== 2. Proven now
+
+All current results are *property-tested in Julia* (not formally
+mechanised). Tests live in
+link:server/test_quandle_axioms.jl[`+server/test_quandle_axioms.jl+`]
+(250 LoC, 8 testsets, ~150 individual assertions).
+
+==== Algebraic / mathematical
+
+[width="100%",cols="15%,39%,21%,25%",options="header",]
+|===
+|ID |Statement |Form |Where
+|*Q-DihedralAxioms* |Dihedral quandle `+Z_p+` satisfies idempotence,
+right-invertibility, right self-distributivity for
+`+p ∈ {3, 5, 7, 11, 13}+` |Julia property tests, exhaustive over `+Z_p+`
+|`+test_quandle_axioms.jl §1+`
+
+|*Q-PresentationWF* |Extracted presentations are structurally
+well-formed (generator indices in-range, one relation per crossing) for
+the standard knot table (trefoil, figure-eight, cinquefoil) |Julia
+property tests |`+test_quandle_axioms.jl §2+`
+
+|*Q-CanonIdem* |`+canonicalize ∘ canonicalize = canonicalize+` on the
+standard test knots |Julia property tests |`+test_quandle_axioms.jl §3+`
+
+|*Q-DescriptorDet* |The same PD yields the same `+presentation_hash+`,
+`+colouring_count_3+`, `+colouring_count_5+`, `+quandle_key+`
+deterministically (run-to-run) |Julia property tests
+|`+test_quandle_axioms.jl §4+`
+
+|*Q-R1Reduce* |Injecting a nugatory crossing into a PD and running
+`+r1_simplify+` strictly reduces crossing/generator count |Julia
+property tests |`+test_quandle_axioms.jl §5+`
+
+|*Q-R2Reduce* |`+s1·S1·s1·s1·s1+` (trefoil + bigon) after
+`+r2_simplify+` agrees with the canonical trefoil on dihedral colouring
+counts |Julia property tests |`+test_quandle_axioms.jl §6+`
+
+|*Q-ColorDistinguishes* |The three standard test knots are pairwise
+distinguished by at least one of `+colouring_count_3+` or
+`+colouring_count_5+` |Julia property tests
+|`+test_quandle_axioms.jl §7+`
+
+|*Q-KeyUniqueness* |`+quandle_key+` is pairwise distinct on the three
+standard test knots |Julia property tests |`+test_quandle_axioms.jl §8+`
+|===
+
+==== Implementation
+
+`+extract_presentation+`, `+canonicalize_presentation+`,
+`+canonical_presentation_blob+`, `+_dihedral_colouring_count+` are
+implemented in `+server/quandle_semantic.jl+` and exercised by the above
+tests on the standard knot table. The implementation is production-grade
+Julia (union-find for Wirtinger arc collapsing, modular linear algebra
+for the colouring counts).
+
+=== 3. Remaining obligations (the narrative arc)
+
+These extend `+PROOF-NEEDS.md+`’s previously-stated M1–M4 / S1–S3 with
+the implementation-level obligations surfaced by the 2026-06-01 audit.
+The narrative is grouped by where the obligation sits in the "`PD →
+presentation → fingerprint → query`" pipeline.
+
+==== Presentation extraction
+
+===== QD-1 — `+extract_presentation+` is well-formed on arbitrary connected PD codes
+
+*Claim.* For *every* connected `+KnotTheory.PlanarDiagram+` (not just
+the three test knots), `+extract_presentation(pd)+` returns a
+`+QuandlePresentation+` such that: - generator indices are in
+`+1..generator_count+` - relation count equals crossing count - each
+relation’s `+lhs+`, `+rhs+`, `+out+` are in range - the union-find
+collapsing is correct (over-strand arcs `+d+` and `+b+` are identified
+at each crossing)
+
+*Why valuable.* Generalises Q-PresentationWF from the standard knot
+table to the full input space. Closes PROOF-NEEDS M1’s remaining gap.
+
+*Assumptions.* - [[A-QD-1.1]] PD codes are well-formed: each crossing
+has exactly 4 arcs in PD-positions `+(a, b, c, d)+`. - [[A-QD-1.2]]
+Connectedness (or per-component handling) is checked by the caller;
+`+extract_presentation+` does not validate it.
+
+*How to discharge.* Either: - _Formal proof_ via Idris2 on a
+dependent-type-encoded `+WellFormedPD+`, or - _Property-based test_
+generating random PD codes from braid words
+(`+KnotTheory.from_braid_word+`) and verifying the four structural
+conditions.
+
+===== QD-9 — Union-find traversal-order independence
+
+*Claim.* The union-find in `+_wirtinger_arc_to_generator+` produces the
+same `+generator_count+` and `+arc_to_gen+` mapping (up to the chosen
+canonical labelling) regardless of the order in which crossings are
+visited.
+
+*Why valuable.* Reproducibility hazard. Same PD on different array
+layouts could yield different generator-count without this, which would
+silently destabilise `+quandle_key+`.
+
+*Assumptions.* - [[A-QD-9.1]] Path compression preserves equivalence
+classes. - [[A-QD-9.2]] Iteration order of `+pd.crossings+` is
+deterministic at the Julia level (true for `+Vector+`).
+
+*How to discharge.* Shuffle-test: for each PD in the test corpus,
+randomly shuffle `+pd.crossings+`, re-extract, assert equality up to
+canonical relabelling. Easy single-PR.
+
+===== QD-10 — KRL parser accepts exactly the language defined by `+spec/grammar.ebnf+`
+
+*Claim.* `+server/krl/Parser.jl::parse_any(s)+` succeeds iff `+s+` is a
+string in the v0.1.0 KRL grammar.
+
+*Why valuable.* Two KRL parsers exist (`+KRLAdapter.jl+` and
+`+server/krl/+`); both must accept the same language for queries to be
+portable. See KRL repo `+KR-6+`.
+
+*Assumptions.* - [[A-QD-10.1]] `+spec/grammar.ebnf+` v0.1.0 is
+unambiguous. - [[A-QD-10.2]] Grammar in KRL repo and quandledb repo are
+kept in lock-step (currently a manual discipline; should be a CI check).
+
+*How to discharge.* Differential property test against
+`+KRLAdapter.jl::parse_krl+`. Coordinate with KRL `+KR-6+`.
+
+===== QD-11 — SQL→KRL translation is semantics-preserving
+
+*Claim.* For every SQL query `+s+` accepted by
+`+server/krl/SqlFrontend.jl::parse_sql+`, the resulting `+KRLProgram+`
+returns the same result set as `+s+` would on a reference SQL engine
+over the same data.
+
+*Why valuable.* User-visible queries depend on this. SqlFrontend exists
+so users can write `+SELECT * FROM knots WHERE crossing < 8+` and have
+it translate to `+find where crossing < 8+`. Semantic preservation is
+the user-facing contract.
+
+*Assumptions.* - [[A-QD-11.1]] The SQL subset supported is well-defined
+(no joins, no subqueries, equality + comparison filters only — verify
+against `+SqlFrontend.jl+`). - [[A-QD-11.2]] `+KnotTheory.jl+`’s notion
+of `+crossing_number+`, `+writhe+`, `+genus+` are stable across
+implementations.
+
+*How to discharge.* Property test: for a corpus of supported SQL
+queries, compare results against a reference Julia implementation that
+traverses the knot table directly.
+
+==== Canonical form and fingerprinting
+
+===== QD-3 — Colouring-count well-definedness
+
+(Re-statement of PROOF-NEEDS M4 with the assumption registry.)
+
+*Claim.* `+_dihedral_colouring_count(p, modulus)+` depends only on the
+isomorphism class of the fundamental quandle of `+p+`, not on the
+particular `+QuandlePresentation+` chosen to represent it.
+
+*Why valuable.* Without this, two presentations of the same knot can
+return different colouring counts. The whole `+quandle_key+` machinery
+becomes unreliable. This is *the central claim* of the semantic-index
+layer.
+
+*Assumptions.* - [[A-QD-3.1]] The number of quandle homomorphisms from
+`+Q+` to a fixed finite quandle `+T+` is a class invariant of `+Q+`
+(standard algebraic result). - [[A-QD-3.2]]
+`+_dihedral_colouring_count+` correctly counts solutions of the linear
+system over `+Z_p+` — i.e., the matrix `+M+` in the implementation
+correctly encodes the dihedral relations.
+
+*How to discharge.* Two parts: 1. For each test knot, build two
+structurally-different presentations (e.g., shuffle the relations) and
+assert equal counts. 2. Lean 4 proof that the dihedral-relation matrix
+`+M+` correctly encodes the homomorphism-counting problem.
+
+===== QD-4 — Fingerprint determinism across platforms
+
+(Re-statement of PROOF-NEEDS S1.)
+
+*Claim.* Given identical input PD codes,
+`+canonical_presentation_blob(p)+` produces identical BLAKE3 output
+bytes on Linux x86_64, Linux aarch64, macOS, and WebAssembly.
+
+*Why valuable.* Two presentations with the same fingerprint are
+isomorphic quandles, *across platforms*. Currently single-platform
+tested only.
+
+*Assumptions.* - [[A-QD-4.1]] BLAKE3 produces identical output for
+identical input bytes (cryptographic primitive assumption). -
+[[A-QD-4.2]] Julia’s `+string(...)+` interpolation of `+Int+` is
+identical across platforms (it is — base-10 ASCII). - [[A-QD-4.3]]
+`+sort(...; by = r -> (r.lhs, r.rhs, r.out, r.is_inverse ? 1 : 0))+` is
+stable and order-preserving across Julia implementations.
+
+*How to discharge.* CI matrix run on Linux x86_64, Linux aarch64, macOS,
+WSL; assert identical hashes. No formal proof needed; this is an
+empirical platform contract.
+
+===== QD-7 — Canonical-form ordering is a total order
+
+*Claim.* The comparator
+`+by = r -> (r.lhs, r.rhs, r.out, r.is_inverse ? 1 : 0)+` is a total
+order on the actual domain of relations seen at runtime.
+
+*Why valuable.* Currently the sort assumes total order. If two relations
+agree on all four fields then `+sort+` is stable but the output of
+`+canonicalize_presentation+` is *identical* for them — which is fine.
+But if there are _invisible_ relation distinctions (e.g., generators
+that get the same numeric id but different provenance) the
+canonicalisation silently merges them.
+
+*Assumptions.* - [[A-QD-7.1]] No relation field outside
+`+(lhs, rhs, out, is_inverse)+` affects quandle equality.
+
+*How to discharge.* Either (a) prove no other field exists (structurally
+trivial — the `+QuandleRelation+` struct has only these four fields), or
+(b) add a comment + test asserting that.
+
+===== QD-8 — `+_dihedral_colouring_count+` correctness
+
+*Claim.* `+_dihedral_colouring_count(p, modulus)+` returns the number of
+quandle homomorphisms from `+fundamental(p)+` to the dihedral quandle
+`+Z_modulus+`.
+
+*Why valuable.* This is the implementation of the central invariant.
+Currently asserted by Q-DihedralAxioms (which tests the target’s quandle
+laws) and Q-ColorDistinguishes (which tests it discriminates), but not
+by a direct correctness statement.
+
+*Assumptions.* - [[A-QD-8.1]] `+_rank_mod_p!+` correctly computes matrix
+rank over `+Z_p+` for prime `+p+`. - [[A-QD-8.2]] `+p^(g - rank)+` is
+the count of solutions of the homogeneous linear system over `+Z_p+`
+with `+g+` unknowns and the computed rank.
+
+*How to discharge.* Cross-check against an independent Brute-force
+counter on small examples (`+g ≤ 4+`, `+modulus ∈ {3, 5, 7}+`); for the
+algebraic argument cite a linear-algebra textbook.
+
+==== Reidemeister invariance
+
+===== QD-2 — R3 invariance (the standing gap)
+
+*Claim.* If diagrams `+D₁+` and `+D₂+` differ by a single Reidemeister-3
+move, their `+quandle_descriptor+` outputs are equal.
+
+*Why valuable.* PROOF-NEEDS M2 covers R1 and R2; R3 is the standing gap.
+Without R3 we do not have full Reidemeister equivalence — the invariant
+is incomplete.
+
+*Assumptions.* - [[A-QD-2.1]] R1 + R2 + R3 generate isotopy on classical
+knot diagrams (Reidemeister 1927 — standard). - [[A-QD-2.2]] R3 acts on
+the fundamental quandle as a permutation of generators (standard
+quandle-theoretic result).
+
+*How to discharge.* Either: 1. Contribute `+r3_simplify+` to
+`+KnotTheory.jl+` upstream (the right long-term home), or 2. Construct
+R3-related PD pairs by hand for a small corpus (trefoil, figure-eight)
+and verify `+quandle_descriptor+` equality.
+
+===== QD-12 — Read-only API guarantee
+
+*Claim.* No HTTP endpoint in `+server/serve.jl+` invokes a mutating
+operation on the Skein.jl database.
+
+*Why valuable.* `+.claude/CLAUDE.md+` states "`Server is read-only
+(database mutations via Skein.jl REPL)`" as a convention. Promoting this
+to a _checked_ invariant prevents accidental mutation creep.
+
+*Assumptions.* - [[A-QD-12.1]] All Skein.jl mutating operations are
+identifiable by name (e.g., `+store!+`, `+delete!+`, `+update!+`).
+
+*How to discharge.* Static check:
+`+grep -E '(store!|delete!|update!)' server/serve.jl+` returns empty.
+Add as a CI gate.
+
+==== FFI / ABI
+
+===== QD-5 — Idris2 ABI ↔ Zig FFI layout agreement
+
+(Re-statement of PROOF-NEEDS S2.)
+
+*Claim.* Every record type defined in `+src/abi/Types.idr+` has a
+byte-for-byte identical memory layout in the corresponding Zig struct in
+`+src/ffi/semantic_ffi.zig+` and the BEAM NIF in
+`+beam/native/quandle_db_nif.zig+`.
+
+*Why valuable.* Standard FFI hazard. Currently _declared_ by the
+existence of both files but not _proved_.
+
+*Assumptions.* - [[A-QD-5.1]] Idris2’s `+HasSize+` / `+HasAlignment+`
+instances are correct for the platforms targeted. - [[A-QD-5.2]] Zig’s
+`+extern struct+` layout is C-ABI compatible.
+
+*How to discharge.* Encode layouts directly in Idris2 dependent types;
+emit a compile-time check in Zig (`+@sizeOf+`, `+@alignOf+`,
+`+@offsetOf+`); cross-check at the BEAM NIF boundary with `+bit_size+`.
+
+===== QD-6 — BEAM NIF never crashes the VM
+
+(Re-statement of PROOF-NEEDS S3.)
+
+*Claim.* For every input the Elixir side can pass to a NIF in
+`+beam/native/quandle_db_nif.zig+`, the NIF either returns a valid
+result, an `+:error+` term, or raises a NIF exception — but never
+crashes the BEAM VM.
+
+*Why valuable.* Production-critical. A NIF crash brings down the whole
+VM.
+
+*Assumptions.* - [[A-QD-6.1]] Zig’s safety guarantees (no UB on
+well-typed code in Release-Safe mode) hold for the NIF code paths. -
+[[A-QD-6.2]] Elixir-side input types are validated before the NIF call
+(typespec discipline).
+
+*How to discharge.* Fuzz harness on the NIF boundary: random bytes +
+random tagged-tuple shapes → NIF → assert "`no VM crash`". Combine with
+Dialyzer for the typespec discipline.
+
+=== 4. The "`stupid proof`" exclusions
+
+For completeness, we do *not* pursue:
+
+* _"``+QuandlePresentation+` has these fields`"_ — Julia struct
+definition.
+* _"``+extract_presentation+` returns a `+QuandlePresentation+``"_ —
+Julia type assertion.
+* _"`BLAKE3 is collision-resistant`"_ — cryptographic primitive
+assumption ([[A-QD-4.1]]).
+* _"`SHA-256 is collision-resistant`"_ — same.
+* _"`union-find converges in nearly-linear amortised time`"_ — Tarjan
+1975, out of scope.
+
+=== 5. How to add a new obligation
+
+[arabic]
+. Add a row to PROOF-NEEDS.md with `+QD-N+` id, category (M, S, ABI),
+prover, priority, effort.
+. Add the narrative entry here with statement, _why valuable_, status,
+*assumptions*, _how to discharge_. Assumptions block is non-optional.
+. Each new assumption gets an entry in ASSUMPTIONS.md with `+A-QD-N.M+`
+id and MATH/DESIGN/EMPIRICAL/CRYPTO classification.
+
+=== 6. References
+
+* Core algorithms:
+link:server/quandle_semantic.jl[`+server/quandle_semantic.jl+`].
+* Property tests:
+link:server/test_quandle_axioms.jl[`+server/test_quandle_axioms.jl+`].
+* Server: link:server/serve.jl[`+server/serve.jl+`].
+* KRL parser: link:server/krl/[`+server/krl/+`].
+* BEAM NIF: link:beam/[`+beam/+`].
+* ABI: link:src/abi/[`+src/abi/+`], link:src/ffi/[`+src/ffi/+`].
+* Companion narratives: `+hyperpolymath/krl/PROOF-NARRATIVE.md+` — KRL
+surface `+hyperpolymath/tangle/PROOF-NARRATIVE.md+` — Tangle semantic
+core
+
+=== 7. Mathematical references
+
+* Joyce 1982 — _A classifying invariant of knots, the knot quandle_.
+* Matveev 1982 — _Distributive groupoids in knot theory_ (parallel
+introduction of quandles).
+* Reidemeister 1927 — _Elementare Begründung der Knotentheorie_
+(R1+R2+R3 generation).
+* Kauffman _Knots and Physics_ — colouring count and dihedral quandle as
+concrete invariant.
+* Eisermann _The number of knot group representations_ — faithfulness of
+the fundamental quandle on prime alternating knots.
diff --git a/PROOF-NARRATIVE.md b/PROOF-NARRATIVE.md
deleted file mode 100644
index d45fdd9..0000000
--- a/PROOF-NARRATIVE.md
+++ /dev/null
@@ -1,400 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
-# Proof Narrative — QuandleDB
-
-This file is the **single coherent story** of what QuandleDB proves,
-what it assumes, and what it has left to prove.
-
-For the per-obligation checklist with status/prover/effort, see
-[PROOF-NEEDS.md](PROOF-NEEDS.md).
-For the registry of every load-bearing unproven assumption, see
-[ASSUMPTIONS.md](ASSUMPTIONS.md).
-
----
-
-## 1. Position in the stack
-
-QuandleDB is the **semantic identity layer** of the KRL stack:
-
-```
-┌─────────────────────────────────────────────────────────┐
-│  KRL surface language     (hyperpolymath/krl)           │
-└─────────────────┬───────────────────────────────────────┘
-                  │ compiles to
-                  ▼
-┌─────────────────────────────────────────────────────────┐
-│  TangleIR                                                │
-└─────────────────┬───────────────────────────────────────┘
-                  │ extract_presentation(ir)
-                  ▼
-┌─────────────────────────────────────────────────────────┐
-│  QuandlePresentation  (THIS REPO)                        │
-│    server/quandle_semantic.jl — Julia core               │
-│    canonicalize_presentation → BLAKE3 fingerprint        │
-│    _dihedral_colouring_count → integer invariants        │
-└─────────────────┬───────────────────────────────────────┘
-                  │ fingerprint, key
-                  ▼
-┌─────────────────────────────────────────────────────────┐
-│  Skein.jl       — invariants table, query layer          │
-└─────────────────────────────────────────────────────────┘
-```
-
-Consequence: QuandleDB owes correctness of the **functor**
-`Q : Tang → Quand` and of the **canonical-form** that makes
-fingerprints meaningful as equality-witnesses.
-
-## 2. Proven now
-
-All current results are **property-tested in Julia** (not formally
-mechanised). Tests live in [`server/test_quandle_axioms.jl`](server/test_quandle_axioms.jl)
-(250 LoC, 8 testsets, ~150 individual assertions).
-
-### Algebraic / mathematical
-
-| ID | Statement | Form | Where |
-|----|-----------|------|-------|
-| **Q-DihedralAxioms** | Dihedral quandle `Z_p` satisfies idempotence, right-invertibility, right self-distributivity for `p ∈ {3, 5, 7, 11, 13}` | Julia property tests, exhaustive over `Z_p` | `test_quandle_axioms.jl §1` |
-| **Q-PresentationWF** | Extracted presentations are structurally well-formed (generator indices in-range, one relation per crossing) for the standard knot table (trefoil, figure-eight, cinquefoil) | Julia property tests | `test_quandle_axioms.jl §2` |
-| **Q-CanonIdem** | `canonicalize ∘ canonicalize = canonicalize` on the standard test knots | Julia property tests | `test_quandle_axioms.jl §3` |
-| **Q-DescriptorDet** | The same PD yields the same `presentation_hash`, `colouring_count_3`, `colouring_count_5`, `quandle_key` deterministically (run-to-run) | Julia property tests | `test_quandle_axioms.jl §4` |
-| **Q-R1Reduce** | Injecting a nugatory crossing into a PD and running `r1_simplify` strictly reduces crossing/generator count | Julia property tests | `test_quandle_axioms.jl §5` |
-| **Q-R2Reduce** | `s1·S1·s1·s1·s1` (trefoil + bigon) after `r2_simplify` agrees with the canonical trefoil on dihedral colouring counts | Julia property tests | `test_quandle_axioms.jl §6` |
-| **Q-ColorDistinguishes** | The three standard test knots are pairwise distinguished by at least one of `colouring_count_3` or `colouring_count_5` | Julia property tests | `test_quandle_axioms.jl §7` |
-| **Q-KeyUniqueness** | `quandle_key` is pairwise distinct on the three standard test knots | Julia property tests | `test_quandle_axioms.jl §8` |
-
-### Implementation
-
-`extract_presentation`, `canonicalize_presentation`,
-`canonical_presentation_blob`, `_dihedral_colouring_count` are
-implemented in `server/quandle_semantic.jl` and exercised by the
-above tests on the standard knot table. The implementation is
-production-grade Julia (union-find for Wirtinger arc collapsing,
-modular linear algebra for the colouring counts).
-
-## 3. Remaining obligations (the narrative arc)
-
-These extend `PROOF-NEEDS.md`'s previously-stated M1–M4 / S1–S3 with
-the implementation-level obligations surfaced by the 2026-06-01
-audit. The narrative is grouped by where the obligation sits in the
-"PD → presentation → fingerprint → query" pipeline.
-
-### Presentation extraction
-
-#### QD-1 — `extract_presentation` is well-formed on arbitrary connected PD codes
-
-**Claim.** For **every** connected `KnotTheory.PlanarDiagram` (not just
-the three test knots), `extract_presentation(pd)` returns a
-`QuandlePresentation` such that:
-- generator indices are in `1..generator_count`
-- relation count equals crossing count
-- each relation's `lhs`, `rhs`, `out` are in range
-- the union-find collapsing is correct (over-strand arcs `d` and `b`
-  are identified at each crossing)
-
-**Why valuable.** Generalises Q-PresentationWF from the standard knot
-table to the full input space. Closes PROOF-NEEDS M1's remaining gap.
-
-**Assumptions.**
-- [[A-QD-1.1]] PD codes are well-formed: each crossing has exactly
-  4 arcs in PD-positions `(a, b, c, d)`.
-- [[A-QD-1.2]] Connectedness (or per-component handling) is checked
-  by the caller; `extract_presentation` does not validate it.
-
-**How to discharge.** Either:
-- _Formal proof_ via Idris2 on a dependent-type-encoded
-  `WellFormedPD`, or
-- _Property-based test_ generating random PD codes from braid words
-  (`KnotTheory.from_braid_word`) and verifying the four structural
-  conditions.
-
-#### QD-9 — Union-find traversal-order independence
-
-**Claim.** The union-find in `_wirtinger_arc_to_generator` produces
-the same `generator_count` and `arc_to_gen` mapping (up to the chosen
-canonical labelling) regardless of the order in which crossings are
-visited.
-
-**Why valuable.** Reproducibility hazard. Same PD on different
-array layouts could yield different generator-count without this,
-which would silently destabilise `quandle_key`.
-
-**Assumptions.**
-- [[A-QD-9.1]] Path compression preserves equivalence classes.
-- [[A-QD-9.2]] Iteration order of `pd.crossings` is deterministic at
-  the Julia level (true for `Vector`).
-
-**How to discharge.** Shuffle-test: for each PD in the test corpus,
-randomly shuffle `pd.crossings`, re-extract, assert equality up to
-canonical relabelling. Easy single-PR.
-
-#### QD-10 — KRL parser accepts exactly the language defined by `spec/grammar.ebnf`
-
-**Claim.** `server/krl/Parser.jl::parse_any(s)` succeeds iff `s` is a
-string in the v0.1.0 KRL grammar.
-
-**Why valuable.** Two KRL parsers exist (`KRLAdapter.jl` and
-`server/krl/`); both must accept the same language for queries to be
-portable. See KRL repo `KR-6`.
-
-**Assumptions.**
-- [[A-QD-10.1]] `spec/grammar.ebnf` v0.1.0 is unambiguous.
-- [[A-QD-10.2]] Grammar in KRL repo and quandledb repo are kept in lock-step
-  (currently a manual discipline; should be a CI check).
-
-**How to discharge.** Differential property test against
-`KRLAdapter.jl::parse_krl`. Coordinate with KRL `KR-6`.
-
-#### QD-11 — SQL→KRL translation is semantics-preserving
-
-**Claim.** For every SQL query `s` accepted by
-`server/krl/SqlFrontend.jl::parse_sql`, the resulting `KRLProgram`
-returns the same result set as `s` would on a reference SQL engine
-over the same data.
-
-**Why valuable.** User-visible queries depend on this. SqlFrontend
-exists so users can write `SELECT * FROM knots WHERE crossing < 8`
-and have it translate to `find where crossing < 8`. Semantic
-preservation is the user-facing contract.
-
-**Assumptions.**
-- [[A-QD-11.1]] The SQL subset supported is well-defined (no
-  joins, no subqueries, equality + comparison filters only — verify
-  against `SqlFrontend.jl`).
-- [[A-QD-11.2]] `KnotTheory.jl`'s notion of `crossing_number`,
-  `writhe`, `genus` are stable across implementations.
-
-**How to discharge.** Property test: for a corpus of supported SQL
-queries, compare results against a reference Julia implementation
-that traverses the knot table directly.
-
-### Canonical form and fingerprinting
-
-#### QD-3 — Colouring-count well-definedness
-
-(Re-statement of PROOF-NEEDS M4 with the assumption registry.)
-
-**Claim.** `_dihedral_colouring_count(p, modulus)` depends only on
-the isomorphism class of the fundamental quandle of `p`, not on the
-particular `QuandlePresentation` chosen to represent it.
-
-**Why valuable.** Without this, two presentations of the same knot
-can return different colouring counts. The whole `quandle_key`
-machinery becomes unreliable. This is **the central claim** of the
-semantic-index layer.
-
-**Assumptions.**
-- [[A-QD-3.1]] The number of quandle homomorphisms from `Q` to a
-  fixed finite quandle `T` is a class invariant of `Q` (standard
-  algebraic result).
-- [[A-QD-3.2]] `_dihedral_colouring_count` correctly counts solutions
-  of the linear system over `Z_p` — i.e., the matrix `M` in the
-  implementation correctly encodes the dihedral relations.
-
-**How to discharge.** Two parts:
-1. For each test knot, build two structurally-different presentations
-   (e.g., shuffle the relations) and assert equal counts.
-2. Lean 4 proof that the dihedral-relation matrix `M` correctly
-   encodes the homomorphism-counting problem.
-
-#### QD-4 — Fingerprint determinism across platforms
-
-(Re-statement of PROOF-NEEDS S1.)
-
-**Claim.** Given identical input PD codes,
-`canonical_presentation_blob(p)` produces identical BLAKE3 output
-bytes on Linux x86_64, Linux aarch64, macOS, and WebAssembly.
-
-**Why valuable.** Two presentations with the same fingerprint are
-isomorphic quandles, **across platforms**. Currently single-platform
-tested only.
-
-**Assumptions.**
-- [[A-QD-4.1]] BLAKE3 produces identical output for identical input
-  bytes (cryptographic primitive assumption).
-- [[A-QD-4.2]] Julia's `string(...)` interpolation of `Int` is
-  identical across platforms (it is — base-10 ASCII).
-- [[A-QD-4.3]] `sort(...; by = r -> (r.lhs, r.rhs, r.out, r.is_inverse ? 1 : 0))`
-  is stable and order-preserving across Julia implementations.
-
-**How to discharge.** CI matrix run on Linux x86_64, Linux aarch64,
-macOS, WSL; assert identical hashes. No formal proof needed; this
-is an empirical platform contract.
-
-#### QD-7 — Canonical-form ordering is a total order
-
-**Claim.** The comparator
-`by = r -> (r.lhs, r.rhs, r.out, r.is_inverse ? 1 : 0)` is a total
-order on the actual domain of relations seen at runtime.
-
-**Why valuable.** Currently the sort assumes total order. If two
-relations agree on all four fields then `sort` is stable but the
-output of `canonicalize_presentation` is **identical** for them —
-which is fine. But if there are *invisible* relation distinctions
-(e.g., generators that get the same numeric id but different
-provenance) the canonicalisation silently merges them.
-
-**Assumptions.**
-- [[A-QD-7.1]] No relation field outside `(lhs, rhs, out, is_inverse)`
-  affects quandle equality.
-
-**How to discharge.** Either (a) prove no other field exists
-(structurally trivial — the `QuandleRelation` struct has only these
-four fields), or (b) add a comment + test asserting that.
-
-#### QD-8 — `_dihedral_colouring_count` correctness
-
-**Claim.** `_dihedral_colouring_count(p, modulus)` returns the number
-of quandle homomorphisms from `fundamental(p)` to the dihedral
-quandle `Z_modulus`.
-
-**Why valuable.** This is the implementation of the central
-invariant. Currently asserted by Q-DihedralAxioms (which tests the
-target's quandle laws) and Q-ColorDistinguishes (which tests it
-discriminates), but not by a direct correctness statement.
-
-**Assumptions.**
-- [[A-QD-8.1]] `_rank_mod_p!` correctly computes matrix rank over
-  `Z_p` for prime `p`.
-- [[A-QD-8.2]] `p^(g - rank)` is the count of solutions of the
-  homogeneous linear system over `Z_p` with `g` unknowns and the
-  computed rank.
-
-**How to discharge.** Cross-check against an independent Brute-force
-counter on small examples (`g ≤ 4`, `modulus ∈ {3, 5, 7}`); for the
-algebraic argument cite a linear-algebra textbook.
-
-### Reidemeister invariance
-
-#### QD-2 — R3 invariance (the standing gap)
-
-**Claim.** If diagrams `D₁` and `D₂` differ by a single Reidemeister-3
-move, their `quandle_descriptor` outputs are equal.
-
-**Why valuable.** PROOF-NEEDS M2 covers R1 and R2; R3 is the standing
-gap. Without R3 we do not have full Reidemeister equivalence — the
-invariant is incomplete.
-
-**Assumptions.**
-- [[A-QD-2.1]] R1 + R2 + R3 generate isotopy on classical knot
-  diagrams (Reidemeister 1927 — standard).
-- [[A-QD-2.2]] R3 acts on the fundamental quandle as a permutation
-  of generators (standard quandle-theoretic result).
-
-**How to discharge.** Either:
-1. Contribute `r3_simplify` to `KnotTheory.jl` upstream (the right
-   long-term home), or
-2. Construct R3-related PD pairs by hand for a small corpus
-   (trefoil, figure-eight) and verify `quandle_descriptor` equality.
-
-#### QD-12 — Read-only API guarantee
-
-**Claim.** No HTTP endpoint in `server/serve.jl` invokes a mutating
-operation on the Skein.jl database.
-
-**Why valuable.** `.claude/CLAUDE.md` states "Server is read-only
-(database mutations via Skein.jl REPL)" as a convention. Promoting
-this to a *checked* invariant prevents accidental mutation creep.
-
-**Assumptions.**
-- [[A-QD-12.1]] All Skein.jl mutating operations are identifiable by
-  name (e.g., `store!`, `delete!`, `update!`).
-
-**How to discharge.** Static check: `grep -E '(store!|delete!|update!)'
-server/serve.jl` returns empty. Add as a CI gate.
-
-### FFI / ABI
-
-#### QD-5 — Idris2 ABI ↔ Zig FFI layout agreement
-
-(Re-statement of PROOF-NEEDS S2.)
-
-**Claim.** Every record type defined in `src/abi/Types.idr` has a
-byte-for-byte identical memory layout in the corresponding Zig
-struct in `src/ffi/semantic_ffi.zig` and the BEAM NIF in
-`beam/native/quandle_db_nif.zig`.
-
-**Why valuable.** Standard FFI hazard. Currently *declared* by the
-existence of both files but not *proved*.
-
-**Assumptions.**
-- [[A-QD-5.1]] Idris2's `HasSize` / `HasAlignment` instances are
-  correct for the platforms targeted.
-- [[A-QD-5.2]] Zig's `extern struct` layout is C-ABI compatible.
-
-**How to discharge.** Encode layouts directly in Idris2 dependent
-types; emit a compile-time check in Zig (`@sizeOf`, `@alignOf`,
-`@offsetOf`); cross-check at the BEAM NIF boundary with `bit_size`.
-
-#### QD-6 — BEAM NIF never crashes the VM
-
-(Re-statement of PROOF-NEEDS S3.)
-
-**Claim.** For every input the Elixir side can pass to a NIF in
-`beam/native/quandle_db_nif.zig`, the NIF either returns a valid
-result, an `:error` term, or raises a NIF exception — but never
-crashes the BEAM VM.
-
-**Why valuable.** Production-critical. A NIF crash brings down the
-whole VM.
-
-**Assumptions.**
-- [[A-QD-6.1]] Zig's safety guarantees (no UB on well-typed code in
-  Release-Safe mode) hold for the NIF code paths.
-- [[A-QD-6.2]] Elixir-side input types are validated before the NIF
-  call (typespec discipline).
-
-**How to discharge.** Fuzz harness on the NIF boundary: random bytes
-+ random tagged-tuple shapes → NIF → assert "no VM crash". Combine
-with Dialyzer for the typespec discipline.
-
-## 4. The "stupid proof" exclusions
-
-For completeness, we do **not** pursue:
-
-- _"`QuandlePresentation` has these fields"_ — Julia struct
-  definition.
-- _"`extract_presentation` returns a `QuandlePresentation`"_ — Julia
-  type assertion.
-- _"BLAKE3 is collision-resistant"_ — cryptographic primitive
-  assumption ([[A-QD-4.1]]).
-- _"SHA-256 is collision-resistant"_ — same.
-- _"union-find converges in nearly-linear amortised time"_ — Tarjan
-  1975, out of scope.
-
-## 5. How to add a new obligation
-
-1. Add a row to [PROOF-NEEDS.md](PROOF-NEEDS.md) with `QD-N` id,
-   category (M, S, ABI), prover, priority, effort.
-2. Add the narrative entry here with statement, _why valuable_,
-   status, **assumptions**, _how to discharge_. Assumptions block is
-   non-optional.
-3. Each new assumption gets an entry in
-   [ASSUMPTIONS.md](ASSUMPTIONS.md) with `A-QD-N.M` id and
-   MATH/DESIGN/EMPIRICAL/CRYPTO classification.
-
-## 6. References
-
-- Core algorithms: [`server/quandle_semantic.jl`](server/quandle_semantic.jl).
-- Property tests: [`server/test_quandle_axioms.jl`](server/test_quandle_axioms.jl).
-- Server: [`server/serve.jl`](server/serve.jl).
-- KRL parser: [`server/krl/`](server/krl/).
-- BEAM NIF: [`beam/`](beam/).
-- ABI: [`src/abi/`](src/abi/), [`src/ffi/`](src/ffi/).
-- Companion narratives:
-  `hyperpolymath/krl/PROOF-NARRATIVE.md` — KRL surface
-  `hyperpolymath/tangle/PROOF-NARRATIVE.md` — Tangle semantic core
-
-## 7. Mathematical references
-
-- Joyce 1982 — _A classifying invariant of knots, the knot quandle_.
-- Matveev 1982 — _Distributive groupoids in knot theory_ (parallel
-  introduction of quandles).
-- Reidemeister 1927 — _Elementare Begründung der Knotentheorie_
-  (R1+R2+R3 generation).
-- Kauffman _Knots and Physics_ — colouring count and dihedral
-  quandle as concrete invariant.
-- Eisermann _The number of knot group representations_ —
-  faithfulness of the fundamental quandle on prime alternating knots.
diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
new file mode 100644
index 0000000..20791b2
--- /dev/null
+++ b/PROOF-NEEDS.adoc
@@ -0,0 +1,196 @@
+== PROOF-NEEDS — QuandleDB
+
+Mathematical and systems obligations for the quandle semantic layer.
+
+=== Mathematical obligations
+
+==== M1. Quandle axioms preserved
+
+Statement: For every `+QuandlePresentation+` produced by
+`+extract_presentation+`, the derived action satisfies the three quandle
+axioms:
+
+[arabic]
+. `+a ▷ a = a+` (idempotence)
+. For every `+a+`, the map `+x ↦ x ▷ a+` is a bijection
+(right-invertibility)
+. `+(a ▷ b) ▷ c = (a ▷ c) ▷ (b ▷ c)+` (right self-distributivity)
+
+Current status: *property-tested* (2026-04-12). - All three axioms
+verified algebraically for the dihedral quandle Z_p at p ∈ \{3, 5, 7,
+11, 13} — see `+server/test_quandle_axioms.jl+` § 1. - Structural
+consistency of extracted presentations verified for standard knots
+(trefoil, figure-eight, cinquefoil) — see § 2. - Remaining gap: formal
+proof that `+extract_presentation+` produces a valid Wirtinger
+presentation for arbitrary connected PD codes.
+
+==== M2. Reidemeister invariance
+
+Statement: If diagrams D₁ and D₂ differ by a single Reidemeister move,
+their extracted presentations produce the same fingerprint.
+
+Current status: *property-tested for R1 and R2* (2026-04-12). - R1: kink
+injection + `+r1_simplify+` verified to reduce crossing count and
+generator count — see `+server/test_quandle_axioms.jl+` § 5. - R2: braid
+word `+s1.S1.s1.s1.s1+` (trefoil + bigon) after `+r2_simplify+` gives
+same dihedral colouring counts as canonical trefoil — § 6. - R3: not yet
+covered (no programmatic R3-inverse available in KnotTheory.jl). -
+Remaining gap: R3 invariance; formal proof via Wirtinger presentation
+isomorphism under each move type.
+
+==== M3. Canonicalisation is idempotent
+
+Statement:
+`+canonicalize_presentation(canonicalize_presentation(p)) == canonicalize_presentation(p)+`.
+
+Current status: *property-tested* (2026-04-12). Verified for trefoil,
+figure-eight, cinquefoil — see `+server/test_quandle_axioms.jl+` § 3.
+
+==== M4. Colouring count well-definedness
+
+Statement: For a finite quandle Q and a presentation p, the number of
+quandle homomorphisms from `+fundamental(p)+` to Q depends only on the
+isomorphism class of `+fundamental(p)+` — not on the particular
+presentation.
+
+Current status: this is a standard result; need to verify the
+implementation actually respects it.
+
+=== Systems obligations
+
+==== S1. Fingerprint determinism across platforms
+
+Statement: Given identical input bytes, `+quandle_fingerprint+` produces
+identical output bytes on Linux x86_64, Linux aarch64, macOS, and
+WebAssembly.
+
+Current status: single-platform tested only.
+
+==== S2. Idris2 ABI ↔ Zig FFI layout agreement
+
+Statement: Every record type defined in `+src/abi/Types.idr+` has a
+byte-for-byte identical memory layout in the corresponding Zig struct in
+`+src/ffi/semantic_ffi.zig+`.
+
+Current status: declared, not proved. Idris2’s dependent types could
+encode the layout directly — this is exactly what the ABI/FFI boundary
+discipline is for.
+
+==== S3. NIF safety
+
+Statement: BEAM NIFs in `+beam/native/quandle_db_nif.zig+` never crash
+the BEAM VM, even on malformed input from the Elixir side.
+
+Current status: tested on well-formed inputs only. No fuzz on the NIF
+boundary.
+
+=== Proof stack (intended)
+
+* *Idris2* for ABI layout / type-level invariants
+* *Property-based tests (Julia)* for mathematical invariants M1-M4 as
+empirical evidence
+* *Zig’s comptime* for layout assertions at the FFI boundary
+* *BEAM Dialyzer* for NIF typespec discipline
+
+=== Implementation-level obligations (2026-06-01 audit extension)
+
+The original M1–M4 / S1–S3 obligations above are mathematical and
+systems contracts. The 2026-06-01 audit added implementation-level
+obligations that complete the proof narrative. Full statements with _why
+valuable_, status, explicit assumptions, and _how to discharge_ are in
+PROOF-NARRATIVE.md. Summary:
+
+[width="100%",cols="6%,22%,20%,20%,16%,16%",options="header",]
+|===
+|# |Statement |Category |Priority |Effort |Status
+|QD-1 |`+extract_presentation+` well-formed on arbitrary connected PD
+codes |M |P1 |3d |NOT STARTED (generalises Q-PresentationWF from 3 knots
+to full input space)
+
+|QD-2 |R3 invariance |M |P1 |5d (or upstream PR to KnotTheory.jl)
+|BLOCKED on `+r3_simplify+` (stated standing gap in M2)
+
+|QD-3 |Colouring-count well-definedness |M |P1 |2d |NOT STARTED (was M4)
+
+|QD-4 |Fingerprint determinism across platforms |S |P2 |1d (CI matrix)
+|NOT STARTED (was S1)
+
+|QD-5 |Idris2 ABI ↔ Zig FFI layout agreement |ABI |P2 |3d |NOT STARTED
+(was S2)
+
+|QD-6 |BEAM NIF never crashes the VM |S |P1 |1w (fuzz harness) |NOT
+STARTED (was S3)
+
+|QD-7 |Canonical-form ordering is total |M |P3 |1h (structural; see
+narrative) |NOT STARTED
+
+|QD-8 |`+_dihedral_colouring_count+` correctness |M |P2 |2d |NOT STARTED
+
+|QD-9 |Union-find traversal-order independence |M / impl |P2 |2h
+(shuffle test) |NOT STARTED
+
+|QD-10 |KRL parser accepts exactly v0.1.0 grammar |M / impl |P1 |4h
+(differential test) |NOT STARTED (cross-references KRL repo KR-6)
+
+|QD-11 |SQL→KRL translation semantics-preserving |M / impl |P2 |3d |NOT
+STARTED
+
+|QD-12 |Read-only API guarantee |S |P3 |1h (CI grep gate) |NOT STARTED
+|===
+
+=== Categories
+
+[width="100%",cols="24%,36%,40%",options="header",]
+|===
+|Code |Meaning |Applies?
+|M |Mathematical obligations |Yes (M1–M4 + QD-1, QD-2, QD-3, QD-7, QD-8,
+QD-9, QD-10, QD-11)
+
+|S |Systems obligations |Yes (S1–S3 + QD-4, QD-6, QD-12)
+
+|ABI |ABI/FFI obligations |Yes (QD-5)
+|===
+
+=== How to propose a new obligation
+
+[arabic]
+. State claim precisely.
+. Classify: mathematical, systems, or contract.
+. Either add property-based test as empirical evidence, OR write formal
+proof under `+verification/+` (create that dir if needed).
+. Add the narrative entry (statement, _why valuable_, status,
+assumptions, _how to discharge_) to PROOF-NARRATIVE.md. The assumptions
+block is non-optional.
+. Each new assumption gets an entry in ASSUMPTIONS.md with `+A-QD-N.M+`
+id and MATH/DESIGN/EMPIRICAL/CRYPTO classification.
+. Move to "`Currently verified`" section (to be created) when
+discharged.
+
+=== Dangerous patterns (BANNED)
+
+CI rejects any PR introducing these:
+
+[width="100%",cols="33%,35%,32%",options="header",]
+|===
+|Pattern |Language |Meaning
+|`+believe_me+` |Idris2 |Unsafe cast
+|`+assert_total+` |Idris2 |Skip totality check
+|`+postulate+` |Idris2 / Agda |Unproven axiom
+|`+sorry+` |Lean 4 |Incomplete proof
+|`+Admitted+` |Coq |Incomplete proof
+|`+Obj.magic+` |OCaml |Unsafe cast
+|`+unsafeCoerce+` |Haskell |Unsafe cast
+|`+unsafe+` (unaudited) |Rust / Zig |Unsafe block without safety comment
+|===
+
+Enforced by `+panic-attack assail --proofs-only+`.
+
+=== References
+
+* Algorithms:
+link:server/quandle_semantic.jl[`+server/quandle_semantic.jl+`]
+* Tests:
+link:server/test_quandle_axioms.jl[`+server/test_quandle_axioms.jl+`]
+* Companion narratives: `+hyperpolymath/krl/PROOF-NARRATIVE.md+` — KRL
+surface `+hyperpolymath/tangle/PROOF-NARRATIVE.md+` — Tangle semantic
+core
diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
deleted file mode 100644
index a252fe5..0000000
--- a/PROOF-NEEDS.md
+++ /dev/null
@@ -1,159 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
-
-# PROOF-NEEDS — QuandleDB
-
-Mathematical and systems obligations for the quandle semantic layer.
-
-## Mathematical obligations
-
-### M1. Quandle axioms preserved
-Statement: For every `QuandlePresentation` produced by `extract_presentation`,
-the derived action satisfies the three quandle axioms:
-
-1. `a ▷ a = a` (idempotence)
-2. For every `a`, the map `x ↦ x ▷ a` is a bijection (right-invertibility)
-3. `(a ▷ b) ▷ c = (a ▷ c) ▷ (b ▷ c)` (right self-distributivity)
-
-Current status: **property-tested** (2026-04-12).
-- All three axioms verified algebraically for the dihedral quandle Z_p at
-  p ∈ {3, 5, 7, 11, 13} — see `server/test_quandle_axioms.jl` § 1.
-- Structural consistency of extracted presentations verified for standard
-  knots (trefoil, figure-eight, cinquefoil) — see § 2.
-- Remaining gap: formal proof that `extract_presentation` produces a
-  valid Wirtinger presentation for arbitrary connected PD codes.
-
-### M2. Reidemeister invariance
-Statement: If diagrams D₁ and D₂ differ by a single Reidemeister move,
-their extracted presentations produce the same fingerprint.
-
-Current status: **property-tested for R1 and R2** (2026-04-12).
-- R1: kink injection + `r1_simplify` verified to reduce crossing count and
-  generator count — see `server/test_quandle_axioms.jl` § 5.
-- R2: braid word `s1.S1.s1.s1.s1` (trefoil + bigon) after `r2_simplify`
-  gives same dihedral colouring counts as canonical trefoil — § 6.
-- R3: not yet covered (no programmatic R3-inverse available in KnotTheory.jl).
-- Remaining gap: R3 invariance; formal proof via Wirtinger presentation
-  isomorphism under each move type.
-
-### M3. Canonicalisation is idempotent
-Statement: `canonicalize_presentation(canonicalize_presentation(p)) ==
-canonicalize_presentation(p)`.
-
-Current status: **property-tested** (2026-04-12).
-Verified for trefoil, figure-eight, cinquefoil — see
-`server/test_quandle_axioms.jl` § 3.
-
-### M4. Colouring count well-definedness
-Statement: For a finite quandle Q and a presentation p, the number of
-quandle homomorphisms from `fundamental(p)` to Q depends only on the
-isomorphism class of `fundamental(p)` — not on the particular presentation.
-
-Current status: this is a standard result; need to verify the
-implementation actually respects it.
-
-## Systems obligations
-
-### S1. Fingerprint determinism across platforms
-Statement: Given identical input bytes, `quandle_fingerprint` produces
-identical output bytes on Linux x86_64, Linux aarch64, macOS, and WebAssembly.
-
-Current status: single-platform tested only.
-
-### S2. Idris2 ABI ↔ Zig FFI layout agreement
-Statement: Every record type defined in `src/abi/Types.idr` has a
-byte-for-byte identical memory layout in the corresponding Zig struct
-in `src/ffi/semantic_ffi.zig`.
-
-Current status: declared, not proved. Idris2's dependent types could
-encode the layout directly — this is exactly what the ABI/FFI boundary
-discipline is for.
-
-### S3. NIF safety
-Statement: BEAM NIFs in `beam/native/quandle_db_nif.zig` never crash the
-BEAM VM, even on malformed input from the Elixir side.
-
-Current status: tested on well-formed inputs only. No fuzz on the NIF boundary.
-
-## Proof stack (intended)
-
-- **Idris2** for ABI layout / type-level invariants
-- **Property-based tests (Julia)** for mathematical invariants M1-M4 as
-  empirical evidence
-- **Zig's comptime** for layout assertions at the FFI boundary
-- **BEAM Dialyzer** for NIF typespec discipline
-
-## Implementation-level obligations (2026-06-01 audit extension)
-
-The original M1–M4 / S1–S3 obligations above are mathematical and
-systems contracts. The 2026-06-01 audit added implementation-level
-obligations that complete the proof narrative. Full statements with
-_why valuable_, status, explicit assumptions, and _how to discharge_
-are in [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). Summary:
-
-| # | Statement | Category | Priority | Effort | Status |
-|---|-----------|----------|----------|--------|--------|
-| QD-1 | `extract_presentation` well-formed on arbitrary connected PD codes | M | P1 | 3d | NOT STARTED (generalises Q-PresentationWF from 3 knots to full input space) |
-| QD-2 | R3 invariance | M | P1 | 5d (or upstream PR to KnotTheory.jl) | BLOCKED on `r3_simplify` (stated standing gap in M2) |
-| QD-3 | Colouring-count well-definedness | M | P1 | 2d | NOT STARTED (was M4) |
-| QD-4 | Fingerprint determinism across platforms | S | P2 | 1d (CI matrix) | NOT STARTED (was S1) |
-| QD-5 | Idris2 ABI ↔ Zig FFI layout agreement | ABI | P2 | 3d | NOT STARTED (was S2) |
-| QD-6 | BEAM NIF never crashes the VM | S | P1 | 1w (fuzz harness) | NOT STARTED (was S3) |
-| QD-7 | Canonical-form ordering is total | M | P3 | 1h (structural; see narrative) | NOT STARTED |
-| QD-8 | `_dihedral_colouring_count` correctness | M | P2 | 2d | NOT STARTED |
-| QD-9 | Union-find traversal-order independence | M / impl | P2 | 2h (shuffle test) | NOT STARTED |
-| QD-10 | KRL parser accepts exactly v0.1.0 grammar | M / impl | P1 | 4h (differential test) | NOT STARTED (cross-references KRL repo KR-6) |
-| QD-11 | SQL→KRL translation semantics-preserving | M / impl | P2 | 3d | NOT STARTED |
-| QD-12 | Read-only API guarantee | S | P3 | 1h (CI grep gate) | NOT STARTED |
-
-## Categories
-
-| Code | Meaning | Applies? |
-|------|---------|----------|
-| M | Mathematical obligations | Yes (M1–M4 + QD-1, QD-2, QD-3, QD-7, QD-8, QD-9, QD-10, QD-11) |
-| S | Systems obligations | Yes (S1–S3 + QD-4, QD-6, QD-12) |
-| ABI | ABI/FFI obligations | Yes (QD-5) |
-
-## How to propose a new obligation
-
-1. State claim precisely.
-2. Classify: mathematical, systems, or contract.
-3. Either add property-based test as empirical evidence, OR write formal
-   proof under `verification/` (create that dir if needed).
-4. Add the narrative entry (statement, _why valuable_, status,
-   assumptions, _how to discharge_) to
-   [PROOF-NARRATIVE.md](PROOF-NARRATIVE.md). The assumptions block is
-   non-optional.
-5. Each new assumption gets an entry in
-   [ASSUMPTIONS.md](ASSUMPTIONS.md) with `A-QD-N.M` id and
-   MATH/DESIGN/EMPIRICAL/CRYPTO classification.
-6. Move to "Currently verified" section (to be created) when discharged.
-
-## Dangerous patterns (BANNED)
-
-CI rejects any PR introducing these:
-
-| Pattern | Language | Meaning |
-|---------|----------|---------|
-| `believe_me` | Idris2 | Unsafe cast |
-| `assert_total` | Idris2 | Skip totality check |
-| `postulate` | Idris2 / Agda | Unproven axiom |
-| `sorry` | Lean 4 | Incomplete proof |
-| `Admitted` | Coq | Incomplete proof |
-| `Obj.magic` | OCaml | Unsafe cast |
-| `unsafeCoerce` | Haskell | Unsafe cast |
-| `unsafe` (unaudited) | Rust / Zig | Unsafe block without safety comment |
-
-Enforced by `panic-attack assail --proofs-only`.
-
-## References
-
-- Algorithms: [`server/quandle_semantic.jl`](server/quandle_semantic.jl)
-- Tests: [`server/test_quandle_axioms.jl`](server/test_quandle_axioms.jl)
-- Companion narratives:
-  `hyperpolymath/krl/PROOF-NARRATIVE.md` — KRL surface
-  `hyperpolymath/tangle/PROOF-NARRATIVE.md` — Tangle semantic core
-
diff --git a/READINESS.adoc b/READINESS.adoc
new file mode 100644
index 0000000..a52700f
--- /dev/null
+++ b/READINESS.adoc
@@ -0,0 +1,66 @@
+== Component Readiness — QuandleDB
+
+*Current Grade:* D *Assessed:* 2026-04-05 *Standard:*
+link:../../standards/component-readiness-grades/[CRG v2.0 STRICT]
+
+=== Grade rationale (evidence for D)
+
+Works on some things + partial RSR compliance. QuandleDB is a polyglot
+project: Julia HTTP server (Skein.jl wrapper) + Julia semantic sidecar +
+Idris2 ABI + Zig FFI + zig API + Elixir BEAM NIFs.
+
+==== Evidence
+
+* *Tests:* 21 passing (9 quandle extraction + 12 semantic index
+integration)
+* *Components present:*
+** `+server/serve.jl+` — HTTP server with quandle_semantic_index SQLite
+sidecar
+** `+server/quandle_semantic.jl+` — QuandleSemantic module (presentation
+extraction + hashing)
+** `+src/abi/Types.idr+` — Idris2 ABI type layer
+** `+src/ffi/semantic_ffi.zig+` — Zig FFI layer
+** `+src/api/*.v+` — zig API triples
+** `+beam/+` — Elixir BEAM client with NIFs
+* *RSR compliance:* Partial. Has 5 per-directory READMEs.
+0-AI-MANIFEST.a2ml present (template). `+.machine_readable/6a2/+`
+directory exists.
+* *CI:* panic-attack assail 0 findings.
+
+=== Gaps preventing higher grades
+
+==== Blocks C (works reliably + annotated)
+
+* [line-through]#No EXPLAINME.adoc, TEST-NEEDS.md, PROOF-NEEDS.md at
+repo root.# _(Added)_
+* Julia server code has no docstrings.
+* [line-through]#Elixir BEAM layer has no dedicated test coverage
+documented here.# _(Added Unit, P2P, Aspect, and Benchmark coverage)_
+* No integration tests spanning the full Idris2 → Zig → V → Julia →
+Elixir stack.
+* No dogfooding evidence — has anyone actually driven this end-to-end?
+* Only 4 commits in history before absorption into nextgen-databases
+monorepo.
+
+==== Blocks B
+
+* Requires C first.
+
+=== What to do for C
+
+[arabic]
+. [line-through]#Add EXPLAINME.adoc explaining the polyglot architecture
+and its intended users.# _(Done)_
+. [line-through]#Add TEST-NEEDS.md documenting what’s tested at each
+language layer and what isn’t.# _(Done)_
+. Write docstrings for `+server/serve.jl+`,
+`+server/quandle_semantic.jl+`.
+. Add per-language READMEs at `+src/abi/+`, `+src/ffi/+`, `+src/api/+`,
+`+beam/+` explaining what each layer contributes.
+. Demonstrate a full-stack dogfood: invoke Idris2 ABI-verified call,
+through Zig FFI, via zig API, hitting Julia server, surfacing via BEAM
+NIF, and have a real test assert on it.
+
+=== Review cycle
+
+Reassess after the full-stack dogfood test exists.
diff --git a/READINESS.md b/READINESS.md
deleted file mode 100644
index 6a3a72f..0000000
--- a/READINESS.md
+++ /dev/null
@@ -1,56 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
-
-# Component Readiness — QuandleDB
-
-**Current Grade:** D
-**Assessed:** 2026-04-05
-**Standard:** [CRG v2.0 STRICT](../../standards/component-readiness-grades/)
-
-## Grade rationale (evidence for D)
-
-Works on some things + partial RSR compliance. QuandleDB is a polyglot project:
-Julia HTTP server (Skein.jl wrapper) + Julia semantic sidecar + Idris2 ABI +
-Zig FFI + zig API + Elixir BEAM NIFs.
-
-### Evidence
-
-- **Tests:** 21 passing (9 quandle extraction + 12 semantic index integration)
-- **Components present:**
-  - `server/serve.jl` — HTTP server with quandle_semantic_index SQLite sidecar
-  - `server/quandle_semantic.jl` — QuandleSemantic module (presentation extraction + hashing)
-  - `src/abi/Types.idr` — Idris2 ABI type layer
-  - `src/ffi/semantic_ffi.zig` — Zig FFI layer
-  - `src/api/*.v` — zig API triples
-  - `beam/` — Elixir BEAM client with NIFs
-- **RSR compliance:** Partial. Has 5 per-directory READMEs. 0-AI-MANIFEST.a2ml
-  present (template). `.machine_readable/6a2/` directory exists.
-- **CI:** panic-attack assail 0 findings.
-
-## Gaps preventing higher grades
-
-### Blocks C (works reliably + annotated)
-- ~~No EXPLAINME.adoc, TEST-NEEDS.md, PROOF-NEEDS.md at repo root.~~ *(Added)*
-- Julia server code has no docstrings.
-- ~~Elixir BEAM layer has no dedicated test coverage documented here.~~ *(Added Unit, P2P, Aspect, and Benchmark coverage)*
-- No integration tests spanning the full Idris2 → Zig → V → Julia → Elixir stack.
-- No dogfooding evidence — has anyone actually driven this end-to-end?
-- Only 4 commits in history before absorption into nextgen-databases monorepo.
-
-### Blocks B
-- Requires C first.
-
-## What to do for C
-
-1. ~~Add EXPLAINME.adoc explaining the polyglot architecture and its intended users.~~ *(Done)*
-2. ~~Add TEST-NEEDS.md documenting what's tested at each language layer and what isn't.~~ *(Done)*
-3. Write docstrings for `server/serve.jl`, `server/quandle_semantic.jl`.
-4. Add per-language READMEs at `src/abi/`, `src/ffi/`, `src/api/`, `beam/`
-   explaining what each layer contributes.
-5. Demonstrate a full-stack dogfood: invoke Idris2 ABI-verified call, through
-   Zig FFI, via zig API, hitting Julia server, surfacing via BEAM NIF, and
-   have a real test assert on it.
-
-## Review cycle
-
-Reassess after the full-stack dogfood test exists.
diff --git a/SECURITY.adoc b/SECURITY.adoc
new file mode 100644
index 0000000..5670516
--- /dev/null
+++ b/SECURITY.adoc
@@ -0,0 +1,434 @@
+== Security Policy
+
+We take security seriously. We appreciate your efforts to responsibly
+disclose vulnerabilities and will make every effort to acknowledge your
+contributions.
+
+=== Table of Contents
+
+* link:#reporting-a-vulnerability[Reporting a Vulnerability]
+* link:#what-to-include[What to Include]
+* link:#response-timeline[Response Timeline]
+* link:#disclosure-policy[Disclosure Policy]
+* link:#scope[Scope]
+* link:#safe-harbour[Safe Harbour]
+* link:#recognition[Recognition]
+* link:#security-updates[Security Updates]
+* link:#security-best-practices[Security Best Practices]
+
+'''''
+
+=== Reporting a Vulnerability
+
+==== Preferred Method: GitHub Security Advisories
+
+The preferred method for reporting security vulnerabilities is through
+GitHub’s Security Advisory feature:
+
+[arabic]
+. Navigate to
+https://github.com/hyperpolymath/quandledb/security/advisories/new[Report
+a Vulnerability]
+. Click *"`Report a vulnerability`"*
+. Complete the form with as much detail as possible
+. Submit — we’ll receive a private notification
+
+This method ensures:
+
+* End-to-end encryption of your report
+* Private discussion space for collaboration
+* Coordinated disclosure tooling
+* Automatic credit when the advisory is published
+
+==== Alternative: Email
+
+If you cannot use GitHub Security Advisories, email us directly at
+j.d.a.jewell@open.ac.uk. No PGP key is currently published; for an
+encrypted channel, request one via a GitHub Security Advisory.
+
+____
+*⚠️ Important:* Do not report security vulnerabilities through public
+GitHub issues, pull requests, discussions, or social media.
+____
+
+'''''
+
+=== What to Include
+
+A good vulnerability report helps us understand and reproduce the issue
+quickly.
+
+==== Required Information
+
+* *Description*: Clear explanation of the vulnerability
+* *Impact*: What an attacker could achieve (confidentiality, integrity,
+availability)
+* *Affected versions*: Which versions/commits are affected
+* *Reproduction steps*: Detailed steps to reproduce the issue
+
+==== Helpful Additional Information
+
+* *Proof of concept*: Code, scripts, or screenshots demonstrating the
+vulnerability
+* *Attack scenario*: Realistic attack scenario showing exploitability
+* *CVSS score*: Your assessment of severity (use
+https://www.first.org/cvss/calculator/3.1[CVSS 3.1 Calculator])
+* *CWE ID*: Common Weakness Enumeration identifier if known
+* *Suggested fix*: If you have ideas for remediation
+* *References*: Links to related vulnerabilities, research, or
+advisories
+
+==== Example Report Structure
+
+[source,markdown]
+----
+## Summary
+[One-sentence description of the vulnerability]
+
+## Vulnerability Type
+[e.g., SQL Injection, XSS, SSRF, Path Traversal, etc.]
+
+## Affected Component
+[File path, function name, API endpoint, etc.]
+
+## Affected Versions
+[Version range or specific commits]
+
+## Severity Assessment
+- CVSS 3.1 Score: [X.X]
+- CVSS Vector: [CVSS:3.1/AV:X/AC:X/PR:X/UI:X/S:X/C:X/I:X/A:X]
+
+## Description
+[Detailed technical description]
+
+## Steps to Reproduce
+1. [First step]
+2. [Second step]
+3. [...]
+
+## Proof of Concept
+[Code, curl commands, screenshots, etc.]
+
+## Impact
+[What can an attacker achieve?]
+
+## Suggested Remediation
+[Optional: your ideas for fixing]
+
+## References
+[Links to related issues, CVEs, research]
+----
+
+'''''
+
+=== Response Timeline
+
+We commit to the following response times:
+
+[width="100%",cols="24%,35%,41%",options="header",]
+|===
+|Stage |Timeframe |Description
+|*Initial Response* |48 hours |We acknowledge receipt and confirm we’re
+investigating
+
+|*Triage* |7 days |We assess severity, confirm the vulnerability, and
+estimate timeline
+
+|*Status Update* |Every 7 days |Regular updates on remediation progress
+
+|*Resolution* |90 days |Target for fix development and release (complex
+issues may take longer)
+
+|*Disclosure* |90 days |Public disclosure after fix is available
+(coordinated with you)
+|===
+
+____
+*Note:* These are targets, not guarantees. Complex vulnerabilities may
+require more time. We’ll communicate openly about any delays.
+____
+
+'''''
+
+=== Disclosure Policy
+
+We follow *coordinated disclosure* (also known as responsible
+disclosure):
+
+[arabic]
+. *You report* the vulnerability privately
+. *We acknowledge* and begin investigation
+. *We develop* a fix and prepare a release
+. *We coordinate* disclosure timing with you
+. *We publish* security advisory and fix simultaneously
+. *You may publish* your research after disclosure
+
+==== Our Commitments
+
+* We will not take legal action against researchers who follow this
+policy
+* We will work with you to understand and resolve the issue
+* We will credit you in the security advisory (unless you prefer
+anonymity)
+* We will notify you before public disclosure
+* We will publish advisories with sufficient detail for users to assess
+risk
+
+==== Your Commitments
+
+* Report vulnerabilities promptly after discovery
+* Give us reasonable time to address the issue before disclosure
+* Do not access, modify, or delete data beyond what’s necessary to
+demonstrate the vulnerability
+* Do not degrade service availability (no DoS testing on production)
+* Do not share vulnerability details with others until coordinated
+disclosure
+
+==== Disclosure Timeline
+
+....
+Day 0          You report vulnerability
+Day 1-2        We acknowledge receipt
+Day 7          We confirm vulnerability and share initial assessment
+Day 7-90       We develop and test fix
+Day 90         Coordinated public disclosure
+               (earlier if fix is ready; later by mutual agreement)
+....
+
+If we cannot reach agreement on disclosure timing, we default to 90 days
+from your initial report.
+
+'''''
+
+=== Scope
+
+==== In Scope ✅
+
+The following are within scope for security research:
+
+* This repository (`+hyperpolymath/quandledb+`) and all its code
+* Official releases and packages published from this repository
+* Documentation that could lead to security issues
+* Build and deployment configurations in this repository
+* Dependencies (report here, we’ll coordinate with upstream)
+
+==== Out of Scope ❌
+
+The following are *not* in scope:
+
+* Third-party services we integrate with (report directly to them)
+* Social engineering attacks against maintainers
+* Physical security
+* Denial of service attacks against production infrastructure
+* Spam, phishing, or other non-technical attacks
+* Issues already reported or publicly known
+* Theoretical vulnerabilities without proof of concept
+
+==== Qualifying Vulnerabilities
+
+We’re particularly interested in:
+
+* Remote code execution
+* SQL injection, command injection, code injection
+* Authentication/authorisation bypass
+* Cross-site scripting (XSS) and cross-site request forgery (CSRF)
+* Server-side request forgery (SSRF)
+* Path traversal / local file inclusion
+* Information disclosure (credentials, PII, secrets)
+* Cryptographic weaknesses
+* Deserialisation vulnerabilities
+* Memory safety issues (buffer overflows, use-after-free, etc.)
+* Supply chain vulnerabilities (dependency confusion, etc.)
+* Significant logic flaws
+
+==== Non-Qualifying Issues
+
+The following generally do not qualify as security vulnerabilities:
+
+* Missing security headers on non-sensitive pages
+* Clickjacking on pages without sensitive actions
+* Self-XSS (requires victim to paste code)
+* Missing rate limiting (unless it enables a specific attack)
+* Username/email enumeration (unless high-risk context)
+* Missing cookie flags on non-sensitive cookies
+* Software version disclosure
+* Verbose error messages (unless exposing secrets)
+* Best practice deviations without demonstrable impact
+
+'''''
+
+=== Safe Harbour
+
+We support security research conducted in good faith.
+
+==== Our Promise
+
+If you conduct security research in accordance with this policy:
+
+* ✅ We will not initiate legal action against you
+* ✅ We will not report your activity to law enforcement
+* ✅ We will work with you in good faith to resolve issues
+* ✅ We consider your research authorised under the Computer Fraud and
+Abuse Act (CFAA), UK Computer Misuse Act, and similar laws
+* ✅ We waive any potential claim against you for circumvention of
+security controls
+
+==== Good Faith Requirements
+
+To qualify for safe harbour, you must:
+
+* Comply with this security policy
+* Report vulnerabilities promptly
+* Avoid privacy violations (do not access others’ data)
+* Avoid service degradation (no destructive testing)
+* Not exploit vulnerabilities beyond proof-of-concept
+* Not use vulnerabilities for profit (beyond bug bounties where offered)
+
+____
+*⚠️ Important:* This safe harbour does not extend to third-party
+systems. Always check their policies before testing.
+____
+
+'''''
+
+=== Recognition
+
+We believe in recognising security researchers who help us improve.
+
+==== Hall of Fame
+
+Researchers who report valid vulnerabilities will be acknowledged in our
+link:SECURITY-ACKNOWLEDGMENTS.md[Security Acknowledgments] (unless they
+prefer anonymity).
+
+Recognition includes:
+
+* Your name (or chosen alias)
+* Link to your website/profile (optional)
+* Brief description of the vulnerability class
+* Date of report
+
+==== What We Offer
+
+* ✅ Public credit in security advisories
+* ✅ Acknowledgment in release notes
+* ✅ Entry in our Hall of Fame
+* ✅ Reference/recommendation letter upon request (for significant
+findings)
+
+==== What We Don’t Currently Offer
+
+* ❌ Monetary bug bounties
+* ❌ Hardware or swag
+* ❌ Paid security research contracts
+
+____
+*Note:* We’re a community project with limited resources. Your
+contributions help everyone who uses this software.
+____
+
+'''''
+
+=== Security Updates
+
+==== Receiving Updates
+
+To stay informed about security updates:
+
+* *Watch this repository*: Click "`Watch`" → "`Custom`" → Select
+"`Security alerts`"
+* *GitHub Security Advisories*: Published at
+https://github.com/hyperpolymath/quandledb/security/advisories[Security
+Advisories]
+* *Release notes*: Security fixes noted in link:CHANGELOG.md[CHANGELOG]
+
+==== Update Policy
+
+[cols=",",options="header",]
+|===
+|Severity |Response
+|*Critical/High* |Patch release as soon as fix is ready
+|*Medium* |Included in next scheduled release (or earlier)
+|*Low* |Included in next scheduled release
+|===
+
+==== Supported Versions
+
+[cols=",,",options="header",]
+|===
+|Version |Supported |Notes
+|`+main+` branch |✅ Yes |Latest development
+|Latest release |✅ Yes |Current stable
+|Previous minor release |✅ Yes |Security fixes backported
+|Older versions |❌ No |Please upgrade
+|===
+
+'''''
+
+=== Security Best Practices
+
+When using QuandleDB, we recommend:
+
+==== General
+
+* Keep dependencies up to date
+* Use the latest stable release
+* Subscribe to security notifications
+* Review configuration against security documentation
+* Follow principle of least privilege
+
+==== For Contributors
+
+* Never commit secrets, credentials, or API keys
+* Use signed commits (`+git config commit.gpgsign true+`)
+* Review dependencies before adding them
+* Run security linters locally before pushing
+* Report any concerns about existing code
+
+'''''
+
+=== Additional Resources
+
+* https://github.com/hyperpolymath/quandledb/security/advisories[Security
+Advisories]
+* link:CHANGELOG.md[Changelog]
+* link:CONTRIBUTING.md[Contributing Guidelines]
+* https://cve.mitre.org/[CVE Database]
+* https://www.first.org/cvss/calculator/3.1[CVSS Calculator]
+
+'''''
+
+=== Contact
+
+[width="100%",cols="50%,50%",options="header",]
+|===
+|Purpose |Contact
+|*Security issues*
+|https://github.com/hyperpolymath/quandledb/security/advisories/new[Report
+via GitHub] or j.d.a.jewell@open.ac.uk
+
+|*General questions*
+|https://github.com/hyperpolymath/quandledb/discussions[GitHub
+Discussions]
+
+|*Other enquiries* |See link:README.md[README] for contact information
+|===
+
+'''''
+
+=== Policy Changes
+
+This security policy may be updated from time to time. Significant
+changes will be:
+
+* Committed to this repository with a clear commit message
+* Noted in the changelog
+* Announced via GitHub Discussions (for major changes)
+
+'''''
+
+_Thank you for helping keep QuandleDB and its users safe._ 🛡️
+
+'''''
+
+Last updated: 2026 · Policy version: 1.0.0
diff --git a/SECURITY.md b/SECURITY.md
deleted file mode 100644
index 0896543..0000000
--- a/SECURITY.md
+++ /dev/null
@@ -1,373 +0,0 @@
-# Security Policy
-
-We take security seriously. We appreciate your efforts to responsibly disclose vulnerabilities and will make every effort to acknowledge your contributions.
-
-## Table of Contents
-
-- [Reporting a Vulnerability](#reporting-a-vulnerability)
-- [What to Include](#what-to-include)
-- [Response Timeline](#response-timeline)
-- [Disclosure Policy](#disclosure-policy)
-- [Scope](#scope)
-- [Safe Harbour](#safe-harbour)
-- [Recognition](#recognition)
-- [Security Updates](#security-updates)
-- [Security Best Practices](#security-best-practices)
-
----
-
-## Reporting a Vulnerability
-
-### Preferred Method: GitHub Security Advisories
-
-The preferred method for reporting security vulnerabilities is through GitHub's Security Advisory feature:
-
-1. Navigate to [Report a Vulnerability](https://github.com/hyperpolymath/quandledb/security/advisories/new)
-2. Click **"Report a vulnerability"**
-3. Complete the form with as much detail as possible
-4. Submit — we'll receive a private notification
-
-This method ensures:
-
-- End-to-end encryption of your report
-- Private discussion space for collaboration
-- Coordinated disclosure tooling
-- Automatic credit when the advisory is published
-
-### Alternative: Email
-
-If you cannot use GitHub Security Advisories, email us directly at
-j.d.a.jewell@open.ac.uk. No PGP key is currently
-published; for an encrypted channel, request one via a GitHub Security
-Advisory.
-
-> **⚠️ Important:** Do not report security vulnerabilities through public GitHub issues, pull requests, discussions, or social media.
-
----
-
-## What to Include
-
-A good vulnerability report helps us understand and reproduce the issue quickly.
-
-### Required Information
-
-- **Description**: Clear explanation of the vulnerability
-- **Impact**: What an attacker could achieve (confidentiality, integrity, availability)
-- **Affected versions**: Which versions/commits are affected
-- **Reproduction steps**: Detailed steps to reproduce the issue
-
-### Helpful Additional Information
-
-- **Proof of concept**: Code, scripts, or screenshots demonstrating the vulnerability
-- **Attack scenario**: Realistic attack scenario showing exploitability
-- **CVSS score**: Your assessment of severity (use [CVSS 3.1 Calculator](https://www.first.org/cvss/calculator/3.1))
-- **CWE ID**: Common Weakness Enumeration identifier if known
-- **Suggested fix**: If you have ideas for remediation
-- **References**: Links to related vulnerabilities, research, or advisories
-
-### Example Report Structure
-
-```markdown
-## Summary
-[One-sentence description of the vulnerability]
-
-## Vulnerability Type
-[e.g., SQL Injection, XSS, SSRF, Path Traversal, etc.]
-
-## Affected Component
-[File path, function name, API endpoint, etc.]
-
-## Affected Versions
-[Version range or specific commits]
-
-## Severity Assessment
-- CVSS 3.1 Score: [X.X]
-- CVSS Vector: [CVSS:3.1/AV:X/AC:X/PR:X/UI:X/S:X/C:X/I:X/A:X]
-
-## Description
-[Detailed technical description]
-
-## Steps to Reproduce
-1. [First step]
-2. [Second step]
-3. [...]
-
-## Proof of Concept
-[Code, curl commands, screenshots, etc.]
-
-## Impact
-[What can an attacker achieve?]
-
-## Suggested Remediation
-[Optional: your ideas for fixing]
-
-## References
-[Links to related issues, CVEs, research]
-```
-
----
-
-## Response Timeline
-
-We commit to the following response times:
-
-| Stage | Timeframe | Description |
-|-------|-----------|-------------|
-| **Initial Response** | 48 hours | We acknowledge receipt and confirm we're investigating |
-| **Triage** | 7 days | We assess severity, confirm the vulnerability, and estimate timeline |
-| **Status Update** | Every 7 days | Regular updates on remediation progress |
-| **Resolution** | 90 days | Target for fix development and release (complex issues may take longer) |
-| **Disclosure** | 90 days | Public disclosure after fix is available (coordinated with you) |
-
-> **Note:** These are targets, not guarantees. Complex vulnerabilities may require more time. We'll communicate openly about any delays.
-
----
-
-## Disclosure Policy
-
-We follow **coordinated disclosure** (also known as responsible disclosure):
-
-1. **You report** the vulnerability privately
-2. **We acknowledge** and begin investigation
-3. **We develop** a fix and prepare a release
-4. **We coordinate** disclosure timing with you
-5. **We publish** security advisory and fix simultaneously
-6. **You may publish** your research after disclosure
-
-### Our Commitments
-
-- We will not take legal action against researchers who follow this policy
-- We will work with you to understand and resolve the issue
-- We will credit you in the security advisory (unless you prefer anonymity)
-- We will notify you before public disclosure
-- We will publish advisories with sufficient detail for users to assess risk
-
-### Your Commitments
-
-- Report vulnerabilities promptly after discovery
-- Give us reasonable time to address the issue before disclosure
-- Do not access, modify, or delete data beyond what's necessary to demonstrate the vulnerability
-- Do not degrade service availability (no DoS testing on production)
-- Do not share vulnerability details with others until coordinated disclosure
-
-### Disclosure Timeline
-
-```
-Day 0          You report vulnerability
-Day 1-2        We acknowledge receipt
-Day 7          We confirm vulnerability and share initial assessment
-Day 7-90       We develop and test fix
-Day 90         Coordinated public disclosure
-               (earlier if fix is ready; later by mutual agreement)
-```
-
-If we cannot reach agreement on disclosure timing, we default to 90 days from your initial report.
-
----
-
-## Scope
-
-### In Scope ✅
-
-The following are within scope for security research:
-
-- This repository (`hyperpolymath/quandledb`) and all its code
-- Official releases and packages published from this repository
-- Documentation that could lead to security issues
-- Build and deployment configurations in this repository
-- Dependencies (report here, we'll coordinate with upstream)
-
-### Out of Scope ❌
-
-The following are **not** in scope:
-
-- Third-party services we integrate with (report directly to them)
-- Social engineering attacks against maintainers
-- Physical security
-- Denial of service attacks against production infrastructure
-- Spam, phishing, or other non-technical attacks
-- Issues already reported or publicly known
-- Theoretical vulnerabilities without proof of concept
-
-### Qualifying Vulnerabilities
-
-We're particularly interested in:
-
-- Remote code execution
-- SQL injection, command injection, code injection
-- Authentication/authorisation bypass
-- Cross-site scripting (XSS) and cross-site request forgery (CSRF)
-- Server-side request forgery (SSRF)
-- Path traversal / local file inclusion
-- Information disclosure (credentials, PII, secrets)
-- Cryptographic weaknesses
-- Deserialisation vulnerabilities
-- Memory safety issues (buffer overflows, use-after-free, etc.)
-- Supply chain vulnerabilities (dependency confusion, etc.)
-- Significant logic flaws
-
-### Non-Qualifying Issues
-
-The following generally do not qualify as security vulnerabilities:
-
-- Missing security headers on non-sensitive pages
-- Clickjacking on pages without sensitive actions
-- Self-XSS (requires victim to paste code)
-- Missing rate limiting (unless it enables a specific attack)
-- Username/email enumeration (unless high-risk context)
-- Missing cookie flags on non-sensitive cookies
-- Software version disclosure
-- Verbose error messages (unless exposing secrets)
-- Best practice deviations without demonstrable impact
-
----
-
-## Safe Harbour
-
-We support security research conducted in good faith.
-
-### Our Promise
-
-If you conduct security research in accordance with this policy:
-
-- ✅ We will not initiate legal action against you
-- ✅ We will not report your activity to law enforcement
-- ✅ We will work with you in good faith to resolve issues
-- ✅ We consider your research authorised under the Computer Fraud and Abuse Act (CFAA), UK Computer Misuse Act, and similar laws
-- ✅ We waive any potential claim against you for circumvention of security controls
-
-### Good Faith Requirements
-
-To qualify for safe harbour, you must:
-
-- Comply with this security policy
-- Report vulnerabilities promptly
-- Avoid privacy violations (do not access others' data)
-- Avoid service degradation (no destructive testing)
-- Not exploit vulnerabilities beyond proof-of-concept
-- Not use vulnerabilities for profit (beyond bug bounties where offered)
-
-> **⚠️ Important:** This safe harbour does not extend to third-party systems. Always check their policies before testing.
-
----
-
-## Recognition
-
-We believe in recognising security researchers who help us improve.
-
-### Hall of Fame
-
-Researchers who report valid vulnerabilities will be acknowledged in our [Security Acknowledgments](SECURITY-ACKNOWLEDGMENTS.md) (unless they prefer anonymity).
-
-Recognition includes:
-
-- Your name (or chosen alias)
-- Link to your website/profile (optional)
-- Brief description of the vulnerability class
-- Date of report
-
-### What We Offer
-
-- ✅ Public credit in security advisories
-- ✅ Acknowledgment in release notes
-- ✅ Entry in our Hall of Fame
-- ✅ Reference/recommendation letter upon request (for significant findings)
-
-### What We Don't Currently Offer
-
-- ❌ Monetary bug bounties
-- ❌ Hardware or swag
-- ❌ Paid security research contracts
-
-> **Note:** We're a community project with limited resources. Your contributions help everyone who uses this software.
-
----
-
-## Security Updates
-
-### Receiving Updates
-
-To stay informed about security updates:
-
-- **Watch this repository**: Click "Watch" → "Custom" → Select "Security alerts"
-- **GitHub Security Advisories**: Published at [Security Advisories](https://github.com/hyperpolymath/quandledb/security/advisories)
-- **Release notes**: Security fixes noted in [CHANGELOG](CHANGELOG.md)
-
-### Update Policy
-
-| Severity | Response |
-|----------|----------|
-| **Critical/High** | Patch release as soon as fix is ready |
-| **Medium** | Included in next scheduled release (or earlier) |
-| **Low** | Included in next scheduled release |
-
-### Supported Versions
-
-<!-- Adjust this table to match your actual version support policy -->
-
-| Version | Supported | Notes |
-|---------|-----------|-------|
-| `main` branch | ✅ Yes | Latest development |
-| Latest release | ✅ Yes | Current stable |
-| Previous minor release | ✅ Yes | Security fixes backported |
-| Older versions | ❌ No | Please upgrade |
-
----
-
-## Security Best Practices
-
-When using QuandleDB, we recommend:
-
-### General
-
-- Keep dependencies up to date
-- Use the latest stable release
-- Subscribe to security notifications
-- Review configuration against security documentation
-- Follow principle of least privilege
-
-### For Contributors
-
-- Never commit secrets, credentials, or API keys
-- Use signed commits (`git config commit.gpgsign true`)
-- Review dependencies before adding them
-- Run security linters locally before pushing
-- Report any concerns about existing code
-
----
-
-## Additional Resources
-
-- [Security Advisories](https://github.com/hyperpolymath/quandledb/security/advisories)
-- [Changelog](CHANGELOG.md)
-- [Contributing Guidelines](CONTRIBUTING.md)
-- [CVE Database](https://cve.mitre.org/)
-- [CVSS Calculator](https://www.first.org/cvss/calculator/3.1)
-
----
-
-## Contact
-
-| Purpose | Contact |
-|---------|---------|
-| **Security issues** | [Report via GitHub](https://github.com/hyperpolymath/quandledb/security/advisories/new) or j.d.a.jewell@open.ac.uk |
-| **General questions** | [GitHub Discussions](https://github.com/hyperpolymath/quandledb/discussions) |
-| **Other enquiries** | See [README](README.md) for contact information |
-
----
-
-## Policy Changes
-
-This security policy may be updated from time to time. Significant changes will be:
-
-- Committed to this repository with a clear commit message
-- Noted in the changelog
-- Announced via GitHub Discussions (for major changes)
-
----
-
-*Thank you for helping keep QuandleDB and its users safe.* 🛡️
-
----
-
-<sub>Last updated: 2026 · Policy version: 1.0.0</sub>
diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc
new file mode 100644
index 0000000..175e5f5
--- /dev/null
+++ b/TEST-NEEDS.adoc
@@ -0,0 +1,84 @@
+== TEST-NEEDS — QuandleDB
+
+Honest accounting of test coverage across the polyglot stack.
+
+=== What’s tested today (21 assertions total)
+
+[width="100%",cols="34%,33%,33%",options="header",]
+|===
+|Layer |Tests |Location
+|Julia quandle extraction |9 |`+server/test_semantic_index.jl+`
+
+|Julia semantic index integration |12 |`+server/test_semantic_index.jl+`
+
+|Idris2 ABI |— |none
+
+|Zig FFI |— |none
+
+|zig API |— |none
+
+|BEAM NIFs |declared |`+beam/test/quandle_db_nif_test.exs+`,
+`+beam/test/quandle_db_nif_live_integration_test.exs+` (not run in
+estate-wide sweep)
+
+|Full-stack (Idris → Zig → V → Julia → BEAM) |— |none
+|===
+
+=== What’s NOT tested
+
+[width="100%",cols="34%,33%,33%",options="header",]
+|===
+|Category |Why missing |Priority
+|unit (per-layer) |Only Julia has explicit unit tests |high
+
+|P2P / cross-process |BEAM↔Julia link not stress-tested |medium
+
+|E2E (polyglot) |No test spans the full stack |high
+
+|build (all layers) |CI only builds Julia server; ABI/FFI/API/BEAM not
+verified in CI |high
+
+|property-based |No property tests for quandle fingerprint determinism,
+canonicalisation |high
+
+|mutation |Not set up anywhere |medium
+
+|fuzz |No fuzz harness for random knot diagrams |medium
+
+|contract |No OpenAPI / interface contract for HTTP endpoints |medium
+
+|regression |No named regression suite |medium
+
+|chaos |No fault injection (e.g. SQLite mid-write) |low
+
+|compatibility |Single-platform only |low
+
+|proof-regression |Idris2 ABI has types but no discharged proofs |medium
+|===
+
+=== Highest-value tests to add next (for CRG grade D → C)
+
+[arabic]
+. *Quandle fingerprint determinism* (property-based): Same input diagram
+→ same fingerprint hash, across N=100+ random test diagrams.
+. *Quandle fingerprint canonicalisation*: For known-equivalent
+presentations (e.g. Reidemeister moves applied), fingerprint matches.
+. *Colouring count on known knots*: Trefoil, figure-eight, unknot
+against expected colouring counts into Z/3, Z/5.
+. *BEAM ↔ Julia NIF handshake*: BEAM test actually loads the NIF and
+executes a quandle extraction end-to-end.
+. *Full-stack smoke*: Idris2-typed call → Zig FFI → V → Julia server →
+round-trip result.
+
+=== How to add new tests
+
+For Julia: - Add to `+server/test_semantic_index.jl+` under an
+appropriate `+@testset+`. - Run with
+`+julia --project=server -e 'include("server/test_semantic_index.jl")'+`.
+
+For BEAM: - Add to `+beam/test/quandle_db_nif_test.exs+`. - Run with
+`+cd beam && mix test+`.
+
+For full-stack integration: - Create `+tests/integration/+` at repo
+root. - Script the Idris2→Zig→V→Julia→BEAM handshake with assertions at
+each layer.
diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md
deleted file mode 100644
index 3f5f74f..0000000
--- a/TEST-NEEDS.md
+++ /dev/null
@@ -1,62 +0,0 @@
-<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
-<!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
-
-# TEST-NEEDS — QuandleDB
-
-Honest accounting of test coverage across the polyglot stack.
-
-## What's tested today (21 assertions total)
-
-| Layer | Tests | Location |
-|---|---|---|
-| Julia quandle extraction | 9 | `server/test_semantic_index.jl` |
-| Julia semantic index integration | 12 | `server/test_semantic_index.jl` |
-| Idris2 ABI | — | none |
-| Zig FFI | — | none |
-| zig API | — | none |
-| BEAM NIFs | declared | `beam/test/quandle_db_nif_test.exs`, `beam/test/quandle_db_nif_live_integration_test.exs` (not run in estate-wide sweep) |
-| Full-stack (Idris → Zig → V → Julia → BEAM) | — | none |
-
-## What's NOT tested
-
-| Category | Why missing | Priority |
-|---|---|---|
-| unit (per-layer) | Only Julia has explicit unit tests | high |
-| P2P / cross-process | BEAM↔Julia link not stress-tested | medium |
-| E2E (polyglot) | No test spans the full stack | high |
-| build (all layers) | CI only builds Julia server; ABI/FFI/API/BEAM not verified in CI | high |
-| property-based | No property tests for quandle fingerprint determinism, canonicalisation | high |
-| mutation | Not set up anywhere | medium |
-| fuzz | No fuzz harness for random knot diagrams | medium |
-| contract | No OpenAPI / interface contract for HTTP endpoints | medium |
-| regression | No named regression suite | medium |
-| chaos | No fault injection (e.g. SQLite mid-write) | low |
-| compatibility | Single-platform only | low |
-| proof-regression | Idris2 ABI has types but no discharged proofs | medium |
-
-## Highest-value tests to add next (for CRG grade D → C)
-
-1. **Quandle fingerprint determinism** (property-based):
-   Same input diagram → same fingerprint hash, across N=100+ random test diagrams.
-2. **Quandle fingerprint canonicalisation**:
-   For known-equivalent presentations (e.g. Reidemeister moves applied), fingerprint matches.
-3. **Colouring count on known knots**:
-   Trefoil, figure-eight, unknot against expected colouring counts into Z/3, Z/5.
-4. **BEAM ↔ Julia NIF handshake**:
-   BEAM test actually loads the NIF and executes a quandle extraction end-to-end.
-5. **Full-stack smoke**:
-   Idris2-typed call → Zig FFI → V → Julia server → round-trip result.
-
-## How to add new tests
-
-For Julia:
-- Add to `server/test_semantic_index.jl` under an appropriate `@testset`.
-- Run with `julia --project=server -e 'include("server/test_semantic_index.jl")'`.
-
-For BEAM:
-- Add to `beam/test/quandle_db_nif_test.exs`.
-- Run with `cd beam && mix test`.
-
-For full-stack integration:
-- Create `tests/integration/` at repo root.
-- Script the Idris2→Zig→V→Julia→BEAM handshake with assertions at each layer.
diff --git a/WHITEPAPER.adoc b/WHITEPAPER.adoc
new file mode 100644
index 0000000..ab18e5c
--- /dev/null
+++ b/WHITEPAPER.adoc
@@ -0,0 +1,477 @@
+== SPDX-License-Identifier: CC-BY-SA-4.0
+
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
+
+== KRL: A Knot-Theoretic Resolution Language for Topological Data
+
+*Author:* Jonathan D.A. Jewell *Version:* 1.0 *Date:* 2026-03-14
+*Status:* Design (v0.2.0 target)
+
+'''''
+
+=== Abstract
+
+We present KRL (Knot Resolution Language), a domain-specific resolution
+language for QuandleDB that treats mathematical equivalence as a
+first-class query primitive. Traditional database query languages (SQL,
+GraphQL, Cypher) model equality as a binary predicate: two values are
+either equal or not. This model is fundamentally inadequate for
+topological data, where two objects (e.g., knot diagrams) may be
+equivalent via multiple distinct paths (Reidemeister moves), and the
+space of equivalences itself has mathematical structure. KRL addresses
+this by grounding its semantics in Homotopy Type Theory (HoTT), where
+equality is not a boolean but a _type_—the type of paths between two
+objects. The result is a query language where equivalence queries return
+not just matching objects but the _derivations_ that establish
+equivalence, with provenance tracking that records which invariants
+contributed to each proof.
+
+'''''
+
+=== 1. Introduction
+
+==== 1.1 Knots and Databases
+
+A _knot_ is a closed curve embedded in three-dimensional space,
+considered up to ambient isotopy (continuous deformation without cutting
+or passing through itself). The classification of knots is a central
+problem in topology, with the KnotInfo database currently cataloguing
+over 350 million prime knots up to 19 crossings and 1.9 billion at 20
+crossings (Livingston & Moore, 2024).
+
+Querying knot databases presents a challenge unlike any in relational,
+document, or graph databases: *equality is hard*. Two knot diagrams may
+look completely different yet represent the same knot, distinguishable
+only through a sequence of Reidemeister moves (local diagrammatic
+transformations) or through the computation of algebraic invariants
+(Jones polynomial, knot group, etc.). No single invariant is
+complete—there exist distinct knots with identical Jones polynomials—so
+equivalence often requires combining multiple invariants and sometimes
+remains unresolvable.
+
+==== 1.2 Why Not SQL?
+
+SQL’s relational model fails for knot data in several fundamental ways:
+
+[arabic]
+. *Binary equality:* SQL’s `+WHERE a = b+` returns a boolean. For knots,
+`+a ≅ b+` should return the _space of equivalences_—a potentially
+non-trivial mathematical object.
+. *No compositional equivalence:* Two knots may be equivalent via
+different paths. SQL has no mechanism to distinguish or compose these
+paths.
+. *No invariant provenance:* When a query determines that two knots are
+equivalent, SQL cannot record _which invariants_ established the
+equivalence and with what confidence.
+. *Three-valued logic:* SQL’s NULL handling (three-valued logic)
+conflates "`unknown`" with "`inapplicable.`" For knot invariants, the
+distinction between "`genus not yet computed`" and "`genus undefined for
+this object`" is mathematically significant.
+. *Type poverty:* SQL lacks sum types, dependent types, and generics—all
+necessary for representing the rich algebraic structures in knot theory.
+
+==== 1.3 Contributions
+
+This paper presents:
+
+[arabic]
+. *KRL’s semantic model* grounded in HoTT identity types, where
+equivalence queries return types, not booleans (Section 3).
+. *E-graph-backed execution* using equality saturation (egglog) to
+compactly represent equivalence classes (Section 4).
+. *Provenance-carrying results* that track which invariants contributed
+to each equivalence proof (Section 5).
+. *Category-theoretic schema* following Spivak’s CQL, where schema is a
+category and queries are functors (Section 6).
+. *Pipeline syntax* inspired by PRQL, with ASCII-art graph patterns from
+Cypher/GQL (Section 7).
+
+'''''
+
+=== 2. Mathematical Background
+
+==== 2.1 Knots and Invariants
+
+A _knot invariant_ is a function from knots to some algebraic structure
+that assigns the same value to equivalent knots. Key invariants include:
+
+[cols=",,",options="header",]
+|===
+|Invariant |Type |Completeness
+|Crossing number |ℕ |Very weak
+|Writhe |ℤ |Weak (diagram-dependent)
+|Genus |ℕ |Moderate
+|Jones polynomial |ℤ[t^±½] |Strong but not complete
+|Alexander polynomial |ℤ[t^±1] |Moderate
+|HOMFLY-PT polynomial |ℤ[a^±1, z^±1] |Strong
+|Knot group |Group presentation |Complete (but undecidable)
+|===
+
+No single computable invariant is known to be complete. In practice,
+equivalence is established by matching multiple invariants and, when
+necessary, finding an explicit isotopy.
+
+==== 2.2 Quandles
+
+A _quandle_ (Q, ▷) is a set Q with a binary operation ▷ satisfying:
+
+[arabic]
+. *Idempotence:* a ▷ a = a for all a ∈ Q.
+. *Right-invertibility:* For all a, b ∈ Q, there exists a unique c such
+that c ▷ a = b.
+. *Self-distributivity:* (a ▷ b) ▷ c = (a ▷ c) ▷ (b ▷ c) for all a, b, c
+∈ Q.
+
+The _fundamental quandle_ of a knot is a complete invariant—two knots
+are equivalent if and only if their fundamental quandles are isomorphic.
+However, quandle isomorphism is computationally expensive and not always
+practical.
+
+==== 2.3 Homotopy Type Theory
+
+In HoTT (Univalent Foundations Program, 2013), the identity type
+`+a =_A b+` is not a proposition (boolean) but a _type_—the type of
+paths from a to b. This type may be:
+
+* *Empty:* a and b are not equal (no path exists).
+* *Contractible:* a and b are _uniquely_ equal (exactly one path, up to
+homotopy).
+* *Non-trivial:* Multiple distinct paths exist, and the space of paths
+has mathematical structure.
+
+For knots, `+K₁ =_Knot K₂+` is the type of isotopies from K₁ to K₂. This
+type may contain multiple distinct isotopies (different sequences of
+Reidemeister moves), and these isotopies can themselves be
+compared—forming higher-dimensional structure.
+
+'''''
+
+=== 3. KRL Semantic Model
+
+==== 3.1 Equivalence as a Type
+
+KRL’s fundamental departure from SQL is that equivalence queries return
+_types_, not booleans:
+
+[source,krl]
+----
+from knots
+| where equivalent_to("3_1")
+| return equivalences
+----
+
+This query does not return a flat list of knot names. It returns, for
+each matching knot K, the _equivalence evidence_:
+
+....
+{
+  knot: K,
+  equivalence_type: [
+    { path: "jones_match", invariant: "jones_polynomial", confidence: "exact" },
+    { path: "genus_match", invariant: "genus", confidence: "exact" },
+    { path: "crossing_number_bound", invariant: "crossing_number", confidence: "necessary" }
+  ]
+}
+....
+
+==== 3.2 Identity Types in KRL
+
+KRL models three levels of identity:
+
+[arabic]
+. *Definitional equality* (`+==+`): Identical representations (same
+Gauss code). Decidable, trivial.
+. *Propositional equality* (`+≅+`): Equivalent via invariants. Returns a
+_proof term_ recording which invariants matched.
+. *Path equality* (`+~+`): Equivalent via explicit isotopy (sequence of
+Reidemeister moves). Returns the path itself.
+
+[source,krl]
+----
+from knots
+| where K ≅ "3_1" via [jones, genus, crossing_number]
+| return K, proof
+----
+
+==== 3.3 Quotient Types
+
+KRL represents equivalence classes as quotient types:
+
+....
+Knot / ≅ = { [K] | K ∈ Knot }
+....
+
+Queries on quotient types operate on equivalence classes rather than
+individual representatives, which is the mathematically natural
+operation for topological data.
+
+'''''
+
+=== 4. E-Graph Execution Engine
+
+==== 4.1 Equality Saturation
+
+KRL queries are executed against an _e-graph_ (equivalence graph), a
+data structure that compactly represents equivalence classes. Following
+the egglog paradigm (Willsey et al., PLDI 2023), KRL combines
+Datalog-style recursive queries with equality saturation:
+
+[source,krl]
+----
+# Define equivalence rules
+rule jones_equivalent(K1, K2) :-
+  knot(K1), knot(K2),
+  jones_polynomial(K1, J), jones_polynomial(K2, J),
+  K1 != K2.
+
+rule genus_equivalent(K1, K2) :-
+  knot(K1), knot(K2),
+  genus(K1, G), genus(K2, G).
+
+# Query: find equivalence class of trefoil
+from knots
+| where jones_equivalent(K, "3_1")
+| where genus_equivalent(K, "3_1")
+| return K, equivalence_class
+----
+
+==== 4.2 Stratified Invariant Evaluation
+
+Not all invariants are equally expensive to compute. KRL’s query planner
+evaluates invariants in order of increasing cost:
+
+[cols=",,",options="header",]
+|===
+|Stratum |Invariants |Cost
+|0 |Crossing number, writhe |O(1) lookup
+|1 |Genus, Seifert circles |O(n) computation
+|2 |Jones polynomial |O(2^n) in crossing number
+|3 |Alexander polynomial |O(n³) matrix determinant
+|4 |HOMFLY-PT polynomial |O(2^n) or worse
+|5 |Fundamental quandle |Undecidable in general
+|===
+
+Early strata can _refute_ equivalence quickly (different crossing
+numbers immediately prove non-equivalence), while later strata provide
+stronger evidence for equivalence.
+
+'''''
+
+=== 5. Provenance-Carrying Results
+
+==== 5.1 Semiring Annotations
+
+Following the provenance semiring framework (Green et al., 2007), KRL
+annotates every result with provenance information recording how the
+result was derived:
+
+....
+Result = (data, provenance)
+
+Provenance = Semiring(
+  invariant_used: Set[Invariant],
+  confidence: {exact, necessary, sufficient, heuristic},
+  computation_path: List[Step],
+  time_cost: Duration
+)
+....
+
+==== 5.2 Confidence Levels
+
+[width="100%",cols="28%,36%,36%",options="header",]
+|===
+|Level |Meaning |Example
+|`+exact+` |Invariant matched exactly |Jones polynomials are identical
+
+|`+necessary+` |Matching is necessary but not sufficient |Same crossing
+number
+
+|`+sufficient+` |Matching is sufficient for equivalence |Quandle
+isomorphism
+
+|`+heuristic+` |Statistical or approximate |Tabulated classification
+|===
+
+'''''
+
+=== 6. Category-Theoretic Schema
+
+==== 6.1 Schema as Category
+
+Following Spivak (2014), KRL models the database schema as a category C:
+
+* *Objects:* Entity types (Knot, Invariant, Isotopy, Diagram).
+* *Morphisms:* Relationships (has_invariant, has_diagram,
+isotopy_between).
+* *Functors:* Data instances (I : C → Set) mapping schema to data.
+
+==== 6.2 Queries as Functors
+
+A KRL query is a functor Q : C → C’ between schema categories. This
+provides:
+
+* *Compositionality:* Queries compose as functors compose.
+* *Type safety:* Functors preserve categorical structure, preventing
+ill-typed queries at the schema level.
+* *Data migration:* Schema changes are functors, with automatic data
+migration.
+
+'''''
+
+=== 7. Surface Syntax
+
+==== 7.1 Pipeline Syntax
+
+KRL adopts PRQL’s pipeline approach for readability:
+
+[source,krl]
+----
+from knots
+| filter crossing_number <= 10
+| filter genus == 1
+| sort jones_polynomial
+| take 20
+| return name, crossing_number, jones_polynomial
+----
+
+==== 7.2 Equivalence Queries
+
+[source,krl]
+----
+from knots
+| find_equivalent "3_1" via [jones, genus]
+| return equivalences with provenance
+----
+
+==== 7.3 Graph Patterns
+
+For navigating relationships between knots (e.g., knots related by
+specific operations like connected sum):
+
+[source,krl]
+----
+from knots as K1
+| match (K1)-[:CONNECTED_SUM]->(K2)
+| where K2.crossing_number < K1.crossing_number
+| return K1.name, K2.name
+----
+
+==== 7.4 Reidemeister Move Queries
+
+[source,krl]
+----
+from diagrams as D1
+| find_path D1 ~> "3_1" via reidemeister
+| return path, move_count
+----
+
+'''''
+
+=== 8. Implementation
+
+==== 8.1 Architecture
+
+[cols=",,",options="header",]
+|===
+|Layer |Language |Purpose
+|Engine |Julia (Skein.jl) |Knot storage, invariant computation
+|Query Parser |Julia |KRL parsing and AST construction
+|E-graph Engine |Julia |Equality saturation, equivalence classes
+|API |Julia (HTTP.jl) |REST API for queries
+|Frontend |ReScript + React |Interactive query interface
+|ABI |Idris2 |Formal verification of query semantics
+|FFI |Zig |C-ABI bridge for external consumers
+|===
+
+==== 8.2 Data Model
+
+QuandleDB stores knots as records with extensible invariant fields:
+
+[source,julia]
+----
+struct KnotRecord
+    name::String
+    gauss_code::Vector{Int}
+    crossing_number::Int
+    writhe::Int
+    genus::Union{Int, Nothing}
+    jones_polynomial::Union{String, Nothing}
+    metadata::Dict{String, String}
+end
+----
+
+'''''
+
+=== 9. Related Work
+
+==== 9.1 Database Query Languages
+
+* *SQL* (Codd, 1970): Relational algebra with binary equality. No
+support for structured equivalences.
+* *Cypher* (Robinson et al., 2015): Graph pattern matching. Useful for
+navigating knot relationships but no equivalence semantics.
+* *PRQL* (PRQL Project, 2022): Pipeline syntax for SQL. KRL adopts its
+ergonomics but not its relational semantics.
+* *HoTTSQL* (Chu et al., PLDI 2017): SQL semantics via HoTT. Proves
+equivalence of SQL queries, not of data. KRL adapts HoTT for data
+equivalence.
+* *egglog* (Willsey et al., PLDI 2023): Equality saturation + Datalog.
+KRL’s execution engine.
+* *CQL* (Spivak, 2014): Categorical Query Language. KRL’s schema model.
+
+==== 9.2 Knot Theory Software
+
+* *SnapPy* (Culler et al.): 3-manifold topology. Computations, not
+queries.
+* *KnotInfo* (Livingston & Moore): Web database. SQL backend, no KRL.
+* *Knot Atlas*: Wiki-based. No structured query language.
+* *Skein.jl* (hyperpolymath): Julia knot engine. KRL’s computation
+backend.
+
+==== 9.3 Type Theory and Equality
+
+* *HoTT* (Univalent Foundations, 2013): Identity types as paths. KRL’s
+semantic foundation.
+* *Cubical Agda* (Vezzosi et al., 2019): Computational HoTT. Potential
+future implementation target.
+* *Lean 4 mathlib* (mathlib Community): Formal quandle definitions.
+KRL’s proof library.
+
+'''''
+
+=== 10. Conclusion
+
+KRL demonstrates that domain-specific query languages can and should
+respect the mathematical structure of their data. For topological data,
+binary equality is the wrong abstraction. By grounding query semantics
+in HoTT identity types, executing queries via equality saturation, and
+carrying provenance through results, KRL provides a resolution language
+that is mathematically honest about what it means for two knots to be
+"`the same.`"
+
+The broader lesson is that the choice of equality model is a fundamental
+design decision for any query language, and different domains may
+require different models. SQL’s binary equality is appropriate for
+business data where two customer IDs are either the same or different.
+But for scientific data—knots, molecular structures, geometric
+objects—equality is richer, and our query languages should reflect that
+richness.
+
+'''''
+
+=== References
+
+[arabic]
+. Chu, S. et al. (2017). "`HoTTSQL: Proving Query Rewrites with
+Univalent SQL Semantics.`" _PLDI 2017_, 510–524.
+. Codd, E. F. (1970). "`A Relational Model of Data for Large Shared Data
+Banks.`" _Communications of the ACM_, 13(6), 377–387.
+. Green, T. J. et al. (2007). "`Provenance Semirings.`" _PODS 2007_,
+31–40.
+. Livingston, C. & Moore, A. H. (2024). _KnotInfo: Table of Knot
+Invariants_. https://www.indiana.edu/~knotinfo
+. Spivak, D. I. (2014). _Category Theory for the Sciences_. MIT Press.
+. The Univalent Foundations Program. (2013). _Homotopy Type Theory:
+Univalent Foundations of Mathematics_.
+. Willsey, M. et al. (2023). "`Better Together: Unifying Datalog and
+Equality Saturation.`" _PLDI 2023_, 468–486.
diff --git a/WHITEPAPER.md b/WHITEPAPER.md
deleted file mode 100644
index e3818e3..0000000
--- a/WHITEPAPER.md
+++ /dev/null
@@ -1,439 +0,0 @@
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-
-# KRL: A Knot-Theoretic Resolution Language for Topological Data
-
-**Author:** Jonathan D.A. Jewell
-**Version:** 1.0
-**Date:** 2026-03-14
-**Status:** Design (v0.2.0 target)
-
----
-
-## Abstract
-
-We present KRL (Knot Resolution Language), a domain-specific resolution language for
-QuandleDB that treats mathematical equivalence as a first-class query primitive.
-Traditional database query languages (SQL, GraphQL, Cypher) model equality as a
-binary predicate: two values are either equal or not. This model is fundamentally
-inadequate for topological data, where two objects (e.g., knot diagrams) may be
-equivalent via multiple distinct paths (Reidemeister moves), and the space of
-equivalences itself has mathematical structure. KRL addresses this by grounding
-its semantics in Homotopy Type Theory (HoTT), where equality is not a boolean
-but a *type*—the type of paths between two objects. The result is a query language
-where equivalence queries return not just matching objects but the *derivations*
-that establish equivalence, with provenance tracking that records which invariants
-contributed to each proof.
-
----
-
-## 1. Introduction
-
-### 1.1 Knots and Databases
-
-A *knot* is a closed curve embedded in three-dimensional space, considered up to
-ambient isotopy (continuous deformation without cutting or passing through itself).
-The classification of knots is a central problem in topology, with the KnotInfo
-database currently cataloguing over 350 million prime knots up to 19 crossings
-and 1.9 billion at 20 crossings (Livingston & Moore, 2024).
-
-Querying knot databases presents a challenge unlike any in relational, document,
-or graph databases: **equality is hard**. Two knot diagrams may look completely
-different yet represent the same knot, distinguishable only through a sequence
-of Reidemeister moves (local diagrammatic transformations) or through the
-computation of algebraic invariants (Jones polynomial, knot group, etc.).
-No single invariant is complete—there exist distinct knots with identical Jones
-polynomials—so equivalence often requires combining multiple invariants and
-sometimes remains unresolvable.
-
-### 1.2 Why Not SQL?
-
-SQL's relational model fails for knot data in several fundamental ways:
-
-1. **Binary equality:** SQL's `WHERE a = b` returns a boolean. For knots,
-   `a ≅ b` should return the *space of equivalences*—a potentially non-trivial
-   mathematical object.
-
-2. **No compositional equivalence:** Two knots may be equivalent via different
-   paths. SQL has no mechanism to distinguish or compose these paths.
-
-3. **No invariant provenance:** When a query determines that two knots are
-   equivalent, SQL cannot record *which invariants* established the equivalence
-   and with what confidence.
-
-4. **Three-valued logic:** SQL's NULL handling (three-valued logic) conflates
-   "unknown" with "inapplicable." For knot invariants, the distinction between
-   "genus not yet computed" and "genus undefined for this object" is
-   mathematically significant.
-
-5. **Type poverty:** SQL lacks sum types, dependent types, and generics—all
-   necessary for representing the rich algebraic structures in knot theory.
-
-### 1.3 Contributions
-
-This paper presents:
-
-1. **KRL's semantic model** grounded in HoTT identity types, where equivalence
-   queries return types, not booleans (Section 3).
-2. **E-graph-backed execution** using equality saturation (egglog) to compactly
-   represent equivalence classes (Section 4).
-3. **Provenance-carrying results** that track which invariants contributed to
-   each equivalence proof (Section 5).
-4. **Category-theoretic schema** following Spivak's CQL, where schema is a
-   category and queries are functors (Section 6).
-5. **Pipeline syntax** inspired by PRQL, with ASCII-art graph patterns from
-   Cypher/GQL (Section 7).
-
----
-
-## 2. Mathematical Background
-
-### 2.1 Knots and Invariants
-
-A *knot invariant* is a function from knots to some algebraic structure that
-assigns the same value to equivalent knots. Key invariants include:
-
-| Invariant | Type | Completeness |
-|-----------|------|-------------|
-| Crossing number | ℕ | Very weak |
-| Writhe | ℤ | Weak (diagram-dependent) |
-| Genus | ℕ | Moderate |
-| Jones polynomial | ℤ[t^±½] | Strong but not complete |
-| Alexander polynomial | ℤ[t^±1] | Moderate |
-| HOMFLY-PT polynomial | ℤ[a^±1, z^±1] | Strong |
-| Knot group | Group presentation | Complete (but undecidable) |
-
-No single computable invariant is known to be complete. In practice, equivalence
-is established by matching multiple invariants and, when necessary, finding an
-explicit isotopy.
-
-### 2.2 Quandles
-
-A *quandle* (Q, ▷) is a set Q with a binary operation ▷ satisfying:
-
-1. **Idempotence:** a ▷ a = a for all a ∈ Q.
-2. **Right-invertibility:** For all a, b ∈ Q, there exists a unique c such that c ▷ a = b.
-3. **Self-distributivity:** (a ▷ b) ▷ c = (a ▷ c) ▷ (b ▷ c) for all a, b, c ∈ Q.
-
-The *fundamental quandle* of a knot is a complete invariant—two knots are
-equivalent if and only if their fundamental quandles are isomorphic. However,
-quandle isomorphism is computationally expensive and not always practical.
-
-### 2.3 Homotopy Type Theory
-
-In HoTT (Univalent Foundations Program, 2013), the identity type `a =_A b` is
-not a proposition (boolean) but a *type*—the type of paths from a to b.
-This type may be:
-
-- **Empty:** a and b are not equal (no path exists).
-- **Contractible:** a and b are *uniquely* equal (exactly one path, up to homotopy).
-- **Non-trivial:** Multiple distinct paths exist, and the space of paths has
-  mathematical structure.
-
-For knots, `K₁ =_Knot K₂` is the type of isotopies from K₁ to K₂. This type
-may contain multiple distinct isotopies (different sequences of Reidemeister
-moves), and these isotopies can themselves be compared—forming higher-dimensional
-structure.
-
----
-
-## 3. KRL Semantic Model
-
-### 3.1 Equivalence as a Type
-
-KRL's fundamental departure from SQL is that equivalence queries return *types*,
-not booleans:
-
-```krl
-from knots
-| where equivalent_to("3_1")
-| return equivalences
-```
-
-This query does not return a flat list of knot names. It returns, for each
-matching knot K, the *equivalence evidence*:
-
-```
-{
-  knot: K,
-  equivalence_type: [
-    { path: "jones_match", invariant: "jones_polynomial", confidence: "exact" },
-    { path: "genus_match", invariant: "genus", confidence: "exact" },
-    { path: "crossing_number_bound", invariant: "crossing_number", confidence: "necessary" }
-  ]
-}
-```
-
-### 3.2 Identity Types in KRL
-
-KRL models three levels of identity:
-
-1. **Definitional equality** (`==`): Identical representations (same Gauss code).
-   Decidable, trivial.
-
-2. **Propositional equality** (`≅`): Equivalent via invariants. Returns a
-   *proof term* recording which invariants matched.
-
-3. **Path equality** (`~`): Equivalent via explicit isotopy (sequence of
-   Reidemeister moves). Returns the path itself.
-
-```krl
-from knots
-| where K ≅ "3_1" via [jones, genus, crossing_number]
-| return K, proof
-```
-
-### 3.3 Quotient Types
-
-KRL represents equivalence classes as quotient types:
-
-```
-Knot / ≅ = { [K] | K ∈ Knot }
-```
-
-Queries on quotient types operate on equivalence classes rather than individual
-representatives, which is the mathematically natural operation for topological
-data.
-
----
-
-## 4. E-Graph Execution Engine
-
-### 4.1 Equality Saturation
-
-KRL queries are executed against an *e-graph* (equivalence graph), a data
-structure that compactly represents equivalence classes. Following the egglog
-paradigm (Willsey et al., PLDI 2023), KRL combines Datalog-style recursive
-queries with equality saturation:
-
-```krl
-# Define equivalence rules
-rule jones_equivalent(K1, K2) :-
-  knot(K1), knot(K2),
-  jones_polynomial(K1, J), jones_polynomial(K2, J),
-  K1 != K2.
-
-rule genus_equivalent(K1, K2) :-
-  knot(K1), knot(K2),
-  genus(K1, G), genus(K2, G).
-
-# Query: find equivalence class of trefoil
-from knots
-| where jones_equivalent(K, "3_1")
-| where genus_equivalent(K, "3_1")
-| return K, equivalence_class
-```
-
-### 4.2 Stratified Invariant Evaluation
-
-Not all invariants are equally expensive to compute. KRL's query planner
-evaluates invariants in order of increasing cost:
-
-| Stratum | Invariants | Cost |
-|---------|-----------|------|
-| 0 | Crossing number, writhe | O(1) lookup |
-| 1 | Genus, Seifert circles | O(n) computation |
-| 2 | Jones polynomial | O(2^n) in crossing number |
-| 3 | Alexander polynomial | O(n³) matrix determinant |
-| 4 | HOMFLY-PT polynomial | O(2^n) or worse |
-| 5 | Fundamental quandle | Undecidable in general |
-
-Early strata can *refute* equivalence quickly (different crossing numbers
-immediately prove non-equivalence), while later strata provide stronger
-evidence for equivalence.
-
----
-
-## 5. Provenance-Carrying Results
-
-### 5.1 Semiring Annotations
-
-Following the provenance semiring framework (Green et al., 2007), KRL annotates
-every result with provenance information recording how the result was derived:
-
-```
-Result = (data, provenance)
-
-Provenance = Semiring(
-  invariant_used: Set[Invariant],
-  confidence: {exact, necessary, sufficient, heuristic},
-  computation_path: List[Step],
-  time_cost: Duration
-)
-```
-
-### 5.2 Confidence Levels
-
-| Level | Meaning | Example |
-|-------|---------|---------|
-| `exact` | Invariant matched exactly | Jones polynomials are identical |
-| `necessary` | Matching is necessary but not sufficient | Same crossing number |
-| `sufficient` | Matching is sufficient for equivalence | Quandle isomorphism |
-| `heuristic` | Statistical or approximate | Tabulated classification |
-
----
-
-## 6. Category-Theoretic Schema
-
-### 6.1 Schema as Category
-
-Following Spivak (2014), KRL models the database schema as a category C:
-
-- **Objects:** Entity types (Knot, Invariant, Isotopy, Diagram).
-- **Morphisms:** Relationships (has_invariant, has_diagram, isotopy_between).
-- **Functors:** Data instances (I : C → Set) mapping schema to data.
-
-### 6.2 Queries as Functors
-
-A KRL query is a functor Q : C → C' between schema categories. This provides:
-
-- **Compositionality:** Queries compose as functors compose.
-- **Type safety:** Functors preserve categorical structure, preventing ill-typed
-  queries at the schema level.
-- **Data migration:** Schema changes are functors, with automatic data migration.
-
----
-
-## 7. Surface Syntax
-
-### 7.1 Pipeline Syntax
-
-KRL adopts PRQL's pipeline approach for readability:
-
-```krl
-from knots
-| filter crossing_number <= 10
-| filter genus == 1
-| sort jones_polynomial
-| take 20
-| return name, crossing_number, jones_polynomial
-```
-
-### 7.2 Equivalence Queries
-
-```krl
-from knots
-| find_equivalent "3_1" via [jones, genus]
-| return equivalences with provenance
-```
-
-### 7.3 Graph Patterns
-
-For navigating relationships between knots (e.g., knots related by specific
-operations like connected sum):
-
-```krl
-from knots as K1
-| match (K1)-[:CONNECTED_SUM]->(K2)
-| where K2.crossing_number < K1.crossing_number
-| return K1.name, K2.name
-```
-
-### 7.4 Reidemeister Move Queries
-
-```krl
-from diagrams as D1
-| find_path D1 ~> "3_1" via reidemeister
-| return path, move_count
-```
-
----
-
-## 8. Implementation
-
-### 8.1 Architecture
-
-| Layer | Language | Purpose |
-|-------|----------|---------|
-| Engine | Julia (Skein.jl) | Knot storage, invariant computation |
-| Query Parser | Julia | KRL parsing and AST construction |
-| E-graph Engine | Julia | Equality saturation, equivalence classes |
-| API | Julia (HTTP.jl) | REST API for queries |
-| Frontend | ReScript + React | Interactive query interface |
-| ABI | Idris2 | Formal verification of query semantics |
-| FFI | Zig | C-ABI bridge for external consumers |
-
-### 8.2 Data Model
-
-QuandleDB stores knots as records with extensible invariant fields:
-
-```julia
-struct KnotRecord
-    name::String
-    gauss_code::Vector{Int}
-    crossing_number::Int
-    writhe::Int
-    genus::Union{Int, Nothing}
-    jones_polynomial::Union{String, Nothing}
-    metadata::Dict{String, String}
-end
-```
-
----
-
-## 9. Related Work
-
-### 9.1 Database Query Languages
-
-- **SQL** (Codd, 1970): Relational algebra with binary equality. No support for
-  structured equivalences.
-- **Cypher** (Robinson et al., 2015): Graph pattern matching. Useful for
-  navigating knot relationships but no equivalence semantics.
-- **PRQL** (PRQL Project, 2022): Pipeline syntax for SQL. KRL adopts its
-  ergonomics but not its relational semantics.
-- **HoTTSQL** (Chu et al., PLDI 2017): SQL semantics via HoTT. Proves
-  equivalence of SQL queries, not of data. KRL adapts HoTT for data equivalence.
-- **egglog** (Willsey et al., PLDI 2023): Equality saturation + Datalog.
-  KRL's execution engine.
-- **CQL** (Spivak, 2014): Categorical Query Language. KRL's schema model.
-
-### 9.2 Knot Theory Software
-
-- **SnapPy** (Culler et al.): 3-manifold topology. Computations, not queries.
-- **KnotInfo** (Livingston & Moore): Web database. SQL backend, no KRL.
-- **Knot Atlas**: Wiki-based. No structured query language.
-- **Skein.jl** (hyperpolymath): Julia knot engine. KRL's computation backend.
-
-### 9.3 Type Theory and Equality
-
-- **HoTT** (Univalent Foundations, 2013): Identity types as paths. KRL's
-  semantic foundation.
-- **Cubical Agda** (Vezzosi et al., 2019): Computational HoTT. Potential
-  future implementation target.
-- **Lean 4 mathlib** (mathlib Community): Formal quandle definitions. KRL's
-  proof library.
-
----
-
-## 10. Conclusion
-
-KRL demonstrates that domain-specific query languages can and should respect
-the mathematical structure of their data. For topological data, binary equality
-is the wrong abstraction. By grounding query semantics in HoTT identity types,
-executing queries via equality saturation, and carrying provenance through
-results, KRL provides a resolution language that is mathematically honest about
-what it means for two knots to be "the same."
-
-The broader lesson is that the choice of equality model is a fundamental design
-decision for any query language, and different domains may require different
-models. SQL's binary equality is appropriate for business data where two customer
-IDs are either the same or different. But for scientific data—knots, molecular
-structures, geometric objects—equality is richer, and our query languages should
-reflect that richness.
-
----
-
-## References
-
-1. Chu, S. et al. (2017). "HoTTSQL: Proving Query Rewrites with Univalent SQL
-   Semantics." *PLDI 2017*, 510–524.
-2. Codd, E. F. (1970). "A Relational Model of Data for Large Shared Data Banks."
-   *Communications of the ACM*, 13(6), 377–387.
-3. Green, T. J. et al. (2007). "Provenance Semirings." *PODS 2007*, 31–40.
-4. Livingston, C. & Moore, A. H. (2024). *KnotInfo: Table of Knot Invariants*.
-   https://www.indiana.edu/~knotinfo
-5. Spivak, D. I. (2014). *Category Theory for the Sciences*. MIT Press.
-6. The Univalent Foundations Program. (2013). *Homotopy Type Theory: Univalent
-   Foundations of Mathematics*.
-7. Willsey, M. et al. (2023). "Better Together: Unifying Datalog and Equality
-   Saturation." *PLDI 2023*, 468–486.
diff --git a/beam/README.adoc b/beam/README.adoc
new file mode 100644
index 0000000..f469e04
--- /dev/null
+++ b/beam/README.adoc
@@ -0,0 +1,66 @@
+== QuandleDB NIF Scaffold
+
+Minimal Elixir + Zig NIF package for BEAM integration of QuandleDB
+semantic APIs.
+
+=== What This Scaffold Provides
+
+* Elixir wrapper module: `+QuandleDBNif+`
+* NIF loader module: `+QuandleDBNif.Native+`
+* Zig NIF library: `+native/quandle_db_nif.zig+`
+* Mix aliases: `+mix compile+` and `+mix test+` run `+nif.build+` first
+
+Current NIF functions are intentionally minimal shape-compatible stubs:
+
+* `+semantic_lookup/1+`
+* `+semantic_equivalents/1+`
+
+These calls are now wired through the semantic FFI boundary and can pull
+live data from the QuandleDB API:
+
+* `+GET /api/semantic/:name+`
+* `+GET /api/semantic-equivalents/:name+`
+
+Runtime environment flags:
+
+* `+QDB_API_BASE_URL+` (default: `+http://127.0.0.1:8080+`)
+* `+QDB_NIF_MODE+`:
+** `+live+` => use live HTTP calls
+** any other value or unset => stub mode (safe default for local tests)
+
+=== Build and Test
+
+[source,bash]
+----
+cd beam
+mix test
+----
+
+This compiles the Zig NIF into `+priv/quandle_db_nif.so+` (or platform
+equivalent) and runs Elixir tests.
+
+==== Optional Live Integration Tests
+
+Run NIF/API parity checks against a running QuandleDB server:
+
+[source,bash]
+----
+cd beam
+QDB_LIVE_TEST_BASE_URL=http://127.0.0.1:8080 mix test
+----
+
+Optional knot override:
+
+[source,bash]
+----
+QDB_LIVE_TEST_BASE_URL=http://127.0.0.1:8080 QDB_LIVE_TEST_KNOT=4_1 mix test
+----
+
+When `+QDB_LIVE_TEST_BASE_URL+` is set, the Mix test alias starts the
+NIF in `+live+` mode automatically.
+
+=== Next Wiring Step
+
+Replace the HTTP host implementation in `+native/quandle_db_nif.zig+`
+with a direct call path to a local semantic runtime (if you want to
+avoid network round-trips inside the NIF process).
diff --git a/beam/README.md b/beam/README.md
deleted file mode 100644
index 25a3820..0000000
--- a/beam/README.md
+++ /dev/null
@@ -1,62 +0,0 @@
-# QuandleDB NIF Scaffold
-
-Minimal Elixir + Zig NIF package for BEAM integration of QuandleDB semantic APIs.
-
-## What This Scaffold Provides
-
-- Elixir wrapper module: `QuandleDBNif`
-- NIF loader module: `QuandleDBNif.Native`
-- Zig NIF library: `native/quandle_db_nif.zig`
-- Mix aliases: `mix compile` and `mix test` run `nif.build` first
-
-Current NIF functions are intentionally minimal shape-compatible stubs:
-
-- `semantic_lookup/1`
-- `semantic_equivalents/1`
-
-These calls are now wired through the semantic FFI boundary and can pull live
-data from the QuandleDB API:
-
-- `GET /api/semantic/:name`
-- `GET /api/semantic-equivalents/:name`
-
-Runtime environment flags:
-
-- `QDB_API_BASE_URL` (default: `http://127.0.0.1:8080`)
-- `QDB_NIF_MODE`:
-  - `live` => use live HTTP calls
-  - any other value or unset => stub mode (safe default for local tests)
-
-## Build and Test
-
-```bash
-cd beam
-mix test
-```
-
-This compiles the Zig NIF into `priv/quandle_db_nif.so` (or platform equivalent)
-and runs Elixir tests.
-
-### Optional Live Integration Tests
-
-Run NIF/API parity checks against a running QuandleDB server:
-
-```bash
-cd beam
-QDB_LIVE_TEST_BASE_URL=http://127.0.0.1:8080 mix test
-```
-
-Optional knot override:
-
-```bash
-QDB_LIVE_TEST_BASE_URL=http://127.0.0.1:8080 QDB_LIVE_TEST_KNOT=4_1 mix test
-```
-
-When `QDB_LIVE_TEST_BASE_URL` is set, the Mix test alias starts the NIF in
-`live` mode automatically.
-
-## Next Wiring Step
-
-Replace the HTTP host implementation in `native/quandle_db_nif.zig` with a
-direct call path to a local semantic runtime (if you want to avoid network
-round-trips inside the NIF process).
diff --git a/docs/db-3-index-strategy.adoc b/docs/db-3-index-strategy.adoc
new file mode 100644
index 0000000..e7cecb5
--- /dev/null
+++ b/docs/db-3-index-strategy.adoc
@@ -0,0 +1,152 @@
+== DB-3 Index Strategy
+
+*Source:* PROOF-NARRATIVE.md §3 DB-3. Phase A audit 2026-06-01.
+
+This file is the *Phase A audit deliverable* for `+quandledb#33+`. It
+inventories every column in the `+quandle_semantic_index+` table,
+classifies its query-access pattern, and recommends an index strategy.
+
+=== Phase A — what’s done
+
+3 new indexes added to `+SEMANTIC_INDEX_STATEMENTS+` in
+`+server/serve.jl+`:
+
+[width="100%",cols="23%,25%,18%,34%",options="header",]
+|===
+|Index |Column |Type |Rationale
+|`+idx_semantic_writhe+` |`+writhe+` |B-tree |Filter on
+`+GET /api/knots?writhe=X+`; medium card (~100)
+
+|`+idx_semantic_genus+` |`+genus+` |B-tree |Filter on both
+`+/api/knots+` + `+/api/semantic+`; sparse but useful
+
+|`+idx_semantic_gencount+` |`+quandle_generator_count+` |B-tree
+|Currently forced in-memory after fetch; index pays for itself
+|===
+
+Total indexes now: *10* (was 7).
+
+=== Column inventory (full audit)
+
+[width="100%",cols="15%,10%,11%,21%,23%,20%",options="header",]
+|===
+|Column |Type |Card. |Filtered by |Index status |Index kind
+|`+knot_name+` |TEXT (PK) |~10⁴ |single-knot lookups |implicit PK |—
+
+|`+descriptor_version+` |TEXT |1-2 |none |— |skip
+
+|`+descriptor_hash+` |TEXT |~10⁴ |`+/api/semantic-equivalents/:name+`
+(line 341 of serve.jl); `+/api/semantic?descriptor_hash=X+` (line 786)
+|`+idx_semantic_hash+` (already) |hash/B-tree
+
+|`+quandle_key+` |TEXT |~5000 |`+/api/semantic?quandle_key=X+` (line
+790); `+semantic_equivalence_buckets+` (line 344) |`+idx_semantic_key+`
+(already) |hash/B-tree
+
+|`+diagram_format+` |TEXT |2-3 |none |— |skip
+
+|`+canonical_representation+` |TEXT |unique |none |— |skip
+
+|`+component_count+` |INTEGER |1-3 |none |— |skip (too low card)
+
+|`+crossing_number+` |INTEGER |~50 |`+/api/knots+`, `+/api/semantic+`,
+KRL pushdown (line 175) |`+idx_semantic_crossing+` (already) |B-tree
+
+|`+writhe+` |INTEGER |~100 |`+/api/knots?writhe=X+` (line 694), KRL
+pushdown (line 176) |*NEW: `+idx_semantic_writhe+`* |B-tree
+
+|`+genus+` |INTEGER |~20 |`+/api/knots?genus=X+` (line 695),
+`+/api/semantic?genus=X+` (line 754), KRL pushdown (line 177) |*NEW:
+`+idx_semantic_genus+`* |B-tree
+
+|`+determinant+` |INTEGER |~500 |`+/api/knots?determinant=X+`,
+`+/api/semantic?determinant=X+` |`+idx_semantic_determinant+` (already)
+|B-tree
+
+|`+signature+` |INTEGER |~200 |`+/api/semantic?signature=X+`
+|`+idx_semantic_signature+` (already) |B-tree
+
+|`+alexander_polynomial+` |TEXT |~2000 |`+find_equivalent+` stages (no
+direct filter) |— |skip Phase B (full-text deferred)
+
+|`+jones_polynomial+` |TEXT |~3000 |same |— |skip Phase B
+
+|`+quandle_generator_count+` |INTEGER |~100
+|`+/api/semantic?quandle_generator_count=X+` (line 756), in-memory
+filter (lines 779-780) |*NEW: `+idx_semantic_gencount+`* |B-tree
+
+|`+quandle_relation_count+` |INTEGER |~80 |none (could be added) |—
+|skip until queried
+
+|`+quandle_degree_partition+` |TEXT |~500 |none |— |skip Phase B
+
+|`+colouring_count_3+` |INTEGER |~300
+|`+/api/semantic?colouring_count_3=X+` |`+idx_semantic_col3+` (already)
+|B-tree
+
+|`+colouring_count_5+` |INTEGER |~300 |(none directly today, but
+`+quandle_key+` derives from it) |`+idx_semantic_col5+` (already)
+|B-tree
+
+|`+indexed_at+` |TEXT |per-load |none |— |skip
+|===
+
+=== Phase B — what’s queued
+
+Phase B replaces raw `+CREATE INDEX+` DDL with calls to Skein.jl’s
+public index-management API once that API exists. Required:
+
+[source,julia]
+----
+create_index!(db::SkeinDB, table::String, column::String, kind::Symbol = :btree)
+drop_index!(db::SkeinDB, index_name::String)
+list_indices(db::SkeinDB, table::String) :: Vector{String}
+----
+
+This is the upstream blocker; should be filed on Skein.jl issue tracker
+when this lands. Until then, raw DDL in `+SEMANTIC_INDEX_STATEMENTS+` is
+the working pattern.
+
+=== Phase C — what’s deferred
+
+* *Full-text indexes on polynomial strings.* `+alexander_polynomial+`,
+`+jones_polynomial+`, `+conway_polynomial+`, `+homfly_polynomial+`.
+Would help substring or coefficient-range queries; SQLite has FTS5 but
+isn’t currently wired into the schema. Defer to a future PR.
+* *Materialised views* for the equivalence buckets. The
+`+semantic_equivalence_buckets()+` function (serve.jl line 336-357)
+scans the whole table; a materialised view keyed by `+descriptor_hash+`
+and `+quandle_key+` would O(1) the bucketing.
+* *Composite indexes* for multi-column queries like
+`+crossing_number=N AND determinant=D+`. SQLite query planner may
+already use index intersection effectively; profile before adding.
+
+=== Profiling guidance
+
+After this PR, verify the planner uses the new indexes:
+
+[source,sql]
+----
+EXPLAIN QUERY PLAN
+SELECT knot_name FROM quandle_semantic_index WHERE writhe = 3;
+-- expected: SEARCH ... USING INDEX idx_semantic_writhe
+
+EXPLAIN QUERY PLAN
+SELECT knot_name FROM quandle_semantic_index WHERE genus = 1;
+-- expected: SEARCH ... USING INDEX idx_semantic_genus
+
+EXPLAIN QUERY PLAN
+SELECT knot_name FROM quandle_semantic_index WHERE quandle_generator_count = 5;
+-- expected: SEARCH ... USING INDEX idx_semantic_gencount
+----
+
+If any of these report a SCAN instead of SEARCH, the index is mis-named
+or the statistics need an `+ANALYZE+`.
+
+=== Cross-references
+
+* PROOF-NARRATIVE.md §3 DB-3
+* Audit doc `+/tmp/krl-quandle-tangle-audit-2026-06-01.md+` DB-3
+* Issue #33 — full DB-3 tracker (Phases B, C remain queued)
+* Issue #34 — DB-6 EXPLAIN (depends on this index layout for selectivity
+estimates)
diff --git a/docs/db-3-index-strategy.md b/docs/db-3-index-strategy.md
deleted file mode 100644
index c65150d..0000000
--- a/docs/db-3-index-strategy.md
+++ /dev/null
@@ -1,106 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
-# DB-3 Index Strategy
-
-**Source:** PROOF-NARRATIVE.md §3 DB-3. Phase A audit 2026-06-01.
-
-This file is the **Phase A audit deliverable** for `quandledb#33`. It
-inventories every column in the `quandle_semantic_index` table,
-classifies its query-access pattern, and recommends an index strategy.
-
-## Phase A — what's done
-
-3 new indexes added to `SEMANTIC_INDEX_STATEMENTS` in `server/serve.jl`:
-
-| Index | Column | Type | Rationale |
-|-------|--------|------|-----------|
-| `idx_semantic_writhe` | `writhe` | B-tree | Filter on `GET /api/knots?writhe=X`; medium card (~100) |
-| `idx_semantic_genus` | `genus` | B-tree | Filter on both `/api/knots` + `/api/semantic`; sparse but useful |
-| `idx_semantic_gencount` | `quandle_generator_count` | B-tree | Currently forced in-memory after fetch; index pays for itself |
-
-Total indexes now: **10** (was 7).
-
-## Column inventory (full audit)
-
-| Column | Type | Card. | Filtered by | Index status | Index kind |
-|--------|------|-------|-------------|--------------|------------|
-| `knot_name` | TEXT (PK) | ~10⁴ | single-knot lookups | implicit PK | — |
-| `descriptor_version` | TEXT | 1-2 | none | — | skip |
-| `descriptor_hash` | TEXT | ~10⁴ | `/api/semantic-equivalents/:name` (line 341 of serve.jl); `/api/semantic?descriptor_hash=X` (line 786) | `idx_semantic_hash` (already) | hash/B-tree |
-| `quandle_key` | TEXT | ~5000 | `/api/semantic?quandle_key=X` (line 790); `semantic_equivalence_buckets` (line 344) | `idx_semantic_key` (already) | hash/B-tree |
-| `diagram_format` | TEXT | 2-3 | none | — | skip |
-| `canonical_representation` | TEXT | unique | none | — | skip |
-| `component_count` | INTEGER | 1-3 | none | — | skip (too low card) |
-| `crossing_number` | INTEGER | ~50 | `/api/knots`, `/api/semantic`, KRL pushdown (line 175) | `idx_semantic_crossing` (already) | B-tree |
-| `writhe` | INTEGER | ~100 | `/api/knots?writhe=X` (line 694), KRL pushdown (line 176) | **NEW: `idx_semantic_writhe`** | B-tree |
-| `genus` | INTEGER | ~20 | `/api/knots?genus=X` (line 695), `/api/semantic?genus=X` (line 754), KRL pushdown (line 177) | **NEW: `idx_semantic_genus`** | B-tree |
-| `determinant` | INTEGER | ~500 | `/api/knots?determinant=X`, `/api/semantic?determinant=X` | `idx_semantic_determinant` (already) | B-tree |
-| `signature` | INTEGER | ~200 | `/api/semantic?signature=X` | `idx_semantic_signature` (already) | B-tree |
-| `alexander_polynomial` | TEXT | ~2000 | `find_equivalent` stages (no direct filter) | — | skip Phase B (full-text deferred) |
-| `jones_polynomial` | TEXT | ~3000 | same | — | skip Phase B |
-| `quandle_generator_count` | INTEGER | ~100 | `/api/semantic?quandle_generator_count=X` (line 756), in-memory filter (lines 779-780) | **NEW: `idx_semantic_gencount`** | B-tree |
-| `quandle_relation_count` | INTEGER | ~80 | none (could be added) | — | skip until queried |
-| `quandle_degree_partition` | TEXT | ~500 | none | — | skip Phase B |
-| `colouring_count_3` | INTEGER | ~300 | `/api/semantic?colouring_count_3=X` | `idx_semantic_col3` (already) | B-tree |
-| `colouring_count_5` | INTEGER | ~300 | (none directly today, but `quandle_key` derives from it) | `idx_semantic_col5` (already) | B-tree |
-| `indexed_at` | TEXT | per-load | none | — | skip |
-
-## Phase B — what's queued
-
-Phase B replaces raw `CREATE INDEX` DDL with calls to Skein.jl's
-public index-management API once that API exists. Required:
-
-```julia
-create_index!(db::SkeinDB, table::String, column::String, kind::Symbol = :btree)
-drop_index!(db::SkeinDB, index_name::String)
-list_indices(db::SkeinDB, table::String) :: Vector{String}
-```
-
-This is the upstream blocker; should be filed on Skein.jl issue
-tracker when this lands. Until then, raw DDL in
-`SEMANTIC_INDEX_STATEMENTS` is the working pattern.
-
-## Phase C — what's deferred
-
-- **Full-text indexes on polynomial strings.** `alexander_polynomial`,
-  `jones_polynomial`, `conway_polynomial`, `homfly_polynomial`. Would
-  help substring or coefficient-range queries; SQLite has FTS5 but
-  isn't currently wired into the schema. Defer to a future PR.
-- **Materialised views** for the equivalence buckets. The
-  `semantic_equivalence_buckets()` function (serve.jl line 336-357)
-  scans the whole table; a materialised view keyed by `descriptor_hash`
-  and `quandle_key` would O(1) the bucketing.
-- **Composite indexes** for multi-column queries like
-  `crossing_number=N AND determinant=D`. SQLite query planner may
-  already use index intersection effectively; profile before adding.
-
-## Profiling guidance
-
-After this PR, verify the planner uses the new indexes:
-
-```sql
-EXPLAIN QUERY PLAN
-SELECT knot_name FROM quandle_semantic_index WHERE writhe = 3;
--- expected: SEARCH ... USING INDEX idx_semantic_writhe
-
-EXPLAIN QUERY PLAN
-SELECT knot_name FROM quandle_semantic_index WHERE genus = 1;
--- expected: SEARCH ... USING INDEX idx_semantic_genus
-
-EXPLAIN QUERY PLAN
-SELECT knot_name FROM quandle_semantic_index WHERE quandle_generator_count = 5;
--- expected: SEARCH ... USING INDEX idx_semantic_gencount
-```
-
-If any of these report a SCAN instead of SEARCH, the index is
-mis-named or the statistics need an `ANALYZE`.
-
-## Cross-references
-
-- PROOF-NARRATIVE.md §3 DB-3
-- Audit doc `/tmp/krl-quandle-tangle-audit-2026-06-01.md` DB-3
-- Issue #33 — full DB-3 tracker (Phases B, C remain queued)
-- Issue #34 — DB-6 EXPLAIN (depends on this index layout for
-  selectivity estimates)
diff --git a/docs/db-6-explain-strategy.adoc b/docs/db-6-explain-strategy.adoc
new file mode 100644
index 0000000..756a76b
--- /dev/null
+++ b/docs/db-6-explain-strategy.adoc
@@ -0,0 +1,274 @@
+== DB-6: EXPLAIN strategy for read-only API queries
+
+Status: *both Phase A surfaces landed.* SQL-side 2026-06-01; KRL-side
+2026-07-28 (issue #34). Phases B + C deferred.
+
+____
+*Two surfaces, one issue number — read this first.*
+
+"`DB-6 Phase A`" has meant two different things in this repo, which
+caused a real mis-assessment (the issue was believed closable when half
+of it had never been built):
+
+[width="100%",cols="25%,25%,25%,25%",options="header",]
+|===
+|Surface |What it is |Where |Landed
+|*SQL-side* |SQLite `+EXPLAIN QUERY PLAN+` over the read-path SQL,
+exposed on an HTTP endpoint |`+server/query_explain.jl+`,
+`+handle_explain+` in `+server/serve.jl+` |2026-06-01 (this document’s
+original scope)
+
+|*KRL-side* |`+explain+` as a KRL keyword returning a structured plan
+with `+indexed+` and selectivity per filter
+|`+server/krl/ExplainPlan.jl+`, `+KRLExplainStmt+` |2026-07-28
+|===
+
+Issue #34’s acceptance criteria describe the *KRL-side* surface. Until
+2026-07-28 only the SQL-side existed: `+explain+` appeared in neither
+`+server/krl/Lexer.jl+` nor `+server/krl/Parser.jl+`, and there was no
+selectivity model anywhere — not even the stub the criteria permit. Both
+now exist and are independently gated in CI.
+____
+
+=== Goal
+
+For every read-path SQL query in `+server/serve.jl+`, surface the SQLite
+`+EXPLAIN QUERY PLAN+` output so query-plan regressions are visible
+during review (Phase A) and at request time (Phase B+C).
+
+This builds on DB-3 (B-tree index inventory): DB-3 enumerated the
+indexed columns; DB-6 confirms the planner actually uses them.
+
+=== Echo-types audit
+
+Per `+[[proofs-must-check-and-cross-doc-echo-types]]+`: echo-types is a
+fibre-based loss-with-residue semantics library. It has zero SQL,
+HTTP-server, or query-plan content. *Verdict: NOT-RELEVANT.* Recorded
+once at
+`+feedback_echo_types_audit_krl_tangle_quandledb_not_relevant.md+` for
+all five krl/tangle/quandledb obligations.
+
+=== Query inventory (current, as of 2026-06-01)
+
+==== Owned by quandledb (SQL visible)
+
+[width="100%",cols="26%,30%,36%,8%",options="header",]
+|===
+|Handler |File:line |SQL surface |EXPLAIN reachable?
+|`+handle_semantic_detail+` |`+server/serve.jl:737+`
+|`+SELECT * FROM quandle_semantic_index WHERE knot_name = ?+` (indirect
+via `+ensure_semantic_entry!+`) |*Yes* (Phase B)
+
+|`+handle_semantic_equivalents+` |`+server/serve.jl:743+` |two
+`+SELECT+` queries on `+quandle_semantic_index+` (strong + weak
+buckets); see `+serve.jl:347+` and `+:350+` |*Yes* (Phase B)
+
+|`+handle_semantic_index+` |`+server/serve.jl:759+` |dynamic
+`+SELECT * FROM quandle_semantic_index WHERE … LIMIT ? OFFSET ?+` — 7
+optional filters + ordering on `+(crossing_number, knot_name)+` |*Yes*
+(Phase A — this is the scaffold target)
+
+|`+handle_krl_query (SQL mode)+` |`+server/serve.jl:816+` |arbitrary
+`+SELECT+`/`+WITH+` queries; passes through `+parse_sql+` →
+`+eval_krl_program+` |*Yes* (Phase B; deeper integration)
+
+|`+handle_krl_query (KRL mode)+` |same |KRL → SQL via the KRL evaluator
+under `+server/krl/+` |*Partial* (depends on `+pushdown_used+`; covered
+Phase C)
+
+|`+handle_statistics+` |`+server/serve.jl:920+`
+|`+SELECT COUNT(*) AS n FROM quandle_semantic_index+` + distribution
+queries |*Yes* (Phase B, low-priority)
+|===
+
+==== Owned by Skein.jl (SQL opaque)
+
+[width="100%",cols="24%,27%,42%,7%",options="header",]
+|===
+|Handler |File:line |Underlying call |Blocker
+|`+handle_knots+` |`+server/serve.jl:699+`
+|`+query(db; crossing_number, writhe, genus, …)+` |Skein.jl `+query+`
+builds SQL internally and does not return the constructed string; we
+cannot pipe it through `+EXPLAIN+` without a Skein.jl API addition.
+
+|`+handle_knot_detail+` |`+server/serve.jl:728+`
+|`+fetch_knot(db, name)+` |Same.
+
+|`+semantic_summary_by_name+` (called from `+handle_knots+`)
+|`+server/serve.jl+` |Joins via Skein.jl. |Same.
+|===
+
+*The Skein.jl gap is the same shape as the DB-3 Phase B blocker*
+(Skein.jl does not expose `+create_index!+` / `+drop_index!+` /
+`+list_indices+`). The fix is upstream: an addition to Skein.jl’s public
+API surface, e.g.
+`+Skein.explain(db; …same kwargs as query) -> String+`. Filed at
+https://github.com/hyperpolymath/quandledb/issues/34[hyperpolymath/quandledb#34]
+as the parent for DB-6.
+
+=== Phase A — what landed today
+
+* `+server/query_explain.jl+`:
+`+explain_query_plan(conn::SQLite.DB, sql::String, args::Vector)::Vector{Dict}+`
+** Wraps `+EXPLAIN QUERY PLAN <sql>+` with the same bind-arg pattern.
+** Returns one Dict per planner row: `+id+`, `+parent+`, `+notused+`,
+`+detail+`.
+** Read-only by construction (SQLite `+EXPLAIN QUERY PLAN+` is a
+`+SELECT+`).
+* `+server/test_query_explain.jl+`: 4 assertions exercising:
+[arabic]
+. trivial `+SELECT 1+` plan is non-empty
+. a single-table `+SELECT+` reads the expected table name in `+detail+`
+. a filtered
+`+SELECT * FROM quandle_semantic_index WHERE crossing_number = ?+`
+mentions either `+SEARCH+` (index hit) or `+SCAN+` (no index hit) —
+sanity check that the planner emits structured output
+. a `+SELECT * … WHERE writhe = ?+` mentions `+idx_semantic_writhe+`
+(the DB-3 index from PR #42); this is the regression hook that proves
+the index is actually used
+
+These tests run against the canonical seed `+data/knots.db+` produced by
+`+server/test_quandle_axioms.jl+` setup.
+
+*Phase A does NOT* wire the utility into any public endpoint. The public
+surface is still strictly `+GET /api/knots+`, `+/api/semantic*+`,
+`+/api/krl/query+`, `+/api/statistics+`. That wiring is Phase B.
+
+=== Phase B — planned (next PR)
+
+[arabic]
+. `+GET /api/explain?endpoint=semantic&…+` — accepts the same query
+parameters as `+/api/semantic+`, builds the same SQL via the same
+`+handle_semantic_index+` helper, but returns the EXPLAIN output instead
+of the rows.
+. `+GET /api/explain?sql=…+` — raw-SQL mode. Validates that the SQL is a
+plain `+SELECT+`/`+WITH+` (no
+`+INSERT+`/`+UPDATE+`/`+DELETE+`/`+PRAGMA+`) before piping through
+`+explain_query_plan+`. Reuses the existing `+read-only-api-gate.yml+`
+discipline (QD-12).
+. Per-request logging: when a query is served, also emit a JSON line
+`+{"query": "...", "plan_summary": "..."}+` to a structured log so
+regressions are visible in the metrics stream.
+
+Phase B is blocked on a small Skein.jl upstream addition (see above).
+Once that lands, the wrapper for `+handle_knots+` becomes one-line.
+
+=== Phase C — deferred (research-grade)
+
+[arabic]
+. *Plan-snapshot regression test*: capture the EXPLAIN output for a
+canonical set of queries on the seed DB and assert byte-equality in
+[upperroman, start=101]
+.. Any drift = fail. (Aligns with VeriSimDB seam-walk in
+`+[[verisimdb-subject-of-everything]]+`.)
+. *Cost-model integration*: pair each plan with the
+`+tropical-resource-typing+` cost-decoration so reviewers see expected
+row counts alongside the planner’s pick.
+. *Composite-index suggestion*: examine which filter combinations on
+`+/api/semantic+` trigger SCANs (no index) and propose composite
+indexes. This is the DB-3 Phase C echo.
+
+=== Out of scope
+
+* Anything beyond SQLite (no Postgres-style `+pg_stat_statements+`).
+* Schema changes (DB-3 owns indexes; DB-6 only reads plans).
+* Frontend rendering of plans (back-end-only this PR).
+* ReScript→AffineScript migration of the frontend (tracked at
+quandledb#43; estate sweep at standards#252).
+
+=== Acceptance
+
+* `+server/query_explain.jl+` compiles and
+`+julia --project=server -e 'include("server/test_query_explain.jl"); run_db6_tests()'+`
+returns nonzero only on regression.
+* `+docs/db-6-explain-strategy.md+` exists and lists all read-path
+queries.
+* No public endpoint is added (Phase A is utility-only).
+
+=== Cross-document
+
+* DB-3 (`+docs/db-3-index-strategy.md+`): index inventory consumed here.
+* QD-12 (`+server/.github/workflows/read-only-api-gate.yml+`): the
+read-only discipline that Phase B explain endpoint must honour.
+* VeriSimDB seam-walk umbrella (`+hyperpolymath/verisimdb#80+`): pattern
+of plan-snapshot regression tests we will echo in Phase C.
+
+=== See also
+
+* https://github.com/hyperpolymath/quandledb/issues/34[hyperpolymath/quandledb#34]
+— DB-6 parent
+* https://github.com/hyperpolymath/quandledb/issues/33[hyperpolymath/quandledb#33]
+— DB-3 Phase B + C parent (Skein.jl gap is shared)
+* https://github.com/hyperpolymath/quandledb/pull/42[hyperpolymath/quandledb#42]
+— DB-3 Phase A (indexes that Phase A test 4 exercises)
+
+'''''
+
+=== KRL-side EXPLAIN (landed 2026-07-28)
+
+==== Syntax
+
+`+explain+` prefixes a pipeline query. It returns the *plan*; it does
+not run the query.
+
+[source,krl]
+----
+explain from knots | filter colouring_count_3 = 9 and crossing < 8 | take 5
+----
+
+==== Plan shape
+
+....
+{"op" => "scan",   "table" => "knots"}
+{"op" => "filter", "column" => "colouring_count_3", "comparator" => "=", "value" => 9,
+                   "indexed" => true,  "selectivity_estimate" => 0.5, "selectivity_source" => "stub"}
+{"op" => "filter", "column" => "crossing",          "comparator" => "<", "value" => 8,
+                   "indexed" => false, "selectivity_estimate" => 0.5, "selectivity_source" => "stub"}
+{"op" => "take",   "n" => 5}
+....
+
+A conjunction becomes *separate* filter operations. That is deliberate:
+it is what makes the Phase B reorder meaningful, since a reorder can
+only permute operations the plan actually distinguishes.
+
+==== Design decisions worth knowing
+
+*`+explain+` parses to its own statement type.* `+KRLExplainStmt+` is
+distinct from `+KRLQueryStmt+` rather than a flag on it, so every
+existing consumer of `+KRLQueryStmt+` still means "`this query will
+actually execute`" and cannot be handed a plan where it expected rows.
+
+*Selectivity is a stub, and says so.* There are no column histograms yet
+— that is DB-3 (#33), and the DB-6 criteria explicitly permit a stub
+until it lands. Every estimate is `+SELECTIVITY_STUB+` (0.5) carrying
+`+"selectivity_source" => "stub"+`, and `+plan_is_costed(plan)+` returns
+`+false+` while any stub remains. *That predicate is the guard that
+stops Phase B optimising against invented numbers* — a cost-based
+reorder driven by uniform 0.5 estimates would be arbitrary while looking
+principled.
+
+*`+indexed+` is driven by a short explicit list.* `+INDEXED_COLUMNS+`
+names only columns that genuinely carry a secondary index. An
+over-claiming list would make `+indexed+` a fake signal, which is worse
+than reporting `+false+`. Extend it as DB-3 lands real indexes — not
+before.
+
+*Predicates the plan cannot describe are not mis-described.*
+Column-to-column comparisons, nested booleans and calls report
+`+"predicate" => "<expression>"+` with no `+column+` key, rather than
+being given a fabricated column.
+
+==== What is deliberately NOT done
+
+Phase B (cost-based reordering) is not attempted. The plan is returned
+in *execution order as written*. Phase B needs real selectivity,
+i.e. DB-3.
+
+==== Tests
+
+`+server/krl/test/explain_test.jl+` — 25 assertions, in the
+dependency-free CI step (so it runs before `+Pkg.instantiate+` and
+cannot be masked by a dependency breakage). Two of its testsets assert
+the _honesty_ properties above rather than the happy path: that
+selectivity is labelled a stub with `+plan_is_costed == false+`, and
+that an undescribable predicate stays opaque.
diff --git a/docs/db-6-explain-strategy.md b/docs/db-6-explain-strategy.md
deleted file mode 100644
index 3e865a9..0000000
--- a/docs/db-6-explain-strategy.md
+++ /dev/null
@@ -1,212 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
--->
-# DB-6: EXPLAIN strategy for read-only API queries
-
-Status: **both Phase A surfaces landed.** SQL-side 2026-06-01; KRL-side
-2026-07-28 (issue #34). Phases B + C deferred.
-
-> **Two surfaces, one issue number — read this first.**
->
-> "DB-6 Phase A" has meant two different things in this repo, which caused a
-> real mis-assessment (the issue was believed closable when half of it had
-> never been built):
->
-> | Surface | What it is | Where | Landed |
-> |---|---|---|---|
-> | **SQL-side** | SQLite `EXPLAIN QUERY PLAN` over the read-path SQL, exposed on an HTTP endpoint | `server/query_explain.jl`, `handle_explain` in `server/serve.jl` | 2026-06-01 (this document's original scope) |
-> | **KRL-side** | `explain` as a KRL keyword returning a structured plan with `indexed` and selectivity per filter | `server/krl/ExplainPlan.jl`, `KRLExplainStmt` | 2026-07-28 |
->
-> Issue #34's acceptance criteria describe the **KRL-side** surface. Until
-> 2026-07-28 only the SQL-side existed: `explain` appeared in neither
-> `server/krl/Lexer.jl` nor `server/krl/Parser.jl`, and there was no
-> selectivity model anywhere — not even the stub the criteria permit.
-> Both now exist and are independently gated in CI.
-
-## Goal
-
-For every read-path SQL query in `server/serve.jl`, surface the SQLite
-`EXPLAIN QUERY PLAN` output so query-plan regressions are visible during
-review (Phase A) and at request time (Phase B+C).
-
-This builds on DB-3 (B-tree index inventory): DB-3 enumerated the
-indexed columns; DB-6 confirms the planner actually uses them.
-
-## Echo-types audit
-
-Per `[[proofs-must-check-and-cross-doc-echo-types]]`: echo-types is a
-fibre-based loss-with-residue semantics library. It has zero SQL,
-HTTP-server, or query-plan content. **Verdict: NOT-RELEVANT.** Recorded
-once at `feedback_echo_types_audit_krl_tangle_quandledb_not_relevant.md`
-for all five krl/tangle/quandledb obligations.
-
-## Query inventory (current, as of 2026-06-01)
-
-### Owned by quandledb (SQL visible)
-
-| Handler | File:line | SQL surface | EXPLAIN reachable? |
-|---------|-----------|-------------|---|
-| `handle_semantic_detail` | `server/serve.jl:737` | `SELECT * FROM quandle_semantic_index WHERE knot_name = ?` (indirect via `ensure_semantic_entry!`) | **Yes** (Phase B) |
-| `handle_semantic_equivalents` | `server/serve.jl:743` | two `SELECT` queries on `quandle_semantic_index` (strong + weak buckets); see `serve.jl:347` and `:350` | **Yes** (Phase B) |
-| `handle_semantic_index` | `server/serve.jl:759` | dynamic `SELECT * FROM quandle_semantic_index WHERE … LIMIT ? OFFSET ?` — 7 optional filters + ordering on `(crossing_number, knot_name)` | **Yes** (Phase A — this is the scaffold target) |
-| `handle_krl_query (SQL mode)` | `server/serve.jl:816` | arbitrary `SELECT`/`WITH` queries; passes through `parse_sql` → `eval_krl_program` | **Yes** (Phase B; deeper integration) |
-| `handle_krl_query (KRL mode)` | same | KRL → SQL via the KRL evaluator under `server/krl/` | **Partial** (depends on `pushdown_used`; covered Phase C) |
-| `handle_statistics` | `server/serve.jl:920` | `SELECT COUNT(*) AS n FROM quandle_semantic_index` + distribution queries | **Yes** (Phase B, low-priority) |
-
-### Owned by Skein.jl (SQL opaque)
-
-| Handler | File:line | Underlying call | Blocker |
-|---------|-----------|-----------------|---|
-| `handle_knots` | `server/serve.jl:699` | `query(db; crossing_number, writhe, genus, …)` | Skein.jl `query` builds SQL internally and does not return the constructed string; we cannot pipe it through `EXPLAIN` without a Skein.jl API addition. |
-| `handle_knot_detail` | `server/serve.jl:728` | `fetch_knot(db, name)` | Same. |
-| `semantic_summary_by_name` (called from `handle_knots`) | `server/serve.jl` | Joins via Skein.jl. | Same. |
-
-**The Skein.jl gap is the same shape as the DB-3 Phase B blocker**
-(Skein.jl does not expose `create_index!` / `drop_index!` / `list_indices`).
-The fix is upstream: an addition to Skein.jl's public API surface, e.g.
-`Skein.explain(db; …same kwargs as query) -> String`. Filed at
-[hyperpolymath/quandledb#34](https://github.com/hyperpolymath/quandledb/issues/34)
-as the parent for DB-6.
-
-## Phase A — what landed today
-
-- `server/query_explain.jl`: `explain_query_plan(conn::SQLite.DB, sql::String, args::Vector)::Vector{Dict}`
-  - Wraps `EXPLAIN QUERY PLAN <sql>` with the same bind-arg pattern.
-  - Returns one Dict per planner row: `id`, `parent`, `notused`, `detail`.
-  - Read-only by construction (SQLite `EXPLAIN QUERY PLAN` is a `SELECT`).
-- `server/test_query_explain.jl`: 4 assertions exercising:
-  1. trivial `SELECT 1` plan is non-empty
-  2. a single-table `SELECT` reads the expected table name in `detail`
-  3. a filtered `SELECT * FROM quandle_semantic_index WHERE crossing_number = ?` mentions either `SEARCH` (index hit) or `SCAN` (no index hit) — sanity check that the planner emits structured output
-  4. a `SELECT * … WHERE writhe = ?` mentions `idx_semantic_writhe` (the DB-3 index from PR #42); this is the regression hook that proves the index is actually used
-
-These tests run against the canonical seed `data/knots.db` produced by
-`server/test_quandle_axioms.jl` setup.
-
-**Phase A does NOT** wire the utility into any public endpoint. The
-public surface is still strictly `GET /api/knots`, `/api/semantic*`,
-`/api/krl/query`, `/api/statistics`. That wiring is Phase B.
-
-## Phase B — planned (next PR)
-
-1. `GET /api/explain?endpoint=semantic&…` — accepts the same query
-   parameters as `/api/semantic`, builds the same SQL via the same
-   `handle_semantic_index` helper, but returns the EXPLAIN output
-   instead of the rows.
-2. `GET /api/explain?sql=…` — raw-SQL mode. Validates that the SQL is a
-   plain `SELECT`/`WITH` (no `INSERT`/`UPDATE`/`DELETE`/`PRAGMA`) before
-   piping through `explain_query_plan`. Reuses the existing
-   `read-only-api-gate.yml` discipline (QD-12).
-3. Per-request logging: when a query is served, also emit a JSON line
-   `{"query": "...", "plan_summary": "..."}` to a structured log so
-   regressions are visible in the metrics stream.
-
-Phase B is blocked on a small Skein.jl upstream addition (see above).
-Once that lands, the wrapper for `handle_knots` becomes one-line.
-
-## Phase C — deferred (research-grade)
-
-1. **Plan-snapshot regression test**: capture the EXPLAIN output for a
-   canonical set of queries on the seed DB and assert byte-equality in
-   CI. Any drift = fail. (Aligns with VeriSimDB seam-walk in
-   `[[verisimdb-subject-of-everything]]`.)
-2. **Cost-model integration**: pair each plan with the
-   `tropical-resource-typing` cost-decoration so reviewers see expected
-   row counts alongside the planner's pick.
-3. **Composite-index suggestion**: examine which filter
-   combinations on `/api/semantic` trigger SCANs (no index) and
-   propose composite indexes. This is the DB-3 Phase C echo.
-
-## Out of scope
-
-- Anything beyond SQLite (no Postgres-style `pg_stat_statements`).
-- Schema changes (DB-3 owns indexes; DB-6 only reads plans).
-- Frontend rendering of plans (back-end-only this PR).
-- ReScript→AffineScript migration of the frontend (tracked at quandledb#43; estate sweep at standards#252).
-
-## Acceptance
-
-- `server/query_explain.jl` compiles and `julia --project=server -e 'include("server/test_query_explain.jl"); run_db6_tests()'` returns nonzero only on regression.
-- `docs/db-6-explain-strategy.md` exists and lists all read-path queries.
-- No public endpoint is added (Phase A is utility-only).
-
-## Cross-document
-
-- DB-3 (`docs/db-3-index-strategy.md`): index inventory consumed here.
-- QD-12 (`server/.github/workflows/read-only-api-gate.yml`): the
-  read-only discipline that Phase B explain endpoint must honour.
-- VeriSimDB seam-walk umbrella (`hyperpolymath/verisimdb#80`): pattern of
-  plan-snapshot regression tests we will echo in Phase C.
-
-## See also
-
-- [hyperpolymath/quandledb#34](https://github.com/hyperpolymath/quandledb/issues/34) — DB-6 parent
-- [hyperpolymath/quandledb#33](https://github.com/hyperpolymath/quandledb/issues/33) — DB-3 Phase B + C parent (Skein.jl gap is shared)
-- [hyperpolymath/quandledb#42](https://github.com/hyperpolymath/quandledb/pull/42) — DB-3 Phase A (indexes that Phase A test 4 exercises)
-
-
----
-
-## KRL-side EXPLAIN (landed 2026-07-28)
-
-### Syntax
-
-`explain` prefixes a pipeline query. It returns the **plan**; it does not run
-the query.
-
-```krl
-explain from knots | filter colouring_count_3 = 9 and crossing < 8 | take 5
-```
-
-### Plan shape
-
-```
-{"op" => "scan",   "table" => "knots"}
-{"op" => "filter", "column" => "colouring_count_3", "comparator" => "=", "value" => 9,
-                   "indexed" => true,  "selectivity_estimate" => 0.5, "selectivity_source" => "stub"}
-{"op" => "filter", "column" => "crossing",          "comparator" => "<", "value" => 8,
-                   "indexed" => false, "selectivity_estimate" => 0.5, "selectivity_source" => "stub"}
-{"op" => "take",   "n" => 5}
-```
-
-A conjunction becomes **separate** filter operations. That is deliberate: it is
-what makes the Phase B reorder meaningful, since a reorder can only permute
-operations the plan actually distinguishes.
-
-### Design decisions worth knowing
-
-**`explain` parses to its own statement type.** `KRLExplainStmt` is distinct
-from `KRLQueryStmt` rather than a flag on it, so every existing consumer of
-`KRLQueryStmt` still means "this query will actually execute" and cannot be
-handed a plan where it expected rows.
-
-**Selectivity is a stub, and says so.** There are no column histograms yet —
-that is DB-3 (#33), and the DB-6 criteria explicitly permit a stub until it
-lands. Every estimate is `SELECTIVITY_STUB` (0.5) carrying
-`"selectivity_source" => "stub"`, and `plan_is_costed(plan)` returns `false`
-while any stub remains. **That predicate is the guard that stops Phase B
-optimising against invented numbers** — a cost-based reorder driven by
-uniform 0.5 estimates would be arbitrary while looking principled.
-
-**`indexed` is driven by a short explicit list.** `INDEXED_COLUMNS` names only
-columns that genuinely carry a secondary index. An over-claiming list would
-make `indexed` a fake signal, which is worse than reporting `false`. Extend it
-as DB-3 lands real indexes — not before.
-
-**Predicates the plan cannot describe are not mis-described.** Column-to-column
-comparisons, nested booleans and calls report `"predicate" => "<expression>"`
-with no `column` key, rather than being given a fabricated column.
-
-### What is deliberately NOT done
-
-Phase B (cost-based reordering) is not attempted. The plan is returned in
-**execution order as written**. Phase B needs real selectivity, i.e. DB-3.
-
-### Tests
-
-`server/krl/test/explain_test.jl` — 25 assertions, in the dependency-free CI
-step (so it runs before `Pkg.instantiate` and cannot be masked by a dependency
-breakage). Two of its testsets assert the *honesty* properties above rather
-than the happy path: that selectivity is labelled a stub with
-`plan_is_costed == false`, and that an undescribable predicate stays opaque.
diff --git a/docs/design/KRL-SQL-LANDSCAPE-RESEARCH-2026-02-22.adoc b/docs/design/KRL-SQL-LANDSCAPE-RESEARCH-2026-02-22.adoc
new file mode 100644
index 0000000..f125a81
--- /dev/null
+++ b/docs/design/KRL-SQL-LANDSCAPE-RESEARCH-2026-02-22.adoc
@@ -0,0 +1,395 @@
+== KRL Design: SQL Landscape Research — 2026-02-22
+
+=== Comprehensive Survey for QuandleDB Query Language Design
+
+*Date:* 2026-02-22 *For:* nextgen-databases/quandledb *Agent:* Claude
+Opus 4.6 *Status:* Research complete — design phase next
+
+'''''
+
+=== EXECUTIVE SUMMARY
+
+*SQL is the wrong paradigm for QuandleDB.* The right foundation is a
+synthesis of:
+
+[arabic]
+. *egglog* — equality saturation over Datalog (handles equivalence
+classes natively)
+. *Spivak’s categorical data model* — functorial data migration, schema
+as category
+. *HoTT identity types* — paths = equivalences (from HoTTSQL paper)
+. *Surfaced through:* PRQL-style pipeline syntax + Cypher-style graph
+pattern matching
+
+The closest existing system is *egglog* (PLDI 2023). The theoretical
+foundation is *HoTTSQL’s univalent semantics*. KRL should build on both.
+
+'''''
+
+=== Part 1: What’s Legitimately Wrong with SQL
+
+==== NULL Handling (Three-Valued Logic)
+
+* NULL conflates "`unknown,`" "`inapplicable,`" "`missing,`" "`not yet
+entered`" into one marker
+* `+NULL = NULL+` evaluates to UNKNOWN, not TRUE
+* `+NOT IN+` with NULLs produces surprising empty results
+* Codd himself proposed two kinds of null (A-marks/I-marks) — SQL never
+adopted this
+* Forces optimizers to be conservative (Guagliardo & Libkin showed real
+DBs return incorrect results due to NULL bugs)
+
+==== Bag Semantics vs Set Semantics
+
+* SQL operates on bags (multisets), not sets — departure from Codd’s
+relational model
+* Union is no longer idempotent; DISTINCT is an expensive band-aid
+* HoTTSQL proved bags can be modeled cleanly via univalent types (700+
+lines Coq reduced to 40)
+
+==== Composability (SQL’s Most Damning Flaw)
+
+* Neumann & Leis (CIDR 2024): SQL is "`a functional programming language
+that lacks parameters for functions`"
+* Cannot pass a relation as an argument to a view definition
+* Cannot parameterize a query fragment
+* CTEs help readability but are just named subqueries — can’t be
+parameterized
+* *QUEL was more composable* but lost to SQL because IBM shipped DB2 and
+Stonebraker didn’t show up to the ANSI committee
+
+==== Impedance Mismatch
+
+* SQL types don’t map cleanly to programming language types
+* ORM-induced slowdowns of 2.6x-5x confirmed by research
+* The real problem: SQL forces a different paradigm from the host
+language
+
+==== Type System Weakness
+
+* No sum types, no product types beyond rows, no generics, no type
+inference
+* CAST is explicit and lossy; implicit coercions vary by vendor
+* No standard way to define custom types with invariants
+
+==== String-Based Injection by Design
+
+* Queries are strings where structure and data are concatenated
+* The "`default, most obvious way`" to use SQL is vulnerable
+* Prepared statements fix it in practice but the design is fundamentally
+flawed
+
+==== Other Issues
+
+* ORDER BY only at outer query
+* WITH RECURSIVE is ugly and limited
+* Temporal data support abysmal (SQL:2011 exists, few implement it)
+* Window functions powerful but syntax baroque
+* GROUP BY / HAVING distinction is weird
+* Date/time handling is a mess across implementations
+* No built-in version/provenance tracking
+* Vendor fragmentation despite "`standard`"
+
+'''''
+
+=== Part 2: Every Notable Alternative and What’s Wrong with THEM
+
+==== QUEL (Ingres, 1976)
+
+* *Good:* More composable, based on tuple relational calculus
+* *Dead:* SQL won on market power (IBM), not technical merit.
+Stonebraker agreed SQL was worse.
+* *Lesson:* Technical superiority doesn’t guarantee adoption. But niche
+domains CAN sustain better languages.
+
+==== Datalog
+
+* *Good:* Declarative, naturally recursive, composable, clean formal
+semantics
+* *Bad:* No standard for aggregation/negation/updates, limited ordered
+data support
+* *Key:* egglog (PLDI 2023) unifies Datalog with equality saturation —
+directly relevant to QuandleDB
+
+==== SPARQL
+
+* *Good:* Powerful pattern matching over graphs
+* *Bad:* Extremely verbose, schema-less means typos return empty results
+silently
+
+==== Cypher (Neo4j) / GQL (ISO 39075:2024)
+
+* *Good:* ASCII-art pattern matching `+(a)-[:KNOWS]->(b)+` is genuinely
+intuitive
+* *Bad:* Limited analytics, performance degrades on large traversals
+* *GQL* is first new ISO DB language since SQL (1987). Adds quantified
+path patterns.
+* *Relevant:* Knot diagrams ARE graphs. Reidemeister moves ARE graph
+rewrites.
+
+==== PRQL (Pipelined Relational Query Language)
+
+* *Good:* Pipeline syntax dramatically more readable. Compiles to SQL.
+Written in Rust.
+* *Bad:* Still relational — no equivalence classes
+* *Lesson:* Pipeline syntax is strictly superior to SQL’s inside-out
+evaluation order
+
+==== Malloy (Google / Lloyd Tabb)
+
+* *Good:* Semantic modeling. Created by Looker founder from frustration
+with SQL.
+* *Bad:* Not an official Google product. No support commitment. Limited
+adoption.
+
+==== EdgeQL (EdgeDB, now "`Gel`")
+
+* *Good:* Modern SQL done right, object-relational model, unified typing
+* *Bad:* Hard to get started (TLS plumbing), doc gaps at complexity,
+write contention
+
+==== FQL (Fauna) — DEAD
+
+* *SHUT DOWN May 2025.* Steep learning curve, proprietary, couldn’t
+raise capital.
+* *Lesson:* Proprietary query languages die with their companies. Design
+for openness.
+
+==== SurrealQL (SurrealDB)
+
+* *Good:* Multi-model with SQL-like syntax
+* *Bad:* Lack of type safety, SDK limitations, limited maturity
+
+==== KQL (Kusto / Azure) — NAME COLLISION [Resolved]
+
+* *Good:* Pipeline syntax for log analytics
+* *Bad:* Read-only, can’t INSERT/UPDATE, Azure lock-in
+* *Note:* Previously shared acronym with our language. Resolved by
+renaming our language to KRL (Knot Resolution Language).
+
+==== DuckDB SQL Extensions
+
+* *Right:* Community extensions (6M downloads/week), SQL-only
+extensions, SQL/PGQ graph queries outperform Neo4j 10-100x
+* *Lesson:* SQL’s extensibility CAN work if done right
+
+==== Others
+
+* *Gremlin:* Imperative graph traversal. Verbose. Less optimizer
+freedom.
+* *MQL (MongoDB):* Schema-free = no compile-time safety. Aggregation
+pipeline unreadable.
+* *AQL (ArangoDB):* Multi-model but small community. BSL 1.1 license
+change (2024).
+* *PartiQL (AWS):* SQL over everything. Tightly coupled to AWS.
+* *CQL (Cassandra):* No JOINs, no ad hoc aggregations. Looks like SQL,
+can’t do SQL.
+* *PromQL/InfluxQL/Flux:* Time-series specific. Flux was deprecated —
+language churn cautionary tale.
+
+'''''
+
+=== Part 3: Academic/Theoretical Criticisms
+
+==== Codd vs SQL
+
+SQL departs from Codd’s relational model: bags not sets, NULLs,
+ordering, duplicate column names, non-1NF data (JSON/arrays).
+
+==== Third Manifesto (Date & Darwen)
+
+* SQL’s problems are NOT the relational model’s problems — they’re SQL’s
+* *Tutorial D* shows "`SQL done right`": proper types, no NULLs, set
+semantics, composability
+* Remains academic/pedagogical, no production implementation
+
+==== Category Theory Approaches (Spivak)
+
+* Schema = small category. Instance = set-valued functor. Query =
+natural transformation.
+* *CQL* (Categorical Query Language) — open-source IDE, active
+development
+* Functorial data migration handles projections/unions/joins over ALL
+tables simultaneously
+* *Directly applicable:* Quandles are algebraic structures. Category
+theory IS the language for algebraic structure relationships.
+
+==== HoTTSQL (Chu et al., PLDI 2017)
+
+* SQL semantics formalized via homotopy type theory
+* Relations as functions from tuples to univalent types
+* Bag equality proved via univalence axiom (700+ lines Coq → 40 lines)
+* *Critical insight for KRL:* Equality is not binary. Multiple distinct
+paths (proofs of equality) between objects. The space of equivalences
+has structure. THIS IS EXACTLY KNOT EQUIVALENCE.
+
+==== egglog (PLDI 2023)
+
+* Merges Datalog with equality saturation
+* E-graph compactly represents exponentially many equivalent terms
+* Systems reimplemented in egglog are faster, simpler, fix bugs
+* PLDI 2025 tutorial scheduled (growing adoption)
+* *THIS MAY BE THE SINGLE MOST RELEVANT PARADIGM FOR QUANDLEDB*
+* An e-graph IS a database of equivalence classes = a knot database
+
+==== Deductive Databases
+
+* Souffle (static analysis), Google Mangle (AI reasoning), Datalevin
+(general-purpose Datalog)
+* Revival driven by static analysis, AI reasoning, program optimization
+
+'''''
+
+=== Part 4: What SQL Gets RIGHT (Don’t Throw Away)
+
+[arabic]
+. *Declarative semantics* — say what, not how. Enables optimizer
+freedom.
+. *50 years of optimizer research* — join reordering, predicate
+pushdown, index selection
+. *Ecosystem* — tools, tutorials, books, Stack Overflow, monitoring,
+migration tools
+. *ACID transactions* — atomic, consistent, isolated, durable
+. *The standard* — imperfect but exists; multiple vendors implement it
+. *Window functions* — running totals, rankings, moving averages in
+single pass
+. *CTEs* — break complex queries into named stages
+
+'''''
+
+=== Part 5: The QuandleDB Domain Problem
+
+==== The Core Challenge
+
+QuandleDB stores mathematical structures where the fundamental operation
+is _equivalence under transformation_. Two knots may look completely
+different but be the same (related by Reidemeister moves). SQL’s
+`+WHERE x = y+` is syntactic/value equality. QuandleDB needs _semantic_
+equality.
+
+==== Scale
+
+* KnotInfo: 350 million prime knots up to 19 crossings, 1.9 billion at
+20
+* 17,528 unresolved 20-crossing knots that resist all known invariants
+* Multiple invariants per knot (Alexander, Jones, Khovanov, etc.)
+
+==== Relevant Query Paradigms
+
+[width="100%",cols="39%,42%,19%",options="header",]
+|===
+|Paradigm |Relevance |How
+|*Pattern matching* (FP) |High |Decompose knot diagrams by structure
+
+|*Unification* (Prolog) |High |Find structural constraints, variable
+binding
+
+|*Term rewriting* |Critical |Reidemeister moves ARE rewrite rules
+
+|*Category theory* (Spivak) |Critical |Quandles are algebraic structures
+in categories
+
+|*HoTT paths* |Critical |Paths = equivalences, space of equivalences has
+structure
+
+|*Equality saturation* (egglog) |Critical |E-graphs ARE databases of
+equivalence classes
+
+|*Provenance semirings* |High |Track which invariants led to equivalence
+determination
+|===
+
+'''''
+
+=== Part 6: What KRL Should Borrow vs Avoid
+
+==== Borrow
+
+[cols=",",options="header",]
+|===
+|Source |What
+|SQL |Declarative semantics, optimizer freedom, transactions
+|PRQL |Pipeline syntax (`+from ... | filter ... | aggregate ...+`)
+|Cypher/GQL |ASCII-art pattern matching for graph structures
+|Datalog |Recursive queries, rule-based reasoning
+|egglog |Equality saturation, e-graph equivalence classes
+|CQL (Spivak) |Functorial data model, schema-as-category
+|HoTT |Identity types as equality primitive, paths between objects
+|Tutorial D |No NULLs, proper types, set semantics by default
+|===
+
+==== Avoid
+
+[cols=",,",options="header",]
+|===
+|Anti-Pattern |Source |Why
+|String-based queries |SQL |Injection by design
+|NULLs / three-valued logic |SQL |Use Option types
+|Bag semantics by default |SQL |Sets, with explicit multiset
+|Pseudo-English syntax |SQL |Consistent algebraic syntax
+|Vendor lock-in / proprietary |FQL |Fauna died, proving the risk
+|Language churn |Flux |Deprecating your own language burns users
+|Schemaless by default |MongoDB/SPARQL |Silent failures on typos
+|===
+
+'''''
+
+=== Part 7: Proposed KRL Architecture
+
+[arabic]
+. *Foundation:* Category-theoretic data model (Spivak). Schema =
+category, instance = functor.
+. *Equality model:* HoTT identity types. `+x == y+` returns a _type_
+(possibly empty, possibly inhabited, possibly multiply inhabited).
+"`These knots are equivalent, and here are the equivalences.`"
+. *Query syntax:* Pipeline-based (PRQL) + pattern matching (FP) +
+ASCII-art graph patterns (Cypher)
+. *Recursion:* Datalog-style fixed-point with equality saturation
+(egglog). Database maintains e-graphs.
+. *Type system:* Dependent types for invariants. Leverage Lean’s mathlib
+quandle formalization.
+. *No NULLs:* Option types.
+. *Provenance:* Built-in semiring annotations. Every result carries
+derivation metadata.
+. *Composability:* First-class. Queries are values. Named,
+parameterized, composed.
+
+==== Honest Risk Assessment
+
+* Building a new query language is enormous
+* Technical superiority doesn’t guarantee adoption (the QUEL problem)
+* *Mitigations:* Compile to SQL where possible, specialize where
+necessary, target the niche (mathematicians value correctness), leverage
+existing infrastructure (egglog/Rust, CQL/Java, DuckDB/C++)
+
+'''''
+
+=== Sources
+
+==== SQL Criticisms
+
+* Guagliardo & Libkin — Formal Semantics of SQL Queries
+* Ricciotti et al. — Formalization of SQL with Nulls
+* Neumann & Leis — A Critique of Modern SQL (CIDR 2024)
+* Jeff Atwood — ORM: Vietnam of Computer Science
+
+==== Key Papers
+
+* HoTTSQL (Chu et al., PLDI 2017) — https://arxiv.org/abs/1607.04822
+* egglog (PLDI 2023) — https://arxiv.org/abs/2304.04332
+* Spivak — Functorial Data Migration — https://arxiv.org/abs/1009.1166
+* CQL — https://categoricaldata.net/CQL/
+* GQL ISO Standard — https://www.iso.org/standard/76120.html
+
+==== Domain (Knot Theory)
+
+* KnotInfo — https://knots.dartmouth.edu/
+* Knot Atlas — https://katlas.org/wiki/The_Take_Home_Database
+* Lean mathlib quandles —
+https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Quandle.html
+* Data-Driven Knot Invariants (2025) —
+https://arxiv.org/html/2503.15103v1
+
+'''''
+
+_Preserved to ~/Desktop/ and nextgen-databases/quandledb/docs/design/_
diff --git a/docs/design/KRL-SQL-LANDSCAPE-RESEARCH-2026-02-22.md b/docs/design/KRL-SQL-LANDSCAPE-RESEARCH-2026-02-22.md
deleted file mode 100644
index 70d84cc..0000000
--- a/docs/design/KRL-SQL-LANDSCAPE-RESEARCH-2026-02-22.md
+++ /dev/null
@@ -1,274 +0,0 @@
-# KRL Design: SQL Landscape Research — 2026-02-22
-## Comprehensive Survey for QuandleDB Query Language Design
-
-**Date:** 2026-02-22
-**For:** nextgen-databases/quandledb
-**Agent:** Claude Opus 4.6
-**Status:** Research complete — design phase next
-
----
-
-## EXECUTIVE SUMMARY
-
-**SQL is the wrong paradigm for QuandleDB.** The right foundation is a synthesis of:
-
-1. **egglog** — equality saturation over Datalog (handles equivalence classes natively)
-2. **Spivak's categorical data model** — functorial data migration, schema as category
-3. **HoTT identity types** — paths = equivalences (from HoTTSQL paper)
-4. **Surfaced through:** PRQL-style pipeline syntax + Cypher-style graph pattern matching
-
-The closest existing system is **egglog** (PLDI 2023). The theoretical foundation is **HoTTSQL's univalent semantics**. KRL should build on both.
-
----
-
-## Part 1: What's Legitimately Wrong with SQL
-
-### NULL Handling (Three-Valued Logic)
-- NULL conflates "unknown," "inapplicable," "missing," "not yet entered" into one marker
-- `NULL = NULL` evaluates to UNKNOWN, not TRUE
-- `NOT IN` with NULLs produces surprising empty results
-- Codd himself proposed two kinds of null (A-marks/I-marks) — SQL never adopted this
-- Forces optimizers to be conservative (Guagliardo & Libkin showed real DBs return incorrect results due to NULL bugs)
-
-### Bag Semantics vs Set Semantics
-- SQL operates on bags (multisets), not sets — departure from Codd's relational model
-- Union is no longer idempotent; DISTINCT is an expensive band-aid
-- HoTTSQL proved bags can be modeled cleanly via univalent types (700+ lines Coq reduced to 40)
-
-### Composability (SQL's Most Damning Flaw)
-- Neumann & Leis (CIDR 2024): SQL is "a functional programming language that lacks parameters for functions"
-- Cannot pass a relation as an argument to a view definition
-- Cannot parameterize a query fragment
-- CTEs help readability but are just named subqueries — can't be parameterized
-- **QUEL was more composable** but lost to SQL because IBM shipped DB2 and Stonebraker didn't show up to the ANSI committee
-
-### Impedance Mismatch
-- SQL types don't map cleanly to programming language types
-- ORM-induced slowdowns of 2.6x-5x confirmed by research
-- The real problem: SQL forces a different paradigm from the host language
-
-### Type System Weakness
-- No sum types, no product types beyond rows, no generics, no type inference
-- CAST is explicit and lossy; implicit coercions vary by vendor
-- No standard way to define custom types with invariants
-
-### String-Based Injection by Design
-- Queries are strings where structure and data are concatenated
-- The "default, most obvious way" to use SQL is vulnerable
-- Prepared statements fix it in practice but the design is fundamentally flawed
-
-### Other Issues
-- ORDER BY only at outer query
-- WITH RECURSIVE is ugly and limited
-- Temporal data support abysmal (SQL:2011 exists, few implement it)
-- Window functions powerful but syntax baroque
-- GROUP BY / HAVING distinction is weird
-- Date/time handling is a mess across implementations
-- No built-in version/provenance tracking
-- Vendor fragmentation despite "standard"
-
----
-
-## Part 2: Every Notable Alternative and What's Wrong with THEM
-
-### QUEL (Ingres, 1976)
-- **Good:** More composable, based on tuple relational calculus
-- **Dead:** SQL won on market power (IBM), not technical merit. Stonebraker agreed SQL was worse.
-- **Lesson:** Technical superiority doesn't guarantee adoption. But niche domains CAN sustain better languages.
-
-### Datalog
-- **Good:** Declarative, naturally recursive, composable, clean formal semantics
-- **Bad:** No standard for aggregation/negation/updates, limited ordered data support
-- **Key:** egglog (PLDI 2023) unifies Datalog with equality saturation — directly relevant to QuandleDB
-
-### SPARQL
-- **Good:** Powerful pattern matching over graphs
-- **Bad:** Extremely verbose, schema-less means typos return empty results silently
-
-### Cypher (Neo4j) / GQL (ISO 39075:2024)
-- **Good:** ASCII-art pattern matching `(a)-[:KNOWS]->(b)` is genuinely intuitive
-- **Bad:** Limited analytics, performance degrades on large traversals
-- **GQL** is first new ISO DB language since SQL (1987). Adds quantified path patterns.
-- **Relevant:** Knot diagrams ARE graphs. Reidemeister moves ARE graph rewrites.
-
-### PRQL (Pipelined Relational Query Language)
-- **Good:** Pipeline syntax dramatically more readable. Compiles to SQL. Written in Rust.
-- **Bad:** Still relational — no equivalence classes
-- **Lesson:** Pipeline syntax is strictly superior to SQL's inside-out evaluation order
-
-### Malloy (Google / Lloyd Tabb)
-- **Good:** Semantic modeling. Created by Looker founder from frustration with SQL.
-- **Bad:** Not an official Google product. No support commitment. Limited adoption.
-
-### EdgeQL (EdgeDB, now "Gel")
-- **Good:** Modern SQL done right, object-relational model, unified typing
-- **Bad:** Hard to get started (TLS plumbing), doc gaps at complexity, write contention
-
-### FQL (Fauna) — DEAD
-- **SHUT DOWN May 2025.** Steep learning curve, proprietary, couldn't raise capital.
-- **Lesson:** Proprietary query languages die with their companies. Design for openness.
-
-### SurrealQL (SurrealDB)
-- **Good:** Multi-model with SQL-like syntax
-- **Bad:** Lack of type safety, SDK limitations, limited maturity
-
-### KQL (Kusto / Azure) — NAME COLLISION [Resolved]
-- **Good:** Pipeline syntax for log analytics
-- **Bad:** Read-only, can't INSERT/UPDATE, Azure lock-in
-- **Note:** Previously shared acronym with our language. Resolved by renaming our language to KRL (Knot Resolution Language).
-
-### DuckDB SQL Extensions
-- **Right:** Community extensions (6M downloads/week), SQL-only extensions, SQL/PGQ graph queries outperform Neo4j 10-100x
-- **Lesson:** SQL's extensibility CAN work if done right
-
-### Others
-- **Gremlin:** Imperative graph traversal. Verbose. Less optimizer freedom.
-- **MQL (MongoDB):** Schema-free = no compile-time safety. Aggregation pipeline unreadable.
-- **AQL (ArangoDB):** Multi-model but small community. BSL 1.1 license change (2024).
-- **PartiQL (AWS):** SQL over everything. Tightly coupled to AWS.
-- **CQL (Cassandra):** No JOINs, no ad hoc aggregations. Looks like SQL, can't do SQL.
-- **PromQL/InfluxQL/Flux:** Time-series specific. Flux was deprecated — language churn cautionary tale.
-
----
-
-## Part 3: Academic/Theoretical Criticisms
-
-### Codd vs SQL
-SQL departs from Codd's relational model: bags not sets, NULLs, ordering, duplicate column names, non-1NF data (JSON/arrays).
-
-### Third Manifesto (Date & Darwen)
-- SQL's problems are NOT the relational model's problems — they're SQL's
-- **Tutorial D** shows "SQL done right": proper types, no NULLs, set semantics, composability
-- Remains academic/pedagogical, no production implementation
-
-### Category Theory Approaches (Spivak)
-- Schema = small category. Instance = set-valued functor. Query = natural transformation.
-- **CQL** (Categorical Query Language) — open-source IDE, active development
-- Functorial data migration handles projections/unions/joins over ALL tables simultaneously
-- **Directly applicable:** Quandles are algebraic structures. Category theory IS the language for algebraic structure relationships.
-
-### HoTTSQL (Chu et al., PLDI 2017)
-- SQL semantics formalized via homotopy type theory
-- Relations as functions from tuples to univalent types
-- Bag equality proved via univalence axiom (700+ lines Coq → 40 lines)
-- **Critical insight for KRL:** Equality is not binary. Multiple distinct paths (proofs of equality) between objects. The space of equivalences has structure. THIS IS EXACTLY KNOT EQUIVALENCE.
-
-### egglog (PLDI 2023)
-- Merges Datalog with equality saturation
-- E-graph compactly represents exponentially many equivalent terms
-- Systems reimplemented in egglog are faster, simpler, fix bugs
-- PLDI 2025 tutorial scheduled (growing adoption)
-- **THIS MAY BE THE SINGLE MOST RELEVANT PARADIGM FOR QUANDLEDB**
-- An e-graph IS a database of equivalence classes = a knot database
-
-### Deductive Databases
-- Souffle (static analysis), Google Mangle (AI reasoning), Datalevin (general-purpose Datalog)
-- Revival driven by static analysis, AI reasoning, program optimization
-
----
-
-## Part 4: What SQL Gets RIGHT (Don't Throw Away)
-
-1. **Declarative semantics** — say what, not how. Enables optimizer freedom.
-2. **50 years of optimizer research** — join reordering, predicate pushdown, index selection
-3. **Ecosystem** — tools, tutorials, books, Stack Overflow, monitoring, migration tools
-4. **ACID transactions** — atomic, consistent, isolated, durable
-5. **The standard** — imperfect but exists; multiple vendors implement it
-6. **Window functions** — running totals, rankings, moving averages in single pass
-7. **CTEs** — break complex queries into named stages
-
----
-
-## Part 5: The QuandleDB Domain Problem
-
-### The Core Challenge
-QuandleDB stores mathematical structures where the fundamental operation is *equivalence under transformation*. Two knots may look completely different but be the same (related by Reidemeister moves). SQL's `WHERE x = y` is syntactic/value equality. QuandleDB needs *semantic* equality.
-
-### Scale
-- KnotInfo: 350 million prime knots up to 19 crossings, 1.9 billion at 20
-- 17,528 unresolved 20-crossing knots that resist all known invariants
-- Multiple invariants per knot (Alexander, Jones, Khovanov, etc.)
-
-### Relevant Query Paradigms
-
-| Paradigm | Relevance | How |
-|----------|-----------|-----|
-| **Pattern matching** (FP) | High | Decompose knot diagrams by structure |
-| **Unification** (Prolog) | High | Find structural constraints, variable binding |
-| **Term rewriting** | Critical | Reidemeister moves ARE rewrite rules |
-| **Category theory** (Spivak) | Critical | Quandles are algebraic structures in categories |
-| **HoTT paths** | Critical | Paths = equivalences, space of equivalences has structure |
-| **Equality saturation** (egglog) | Critical | E-graphs ARE databases of equivalence classes |
-| **Provenance semirings** | High | Track which invariants led to equivalence determination |
-
----
-
-## Part 6: What KRL Should Borrow vs Avoid
-
-### Borrow
-| Source | What |
-|--------|------|
-| SQL | Declarative semantics, optimizer freedom, transactions |
-| PRQL | Pipeline syntax (`from ... | filter ... | aggregate ...`) |
-| Cypher/GQL | ASCII-art pattern matching for graph structures |
-| Datalog | Recursive queries, rule-based reasoning |
-| egglog | Equality saturation, e-graph equivalence classes |
-| CQL (Spivak) | Functorial data model, schema-as-category |
-| HoTT | Identity types as equality primitive, paths between objects |
-| Tutorial D | No NULLs, proper types, set semantics by default |
-
-### Avoid
-| Anti-Pattern | Source | Why |
-|-------------|--------|-----|
-| String-based queries | SQL | Injection by design |
-| NULLs / three-valued logic | SQL | Use Option types |
-| Bag semantics by default | SQL | Sets, with explicit multiset |
-| Pseudo-English syntax | SQL | Consistent algebraic syntax |
-| Vendor lock-in / proprietary | FQL | Fauna died, proving the risk |
-| Language churn | Flux | Deprecating your own language burns users |
-| Schemaless by default | MongoDB/SPARQL | Silent failures on typos |
-
----
-
-## Part 7: Proposed KRL Architecture
-
-1. **Foundation:** Category-theoretic data model (Spivak). Schema = category, instance = functor.
-2. **Equality model:** HoTT identity types. `x == y` returns a *type* (possibly empty, possibly inhabited, possibly multiply inhabited). "These knots are equivalent, and here are the equivalences."
-3. **Query syntax:** Pipeline-based (PRQL) + pattern matching (FP) + ASCII-art graph patterns (Cypher)
-4. **Recursion:** Datalog-style fixed-point with equality saturation (egglog). Database maintains e-graphs.
-5. **Type system:** Dependent types for invariants. Leverage Lean's mathlib quandle formalization.
-6. **No NULLs:** Option types.
-7. **Provenance:** Built-in semiring annotations. Every result carries derivation metadata.
-8. **Composability:** First-class. Queries are values. Named, parameterized, composed.
-
-### Honest Risk Assessment
-- Building a new query language is enormous
-- Technical superiority doesn't guarantee adoption (the QUEL problem)
-- **Mitigations:** Compile to SQL where possible, specialize where necessary, target the niche (mathematicians value correctness), leverage existing infrastructure (egglog/Rust, CQL/Java, DuckDB/C++)
-
----
-
-## Sources
-
-### SQL Criticisms
-- Guagliardo & Libkin — Formal Semantics of SQL Queries
-- Ricciotti et al. — Formalization of SQL with Nulls
-- Neumann & Leis — A Critique of Modern SQL (CIDR 2024)
-- Jeff Atwood — ORM: Vietnam of Computer Science
-
-### Key Papers
-- HoTTSQL (Chu et al., PLDI 2017) — https://arxiv.org/abs/1607.04822
-- egglog (PLDI 2023) — https://arxiv.org/abs/2304.04332
-- Spivak — Functorial Data Migration — https://arxiv.org/abs/1009.1166
-- CQL — https://categoricaldata.net/CQL/
-- GQL ISO Standard — https://www.iso.org/standard/76120.html
-
-### Domain (Knot Theory)
-- KnotInfo — https://knots.dartmouth.edu/
-- Knot Atlas — https://katlas.org/wiki/The_Take_Home_Database
-- Lean mathlib quandles — https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Quandle.html
-- Data-Driven Knot Invariants (2025) — https://arxiv.org/html/2503.15103v1
-
----
-
-*Preserved to ~/Desktop/ and nextgen-databases/quandledb/docs/design/*
diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc
new file mode 100644
index 0000000..7d465f2
--- /dev/null
+++ b/docs/tech-debt-2026-05-26.adoc
@@ -0,0 +1,67 @@
+== Tech-Debt Audit — quandledb — 2026-05-26
+
+*Source:* estate-wide automated scan 2026-05-26. *Companion:*
+https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+`
+2026-05-26-estate-*-debt audits]. *Combined severity:* `+MEDIUM+`.
+
+This file records the _raw findings_ — it does not by itself fix the
+debt. Each section ends with a '`Recommended next move`' line; closing
+the debt is follow-up work.
+
+=== 1. Proof debt
+
+No proof-bearing files (`+*.v+`, `+*.lean+`, `+*.agda+`, `+*.idr+`,
+`+*.idr2+`, `+*.fst+`, `+*.dfy+`, `+*.tla+`, `+*.ads+`, `+*.adb+`) found
+in this repo.
+
+*Recommended next move:* none.
+
+=== 2. Licence debt
+
+[cols=",",options="header",]
+|===
+|Field |Value
+|LICENSE file |`+LICENSE+`
+|SPDX header |`+MPL-2.0+`
+|Manifest licence |`+NONE+`
+|Body classifier |`+MPL-some+`
+|Severity |`+ok+`
+|===
+
+*Recommended next move:* none for licence.
+
+=== 3. Documentation debt
+
+[cols=",",options="header",]
+|===
+|Field |Value
+|README lines |143
+|`+docs/+` files |2
+|`+docs/+` LoC |391
+|CHANGELOG.md |Y
+|CONTRIBUTING.md |Y
+|CODE_OF_CONDUCT.md |Y
+|SECURITY.md |Y
+|Severity |`+MEDIUM+`
+|===
+
+*Recommended next move:* introduce a `+docs/+` directory. The README at
+143 lines has likely grown to do the work of `+docs/+` — split it into a
+thin README + `+docs/architecture.md+`, `+docs/usage.md+`, etc.
+Heavy-wiki exemplars to copy from: `+affinescript+`, `+boj-server+`,
+`+echidna+`, `+hypatia+`.
+
+=== Cross-references
+
+* Estate proof-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+`
+* Estate licence-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+`
+* Estate documentation-debt audit:
+`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+`
+
+'''''
+
+🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26).
+This file is informational — closing the debt is follow-up work owned by
+the maintainer.
diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md
deleted file mode 100644
index d88eadd..0000000
--- a/docs/tech-debt-2026-05-26.md
+++ /dev/null
@@ -1,55 +0,0 @@
-<!--
-SPDX-License-Identifier: CC-BY-SA-4.0
-SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
--->
-
-# Tech-Debt Audit — quandledb — 2026-05-26
-
-**Source:** estate-wide automated scan 2026-05-26.
-**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits).
-**Combined severity:** `MEDIUM`.
-
-This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work.
-
-## 1. Proof debt
-
-No proof-bearing files (`*.v`, `*.lean`, `*.agda`, `*.idr`, `*.idr2`, `*.fst`, `*.dfy`, `*.tla`, `*.ads`, `*.adb`) found in this repo.
-
-**Recommended next move:** none.
-
-## 2. Licence debt
-
-| Field | Value |
-|---|---|
-| LICENSE file | `LICENSE` |
-| SPDX header | `MPL-2.0` |
-| Manifest licence | `NONE` |
-| Body classifier | `MPL-some` |
-| Severity | `ok` |
-
-**Recommended next move:** none for licence.
-
-## 3. Documentation debt
-
-| Field | Value |
-|---|---|
-| README lines | 143 |
-| `docs/` files | 2 |
-| `docs/` LoC | 391 |
-| CHANGELOG.md | Y |
-| CONTRIBUTING.md | Y |
-| CODE_OF_CONDUCT.md | Y |
-| SECURITY.md | Y |
-| Severity | `MEDIUM` |
-
-**Recommended next move:** introduce a `docs/` directory. The README at 143 lines has likely grown to do the work of `docs/` — split it into a thin README + `docs/architecture.md`, `docs/usage.md`, etc. Heavy-wiki exemplars to copy from: `affinescript`, `boj-server`, `echidna`, `hypatia`.
-
-## Cross-references
-
-- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md`
-- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md`
-- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md`
-
----
-
-🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer.
diff --git a/spec/dependent-type-variants.md b/spec/dependent-type-variants.adoc
similarity index 62%
rename from spec/dependent-type-variants.md
rename to spec/dependent-type-variants.adoc
index ef94974..f72004c 100644
--- a/spec/dependent-type-variants.md
+++ b/spec/dependent-type-variants.adoc
@@ -1,72 +1,75 @@
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+== SPDX-License-Identifier: CC-BY-SA-4.0
 
-# KRL Dependent Type Variants
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
 
-**Version:** 0.1.0
-**Date:** 2026-03-20
+== KRL Dependent Type Variants
 
----
+*Version:* 0.1.0 *Date:* 2026-03-20
 
-## 1. Overview
+'''''
 
-KRL's type system goes beyond conventional query language types (SQL's
-scalar types, GraphQL's object types) by incorporating **dependent types**
+=== 1. Overview
+
+KRL’s type system goes beyond conventional query language types (SQL’s
+scalar types, GraphQL’s object types) by incorporating *dependent types*
 — types that depend on values. This enables:
 
-1. **Pipeline type safety:** The type of a query result depends on which
-   stages appear in the pipeline (dependent projection).
-2. **Confidence-indexed results:** The type of an equivalence result
-   depends on the confidence level achieved during evaluation.
-3. **Invariant-dependent records:** The fields available in a result
-   depend on which invariants were requested.
-4. **Stratum-bounded evaluation:** The evaluation strategy is indexed by
-   the number of invariant strata, proving termination.
+[arabic]
+. *Pipeline type safety:* The type of a query result depends on which
+stages appear in the pipeline (dependent projection).
+. *Confidence-indexed results:* The type of an equivalence result
+depends on the confidence level achieved during evaluation.
+. *Invariant-dependent records:* The fields available in a result depend
+on which invariants were requested.
+. *Stratum-bounded evaluation:* The evaluation strategy is indexed by
+the number of invariant strata, proving termination.
 
 This document specifies how these dependent types surface in the KRL
 language and how they map to Idris2 ABI proofs.
 
----
+'''''
 
-## 2. Dependent Projection (Pipeline Type Refinement)
+=== 2. Dependent Projection (Pipeline Type Refinement)
 
-### 2.1 The Problem
+==== 2.1 The Problem
 
-In SQL, `SELECT a, b FROM t` always produces a two-column result, but
+In SQL, `+SELECT a, b FROM t+` always produces a two-column result, but
 the schema of the result is only checked at planning time — not at the
-type level. In KRL, the `return` clause is a **dependent projection**:
+type level. In KRL, the `+return+` clause is a *dependent projection*:
 the return type is computed from the fields listed.
 
-### 2.2 Typing Rule
+==== 2.2 Typing Rule
 
-```
+....
     Γ ⊢ R : ResultSet[τ]     fields ⊆ fields(τ)
     Π(τ, fields) = τ'
     ──────────────────────────────────────────────  [T-Dep-Return]
     Γ ⊢ R | return fields : ResultSet[τ']
-```
+....
 
-Here, `Π(τ, fields)` is a **type-level function** that computes the
+Here, `+Π(τ, fields)+` is a *type-level function* that computes the
 projected record type. This is a dependent type: the output type depends
-on the value `fields`.
+on the value `+fields+`.
 
-### 2.3 Idris2 ABI Proof
+==== 2.3 Idris2 ABI Proof
 
-```idris
+[source,idris]
+----
 -- Pipeline type refinement: projection preserves well-formedness
 data Project : (fields : List String) -> KqlTy -> KqlTy -> Type where
   ProjectNil  : Project [] (TyRecord fs) (TyRecord [])
   ProjectCons : Elem (f, t) fs -> Project rest (TyRecord fs) (TyRecord fs')
              -> Project (f :: rest) (TyRecord fs) (TyRecord ((f, t) :: fs'))
-```
+----
 
 This proves that projecting a list of field names from a record type
-produces a valid sub-record type, and each projected field must exist
-in the source record (via `Elem` proof).
+produces a valid sub-record type, and each projected field must exist in
+the source record (via `+Elem+` proof).
 
-### 2.4 User-Facing Syntax
+==== 2.4 User-Facing Syntax
 
-```krl
+[source,krl]
+----
 -- The return clause determines the result type
 from knots
 | return name, crossing_number
@@ -80,22 +83,22 @@ from knots
 from knots
 | return name, foobar
 -- Error: Field 'foobar' not found in record type Knot
-```
+----
 
----
+'''''
 
-## 3. Confidence-Indexed Equivalence Types
+=== 3. Confidence-Indexed Equivalence Types
 
-### 3.1 The Problem
+==== 3.1 The Problem
 
 When KRL reports that two knots are equivalent, the strength of that
 claim depends on which invariants were used. Jones polynomial matching
-is *necessary* but not *sufficient*; quandle isomorphism is *exact*.
-The type of the result should reflect this.
+is _necessary_ but not _sufficient_; quandle isomorphism is _exact_. The
+type of the result should reflect this.
 
-### 3.2 Type Variants
+==== 3.2 Type Variants
 
-```
+....
 Equivalence[τ, c] where c : Confidence
 
 -- Four variants, indexed by confidence level:
@@ -103,11 +106,11 @@ Equivalence[Knot, Exact]      -- proven by complete invariant
 Equivalence[Knot, Sufficient] -- proven by sufficient invariant combination
 Equivalence[Knot, Necessary]  -- all necessary conditions met, not proven
 Equivalence[Knot, Heuristic]  -- statistical match only
-```
+....
 
-### 3.3 Typing Rules
+==== 3.3 Typing Rules
 
-```
+....
     Γ ⊢ R : ResultSet[Knot]     inv ∈ exact_invariants
     ─────────────────────────────────────────────────────────────  [T-Equiv-Exact]
     Γ ⊢ R | find_equivalent K via [inv] : ResultSet[Equivalence[Knot, Exact]]
@@ -120,11 +123,12 @@ Equivalence[Knot, Heuristic]  -- statistical match only
     ─────────────────────────────────────────────────────────────  [T-Equiv-Threshold]
     Γ ⊢ R | find_equivalent K via [invs] confidence >= c
         : ResultSet[Equivalence[Knot, c]]
-```
+....
 
-### 3.4 Idris2 ABI Proof
+==== 3.4 Idris2 ABI Proof
 
-```idris
+[source,idris]
+----
 -- Confidence-indexed equivalence type
 data ConfEquiv : KqlTy -> Confidence -> Type where
   MkConfEquiv : (source : Knot) -> (target : Knot)
@@ -135,11 +139,12 @@ data ConfEquiv : KqlTy -> Confidence -> Type where
 
 -- Combining two equivalence results: confidence is the minimum
 combineConf : ConfEquiv t c1 -> ConfEquiv t c2 -> ConfEquiv t (MinConf c1 c2)
-```
+----
 
-### 3.5 User-Facing Syntax
+==== 3.5 User-Facing Syntax
 
-```krl
+[source,krl]
+----
 -- Request only exact results
 from knots
 | find_equivalent "3_1" via [quandle] confidence >= exact
@@ -154,25 +159,24 @@ from knots
 from knots
 | find_equivalent "3_1" via [jones]
 -- Type: ResultSet[Equivalence[Knot, Heuristic]]
-```
+----
 
----
+'''''
 
-## 4. Invariant-Dependent Records
+=== 4. Invariant-Dependent Records
 
-### 4.1 The Problem
+==== 4.1 The Problem
 
-Different invariants produce different types:
-- `crossing_number` produces `Int`
-- `jones_polynomial` produces `Polynomial`
-- `quandle` produces `Quandle`
+Different invariants produce different types: - `+crossing_number+`
+produces `+Int+` - `+jones_polynomial+` produces `+Polynomial+` -
+`+quandle+` produces `+Quandle+`
 
 When a query requests specific invariants, the result type should
 reflect exactly which fields are available.
 
-### 4.2 Type-Level Invariant Registry
+==== 4.2 Type-Level Invariant Registry
 
-```
+....
 InvariantType : InvariantName -> KqlTy
 
 InvariantType "crossing_number"  = TyInt
@@ -180,11 +184,12 @@ InvariantType "writhe"           = TyInt
 InvariantType "genus"            = TyOption TyInt
 InvariantType "jones_polynomial" = TyOption TyPolynomial
 InvariantType "quandle"          = TyOption TyQuandle
-```
+....
 
-### 4.3 Dependent Via Clause
+==== 4.3 Dependent Via Clause
 
-```krl
+[source,krl]
+----
 -- The 'via' clause determines which invariant fields appear in results
 from knots
 | find_equivalent "3_1" via [jones, genus]
@@ -192,11 +197,12 @@ from knots
 -- Each equivalence path carries:
 --   {method: "jones", evidence: Polynomial, confidence: Necessary}
 --   {method: "genus", evidence: Option[Int], confidence: Necessary}
-```
+----
 
-### 4.4 Idris2 ABI
+==== 4.4 Idris2 ABI
 
-```idris
+[source,idris]
+----
 -- Type-level invariant registry
 InvType : String -> KqlTy
 InvType "crossing_number" = TyInt
@@ -213,21 +219,22 @@ data ViaClause : List String -> Type where
 
 -- Result type depends on the via clause
 ViaResultType : ViaClause invs -> KqlTy
-```
+----
 
----
+'''''
 
-## 5. Stratum-Bounded Evaluation
+=== 5. Stratum-Bounded Evaluation
 
-### 5.1 The Problem
+==== 5.1 The Problem
 
-KRL's equivalence queries evaluate invariants in order of increasing
-cost (crossing number is cheap; quandle isomorphism is expensive).
-The type system must guarantee that evaluation terminates.
+KRL’s equivalence queries evaluate invariants in order of increasing
+cost (crossing number is cheap; quandle isomorphism is expensive). The
+type system must guarantee that evaluation terminates.
 
-### 5.2 Stratified Evaluation Type
+==== 5.2 Stratified Evaluation Type
 
-```idris
+[source,idris]
+----
 -- Evaluation indexed by stratum count
 data StratEval : (n : Nat) -> Type where
   EvalDone : StratEval 0
@@ -235,15 +242,16 @@ data StratEval : (n : Nat) -> Type where
           -> (result : Either ShortCircuit Provenance)
           -> StratEval n
           -> StratEval (S n)
-```
+----
 
-This is a dependent type: the evaluation trace has type `StratEval n`
-where `n` is the number of strata. Since `n : Nat` is finite and each
-step strictly decreases it, evaluation is provably terminating.
+This is a dependent type: the evaluation trace has type `+StratEval n+`
+where `+n+` is the number of strata. Since `+n : Nat+` is finite and
+each step strictly decreases it, evaluation is provably terminating.
 
-### 5.3 Termination Proof
+==== 5.3 Termination Proof
 
-```idris
+[source,idris]
+----
 -- Stratified evaluation terminates: each step reduces the stratum count
 stratTerminates : (n : Nat) -> StratEval n -> Nat
 stratTerminates 0 EvalDone = 0
@@ -253,33 +261,47 @@ stratTerminates (S k) (EvalStep _ _ rest) = S (stratTerminates k rest)
 stratStepCount : (n : Nat) -> (eval : StratEval n) -> stratTerminates n eval = n
 stratStepCount 0 EvalDone = Refl
 stratStepCount (S k) (EvalStep _ _ rest) = cong S (stratStepCount k rest)
-```
+----
+
+'''''
+
+=== 6. Dependent Type Variant Summary
+
+[width="100%",cols="24%,26%,19%,31%",options="header",]
+|===
+|Variant |Depends On |Proves |User Syntax
+|*Dependent Projection* |Field names in `+return+` clause |Result record
+matches requested fields |`+return name, x+`
+
+|*Confidence-Indexed Equiv* |Confidence level in `+confidence >=+`
+|Result confidence meets threshold |`+confidence >= exact+`
 
----
+|*Invariant-Dependent Records* |Invariant names in `+via+` clause
+|Evidence types match invariant types |`+via [jones, genus]+`
 
-## 6. Dependent Type Variant Summary
+|*Stratum-Bounded Eval* |Number of invariant strata |Evaluation
+terminates |(implicit)
 
-| Variant | Depends On | Proves | User Syntax |
-|---------|-----------|--------|-------------|
-| **Dependent Projection** | Field names in `return` clause | Result record matches requested fields | `return name, x` |
-| **Confidence-Indexed Equiv** | Confidence level in `confidence >=` | Result confidence meets threshold | `confidence >= exact` |
-| **Invariant-Dependent Records** | Invariant names in `via` clause | Evidence types match invariant types | `via [jones, genus]` |
-| **Stratum-Bounded Eval** | Number of invariant strata | Evaluation terminates | (implicit) |
-| **Pipeline Composition** | Sequence of pipeline stages | Each stage preserves ResultSet type | `| stage1 | stage2` |
+|*Pipeline Composition* |Sequence of pipeline stages |Each stage
+preserves ResultSet type |`+| stage1 | stage2+`
+|===
 
----
+'''''
 
-## 7. Relationship to Idris2 ABI
+=== 7. Relationship to Idris2 ABI
 
 All dependent type variants have corresponding Idris2 proofs in
-`src/abi/Types.idr`. The ABI layer provides:
+`+src/abi/Types.idr+`. The ABI layer provides:
 
-1. **Type definitions** (`KqlTy`, `PipeStage`, `Pipeline`, `Confidence`)
-2. **Proofs** (`pipeAssoc`, `combinePreservesInvariants`, `StratumBounded`)
-3. **Translation** — each KRL type variant maps to an Idris2 type that
-   can be type-checked at compile time
+[arabic]
+. *Type definitions* (`+KqlTy+`, `+PipeStage+`, `+Pipeline+`,
+`+Confidence+`)
+. *Proofs* (`+pipeAssoc+`, `+combinePreservesInvariants+`,
+`+StratumBounded+`)
+. *Translation* — each KRL type variant maps to an Idris2 type that can
+be type-checked at compile time
 
 The SQL compatibility layer (§sql-compat.md) translates SQL queries into
-KRL AST nodes, which are then type-checked against these dependent types.
-SQL queries that would produce ill-typed results (e.g., projecting a
-non-existent field) are rejected at translation time.
+KRL AST nodes, which are then type-checked against these dependent
+types. SQL queries that would produce ill-typed results (e.g.,
+projecting a non-existent field) are rejected at translation time.
diff --git a/spec/operational-semantics.md b/spec/operational-semantics.adoc
similarity index 81%
rename from spec/operational-semantics.md
rename to spec/operational-semantics.adoc
index 84183a1..877b6c9 100644
--- a/spec/operational-semantics.md
+++ b/spec/operational-semantics.adoc
@@ -1,25 +1,25 @@
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+== SPDX-License-Identifier: CC-BY-SA-4.0
 
-# KRL Operational Semantics
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
 
-**Version:** 0.1.0
-**Date:** 2026-03-14
+== KRL Operational Semantics
 
----
+*Version:* 0.1.0 *Date:* 2026-03-14
 
-## 1. Notation
+'''''
 
-- `D` — Database state (knot store, invariant cache, e-graph)
-- `ρ` — Query environment (bound variables)
-- `D, ρ ⊢ q ⇓ R` — Query `q` evaluates to result set `R`
-- `⊥` — Error
+=== 1. Notation
 
----
+* `+D+` — Database state (knot store, invariant cache, e-graph)
+* `+ρ+` — Query environment (bound variables)
+* `+D, ρ ⊢ q ⇓ R+` — Query `+q+` evaluates to result set `+R+`
+* `+⊥+` — Error
 
-## 2. Values
+'''''
 
-```
+=== 2. Values
+
+....
 v ∈ Value ::=
     n ∈ ℤ                                    integer
   | f ∈ ℝ                                    float
@@ -34,11 +34,11 @@ v ∈ Value ::=
   | {f₁: v₁, …, fₙ: vₙ}                     record
   | Equiv(K₁, K₂, paths)                     equivalence evidence
   | Provenance(invariants, confidence, cost)  provenance annotation
-```
+....
 
-### 2.1 Knot Record
+==== 2.1 Knot Record
 
-```
+....
 Knot = ⟨ name             : String,
          gauss_code       : GaussCode,
          crossing_number  : ℕ,
@@ -47,39 +47,39 @@ Knot = ⟨ name             : String,
          seifert_circles  : Option<ℕ>,
          jones_polynomial : Option<Polynomial>,
          metadata         : Map<String, String> ⟩
-```
+....
 
----
+'''''
 
-## 3. Database State
+=== 3. Database State
 
-```
+....
 D = ⟨ knots      : Set<Knot>,
       invariants : Knot → InvariantName → Option<Value>,
       egraph     : EGraph,
       rules      : List<Rule> ⟩
 
 EGraph = equivalence classes over Knot, saturated by rules
-```
+....
 
----
+'''''
 
-## 4. Pipeline Semantics
+=== 4. Pipeline Semantics
 
 KRL queries are pipelines: each stage transforms a result set.
 
-```
+....
     D, ρ ⊢ from_clause ⇓ R₀
     D, ρ ⊢ stage₁(R₀) ⇓ R₁
     …
     D, ρ ⊢ stageₙ(Rₙ₋₁) ⇓ Rₙ
     ──────────────────────────────────────────────  [Pipeline]
     D, ρ ⊢ from … | stage₁ | … | stageₙ ⇓ Rₙ
-```
+....
 
-### 4.1 From
+==== 4.1 From
 
-```
+....
     ────────────────────────────────  [From-Knots]
     D, ρ ⊢ from knots ⇓ D.knots
 
@@ -89,28 +89,28 @@ KRL queries are pipelines: each stage transforms a result set.
     D, ρ ⊢ q ⇓ R
     ────────────────────────────────  [From-Subquery]
     D, ρ ⊢ from (q) ⇓ R
-```
+....
 
-### 4.2 Filter
+==== 4.2 Filter
 
-```
+....
     ∀k ∈ R: ρ[k], D ⊢ expr ⇓ bₖ
     R' = { k ∈ R | truthy(bₖ) }
     ──────────────────────────────────  [Filter]
     D, ρ ⊢ filter expr (R) ⇓ R'
-```
+....
 
-### 4.3 Sort
+==== 4.3 Sort
 
-```
+....
     R' = sort R by (λk. ρ[k], D ⊢ expr ⇓ vₖ) [asc|desc]
     ──────────────────────────────────────────────────────  [Sort]
     D, ρ ⊢ sort expr [asc|desc] (R) ⇓ R'
-```
+....
 
-### 4.4 Take / Skip
+==== 4.4 Take / Skip
 
-```
+....
     R' = R[0..n]
     ────────────────────────  [Take]
     D, ρ ⊢ take n (R) ⇓ R'
@@ -118,11 +118,11 @@ KRL queries are pipelines: each stage transforms a result set.
     R' = R[n..]
     ────────────────────────  [Skip]
     D, ρ ⊢ skip n (R) ⇓ R'
-```
+....
 
-### 4.5 Return
+==== 4.5 Return
 
-```
+....
     ∀k ∈ R: project fields from k
     R' = [{ f₁: k.f₁, …, fₘ: k.fₘ } | k ∈ R]
     ──────────────────────────────────────────  [Return]
@@ -132,32 +132,32 @@ KRL queries are pipelines: each stage transforms a result set.
     R' = [{ …k, _provenance: prov(k) } | k ∈ R]
     ──────────────────────────────────────────────  [Return-Provenance]
     D, ρ ⊢ return … with provenance (R) ⇓ R'
-```
+....
 
-### 4.6 Group / Aggregate
+==== 4.6 Group / Aggregate
 
-```
+....
     groups = partition R by (λk. ρ[k] ⊢ key_expr ⇓ gₖ)
     ∀g: agg_result(g) = apply aggregate_fn to g
     ────────────────────────────────────────────────  [Aggregate]
     D, ρ ⊢ group_by key | aggregate fn(expr) (R) ⇓ [agg_result(g) | g ∈ groups]
-```
+....
 
-### 4.7 Let (inline binding)
+==== 4.7 Let (inline binding)
 
-```
+....
     D, ρ ⊢ expr ⇓ v     ρ' = ρ[x ↦ v]
     ─────────────────────────────────────  [Let]
     D, ρ ⊢ let x = expr (R) ⇓ R  (with ρ' for subsequent stages)
-```
+....
 
----
+'''''
 
-## 5. Equivalence Queries
+=== 5. Equivalence Queries
 
-### 5.1 Find Equivalent (Propositional Equality ≅)
+==== 5.1 Find Equivalent (Propositional Equality ≅)
 
-```
+....
     D.invariants(target, inv_name) = v_target     for each inv in invariant_list
     candidates = { k ∈ R | ∀inv ∈ invariant_list:
                      D.invariants(k, inv) = D.invariants(target, inv) }
@@ -166,11 +166,11 @@ KRL queries are pipelines: each stage transforms a result set.
     ─────────────────────────────────────────────────────────────────────  [FindEquiv]
     D, ρ ⊢ find_equivalent target via [inv₁, …, invₘ] (R)
       ⇓ [{ knot: k, equivalence_evidence: evidence(k) } | k ∈ candidates]
-```
+....
 
-### 5.2 Confidence Levels
+==== 5.2 Confidence Levels
 
-```
+....
 confidence : InvariantName → ConfidenceLevel
 
 confidence(crossing_number)  = necessary        (matching is necessary but not sufficient)
@@ -180,14 +180,14 @@ confidence(jones_polynomial) = exact             (matching is strong evidence)
 confidence(alexander)        = exact
 confidence(homfly)           = exact
 confidence(quandle)          = sufficient        (isomorphism implies equivalence)
-```
+....
 
-### 5.3 Stratified Evaluation
+==== 5.3 Stratified Evaluation
 
-Invariants are evaluated in order of increasing cost. Early strata can refute
-equivalence quickly (short-circuit):
+Invariants are evaluated in order of increasing cost. Early strata can
+refute equivalence quickly (short-circuit):
 
-```
+....
     stratum(crossing_number) = 0     (O(1) lookup)
     stratum(genus)           = 1     (O(n) computation)
     stratum(jones)           = 2     (O(2^n) in crossing number)
@@ -199,15 +199,15 @@ equivalence quickly (short-circuit):
       if all match → proceed to next stratum
     ───────────────────────────────────────────────────  [Stratified]
     Evaluation terminates at first refutation or exhaustion of strata
-```
+....
 
----
+'''''
 
-## 6. Path Queries
+=== 6. Path Queries
 
-### 6.1 Find Path (Path Equality ~>)
+==== 6.1 Find Path (Path Equality ~>)
 
-```
+....
     D ⊢ search_reidemeister(source_diagram, target_diagram) = path
     path = [move₁, move₂, …, moveₖ]     each moveᵢ ∈ {R1, R2, R3}
     ─────────────────────────────────────────────────────────────────  [FindPath]
@@ -217,35 +217,35 @@ equivalence quickly (short-circuit):
     no path found within search limit
     ──────────────────────────────────────────────  [FindPath-NotFound]
     D, ρ ⊢ find_path … ⇓ []
-```
+....
 
----
+'''''
 
-## 7. Graph Pattern Matching
+=== 7. Graph Pattern Matching
 
-```
+....
     ∀(K₁, K₂) ∈ R × R:
       edge_exists(K₁, label, K₂) = D.edges(K₁, label, K₂)
       properties_match(K₁, K₂, constraints)
     R' = [(K₁, K₂) | (K₁, K₂) matching pattern]
     ────────────────────────────────────────────────  [Match]
     D, ρ ⊢ match (K1)-[:LABEL]->(K2) (R) ⇓ R'
-```
+....
 
----
+'''''
 
-## 8. Rule Definitions (Datalog)
+=== 8. Rule Definitions (Datalog)
 
-```
+....
     D' = D ∪ { rule(name, params, body) }
     D' ⊢ saturate(egraph)     (fixed-point equality saturation)
     ──────────────────────────────────────────────────────────  [Rule-Def]
     D, ρ ⊢ rule name(params) :- body ⇒ D'
-```
+....
 
-### 8.1 Equality Saturation
+==== 8.1 Equality Saturation
 
-```
+....
     egraph₀ = initial e-graph from D.knots
     repeat:
       ∀rule ∈ D.rules:
@@ -254,13 +254,13 @@ equivalence quickly (short-circuit):
     until fixed point (no new merges)
     ──────────────────────────────────────────  [Saturate]
     saturate(D) ⇓ D[egraph ↦ egraph_saturated]
-```
+....
 
----
+'''''
 
-## 9. Expressions
+=== 9. Expressions
 
-```
+....
     ρ ⊢ x ⇓ ρ(x)                              [Var]
     ρ ⊢ lit ⇓ lit                              [Lit]
     ρ ⊢ e₁ ⊕ e₂ ⇓ eval(e₁) ⊕ eval(e₂)        [BinOp]
@@ -268,15 +268,16 @@ equivalence quickly (short-circuit):
     ρ ⊢ f(args) ⇓ apply(f, eval(args))         [Call]
     ρ ⊢ [e₁, …, eₙ] ⇓ [eval(e₁), …, eval(eₙ)] [Array]
     ρ ⊢ {f₁: e₁, …} ⇓ {f₁: eval(e₁), …}      [Record]
-```
+....
 
----
+'''''
 
-## 10. Provenance Semantics
+=== 10. Provenance Semantics
 
-Every result carries provenance as a semiring annotation (Green et al., 2007):
+Every result carries provenance as a semiring annotation (Green et al.,
+2007):
 
-```
+....
 Provenance = ⟨ invariants_used : Set<InvariantName>,
                confidence      : ConfidenceLevel,
                computation_path: List<Step>,
@@ -286,15 +287,23 @@ combine(p₁, p₂) = ⟨ p₁.invariants ∪ p₂.invariants,
                      min(p₁.confidence, p₂.confidence),
                      p₁.path ++ p₂.path,
                      p₁.time + p₂.time ⟩
-```
-
----
-
-## 11. Invariants
-
-1. **Pipeline compositionality:** Each stage is a pure function on result sets.
-2. **Stratified termination:** Invariant evaluation terminates because strata are finite and evaluation at each stratum terminates (except quandle, which has a search limit).
-3. **Provenance completeness:** Every equivalence result carries evidence of which invariants matched.
-4. **Short-circuit correctness:** If any necessary invariant differs, the knots are provably non-equivalent.
-5. **E-graph confluence:** Equality saturation reaches a unique fixed point regardless of rule application order.
-6. **Deterministic collapse:** Given the same database state and query, results are deterministic.
+....
+
+'''''
+
+=== 11. Invariants
+
+[arabic]
+. *Pipeline compositionality:* Each stage is a pure function on result
+sets.
+. *Stratified termination:* Invariant evaluation terminates because
+strata are finite and evaluation at each stratum terminates (except
+quandle, which has a search limit).
+. *Provenance completeness:* Every equivalence result carries evidence
+of which invariants matched.
+. *Short-circuit correctness:* If any necessary invariant differs, the
+knots are provably non-equivalent.
+. *E-graph confluence:* Equality saturation reaches a unique fixed point
+regardless of rule application order.
+. *Deterministic collapse:* Given the same database state and query,
+results are deterministic.
diff --git a/spec/sql-compat.adoc b/spec/sql-compat.adoc
new file mode 100644
index 0000000..56fc8be
--- /dev/null
+++ b/spec/sql-compat.adoc
@@ -0,0 +1,264 @@
+== SPDX-License-Identifier: CC-BY-SA-4.0
+
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
+
+== KRL–SQL Compatibility Layer
+
+*Version:* 0.1.0 *Date:* 2026-03-20
+
+'''''
+
+=== 1. Purpose
+
+This document defines how standard SQL (ISO 9075) concepts map to KRL’s
+pipeline syntax. The goal is twofold:
+
+[arabic]
+. *Accessibility:* Users familiar with SQL can write queries against
+QuandleDB without learning KRL’s pipeline syntax from scratch.
+. *Interoperability:* External tools (BI dashboards, ODBC/JDBC drivers)
+can issue SQL queries that are mechanically translated to KRL pipelines.
+
+KRL is _not_ a SQL dialect — it is a superset with fundamentally richer
+semantics (equivalence types, provenance, dependent types). The SQL
+compatibility layer covers the relational subset of KRL.
+
+'''''
+
+=== 2. Translation Rules
+
+==== 2.1 SELECT … FROM … WHERE
+
+[source,sql]
+----
+-- SQL
+SELECT name, crossing_number, jones_polynomial
+FROM knots
+WHERE crossing_number <= 10
+  AND genus = 1
+ORDER BY crossing_number ASC
+LIMIT 20;
+----
+
+[source,krl]
+----
+-- KRL translation
+from knots
+| filter crossing_number <= 10
+| filter genus == 1
+| sort crossing_number asc
+| take 20
+| return name, crossing_number, jones_polynomial
+----
+
+*Translation rules:* - `+SELECT fields+` → `+| return fields+` -
+`+FROM source+` → `+from source+` - `+WHERE pred+` → `+| filter pred+` -
+`+AND+` chains → multiple `+| filter+` stages (short-circuit semantics
+preserved) - `+ORDER BY expr [ASC|DESC]+` → `+| sort expr [asc|desc]+` -
+`+LIMIT n+` → `+| take n+` - `+OFFSET n+` → `+| skip n+` - `+SELECT *+`
+→ `+| return *+`
+
+==== 2.2 Aggregation
+
+[source,sql]
+----
+-- SQL
+SELECT crossing_number, COUNT(*) AS cnt
+FROM knots
+GROUP BY crossing_number
+HAVING cnt > 5;
+----
+
+[source,krl]
+----
+-- KRL
+from knots
+| group_by crossing_number
+| aggregate count(*) as cnt
+| filter cnt > 5
+| return crossing_number, cnt
+----
+
+*Rules:* - `+GROUP BY expr+` → `+| group_by expr+` -
+`+COUNT/MIN/MAX/AVG/SUM(expr)+` → `+| aggregate fn(expr)+` -
+`+HAVING pred+` → `+| filter pred+` (after aggregate)
+
+==== 2.3 Subqueries
+
+[source,sql]
+----
+-- SQL
+SELECT * FROM knots
+WHERE crossing_number IN (
+    SELECT crossing_number FROM knots WHERE genus = 1
+);
+----
+
+[source,krl]
+----
+-- KRL
+let genus_1_crossings = from knots
+  | filter genus == 1
+  | return crossing_number
+
+from knots
+| filter crossing_number in genus_1_crossings
+----
+
+*Rules:* - `+IN (SELECT …)+` → `+let+` binding + `+in+` predicate -
+Correlated subqueries → `+let+` with captured variables
+
+==== 2.4 Joins
+
+KRL does not have explicit JOIN syntax — knot relationships are modelled
+as equivalence queries and graph patterns instead. For SQL
+compatibility:
+
+[source,sql]
+----
+-- SQL join (relating knots by shared invariants)
+SELECT K1.name, K2.name
+FROM knots K1, knots K2
+WHERE K1.jones_polynomial = K2.jones_polynomial
+  AND K1.name != K2.name;
+----
+
+[source,krl]
+----
+-- KRL (natural expression of the same query)
+from knots
+| find_equivalent via [jones]
+| return source.name, target.name
+----
+
+*Rules:* - Self-joins on invariant equality →
+`+find_equivalent via [invariant]+` - Cross-joins → not directly
+supported (use `+match+` patterns for relationships) - Foreign-key joins
+→ `+match (A)-[:REL]->(B)+` graph pattern
+
+==== 2.5 SQL Functions → KRL Equivalents
+
+[cols=",,",options="header",]
+|===
+|SQL |KRL |Notes
+|`+COUNT(*)+` |`+count(*)+` |Identical
+|`+MIN(expr)+` |`+min(expr)+` |Identical
+|`+MAX(expr)+` |`+max(expr)+` |Identical
+|`+AVG(expr)+` |`+avg(expr)+` |Identical
+|`+SUM(expr)+` |`+sum(expr)+` |Identical
+|`+COALESCE(a, b)+` |`+a ?? b+` |Option unwrap with default
+|`+CASE WHEN … THEN … END+` |`+match+` expression |Pattern matching
+|`+IS NULL+` |`+== none+` |Option check
+|`+IS NOT NULL+` |`+!= none+` |Option check
+|`+LIKE '%pat%'+` |`+contains(field, "pat")+` |String matching
+|`+CAST(x AS T)+` |`+x : T+` |Type annotation
+|`+DISTINCT+` |`+unique+` |Deduplication
+|===
+
+'''''
+
+=== 3. SQL Features NOT Supported
+
+These SQL features have no KRL equivalent because they conflict with
+KRL’s type-safe, provenance-carrying semantics:
+
+[width="99%",cols="30%,34%,36%",options="header",]
+|===
+|SQL Feature |Why Not in KRL |KRL Alternative
+|`+NULL+` (three-valued logic) |KRL uses `+Option[τ]+` — explicit
+absence |`+Option[τ]+` with `+none+`
+
+|`+UNION ALL+` |Untyped bag union loses provenance |`+merge+` with
+provenance tracking
+
+|`+INSERT/UPDATE/DELETE+` |QuandleDB is read-only (invariants are
+computed) |Skein.jl REPL
+
+|`+CREATE TABLE+` |Schema is fixed (knots + invariants) |—
+
+|`+ALTER TABLE+` |Schema is fixed |—
+
+|`+GRANT/REVOKE+` |No access control model yet |—
+
+|Implicit type coercion |KRL is strongly typed |Explicit `+x : T+`
+|===
+
+'''''
+
+=== 4. Extensions Beyond SQL
+
+KRL provides capabilities that have NO SQL equivalent:
+
+==== 4.1 Equivalence Queries (unique to KRL)
+
+[source,krl]
+----
+from knots
+| find_equivalent "3_1" via [jones, genus]
+| return equivalences with provenance
+----
+
+Returns structured `+Equivalence[Knot]+` records with proof derivations
+and invariant provenance. SQL can only return boolean equality.
+
+==== 4.2 Path Queries (unique to KRL)
+
+[source,krl]
+----
+from diagrams as D
+| find_path D ~> "3_1" via reidemeister
+| return path, move_count
+----
+
+Finds explicit Reidemeister move sequences between diagram
+representations.
+
+==== 4.3 Dependent Type Annotations (unique to KRL)
+
+[source,krl]
+----
+-- Query result type depends on which invariants are requested
+from knots
+| filter crossing_number <= 10
+| return name, crossing_number
+  -- Result type: ResultSet[{name: String, crossing_number: Int}]
+  -- The return clause DETERMINES the record type (dependent projection)
+----
+
+==== 4.4 Provenance Tracking (unique to KRL)
+
+Every query result can carry provenance metadata showing which
+invariants were computed and at what confidence level.
+
+'''''
+
+=== 5. Implementation Strategy
+
+The SQL compatibility layer is implemented as a *syntactic frontend*
+that parses SQL and emits a KRL AST. The KRL type checker and evaluator
+then process the AST normally.
+
+....
+SQL input → SQL parser → KRL AST → Type checker → Evaluator → Result
+                                         ↑
+KRL input → KRL parser ─────────────────┘
+....
+
+The SQL parser is a *subset parser* — it accepts only the SQL features
+that have KRL translations (§2). Unsupported features produce a clear
+error message pointing the user to the KRL syntax for the equivalent
+operation.
+
+==== 5.1 Type Safety
+
+SQL queries are translated to *typed* KRL AST nodes. The type checker
+runs on the KRL AST regardless of whether the query was written in SQL
+or KRL. This means SQL queries get the same type-safety guarantees as
+native KRL queries — including pipeline type preservation (§4 of
+type-system.md).
+
+==== 5.2 Provenance
+
+SQL queries automatically get provenance tracking. Even `+SELECT *+`
+queries carry an implicit provenance annotation recording which columns
+were accessed and from which invariant computations.
diff --git a/spec/sql-compat.md b/spec/sql-compat.md
deleted file mode 100644
index 0d1ae20..0000000
--- a/spec/sql-compat.md
+++ /dev/null
@@ -1,242 +0,0 @@
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-
-# KRL–SQL Compatibility Layer
-
-**Version:** 0.1.0
-**Date:** 2026-03-20
-
----
-
-## 1. Purpose
-
-This document defines how standard SQL (ISO 9075) concepts map to KRL's
-pipeline syntax. The goal is twofold:
-
-1. **Accessibility:** Users familiar with SQL can write queries against
-   QuandleDB without learning KRL's pipeline syntax from scratch.
-2. **Interoperability:** External tools (BI dashboards, ODBC/JDBC drivers)
-   can issue SQL queries that are mechanically translated to KRL pipelines.
-
-KRL is *not* a SQL dialect — it is a superset with fundamentally richer
-semantics (equivalence types, provenance, dependent types). The SQL
-compatibility layer covers the relational subset of KRL.
-
----
-
-## 2. Translation Rules
-
-### 2.1 SELECT … FROM … WHERE
-
-```sql
--- SQL
-SELECT name, crossing_number, jones_polynomial
-FROM knots
-WHERE crossing_number <= 10
-  AND genus = 1
-ORDER BY crossing_number ASC
-LIMIT 20;
-```
-
-```krl
--- KRL translation
-from knots
-| filter crossing_number <= 10
-| filter genus == 1
-| sort crossing_number asc
-| take 20
-| return name, crossing_number, jones_polynomial
-```
-
-**Translation rules:**
-- `SELECT fields` → `| return fields`
-- `FROM source` → `from source`
-- `WHERE pred` → `| filter pred`
-- `AND` chains → multiple `| filter` stages (short-circuit semantics preserved)
-- `ORDER BY expr [ASC|DESC]` → `| sort expr [asc|desc]`
-- `LIMIT n` → `| take n`
-- `OFFSET n` → `| skip n`
-- `SELECT *` → `| return *`
-
-### 2.2 Aggregation
-
-```sql
--- SQL
-SELECT crossing_number, COUNT(*) AS cnt
-FROM knots
-GROUP BY crossing_number
-HAVING cnt > 5;
-```
-
-```krl
--- KRL
-from knots
-| group_by crossing_number
-| aggregate count(*) as cnt
-| filter cnt > 5
-| return crossing_number, cnt
-```
-
-**Rules:**
-- `GROUP BY expr` → `| group_by expr`
-- `COUNT/MIN/MAX/AVG/SUM(expr)` → `| aggregate fn(expr)`
-- `HAVING pred` → `| filter pred` (after aggregate)
-
-### 2.3 Subqueries
-
-```sql
--- SQL
-SELECT * FROM knots
-WHERE crossing_number IN (
-    SELECT crossing_number FROM knots WHERE genus = 1
-);
-```
-
-```krl
--- KRL
-let genus_1_crossings = from knots
-  | filter genus == 1
-  | return crossing_number
-
-from knots
-| filter crossing_number in genus_1_crossings
-```
-
-**Rules:**
-- `IN (SELECT …)` → `let` binding + `in` predicate
-- Correlated subqueries → `let` with captured variables
-
-### 2.4 Joins
-
-KRL does not have explicit JOIN syntax — knot relationships are modelled
-as equivalence queries and graph patterns instead. For SQL compatibility:
-
-```sql
--- SQL join (relating knots by shared invariants)
-SELECT K1.name, K2.name
-FROM knots K1, knots K2
-WHERE K1.jones_polynomial = K2.jones_polynomial
-  AND K1.name != K2.name;
-```
-
-```krl
--- KRL (natural expression of the same query)
-from knots
-| find_equivalent via [jones]
-| return source.name, target.name
-```
-
-**Rules:**
-- Self-joins on invariant equality → `find_equivalent via [invariant]`
-- Cross-joins → not directly supported (use `match` patterns for relationships)
-- Foreign-key joins → `match (A)-[:REL]->(B)` graph pattern
-
-### 2.5 SQL Functions → KRL Equivalents
-
-| SQL | KRL | Notes |
-|-----|-----|-------|
-| `COUNT(*)` | `count(*)` | Identical |
-| `MIN(expr)` | `min(expr)` | Identical |
-| `MAX(expr)` | `max(expr)` | Identical |
-| `AVG(expr)` | `avg(expr)` | Identical |
-| `SUM(expr)` | `sum(expr)` | Identical |
-| `COALESCE(a, b)` | `a ?? b` | Option unwrap with default |
-| `CASE WHEN … THEN … END` | `match` expression | Pattern matching |
-| `IS NULL` | `== none` | Option check |
-| `IS NOT NULL` | `!= none` | Option check |
-| `LIKE '%pat%'` | `contains(field, "pat")` | String matching |
-| `CAST(x AS T)` | `x : T` | Type annotation |
-| `DISTINCT` | `unique` | Deduplication |
-
----
-
-## 3. SQL Features NOT Supported
-
-These SQL features have no KRL equivalent because they conflict with
-KRL's type-safe, provenance-carrying semantics:
-
-| SQL Feature | Why Not in KRL | KRL Alternative |
-|-------------|----------------|-----------------|
-| `NULL` (three-valued logic) | KRL uses `Option[τ]` — explicit absence | `Option[τ]` with `none` |
-| `UNION ALL` | Untyped bag union loses provenance | `merge` with provenance tracking |
-| `INSERT/UPDATE/DELETE` | QuandleDB is read-only (invariants are computed) | Skein.jl REPL |
-| `CREATE TABLE` | Schema is fixed (knots + invariants) | — |
-| `ALTER TABLE` | Schema is fixed | — |
-| `GRANT/REVOKE` | No access control model yet | — |
-| Implicit type coercion | KRL is strongly typed | Explicit `x : T` |
-
----
-
-## 4. Extensions Beyond SQL
-
-KRL provides capabilities that have NO SQL equivalent:
-
-### 4.1 Equivalence Queries (unique to KRL)
-
-```krl
-from knots
-| find_equivalent "3_1" via [jones, genus]
-| return equivalences with provenance
-```
-
-Returns structured `Equivalence[Knot]` records with proof derivations
-and invariant provenance. SQL can only return boolean equality.
-
-### 4.2 Path Queries (unique to KRL)
-
-```krl
-from diagrams as D
-| find_path D ~> "3_1" via reidemeister
-| return path, move_count
-```
-
-Finds explicit Reidemeister move sequences between diagram representations.
-
-### 4.3 Dependent Type Annotations (unique to KRL)
-
-```krl
--- Query result type depends on which invariants are requested
-from knots
-| filter crossing_number <= 10
-| return name, crossing_number
-  -- Result type: ResultSet[{name: String, crossing_number: Int}]
-  -- The return clause DETERMINES the record type (dependent projection)
-```
-
-### 4.4 Provenance Tracking (unique to KRL)
-
-Every query result can carry provenance metadata showing which
-invariants were computed and at what confidence level.
-
----
-
-## 5. Implementation Strategy
-
-The SQL compatibility layer is implemented as a **syntactic frontend**
-that parses SQL and emits a KRL AST. The KRL type checker and
-evaluator then process the AST normally.
-
-```
-SQL input → SQL parser → KRL AST → Type checker → Evaluator → Result
-                                         ↑
-KRL input → KRL parser ─────────────────┘
-```
-
-The SQL parser is a **subset parser** — it accepts only the SQL features
-that have KRL translations (§2). Unsupported features produce a clear
-error message pointing the user to the KRL syntax for the equivalent
-operation.
-
-### 5.1 Type Safety
-
-SQL queries are translated to **typed** KRL AST nodes. The type checker
-runs on the KRL AST regardless of whether the query was written in SQL
-or KRL. This means SQL queries get the same type-safety guarantees as
-native KRL queries — including pipeline type preservation (§4 of
-type-system.md).
-
-### 5.2 Provenance
-
-SQL queries automatically get provenance tracking. Even `SELECT *` queries
-carry an implicit provenance annotation recording which columns were
-accessed and from which invariant computations.
diff --git a/spec/system-specs.adoc b/spec/system-specs.adoc
new file mode 100644
index 0000000..daa3d53
--- /dev/null
+++ b/spec/system-specs.adoc
@@ -0,0 +1,116 @@
+== SPDX-License-Identifier: CC-BY-SA-4.0
+
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
+
+== QuandleDB/KRL System Specification
+
+=== Overview
+
+QuandleDB is a knot-theoretic database for storing, querying, and
+classifying knots via algebraic invariants. The stack comprises Julia
+(server and engine via Skein.jl) and ReScript (frontend). Knot
+Resolution Language (KRL) provides the query interface.
+
+=== Memory Model
+
+==== Julia Runtime
+
+All knot records, quandle structures, and invariant results are managed
+by Julia’s generational garbage collector. Knot records are immutable
+structs (`+struct KnotRecord ... end+`). Short-lived intermediates
+benefit from young-generation collection. Long-lived catalog data is
+pinned in a global `+KnotCatalog+` dictionary that survives GC cycles.
+
+==== E-Graph Representation
+
+Equivalence classes of knots under Reidemeister moves are stored as an
+in-memory e-graph (equality saturation). Each e-class contains a set of
+equivalent knot representations. The e-graph grows monotonically: new
+equivalences are discovered but never retracted. Backed by a union-find
+with path compression, stored as a flat `+Vector{Int}+` for cache
+locality.
+
+==== Memory Budget
+
+The e-graph enforces a configurable node limit (default: 10M e-nodes).
+When reached, saturation halts and returns best-known equivalence
+classes. Adjustable per query via `+SATURATE ... LIMIT n+` KRL clause.
+
+==== ReScript Frontend
+
+The frontend maintains a local LRU cache (default: 500 entries) of
+recently queried knot records as ReScript immutable records. No knot
+computation occurs on the frontend; it is purely a presentation and
+query-composition layer.
+
+=== Concurrency Model
+
+==== Julia Task Parallelism
+
+KRL evaluation proceeds in strata: stratum 0 computes base invariants
+(crossing number, writhe), stratum 1 computes polynomial invariants
+(Jones, HOMFLY-PT via Skein.jl), stratum 2 computes homological
+invariants (Khovanov homology). Strata evaluate sequentially, but within
+each stratum independent knot records are processed in parallel via
+`+Threads.@spawn+`.
+
+==== Query Isolation
+
+Each KRL query runs in its own Julia `+Task+` with a private e-graph
+instance. Queries share read access to the global `+KnotCatalog+`.
+Catalog mutations are serialized through a `+ReentrantLock+`-protected
+append operation, eliminating write contention.
+
+==== Frontend Concurrency
+
+The ReScript frontend uses async/await for non-blocking server
+communication. Stale cache entries are invalidated by a version counter
+returned with each response.
+
+=== Effect System
+
+==== Provenance Effect
+
+Every equivalence result carries derivation evidence: the sequence of
+Reidemeister moves or skein relations that established it. Evidence is
+stored as proof steps attached to each e-class merge. Queryable via
+`+EXPLAIN EQUIVALENCE k1 k2+`. Provenance is append-only.
+
+==== Computation Cost Effect
+
+Each computed invariant carries a cost annotation (wall-clock
+microseconds and allocation bytes). Exposed via `+EXPLAIN COST+` KRL
+clause. Queries exceeding a cost budget (configurable via `+BUDGET+`
+clause) are terminated early with a partial result and cost report.
+
+==== Effect Composition
+
+Provenance and cost compose: the cost of producing a provenance chain is
+itself tracked. Expensive derivations are flagged in the cost report.
+
+=== Module System
+
+==== Julia Modules
+
+Organized as `+QuandleDB.jl+` with submodules: `+Catalog+` (storage),
+`+Engine+` (evaluation), `+EGraph+` (equality saturation),
+`+Invariants+` (computations), `+Server+` (HTTP/WebSocket). `+Skein.jl+`
+is declared as a dependency in `+Project.toml+`.
+
+==== ReScript Modules
+
+One module per concern: `+KnotViewer.res+`, `+QueryEditor.res+`,
+`+ServerClient.res+`, `+Cache.res+`, `+KnotTypes.res+`. Interface files
+(`+.resi+`) define public APIs.
+
+==== KRL Query Modules
+
+User-defined modules via `+MODULE name { ... }+` blocks encapsulate
+named queries and invariant definitions, imported with `+USE+`. Module
+resolution is flat. Modules are stored server-side in the catalog.
+
+==== Cross-Language Boundary
+
+Julia and ReScript communicate via JSON over HTTP or WebSocket. The wire
+format is defined by `+schema/krl-wire.json+`. ReScript types are
+generated from this schema for cross-boundary type safety.
diff --git a/spec/system-specs.md b/spec/system-specs.md
deleted file mode 100644
index c76e943..0000000
--- a/spec/system-specs.md
+++ /dev/null
@@ -1,114 +0,0 @@
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
-
-# QuandleDB/KRL System Specification
-
-## Overview
-
-QuandleDB is a knot-theoretic database for storing, querying, and
-classifying knots via algebraic invariants. The stack comprises Julia
-(server and engine via Skein.jl) and ReScript (frontend). Knot Resolution
-Language (KRL) provides the query interface.
-
-## Memory Model
-
-### Julia Runtime
-
-All knot records, quandle structures, and invariant results are managed
-by Julia's generational garbage collector. Knot records are immutable
-structs (`struct KnotRecord ... end`). Short-lived intermediates benefit
-from young-generation collection. Long-lived catalog data is pinned in
-a global `KnotCatalog` dictionary that survives GC cycles.
-
-### E-Graph Representation
-
-Equivalence classes of knots under Reidemeister moves are stored as an
-in-memory e-graph (equality saturation). Each e-class contains a set of
-equivalent knot representations. The e-graph grows monotonically: new
-equivalences are discovered but never retracted. Backed by a union-find
-with path compression, stored as a flat `Vector{Int}` for cache locality.
-
-### Memory Budget
-
-The e-graph enforces a configurable node limit (default: 10M e-nodes).
-When reached, saturation halts and returns best-known equivalence
-classes. Adjustable per query via `SATURATE ... LIMIT n` KRL clause.
-
-### ReScript Frontend
-
-The frontend maintains a local LRU cache (default: 500 entries) of
-recently queried knot records as ReScript immutable records. No knot
-computation occurs on the frontend; it is purely a presentation and
-query-composition layer.
-
-## Concurrency Model
-
-### Julia Task Parallelism
-
-KRL evaluation proceeds in strata: stratum 0 computes base invariants
-(crossing number, writhe), stratum 1 computes polynomial invariants
-(Jones, HOMFLY-PT via Skein.jl), stratum 2 computes homological
-invariants (Khovanov homology). Strata evaluate sequentially, but
-within each stratum independent knot records are processed in parallel
-via `Threads.@spawn`.
-
-### Query Isolation
-
-Each KRL query runs in its own Julia `Task` with a private e-graph
-instance. Queries share read access to the global `KnotCatalog`.
-Catalog mutations are serialized through a `ReentrantLock`-protected
-append operation, eliminating write contention.
-
-### Frontend Concurrency
-
-The ReScript frontend uses async/await for non-blocking server
-communication. Stale cache entries are invalidated by a version counter
-returned with each response.
-
-## Effect System
-
-### Provenance Effect
-
-Every equivalence result carries derivation evidence: the sequence of
-Reidemeister moves or skein relations that established it. Evidence is
-stored as proof steps attached to each e-class merge. Queryable via
-`EXPLAIN EQUIVALENCE k1 k2`. Provenance is append-only.
-
-### Computation Cost Effect
-
-Each computed invariant carries a cost annotation (wall-clock
-microseconds and allocation bytes). Exposed via `EXPLAIN COST` KRL
-clause. Queries exceeding a cost budget (configurable via `BUDGET`
-clause) are terminated early with a partial result and cost report.
-
-### Effect Composition
-
-Provenance and cost compose: the cost of producing a provenance chain
-is itself tracked. Expensive derivations are flagged in the cost report.
-
-## Module System
-
-### Julia Modules
-
-Organized as `QuandleDB.jl` with submodules: `Catalog` (storage),
-`Engine` (evaluation), `EGraph` (equality saturation), `Invariants`
-(computations), `Server` (HTTP/WebSocket). `Skein.jl` is declared as
-a dependency in `Project.toml`.
-
-### ReScript Modules
-
-One module per concern: `KnotViewer.res`, `QueryEditor.res`,
-`ServerClient.res`, `Cache.res`, `KnotTypes.res`. Interface files
-(`.resi`) define public APIs.
-
-### KRL Query Modules
-
-User-defined modules via `MODULE name { ... }` blocks encapsulate
-named queries and invariant definitions, imported with `USE`. Module
-resolution is flat. Modules are stored server-side in the catalog.
-
-### Cross-Language Boundary
-
-Julia and ReScript communicate via JSON over HTTP or WebSocket. The
-wire format is defined by `schema/krl-wire.json`. ReScript types are
-generated from this schema for cross-boundary type safety.
diff --git a/spec/type-system.md b/spec/type-system.adoc
similarity index 82%
rename from spec/type-system.md
rename to spec/type-system.adoc
index 8c833ff..50c5569 100644
--- a/spec/type-system.md
+++ b/spec/type-system.adoc
@@ -1,16 +1,16 @@
-# SPDX-License-Identifier: CC-BY-SA-4.0
-# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+== SPDX-License-Identifier: CC-BY-SA-4.0
 
-# KRL Type System Specification
+== Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) j.d.a.jewell@open.ac.uk
 
-**Version:** 0.1.0
-**Date:** 2026-03-14
+== KRL Type System Specification
 
----
+*Version:* 0.1.0 *Date:* 2026-03-14
 
-## 1. Type Language
+'''''
 
-```
+=== 1. Type Language
+
+....
 τ ::= Int | Float | String | Bool                   scalars
     | Knot                                          knot record
     | Diagram                                       knot diagram
@@ -27,15 +27,15 @@
     | Provenance                                    provenance annotation
     | ResultSet[τ]                                  query result (ordered set of records)
     | α                                             type variable
-```
+....
 
----
+'''''
 
-## 2. Knot Record Type
+=== 2. Knot Record Type
 
-The `Knot` type is a fixed record:
+The `+Knot+` type is a fixed record:
 
-```
+....
 Knot = {
   name             : String,
   gauss_code       : GaussCode,
@@ -46,21 +46,21 @@ Knot = {
   jones_polynomial : Option[Polynomial],
   metadata         : Map[String, String]
 }
-```
+....
 
-Fields with `Option[τ]` may not be computed for all knots.
+Fields with `+Option[τ]+` may not be computed for all knots.
 
----
+'''''
 
-## 3. Equivalence Types (HoTT-Inspired)
+=== 3. Equivalence Types (HoTT-Inspired)
 
-### 3.1 Identity Type
+==== 3.1 Identity Type
 
-KRL's distinguishing feature is that equivalence queries return *types*, not
-booleans. The identity type `Equivalence[τ]` represents the space of paths
-between two values of type `τ`:
+KRL’s distinguishing feature is that equivalence queries return _types_,
+not booleans. The identity type `+Equivalence[τ]+` represents the space
+of paths between two values of type `+τ+`:
 
-```
+....
 Equivalence[Knot] = {
   source    : Knot,
   target    : Knot,
@@ -75,11 +75,11 @@ EquivalencePath = {
 }
 
 Confidence = Exact | Necessary | Sufficient | Heuristic
-```
+....
 
-### 3.2 Typing Rules for Equivalence
+==== 3.2 Typing Rules for Equivalence
 
-```
+....
     Γ ⊢ e₁ : Knot     Γ ⊢ e₂ : Knot
     ───────────────────────────────────────────────  [T-Equiv-Query]
     Γ ⊢ find_equivalent e₁ via [invs] : ResultSet[Equivalence[Knot]]
@@ -87,15 +87,15 @@ Confidence = Exact | Necessary | Sufficient | Heuristic
     Γ ⊢ e₁ : Diagram     Γ ⊢ e₂ : Diagram
     ──────────────────────────────────────────────────────  [T-Path-Query]
     Γ ⊢ find_path e₁ ~> e₂ via reidemeister : ResultSet[{path: List[Move], move_count: Int}]
-```
+....
 
----
+'''''
 
-## 4. Pipeline Type System
+=== 4. Pipeline Type System
 
 Each pipeline stage transforms the type of the result set:
 
-```
+....
     Γ ⊢ from knots : ResultSet[Knot]
 
     Γ ⊢ R : ResultSet[τ]     Γ, x: τ ⊢ expr : Bool
@@ -127,13 +127,13 @@ Each pipeline stage transforms the type of the result set:
     Γ, x: τ ⊢ agg(expr) : τ_agg
     ──────────────────────────────────────────────────────  [T-GroupAgg]
     Γ ⊢ R | group_by key | aggregate agg(expr) : ResultSet[{key: κ, agg: τ_agg}]
-```
+....
 
----
+'''''
 
-## 5. Expression Types
+=== 5. Expression Types
 
-```
+....
     ──────────────────  [T-IntLit]       ──────────────────  [T-FloatLit]
     Γ ⊢ n : Int                         Γ ⊢ f : Float
 
@@ -171,45 +171,49 @@ Each pipeline stage transforms the type of the result set:
     ∀i. Γ ⊢ eᵢ : Int
     ────────────────────────────────────────  [T-Gauss]
     Γ ⊢ gauss(e₁, …, eₙ) : GaussCode
-```
+....
 
----
+'''''
 
-## 6. Rule Types
+=== 6. Rule Types
 
-```
+....
     ∀param ∈ params: param : Knot
     ∀clause ∈ body: well-typed predicate or guard
     ────────────────────────────────────────────  [T-Rule]
     Γ ⊢ rule name(params) :- body : Rule
-```
+....
 
 Rules extend the e-graph. Type checking ensures all predicate arguments
-are of the correct type (e.g., `jones_polynomial(K, J)` requires `K: Knot`
-and `J: Polynomial`).
+are of the correct type (e.g., `+jones_polynomial(K, J)+` requires
+`+K: Knot+` and `+J: Polynomial+`).
 
----
+'''''
 
-## 7. Axiom Types
+=== 7. Axiom Types
 
-```
+....
     Γ, params ⊢ premise : Bool     Γ, params ⊢ conclusion : Bool
     ──────────────────────────────────────────────────────────────  [T-Axiom]
     Γ ⊢ axiom name : forall params, premise -> conclusion
-```
+....
 
 Axioms are trusted declarations used by the equivalence engine. They are
-not verified by the type checker but are type-checked for well-formedness.
-
----
-
-## 8. Properties
-
-1. **Pipeline type preservation:** Each stage produces a well-typed ResultSet.
-2. **Field access safety:** Projecting fields not in the record is a type error.
-3. **Equivalence type richness:** Equivalence results carry structured evidence,
-   not just boolean matches.
-4. **Provenance compositionality:** Combining results preserves provenance
-   (semiring structure).
-5. **Invariant type safety:** Each invariant function has a declared return type;
-   comparisons are type-checked.
+not verified by the type checker but are type-checked for
+well-formedness.
+
+'''''
+
+=== 8. Properties
+
+[arabic]
+. *Pipeline type preservation:* Each stage produces a well-typed
+ResultSet.
+. *Field access safety:* Projecting fields not in the record is a type
+error.
+. *Equivalence type richness:* Equivalence results carry structured
+evidence, not just boolean matches.
+. *Provenance compositionality:* Combining results preserves provenance
+(semiring structure).
+. *Invariant type safety:* Each invariant function has a declared return
+type; comparisons are type-checked.