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

[hyperpolymath]

Implements the owner ruling on #50 — option (a) true braid-group equivalence.

σ₁σ₂σ₁ == σ₂σ₁σ₂ is now true. Syntactic equality contradicted the language's own thesis (programs are topological objects; equivalence is isotopy), so == was the one place that quietly reverted to comparing representations.

Both engines, one change

The TG-3 differential and the Lean proof oracle straddle OCaml and Lean, so they move together.

OCaml — eval.ml Eq on VBraid routes through the existing, already-tested braid_equiv.ml (Dehornoy handle reduction). 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.

Lean — new §BRAID-GROUP EQUIVALENCE in Tangle.lean ports the same procedure. Six Step rules use it: eqBraids, eqIdBraid, eqBraidId, and the three echoEq counterparts — echoEq must follow, because eval.ml's EchoEq explicitly reuses the Eq logic.

~ (isotopy) moved too — a completeness fix

~ used simplify_gens, which only cancels adjacent inverses and does not implement the braid relation. Leaving it while == became complete would allow a == b true with a ~ b false — incoherent, since for braids isotopy is braid-group equality. So this is a completeness fix, not a change of intended meaning.

Closed tangles are documented honestly: link isotopy is Markov equivalence (conjugation + stabilisation), which is NOT implemented. On tv_closed tangles this stays a sound-but-incomplete under-approximation — true is trustworthy, false only means "not equal as braids".

Metatheory: unchanged, and that is the point

