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

## What

First instance of **mathematical-object arbitration**: when several
provers rule on the same goal, ECHIDNA now fuses their verdicts through
a policy-selected arbiter instead of an inline boolean all-must-agree
check.

The four arbitration mechanisms (portfolio `reconcile`, Bayesian
log-odds, Dempster-Shafer, Pareto) already existed in
`src/rust/verification/` but were **orphaned** — each had its own
bespoke input type and nothing outside its own tests called it.
`verify_proof_cross_checked` collapsed every cross-checker to a bool,
counted a timeout as disagreement, and flattened a genuine
Proven-vs-Refuted conflict to `verified=false`.

## How

- **`result_arbiter.rs`** (new):
`ResultArbiter::arbitrate(&[ProverAttempt]) -> ArbitratedVerdict`.
Adapts the 8-variant `ProverOutcome` taxonomy into each mechanism's
input; `ArbitrationPolicy` (`portfolio` default | `bayesian` |
`dempster_shafer`) selected via `DispatchConfig.arbitration_policy`. The
verdict carries agreeing/disagreeing/inconclusive camps, a [0,1]
conflict metric, `needs_review`, policy-specific posterior/belief, and a
Pareto-recommended prover among the agreeing set.
- **`dispatch.rs`**: cross-check path feeds rich outcomes to the
arbiter; `DispatchResult` gains `needs_review` + `arbitration`
(serde-defaulted → wire-compatible). Disagreements are named in the
message ("PROVERS DISAGREE: … — flagged for review").
- Semantics: timeout/error = **no-information** (no longer vetoes
agreement); `InconsistentPremises` from any prover taints the verdict
(`suspect_premises` → review); conclusive disagreement is never silently
flattened.
- `verified` stays primary-anchored (arbitrated-Proven **and** primary
proved) so existing consumers see no surprise flips.

## Owner decision embedded here (why this PR is NOT armed for
auto-merge)

The **default `ArbitrationPolicy::Portfolio`** keeps conservative
categorical semantics, but the timeout-is-not-disagreement change and
the `NoProofFound→Refuted` verdict mapping are policy calls on the trust
pipeline — please ratify (or request `bayesian`/`dempster_shafer` as
default).

## Verification

- 11 new unit tests: Proven-vs-Refuted conflict flagged not flattened,
DS high-conflict refusal, timeout tolerance, suspect premises, Pareto
pick, serde round-trip
- `cargo test --lib`: 1185 passed; edited integration suites (stage1,
e2e pipeline/prover, aspect, security, concurrency): 154 passed
- `cargo fmt --check` + clippy clean on the new module

Refs echidnabot#58 (multi-prover consensus). Follow-up (out of scope):
proof-object-level arbitration via the exchange/ translators — needs
`ProverBackend` to return proof objects first.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

Author: hyperpolymath

benches/routing_benchmarks.rs

@@ -307,6 +307,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};