Decision needed (owner)
TG-7 asks whether == on braids should decide braid-group equivalence rather than list equality.
Current state. == on braids is list equality in both compiler/lib/eval.ml and the Lean Step.eqBraids rule. A complete braid-group equivalence checker (Dehornoy handle reduction) now exists out-of-band as compiler/lib/braid_equiv.ml (tested in compiler/test/tg7, 2220 assertions). It does not change ==.
The fork:
- (a) Change semantics — route
== / Step.eqBraids through braid-group equivalence. Changes the observable semantics of == on braids; touches eval.ml and the Lean Step relation, rippling into the Progress / Preservation / Determinism proofs.
- (b) Keep
== as list equality — use braid_equiv only as a tool (tooling / compute-style checks), leaving language semantics unchanged.
A mechanised Lean Garside/Dehornoy correctness proof for braid_equiv is research-grade either way (tracked in the remaining-work issue).
Refs: PROOF-NEEDS.md (TG-7); landed at origin/main 5ed31f8.
Decision needed (owner)
TG-7 asks whether
==on braids should decide braid-group equivalence rather than list equality.Current state.
==on braids is list equality in bothcompiler/lib/eval.mland the LeanStep.eqBraidsrule. A complete braid-group equivalence checker (Dehornoy handle reduction) now exists out-of-band ascompiler/lib/braid_equiv.ml(tested incompiler/test/tg7, 2220 assertions). It does not change==.The fork:
==/Step.eqBraidsthrough braid-group equivalence. Changes the observable semantics of==on braids; toucheseval.mland the LeanSteprelation, rippling into the Progress / Preservation / Determinism proofs.==as list equality — usebraid_equivonly as a tool (tooling /compute-style checks), leaving language semantics unchanged.A mechanised Lean Garside/Dehornoy correctness proof for
braid_equivis research-grade either way (tracked in the remaining-work issue).Refs:
PROOF-NEEDS.md(TG-7); landed atorigin/main5ed31f8.