feat(cli): add Codex-backed tactic search export path

[markm39]

Summary

• add a Codex-backed tactic proposer for tactic search using OpenProof's existing ChatGPT auth transport
• export solved Pantograph trajectories to append-only JSONL under ~/.openproof/expert-data/ in prompt/completion format
• add openproof tactic-search --resume <session_id> for direct expert-play/data-generation runs on an existing session workspace
• fall back to the active node statement or accepted target when line-level goal extraction is empty

Validation

• cargo check -p openproof-cli
• target/debug/openproof ask "Return exactly OK."
• OPENPROOF_TACTIC_PROPOSER=standard target/debug/openproof tactic-search --resume export_smoke_1774880498
• OPENPROOF_TACTIC_PROPOSER=codex OPENPROOF_TACTIC_MODEL=gpt-5.4 target/debug/openproof tactic-search --resume export_smoke_1774880498
• confirmed ~/.openproof/expert-data/positives.jsonl and ~/.openproof/expert-data/trajectories.jsonl were written with a verified record:
  {"prompt":"True:::","completion":"exact True.intro", ... "backend":"codex","model":"gpt-5.4"}