|
| 1 | +-- SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +-- |
| 4 | +-- ParetoStrongMaximality.lean |
| 5 | +-- |
| 6 | +-- Closes the strong-maximality gap for **E10 / PO-12**. |
| 7 | +-- |
| 8 | +-- This file is intentionally separate from `ParetoMaximality.lean`: |
| 9 | +-- the main file holds the algebraic-property theorems (PO-1..PO-11 |
| 10 | +-- + descent groundwork PD-1, PD-2) that compile cleanly under any |
| 11 | +-- Lean 4 toolchain. This file holds the load-bearing PD-3 lemma |
| 12 | +-- + the well-founded-recursion descent argument for the headline |
| 13 | +-- `dominated_by_frontier_member` theorem. |
| 14 | +-- |
| 15 | +-- Both halves of the proof are *mathematically* settled. The |
| 16 | +-- formalisation here uses only core Lean 4 (no mathlib) — at the |
| 17 | +-- cost of hand-rolling `List.length_lt_of_strict_subset_of_nodup` |
| 18 | +-- as a 25-line auxiliary lemma. |
| 19 | +-- |
| 20 | +-- **Toolchain note**: written 2026-04-27 by Opus without local |
| 21 | +-- access to a Lean 4 toolchain. The 2026-05-11 lake-build agent |
| 22 | +-- (per `docs/handover/PHASE-3-PROMPT.md` / scheduled routine |
| 23 | +-- `trig_01Tm7zTxYEY7kmzBsu7P4nc9`) will be the first run that |
| 24 | +-- actually tries `lake build` on this file. Tactic fixups (rather |
| 25 | +-- than mathematical errors) are expected; the proof structure is |
| 26 | +-- the load-bearing artefact. |
| 27 | + |
| 28 | +import EchidnaPareto.ParetoMaximality |
| 29 | + |
| 30 | +namespace EchidnaPareto |
| 31 | + |
| 32 | +-- ========================================================================== |
| 33 | +-- Section 1: Auxiliary List lemma — strict subset + nodup ⇒ shorter |
| 34 | +-- ========================================================================== |
| 35 | + |
| 36 | +/-- For two `Nodup` lists `xs ⊆ ys` with a witness `w` showing |
| 37 | + `w ∈ ys ∧ w ∉ xs`, the length of `xs` is strictly less than the |
| 38 | + length of `ys`. |
| 39 | +
|
| 40 | + *Proof sketch.* Recurse on `ys`. If `ys = []`, the witness is |
| 41 | + impossible. If `ys = y :: ys'`: |
| 42 | +
|
| 43 | + - Case `w = y`: every element of `xs` is in `ys`; by `xs.Nodup` |
| 44 | + and the absence of `w = y` in `xs`, every element of `xs` is |
| 45 | + in `ys'`. Then `xs.length ≤ ys'.length < ys.length`. |
| 46 | + - Case `w ≠ y`: split `xs` on whether `y ∈ xs`. |
| 47 | + - `y ∈ xs`: drop `y` from both; recursive call on |
| 48 | + `xs.erase y` and `ys'` (both still `Nodup`, witness `w` |
| 49 | + still applies, subset still holds). Length bookkeeping |
| 50 | + gives the desired strict inequality. |
| 51 | + - `y ∉ xs`: every element of `xs` is in `ys'`; recurse with |
| 52 | + `ys'` and the same `xs`. -/ |
| 53 | +theorem List.length_lt_of_subset_with_witness {α : Type*} [DecidableEq α] |
| 54 | + (xs ys : List α) (h_xs_nodup : xs.Nodup) (h_ys_nodup : ys.Nodup) |
| 55 | + (h_subset : ∀ x ∈ xs, x ∈ ys) |
| 56 | + (w : α) (hw_in_ys : w ∈ ys) (hw_not_in_xs : w ∉ xs) : |
| 57 | + xs.length < ys.length := by |
| 58 | + induction ys generalizing xs with |
| 59 | + | nil => |
| 60 | + -- ys = []: hw_in_ys says w ∈ [], impossible. |
| 61 | + exact absurd hw_in_ys (List.not_mem_nil w) |
| 62 | + | cons y ys' ih => |
| 63 | + -- Use Nodup of (y :: ys') to get y ∉ ys' and ys'.Nodup |
| 64 | + have hy_not_in_ys' : y ∉ ys' := List.Nodup.not_mem h_ys_nodup |
| 65 | + have h_ys'_nodup : ys'.Nodup := List.Nodup.of_cons h_ys_nodup |
| 66 | + -- Case-split on y ∈ xs. |
| 67 | + by_cases hy_in_xs : y ∈ xs |
| 68 | + · -- y ∈ xs: shrink both lists. |
| 69 | + let xs' := xs.erase y |
| 70 | + have h_xs'_nodup : xs'.Nodup := List.Nodup.erase y h_xs_nodup |
| 71 | + have h_xs'_subset : ∀ x ∈ xs', x ∈ ys' := by |
| 72 | + intro x hx |
| 73 | + have hx_in_xs : x ∈ xs := List.mem_of_mem_erase hx |
| 74 | + have hx_ne_y : x ≠ y := by |
| 75 | + intro heq |
| 76 | + rw [heq] at hx |
| 77 | + exact (List.Nodup.not_mem_erase h_xs_nodup) hx |
| 78 | + have hx_in_yys' : x ∈ y :: ys' := h_subset x hx_in_xs |
| 79 | + rcases List.mem_cons.mp hx_in_yys' with h | h |
| 80 | + · exact absurd h hx_ne_y |
| 81 | + · exact h |
| 82 | + -- Witness: w is still in ys' (we know w ≠ y because hw_not_in_xs vs hy_in_xs) |
| 83 | + have hw_ne_y : w ≠ y := by |
| 84 | + intro heq; rw [heq] at hw_not_in_xs; exact hw_not_in_xs hy_in_xs |
| 85 | + have hw_in_ys' : w ∈ ys' := by |
| 86 | + rcases List.mem_cons.mp hw_in_ys with h | h |
| 87 | + · exact absurd h hw_ne_y |
| 88 | + · exact h |
| 89 | + have hw_not_in_xs' : w ∉ xs' := by |
| 90 | + intro h |
| 91 | + exact hw_not_in_xs (List.mem_of_mem_erase h) |
| 92 | + -- Recursive call |
| 93 | + have ih_app : xs'.length < ys'.length := |
| 94 | + ih xs' h_xs'_nodup h_ys'_nodup h_xs'_subset w hw_in_ys' hw_not_in_xs' |
| 95 | + -- xs.length = xs'.length + 1 (since y ∈ xs and xs.Nodup) |
| 96 | + have h_xs_len : xs.length = xs'.length + 1 := |
| 97 | + List.length_erase_of_mem hy_in_xs |>.symm ▸ by simp [xs']; omega |
| 98 | + -- ys.length = ys'.length + 1 |
| 99 | + have h_ys_len : (y :: ys').length = ys'.length + 1 := by |
| 100 | + simp [List.length_cons] |
| 101 | + rw [h_xs_len, h_ys_len] |
| 102 | + omega |
| 103 | + · -- y ∉ xs: xs is fully a sublist of ys'. |
| 104 | + have h_xs_subset_ys' : ∀ x ∈ xs, x ∈ ys' := by |
| 105 | + intro x hx |
| 106 | + have hx_in_yys' : x ∈ y :: ys' := h_subset x hx |
| 107 | + have hx_ne_y : x ≠ y := fun heq => hy_in_xs (heq ▸ hx) |
| 108 | + rcases List.mem_cons.mp hx_in_yys' with h | h |
| 109 | + · exact absurd h hx_ne_y |
| 110 | + · exact h |
| 111 | + -- Decide: is the witness w in ys'? |
| 112 | + have hw_ne_y_or : w = y ∨ w ≠ y := Decidable.em _ |
| 113 | + rcases hw_ne_y_or with hw_eq_y | hw_ne_y |
| 114 | + · -- w = y: subset xs ⊆ ys' is the strict-shorter proof since |
| 115 | + -- y ∈ ys but y ∉ xs and y ∉ ys'. |
| 116 | + have h_xs_le_ys' : xs.length ≤ ys'.length := |
| 117 | + List.Sublist.length_le |
| 118 | + (List.sublist_of_subset_of_nodup h_xs_subset_ys' h_xs_nodup h_ys'_nodup) |
| 119 | + have : (y :: ys').length = ys'.length + 1 := by simp [List.length_cons] |
| 120 | + rw [this] |
| 121 | + omega |
| 122 | + · -- w ≠ y: recurse on ys'. |
| 123 | + have hw_in_ys' : w ∈ ys' := by |
| 124 | + rcases List.mem_cons.mp hw_in_ys with h | h |
| 125 | + · exact absurd h hw_ne_y |
| 126 | + · exact h |
| 127 | + have ih_app : xs.length < ys'.length := |
| 128 | + ih xs h_xs_nodup h_ys'_nodup h_xs_subset_ys' w hw_in_ys' hw_not_in_xs |
| 129 | + have : (y :: ys').length = ys'.length + 1 := by simp [List.length_cons] |
| 130 | + rw [this] |
| 131 | + omega |
| 132 | + |
| 133 | +-- ========================================================================== |
| 134 | +-- Section 2: PD-3 — domCount strictly decreases along dominator edges |
| 135 | +-- ========================================================================== |
| 136 | + |
| 137 | +/-- **PD-3 (E10/PD-3)** When `b ∈ cs` dominates `a`, the descent |
| 138 | + measure `domCount` strictly decreases: |
| 139 | +
|
| 140 | + `domCount b cs < domCount a cs`. |
| 141 | +
|
| 142 | + Proof: PD-1 gives `domSet b cs ⊆ domSet a cs`; PD-2 supplies |
| 143 | + `b ∈ domSet a cs ∧ b ∉ domSet b cs` as the strict-difference |
| 144 | + witness; `List.length_lt_of_subset_with_witness` (above) |
| 145 | + closes the cardinality argument provided both filtered lists |
| 146 | + are `Nodup`. |
| 147 | +
|
| 148 | + Filtered lists inherit `Nodup` from the original — but we have |
| 149 | + no hypothesis that `cs.Nodup`. In practice, `compute` in the |
| 150 | + Rust pareto module operates on indices `0..n`, which are |
| 151 | + trivially `Nodup`; the Lean spec carries this assumption as a |
| 152 | + side condition. -/ |
| 153 | +theorem domCount_strictly_decreases (a b : ProofObjective) |
| 154 | + (cs : List ProofObjective) (hcs_nodup : cs.Nodup) |
| 155 | + (hba : dominates b a) (hb_mem : b ∈ cs) : |
| 156 | + domCount b cs < domCount a cs := by |
| 157 | + unfold domCount |
| 158 | + apply List.length_lt_of_subset_with_witness |
| 159 | + (domSet b cs) (domSet a cs) |
| 160 | + · -- (domSet b cs).Nodup follows from cs.Nodup via filter preservation |
| 161 | + exact List.Nodup.filter _ hcs_nodup |
| 162 | + · exact List.Nodup.filter _ hcs_nodup |
| 163 | + · exact domSet_subset_of_dominates a b cs hba |
| 164 | + · exact b |
| 165 | + · exact (domSet_strict_witness a b cs hba hb_mem).1 |
| 166 | + · exact (domSet_strict_witness a b cs hba hb_mem).2 |
| 167 | + |
| 168 | +-- ========================================================================== |
| 169 | +-- Section 3: Strong maximality via well-founded recursion |
| 170 | +-- ========================================================================== |
| 171 | + |
| 172 | +/-- **PO-12 (E10/12) Strong maximality**: every input candidate not |
| 173 | + on the frontier is strictly dominated by some *frontier* |
| 174 | + member. This is the constructive content of "the Pareto |
| 175 | + frontier covers the input under dominance". |
| 176 | +
|
| 177 | + *Proof.* Strong induction on the descent measure `domCount a cs`, |
| 178 | + using `domCount_strictly_decreases` (PD-3) to feed the recursion. |
| 179 | + Termination is guaranteed by PD-3: each step strictly decreases |
| 180 | + `domCount`, so the chain bottoms out at a Pareto member. -/ |
| 181 | +theorem dominated_by_frontier_member (cs : List ProofObjective) |
| 182 | + (hcs_nodup : cs.Nodup) : |
| 183 | + ∀ a ∈ cs, a ∉ frontier cs → ∃ f ∈ frontier cs, dominates f a := by |
| 184 | + -- Strong induction on `domCount a cs`. |
| 185 | + intro a |
| 186 | + induction hk : domCount a cs using Nat.strong_induction_on with |
| 187 | + | _ k ih => |
| 188 | + intro ha hnf |
| 189 | + -- a is not Pareto, so some b ∈ cs dominates a. |
| 190 | + rcases frontier_or_dominated cs a ha with hf | ⟨b, hb_mem, hb_dom⟩ |
| 191 | + · exact absurd hf hnf |
| 192 | + -- Either b is Pareto (done) or recurse on b with smaller domCount. |
| 193 | + by_cases hp : isPareto b cs |
| 194 | + · exact ⟨b, frontier_complete cs b hb_mem hp, hb_dom⟩ |
| 195 | + · -- Recurse: domCount b cs < domCount a cs by PD-3. |
| 196 | + have hdec : domCount b cs < k := by |
| 197 | + rw [← hk] |
| 198 | + exact domCount_strictly_decreases a b cs hcs_nodup hb_dom hb_mem |
| 199 | + have hb_not_front : b ∉ frontier cs := by |
| 200 | + intro hb_in_front |
| 201 | + exact hp (frontier_sound cs b hb_in_front) |
| 202 | + obtain ⟨f, hf_front, hf_dom_b⟩ := |
| 203 | + ih (domCount b cs) hdec b rfl hb_mem hb_not_front |
| 204 | + -- f dominates b, b dominates a → f dominates a (transitivity) |
| 205 | + exact ⟨f, hf_front, dominates_transitive f b a hf_dom_b hb_dom⟩ |
| 206 | + |
| 207 | +end EchidnaPareto |
0 commit comments