feat(lean4): scaffold EchidnaTrustProofs lakefile + apply mechanical build fixes; update PROOF-NEEDS.md

Adds verification/proofs/lean4/lakefile.lean and lean-toolchain
(leanprover/lean4:v4.13.0, no mathlib) so E10/E11/E13 proof files
can be built with `lake build`. Library name: EchidnaTrustProofs.
Roots: ConfidenceLattice, IntegrityVerification, ParetoMaximality,
ParetoStrongMaximality, PortfolioCompleteness.

Three mechanical fixes identified by static analysis:

1. ParetoStrongMaximality.lean: wrong import path
   EchidnaPareto.ParetoMaximality → ParetoMaximality
   (Lake maps module names to flat file paths; no subdirectory exists).

2. IntegrityVerification.lean: integrityToBool body was a Prop where
   Bool is required; fixed to decide (s = IntegrityStatus.verified).

3. ConfidenceLattice.lean: 10 level-distinctness theorems used omega
   on inductive-type constructor inequality; changed to decide.

lake unavailable in 2026-05-11 build env — no actual build was run.
Remaining tactic/API fixups tracked in #53.

PROOF-NEEDS.md updated to reflect lakefile-scaffolded status for
E10/E11/E13 and point to #53 for open items.

https://claude.ai/code/session_01QoazAuafVkKFZnBkkQgGAH

Author: hyperpolymath

PROOF-NEEDS.md

