sweep reconcile: licence canonicalisation, test-suite repair, full Julia+TLC CI gating (#72)

## Summary

Sitrep-driven remediation. Local `main` had drifted 4 ahead / 2 behind
origin with three unpushed, unreviewed AI-generated "sweep" commits; the
mathematical core of the test suite ran in no CI; and actually running
that suite surfaced two genuine upstream bugs plus three test-harness
defects.

### 1. Sweep reconciliation (minus the AGPL landmine)

Only the licence-text canonicalisation survives review (MPL-2.0 `https`
Exhibit A + canonical CC-BY-SA-4.0 plaintext). Deliberately dropped:
- `LICENSES/AGPL-3.0-or-later.txt` — no file here declares AGPL and
`.machine_readable/6a2/AGENTIC.a2ml` forbids it ("Never use AGPL license
(use MPL-2.0)").
- `mise.toml` / `CODEOWNERS` / `funding.yml` / `MAINTAINERS` /
`GOVERNANCE.md` / `ARCHITECTURE.md` — generic boilerplate crediting
`@metadatastician` (this repo is `hyperpolymath`) and describing a
directory layout this repo does not have.

### 2. Test-harness fixes (they were hiding real results)

- `test_quandle_axioms.jl`: `@testset label begin` with a bare variable
×9 — Julia hard-errors, so **§3 onward (including both Reidemeister
suites) never executed**.
- `seam_test.jl`: `KRLLexError` never imported — errored Seam 1, masking
the rest.
- `Evaluator.jl`: the `max_rows` cap was pushed down as an exact
provider limit, making truncation silent and — for stage-free queries —
not applied at all. Now fetches one row past the cap and enforces it
after source resolution, so the "row cap applied" warning fires whenever
data was actually dropped.

### 3. Two genuine upstream KnotTheory.jl defects, tracked honestly

Both marked `@test_broken` (reports "Broken"; **flips to a hard error
the moment the upstream fix lands**, forcing marker removal):

- `r2_simplify` removes a bigon without re-splicing the severed arcs (4
arc labels occur once instead of twice) → trefoil 5-colouring count 25
instead of 5. Repro:
`r2_simplify(from_braid_word("s1.S1.s1.s1.s1").pd)`.
- The alexander/conway/homfly segments of `quandle_key` are
crossing-order sensitive (no canonical ±t^k unit normalisation): 25/200
seeded BR-5 trials disagree after a crossing shuffle, while
`presentation_hash` and colouring counts agree.

### 4. CI: the mathematical core is now gated

`krl-verification.yml`:
- `seam_test.jl` joins the dependency-free fast step (pure Julia +
stdlib).
- Sibling `KnotTheory.jl` / `Skein.jl` / `AcceleratorGate.jl` are
checked out under `deps/` and symlinked to the `server/../../../` layout
`server/Project.toml [sources]` expects; `Pkg.instantiate`; then axioms
/ EXPLAIN / BR-5 fuzz as separately-named steps.
- New `tlaplus-model-check` job: TLC (pinned v1.7.4, sha256-verified)
checks `TypeOK` / `IsEquivalence` / `SoundBelow` / `Confluent` on
`MCEGraph`. `-deadlock` disables deadlock *reporting* only (the merge
sequence terminates by design).
- Fixed the stale header claim that this repo has no `mix.exs`.

## Verification

- All seven Julia suites run locally (Julia 1.12.6, sibling checkouts):
lexer / parser / sql / seam / query_explain fully green; axioms + fuzz
green with exactly the two documented Broken marks.
- TLC: 8 distinct states, all four invariants, exit 0 in 2s.
- **Negative-tested both new gate types**: a real test failure exits 1
(observed twice during diagnosis); an injected false TLA+ invariant
exits 12.
- The six `startup_failure` workflows (Secret Scanner, Governance,
Mirror, Instant Sync, Push email, Pages) are pre-existing shared
`hyperpolymath/standards` reusable rot — out of scope here.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Mistral Vibe <vibe@mistral.ai>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Author: 3 people

.github/workflows/krl-verification.yml

@@ -1,15 +1,18 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
-# KRL Verification — runs the self-contained KRL lexer/parser/SQL test suite
-# (pure Julia: the `KRL` module pulls in no external packages, so it loads on
-# base Julia with no Pkg.instantiate) AND machine-checks the Agda proofs under
-# verification/proofs/agda.
+# KRL Verification — runs the KRL lexer/parser/SQL/seam test suites (pure
+# Julia: the `KRL` module pulls in no external packages, so those load on base
+# Julia with no Pkg.instantiate), the full server test suites (quandle axioms /
+# EXPLAIN / BR-5 fuzz — these need the sibling KnotTheory.jl / Skein.jl /
+# AcceleratorGate.jl checkouts that server/Project.toml [sources] points at),
+# machine-checks the Agda proofs under verification/proofs/agda, AND
+# model-checks the TLA+ specs under verification/proofs/tlaplus with TLC.
 #
-# Why this exists: `.gitlab-ci.yml` only defines jobs gated on `Cargo.toml` /
-# `mix.exs`, neither of which this (Julia + ReScript) repo has — so the Julia
-# test suite was never executed by any CI gate. This workflow closes that gap
-# so lexer/parser regressions are caught in future.
+# Why this exists: `.gitlab-ci.yml` only defines jobs gated on root-level
+# `Cargo.toml` / `mix.exs` (this repo has only `beam/mix.exs`, which those
+# `exists:` rules never match) — so the Julia test suite was never executed by
+# any CI gate. This workflow closes that gap so regressions are caught.
 
 name: KRL Verification
 
@@ -45,14 +48,63 @@ jobs:
       - name: Julia version
         run: julia --version
 
-      - name: Run KRL test suite
+      - name: Run KRL test suite (no package deps)
         run: |
           set -e
           # Each test file includes ../KRL.jl (or ../Lexer.jl) relative to its
           # own location; a top-level @testset throws on failure → non-zero exit.
+          # These four are pure Julia + stdlib and run before instantiate so a
+          # dependency-resolution breakage cannot mask a lexer/parser regression.
           julia --color=yes server/krl/test/lexer_test.jl
           julia --color=yes server/krl/test/parser_test.jl
           julia --color=yes server/krl/test/sql_test.jl
+          julia --color=yes server/krl/test/seam_test.jl
+
+      # server/Project.toml [sources] resolves KnotTheory/Skein/AcceleratorGate
+      # at server/../../../<name>.jl — i.e. two directories above the repo
+      # checkout ($GITHUB_WORKSPACE/../../<name>.jl). actions/checkout cannot
+      # write outside the workspace, so check out under deps/ and symlink.
+      - name: Checkout KnotTheory.jl
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
+        with:
+          repository: hyperpolymath/KnotTheory.jl
+          path: deps/KnotTheory.jl
+
+      - name: Checkout Skein.jl
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
+        with:
+          repository: hyperpolymath/Skein.jl
+          path: deps/Skein.jl
+
+      - name: Checkout AcceleratorGate.jl
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
+        with:
+          repository: hyperpolymath/AcceleratorGate.jl
+          path: deps/AcceleratorGate.jl
+
+      - name: Link sibling packages where server/Project.toml expects them
+        run: |
+          set -euo pipefail
+          for p in KnotTheory.jl Skein.jl AcceleratorGate.jl; do
+            ln -sfn "$GITHUB_WORKSPACE/deps/$p" "$GITHUB_WORKSPACE/../../$p"
+          done
+
+      - name: Instantiate server project
+        run: julia --color=yes --project=server -e 'using Pkg; Pkg.instantiate()'
+
+      # Each server suite is its own step so a failure names itself in the UI.
+      # Two known-broken upstream KnotTheory.jl defects are tracked inside the
+      # suites with @test_broken (r2_simplify arc re-splicing; polynomial
+      # order-sensitivity in quandle_key) — @test_broken flips to a hard error
+      # the moment the upstream fix lands, forcing the marker's removal.
+      - name: Quandle axioms + Reidemeister invariance
+        run: julia --color=yes --project=server server/test_quandle_axioms.jl
+
+      - name: KRL EXPLAIN (DB-6)
+        run: julia --color=yes --project=server server/test_query_explain.jl
+
+      - name: BR-5 crossing-order fuzz
+        run: julia --color=yes --project=server server/test_br5_fuzz.jl
 
   agda-proofs:
     name: Agda proofs (--safe)
@@ -91,3 +143,32 @@ jobs:
           done
           if [ "$found" = "0" ]; then echo "No Agda proofs found"; exit 1; fi
           echo "PASS: all Agda proofs check under --safe"
+
+  tlaplus-model-check:
+    name: TLA+ model check (TLC)
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
+
+      # The ubuntu-latest image ships a Temurin JDK; TLC needs Java 11+.
+      - name: Fetch TLA+ tools (pinned release, checksum-verified)
+        run: |
+          set -euo pipefail
+          curl -fsSL -o tla2tools.jar \
+            https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
+          echo "936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88  tla2tools.jar" \
+            | sha256sum -c -
+
+      - name: Model-check MCEGraph (TypeOK / IsEquivalence / SoundBelow / Confluent)
+        run: |
+          set -euo pipefail
+          test -f verification/proofs/tlaplus/MCEGraph.tla || { echo "::error::MCEGraph.tla missing — nothing was model-checked"; exit 1; }
+          test -f verification/proofs/tlaplus/MCEGraph.cfg || { echo "::error::MCEGraph.cfg missing — nothing was model-checked"; exit 1; }
+          # -deadlock disables deadlock REPORTING only (the merge sequence
+          # legitimately terminates); every INVARIANT in the .cfg is still
+          # checked and any violation exits non-zero.
+          ( cd verification/proofs/tlaplus && \
+            java -XX:+UseParallelGC -cp "$GITHUB_WORKSPACE/tla2tools.jar" \
+              tlc2.TLC -deadlock -config MCEGraph.cfg MCEGraph.tla )
+          echo "PASS: TLC checked all invariants in MCEGraph.cfg"