feat(tg-8): virtual-knot dialect as a conservative extension of core (template)

TG-8 template. compiler/lib/dialect_vk.ml models the virtual-knot dialect (the
virtual braid monoid VBn, braids plus involutive virtual crossings v_i) as a
CONSERVATIVE EXTENSION of the core braid language: a vgen is a real crossing or
a virtual crossing; the real fragment embeds via `embed`, and every decision on
it is DELEGATED to Braid_equiv (TG-7). Conservativity therefore holds BY
CONSTRUCTION -- the dialect cannot change core typing/semantics.

compiler/test/tg8/tg8_conservativity.ml (2311 assertions) verifies: faithful
embedding (project . embed = id); the dialect decides core terms exactly as the
core procedure (decide_trivial (embed w) = Some (is_trivial w); equiv likewise);
permutation/writhe invariants agree on the real fragment; proper extension (a
virtual crossing is a genuinely-new non-real element, v_i v_i = e); and an
honest partial-decision frontier (irreducible mixed virtual content -> None,
never guessed).

Built as a SEPARATE module: no core-AST or Lean-oracle edits, avoiding the
Warning 8 exhaustiveness cascade and keeping the proof oracle safe. Honest
scope: this is the dialect's semantic core + conservativity bridge, not a
surface-syntax parser integration, and VBn equivalence is a sound partial
decider. Surface syntax, the other four dialects (replicate the template), and
a Lean conservativity proof are the next rungs (PROOF-NEEDS.md TG-8).

dune runtest green (existing 597 + tg3 1008 + tg5 189 + tg7 2220 + tg8 2311).
Docs: PROOF-NEEDS, CHANGELOG, STATE.a2ml.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -36,7 +36,7 @@ milestones = [
   "DONE (TG-9): LSP diagnostics ⊆ HasType failures — tangle-lsp delegates to `tanglec --check` (compiler/lib/check.ml); hand-rolled LSP-only diagnostics removed; subset by construction",
   "DONE (TG-3): OCaml typecheck.ml refines Lean HasType (translation validation) — closure proof + proofs/TG3Differential.lean (496 by-decide obligations generated from infer_expr) + compiler/test/tg3 (1008 --check assertions) + proofs/check-tg3-differential.sh wired into lean-proofs.yml; divergences D1 close / D2 bool-eq; proofs/TG3-REFINEMENT.md",
   "DONE (TG-5): compositional PD-lowering preserves structural invariants + verbatim echo residue — compiler/test/tg5/tg5_invariants.ml (189 assertions in dune runtest)",
-  "BLOCKED (TG-8): dialects are README-only — need one dialect implemented (AST+parser+HasType/Step+eval) before conservativity is even stateable",
+  "TEMPLATE-DONE (TG-8): virtual-knot conservative-extension template — compiler/lib/dialect_vk.ml (VBn = core + virtual layer delegating to Braid_equiv on the real fragment; conservativity by construction) + compiler/test/tg8 (2311 assertions). Remaining: surface syntax, other 4 dialects, Lean conservativity proof.",
   "RUNG-DONE (TG-7): out-of-band braid_equiv (Dehornoy handle reduction) in compiler/lib/braid_equiv.ml — decides braid-group equivalence WITHOUT changing == (compiler/test/tg7, 2220 assertions). Routing == through it stays an owner decision; Lean correctness research-grade.",
   "RUNG-DONE (TG-6): wasm differential — compiler/tangle-wasm/tests/differential.rs executes generated wasm via wasmi (dev-dep) and checks strand permutation == reference model (trefoil, non-commuting, braid-relation, 5-strand). Codegen-vs-semantics; not a cross-binary eval.ml diff; full bisimulation research-grade.",
 ]
