hyperpolymath · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026
diff --git a/.github/workflows/idris2-abi-ci.yml b/.github/workflows/idris2-abi-ci.yml
@@ -11,6 +11,8 @@ on:
     paths:
       - 'src/abi/**'
       - 'src/idris/**'
+      - 'tests/abi/**'
+      - 'scripts/abi-fixtures.sh'
       - '.github/workflows/idris2-abi-ci.yml'
   # No paths-filter on pull_request: this job is a REQUIRED status check, so it
   # must report on every PR (a path-filtered required check deadlocks PRs that
@@ -44,7 +46,7 @@ jobs:
           GH_TOKEN: ${{ github.token }}
         run: |
           set -euo pipefail
-          PATTERN='^(src/abi/|src/idris/)'
+          PATTERN='^(src/abi/|src/idris/|tests/abi/|scripts/abi-fixtures\.sh$)'
           if [ "${{ github.event_name }}" = "pull_request" ]; then
             FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \
                       --paginate --jq '.[].filename')
@@ -93,6 +95,13 @@ jobs:
           idris2 --build echidnaabi.ipkg
           echo "✓ All ABI modules type-check successfully"
 
+      - name: Accept/reject fixtures (mechanical falsifier)
+        if: steps.detect.outputs.relevant == 'true'
+        run: |
+          # tests/abi/accept must type-check; tests/abi/reject must be refused
+          # with a unification error (each reject mirrors one accept fixture).
+          bash scripts/abi-fixtures.sh
+
       - name: Type-check Idris2 proof validator (src/idris)
         if: steps.detect.outputs.relevant == 'true'
         run: |

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
@@ -8,6 +8,24 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Added — arbitration 2026-10-14 (ECH-05)
+
+* *Fidelity-levelled arbitration*: `+ProverAttempt+` carries
+`+FidelityEvidence+` (`+KernelTranslation+` / `+DeclaredCorrespondence+` /
+`+None+`) and `+ArbitratedVerdict+` gains `+level+` (`+belief+` / `+epi+` /
+`+sound+`), `+retracted+` and `+warranted_term+`. `+sound+` needs every
+fused attempt to be a kernel-checked translation to one exchange-layer
+term (`+exchange::term_hash+`); a synonym collision stays `+belief+`
+however many backends agree. `+ResultArbiter::retract+` marks a backend
+unsound and lowers every verdict that rested on it. Numeric fusion is
+unchanged: `+tests/arbitration_regression_test.rs+` replays the
+pre-change numbers. Dispatch attaches no evidence yet, so dispatched
+verdicts are `+belief+`.
+* *`+EchidnaABI.Arbitration+`* (Idris2): the three-level verdict as a
+closed sum whose `+Sound+` constructor carries the hash-equality proofs,
+with the classifier and its properties; `+tests/abi/{accept,reject}+`
+fixtures checked by `+scripts/abi-fixtures.sh+` in `+idris2-abi-ci.yml+`.
+
 ==== Added — integrations 2026-10-05
 
 * *`+echidna prove --output json+`*: prints exactly one

diff --git a/Justfile b/Justfile
@@ -311,6 +311,11 @@ proofs-verif-idris:
     fi
     echo "Idris2 verification corpus: all files type-check"
 
+# Accept fixtures must type-check, reject fixtures must be refused (tests/abi).
+# Type-check the Idris2 ABI accept/reject fixtures (mechanical falsifier).
+abi-fixtures:
+    bash scripts/abi-fixtures.sh
+
 # Heavy (downloads the ~500MB Isabelle release), so this is gated by the weekly
 # verification-proofs-cron workflow, not the per-PR `proofs` rollup. Covers the
 # base-HOL theories; algebra/GroupTheory.thy is excluded (see proofs/isabelle/ROOT).

diff --git a/docs/ROADMAP.adoc b/docs/ROADMAP.adoc
@@ -108,6 +108,12 @@ Stage 6  Cross‑prover semantics             translation actually works
     6b  Dedukti bridge real                 λΠ modulo as lingua franca
     6c  mathematical identity arbitration   canonicalise across representations
     6d  Coursera delivery                   Zig ABI exposes capability
+    acceptance (ECH‑05)                     a KernelTranslation certificate
+                                            is producible for a named backend
+                                            pair; arbitration already levels
+                                            verdicts belief / epi / sound by
+                                            that evidence (row "Cross‑prover
+                                            semantics" in §3)
 
 Stage 7  Sovereign tooling surround         the rest of the ecosystem
     7a  Stapeln container lifecycle
@@ -198,6 +204,18 @@ schema; nightly CI ≥ 1 h; zero known panic paths
 orphans, verified 2026‑04‑27) |*`+ProverKind+` ≥ 65 variants, every one
 factory‑dispatched*; CLAUDE.md states the canonical count; no orphans —
 *target met and exceeded*
