feat(verification): unified ResultArbiter — wire the 4-mechanism arbitration stack into dispatch

The arbitration stack (portfolio reconcile, Bayesian log-odds,
Dempster-Shafer, Pareto) existed but was orphaned: each mechanism
defined its own input type and nothing outside its own tests called it.
verify_proof_cross_checked re-implemented a boolean all-must-agree
check inline, collapsed cross-checker outcomes to bool, counted a
timeout as disagreement, and flattened Proven-vs-Refuted conflicts to
verified=false.

New src/rust/verification/result_arbiter.rs:
- ProverAttempt (prover, ProverOutcome, elapsed) as the common input;
  outcome_to_verdict maps the 8-variant taxonomy onto the verdict frame
  (timeout/error = no-information; InconsistentPremises = suspect flag)
- ArbitrationPolicy (portfolio default | bayesian | dempster_shafer)
  selected via DispatchConfig.arbitration_policy
- ArbitratedVerdict: winning verdict, agreeing/disagreeing/inconclusive
  camps, [0,1] conflict metric, needs_review, policy posterior/belief,
  and a Pareto-recommended prover among the agreeing set

dispatch.rs: verify_proof_cross_checked now feeds every cross-checker's
rich outcome to the arbiter; DispatchResult gains needs_review +
arbitration (serde-defaulted, wire-compatible). verified stays
primary-anchored, but a cross-checker timeout no longer vetoes
agreement, and conclusive disagreement is surfaced by name in the
message and flagged for review.

11 new unit tests incl. the Proven-vs-Refuted conflict, DS high-conflict
refusal, and timeout-tolerance cases. 1185 lib + 154 integration tests
green.

Refs echidnabot#58 (multi-prover consensus roadmap).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: hyperpolymath

benches/routing_benchmarks.rs

@@ -306,6 +306,7 @@ fn bench_dispatch_config_construction(c: &mut Criterion) {
                 generate_certificates: true,
                 timeout: 60,
                 diagnostics: false,
+                arbitration_policy: Default::default(),
             })
         })
     });

docs/wiki/Guides.md

@@ -101,6 +101,10 @@ Motivating examples:
 - **Dempster-Shafer** — "Five solvers; three Proven, two Refuted; either commit a posterior or *refuse to arbitrate* because conflict is too high."
 - **Pareto** — "Lean took 30s and produced a 4kB certificate; Z3 took 0.2s and produced no certificate. Which dominates?" — neither; return both as Pareto-optimal.
 
+### Unified entry point: `ResultArbiter`
+
+You normally don't call the four mechanisms directly. `ResultArbiter` (`src/rust/verification/result_arbiter.rs`) takes the per-prover `ProverOutcome`s from a cross-checked dispatch, adapts them into whichever mechanism `DispatchConfig.arbitration_policy` selects (`portfolio` default | `bayesian` | `dempster_shafer`), and returns an `ArbitratedVerdict`: winning verdict, agreeing/disagreeing/inconclusive camps, a `[0,1]` conflict metric, `needs_review`, and a Pareto-recommended prover among the agreeing set. `Dispatcher::verify_proof_cross_checked` attaches it to `DispatchResult.arbitration`. Key semantics: timeouts and errors are no-information (they no longer veto agreement), and a genuine Proven-vs-Refuted split is flagged for review instead of being flattened to `verified = false`.
+
 ## Guide: Cross-prover semantic queries
 
 The synonym layer carries an optional `semantic_class` tag per entry. Combined with the three cross-prover dictionaries (`_msc2020.toml`, `_wordnet_math.toml`, `_conceptnet_seed.toml`) this gives "every prover's name for the same concept" lookups, fully offline.

src/rust/dispatch.rs

@@ -25,6 +25,9 @@ use crate::provers::outcome::{classify_anyhow_error, ProverOutcome};
 use crate::provers::{ProverConfig, ProverFactory, ProverKind};
 use crate::verification::axiom_tracker::{AxiomTracker, AxiomUsage, DangerLevel};
 use crate::verification::confidence::{compute_trust_level, TrustFactors, TrustLevel};
+use crate::verification::result_arbiter::{
+    ArbitratedVerdict, ArbitrationPolicy, ProverAttempt, ResultArbiter,
+};
 
 #[cfg(feature = "chapel")]
 use crate::proof_search::{ChapelParallelSearch, ProofSearchStrategy};