Progress / Preservation / Determinism re-verified with 0 errors, no proof edits. All three need only that the right-hand side is a total function into Bool. Determinism is immediate: a function applied to fixed arguments yields a fixed result. 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, still research-grade (#51).

Recorded as new assumption A-TG-7.2 and stated plainly in PROOF-NARRATIVE.md, so a green gate cannot be mistaken for a proof. The Lean port is fuel-bounded rather than well-founded, because proving termination is that research obligation.

Tests that actually distinguish the semantics

The pre-existing braid-equality tests pass under either semantics, so they could not demonstrate this change. Eight new cases in test_eval.ml do:

Case	Under list-eq	Now
s1.s2.s1 == s2.s1.s2 (braid relation)	false	true
s1.s3 == s3.s1 (far commutation)	false	true
s1.s1^-1 == identity	false	true
identity == s1.s1^-1 (symmetry)	false	true
s1 == s1^-1 (guard: differing writhe)	false	false
s1.s2 == s2.s1 (guard: adjacent don't commute)	false	false
~ agrees with == on the braid relation	false	true
echoEq lowers to braid-group equality	false	true

Two are deliberate negatives, guarding against a decision procedure that just returns true. eval suite 104 → 112; whole suite 0 failures.

Two defects found while doing this

1. The OCaml compiler was never gated. dune build/dune test ran nowhere in CI — the lexer, parser, typechecker, interpreter and 4,000+ assertions (TG-3 1008, TG-5 189, TG-7 2220, TG-8 2311, plus the rest) were entirely ungated. A semantics change to eval.ml could have landed fully green with nothing having compiled it. Adds .github/workflows/ocaml-ci.yml, using apt rather than a setup action so no new third-party pin enters the estate (an unresolvable pin produces no check run at all).

2. 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 — only the unanchored /- alternative did anything. It went unnoticed purely because no comment had yet contained one of those words; the TG-7 trusted-base note does. Now anchored after the prefix: strictly tighter than the old catch-all, and verified to still catch a real sorry (negative control).

Verification

• lean Tangle.lean → 0 errors
• sorry/axiom/admit gate (fixed filter) → pass, and still catches an injected sorry
• check-tg3-differential.sh → 496 obligations, 0 errors
• dune build → clean; dune test --force → 0 failures across all suites

Closes the semantics half of #51.

🤖 Generated with Claude Code

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ⚠️ Changes requested 0 resolved / 2 findings

Implements true braid-group equivalence for == and ~ in OCaml and Lean, but the changes require fixes for OCaml CI grep false-positives and missing test coverage for the Lean braidEquiv port.

⚠️ Bug: New OCaml CI FAIL-grep false-positives on green runs

📄 .github/workflows/ocaml-ci.yml:78

The Test step greps the combined log with grep -qiE '^[[:space:]]*FAIL'. Because it is case-insensitive, it matches the summary line Failed: 0 that compiler/test/test_compositional.ml unconditionally prints (Printf.printf "Failed: %d ") even when zero tests failed. dune test surfaces that line, so this step will exit 1 and turn the gate red on a fully passing run — defeating the purpose of the newly-added gate (I verified the grep matches Failed: 0). Fix by dropping -i (all real per-test failures print uppercase FAIL, so case-sensitive matching still catches them while no longer colliding with the Failed: label).

Remove the -i flag so the summary label `Failed: 0` no longer matches; uppercase per-test `FAIL` lines are still caught.

if grep -qE '^[[:space:]]*FAIL' /tmp/dune-test.log; then
  echo "::error::A test reported FAIL — see the log above."
  exit 1
fi

💡 Quality: Lean braidEquiv port has no test coverage

📄 proofs/Tangle.lean:187-201

The new §BRAID-GROUP EQUIVALENCE definitions in Tangle.lean (braidEquiv/isTrivialBraid/reduceOne/scanHandle) are claimed to be a faithful port of braid_equiv.ml, but only the OCaml side is exercised by tests (test_eval.ml). A-TG-7.2 explicitly assumes the two engines agree, yet nothing would catch a divergence in the Lean port. Consider adding a few #eval/example checks in Tangle.lean mirroring the OCaml TG-7 cases (e.g. braidEquiv [σ1σ2σ1] [σ2σ1σ2] = true, [σ1] vs [σ1⁻¹] = false) so the port's behavior is at least smoke-tested where it is defined.

🤖 Prompt for agents

Code Review: Implements true braid-group equivalence for `==` and `~` in OCaml and Lean, but the changes require fixes for OCaml CI grep false-positives and missing test coverage for the Lean braidEquiv port.

1. ⚠️ Bug: New OCaml CI FAIL-grep false-positives on green runs
   Files: .github/workflows/ocaml-ci.yml:78

   The Test step greps the combined log with `grep -qiE '^[[:space:]]*FAIL'`. Because it is case-insensitive, it matches the summary line `Failed: 0` that `compiler/test/test_compositional.ml` unconditionally prints (`Printf.printf "Failed: %d
   "`) even when zero tests failed. `dune test` surfaces that line, so this step will `exit 1` and turn the gate red on a fully passing run — defeating the purpose of the newly-added gate (I verified the grep matches `Failed: 0`). Fix by dropping `-i` (all real per-test failures print uppercase `FAIL`, so case-sensitive matching still catches them while no longer colliding with the `Failed:` label).

   Fix (Remove the -i flag so the summary label `Failed: 0` no longer matches; uppercase per-test `FAIL` lines are still caught.):
   if grep -qE '^[[:space:]]*FAIL' /tmp/dune-test.log; then
     echo "::error::A test reported FAIL — see the log above."
     exit 1
   fi

2. 💡 Quality: Lean braidEquiv port has no test coverage
   Files: proofs/Tangle.lean:187-201

   The new §BRAID-GROUP EQUIVALENCE definitions in Tangle.lean (braidEquiv/isTrivialBraid/reduceOne/scanHandle) are claimed to be a faithful port of braid_equiv.ml, but only the OCaml side is exercised by tests (test_eval.ml). A-TG-7.2 explicitly assumes the two engines agree, yet nothing would catch a divergence in the Lean port. Consider adding a few `#eval`/`example` checks in Tangle.lean mirroring the OCaml TG-7 cases (e.g. `braidEquiv [σ1σ2σ1] [σ2σ1σ2] = true`, `[σ1] vs [σ1⁻¹] = false`) so the port's behavior is at least smoke-tested where it is defined.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}