+
+|"`Cross‑prover semantics`" |The exchange bridges
+(`+src/rust/exchange/+`) parse and emit their formats; none produces a
+kernel‑checked translation. `+ResultArbiter+` grades each verdict
+`+belief+` / `+epi+` / `+sound+` by per‑attempt `+FidelityEvidence+`
+(ECH‑05), so a synonym collision cannot reach `+sound+`; dispatch attaches
+no evidence yet, so every dispatched verdict is `+belief+`
+|*A `+KernelTranslation+` certificate is producible for a named backend
+pair*, and a verdict on that pair reaches `+sound+`. First candidate:
+HOL4 ↔ HOL Light through OpenTheory (6a); then Lean 4 ↔ Rocq through
+Dedukti (6b). Pair table: `+docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc+`
+§ "Backend pairs that can share a term"
 |===
 
 === 4. Current sprint — "`the smallest set that flips half the table`"

diff --git a/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc b/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc
@@ -95,6 +95,12 @@ epistemic type detection 3. Implement knowledge/belief type operators 4.
 Develop common knowledge analysis 5. Add secrecy/privacy type
 verification
 
+*Meta-level use (ECH-05)*: result arbitration grades each verdict
+`belief` / `epi` / `sound`, following epistemic-types' `Warrant` /
+`Epi` / `SoundWarrant`; see "Backend pairs that can share a term" below.
+That is a level on ECHIDNA's own verdicts, not epistemic typing of user
+proofs, so the status above stands.
+
 === 5. Advanced Substructural Types
 
 *Status*: ✅ Partial (via Idris2 linear types)
@@ -216,6 +222,50 @@ analysis
 |Type Classes |❌ |✅ Multiple |Low |Low
 |===
 
+==== Backend pairs that can share a term
+
+Cross-prover agreement only warrants the source claim when the backends'
+statements are the same term. `ResultArbiter` (ECH-05) grades a verdict
+`sound` only if every fused attempt carries a `KernelTranslation`
+certificate to one exchange-layer term, and `epi` for declared
+correspondences validated by consequence testing; lexical alignment
+through `data/synonyms/` alone is `belief`. The table names the backend
+pairs whose type theories meet in an exchange format, so that a
+kernel-checked shared term is possible in principle.
+
+The route column names external projects, which were not run for this
+table. The last column is ECHIDNA's own state: no bridge in
+`src/rust/exchange/` produces a kernel-checked translation yet, so every
+row is DESIGNED and no pair reaches `sound` today. Producing one
+certificate for one pair is the ROADMAP stage 6 acceptance.
+
+[cols="2,2,3,2",options="header"]
+|===
+|Backend pair |`ExchangeFormat` |External route |In ECHIDNA
+|HOL4 ↔ HOL Light |`open_theory` |OpenTheory articles, both directions;
+checked by the OpenTheory article reader |DESIGNED (`opentheory.rs`
+exports and imports proof states, not checked articles); first candidate
+|Lean 4 ↔ Rocq |`dedukti` / `lambdapi` |Lean and Coq encodings in λΠ
+modulo (Lean4Less/lean4dk, CoqInE); checked by Dedukti or Lambdapi
+|DESIGNED (`dedukti.rs`, `lambdapi.rs` translate syntax only)
+|HOL family ↔ Lean 4 / Rocq |`dedukti` |OpenTheory → Dedukti (Holide),
+then as above |DESIGNED
+|Agda ↔ Lean 4 / Rocq |`dedukti` |Agda → Dedukti (agda2dk, research
+prototype) |DESIGNED
+|cvc5 / veriT ↔ Rocq |`smt_coq` |Alethe or LFSC certificates replayed by
+the Coq kernel (SMTCoq) |DESIGNED (`smtcoq.rs` parses certificates and
+emits a skeleton)
+|Z3 / cvc5 / veriT ↔ Isabelle/HOL |`smt_lib` |SMT proofs reconstructed by
+Isabelle's `smt` method |DESIGNED
+|Vampire / E ↔ Isabelle/HOL |`tptp` |TPTP problems generated by
+Sledgehammer, proofs reconstructed with Metis |DESIGNED
+|===
+
+For the automated rows the exchange-layer term is the problem the
+interactive side generated, so fidelity there is the interactive
+system's translation into SMT-LIB or TPTP; that translation is what a
+`KernelTranslation` certificate for the pair has to cover.
+
 === Strategic Expansion Plan
 
 ==== Phase 1: Critical Gap Closure (6-12 months)

diff --git a/docs/design/TYPING_CAPABILITIES_COMPARISON.adoc b/docs/design/TYPING_CAPABILITIES_COMPARISON.adoc
@@ -194,7 +194,11 @@ comparing:
 ==== What We Provide That Single Systems Cannot
 
 * *Cross-System Type Arbitration*: Determine when types from different
