roadmap: Proof caching & incremental verification (v1.0.0 long-term)

[hyperpolymath]

Origin

ROADMAP.adoc §"Long-Term Goals (v1.0.0 -- Q3-Q4 2026)", "Proof Caching and Incremental Verification" (lines 143-147):

=== Proof Caching and Incremental Verification

• Cache verified proofs (skip re-verification if unchanged)
• Incremental verification (only changed theorems + dependents)
• Proof dependency tracking

Scope

Three bullets, one tracker. Per the long-tail roadmap enumeration this is a v1.0 long-term commitment (Q3-Q4 2026):

1. Proof cache: hash-key on (theorem_id, prover, prover_version, dependency_hashes); cache hit skips re-verification
2. Incremental verification: a dependency-graph walker that finds the closure of changed theorems and re-verifies only that set
3. Dependency tracking: per-theorem dependency manifest extracted from each prover backend (Coq .vo deps, Lean olean deps, Isabelle theory imports, etc.)

PR count not estimated in roadmap; rough order: ~6-10 PRs (cache layer + per-backend dep extractor + graph walker + tests).

Dependencies

• Echidnabot v0.2.0 production hardening should land first (OpenTelemetry tracing, structured logging, graceful shutdown — ROADMAP.adoc:124-127) so cache-hit/miss events are observable
• No upstream blocker

Why filed

To make the v1.0 "Proof Caching and Incremental Verification" commitment trackable. Today the three bullets live only as a checklist in ROADMAP.adoc with no issue, no milestone, no owner. Caching is the highest-value of the three v1.0 long-term tracks because it directly affects PR latency on every echidnabot deploy.