Repository navigation
Consume fidelity evidence, not re-proofs #429
Description
The multi-prover plan's value was the disagreement signal between
independent formalisations, which autoformal-fidelity states precisely
(two target standpoints; agreement = identical partitions; convergence is
evidence only under independence). Ask: echidna ingests fibre coverage,
round-trip and cross-prover agreement from one kernel (Agda) plus
independent standpoints, rather than N copies of each proof.
Filed from the 2026-10-12 family session; see nextgen-typing docs/TYPE-CONNECTIONS.adoc for the connection statuses.
Activity
hyperpolymath commentedon Oct 14, 2026
The arbiter-typing slice of this is done: ECH-05 (#431), via #430.
The arbiter now takes per-backend fidelity evidence and grades each verdict
belief/epi/sound. A synonym collision can no longer fuse tosound.Still open here: ingesting fibre coverage, round trips and cross-prover agreement from one kernel (Agda) plus independent standpoints. #430 doesn't attempt that, so this issue stays open.
Generated by Claude Code
chore(ech05): regression fixture -> JCS; stage 6 first target; ECH-05…
chore(ech05): regression fixture → JCS, stage 6 first target, #431 ro…