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.