R5 — spec v1.1 delta and the R-series roadmap

Spec v1.1 delta consolidated by reference (delta.md §7: as-built table, six D6 demotions with reconsideration conditions) plus the R-series roadmap (spec/roadmap-v1.1.md). Docs-only; no behavior change.

R4 — the VerInf demo

Proof Broker closes 19/19 targeted Lean obligations in a real downstream consumer — VerInf's softmax-bracket spike, statements untouched. External search (cvc4 / cvc5 / z3), every certificate checked before Lean accepts the result, everything within the sanctioned axiom ceiling.

Evidence and generated tables: proof-broker-demo · write-up · decision records: delta.md §5.7.