[P1] echidna: ConfidenceLattice.lean E4-Lean half fails lake build (unfold_let removed)

[hyperpolymath]

Surfaced reconciling #126. verification/proofs/lean4/ConfidenceLattice.lean (386 LoC) fails lake build with ~49 errors: 30× unfold_let, removed in Lean 4.13.0. Mechanical token-swap to simp only [instLE]/unfold instLE tested → worse (104 errors); fix is non-mechanical. E4's I2 half (TrustLevelSoundness.idr) is constructive and stands; only the L4 half is unverified. This is genuine proof debt the #53/E-series narrative masked.

Sub-issue of #124. PRs Refs hyperpolymath/standards#124. Joint-close on agreement only.

🤖 Generated with Claude Code

[hyperpolymath]

Closing as already-resolved. Swarm verification (2026-05-18): ConfidenceLattice.lean is 301 LoC with zero unfold_let — the debt was already remediated by landed commit 8b357bf (echidna PR #71, 'discharge E-series proofs on Lean 4.13.0', Refs #53). Clean lake build (Lean 4.13.0, .lake/build removed) = all 7 targets/5 modules green, exit 0. No sorry/admit/native_decide. The #53 narrative had masked that #71 already fixed E4-Lean. Nothing to do.