Doc cleanup: dead-code item is closed, archive Phase 4C Lean docs

Closes the "dead code" leg of audit-2026-04-04 residuals (item 10c
of CRG-AUDIT-2026-04-18). Investigation found:

  * `lean_ffi.rs` and `daemon_client.rs` were removed from
    `impl/rust-cli/src/` on 2026-02-12 in commit `5802dc9` (the Opus
    deep-audit session) — well before either audit. The 2026-04-04 and
    2026-04-18 audits both carried the stale "remove dead code"
    finding.

  * Confirmed via `find` (zero matches) and `git log --diff-filter=D`
    (single deletion commit). Only stale references remain in
    documentation.

Updates in this commit:

  * `CLAUDE.md` High Priority section: "Dead code" bullet removed; the
    remaining 47-spoofed-author and Echidna-CI items renumber. Note
    block points readers at this commit + the archived Phase 4C docs.

  * `ROADMAP.adoc` v0.9.x audit-residuals item: split into three
    sub-items so the dead-code leg can be marked closed independently.
    47-author re-write left open with explicit human-authorization
    gate (history rewrite + force-push).

  * `impl/rust-cli/docs/PHASE4C_LEAN_EXTRACTION.md` and
    `impl/rust-cli/docs/LEAN_EXTRACTION_BUILD_GUIDE.md`: archive
    banners added to the top. Phase 4C described a Lean→C→Rust
    extraction pipeline whose Rust endpoint (`lean_ffi.rs`) was
    removed because the underlying extracted-C library was never
    produced. Status lines updated to "(archived 2026-04-19)" so future
    readers don't act on the misleading "✅ COMPLETE" claim.

Not touched: the `daemon_client.zig` import in `impl/zig/src/main.zig`
is a live Zig file (different from the deleted Rust `daemon_client.rs`)
and stays. Historical audit docs (`audit-2026-04-04.md`,
`CRG-AUDIT-2026-04-18.adoc`) are not rewritten — they accurately
recorded the state at audit time.

Audit closure scoreboard now: 7 of 10 items closed (1, 2, 4, 5, 7, 9,
plus 10c). Remaining: 3 (READMEs XL), 6 (verify-proofs CI), 8
(contractile six-verb), 10a (47 authors, needs auth), 10b (Echidna CI).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

CLAUDE.md

@@ -91,8 +91,12 @@ The Rust CLI is a functional interactive shell with these features:
 ### High Priority
 
 1. **47/58 commits authored as `Test <test@example.com>`** (Sonnet damage)
-2. **Dead code**: `lean_ffi.rs` (library doesn't exist), `daemon_client.rs` (no daemon)
-3. **No Echidna integration** for automated verification
+2. **No Echidna integration** for automated verification
+
+_Note: the prior "Dead code" bullet (`lean_ffi.rs`, `daemon_client.rs`)
+is closed — both files were removed in commit `5802dc9` (2026-02-12
+deep-audit session). The corresponding Phase 4C design docs under
+`impl/rust-cli/docs/` carry archival banners pointing here._
 
 ### Medium Priority
 

ROADMAP.adoc

@@ -47,9 +47,16 @@ CI on `rust-cli.yml`, dogfood evidence, structural compliance.
   former `lust/`, already removed in commit `a48a1dc`), `adjust/`;
   relocate `k9` out of `contractiles/` per ADR-001 (k9 is svc, not a
   contractile).
-* [ ] Close `docs/reports/audit/audit-2026-04-04.md` residuals: re-author
-  47 spoofed git commits, wire Echidna CI, remove dead code
-  (`lean_ffi.rs`, `daemon_client.rs`).
+* [~] Close `docs/reports/audit/audit-2026-04-04.md` residuals:
+** [ ] Re-author 47 spoofed git commits (`Test <test@example.com>` →
+   canonical attribution). Requires history rewrite + force-push;
+   needs explicit human authorization before execution.
+** [ ] Wire Echidna CI integration for automated property-based
+   verification.
+** [x] Remove dead code (`lean_ffi.rs`, `daemon_client.rs`) — closed
+   2026-02-12 in commit `5802dc9` (predates the 2026-04-18 audit; the
+   audit's residual claim was stale). Phase 4C design docs under
+   `impl/rust-cli/docs/` carry archival banners noting the removal.
 
 == v0.10.x — POSIX Coverage
 

impl/rust-cli/docs/LEAN_EXTRACTION_BUILD_GUIDE.md

@@ -1,8 +1,15 @@
 # Lean 4 Extraction Pipeline - Build Guide
 
+> **⚠️ ARCHIVED 2026-04-19** — companion to `PHASE4C_LEAN_EXTRACTION.md`,
+> which describes the Lean→C→Rust pipeline whose Rust endpoint
+> (`impl/rust-cli/src/lean_ffi.rs`) was removed as dead code in commit
+> `5802dc9` (2026-02-12). The build steps below remain accurate as a
+> Lean-extraction reference but no longer terminate at a live Rust
+> consumer in this repo.
+
 **Version**: 0.15.0
 **Date**: 2026-01-29
-**Status**: Ready for compilation and testing
+**Status**: Ready for compilation and testing _(archived 2026-04-19)_
 
 ---
 

impl/rust-cli/docs/PHASE4C_LEAN_EXTRACTION.md

@@ -1,8 +1,15 @@
 # Phase 4C: Lean Extraction Pipeline
 
+> **⚠️ ARCHIVED 2026-04-19** — describes the Phase 4C design where
+> `impl/rust-cli/src/lean_ffi.rs` (170 LOC) bridged extracted Lean 4 C
+> code into the Rust shell. `lean_ffi.rs` was removed as dead code in
+> commit `5802dc9` (2026-02-12 deep-audit session) because the underlying
+> extracted-C library was never produced. This document is retained for
+> design history; do NOT treat its "Status: ✅ COMPLETE" as current.
+
 **Version**: 0.15.0
 **Date**: 2026-01-29
-**Status**: ✅ COMPLETE
+**Status**: ✅ COMPLETE _(at the time; archived as dead-feature 2026-04-19)_
 **Integration**: Optional runtime verification via feature flag
 
 ---