-systems are equivalent
+systems are equivalent. Today the arbiter grades each verdict `belief` /
+`epi` / `sound` by per-backend fidelity evidence (ECH-05); `sound` needs a
+kernel-checked shared term, which no backend pair can produce yet. Pair
+table: `ADVANCED_TYPING_GAP_ANALYSIS.adoc`, "Backend pairs that can share
+a term".
 * *Multi-Type-System Proof Routing*: Send proofs to the most appropriate
 type system
 * *Heterogeneous Type Safety*: Ensure type safety across mixed-system

diff --git a/docs/wikis/Guides.md b/docs/wikis/Guides.md
@@ -105,6 +105,8 @@ Motivating examples:
 
 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`.
 
+Agreement is not identity: N backends proving N lexically aligned statements are N warrants for N propositions. Each `ProverAttempt` therefore carries `FidelityEvidence` — `KernelTranslation { format, checked_by, term_hash }` (a kernel-checked translation through `src/rust/exchange/`), `DeclaredCorrespondence { consequence_tests, failures }`, or `None` — and `ArbitratedVerdict.level` grades the fused verdict `belief` / `epi` / `sound` (ECH-05). `sound` needs every fused attempt to be a kernel translation to the same exchange-layer term; a tested correspondence with no failures gives `epi`; anything else, any attempt without evidence, a verdict that needs review, or one resting on a backend marked unsound with `ResultArbiter::retract` is `belief`. The numeric fusion is unchanged under the level. Dispatch does not attach evidence yet, so every dispatched verdict is `belief` until the exchange bridges can produce certificates (ROADMAP stage 6). The Idris2 statement is `src/abi/EchidnaABI/Arbitration.idr`.
+
 ## 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.

diff --git a/issues/README.md b/issues/README.md
@@ -4,7 +4,8 @@ SPDX-License-Identifier: CC-BY-SA-4.0
 
 # Issue specifications
 
-Drafted issue specifications for the ParadisEO metaheuristic integration roadmap.
+Drafted issue specifications: ECH-01..04, PB and EB for the ParadisEO metaheuristic
+integration roadmap; ECH-05 for fidelity-levelled result arbitration.
 Each file is the body for one GitHub issue; the title and labels are in the file header.
 
 To produce an issue body from a file (everything after the `# ` title line, without the SPDX header):
@@ -19,6 +20,7 @@ awk 'f;/^# /{f=1}' issues/<file> | sed '1{/^$/d}' > /tmp/body.md
 | ECH-02 | hyperpolymath/echidna        | #421         | `echidna-02-cmaes-julia-gnn.md`                       |
 | ECH-03 | hyperpolymath/echidna        | #422         | `echidna-03-chapel-island-migration.md`               |
 | ECH-04 | hyperpolymath/echidna        | #424         | `echidna-04-ffi-abi-bridge.md`                        |
+| ECH-05 | hyperpolymath/echidna        | not filed    | `echidna-05-fidelity-evidence.md`                     |
 | PB-01  | hyperpolymath/proof-burrower | not filed    | `proof-burrower-01-combinatorial-tactic-synthesis.md` |
 | PB-02  | hyperpolymath/proof-burrower | not filed    | `proof-burrower-02-ledger-fitness-formulation.md`     |
 | EB-01  | hyperpolymath/echidnabot     | not filed    | `echidnabot-01-adaptive-ci-portfolio-scheduler.md`    |
@@ -28,6 +30,7 @@ awk 'f;/^# /{f=1}' issues/<file> | sed '1{/^$/d}' > /tmp/body.md
 ## Status
 
 - **ECH-01..04** are filed on hyperpolymath/echidna and carry all their labels. On 2026-10-09 their bodies were replaced by hand with a different text that is not these files; the owner decides which is canonical (see `docs/handover/PARADISEO-ROADMAP-PROMPT.adoc`, WP0). `scripts/issues/sync-roadmap-issues.sh` syncs the bodies from these files (dry run by default; refuses to replace hand-edited bodies without `--overwrite`).
+- **ECH-05** is a draft for hyperpolymath/echidna, not filed. Its implementation (fidelity evidence on `ProverAttempt`, `level` on `ArbitratedVerdict`, `EchidnaABI.Arbitration`, the fidelity tests) lands with the PR that adds the file.
 - **PB-01, PB-02, EB-01** are drafts for copying to their own repositories. They are not filed.
 
 ## Provenance of the PB and EB drafts
@@ -46,5 +49,6 @@ Labels named in the drafts that did not exist when they were written (checked 20
 |------------------------------|---------------------------------------------------------------------|
 | hyperpolymath/proof-burrower | `area:swarm`, `rust`, `search-tactics`, `area:ledger`, `heuristics` |
 | hyperpolymath/echidnabot     | `area:dispatcher`, `ci-optimization` (`rust` exists)                |
+| hyperpolymath/echidna        | `area:arbitration`, `area:exchange`, `epistemic-types`, `residual-evidence-types` (ECH-05; checked 2026-10-14) |
 
-All labels used by ECH-01..04 exist on hyperpolymath/echidna.
+All labels used by ECH-01..04 exist on hyperpolymath/echidna; ECH-05's `enhancement` and `idris2` do.