@@ -89,6 +92,17 @@ pub struct DispatchResult {
     /// input and per-prover records.
     #[serde(default)]
     pub diagnostics: Option<RunDiagnostics>,
+    /// True when arbitration found conclusive disagreement, all-timeout,
+    /// high evidential conflict, or suspect premises. A `verified = false`
+    /// with `needs_review = true` means "the provers could not settle it",
+    /// not "the proof is bad".
+    #[serde(default)]
+    pub needs_review: bool,
+    /// Full arbitration verdict for cross-checked dispatches: winning
+    /// verdict, agreeing/disagreeing camps, conflict metric, and any
+    /// policy-specific posterior/belief. `None` on single-prover paths.
+    #[serde(default)]
+    pub arbitration: Option<ArbitratedVerdict>,
 }
 
 /// Configuration for the dispatch pipeline
@@ -109,6 +123,11 @@ pub struct DispatchConfig {
     /// default is `false` so production callers pay nothing.
     #[serde(default)]
     pub diagnostics: bool,
+    /// Which mechanism fuses cross-checked prover outcomes into one
+    /// verdict. Default `Portfolio` (categorical agreement) — the
+    /// conservative pre-arbiter behaviour.
+    #[serde(default)]
+    pub arbitration_policy: ArbitrationPolicy,
 }
 
 impl Default for DispatchConfig {
@@ -120,6 +139,7 @@ impl Default for DispatchConfig {
             generate_certificates: false,
             timeout: 300,
             diagnostics: false,
+            arbitration_policy: ArbitrationPolicy::default(),
         }
     }
 }
@@ -568,6 +588,8 @@ impl ProverDispatcher {
                     cross_checked: false,
                     outcome,
                     diagnostics,
+                    needs_review: false,
+                    arbitration: None,
                 });
             },
         };
@@ -688,6 +710,8 @@ impl ProverDispatcher {
             cross_checked: false,
             outcome,
             diagnostics,
+            needs_review: false,
+            arbitration: None,
         })
     }
 
@@ -769,27 +793,40 @@ impl ProverDispatcher {
                 .collect()
         };
 
-        // Run additional provers for cross-checking
-        let mut all_agree = primary_result.verified;
+        // Run additional provers and collect their rich outcomes — the
+        // arbiter needs to distinguish "refuted" from "timed out" from
+        // "errored", which the boolean `verified` flattens away.
+        let mut attempts = vec![ProverAttempt::new(
+            primary_prover,
+            primary_result.outcome.clone(),
+            primary_result.proof_time_ms,
+        )];
         let mut provers_used = vec![format!("{:?}", primary_prover)];
-        let mut confirming_count: u32 = if primary_result.verified { 1 } else { 0 };
 
         for &additional in available_cross_checkers.iter() {
             match self.verify_proof(additional, content).await {
                 Ok(result) => {
                     provers_used.push(format!("{:?}", additional));
-                    if result.verified {
-                        confirming_count += 1;
-                    } else {
-                        all_agree = false;
-                    }
+                    attempts.push(ProverAttempt::new(
+                        additional,
+                        result.outcome.clone(),
+                        result.proof_time_ms,
+                    ));
                 },
                 Err(e) => {
                     warn!("Cross-check with {:?} failed: {}", additional, e);
                 },
             }
         }
 
+        // Arbitrate: fuse the per-prover outcomes under the configured
+        // policy instead of the old inline all-must-agree boolean check.
+        let arbiter =
+            ResultArbiter::new(self.config.arbitration_policy, self.config.timeout * 1000);
+        let arbitration = arbiter.arbitrate(&attempts);
+
+        let confirming_count = attempts.iter().filter(|a| a.outcome.is_proved()).count() as u32;
+
         let elapsed = start.elapsed().as_millis() as u64;
 
         // Recompute trust level with cross-checking info