@@ -8,7 +8,7 @@ scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-sp
 When this project needs formal ABI verification, create domain-specific Idris2 proofs
 following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`.
 
-## Current state (Updated 2026-04-26)
+## Current state (Updated 2026-05-11)
 
 ### Completed proofs
 
@@ -34,14 +34,14 @@ following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-s
 |---|------|--------|--------|
 | E1 | Confidence scoring lattice (TrustLevel forms valid partial order) | L4 | Covered by ConfidenceLattice.lean |
 | E8 | VQL-UT query safety (SEC, deeper layer) | I2 | Partially covered by VqlUt.idr |
-| E10 | Pareto frontier maximality | L4 | **Design landed 2026-04-27** (`verification/proofs/lean4/ParetoMaximality.lean` + `ParetoStrongMaximality.lean` + Creusot mirror at `crates/echidna-core-spark/src/pareto.rs`); 11/12 PO theorems closed in main file (PO-1..PO-11); PO-12 strong maximality staged in `ParetoStrongMaximality.lean` as: `List.length_lt_of_subset_with_witness` (auxiliary List lemma, hand-rolled core-Lean) → `domCount_strictly_decreases` (PD-3) → `dominated_by_frontier_member` (PO-12 via `Nat.strong_induction_on` on the descent measure). Proof structure complete; tactic-level fixups expected at first `lake build` (no Lean toolchain locally 2026-04-27 — agent `trig_01Tm7zTxYEY7kmzBsu7P4nc9` will catch). Adds `cs.Nodup` side-condition (cheap to satisfy from the indexed-list shape used by Rust `compute`). Tracking ticket: ECHIDNA-PARETO-DESCENT |
-| E11 | SHAKE3-512/BLAKE3 integrity | L4 | **Design landed 2026-04-27** (`verification/proofs/lean4/IntegrityVerification.lean`); 12 PI theorems including verifier soundness/completeness, status exhaustiveness, BLAKE3 cache freshness; collision-resistance theorems (PI-7, PI-9) state assumption explicitly as a typeclass per zero-axiom policy. NB: hash naming clarification — implementation is SHAKE-256 squeezing 512 bits, not "SHAKE3-512" |
-| E13 | Portfolio cross-checking completeness | L4 | **Design landed 2026-04-27** (`verification/proofs/lean4/PortfolioCompleteness.lean`); 14 PR theorems covering exhaustiveness, AllTimedOut iff no completed, CrossChecked agreement, Inconclusive disagreement detection, needs_review iff non-consensus, unanimity → CrossChecked |
+| E10 | Pareto frontier maximality | L4 | **Lakefile scaffolded 2026-05-11.** `verification/proofs/lean4/lakefile.lean` + `lean-toolchain` (v4.13.0) in place. PO-1..PO-11 (`ParetoMaximality.lean`) expected to compile cleanly — no imports, pure omega/decide arithmetic proofs. PO-12 (`ParetoStrongMaximality.lean`): import path fix applied (`EchidnaPareto.ParetoMaximality` → `ParetoMaximality`); 8 List.Nodup API calls + `Nat.strong_induction_on` tactic syntax flagged as uncertain without a live toolchain — tracked in #53. `lake build` not yet run (`lake` unavailable in 2026-05-11 env). Tracking ticket: ECHIDNA-PARETO-DESCENT (math); #53 (tactic fixups). |
+| E11 | SHAKE3-512/BLAKE3 integrity | L4 | **Lakefile scaffolded 2026-05-11.** 12 PI theorems (PI-1..PI-12) expected to compile cleanly after mechanical fix: `integrityToBool` body corrected from bare `Prop` expression to `decide (s = IntegrityStatus.verified)`. Collision-resistance typeclasses (PI-7, PI-9) remain assumptions per zero-axiom policy. `match hf : file, hh : entry.hash` simultaneous named tactic match in `verify_sound` flagged in #53 as uncertain. `lake build` not yet run. NB: hash naming — implementation is SHAKE-256 squeezing 512 bits. |
+| E13 | Portfolio cross-checking completeness | L4 | **Lakefile scaffolded 2026-05-11.** 14 PR theorems (PR-1..PR-14) expected to mostly compile. Flagged in #53: `List.filter_eq_nil_iff` name (PR-14 prerequisite), `Option.some_injective` → `Option.some.inj` (PR-10), PR-14 `simp` through inner `let firstVerdict` may need `show` pre-computation. `lake build` not yet run. |
 
 ## Recommended prover
 - **Idris2** for ABI-level properties and prover dispatch correctness
 - **Lean4** for algebraic properties of the confidence lattice
 - **Agda** for metatheoretic properties of proof composition
 
 ## Priority
-- **MEDIUM** (was HIGH) — Core trust pipeline proofs (E2-E6) are now complete. E10-E13 design + statements landed 2026-04-27; remaining work is `lake build` integration (no Lean toolchain pinned in `verification/proofs/lean4/`; the existing `proofs/lean/lakefile.lean` is for the playground, not these proofs). E10-E13 are P2 and do not block the critical path.
+- **MEDIUM** (was HIGH) — Core trust pipeline proofs (E2-E6) are now complete. E10-E13 design + statements landed 2026-04-27; `verification/proofs/lean4/lakefile.lean` scaffolded 2026-05-11 (Lean 4.13.0, no mathlib). Remaining work: run `lake build` in an environment with Lean 4.13.0 and apply the API fixups tracked in #53. E10-E13 are P2 and do not block the critical path.

verification/proofs/lean4/ConfidenceLattice.lean

@@ -356,16 +356,16 @@ theorem small_kernel_monotone (f : TrustFactors) :
 -- Section 6: Exhaustive level distinctness
 -- ==========================================================================
 
-theorem level1_ne_level2 : Level1 ≠ Level2 := by omega
-theorem level1_ne_level3 : Level1 ≠ Level3 := by omega
-theorem level1_ne_level4 : Level1 ≠ Level4 := by omega
-theorem level1_ne_level5 : Level1 ≠ Level5 := by omega
-theorem level2_ne_level3 : Level2 ≠ Level3 := by omega
-theorem level2_ne_level4 : Level2 ≠ Level4 := by omega
-theorem level2_ne_level5 : Level2 ≠ Level5 := by omega
-theorem level3_ne_level4 : Level3 ≠ Level4 := by omega
-theorem level3_ne_level5 : Level3 ≠ Level5 := by omega
-theorem level4_ne_level5 : Level4 ≠ Level5 := by omega
+theorem level1_ne_level2 : Level1 ≠ Level2 := by decide
+theorem level1_ne_level3 : Level1 ≠ Level3 := by decide
+theorem level1_ne_level4 : Level1 ≠ Level4 := by decide
+theorem level1_ne_level5 : Level1 ≠ Level5 := by decide
+theorem level2_ne_level3 : Level2 ≠ Level3 := by decide
+theorem level2_ne_level4 : Level2 ≠ Level4 := by decide
+theorem level2_ne_level5 : Level2 ≠ Level5 := by decide
+theorem level3_ne_level4 : Level3 ≠ Level4 := by decide
+theorem level3_ne_level5 : Level3 ≠ Level5 := by decide
+theorem level4_ne_level5 : Level4 ≠ Level5 := by decide
 
 -- ==========================================================================
 -- Section 7: Strict ordering chain

verification/proofs/lean4/IntegrityVerification.lean

@@ -364,7 +364,7 @@ theorem quickReverify_complete (e : Blake3CacheEntry) (current : ByteString)
     canonical mapping here so that downstream proofs can chain the
     integrity result into the trust-level computation. -/
 def integrityToBool (s : IntegrityStatus) : Bool :=
-  s = IntegrityStatus.verified
+  decide (s = IntegrityStatus.verified)
 
 /-- **PI-11 (E11/11) Trust gate**: `solver_integrity_ok` is `true` iff
     the verifier returns `verified`. -/

verification/proofs/lean4/ParetoStrongMaximality.lean

@@ -25,7 +25,7 @@
 -- than mathematical errors) are expected; the proof structure is
 -- the load-bearing artefact.
 
-import EchidnaPareto.ParetoMaximality
+import ParetoMaximality
 
 namespace EchidnaPareto
 

verification/proofs/lean4/lakefile.lean

@@ -0,0 +1,30 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- lakefile.lean — EchidnaTrustProofs
+--
+-- Builds the E-series verification proof obligations:
+--   E4  ConfidenceLattice.lean   (trust-level partial order + scoring)
+--   E10 ParetoMaximality.lean    (PO-1..PO-11 algebraic properties)
+--       ParetoStrongMaximality.lean  (PO-12 descent / strong maximality)
+--   E11 IntegrityVerification.lean  (SHAKE-256/512 + BLAKE3 verifier)
+--   E13 PortfolioCompleteness.lean  (portfolio cross-checking)
+--
+-- Toolchain: leanprover/lean4:v4.13.0 (pinned in lean-toolchain).
+-- No mathlib dependency — proofs use only core Lean 4.
+
+import Lake
+open Lake DSL
+
+package echidna_trust_proofs where
+  -- No external dependencies required.
+
+@[default_target]
+lean_lib EchidnaTrustProofs where
+  roots := #[
+    `ConfidenceLattice,
+    `IntegrityVerification,
+    `ParetoMaximality,
+    `ParetoStrongMaximality,
+    `PortfolioCompleteness
+  ]

verification/proofs/lean4/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.13.0