verification/proofs/lean4: discharge E10/E11/E13 lake build

[hyperpolymath]

Context

verification/proofs/lean4/ now has a lakefile.lean + lean-toolchain (v4.13.0) scaffolded on 2026-05-11 by the lake-build agent. Three mechanical fixes were applied at the same time:

1. ParetoStrongMaximality.lean — wrong import path EchidnaPareto.ParetoMaximality → ParetoMaximality (flat-file layout; Lake maps module names to paths).
2. IntegrityVerification.lean — integrityToBool body was s = IntegrityStatus.verified (a Prop) where Bool is expected; fixed to decide (s = IntegrityStatus.verified).
3. ConfidenceLattice.lean — 10 level-distinctness theorems used omega on inductive-type constructor inequality (not reachable by linear arithmetic); changed to decide.

lake was not available in the build environment, so no actual build was run. This issue tracks the remaining items identified by static analysis that require a live Lean 4.13.0 toolchain to resolve.

---

Punch list (static analysis — unverified without running lake build)

A. ParetoStrongMaximality.lean — multiple List.Nodup API calls

The file was written without local Lean access (2026-04-27); several Lean 4.13.0 List lemma names are uncertain. Expected failures and candidate fixes:

Call site (approx line)	Suspect call	Likely fix
~60	List.Nodup.not_mem h_ys_nodup	(List.nodup_cons.mp h_ys_nodup).1
~62	List.Nodup.of_cons h_ys_nodup	(List.nodup_cons.mp h_ys_nodup).2 or h_ys_nodup.tail
~80	List.Nodup.not_mem_erase h_xs_nodup	No such lemma — replace with fun h => hw_not_in_xs (List.mem_of_mem_erase h) or similar
~74	List.Nodup.erase y h_xs_nodup	May be List.nodup_erase_of_nodup _ h_xs_nodup
~75	List.mem_of_mem_erase hx	Should be stable in Lean 4.13.0; verify
~113	List.sublist_of_subset_of_nodup	This lemma may not exist in core Lean; may need List.Sublist + List.nodup_iff_injOn hand-roll or List.Nodup.sublist_iff
~114	List.Sublist.length_le	Likely List.Sublist.length_le — check exact capitalization
~81	`List.length_erase_of_mem hy_in_xs	>.symm ▸ by simp [xs']; omega`

B. ParetoStrongMaximality.lean — Nat.strong_induction_on tactic syntax

induction hk : domCount a cs using Nat.strong_induction_on with
| _ k ih =>

In Lean 4.13.0 this syntax may not match Nat.strong_induction_on's recursor shape. Alternative:

-- Option 1: use Nat.strongRecOn
induction h : domCount a cs using Nat.strongRecOn with
| _ k ih => ...

-- Option 2: apply strong_induction_on directly
apply Nat.strong_induction_on (domCount a cs)
intro k ih ...

C. ConfidenceLattice.lean — unfold_let instLE / unfold_let instLT

unfold_let unfolds local let-bindings in the tactic context; instLE / instLT are global instance definitions and are not local lets. These calls may silently succeed (if Lean inlines the instance at elaboration) or fail with "not found".

Candidate fix if failing:

-- replace: unfold_let instLE; simp [LE.le, le]
-- with:
simp only [LE.le, TrustLevel.le]

Affects: le_refl, le_antisymm, le_trans, le_total, meet_le_left, le_join_right, level1_le_all, all_le_level5, level1_lt_level2–level4_lt_level5.

D. PortfolioCompleteness.lean — List.filter_eq_nil_iff

apply List.filter_eq_nil_iff.mpr

Lean 4 core (no Mathlib) may spell this List.filter_eq_nil or require List.filter_congr + List.filter_false. Check with #check @List.filter_eq_nil in the live toolchain.

E. PortfolioCompleteness.lean — Option.some_injective

have := Option.some_injective _ heq

In Lean 4.13.0 this is Option.some.inj heq (a field access on the some.injEq simp lemma). One-line fix: exact Option.some.inj heq.

F. PortfolioCompleteness.lean — PR-14 (unanimous_yields_crosschecked)

The proof author self-noted (line 459–463):

If lake build rejects the current tactic structure, the unfold reconcile step may need to be replaced with a hand-rolled show clause that pre-computes firstVerdict outside the match.

The simp only [hfv, hfilter, List.map_nil, List.isEmpty_nil] step after rw [hc] may fail because the inner let firstVerdict := first.verified.getD false in reconcile is not automatically simplified. Fix: add simp only [List.getD, Option.some_getD] or use show to fully instantiate the goal before simp.

G. IntegrityVerification.lean — match hf : file, hh : entry.hash with in tactic mode

match hf : file, hh : entry.hash with
| FileResult.notFound, _ => ...

Simultaneous named multi-subject match in tactic mode may not be supported in Lean 4.13.0. If it fails, split into sequential rcases/cases with explicit equation naming.

---

Not in scope

• Mathlib dependency: PO-12 strong-maximality in ParetoStrongMaximality.lean uses only core Lean (hand-rolled List.length_lt_of_subset_with_witness). Do NOT add mathlib to resolve the API issues above — the hand-rolled auxiliary lemma is the chosen approach. Only add mathlib if the hand-rolled proof is fundamentally broken (not just API-name issues).
• PO-12 tracking: ECHIDNA-PARETO-DESCENT is a separate ticket for the mathematical content of PO-12. This issue is purely about tactic/API fixups.

---

Acceptance criteria

lake build exits 0 with EchidnaTrustProofs as the default target, covering all 5 .lean files. Update PROOF-NEEDS.md with per-theorem pass/fail once a live build is available.