@@ -47,12 +47,12 @@ issues = []
 [critical-next-actions]
 actions = [
   "TG-7 OWNER DECISION (rung done): out-of-band braid_equiv now exists (compiler/lib/braid_equiv.ml). Decide whether to route `==`/Step.eqBraids through it (semantics change to eval.ml + Lean + proofs) or keep them list-equality and use braid_equiv only as a tool.",
-  "TG-8 prerequisite: implement one dialect end-to-end (virtual-knot suggested) as the conservativity template; dialects are currently README-only.",
+  "TG-8 (template done): replicate the virtual-knot conservative-extension template to the other 4 dialects; add surface syntax; mechanise the Lean conservativity proof.",
   "TG-6 (rung done): optional next rungs = cross-binary differential vs eval.ml; Markov-helper coverage; Lean/WasmCert bisimulation (research-grade).",
   "TangleIR Julia: implement EchoClosed node in KRLAdapter.jl per contract (quandledb session)",
 ]
 
 [maintenance-status]
-last-run-utc = "2026-06-14T17:00:00Z"
+last-run-utc = "2026-06-14T18:00:00Z"
 last-result = "pass"               # unknown | pass | warn | fail
-notes = "dune build + dune test GREEN (tg3 1008 + tg5 189 + tg7 2220); cargo test tangle-wasm GREEN (10 unit + 2 differential via wasmi); lean Tangle.lean 0 errors; proofs/check-tg3-differential.sh GREEN (496); LANDED: TG-1/2/3/5/9/10 + TG-6 differential rung + TG-7 non-semantic rung; remaining: TG-8 blocked (dialects README-only), TG-7 semantics change owner-gated, full WASM bisimulation research-grade; echo-types f7a965f grade semiring experimental (firewalled)"
+notes = "dune build + dune test GREEN (tg3 1008 + tg5 189 + tg7 2220 + tg8 2311); cargo test tangle-wasm GREEN (10 unit + 2 differential via wasmi); lean Tangle.lean 0 errors; proofs/check-tg3-differential.sh GREEN (496); LANDED: TG-1/2/3/5/9/10 + TG-6 differential rung + TG-7 non-semantic rung + TG-8 conservativity template (virtual-knot); remaining owner-gated/research-grade: TG-7 semantics change, TG-8 surface+other-dialects+Lean, full WASM bisimulation; echo-types f7a965f grade semiring experimental (firewalled)"

CHANGELOG.md

@@ -13,6 +13,24 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### TG-8 (template): virtual-knot dialect as a conservative extension of core
+
+- **`compiler/lib/dialect_vk.ml`** models the virtual-knot dialect (the virtual
+  braid monoid VBₙ ⊃ Bₙ — braids plus involutive virtual crossings vᵢ) as a
+  *conservative extension* of the core braid language: a real crossing or a
+  virtual crossing, with the core (real) fragment embedding via `embed` and every
+  decision on it DELEGATED to `Braid_equiv` (TG-7). Conservativity therefore
+  holds by construction — the dialect cannot change core typing/semantics.
+- **`compiler/test/tg8/tg8_conservativity.ml`** (2311 assertions) verifies:
+  faithful embedding (`project ∘ embed = id`); the dialect decides core terms
+  exactly as the core procedure; permutation/writhe invariants agree on the real
+  fragment; proper extension (a virtual crossing is a genuinely-new non-real
+  element, `vᵢ vᵢ = ε`); and an honest partial-decision frontier (irreducible
+  mixed virtual content → `None`, never guessed).
+- Built as a separate module — no core-AST or Lean-oracle edits (avoids the
+  `Warning 8` exhaustiveness cascade). Surface-syntax integration, the other four
+  dialects, and a Lean conservativity proof are the next rungs (PROOF-NEEDS TG-8).
+
 ### TG-6 (differential rung): execute generated wasm and check it preserves semantics
 
 - **`compiler/tangle-wasm/tests/differential.rs`** adds `wasmi` (a pure-Rust wasm

PROOF-NEEDS.md

@@ -60,7 +60,7 @@ Cross-referenced to [PROOF-NARRATIVE.md §3](PROOF-NARRATIVE.md#3-remaining-obli
 | TG-5 | `compositional.ml` (418 LoC) rewriter preserves types | TP | OCaml property test | P2 | — | **LANDED** (`compiler/test/tg5/tg5_invariants.ml`, 189 assertions in `dune runtest`). compositional is below the Ty layer, so "preserves types" = preserves the PD-lowering structural invariants + echo residue-recovery: `OpenWord`/`ClosedDiagram`/`EchoClosed` each pinned (closedness, `\|crossings\|`=unit-length, source unit-expanded, **verbatim residue** for `EchoClose` with `expand(residue)=diagram word` and echo-diagram pdv1-identical to plain `close`), error paths, count pins. Lean IR model = optional later rung |
 | TG-6 | WASM compilation preserves semantics (source eval ≡ wasm exec) | TP / ALG | differential + Lean bisimulation | P1 | — | **RUNG LANDED (differential)**: `compiler/tangle-wasm/tests/differential.rs` EXECUTES the generated wasm with the `wasmi` interpreter (dev-dep) and checks the braid strand-permutation equals an independent reference model (trefoil, non-commuting pairs, braid-relation pairs, 5-strand weave). Validates codegen vs the permutation semantics; not a cross-binary diff against `eval.ml`, and Markov helpers untested. Full source↔wasm bisimulation (WasmCert) remains research-grade |
 | TG-7 | `Step.eqBraids` decides braid-group equivalence (not list equality) | ALG / DOM | OCaml + Lean 4 | P2 | — | **RUNG LANDED (non-semantic)**: `compiler/lib/braid_equiv.ml` decides braid-group equivalence via Dehornoy handle reduction, out-of-band (leaves `==`/`Step.eqBraids` as list equality). Tested (`compiler/test/tg7`, 2220 assertions: defining relations + 400 constructed-equivalent pairs + invariant-distinguished negatives). **Still OWNER-GATED**: whether to route `==` through it (a semantics change to eval.ml + Lean Step + proofs) is a language-design decision; Lean correctness (Garside/Dehornoy) remains research-grade |
-| TG-8 | Each dialect (braid-calculus, quantum-circuit, skein-algebra, string-diagram, virtual-knot) is a conservative extension of core | TP | Lean 4 per-dialect | P3 | 1w each | NOT STARTED |
+| TG-8 | Each dialect (braid-calculus, quantum-circuit, skein-algebra, string-diagram, virtual-knot) is a conservative extension of core | TP | OCaml model + Lean per-dialect | P3 | — | **TEMPLATE LANDED (virtual-knot)**: `compiler/lib/dialect_vk.ml` models VBₙ ⊃ Bₙ as core + a virtual layer that DELEGATES to `Braid_equiv` on the real fragment, so conservativity holds by construction; `compiler/test/tg8` (2311 assertions) verifies faithful embedding, core-delegation, invariant agreement, proper extension, virtual involution, honest undecided-frontier. Remaining: surface-syntax parser integration, the other 4 dialects (replicate the template), and a Lean conservativity proof |
 | TG-9 | LSP diagnostics are a subset of `HasType` failures (no LSP-only diagnostics) | INV | Audit + refactor | P2 | — | **LANDED** (`tangle-lsp` delegates all diagnostics to `tanglec --check` ⇒ `compiler/lib/check.ml`; hand-rolled LSP-only false positives removed. Subset holds by construction. Tests: `test_check.ml` + tangle-lsp unit/delegation tests) |
 | TG-10 | Echo-types integrated into the type system: `Echo[ρ,τ]` former + `echoClose`/`lower`/`residue`/`echoAdd`/`echoEq` + product type (`pair`/`fst`/`snd`), with Progress/Preservation/Determinism/TypeSafety extended to cover them and the non-injectivity / residue-recovery capstones proven | TP / DOM | Lean 4 | P1 | — | **LANDED** (`proofs/Tangle.lean` §ECHO-TYPES) |
 
@@ -70,12 +70,13 @@ assumptions each rests on, see PROOF-NARRATIVE.md.
 ## Scoping of the remaining obligations (2026-06-14)
 
 Concrete approach, effort, risk, and dependencies for what is left after
-TG-0/1/2/3/4/5/9/10 landed. **Landable rungs of TG-6 and TG-7 also landed**
-(2026-06-14): TG-6 now has a `wasmi` differential test executing the generated
-wasm; TG-7 has an out-of-band `braid_equiv` checker. What genuinely remains is
-**prerequisite-gated, not effort-gated**: TG-8 needs a dialect to exist as code;
-TG-7's *semantics change* needs an owner decision; TG-6's *full bisimulation*
-and TG-7's *Lean correctness proof* are research-grade.
+TG-0/1/2/3/4/5/9/10 landed. **Landable rungs of TG-6, TG-7, and TG-8 also
+landed** (2026-06-14): TG-6 a `wasmi` differential test; TG-7 an out-of-band
+`braid_equiv` checker; TG-8 a virtual-knot conservative-extension template. What
+genuinely remains is **owner-gated or research-grade**: TG-7's *semantics
+change* (decision); TG-8's *surface-syntax integration + other 4 dialects +
+Lean conservativity proof*; TG-6's *full source↔wasm bisimulation* and TG-7's
+*Lean correctness proof*.
 
 ### TG-3 — OCaml `typecheck.ml` refines Lean `HasType` — ✅ **LANDED 2026-06-14**
 - **Key lever (used):** TG-2 proves Lean `infer ≡ HasType`, so refinement
@@ -132,16 +133,24 @@ and TG-7's *Lean correctness proof* are research-grade.
   with tests, no semantic change. Lean correctness (Garside/Dehornoy) remains
   research-grade either way.
 
-### TG-8 — each dialect is a conservative extension of core — ⛔ **BLOCKED (no implementation)**
-- All five dialects (`dialects/{braid-calculus,quantum-circuit,skein-algebra,
-  string-diagram,virtual-knot}/`) are **prose + EBNF READMEs only** — zero
-  parser, typing, or evaluation code. Conservativity is a property of a formal
-  type system; there is no extended judgment/rules to state it over.
-- **Prerequisite:** implement ONE dialect end-to-end as the template — e.g.
-  virtual-knot: AST constructors (`ast.ml`), parser productions (`parser.mly`),
-  `HasType`+`Step` rules (`Tangle.lean`), eval (`eval.ml`), then a conservativity
-  test (core typed-in-core iff typed-in-dialect) mirroring the tg3/tg5 harness.
-  Only then can conservativity be proven; replicate per dialect (~1w each).
+### TG-8 — each dialect is a conservative extension of core — 🟡 **TEMPLATE LANDED (virtual-knot)**
+- ✅ **Conservativity template landed 2026-06-14**: `compiler/lib/dialect_vk.ml`
+  models the virtual-knot dialect (VBₙ ⊃ Bₙ — braids plus involutive virtual
+  crossings) as **core + a virtual layer that delegates to `Braid_equiv` (TG-7)
+  on the real fragment**, so conservativity holds *by construction* (the dialect
+  cannot change core typing/semantics). `compiler/test/tg8/tg8_conservativity.ml`
+  (2311 assertions) verifies: faithful embedding (`project∘embed=id`); the dialect
+  decides core terms exactly as the core procedure; invariant agreement
+  (permutation/writhe); proper extension (a virtual crossing is a genuinely-new
+  non-real element; vᵢvᵢ=ε); and an honest undecided-frontier (irreducible mixed
+  virtual content is reported `None`, never guessed).
+- **Honest scope:** this is the dialect's semantic core + conservativity bridge,
+  built as a separate module (no core-AST/Lean-oracle edits, avoiding the
+  `Warning 8` cascade). It is NOT yet a surface-syntax parser integration, and
+  VBₙ equivalence is a sound *partial* decider (full VBₙ word problem is
+  research-grade).
+- **Remaining:** surface syntax (`lexer`/`parser`/`ast`/`eval`); replicate the
+  template to the other four dialects; a mechanised Lean conservativity proof.
 
 ### TG-6 — WASM compilation preserves semantics — 🟡 **RUNG LANDED (differential)**
 - ✅ **Differential rung landed 2026-06-14**: `compiler/tangle-wasm/tests/differential.rs`

compiler/lib/dialect_vk.ml

@@ -0,0 +1,101 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* dialect_vk.ml — the virtual-knot dialect as a CONSERVATIVE EXTENSION of the
+ * core braid language.  TG-8 template (OCaml conservativity rung).
+ *
+ * The virtual braid monoid VBₙ extends the braid group Bₙ with *virtual*
+ * crossings vᵢ: involutions (vᵢ vᵢ = ε) with no over/under information and no
+ * writhe.  The classical embedding Bₙ ↪ VBₙ is known to be faithful, so VBₙ is a
+ * conservative extension of Bₙ.
+ *
+ * This module realises that extension so that conservativity holds BY
+ * CONSTRUCTION at the implementation level: the core (real) braid language
+ * embeds via [embed], and every decision on the real fragment is DELEGATED to
+ * the core decision procedure [Braid_equiv] (TG-7).  The dialect therefore
+ * cannot change core typing/semantics; virtual crossings are handled by new
+ * rules (involution, virtual permutation) that fire only on virtual syntax.
+ * `compiler/test/tg8` verifies this (delegation, faithful embedding, invariant
+ * agreement, proper extension, virtual involution).
+ *
+ * SCOPE (honest).  This is the dialect's semantic core + conservativity bridge,
+ * NOT a surface-syntax parser integration, and equivalence is a SOUND, PARTIAL
+ * decision procedure for VBₙ: real Dehornoy handle reduction (via Braid_equiv) +
+ * virtual involution + free reduction.  Words with irreducible mixed virtual
+ * content are reported UNDECIDED (`None`) rather than guessed.  A complete VBₙ
+ * word problem and a mechanised Lean conservativity proof are the next rungs.
+ *)
+
+module BE = Braid_equiv
+
+(* A virtual braid generator: a real crossing σᵢ^{±k} or a virtual crossing vᵢ. *)
+type vgen =
+  | Real of Ast.generator      (* real crossing (carries index + exponent) *)
+  | Virt of int                (* virtual crossing vᵢ at index i (involution) *)
+
+type vword = vgen list
+
+(* ---- embedding / projection (faithfulness) ---- *)
+
+(** Embed a core braid word into the dialect (all crossings real). *)
+let embed (gs : Ast.generator list) : vword = List.map (fun g -> Real g) gs
+
+(** Recover the core braid word iff the vword has no virtual crossings. *)
+let project (w : vword) : Ast.generator list option =
+  let rec go acc = function
+    | [] -> Some (List.rev acc)
+    | Real g :: r -> go (g :: acc) r
+    | Virt _ :: _ -> None
+  in
+  go [] w
+
+let is_real (w : vword) : bool = project w <> None
+let has_virtual (w : vword) : bool = List.exists (function Virt _ -> true | _ -> false) w
+
+(* ---- invariants ---- *)
+
+(** Underlying permutation on [1..strands]: BOTH real and virtual crossings
+    transpose adjacent strands (σᵢ^k acts as the transposition (i,i+1) repeated
+    |k| times; vᵢ once). *)
+let permutation ~(strands : int) (w : vword) : int array =
+  let p = Array.init strands (fun k -> k + 1) in
+  let swap i = if i >= 1 && i < strands then (let t = p.(i-1) in p.(i-1) <- p.(i); p.(i) <- t) in
+  List.iter (function
+    | Real g -> for _ = 1 to abs g.gen_exponent do swap g.gen_index done
+    | Virt i -> swap i) w;
+  p
+
+(** Writhe counts REAL crossings only (virtual crossings carry no sign). *)
+let writhe (w : vword) : int =
+  List.fold_left (fun a -> function Real g -> a + g.gen_exponent | Virt _ -> a) 0 w
+
+(* ---- reduction ---- *)
+
+let vinverse (w : vword) : vword =
+  List.rev_map (function
+    | Real g -> Real { g with gen_exponent = - g.gen_exponent }
+    | Virt i -> Virt i) w
+
+(* one pass of free + involution cancellation: σᵢ^a σᵢ^{-a} and vᵢ vᵢ. *)
+let cancel (a : vgen) (b : vgen) : bool =
+  match a, b with
+  | Virt i, Virt j -> i = j
+  | Real g, Real h -> g.gen_index = h.gen_index && g.gen_exponent = - h.gen_exponent
+  | _ -> false
+
+let free_reduce (w : vword) : vword =
+  List.fold_right (fun x acc ->
+    match acc with y :: rest when cancel x y -> rest | _ -> x :: acc) w []
+
+(** Decide whether a vword is the trivial braid.
+    [Some true]/[Some false] when decided; [None] when the word still has
+    irreducible mixed virtual content (the partial-decision frontier — honest,
+    never guessed).  On the REAL fragment this is the core decision procedure. *)
+let decide_trivial (w : vword) : bool option =
+  let r = free_reduce w in
+  if r = [] then Some true
+  else match project r with
+    | Some real -> Some (BE.is_trivial real)   (* real fragment → core decides (complete) *)
+    | None -> None                              (* mixed virtual residue → research-grade *)
+
+(** Equivalence in the dialect: [decide_trivial (u · v⁻¹)]. *)
+let equiv (u : vword) (v : vword) : bool option =
+  decide_trivial (u @ vinverse v)

compiler/lib/dialect_vk.mli

@@ -0,0 +1,39 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* dialect_vk.mli — virtual-knot dialect as a conservative extension of core
+ * braids (TG-8 template).  See dialect_vk.ml for scope and method. *)
+
+(** A virtual braid generator: a real crossing or a virtual crossing vᵢ. *)
+type vgen =
+  | Real of Ast.generator
+  | Virt of int
+
+type vword = vgen list
+
+(** Embed a core braid word (all crossings real).  [project (embed w) = Some w]. *)
+val embed : Ast.generator list -> vword
+
+(** Recover the core braid word iff there are no virtual crossings. *)
+val project : vword -> Ast.generator list option
+
+val is_real : vword -> bool
+val has_virtual : vword -> bool
+
+(** Underlying permutation on [1..strands] (real and virtual both transpose). *)
+val permutation : strands:int -> vword -> int array
+
+(** Writhe (real crossings only). *)
+val writhe : vword -> int
+
+(** Inverse virtual braid word. *)
+val vinverse : vword -> vword
+
+(** Free + involution reduction (σσ⁻¹ and vᵢvᵢ cancellation). *)
+val free_reduce : vword -> vword
+
+(** Decide triviality.  [Some _] when decided; on the real fragment this is the
+    core decision procedure (complete).  [None] iff irreducible mixed virtual
+    content remains (the honest partial-decision frontier). *)
+val decide_trivial : vword -> bool option
+
+(** Dialect equivalence = [decide_trivial (u · v⁻¹)]. *)
+val equiv : vword -> vword -> bool option

compiler/test/tg8/dune

@@ -0,0 +1,13 @@
+; SPDX-License-Identifier: MPL-2.0
+; TG-8 virtual-knot dialect conservativity template (Dialect_vk).
+;   dune runtest -> runs ./tg8_conservativity.exe --check.
+
+(executable
+ (name tg8_conservativity)
+ (modules tg8_conservativity)
+ (libraries tangle))
+
+(rule
+ (alias runtest)
+ (deps tg8_conservativity.exe)
+ (action (run ./tg8_conservativity.exe --check)))