eml-optimize — shorter witnesses & equivalence gate

Read ../_shared/eml-foundations.md first. Algorithm details live in references/search-internals.md.

When this skill triggers (and when it doesn't)

Triggers on: "are these two EML trees equivalent?", "can you shorten this witness?", "find the shortest EML tree for cos(x)", "run peephole swap on this compiled tree", "regenerate the leaderboard", "is the published K=15 for neg reproducible?".

Does not trigger on: compiling a sympy expression to EML (that's /eml-lab), verifying a single tree against a named claim (use /eml-check), or fitting a law from data (/eml-fit). For "is identity X true?" on arbitrary elementary expressions, use /math-identity-check.

Subcommands

subcommand	what it does
`equiv`	Dense interior sampling (default 1024) + branch-cut probes from `/eml-check`'s catalog. Two trees or a tree + named claim. Returns verdict, max_abs_diff, and per-locus branch flags.
`peephole`	Walks a tree bottom-up; for each subtree, tries every stored witness that is shorter. A numerical gate decides. Returns new RPN, delta_K, and list of swaps.
`search`	Bottom-up enumerative beam search. `targeted` (default) uses meet-in-the-middle complement lookup, backward goal propagation, optional library-witness seeding (`--seed-witnesses`), optional subtree seeding (`--seed-subtrees`), and an optional `--symbolic-gate` that runs sympy.simplify on top-N near-miss candidates when beam returns not-found. Target matches are re-gated by full equivalence. `closure` is the reference enumerator (no goal propagation).
`leaderboard`	Standalone `scripts/leaderboard.py` reads `WITNESSES` → `docs/leaderboard.md` (public). Columns: name · arity · best known K · paper K · proof-engine K · domain · verdict · collapsible tree · proof URL. `--check` exits 1 on staleness (used as a CI gate); `--format json` for web consumers.