[FINDING] Kani evidence hygiene: 3 ERC-7730 Phase-D harnesses lack in-tree receipts; '173 active' overstates the enforced set by 3; map row 4 billing-outage claim stale

[Nicola-Ceornea]

Surface: fv · Severity: low (provenance/disclosure, not soundness) · Evidence: mixed (one harness executed green today) · Target: f91aa82

1. The claimed "individual verification of the three ERC-7730 Phase-D parameter harnesses (Kani 0.67.0)" has no receipt anywhere in-tree (names occur only in params.rs, the census lock, the mutation manifest). Mitigation: params_native_currency_list_canonicality re-ran SUCCESSFUL today; source read shows real biconditional assertions + positive controls. Fix: commit the receipt or drop the sentence.
2. per_record_page_bound, no_hidden_value, cow_presign_precedence are #[cfg(feature = "kani-heavy")] — nightly runs only make kani; make kani-heavy is local_documented. The census counts them "active"; map row 4's enforcement wording doesn't mention the carve-out (gate_enforcement.json does disclose it). Fix: one clause in row 4.
3. Map row 4 attributes suspended Kani CI to "the billing outage" — that ended 2026-07-29 (docs/STATUS.md:46); CI is now red/cancelled, not dark. Fix: re-date the row.

Found 2026-08-20 FV red-team.

[Nicola-Ceornea]

FIXED in working tree. Receipts recorded in REVIEW_PROVENANCE.md (new 'Executing receipts' section): the three Phase-D harnesses re-run SUCCESSFUL on cargo-kani 0.67.0 at HEAD, plus the #659/#662 remediation receipt. Map row 4 reworded (post-07-29 red-CI reality + kani-heavy 3/173 carve-out) — in FV_SURFACE_MAP.md:16.