feat(tg-7): == on braids decides braid-group equivalence (#50 ruling)

Implements the owner ruling on #50: option (a), true braid-group
equivalence. Syntactic equality contradicted the language's own thesis —
programs are topological objects and equivalence is isotopy — so `==` was
the one place that quietly reverted to comparing representations.
`σ₁σ₂σ₁ == σ₂σ₁σ₂` is now true.

Landed on BOTH engines in one change, because the TG-3 differential and the
Lean proof oracle straddle them:

* OCaml — `eval.ml` `Eq` on VBraid routes through `braid_equiv.ml`
  (Dehornoy handle reduction, already present and tested). `Identity` is
  `VBraid []`, so identity comparisons flow through the same case.
  Added `ast_of_gen(s)`, the missing inverse of the existing `gen_of_ast`
  (the runtime and AST generator records are structurally identical but
  nominally distinct).

* Lean — new §BRAID-GROUP EQUIVALENCE in `Tangle.lean` ports the same
  procedure (`unitsOf`, `inverseWord`, `freeReduce`, `scanHandle`,
  `rewriteInterior`, `reduceOne`, `reduceFuel`, `braidEquiv`). Six Step
  rules now use it: `eqBraids`, `eqIdBraid`, `eqBraidId` and the three
  `echoEq` counterparts — echoEq must follow because eval.ml's EchoEq
  explicitly reuses the Eq logic.

`~` (isotopy) routes there too. It used `simplify_gens`, which only cancels
adjacent inverses and does NOT implement the braid relation. Leaving that
while `==` became complete would have allowed `a == b` true with `a ~ b`
false, which is incoherent — for braids, isotopy IS braid-group equality.
This is a completeness fix, not a change of intended meaning. Closed
tangles are documented as a sound-but-incomplete under-approximation:
link isotopy is Markov equivalence, which is NOT implemented.

Progress / Preservation / Determinism re-verified UNCHANGED — all three need
only that the RHS is a total function into Bool. TG-3's 496 kernel-checked
obligations still pass (typing is untouched; only the runtime value changes).

TRUSTED, NOT PROVEN. These are definitions, not axioms, so the sorry/axiom
gate passes legitimately — but that does not make the claim proven. The
metatheory holds *relative to* `braidEquiv`; that `braidEquiv` correctly
DECIDES braid-group equality is the mechanised Garside/Dehornoy proof, which
remains research-grade (#51). Recorded as new assumption A-TG-7.2, and
stated plainly in PROOF-NARRATIVE.md so the green gate cannot be mistaken
for a proof. The Lean port is fuel-bounded rather than well-founded, since
proving termination IS that research obligation.

Tests: 8 new cases in test_eval.ml that DISTINGUISH the two semantics (the
pre-existing braid-equality tests pass either way, so they could not). They
cover the braid relation, far commutation, free cancellation, symmetry, and
two negatives guarding against a procedure that just says true. eval suite
104 -> 112, whole suite 0 failures.

Also in this change, both found while doing the above:

* `.github/workflows/ocaml-ci.yml` (NEW) — the OCaml compiler and its 4,000+
  assertions were NOT built or run by CI at all; only the Lean proofs were
  gated. A semantics change to eval.ml could have landed fully green with
  nothing having compiled it. Uses apt rather than a setup action so no new
  third-party pin enters the estate.

* `lean-proofs.yml` — the sorry/axiom gate's comment filter never worked:
  it anchored on `^\s*--` AFTER `grep -n` had prepended `<line>:`, so the
  documented "outside comments" exemption could never match. It went
  unnoticed only because no comment had yet contained one of these words;
  the TG-7 trusted-base note does. Anchored after the prefix — strictly
  tighter than the old unanchored `/-` catch-all, and verified to still
  catch a real `sorry`.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/lean-proofs.yml

@@ -74,7 +74,15 @@ jobs:
           set -euo pipefail
           banned_count=0
           for pat in '\bsorry\b' '\baxiom\b' '\badmit\b' '\bAdmitted\b'; do
-            matches=$(grep -nE "$pat" Tangle.lean | grep -vE "^\s*--|^\s*/--|/-" || true)
+            # NB the comment filter must account for grep -n's "<line>:" prefix.
+            # The previous pattern anchored on "^\s*--", which could NEVER match
+            # once -n had prepended "178:" — so the documented "outside comments"
+            # exemption was dead, and only the unanchored "/-" alternative
+            # excluded anything. It went unnoticed purely because no comment had
+            # yet contained one of these words; the TG-7 trusted-base note does.
+            # Anchoring after the prefix restores the intended behaviour and is
+            # STRICTER than the old unanchored "/-" catch-all.
+            matches=$(grep -nE "$pat" Tangle.lean | grep -vE "^[0-9]+:[[:space:]]*(--|/--|/-)" || true)
             if [ -n "$matches" ]; then
               echo "::error::Forbidden token matching '$pat' in Tangle.lean:"
               echo "$matches"

.github/workflows/ocaml-ci.yml

@@ -0,0 +1,104 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# OCaml compiler build + test gate.
+#
+# ── Why this exists ────────────────────────────────────────────────────────
+# Until 2026-07-29 the OCaml compiler — the lexer, parser, typechecker and
+# interpreter, plus a test suite of well over 4,000 assertions (TG-3 1008,
+# TG-5 189, TG-7 2220, TG-8 2311, and the parser/typecheck/eval/e2e/property/
+# round-trip suites) — was **not built or run by CI at all**.  Only the Lean
+# proofs were gated.  A semantics change to `eval.ml` could therefore land
+# fully green with nothing having compiled it.
+#
+# That gap was found while implementing the TG-7 ruling (#50), which changes
+# what `==` MEANS on braids.  A change of that weight must be gated, so this
+# workflow makes `dune build` + `dune test` the oracle: any PR that breaks the
+# compiler or a single assertion fails here rather than landing silently.
+#
+# ── Toolchain choice ───────────────────────────────────────────────────────
+# Debian/Ubuntu packages (`ocaml-dune`, `menhir`) rather than an OCaml setup
+# ACTION, deliberately: it adds no new third-party action pin to the estate's
+# allowlist, and no pin that can later become unresolvable — the failure mode
+# that produces a workflow with NO check run at all.
+
+name: OCaml CI
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'compiler/**'
+      - '.github/workflows/ocaml-ci.yml'
+  pull_request:
+    paths:
+      - 'compiler/**'
+      - '.github/workflows/ocaml-ci.yml'
+  workflow_dispatch: {}
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build-and-test:
+    name: Build + test the OCaml compiler
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Install OCaml toolchain
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends ocaml ocaml-dune menhir
+          ocaml -version
+          dune --version
+          menhir --version
+
+      - name: Build
+        working-directory: compiler
+        run: dune build
+
+      - name: Test
+        working-directory: compiler
+        run: |
+          set -euo pipefail
+          # `dune test` exits non-zero if any suite fails. Also fail on any
+          # "FAIL" line: several suites print their own tally and would
+          # otherwise report failures while still exiting 0.
+          dune test --force 2>&1 | tee /tmp/dune-test.log
+          if grep -qiE '^[[:space:]]*FAIL' /tmp/dune-test.log; then
+            echo "::error::A test reported FAIL — see the log above."
+            exit 1
+          fi
+          if grep -qE '[1-9][0-9]* failed' /tmp/dune-test.log; then
+            echo "::error::A suite reported a nonzero failure count."
+            grep -nE '[1-9][0-9]* failed' /tmp/dune-test.log
+            exit 1
+          fi
+          echo "OCaml compiler: build + all suites GREEN."
+
+      - name: TG-7 semantics guard
+        working-directory: compiler
+        run: |
+          set -euo pipefail
+          # The TG-7 ruling (#50) is only real if `==` actually decides
+          # braid-group equality. These cases are FALSE under list equality,
+          # so their presence and passing is what distinguishes the two
+          # semantics — guard against a silent revert.
+          missing=0
+          for t in "braid relation s1.s2.s1 == s2.s1.s2" \
+                   "far commutation s1.s3 == s3.s1" \
+                   "non-equivalent braids still compare false"; do
+            grep -qF "$t" test/test_eval.ml || { echo "::error::TG-7 test missing: $t"; missing=1; }
+          done
+          [ "$missing" -eq 0 ] || exit 1
+          echo "TG-7 semantics tests present."

ASSUMPTIONS.md

@@ -32,6 +32,7 @@ Cross-references use `[[A-TG-N.M]]` syntax, resolved here.
 | A-TG-6.1 | MATH | WASM small-step semantics is well-defined; assume the official Wasm spec / WasmCert-Isabelle definition | TG-6 | wasm-spec, WasmCert-Isabelle |
 | A-TG-6.2 | DESIGN | Source semantics has no floating-point non-determinism (Tangle has only `Int` currently) | TG-6 | `Tangle.lean::Ty` lacks `.float` |
 | A-TG-7.1 | MATH | Word problem in the braid group `B_n` is solvable in polynomial time (Birman–Ko–Lee / Garside normal form) | TG-7 | Birman–Ko–Lee 1998; _A New Approach to the Word and Conjugacy Problems in the Braid Groups_ |
+| A-TG-7.2 | IMPL | `braidEquiv` (`proofs/Tangle.lean`) and `braid_equiv.ml` implement Dehornoy handle reduction **correctly**, and agree with each other. Since the 2026-07-29 ruling (#50) routed `==` through them, this is **load-bearing for the semantics of `==`**: the Step relation's metatheory is proven only *relative to* `braidEquiv`, never that it decides braid-group equality. Evidenced by testing (2220 + 8 assertions), not proof. Retired by the mechanised Garside/Dehornoy proof (#51, research-grade). The Lean port is additionally **fuel-bounded**, so termination is assumed rather than proven. | TG-7 | `compiler/lib/braid_equiv.ml`; `proofs/Tangle.lean` §BRAID-GROUP EQUIVALENCE; `compiler/test/tg7` |
 | A-TG-8.1 | DESIGN | Each dialect's grammar is a strict superset of core's EBNF (`tangle.ebnf`) | TG-8 | `dialects/*/grammar.ebnf` |
 | A-TG-8.2 | DESIGN | Each dialect's typing rules are additive (new constructors + their typing rules only; no modification of existing rules) | TG-8 | Per-dialect spec |
 | A-TG-9.1 | DESIGN | `tangle-lsp` emits diagnostics in four documented categories (`PARSE_ERROR`, `MISSPELLING_HINT`, `STRUCTURAL_HINT`, `NAME_HINT`); only `PARSE_ERROR` corresponds to a grammar-level rejection. The other three are LSP-only by design (Option B from TG-9 audit; Option A — full refinement via FFI to `typecheck.ml` — remains queued at #28). Each emission site is tagged in the `Diagnostic.source` field as `tangle-lsp[CATEGORY]`. | TG-9 | `compiler/tangle-lsp/src/backend.rs`; `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md` |

PROOF-NARRATIVE.md

@@ -413,17 +413,56 @@ by isotopy." Currently `eqBraids` only checks list equality, so
 `σ_1 σ_2 σ_1` and `σ_2 σ_1 σ_2` are reported unequal. That's the
 trivial reading.
 
-**Status.** Current `eqBraids` is a soundness floor (if equal lists
-then equal braids), not a completeness ceiling. Promoting it to
-braid-group equivalence is a research-grade extension.
+**Status — LANDED 2026-07-29 (owner ruling #50), with a stated trusted base.**
+`==` on braids now decides braid-group equivalence in both engines:
+
+- **OCaml** — `eval.ml` `Eq` (and `Isotopy`, which for braids denotes the
+  *same* relation) route through `compiler/lib/braid_equiv.ml` (Dehornoy
+  handle reduction). `Identity` is `VBraid []`, so identity comparisons flow
+  through the same case.
+- **Lean** — `Step.eqBraids` / `eqIdBraid` / `eqBraidId`, and the three
+  `echoEq` counterparts, use `braidEquiv` / `isTrivialBraid`: a faithful
+  in-Lean port of the same procedure, in §BRAID-GROUP EQUIVALENCE of
+  `Tangle.lean`.
+
+`σ₁σ₂σ₁ == σ₂σ₁σ₂` is now `true`, which is what the README's "equivalence is
+defined by isotopy" always claimed. Progress / Preservation / Determinism were
+re-verified **unchanged** — all three need only that the right-hand side is a
+*total function into `Bool`*, which `braidEquiv` is; Determinism in particular
+is immediate, since a function applied to fixed arguments yields a fixed result.
+
+> ### ⚠ TRUSTED, NOT PROVEN — the honest boundary
+> `braidEquiv` is a **definition**, not an axiom: nothing is postulated, and
+> the sorry/axiom gate passes legitimately. But **the gate passing does NOT
+> mean this claim is proven.** What is established is that the metatheory
+> holds *relative to* `braidEquiv`. What is **not** established is that
+> `braidEquiv` correctly **decides** braid-group equality — that is the
+> mechanised Garside/Dehornoy correctness proof, which remains research-grade
+> and out of scope (#51).
+>
+> Correctness is currently evidenced **by testing only**: `compiler/test/tg7`
+> (2220 assertions — defining relations, 400 constructed-equivalent pairs,
+> invariant-distinguished negatives) plus 8 semantics-distinguishing cases in
+> `test_eval.ml`. Testing is not proof.
+>
+> Termination in the Lean port is by an explicit **fuel** bound mirroring the
+> OCaml `max_steps`, not by a well-founded measure. Dehornoy reduction does
+> terminate, but proving that *is* the research obligation above; fuel keeps
+> the definitions total without smuggling in an unproven termination claim.
 
 **Assumptions.**
 - [[A-TG-7.1]] Word problem in the braid group is solvable in
   polynomial time on finitely many strands (Birman–Ko–Lee /
   Garside-normal-form algorithm — known true).
-
-**How to discharge.** Implement Birman–Ko–Lee normal form;
-re-prove `Step.eqBraids` against the normal form.
+- [[A-TG-7.2]] `braidEquiv` (Lean) and `braid_equiv.ml` (OCaml) implement
+  Dehornoy handle reduction *correctly*, and agree with each other. Evidenced
+  by testing, not proof. **This is the load-bearing unproven assumption of
+  TG-7.**
+
+**How to discharge the remainder.** Mechanise the Dehornoy correctness
+argument (or a Birman–Ko–Lee normal form) in Lean, prove `braidEquiv u v =
+true ↔ u ≡ v` in the braid group, and prove termination to replace the fuel
+bound. That retires [[A-TG-7.2]].
 
 ### TG-8 — Dialect conservativity
 

PROOF-NEEDS.md

@@ -59,7 +59,7 @@ Cross-referenced to [PROOF-NARRATIVE.md §3](PROOF-NARRATIVE.md#3-remaining-obli
 | TG-4 | Pretty-print/parse round-trip on closed values | INV | OCaml property test (cheap) | P2 | 4h | **LANDED** (PR #46 — OCaml property test in `compiler/test/test_roundtrip.ml`, 26-entry corpus including 8 echo/product constructors; 52 round-trip runs) |
 | 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-7 | `Step.eqBraids` decides braid-group equivalence (not list equality) | ALG / DOM | OCaml + Lean 4 | P2 | — | **SEMANTICS LANDED 2026-07-29** (owner ruling #50 → (a) true braid-group equivalence). `==` on braids now decides braid-group equality in BOTH engines: OCaml `eval.ml` `Eq`/`Isotopy` route through `compiler/lib/braid_equiv.ml`; Lean `Step.eqBraids`/`eqIdBraid`/`eqBraidId` (and the three `echoEq` counterparts) use `braidEquiv`, a faithful in-Lean port of the same Dehornoy procedure. Progress/Preservation/Determinism re-verified unchanged (they need only a total function into `Bool`). Tested: `compiler/test/tg7` 2220 assertions + 8 new semantics-distinguishing cases in `test_eval.ml`. **Remaining (research-grade): the mechanised Garside/Dehornoy correctness proof — `braidEquiv` is TRUSTED, NOT PROVEN; the Step relation is proven only RELATIVE to it** |
 | 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) |
@@ -73,10 +73,11 @@ 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, 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*.
+genuinely remains is **research-grade**: 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-7's **semantics
+change is no longer owner-gated — it was ruled and landed 2026-07-29**, see
+#50 and the TG-7 row above.)
 
 ### TG-3 — OCaml `typecheck.ml` refines Lean `HasType` — ✅ **LANDED 2026-06-14**
 - **Key lever (used):** TG-2 proves Lean `infer ≡ HasType`, so refinement

compiler/lib/braid_equiv.ml

@@ -2,12 +2,16 @@
 (* braid_equiv.ml — decide braid-GROUP equivalence of braid words via Dehornoy
  * handle reduction.
  *
- * TG-7, NON-SEMANTIC rung.  The language's `==` on braids (eval.ml `VBraid`
- * equality and the Lean `Step.eqBraids` rule) is LIST equality and is left
- * UNCHANGED by this module — `braid_equiv` is an out-of-band decision procedure
- * for callers who want true braid-group equivalence (e.g. tooling, future
- * `compute`-style checks).  Changing `==` itself to use this is a separate
- * language-design decision (see PROOF-NEEDS.md TG-7).
+ * TG-7, SEMANTIC rung as of 2026-07-29.  Owner ruling tangle#50 settled the
+ * open question in favour of true braid-group equivalence: the language's `==`
+ * on braids (eval.ml `Eq` on `VBraid`, and the Lean `Step.eqBraids` rule via
+ * `braidEquiv`) now DECIDES braid-group equality, not list equality.  `~`
+ * (isotopy) routes here too — for braids, isotopy IS equality in the braid
+ * group, so the two must agree.
+ *
+ * Rationale: syntactic equality contradicts the language's own thesis, that
+ * programs are topological objects and equivalence is isotopy.  `==` must not
+ * be the one place that quietly reverts to comparing representations.
  *
  * Algorithm (Dehornoy 1997, "A fast method for comparing braids").  A braid
  * word on σ₁,σ₂,…  A σᵢ-handle is a factor

compiler/lib/braid_equiv.mli

@@ -1,9 +1,9 @@
 (* SPDX-License-Identifier: MPL-2.0 *)
-(* braid_equiv.mli — out-of-band braid-GROUP equivalence (TG-7, non-semantic).
+(* braid_equiv.mli — braid-GROUP equivalence (TG-7; the semantics of `==`).
  *
- * Decides braid-group equality via Dehornoy handle reduction.  This does NOT
- * change the language's `==` on braids (eval.ml / Lean Step keep list equality);
- * it is a separate decision procedure for callers wanting true equivalence. *)
+ * Decides braid-group equality via Dehornoy handle reduction.  As of the
+ * owner ruling tangle#50 (2026-07-29) this IS the language's `==` on braids
+ * (eval.ml `Eq`, Lean `Step.eqBraids` via `braidEquiv`), and `~` too. *)
 
 (** A braid word as unit letters (index >= 1, sign +/-1). *)
 type letter = { idx : int; sgn : int }