feat(exchange): TPTP + SMT-LIB + SMTCoq + Lambdapi bridges

Four new cross-prover proof exchange bridges extending the existing
OpenTheory + Dedukti coverage in src/rust/exchange/:

- tptp.rs: structured TptpProblem/TptpFormula/TptpRole/TptpDialect
  (CNF/FOF/TFF/THF/TCF). import_problem + export_problem round-trip;
  translate_to_smtlib for CNF/FOF (TFF/THF return UnsupportedDialect);
  translate_from_smtlib best-effort reverse. ExchangeError enum.
  6 tests.

- smtlib.rs: SmtLibScript + SmtLibCommand enum (SetLogic, SetInfo,
  SetOption, DeclareSort, DeclareFun, DefineFun, Assert, CheckSat,
  GetModel, GetProof, GetUnsatCore, Push, Pop, Exit, Reset, Other).
  parse / emit / normalise (alpha-sorts declarations while preserving
  semantic order); extract_logic; translate_to_tptp_fof. 5 tests.

- smtcoq.rs: STUB BRIDGE (documented as such — gated on upstream
  SMTCoq plugin). AletheProof / AletheStep / LfscProof / DratProof
  types. parse_alethe_proof + parse_lfsc_proof + parse_drat_unsat.
  emit_coq_skeleton produces a Lemma ... admit. Qed. skeleton with
  proof bytes as comments; validate_proof_well_formed. 6 tests.

- lambdapi.rs: Dedukti's successor. LambdapiModule / LambdapiSymbol
  (Constant/Definition/Theorem/Symbol/Injective/Sequential/Private/
  Protected) / LambdapiRule. import / export round-trip;
  translate_from_dedukti rewrites `def x := ...` -> `symbol x ≔ ...;`
  and rewrite rules; translate_to_dedukti reverse. 7 tests.

mod.rs registers the four new modules (additive only).

Lane: prover-corpus-saturation.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath