feat(provers): add KeYmaera X backend (Phase 3 differential dynamic logic)

Lands the worked example for Phase 3 of the ECHIDNA expansion —
differential dynamic logic and hybrid systems verification. KeYmaera X
is the only prover in the 128-backend roster that targets dL natively
(hybrid programs, ODE evolution under domain constraints, modal box/
diamond formulas). It plugs the hybrid-systems gap that no SMT or
TPTP-shaped ATP can cover.

Implementation:
- src/rust/provers/keymaerax.rs (313 LOC, 8 unit tests)
  - to_kyx: ProofState → .kyx ArchiveEntry serialiser
  - parse_result: stdout/stderr scanner for closed/open/refuted markers
  - parse_string: extracts the Problem ... End. body as a single goal
- 10 integration points wired in mod.rs: pub mod, ProverKind variant
  (Tier 5d), name parser, all() list, complexity (4), trust tier (2,
  delegates QE to external CAS), ml-score (2.5), binary name
  (keymaerax), factory dispatch
- FFI u8 = 128 (next free slot after LiquidHaskell at 127); both
  kind_to_u8 and kind_from_u8 updated

Acceptance:
- cargo build --lib clean
- cargo test --lib keymaerax: 8/8 passed
- cargo test --lib overall green (886 tests + 8 new)
- panic-attack: 0 unsafe_blocks / 0 panic_sites / 0 unwrap_calls

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

Author: hyperpolymath

src/rust/ffi/mod.rs

@@ -529,6 +529,7 @@ pub fn kind_from_u8(kind: u8) -> Option<ProverKind> {
         125 => Some(ProverKind::GNATprove),
         126 => Some(ProverKind::Stainless),
         127 => Some(ProverKind::LiquidHaskell),
+        128 => Some(ProverKind::KeYmaeraX),
         _ => None,
     }
 }
@@ -1270,6 +1271,7 @@ pub fn kind_to_u8(kind: ProverKind) -> u8 {
         ProverKind::GNATprove => 125,
         ProverKind::Stainless => 126,
         ProverKind::LiquidHaskell => 127,
+        ProverKind::KeYmaeraX => 128,
     }
 }