@@ -822,13 +859,7 @@ impl ProverDispatcher {
             certificate_verified: false,
             worst_axiom_danger: worst_danger,
             solver_integrity_ok,
-            portfolio_confidence: Some(if confirming_count >= 2 {
-                crate::verification::portfolio::PortfolioConfidence::CrossChecked
-            } else if confirming_count == 1 {
-                crate::verification::portfolio::PortfolioConfidence::SingleSolver
-            } else {
-                crate::verification::portfolio::PortfolioConfidence::Inconclusive
-            }),
+            portfolio_confidence: Some(arbitration.confidence),
         };
 
         let trust_level = compute_trust_level(&trust_factors);
@@ -841,14 +872,32 @@ impl ProverDispatcher {
         primary_result.provers_used = provers_used;
         primary_result.proof_time_ms = elapsed;
         primary_result.cross_checked = cross_checked;
-        primary_result.verified = all_agree && primary_result.verified;
+        // `verified` stays primary-anchored: the arbitrated verdict must be
+        // Proven AND the primary itself proved the goal. A timeout among the
+        // cross-checkers no longer vetoes agreement (it is no-information),
+        // but a conclusive disagreement always does. Consumers wanting the
+        // fused multi-prover verdict read `arbitration`.
+        primary_result.verified =
+            matches!(arbitration.verified, Some(true)) && primary_result.outcome.is_proved();
+        primary_result.needs_review = arbitration.needs_review;
 
         if cross_checked {
-            primary_result.message = format!(
-                "Proof cross-checked by {} prover(s) with {}",
-                confirming_count, trust_level
-            );
+            primary_result.message = if !arbitration.disagreeing.is_empty() {
+                format!(
+                    "PROVERS DISAGREE on this goal: {:?} vs {:?} (conflict {:.2}) — flagged for review",
+                    arbitration.agreeing, arbitration.disagreeing, arbitration.conflict
+                )
+            } else if arbitration.suspect_premises {
+                "Premises flagged inconsistent by a cross-checker — result withheld for review"
+                    .to_string()
+            } else {
+                format!(
+                    "Proof cross-checked by {} prover(s) with {}",
+                    confirming_count, trust_level
+                )
+            };
         }
+        primary_result.arbitration = Some(arbitration);
 
         Ok(primary_result)
     }
@@ -1012,6 +1061,8 @@ impl ProverDispatcher {
                 cross_checked: false,
                 outcome,
                 diagnostics,
+                needs_review: false,
+                arbitration: None,
             })
         }
 
@@ -1186,6 +1237,8 @@ mod tests {
             cross_checked: false,
             outcome: ProverOutcome::Proved { elapsed_ms: 1500 },
             diagnostics: None,
+            needs_review: false,
+            arbitration: None,
         };
 
         let json = serde_json::to_string(&result).unwrap();
@@ -1229,6 +1282,7 @@ mod tests {
             generate_certificates: true,
             timeout: 600,
             diagnostics: false,
+            arbitration_policy: Default::default(),
         };
         assert!(config.cross_check);
         assert_eq!(config.min_trust_level, TrustLevel::Level4);

src/rust/verification/mod.rs

@@ -28,6 +28,11 @@
 //!
 //! Picking between them: see the "Guide: Picking an arbitration
 //! mechanism" entry in `docs/wiki/Guides.md`.
+//!
+//! Unified entry point: `result_arbiter` adapts per-prover
+//! [`crate::provers::outcome::ProverOutcome`]s into whichever mechanism
+//! the configured [`result_arbiter::ArbitrationPolicy`] selects; the
+//! dispatch cross-check path delegates to it.
 
 pub mod axiom_tracker;
 pub mod bayesian_arbiter;
@@ -40,6 +45,7 @@ pub mod pareto_arbiter;
 pub mod portfolio;
 #[cfg(feature = "verisim")]
 pub mod proof;
+pub mod result_arbiter;
 pub mod statistics;
 
 pub use axiom_tracker::{AxiomPolicy, AxiomTracker, AxiomUsage, DangerLevel};
@@ -52,4 +58,5 @@ pub use portfolio::{PortfolioConfig, PortfolioResult, PortfolioSolver};
 pub use proof::{
     theorem_identity, Proof, ProofStateRecord, ProofVersion, TacticApplication, TacticStatus,
 };
+pub use result_arbiter::{ArbitratedVerdict, ArbitrationPolicy, ProverAttempt, ResultArbiter};
 pub use statistics::{StatisticsTracker, StatsSummaryRecord};