docs: sync Lean-side Priority 17 bridge provenance contract

README.md

@@ -4,6 +4,22 @@ External **Lean 4** proof backend for the [mumei](https://github.com/mumei-lang/
 
 For P9-G NLAE integration, mumei-lean is the Fidelity Checker: it confirms that reconstructed `.mm` obligations can become `lean_verified` certificates, including live generated theorem paths.
 
+## Distributed proof bundle verification
+
+mumei release bundles expose per-module certificates and a bundle-level
+`lean_provenance` index. Consumers use `artifact_paths` to locate each
+certificate and source, confirm `z3_check_result: "lean_verified"` together
+with the current `translator_version`, `bridge_lemma_hash`, and
+`manual_lemma_reason`, and re-run:
+
+```bash
+mumei verify-cert <certificate> <source> --strict
+```
+
+Use `--allow-lean-verified` explicitly on mumei acceptance paths that permit
+Lean results. A translator or bridge-lemma mismatch is `stale_translator`, not
+a successful proof.
+
 ## Unknown obligation bridge contract
 
 The promoted path is: select Z3 `unknown` atoms, translate them with typed metadata, build generated Lean, export a certificate with `translator_version` and `bridge_lemma_hash`, and let mumei accept only matching `lean_verified` results. Eight live theorem paths are covered: `abs_saturating`, `bounded_mul_with_overflow_check`, `constant_time_eq_flag`, `ff_zero_eq_zero`, `verified_insertion_sort_ascending`, `poly_bound_monotone`, `exists_pivot_partition`, and `sum_nonneg_inductive`. See [`docs/LEAN_HARNESS_CONTRACT.md`](docs/LEAN_HARNESS_CONTRACT.md) for per-path details.

docs/BRIDGE_HARNESS_SPEC.md

@@ -11,6 +11,18 @@ For the artifact-level contract covering `.proof-cert.json`, generated Lean,
 
 Vocabulary is inherited from the cross-project roadmap: `harness_contract`, `intent_fidelity`, `artifact_paths`, `budget_policy_fingerprint`, and `lean_verified` are the only canonical field names.
 
+## Distributed bundle verification
+
+Consumers of a distributed `std-proof-bundle.json` should use its
+`artifact_paths` to locate the packaged per-module certificate and source, then
+check the corresponding `lean_provenance` entry. Promotion requires
+`z3_check_result == "lean_verified"` plus matching `translator_version` and
+`bridge_lemma_hash`; `manual_lemma_reason` must be inspected and must not hide an
+unresolved manual obligation. Re-run the packaged certificate with
+`mumei verify-cert <certificate> <source> --strict`. Where the mumei acceptance
+path allows Lean results, add `--allow-lean-verified` explicitly. Any metadata
+mismatch remains `stale_translator` and is not proven.
+
 
 ## Unknown obligation bridge contract
 

docs/LEAN_HARNESS_CONTRACT.md

@@ -8,6 +8,23 @@ contract that callers can use to validate inputs, generated Lean, `lake build`,
 
 The cross-project roadmap is the sole upper roadmap. This contract uses the canonical field names `harness_contract`, `intent_fidelity`, `artifact_paths`, `budget_policy_fingerprint`, and `lean_verified` without aliases. The docs-sync and code-surface contract is pinned by `tests/test_contract_vocabulary.py` so `lean_verified`, `stale_translator`, `translator_version`, and `bridge_lemma_hash` do not drift. The test covers docs text, Python bridge code constants (`scripts/export_cert.py` `TRANSLATOR_VERSION` / `BRIDGE_LEMMA_HASH` ↔ document pinned values), and code-surface alias drift in docstrings, argparse help, and user-visible output strings across `scripts/export_cert.py`, `scripts/bridge.py`, `scripts/ingest_cert.py`, and `scripts/bridge_harness.py`.
 
+## Distributed bundle consumer procedure
+
+When consuming a distributed proof bundle, use `artifact_paths` to locate the
+per-module certificate and source, then select the module and atom from
+`lean_provenance`. Confirm `z3_check_result == "lean_verified"` and verify the
+entry's `translator_version`, `bridge_lemma_hash`, and `manual_lemma_reason`.
+Re-run the packaged certificate with:
+
+```bash
+mumei verify-cert <certificate> <source> --strict
+```
+
+If the mumei acceptance path is configured to accept Lean-proved atoms, pass
+`--allow-lean-verified` explicitly as well. The certificate and provenance must
+agree with the current translator contract; otherwise the result is
+`stale_translator` and must remain unproven.
+
 
 ## Unknown obligation bridge contract
 

docs/ROADMAP.md

@@ -6,6 +6,23 @@
 
 Promotion to `lean_verified` requires a successful Lean build plus matching `translator_version` and `bridge_lemma_hash` in both the exported atom and `lean_result_metadata`; mismatches are `stale_translator`. PRs that update this roadmap should review the cross-project roadmap in the same diff and record relevant bridge regression commands from `tests/`.
 
+### Priority 17 bridge surface
+
+The mumei `docs/CROSS_PROJECT_ROADMAP.md` is canonical for the cross-project
+Priority 17 contract. This local checkpoint records only the Lean-relevant
+surface: distributed proof bundles expose `lean_provenance` entries whose
+`z3_check_result` is `"lean_verified"` together with `translator_version`,
+`bridge_lemma_hash`, and `manual_lemma_reason`. Consumers must preserve
+`stale_translator` as the signal for translator or bridge-lemma drift.
+
+For a distributed bundle, locate the referenced certificate using its
+`artifact_paths`, inspect the matching `lean_provenance` entry, and confirm the
+atom has `z3_check_result == "lean_verified"`, current `translator_version` and
+`bridge_lemma_hash`, and an understood `manual_lemma_reason`. Re-run
+`mumei verify-cert <certificate> <source> --strict`; on a mumei acceptance path
+that permits Lean results, pass `--allow-lean-verified` explicitly. A mismatch
+remains `stale_translator` and is not promoted.
+
 Run the local contract vocabulary gate before opening a PR that touches `README.md`, `docs/LEAN_HARNESS_CONTRACT.md`, `docs/INTEGRATION.md`, or the bridge scripts:
 
 ```bash