docs: sync Lean-side Priority 17 bridge provenance contract

[AkiraTamai]

Summary

Lean-side half of canonical Priority 17 (implemented in mumei-lang/mumei#497). Documentation only — no bridge code, no vocabulary, and no existing implementation status changed.

mumei releases and Homebrew now ship per-module proof certificates plus a std-proof-bundle.json whose lean_provenance index carries translator_version, bridge_lemma_hash, and manual_lemma_reason per Lean-proved atom. That makes provenance checkable from a distribution alone, so this repo's consumer-facing docs need to say how:

• docs/ROADMAP.md — new "Priority 17 bridge surface" checkpoint, explicitly subordinate to mumei docs/CROSS_PROJECT_ROADMAP.md as the sole upper roadmap.
• docs/BRIDGE_HARNESS_SPEC.md, docs/LEAN_HARNESS_CONTRACT.md, README.md — the distributed-bundle consumer procedure: locate certificate and source via artifact_paths, read the matching lean_provenance entry, require z3_check_result == "lean_verified" with current translator_version / bridge_lemma_hash and an understood manual_lemma_reason, then re-run mumei verify-cert <certificate> <source> --strict (adding --allow-lean-verified on acceptance paths that permit Lean results).

The key point every added section repeats: a translator or bridge-lemma mismatch stays stale_translator and is not a proof. lean_verified / stale_translator / translator_version / bridge_lemma_hash are reflected as-is, never aliased.

Verification

PYTHONPATH=scripts MUMEI_LEAN_SKIP_LIVE=1 python -m pytest tests/test_contract_vocabulary.py -q   # 6 passed
PYTHONPATH=scripts MUMEI_LEAN_SKIP_LIVE=1 python -m pytest tests -q                              # 131 passed (offline bridge suite)

Link to Devin session: https://app.devin.ai/sessions/0f87f38914874eedbc48c92f3b941354
Requested by: @AkiraTamai

[devin-ai-integration]

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

• Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
• Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

• Disable automatic comment, CI, and merge conflict monitoring

[devin-ai-integration]

✅ Devin Review: No Issues Found

Devin Review analyzed this PR and found no bugs or issues to report.