Proof obligations: remaining work after TG-3/5/6/7/8 (2026-06-14)

[hyperpolymath]

Tracking the remaining proof-obligation work for tangle.

Landed + pushed this round (origin/main 5ed31f8): TG-3 (translation validation — proofs/TG3Differential.lean, 496 kernel-checked obligations + proofs/TG3-REFINEMENT.md), TG-5 (compositional invariants), and the TG-6 / TG-7 / TG-8 rungs. Fully closed: TG-0/1/2/3/4/5/9/10. See PROOF-NEEDS.md.

Remaining

• TG-7 — == semantics decision (owner; blocks TG-7 completion) — see TG-7 decision: braid == semantics — list-equality vs braid-group equivalence #50
• TG-8 — replicate the virtual-knot conservative-extension template (compiler/lib/dialect_vk.ml) to the other four dialects: braid-calculus, quantum-circuit, skein-algebra, string-diagram
• TG-8 — surface-syntax parser integration for the dialect(s) (lexer/parser/ast/eval)
• TG-8 — mechanised Lean conservativity proof
• TG-6 — full source↔wasm bisimulation (WasmCert); current rung is a wasmi differential test only (compiler/tangle-wasm/tests/differential.rs) — research-grade
• TG-7 — mechanised Lean Garside/Dehornoy correctness proof for braid_equiv — research-grade

Notes

• Do not start the TG-8 dialect fan-out until scope is re-confirmed.
• A concurrent session (claude/practical-newton-*) is/was active on this repo; git fetch + rebase onto origin/main before any push.

[hyperpolymath]

TG-7 semantics: LANDED (PR #87)

The first checkbox — TG-7 == semantics decision (owner; blocks TG-7 completion) — is now done. Ruling #50 was (a) true braid-group equivalence, and it is implemented in both engines:

• OCaml — eval.ml Eq (and Isotopy) route through braid_equiv.ml.
• Lean — new §BRAID-GROUP EQUIVALENCE in Tangle.lean; six Step rules use braidEquiv/isTrivialBraid (eqBraids, eqIdBraid, eqBraidId + the three echoEq counterparts).

σ₁σ₂σ₁ == σ₂σ₁σ₂ is now true. Progress/Preservation/Determinism re-verified unchanged (they need only a total function into Bool); TG-3's 496 kernel-checked obligations still pass.

Still open on this issue

• TG-7 — mechanised Lean Garside/Dehornoy correctness proof — research-grade, and now load-bearing: since == routes through braidEquiv, the Step relation is proven only relative to it. Registered as assumption A-TG-7.2; stated explicitly in PROOF-NARRATIVE.md so the green sorry/axiom gate is not mistaken for a proof. The Lean port is also fuel-bounded, so termination is assumed rather than proven — that too is retired by this proof.
• TG-8 dialect fan-out (scope still unconfirmed — not started, per the note in this issue)
• TG-8 surface-syntax parser integration
• TG-8 mechanised Lean conservativity proof
• TG-6 full source↔wasm bisimulation (WasmCert) — research-grade

Incidental fixes in #87

• .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.
• lean-proofs.yml — the sorry/axiom gate's comment filter never worked (it anchored ^\s*-- after grep -n had prepended <line>:). Fixed and verified to still catch a real sorry.