feat(proofs): Evidence Mode foundations — Agda library + golden vectors (#7)

[arena-ai-coding-agent]

Summary

First slice of #7 (Full Evidence Mode): the formal foundations. What a residual, an evidence-refined candidate set, a warrant token and a presence verdict are — proved, executable inside Agda, and pinned across implementations.

The reference explorer's own footer admits its signed JavaScript model has no proved extraction correspondence with any proof. This PR closes exactly that gap:

• L0 — abstract semantics (Evidence.Residual, Echo, Warrant): Candidate observe r E = Σ W ((observe w ≡ r) × E w); Holds quantifies over all candidates, not the case's chosen witness; actual-world-sound is the honesty boundary (a warranted claim about candidates says nothing about reality until the actual world is shown admissible); Echo/AvecFibre fibre semantics with the total-space factorisation (the licence for storing rows as (observed, witnesses) pairs); Warrant/Epi/SoundWarrant with epi-does-not-give — a warrant token is not truth, proved by countermodel.
• L1 — signed finite model (Evidence.Signed): signed-integer-v1 as ℕ offsets, so every predicate is decidable and the model runs inside Agda; enumeration proved sound (listed ⇒ satisfies) and complete (satisfies ∧ b ≤ 6 ⇒ listed).
• L2 — decision procedures (Evidence.Decision): the exact computation the server routes and the residual explorer run, proved to decide the candidate semantics: entailed ⇒ Present holds; refuted ⇒ Absent holds; unresolved ⇒ neither (explicit witnesses both ways); inconsistent ⇒ no inhabited case — an empty candidate set does not make claims vacuously true. The five reference presets land as computed, proved terms (e.g. present-without-identification: presence without a value).
• L3 — the pin: 546 golden vectors (proofs/vectors/evidence_vectors.json, regenerate with scripts/gen_evidence_vectors.py) covering all four verdicts and both identification outcomes, for Julia and bun test stacks to consume so Agda/Julia/TS are bound to one truth.

Negative control: reject/IdentificationWithoutUniqueness.agda — reporting an identified value from a mere presence verdict (the UI bug Evidence Mode exists to prevent) must fail to type-check, and does.

Changes

• proofs/agda/MetaManifold/Evidence/ — six new stdlib-free modules (only Agda.Builtin.*, so they check under any Agda ≥ 2.6.4.3)
• proofs/agda/MetaManifold/All.agda, proofs/agda/README.md — suite integration
• proofs/agda/reject/IdentificationWithoutUniqueness.agda — new negative control
• scripts/gen_evidence_vectors.py + proofs/vectors/evidence_vectors.json — the golden-vector pin
• docs/formal/evidence-verification.md — layering, verdict theorems, theorem-to-test map, and what is deliberately not proved

Verification

• All six modules type-check clean (exit 0, no errors) under Agda 2.7.0.1, --safe --without-K.
• check-proofs.sh guard logic replicated locally on all 17 modules: no postulates/holes/escape flags; pragma present.
• Reject control fails with the error its -- EXPECT: line states.
• scripts/check-spdx.sh: OK (327 files).
• Vectors regenerate byte-identically (546 cases).
• The full All.agda suite check runs in CI under the estate pin (Agda 2.6.4.3 + stdlib 2.1); the Evidence half is stdlib-free by construction, so toolchain drift cannot affect it.

Scope note

The UI layer of #7 (avec_fibre editor, fibre visualizer, residual explorer, warrant editor, provenance logging, DANGER banner) follows in later stacks on top of these foundations. Refs #7.

Note on CI

File-based workflows have been failing repo-wide with startup_failure since 2026-09-25 (diagnosed in #76 as settings/platform-side). If checks show that, it is unrelated to this change.

[coderabbitai]

Important

Review skipped

Bot user detected.

To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 93389df1-e9ed-4790-824f-51ad1063e46c

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}