feat(llm): Add frontier LLM advisor via BoJ Server integration

Integrate frontier language models (Claude, GPT-4, etc.) as proof
advisors through BoJ Server's cartridge system. The LLM suggests
tactics, ranks provers, decomposes goals, and generates auxiliary
lemmas — but CANNOT influence trust levels.

Architecture:
  ProofState → LlmAdvisor → BoJ REST API → Frontier LLM
  LLM suggestions → ProverDispatcher (trust pipeline unchanged)

New module: src/rust/llm.rs
  - LlmAdvisor: connects to BoJ (localhost:7700) for LLM guidance
  - TacticSuggestionRequest/Response: structured JSON protocol
  - ProverRecommendation: LLM-ranked prover selection
  - GoalDecomposition: LLM-suggested subgoal splitting
  - DispatchOptimisation: LLM-guided dispatch configuration
  - In-context learning via proof attempt history
  - Cost-aware model routing via BoJ model-router cartridge
  - 8 tests (all passing)

Integration into dispatch.rs:
  - ProverDispatcher.with_llm_advisor(): attach LLM advisor
  - verify_proof_llm_guided(): LLM-optimised dispatch path
  - Falls back to standard dispatch if LLM unavailable

Trust invariant: LLM optimises WHICH PATH to take, never WHAT
THE ANSWER IS. Trust levels computed solely by dispatch pipeline.

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

Author: hyperpolymath

src/rust/dispatch.rs

@@ -13,6 +13,7 @@ use std::time::Instant;
 use tracing::{info, warn};
 
 use crate::integrity::solver_integrity::{IntegrityChecker, IntegrityStatus};
+use crate::llm::{LlmAdvisor, DispatchOptimisation};
 use crate::provers::{ProverConfig, ProverFactory, ProverKind};
 use crate::verification::axiom_tracker::{AxiomTracker, AxiomUsage, DangerLevel};
 use crate::verification::confidence::{compute_trust_level, TrustFactors, TrustLevel};
@@ -71,6 +72,9 @@ impl Default for DispatchConfig {
 pub struct ProverDispatcher {
     config: DispatchConfig,
     integrity_checker: Option<IntegrityChecker>,
+    /// Optional frontier LLM advisor for intelligent dispatch optimisation.
+    /// Advisory only — cannot influence trust levels.
+    llm_advisor: Option<LlmAdvisor>,
 }
 
 impl ProverDispatcher {
@@ -79,12 +83,13 @@ impl ProverDispatcher {
         Self {
             config: DispatchConfig::default(),
             integrity_checker: None,
+            llm_advisor: None,
         }
     }
 
     /// Create a dispatcher with custom configuration
     pub fn with_config(config: DispatchConfig) -> Self {
-        Self { config, integrity_checker: None }
+        Self { config, integrity_checker: None, llm_advisor: None }
     }
 
     /// Set the integrity checker for solver binary verification
@@ -93,6 +98,59 @@ impl ProverDispatcher {
         self
     }
 
+    /// Set the frontier LLM advisor for intelligent dispatch optimisation.
+    /// Advisory only — the trust pipeline remains inviolable.
+    pub fn with_llm_advisor(mut self, advisor: LlmAdvisor) -> Self {
+        self.llm_advisor = Some(advisor);
+        self
+    }
+
+    /// Dispatch with LLM-guided optimisation
+    ///
+    /// The LLM suggests which prover to try and which cross-checkers to use.
+    /// If the LLM is unavailable, falls back to the provided prover_kind.
+    /// Trust levels are NEVER influenced by the LLM.
+    pub async fn verify_proof_llm_guided(
+        &self,
+        content: &str,
+        fallback_prover: ProverKind,
+    ) -> Result<DispatchResult> {
+        // Try to get LLM optimisation
+        if let Some(ref advisor) = self.llm_advisor {
+            if advisor.is_available() {
+                // Parse content into a minimal proof state for the LLM
+                let prover_config = ProverConfig::default();
+                if let Ok(prover) = ProverFactory::create(fallback_prover, prover_config) {
+                    if let Ok(state) = prover.parse_string(content).await {
+                        if let Some(opt) = advisor.optimise_dispatch(&state).await {
+                            info!(
+                                "LLM dispatch optimisation: primary={:?}, cross_check={:?}",
+                                opt.primary_prover, opt.cross_check_provers
+                            );
+
+                            let primary = opt.primary_prover.unwrap_or(fallback_prover);
+
+                            if !opt.cross_check_provers.is_empty() {
+                                return self
+                                    .verify_proof_cross_checked(
+                                        primary,
+                                        content,
+                                        &opt.cross_check_provers,
+                                    )
+                                    .await;
+                            }
+
+                            return self.verify_proof(primary, content).await;
+                        }
+                    }
+                }
+            }
+        }
+
+        // Fallback: use provided prover without LLM guidance
+        self.verify_proof(fallback_prover, content).await
+    }
+
     /// Dispatch a proof verification request through the trust-hardening pipeline
     pub async fn verify_proof(
         &self,

src/rust/lib.rs

@@ -10,6 +10,7 @@ pub mod core;
 pub mod provers;
 pub mod parsers;
 pub mod neural;
+pub mod llm; // Frontier LLM advisor (via BoJ Server)
 pub mod aspect;
 pub mod agent;
 pub mod ffi;
@@ -24,6 +25,7 @@ pub mod dispatch;
 pub use core::{ProofState, Term, Tactic, TacticResult};
 pub use provers::{ProverBackend, ProverKind, ProverConfig};
 pub use agent::{AgentCore, AgentConfig};
+pub use llm::{LlmAdvisor, LlmConfig};
 
 #[cfg(test)]
 mod tests {