diff --git a/.github/workflows/lean.yml b/.github/workflows/lean.yml new file mode 100644 index 0000000..55486d5 --- /dev/null +++ b/.github/workflows/lean.yml @@ -0,0 +1,53 @@ +name: Lean proofs + +on: + pull_request: + paths: + - 'formal/lean/**' + - 'src/**' + - 'docs/pruning-proof.md' + - 'docs/exactness-proof.md' + - '.github/workflows/lean.yml' + push: + branches: [main] + paths: + - 'formal/lean/**' + - 'src/**' + - 'docs/pruning-proof.md' + - 'docs/exactness-proof.md' + - '.github/workflows/lean.yml' + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: lean-${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + check-proofs: + runs-on: ubuntu-latest + timeout-minutes: 30 + env: + LEAN_NUM_THREADS: 2 + PYTHONUTF8: 1 + steps: + - uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 # v5 + with: + persist-credentials: false + - uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 # v1 + with: + lake-package-directory: formal/lean + auto-config: 'false' + build: 'true' + test: 'false' + lint: 'false' + use-mathlib-cache: 'true' + - name: Check source snapshot, full imports and transitive axioms + run: python3 formal/lean/verify.py --self-test + - name: Report verification boundary + run: | + echo 'This job verifies the scope declared in formal/lean/coverage.json.' + echo 'A green job is not an all-scenes or Rust-refinement certificate.' + echo 'Use verify.py --require-complete to check stage-one completion.' diff --git a/README.md b/README.md index 8e83ad7..0bfbb49 100644 --- a/README.md +++ b/README.md @@ -28,6 +28,8 @@ Project Sekai 组卡推荐引擎的 Rust 实现，专攻 **DFS / 分支限界（ [验证指南](docs/search-validation.md) 提供独立小池穷举、完整结果对拍和可复现的性能测量方法。 +[Lean 数学证明](formal/lean/README.md) 提供机器检查的搜索核心与剪枝引理，当前仍为部分覆盖；尚未完成全场景、全部剪枝的形式化验证。覆盖范围和未完成义务见该目录的说明与清单。 + ## 对外 API 主入口是 `engine::recommend_json`——纯 JSON 进、JSON 出： diff --git a/formal/lean/.gitignore b/formal/lean/.gitignore new file mode 100644 index 0000000..7f3c362 --- /dev/null +++ b/formal/lean/.gitignore @@ -0,0 +1,5 @@ +.lake/ +*.olean +*.ilean +*.trace +__pycache__/ diff --git a/formal/lean/Allium.lean b/formal/lean/Allium.lean new file mode 100644 index 0000000..883a6b3 --- /dev/null +++ b/formal/lean/Allium.lean @@ -0,0 +1,17 @@ +import Allium.Arithmetic +import Allium.Budget +import Allium.Canonical +import Allium.Collection +import Allium.DynamicProgramming +import Allium.Enumeration +import Allium.FiniteBounds +import Allium.Quadratic +import Allium.Search +import Allium.Skill +import Allium.Support +import Allium.TopK +import Allium.PowerModel +import Allium.Composition +import Allium.ScenarioSearch +import Allium.ConcretePower +import Allium.ScenarioPower diff --git a/formal/lean/Allium/Arithmetic.lean b/formal/lean/Allium/Arithmetic.lean new file mode 100644 index 0000000..671e6eb --- /dev/null +++ b/formal/lean/Allium/Arithmetic.lean @@ -0,0 +1,160 @@ +import Mathlib.Algebra.Order.Floor.Ring +import Mathlib.Data.Real.Basic +import Mathlib.Tactic + +/-! +# Exact arithmetic used by pruning + +These lemmas separate exact integer/rational reasoning from floating-point +error estimates. `grid_floor` requires a strict error premise; it does not +claim arbitrary binary64 expressions meet that premise. + +Source: objective.rs, correlated.rs, bonus_tiers.rs; pruning-proof §§1,10,17,29. +-/ +namespace Allium.Arithmetic + +theorem upper_min {x a b : ℕ} (ha : x ≤ a) (hb : x ≤ b) : x ≤ min a b := + le_min ha hb + +theorem lower_max {x a b : ℕ} (ha : a ≤ x) (hb : b ≤ x) : max a b ≤ x := + max_le ha hb + +theorem clamp_mono (cap : ℕ) : Monotone (fun x : ℕ => min x cap) := by + intro x y h + exact min_le_min_right cap h + +/-- Exact replacement of a hot division by a threshold multiplication. -/ +theorem numerator_prune (n d t : ℕ) (hd : 0 < d) : + n / d < t ↔ n < t * d := by + exact Nat.div_lt_iff_lt_mul hd + +def ceilDiv (n d : ℕ) : ℕ := (n + d - 1) / d + +theorem ceilDiv_upper (n d : ℕ) (hd : 0 < d) : n ≤ ceilDiv n d * d := by + have hmod := Nat.mod_lt (n + d - 1) hd + have hdivision := Nat.mod_add_div (n + d - 1) d + have hsub : n + d - 1 + 1 = n + d := by omega + unfold ceilDiv + nlinarith + +theorem ceilDiv_minimal (n d q : ℕ) (hd : 0 < d) (hq : n ≤ q * d) : + ceilDiv n d ≤ q := by + unfold ceilDiv + apply Nat.lt_succ_iff.mp + rw [Nat.div_lt_iff_lt_mul hd] + have hsub : n + d - 1 + 1 = n + d := by omega + change n + d - 1 < (q + 1) * d + nlinarith + +theorem ceilDiv_mono (d : ℕ) {a b : ℕ} (h : a ≤ b) : + ceilDiv a d ≤ ceilDiv b d := by + unfold ceilDiv + exact Nat.div_le_div_right (by omega) + +/-- Mathematical packing. The width hypotheses prevent field overlap. -/ +def pack (base high low : ℕ) : ℕ := high * base + low + +theorem pack_mono (base : ℕ) {hi hi' lo lo' : ℕ} + (hh : hi ≤ hi') (hl : lo ≤ lo') : pack base hi lo ≤ pack base hi' lo' := by + unfold pack + exact Nat.add_le_add (Nat.mul_le_mul_right base hh) hl + +theorem pack_lt_iff (base hi hi' lo lo' : ℕ) + (hlo : lo < base) (hlo' : lo' < base) : + pack base hi lo < pack base hi' lo' ↔ + hi < hi' ∨ (hi = hi' ∧ lo < lo') := by + unfold pack + constructor + · intro h + rcases lt_trichotomy hi hi' with hh | hh | hh + · exact Or.inl hh + · subst hi' + exact Or.inr ⟨rfl, by omega⟩ + · have hmul := Nat.mul_le_mul_right base (Nat.succ_le_of_lt hh) + nlinarith + · rintro (hh | ⟨rfl, hl⟩) + · have hmul := Nat.mul_le_mul_right base (Nat.succ_le_of_lt hh) + nlinarith + · omega + +theorem noevent_order (base a b : ℕ) : + pack base a a < pack base b b ↔ a < b := by + unfold pack + constructor + · intro h + by_contra hnot + have hmul := Nat.mul_le_mul_right base (Nat.le_of_not_gt hnot) + omega + · intro h + have hmul := Nat.mul_le_mul_right base h.le + omega + +/-- Oversized exact bounds may be clipped if legal outputs fit below the +clip. Wrapping arithmetic has no corresponding theorem. -/ +theorem safe_clip {value bound limit : ℕ} + (hb : value ≤ bound) (hl : value ≤ limit) : value ≤ min bound limit := + le_min hb hl + +theorem optional_bound {value fallback infinity : ℕ} + (hf : value ≤ fallback) (hi : value ≤ infinity) + (tight : Option ℕ) (ht : ∀ t, tight = some t → value ≤ t) : + value ≤ min fallback (tight.getD infinity) := by + cases tight with + | none => exact le_min hf hi + | some t => exact le_min hf (ht t rfl) + +/-- The integer grid supplies a full 1/d gap to the next integer. -/ +theorem grid_floor (n : ℤ) (d : ℕ) (hd : 0 < d) (x : ℝ) + (hx : x < ((n : ℝ) + 1) / (d : ℝ)) : + Int.floor x ≤ n / (d : ℤ) := by + have hdZ : (0 : ℤ) < d := by exact_mod_cast hd + have hdR : (0 : ℝ) < d := by exact_mod_cast hd + have hmod := Int.emod_lt_of_pos n hdZ + have heq := Int.mul_ediv_add_emod n (d : ℤ) + have hgridZ : n + 1 ≤ (n / (d : ℤ) + 1) * (d : ℤ) := by nlinarith + have hgridR : (n : ℝ) + 1 ≤ ((n / (d : ℤ) : ℤ) + 1 : ℝ) * (d : ℝ) := by + exact_mod_cast hgridZ + have hxnext : x < ((n / (d : ℤ) : ℤ) : ℝ) + 1 := by + apply lt_of_lt_of_le hx + exact (div_le_iff₀ hdR).mpr hgridR + have hfloor := Int.floor_le x + by_contra hnot + have hi : n / (d : ℤ) + 1 ≤ Int.floor x := by omega + have hiR : ((n / (d : ℤ) : ℤ) : ℝ) + 1 ≤ (Int.floor x : ℝ) := by + exact_mod_cast hi + linarith + +theorem grid_floor_of_error (n : ℤ) (d : ℕ) (hd : 0 < d) + (x error : ℝ) (hx : x ≤ (n : ℝ) / d + error) (he : error < 1 / (d : ℝ)) : + Int.floor x ≤ n / (d : ℤ) := by + apply grid_floor n d hd x + calc + x ≤ (n : ℝ) / d + error := hx + _ < (n : ℝ) / d + 1 / (d : ℝ) := add_lt_add_left he _ + _ = ((n : ℝ) + 1) / (d : ℝ) := by ring + +/-- Strict support compensation must pay for both decks' rounding errors. -/ +theorem support_compensation (oldExact newExact oldEval newEval loss surplus eOld eNew : ℝ) + (hchange : oldExact + surplus - loss ≤ newExact) + (hold : oldEval ≤ oldExact + eOld) + (hnew : newExact - eNew ≤ newEval) + (hmargin : eOld + eNew < surplus - loss) : oldEval < newEval := by + linarith + +/-- The suffix interval implied by key/slack/excess bounds for an exact tier. -/ +theorem tier_suffix_interval (target pre suffix extra slack extraLo extraHi + slackMax excess excessMax : ℤ) + (hlower : pre + suffix + extra - excess ≤ target) + (hupper : target ≤ pre + suffix + slack + extra) + (heLo : extraLo ≤ extra) (heHi : extra ≤ extraHi) + (hs : slack ≤ slackMax) (hx : excess ≤ excessMax) : + target - extraHi - slackMax - pre ≤ suffix ∧ + suffix ≤ target - extraLo + excessMax - pre := by + constructor <;> omega + +theorem unavoidable_bonus_exclusion (unavoidable total maxTier requested : ℕ) + (hcontribution : unavoidable ≤ total) (hrequest : requested ≤ maxTier) + (hexceeds : maxTier < unavoidable) : total ≠ requested := by + omega + +end Allium.Arithmetic diff --git a/formal/lean/Allium/Budget.lean b/formal/lean/Allium/Budget.lean new file mode 100644 index 0000000..d1265e1 --- /dev/null +++ b/formal/lean/Allium/Budget.lean @@ -0,0 +1,142 @@ +import Allium.Search + +/-! +# Interrupted search + +The deadline oracle may return any Boolean. A stopped left subtree is never +silently turned into Complete by the right subtree. Partial results contain +only evaluated seeds/leaves; Complete additionally agrees with normal search. +This models the semantic boundary, not a wall-clock or OS timer. +-/ +namespace Allium + +variable {Candidate Identity : Type*} [LinearOrder Candidate] [DecidableEq Identity] + +structure SearchOutcome (Candidate : Type*) where + retained : Finset Candidate + deadlineHit : Bool + +/-- Observe a deadline before each nonempty tree; propagate the first expiry. -/ +def searchInterruptible (identity : Candidate → Identity) (score : Candidate → ℕ) + (k : ℕ) (expired : SearchTree Candidate → Bool) (retained : Finset Candidate) : + SearchTree Candidate → SearchOutcome Candidate + | .empty => ⟨retained, false⟩ + | .leaf candidate => + if expired (.leaf candidate) then ⟨retained, true⟩ + else ⟨insert candidate retained, false⟩ + | .branch upper left right => + if expired (.branch upper left right) then ⟨retained, true⟩ + else if k ≤ (strictWitnesses identity score retained upper).card then + ⟨retained, false⟩ + else + let first := searchInterruptible identity score k expired retained left + if first.deadlineHit then first + else searchInterruptible identity score k expired first.retained right + +/-- Legality of partial incumbents needs no optimality assumption. -/ +theorem interruptible_valid (identity : Candidate → Identity) (score : Candidate → ℕ) + (k : ℕ) (expired : SearchTree Candidate → Bool) (tree : SearchTree Candidate) + (retained : Finset Candidate) : + retained ⊆ (searchInterruptible identity score k expired retained tree).retained ∧ + (searchInterruptible identity score k expired retained tree).retained ⊆ + retained ∪ tree.leaves := by + classical + induction tree generalizing retained with + | empty => simp [searchInterruptible, SearchTree.leaves] + | leaf candidate => + by_cases hx : expired (.leaf candidate) = true + · simp [searchInterruptible, hx, SearchTree.leaves] + · simp only [searchInterruptible, if_neg hx, SearchTree.leaves] + constructor + · exact Finset.subset_insert _ _ + · intro x hx + simpa only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton, + or_comm] using hx + | branch upper left right ihLeft ihRight => + by_cases hx : expired (.branch upper left right) = true + · simp [searchInterruptible, hx, SearchTree.leaves] + · by_cases hp : k ≤ (strictWitnesses identity score retained upper).card + · simp [searchInterruptible, hx, hp, SearchTree.leaves] + · let first := searchInterruptible identity score k expired retained left + rcases ihLeft retained with ⟨hlgrow, hlvalid⟩ + rcases ihRight first.retained with ⟨hrgrow, hrvalid⟩ + simp only [searchInterruptible, if_neg hx, if_neg hp, SearchTree.leaves] + change retained ⊆ (if first.deadlineHit then first else + searchInterruptible identity score k expired first.retained right).retained ∧ + (if first.deadlineHit then first else + searchInterruptible identity score k expired first.retained right).retained ⊆ + retained ∪ (left.leaves ∪ right.leaves) + by_cases hf : first.deadlineHit = true + · simp only [if_pos hf] + refine ⟨hlgrow, ?_⟩ + intro candidate hc + rcases Finset.mem_union.mp (hlvalid hc) with hs | hl + · exact Finset.mem_union_left _ hs + · exact Finset.mem_union_right _ (Finset.mem_union_left _ hl) + · simp only [if_neg hf] + refine ⟨hlgrow.trans hrgrow, ?_⟩ + intro candidate hc + rcases Finset.mem_union.mp (hrvalid hc) with hm | hr + · rcases Finset.mem_union.mp (hlvalid hm) with hs | hl + · exact Finset.mem_union_left _ hs + · exact Finset.mem_union_right _ (Finset.mem_union_left _ hl) + · exact Finset.mem_union_right _ (Finset.mem_union_right _ hr) + +/-- Completion is operational: it implies equality with the uninterrupted +algorithm, not merely that the returned vector happens to be nonempty. -/ +theorem complete_agrees_search (identity : Candidate → Identity) (score : Candidate → ℕ) + (k : ℕ) (expired : SearchTree Candidate → Bool) (tree : SearchTree Candidate) + (retained : Finset Candidate) + (hcomplete : (searchInterruptible identity score k expired retained tree).deadlineHit = false) : + (searchInterruptible identity score k expired retained tree).retained = + search identity score k retained tree := by + induction tree generalizing retained with + | empty => rfl + | leaf candidate => + by_cases hx : expired (.leaf candidate) = true + · simp [searchInterruptible, hx] at hcomplete + · simp [searchInterruptible, hx, search] + | branch upper left right ihLeft ihRight => + by_cases hx : expired (.branch upper left right) = true + · simp [searchInterruptible, hx] at hcomplete + · by_cases hp : k ≤ (strictWitnesses identity score retained upper).card + · simp [searchInterruptible, hx, hp, search] + · let first := searchInterruptible identity score k expired retained left + simp only [searchInterruptible, if_neg hx, if_neg hp] at hcomplete ⊢ + change (if first.deadlineHit then first else + searchInterruptible identity score k expired first.retained right).deadlineHit = false + at hcomplete + change (if first.deadlineHit then first else + searchInterruptible identity score k expired first.retained right).retained = _ + by_cases hf : first.deadlineHit = true + · simp [hf] at hcomplete + · simp only [if_neg hf] at hcomplete ⊢ + have hleft : first.deadlineHit = false := Bool.eq_false_iff.mpr hf + rw [ihRight first.retained hcomplete, ihLeft retained hleft] + simp only [search, if_neg hp] + +/-- The public mathematical completion theorem. There is deliberately no +exactness assertion for TimedOut. -/ +theorem complete_exact (identity : Candidate → Identity) (score : Candidate → ℕ) + (horder : ∀ a b, score b < score a → a < b) (k : ℕ) + (expired : SearchTree Candidate → Bool) (tree : SearchTree Candidate) + (hsound : tree.Sound score) (seeds : Finset Candidate) + (hseeds : seeds ⊆ tree.leaves) + (hcomplete : (searchInterruptible identity score k expired seeds tree).deadlineHit = false) : + topK identity k (searchInterruptible identity score k expired seeds tree).retained = + topK identity k tree.leaves := by + rw [complete_agrees_search identity score k expired tree seeds hcomplete] + exact search_exact identity score horder k tree hsound seeds hseeds + +/-- With legal seeds, even a timeout cannot fabricate an invalid deck. -/ +theorem timed_out_results_legal (identity : Candidate → Identity) (score : Candidate → ℕ) + (k : ℕ) (expired : SearchTree Candidate → Bool) (tree : SearchTree Candidate) + (seeds : Finset Candidate) (hseeds : seeds ⊆ tree.leaves) : + (searchInterruptible identity score k expired seeds tree).retained ⊆ tree.leaves := by + intro candidate hc + rcases Finset.mem_union.mp ((interruptible_valid identity score k expired tree seeds).2 hc) + with hs | hl + · exact hseeds hs + · exact hl + +end Allium diff --git a/formal/lean/Allium/Canonical.lean b/formal/lean/Allium/Canonical.lean new file mode 100644 index 0000000..11ecb34 --- /dev/null +++ b/formal/lean/Allium/Canonical.lean @@ -0,0 +1,95 @@ +import Allium.Collection +import Mathlib.Data.Prod.Lex +import Mathlib.Data.List.Lex + +/-! +# The five-field canonical result key + +Descending objective, descending resolved MySekai power, sorted public IDs, +ordered public IDs, and ordered dense cultivation variants. Naturals model the +validated unsigned fields; no value is reserved as an empty-slot sentinel. + +Source: tracker.rs ResultKey / PublicSetKey; problem.rs Objective. +-/ +namespace Allium.Canonical + +abbrev Key := OrderDual ℕ ×ₗ (OrderDual ℕ ×ₗ (List ℕ ×ₗ (List ℕ ×ₗ List ℕ))) + +def make (objective resolvedPower : ℕ) (sortedIds orderedIds variants : List ℕ) : Key := + toLex (OrderDual.toDual objective, + toLex (OrderDual.toDual resolvedPower, toLex (sortedIds, toLex (orderedIds, variants)))) + +def score (key : Key) : ℕ := key.1 +def power (key : Key) : ℕ := key.2.1 +def identity (key : Key) : List ℕ := key.2.2.1 +def orderedIds (key : Key) : List ℕ := key.2.2.2.1 +def variants (key : Key) : List ℕ := key.2.2.2.2 + +/-- Strict objective improvement wins before any tie-break field is read. -/ +theorem score_order (a b : Key) (h : score b < score a) : a < b := + Prod.Lex.lt_iff.mpr (Or.inl h) + +/-- Full priority order; equal objective values must keep all later fields. -/ +theorem key_lt_iff (s p s' p' : ℕ) (ids order dense ids' order' dense' : List ℕ) : + make s p ids order dense < make s' p' ids' order' dense' ↔ + s' < s ∨ (s = s' ∧ (p' < p ∨ (p = p' ∧ + (ids < ids' ∨ (ids = ids' ∧ (order < order' ∨ (order = order' ∧ dense < dense'))))))) := by + simp only [make, Prod.Lex.toLex_lt_toLex, OrderDual.toDual_lt_toDual, + OrderDual.toDual_inj] + +/-- Negation within a validated unsigned width represents ascending Power. -/ +theorem minimizing_power_order (width a b : ℕ) (ha : a ≤ width) (hb : b ≤ width) : + width - b < width - a ↔ a < b := by omega + +/-- A deck key retains dense variants even when its public card set is equal. -/ +def ofDeck {Card : Type*} (publicId denseId : Card → ℕ) + (objective resolvedPower : List Card → ℕ) (deck : List Card) : Key := + make (objective deck) (resolvedPower deck) + ((deck.map publicId).toFinset.sort (· ≤ ·)) (deck.map publicId) (deck.map denseId) + +@[simp] theorem deck_variants {Card : Type*} (publicId denseId : Card → ℕ) + (objective resolvedPower : List Card → ℕ) (deck : List Card) : + variants (ofDeck publicId denseId objective resolvedPower deck) = deck.map denseId := rfl + +@[simp] theorem deck_score {Card : Type*} (publicId denseId : Card → ℕ) + (objective resolvedPower : List Card → ℕ) (deck : List Card) : + score (ofDeck publicId denseId objective resolvedPower deck) = objective deck := rfl + +/-- Public identity is exactly the sorted public-ID set, independent of +placement, cultivation choice, objective score or result insertion order. -/ +@[simp] theorem deck_identity {Card : Type*} (publicId denseId : Card → ℕ) + (objective resolvedPower : List Card → ℕ) (deck : List Card) : + (identity (ofDeck publicId denseId objective resolvedPower deck)).toFinset = + (deck.map publicId).toFinset := by + change (((deck.map publicId).toFinset).sort (· ≤ ·)).toFinset = + (deck.map publicId).toFinset + exact Finset.sort_toFinset (· ≤ ·) _ + +/-- No two distinct ordered decks collapse to one result key when dense +indices identify variants injectively. -/ +theorem deck_key_injective {Card : Type*} (publicId denseId : Card → ℕ) + (hdense : Function.Injective denseId) (objective resolvedPower : List Card → ℕ) : + Function.Injective (ofDeck publicId denseId objective resolvedPower) := by + intro a b h + have hmap : a.map denseId = b.map denseId := congrArg variants h + exact List.map_injective_iff.mpr hdense hmap + +/-- Instantiation of generic Top-K cardinality at the actual five-field key. -/ +theorem result_count (k : ℕ) (keys : Finset Key) : + (topK identity k keys).card = min k (keys.image identity).card := + topK_card identity k keys + +/-- Instantiation of generic collection exactness at the actual key. -/ +theorem result_collection_exact (k : ℕ) (keys : List Key) : + collect identity k keys = topK identity k keys.toFinset := collect_exact identity k keys + +/-- Equal-score IDs 65535 and 0 are both ordinary identity values. -/ +theorem max_u16_is_not_sentinel : + identity (make 1 0 [65535] [65535] [0]) ≠ identity (make 1 0 [] [] []) := by decide + +/-- Equal score and power are decided by public IDs before dense variants. -/ +theorem public_id_tie_regression : + make 100 20 [0, 1, 2, 3, 65535] [0, 1, 2, 3, 65535] [9, 8, 7, 6, 5] < + make 100 20 [0, 1, 2, 4, 5] [0, 1, 2, 4, 5] [0, 1, 2, 3, 4] := by decide + +end Allium.Canonical diff --git a/formal/lean/Allium/Collection.lean b/formal/lean/Allium/Collection.lean new file mode 100644 index 0000000..4e9ebc9 --- /dev/null +++ b/formal/lean/Allium/Collection.lean @@ -0,0 +1,191 @@ +import Allium.TopK +import Mathlib.Data.Finset.Max + +/-! +# Bounded canonical collection and group merging + +This proves that the rank specification really returns min(K, distinct IDs) +candidates, and that truncating after each insertion or inside each group is +exact. Merely proving a property of an arbitrarily empty result would not do. + +Source: tracker.rs; Challenge-all merge; composition regimes. +-/ +namespace Allium + +variable {Candidate Identity : Type*} [LinearOrder Candidate] [DecidableEq Identity] + +/-- Every public set has a least concrete representative in a finite pool. -/ +theorem best_representative (identity : Candidate → Identity) + (pool : Finset Candidate) (candidate : Candidate) (hmem : candidate ∈ pool) : + ∃ best ∈ pool, + (∀ other ∈ pool, identity other = identity best → best ≤ other) ∧ + identity best = identity candidate ∧ best ≤ candidate := by + classical + let fiber := pool.filter (fun other => identity other = identity candidate) + have hx : candidate ∈ fiber := by simp [fiber, hmem] + have hnonempty : fiber.Nonempty := ⟨candidate, hx⟩ + let best := fiber.min' hnonempty + have hb : best ∈ fiber := Finset.min'_mem fiber hnonempty + rcases Finset.mem_filter.mp hb with ⟨hpool, hid⟩ + refine ⟨best, hpool, ?_, hid, Finset.min'_le fiber candidate hx⟩ + intro other ho hi + exact Finset.min'_le fiber other (Finset.mem_filter.mpr ⟨ho, hi.trans hid⟩) + +/-- Top-K itself provides the certificates required to safely discard the +rest of a finite pool. Witnesses are counted by distinct public identity. -/ +theorem topK_covers (identity : Candidate → Identity) (k : ℕ) + (pool : Finset Candidate) : + ∀ candidate ∈ pool, Covered identity k (topK identity k pool) candidate := by + classical + intro candidate hc + rcases best_representative identity pool candidate hc with + ⟨best, hbestMem, hbest, hbestId, hbestLe⟩ + by_cases hkept : best ∈ topK identity k pool + · exact Or.inl ⟨best, hkept, hbestId, hbestLe⟩ + · let bad := pool.filter (fun a => + (∀ b ∈ pool, identity b = identity a → a ≤ b) ∧ + a ≤ candidate ∧ a ∉ topK identity k pool) + have hbadBest : best ∈ bad := Finset.mem_filter.mpr + ⟨hbestMem, hbest, hbestLe, hkept⟩ + have hnonempty : bad.Nonempty := ⟨best, hbadBest⟩ + let pivot := bad.min' hnonempty + have hpivot : pivot ∈ bad := Finset.min'_mem bad hnonempty + rcases Finset.mem_filter.mp hpivot with ⟨hpMem, hpBest, hpLe, hpNot⟩ + have hrank : k ≤ (earlierIds identity pool pivot).card := by + by_contra hnot + exact hpNot ((mem_topK identity k pool pivot).mpr + ⟨hpMem, hpBest, Nat.lt_of_not_ge hnot⟩) + have hbefore : earlierIds identity pool pivot ⊆ + earlierIds identity (topK identity k pool) candidate := by + intro key hk + rcases (mem_earlierIds _ _ _ _).mp hk with ⟨other, ho, hv, hid⟩ + rcases best_representative identity pool other ho with + ⟨replacement, hm, hb, hi, hl⟩ + have hrp : replacement < pivot := lt_of_le_of_lt hl hv + have hrTop : replacement ∈ topK identity k pool := by + by_contra hn + have hrBad : replacement ∈ bad := Finset.mem_filter.mpr + ⟨hm, hb, hrp.le.trans hpLe, hn⟩ + exact (not_lt_of_ge (Finset.min'_le bad replacement hrBad)) hrp + exact (mem_earlierIds _ _ _ _).mpr + ⟨replacement, hrTop, lt_of_lt_of_le hrp hpLe, hi.trans hid⟩ + exact Or.inr (hrank.trans (Finset.card_le_card hbefore)) + +/-- The result cannot exceed its requested capacity. -/ +theorem topK_card_le (identity : Candidate → Identity) (k : ℕ) + (pool : Finset Candidate) : (topK identity k pool).card ≤ k := by + classical + let kept := topK identity k pool + change kept.card ≤ k + by_cases hn : kept.Nonempty + · let last := kept.max' hn + have hlast : last ∈ kept := Finset.max'_mem kept hn + have hrank := ((mem_topK identity k pool last).mp hlast).2.2 + have hsubset : (kept.erase last).image identity ⊆ earlierIds identity pool last := by + intro key hk + rcases Finset.mem_image.mp hk with ⟨other, ho, hid⟩ + rcases Finset.mem_erase.mp ho with ⟨hne, hm⟩ + have hlt : other < last := lt_iff_le_and_ne.mpr + ⟨Finset.le_max' kept other hm, hne⟩ + exact (mem_earlierIds _ _ _ _).mpr + ⟨other, topK_subset identity k pool hm, hlt, hid⟩ + have hinj : Set.InjOn identity (kept.erase last) := by + intro a ha b hb hid + exact topK_identity_injective identity k pool + (Finset.mem_erase.mp ha).2 (Finset.mem_erase.mp hb).2 hid + have hcard := Finset.card_le_card hsubset + rw [Finset.card_image_of_injOn hinj] at hcard + have herase := Finset.card_erase_add_one hlast + omega + · have he : kept = ∅ := Finset.not_nonempty_iff_eq_empty.mp hn + simp [he] + +/-- Exactly min(K, the number of public sets) representatives are returned. -/ +theorem topK_card (identity : Candidate → Identity) (k : ℕ) + (pool : Finset Candidate) : + (topK identity k pool).card = min k (pool.image identity).card := by + classical + let kept := topK identity k pool + have hinj : Set.InjOn identity kept := topK_identity_injective identity k pool + have hleK : kept.card ≤ k := topK_card_le identity k pool + have hleId : kept.card ≤ (pool.image identity).card := by + rw [← Finset.card_image_of_injOn hinj] + exact Finset.card_le_card (Finset.image_subset_image (topK_subset identity k pool)) + change kept.card = min k (pool.image identity).card + by_cases heq : kept.card = k + · rw [heq] at hleId ⊢ + exact (min_eq_left hleId).symm + · have hlt : kept.card < k := by omega + have hfull : pool.image identity ⊆ kept.image identity := by + intro key hk + rcases Finset.mem_image.mp hk with ⟨candidate, hc, hid⟩ + rcases topK_covers identity k pool candidate hc with ⟨other, ho, hi, _⟩ | hr + · exact Finset.mem_image.mpr ⟨other, ho, hi.trans hid⟩ + · have hs : earlierIds identity kept candidate ⊆ kept.image identity := + Finset.image_subset_image (Finset.filter_subset _ _) + have hbound := Finset.card_le_card hs + rw [Finset.card_image_of_injOn hinj] at hbound + exact False.elim (Nat.not_le_of_lt hlt (hr.trans hbound)) + have hidEq : kept.image identity = pool.image identity := + Finset.Subset.antisymm + (Finset.image_subset_image (topK_subset identity k pool)) hfull + have hcount : (pool.image identity).card = kept.card := by + rw [← hidEq, Finset.card_image_of_injOn hinj] + rw [hcount] + exact (min_eq_right hleK).symm + +theorem topK_idempotent (identity : Candidate → Identity) (k : ℕ) + (pool : Finset Candidate) : + topK identity k (topK identity k pool) = topK identity k pool := + coverage_exactness identity k (topK_subset identity k pool) (topK_covers identity k pool) + +/-- Local truncation followed by insertion/union preserves global Top-K. -/ +theorem topK_union_left (identity : Candidate → Identity) (k : ℕ) + (left right : Finset Candidate) : + topK identity k (topK identity k left ∪ right) = topK identity k (left ∪ right) := by + apply coverage_exactness identity k + · exact Finset.union_subset_union (topK_subset identity k left) (fun _ h => h) + · intro candidate hc + rcases Finset.mem_union.mp hc with hl | hr + · exact covered_mono identity k Finset.subset_union_left (topK_covers identity k left candidate hl) + · exact covered_of_mem identity k (Finset.mem_union_right _ hr) + +/-- Challenge-all and scenario merging are exact even with duplicate public +sets across groups, unequal group sizes, ties, variants, and K=0. -/ +theorem group_topK_merge {Group : Type*} [DecidableEq Group] + (identity : Candidate → Identity) (k : ℕ) (groups : Finset Group) + (pool : Group → Finset Candidate) : + topK identity k (groups.biUnion (fun g => topK identity k (pool g))) = + topK identity k (groups.biUnion pool) := by + apply coverage_exactness identity k + · intro candidate hc + rcases Finset.mem_biUnion.mp hc with ⟨g, hg, hm⟩ + exact Finset.mem_biUnion.mpr ⟨g, hg, topK_subset identity k (pool g) hm⟩ + · intro candidate hc + rcases Finset.mem_biUnion.mp hc with ⟨g, hg, hm⟩ + apply covered_mono identity k _ (topK_covers identity k (pool g) candidate hm) + intro other ho + exact Finset.mem_biUnion.mpr ⟨g, hg, ho⟩ + +/-- A bounded mathematical tracker, truncating after every insertion. -/ +noncomputable def collect (identity : Candidate → Identity) (k : ℕ) : + List Candidate → Finset Candidate + | [] => ∅ + | candidate :: rest => topK identity k (insert candidate (collect identity k rest)) + +theorem collect_exact (identity : Candidate → Identity) (k : ℕ) + (candidates : List Candidate) : + collect identity k candidates = topK identity k candidates.toFinset := by + induction candidates with + | nil => simp [collect, topK] + | cons candidate rest ih => + simp only [collect, ih, List.toFinset_cons] + simpa only [Finset.union_singleton] using + topK_union_left identity k rest.toFinset {candidate} + +theorem collect_order_independent (identity : Candidate → Identity) (k : ℕ) + (left right : List Candidate) (h : left.toFinset = right.toFinset) : + collect identity k left = collect identity k right := by + rw [collect_exact, collect_exact, h] + +end Allium diff --git a/formal/lean/Allium/Composition.lean b/formal/lean/Allium/Composition.lean new file mode 100644 index 0000000..b4152d8 --- /dev/null +++ b/formal/lean/Allium/Composition.lean @@ -0,0 +1,146 @@ +import Allium.PowerModel +import Allium.Collection + +/-! +# All 49 area-item composition regimes + +The option pair represents Mixed, SharedAttr, SharedUnit, SharedUnitAttr. +`Matches` is the semantic deck class; `Admits` is the weaker pool filter. +The latter alone does NOT justify a regime bound. Tables remain arbitrary. + +Sources: composition.rs::{Regime,RegimePlan::new,power_over_keys,search_regimes}. +-/ +namespace Allium.Composition +open PowerModel + +abbrev Regime := Option UnitId × Option Attribute + +theorem regime_count : Fintype.card Regime = 49 := by decide + +def Admits (data : CardData) (r : Regime) : Prop := + (match r.1 with | none => True | some unit => unit ∈ data.units) ∧ + (match r.2 with | none => True | some attr => data.attr = attr) + +variable {Card : Type*} + +def Matches (data : Card → CardData) (deck : List Card) (r : Regime) : Prop := + (match r.1 with + | none => commonUnits data deck = ∅ + | some unit => unit ∈ commonUnits data deck) ∧ + (match r.2 with + | none => ¬ ∃ attr, UniformAt data deck attr + | some attr => UniformAt data deck attr) + +/-- Every deck has a regime, also when several units are shared at once. -/ +theorem regimes_cover (data : Card → CardData) (deck : List Card) : + ∃ r : Regime, Matches data deck r := by + classical + by_cases hu : commonUnits data deck = ∅ + · by_cases ha : ∃ attr, UniformAt data deck attr + · rcases ha with ⟨attr, ha⟩ + exact ⟨(none, some attr), hu, ha⟩ + · exact ⟨(none, none), hu, ha⟩ + · obtain ⟨unit, hu⟩ := Finset.nonempty_iff_ne_empty.mpr hu + by_cases ha : ∃ attr, UniformAt data deck attr + · rcases ha with ⟨attr, ha⟩ + exact ⟨(some unit, some attr), hu, ha⟩ + · exact ⟨(some unit, none), hu, ha⟩ + +/-- Every real member of a regime survives that regime's pool filter. -/ +theorem matches_admits (data : Card → CardData) (deck : List Card) (r : Regime) + (h : Matches data deck r) (card : Card) (hc : card ∈ deck) : + Admits (data card) r := by + rcases r with ⟨unit, attr⟩ + rcases h with ⟨hu, ha⟩ + constructor + · cases unit with + | none => trivial + | some unit => exact (mem_commonUnits data deck unit).mp hu card hc + · cases attr with + | none => trivial + | some attr => exact ha card hc + +def unitFlags (r : Regime) : Finset Bool := + if r.1.isSome then {false, true} else {false} + +def attrFlag (r : Regime) : Bool := r.2.isSome + +/-- Mixed/SharedAttr use only false; shared-unit regimes must include BOTH +false and true because a card may carry units outside the common intersection. -/ +theorem actual_unit_flag_mem (data : Card → CardData) (deck : List Card) + (r : Regime) (h : Matches data deck r) (unit : UnitId) : + decide (unit ∈ commonUnits data deck) ∈ unitFlags r := by + rcases r with ⟨u, a⟩ + cases u with + | none => + have he : commonUnits data deck = ∅ := h.1 + change decide (unit ∈ commonUnits data deck) ∈ ({false} : Finset Bool) + rw [he] + simp + | some u => + change decide (unit ∈ commonUnits data deck) ∈ ({false, true} : Finset Bool) + cases decide (unit ∈ commonUnits data deck) <;> decide + +theorem actual_attribute_flag (data : Card → CardData) (deck : List Card) + (r : Regime) (h : Matches data deck r) : + sharesAttribute data deck = attrFlag r := by + classical + rcases r with ⟨u, a⟩ + cases a with + | none => + have ha : ¬ ∃ attr, UniformAt data deck attr := h.2 + simp [sharesAttribute, attrFlag, ha] + | some a => + have ha : ∃ attr, UniformAt data deck attr := ⟨a, h.2⟩ + simp [sharesAttribute, attrFlag, ha] + +/-- Maximum over carried units and exactly the selected member keys. -/ +def powerBound (card : CardData) (r : Regime) : ℕ := + card.units.sup (fun unit => (unitFlags r).sup (fun shared => + card.values (tableIndex (card.profile unit) shared (attrFlag r)))) + +/-- A concrete bound, derived from the evaluator's key selection. No premise +of the form `actual power <= bound` or table monotonicity is assumed. -/ +theorem power_bound_sound (data : Card → CardData) (deck : List Card) + (r : Regime) (h : Matches data deck r) (card : Card) : + cardPower data deck card ≤ powerBound (data card) r := by + unfold cardPower resolved + apply Finset.sup_le + intro unit hu + have inner : unitValue (data card) (commonUnits data deck) (sharesAttribute data deck) unit ≤ + (unitFlags r).sup (fun shared => + (data card).values (tableIndex ((data card).profile unit) shared (attrFlag r))) := by + unfold unitValue + rw [actual_attribute_flag data deck r h] + exact Finset.le_sup (f := fun shared => + (data card).values (tableIndex ((data card).profile unit) shared (attrFlag r))) + (actual_unit_flag_mem data deck r h unit) + exact inner.trans (Finset.le_sup (f := fun unit => (unitFlags r).sup (fun shared => + (data card).values (tableIndex ((data card).profile unit) shared (attrFlag r)))) hu) + +/-- Independent sum relaxation; legality constraints are not needed here. -/ +theorem deck_sum_bound (data : Card → CardData) (deck : List Card) + (r : Regime) (h : Matches data deck r) : + total data deck ≤ (deck.map (fun card => powerBound (data card) r)).sum := + List.sum_le_sum (fun card _ => power_bound_sound data deck r h card) + +/-- A regime partition may overlap. Keeping all variants and canonicalizing +only at the end avoids assuming disjoint public card sets across regimes. -/ +noncomputable def deckClass (data : Card → CardData) (pool : Finset (List Card)) + (r : Regime) : Finset (List Card) := by + classical + exact pool.filter (fun deck => Matches data deck r) + +theorem deck_classes_cover [DecidableEq Card] (data : Card → CardData) (pool : Finset (List Card)) : + Finset.univ.biUnion (deckClass data pool) = pool := by + classical + ext deck + simp only [Finset.mem_biUnion, Finset.mem_univ, true_and, deckClass, Finset.mem_filter] + constructor + · rintro ⟨_, h, _⟩ + exact h + · intro h + obtain ⟨r, hr⟩ := regimes_cover data deck + exact ⟨r, h, hr⟩ + +end Allium.Composition diff --git a/formal/lean/Allium/ConcretePower.lean b/formal/lean/Allium/ConcretePower.lean new file mode 100644 index 0000000..4dcea87 --- /dev/null +++ b/formal/lean/Allium/ConcretePower.lean @@ -0,0 +1,187 @@ +import Allium.Composition +import Allium.ScenarioSearch +import Allium.Enumeration + +/-! +# A concrete end-to-end Power instance + +Ordered five-slot legality -> all 49 regimes -> admitted pools -> arbitrary +8-entry table bounds -> character-aware / unrestricted top-five sums -> +optional cap and honor -> shared-threshold search -> canonical exhaustive Top-K. + +The theorem does not take SearchTree.Sound, a score upper bound, scene coverage, +or equality with exhaustive search as a premise. Those obligations are built +and proved below. The search is a mathematical scenario-level implementation; +it does not instantiate every production DFS optimization or the other scoring +targets. Enumeration.Roles remains the explicitly stated input specification. +-/ +namespace Allium.ConcretePower +open PowerModel Composition ScenarioSearch + +variable {Card : Type*} + +-- Keep concrete key equality aligned with the search kernel's LinearOrder. +local instance : DecidableEq Canonical.Key := + (inferInstance : LinearOrder Canonical.Key).toDecidableEq + +structure Input (Card : Type*) where + pool : Finset Card + publicId : Card → ℕ + denseId : Card → ℕ + character : Card → ℕ + roles : Enumeration.Roles + uniqueCharacters : Bool + data : Card → CardData + honor : ℕ + cap : Option ℕ + +noncomputable def decks (input : Input Card) : Finset (List Card) := + Enumeration.allValidDecks input.pool input.publicId input.character input.roles input.uniqueCharacters + +noncomputable def value (input : Input Card) : List Card → ℕ := + objective input.data input.honor input.cap + +noncomputable def keyOf (input : Input Card) : List Card → Canonical.Key := + Canonical.ofDeck input.publicId input.denseId (value input) (value input) + +noncomputable def legalKeys (input : Input Card) : Finset Canonical.Key := + (decks input).image (keyOf input) + +noncomputable def admittedPool (input : Input Card) (r : Regime) : Finset Card := by + classical + exact input.pool.filter (fun card => Admits (input.data card) r) + +noncomputable def planPower (input : Input Card) (r : Regime) : ℕ := + if input.uniqueCharacters then + FiniteBounds.characterBound 5 (admittedPool input r) input.character + (fun card => powerBound (input.data card) r) + else + FiniteBounds.maxSum 5 (admittedPool input r) (fun card => powerBound (input.data card) r) + +noncomputable def ceiling (input : Input Card) (r : Regime) : ℕ := + clamp input.cap (planPower input r + input.honor) + +theorem member_admitted (input : Input Card) (r : Regime) (deck : List Card) + (hd : deck ∈ decks input) (hr : Matches input.data deck r) : + ∀ card ∈ deck, card ∈ admittedPool input r := by + classical + have hv := (Enumeration.exhaustive_complete _ _ _ _ _ deck).mp hd + intro card hc + exact Finset.mem_filter.mpr + ⟨Enumeration.valid_card_in_pool _ _ _ _ _ deck hv card hc, + matches_admits input.data deck r hr card hc⟩ + +/-- This is the actual per-character versus per-card split of a regime plan, +not a maximum obtained by evaluating all completed decks. -/ +theorem planPower_sound (input : Input Card) (r : Regime) (deck : List Card) + (hd : deck ∈ decks input) (hr : Matches input.data deck r) : + total input.data deck ≤ planPower input r := by + classical + have hv := (Enumeration.exhaustive_complete _ _ _ _ _ deck).mp hd + have hlen := Enumeration.valid_length _ _ _ _ _ deck hv + have hcards := member_admitted input r deck hd hr + have hnd : deck.Nodup := List.Nodup.of_map input.publicId hv.2.1 + let weight := fun card => powerBound (input.data card) r + have hsum : total input.data deck ≤ (deck.map weight).sum := deck_sum_bound input.data deck r hr + by_cases hu : input.uniqueCharacters = true + · have hchars : (deck.map input.character).Nodup := hv.2.2.1 hu + simp only [planPower, hu, ↓reduceIte, FiniteBounds.characterBound] + let perChar := FiniteBounds.characterMax (admittedPool input r) input.character weight + calc + total input.data deck ≤ (deck.map weight).sum := hsum + _ ≤ (deck.map (fun card => perChar (input.character card))).sum := + List.sum_le_sum (fun card hc => + FiniteBounds.le_characterMax _ _ _ card (hcards card hc)) + _ = ((deck.map input.character).map perChar).sum := by simp only [List.map_map, Function.comp_def] + _ = ∑ char ∈ (deck.map input.character).toFinset, perChar char := + (List.sum_toFinset perChar hchars).symm + _ ≤ FiniteBounds.maxSum 5 ((admittedPool input r).image input.character) perChar := by + apply FiniteBounds.sum_le_maxSum + · intro char hc + obtain ⟨card, hc, heq⟩ := List.mem_map.mp (List.mem_toFinset.mp hc) + exact Finset.mem_image.mpr ⟨card, hcards card hc, heq⟩ + · have hn := List.toFinset_card_le (deck.map input.character) + simpa [hlen] using hn + · simp only [planPower, if_neg hu] + calc + total input.data deck ≤ (deck.map weight).sum := hsum + _ = ∑ card ∈ deck.toFinset, weight card := (List.sum_toFinset weight hnd).symm + _ ≤ FiniteBounds.maxSum 5 (admittedPool input r) weight := by + apply FiniteBounds.sum_le_maxSum + · intro card hc + exact hcards card (List.mem_toFinset.mp hc) + · exact (List.toFinset_card_le deck).trans hlen.le + +theorem ceiling_sound (input : Input Card) (r : Regime) (deck : List Card) + (hd : deck ∈ decks input) (hr : Matches input.data deck r) : + value input deck ≤ ceiling input r := + clamp_monotone input.cap (Nat.add_le_add_right (planPower_sound input r deck hd hr) input.honor) + +noncomputable def admittedDecks (input : Input Card) (r : Regime) : Finset (List Card) := by + classical + exact (decks input).filter (fun deck => ∀ card ∈ deck, Admits (input.data card) r) + +noncomputable def requiredDecks (input : Input Card) (r : Regime) : Finset (List Card) := + deckClass input.data (decks input) r + +noncomputable def admittedKeys (input : Input Card) (r : Regime) : Finset Canonical.Key := + (admittedDecks input r).image (keyOf input) + +noncomputable def requiredKeys (input : Input Card) (r : Regime) : Finset Canonical.Key := + (requiredDecks input r).image (keyOf input) + +noncomputable def scene (input : Input Card) (r : Regime) : Scene Canonical.Key := + ⟨boundedLeaves (ceiling input r) (admittedKeys input r).toList, requiredKeys input r⟩ + +/-- Incidental decks are genuinely retained as leaves. Their scores need not +satisfy the bound of this scene, but they must be legal globally. -/ +theorem scene_valid (input : Input Card) (r : Regime) : + (scene input r).Valid Canonical.score (legalKeys input) := by + classical + refine ⟨?_, ?_, ?_⟩ + · change requiredKeys input r ⊆ (boundedLeaves (ceiling input r) (admittedKeys input r).toList).leaves + rw [boundedLeaves_leaves, Finset.toList_toFinset] + apply Finset.image_subset_image + intro deck hd + rcases Finset.mem_filter.mp hd with ⟨hlegal, hmatch⟩ + exact Finset.mem_filter.mpr ⟨hlegal, matches_admits input.data deck r hmatch⟩ + · change (boundedLeaves (ceiling input r) (admittedKeys input r).toList).leaves ⊆ legalKeys input + rw [boundedLeaves_leaves, Finset.toList_toFinset] + exact Finset.image_subset_image (Finset.filter_subset _ _) + · apply boundedLeaves_sound + intro key hk + obtain ⟨deck, hd, heq⟩ := Finset.mem_image.mp hk + rcases Finset.mem_filter.mp hd with ⟨hlegal, hmatch⟩ + subst key + exact ceiling_sound input r deck hlegal hmatch + +noncomputable def scenes (input : Input Card) : List (Scene Canonical.Key) := + (Finset.univ : Finset Regime).toList.map (scene input) + +theorem scenes_cover (input : Input Card) : + ∀ key ∈ legalKeys input, ∃ s ∈ scenes input, key ∈ s.required := by + classical + intro key hk + obtain ⟨deck, hd, heq⟩ := Finset.mem_image.mp hk + obtain ⟨r, hr⟩ := regimes_cover input.data deck + refine ⟨scene input r, ?_, ?_⟩ + · exact List.mem_map.mpr ⟨r, Finset.mem_toList.mpr (Finset.mem_univ r), rfl⟩ + · exact Finset.mem_image.mpr ⟨deck, Finset.mem_filter.mpr ⟨hd, hr⟩, heq⟩ + +/-- End-to-end instance: no abstract bound/coverage assumptions remain. +All cultivation and placement variants stay until canonical public-set Top-K. -/ +theorem power_search_exact (input : Input Card) (k : ℕ) (seeds : Finset Canonical.Key) + (hseeds : seeds ⊆ legalKeys input) : + topK Canonical.identity k + (runScenes Canonical.identity Canonical.score k seeds (scenes input)) = + topK Canonical.identity k + (Enumeration.exhaustiveKeys input.pool input.publicId input.denseId input.character + input.roles input.uniqueCharacters (value input) (value input)) := by + apply runScenes_exact Canonical.identity Canonical.score Canonical.score_order k + (legalKeys input) (scenes input) _ (scenes_cover input) seeds hseeds + intro s hs + obtain ⟨r, _, heq⟩ := List.mem_map.mp hs + subst s + exact scene_valid input r + +end Allium.ConcretePower diff --git a/formal/lean/Allium/DynamicProgramming.lean b/formal/lean/Allium/DynamicProgramming.lean new file mode 100644 index 0000000..913d4ed --- /dev/null +++ b/formal/lean/Allium/DynamicProgramming.lean @@ -0,0 +1,204 @@ +import Allium.FiniteBounds + +/-! +# Group choices, reachability and componentwise-max DP compression + +A group offers exactly the choices listed in its finite set. Optional groups +explicitly include None; mandatory groups do not. A state key is preserved +exactly while independent feature maxima may come from different paths. + +Source: bonus_tiers.rs key/count tables; Challenge bound-state frontier; +Final attribute-mask DP. Mapping a particular solver's groups into this model +is a separate obligation, not an implicit completeness assumption. +-/ +namespace Allium.DP + +variable {Choice State : Type*} [DecidableEq Choice] [DecidableEq State] + +def assignments : List (Finset Choice) → Finset (List Choice) + | [] => {[]} + | options :: rest => options.biUnion (fun choice => (assignments rest).image (choice :: ·)) + +/-- Full Cartesian choice enumeration, preserving group/role positions. -/ +theorem mem_assignments (groups : List (Finset Choice)) (path : List Choice) : + path ∈ assignments groups ↔ + List.Forall₂ (fun options choice => choice ∈ options) groups path := by + induction groups generalizing path with + | nil => simp [assignments] + | cons options rest ih => + constructor + · intro h + rcases Finset.mem_biUnion.mp h with ⟨choice, hc, ht⟩ + rcases Finset.mem_image.mp ht with ⟨tail, hm, heq⟩ + subst path + exact List.Forall₂.cons hc ((ih tail).mp hm) + · intro h + cases h with + | cons hc ht => + exact Finset.mem_biUnion.mpr ⟨_, hc, Finset.mem_image.mpr ⟨_, ih _ |>.mpr ht, rfl⟩⟩ + +def optional (cards : Finset Choice) : Finset (Option Choice) := insert none (cards.image some) +def mandatory (cards : Finset Choice) : Finset (Option Choice) := cards.image some + +@[simp] theorem optional_skip (cards : Finset Choice) : none ∈ optional cards := by + simp [optional] + +@[simp] theorem mandatory_no_skip (cards : Finset Choice) : none ∉ mandatory cards := by + simp [mandatory] + +@[simp] theorem optional_take (cards : Finset Choice) (card : Choice) : + some card ∈ optional cards ↔ card ∈ cards := by simp [optional] + +@[simp] theorem mandatory_take (cards : Finset Choice) (card : Choice) : + some card ∈ mandatory cards ↔ card ∈ cards := by simp [mandatory] + +def step (update : State → Choice → State) (states : Finset State) + (options : Finset Choice) : Finset State := + states.biUnion (fun state => options.image (update state)) + +def reachable (update : State → Choice → State) : + List (Finset Choice) → Finset State → Finset State + | [], states => states + | options :: rest, states => reachable update rest (step update states options) + +/-- The DP recurrence is exactly the fold of all legal group choices. -/ +theorem mem_reachable (update : State → Choice → State) (groups : List (Finset Choice)) + (states : Finset State) (result : State) : + result ∈ reachable update groups states ↔ + ∃ initial ∈ states, ∃ path ∈ assignments groups, path.foldl update initial = result := by + induction groups generalizing states with + | nil => simp [reachable, assignments] + | cons options rest ih => + rw [reachable, ih] + constructor + · rintro ⟨middle, hm, tail, ht, heval⟩ + rcases Finset.mem_biUnion.mp hm with ⟨initial, hi, hc⟩ + rcases Finset.mem_image.mp hc with ⟨choice, hchoice, heq⟩ + subst middle + exact ⟨initial, hi, choice :: tail, + Finset.mem_biUnion.mpr ⟨choice, hchoice, Finset.mem_image.mpr ⟨tail, ht, rfl⟩⟩, + heval⟩ + · rintro ⟨initial, hi, path, hp, heval⟩ + rcases Finset.mem_biUnion.mp hp with ⟨choice, hc, htail⟩ + rcases Finset.mem_image.mp htail with ⟨tail, ht, heq⟩ + subst path + exact ⟨update initial choice, + Finset.mem_biUnion.mpr ⟨initial, hi, Finset.mem_image.mpr ⟨choice, hc, rfl⟩⟩, + tail, ht, heval⟩ + +/-- Reachability is not replaced by the all-zero feature vector. -/ +theorem unreachable_excludes_paths (update : State → Choice → State) + (groups : List (Finset Choice)) (states : Finset State) + (accept : State → Prop) [DecidablePred accept] + (hempty : (reachable update groups states).filter accept = ∅) : + ∀ initial ∈ states, ∀ path ∈ assignments groups, + ¬ accept (path.foldl update initial) := by + intro initial hi path hp ha + have hmem : path.foldl update initial ∈ reachable update groups states := + (mem_reachable update groups states _).mpr ⟨initial, hi, path, hp, rfl⟩ + have hbad := Finset.mem_filter.mpr ⟨hmem, ha⟩ + rw [hempty] at hbad + exact Finset.notMem_empty _ hbad + +section Compression +variable {Key : Type*} [DecidableEq Key] {n : ℕ} + +abbrev Features (n : ℕ) := Fin n → ℕ +abbrev Cell (Key : Type*) (n : ℕ) := Key × Features n + +def CellLE (a b : Cell Key n) : Prop := a.1 = b.1 ∧ ∀ i, a.2 i ≤ b.2 i + +def Covers (concrete abstract : Finset (Cell Key n)) : Prop := + ∀ cell ∈ concrete, ∃ upper ∈ abstract, CellLE cell upper + +/-- Exact keys and independent maxima of every feature in that key's cell. -/ +def compress (cells : Finset (Cell Key n)) : Finset (Cell Key n) := + (cells.image Prod.fst).image (fun key => + (key, fun i => (cells.filter (fun cell => cell.1 = key)).sup (fun cell => cell.2 i))) + +theorem compression_covers (cells : Finset (Cell Key n)) : Covers cells (compress cells) := by + intro cell hc + refine ⟨(cell.1, fun i => + (cells.filter (fun other => other.1 = cell.1)).sup (fun other => other.2 i)), ?_, rfl, ?_⟩ + · exact Finset.mem_image.mpr + ⟨cell.1, Finset.mem_image.mpr ⟨cell, hc, rfl⟩, rfl⟩ + · intro i + exact Finset.le_sup (f := fun other : Cell Key n => other.2 i) + (Finset.mem_filter.mpr ⟨hc, rfl⟩) + +omit [DecidableEq Key] in +theorem covers_refl (cells : Finset (Cell Key n)) : Covers cells cells := by + intro cell hc + exact ⟨cell, hc, rfl, fun _ => le_rfl⟩ + +omit [DecidableEq Key] in +theorem covers_trans {a b c : Finset (Cell Key n)} (hab : Covers a b) (hbc : Covers b c) : + Covers a c := by + intro cell hc + rcases hab cell hc with ⟨mid, hm, hkey, hfeat⟩ + rcases hbc mid hm with ⟨upper, hu, hkey', hfeat'⟩ + exact ⟨upper, hu, hkey.trans hkey', fun i => (hfeat i).trans (hfeat' i)⟩ + +omit [DecidableEq Choice] in +/-- Key updates must depend only on the exact key/choice, while feature updates +must be monotone. Additive, maximum and non-negative affine updates qualify. -/ +theorem step_covers (update : Cell Key n → Choice → Cell Key n) + (hmono : ∀ a b choice, CellLE a b → CellLE (update a choice) (update b choice)) + (options : Finset Choice) {concrete abstract : Finset (Cell Key n)} + (hcover : Covers concrete abstract) : + Covers (step update concrete options) (step update abstract options) := by + intro cell hc + rcases Finset.mem_biUnion.mp hc with ⟨prior, hp, hm⟩ + rcases Finset.mem_image.mp hm with ⟨choice, hchoice, heq⟩ + subst cell + rcases hcover prior hp with ⟨upper, hu, hle⟩ + exact ⟨update upper choice, + Finset.mem_biUnion.mpr ⟨upper, hu, Finset.mem_image.mpr ⟨choice, hchoice, rfl⟩⟩, + hmono prior upper choice hle⟩ + +def compressedReachable (update : Cell Key n → Choice → Cell Key n) : + List (Finset Choice) → Finset (Cell Key n) → Finset (Cell Key n) + | [], cells => cells + | options :: rest, cells => + compressedReachable update rest (compress (step update cells options)) + +omit [DecidableEq Choice] in +/-- Cell compression after EVERY group cannot lose an actual state's key or +underestimate any of its features. Correlation loss is only an overestimate. -/ +theorem compressed_reachable_covers (update : Cell Key n → Choice → Cell Key n) + (hmono : ∀ a b choice, CellLE a b → CellLE (update a choice) (update b choice)) + (groups : List (Finset Choice)) (concrete abstract : Finset (Cell Key n)) + (hcover : Covers concrete abstract) : + Covers (reachable update groups concrete) (compressedReachable update groups abstract) := by + induction groups generalizing concrete abstract with + | nil => exact hcover + | cons options rest ih => + exact ih (step update concrete options) (compress (step update abstract options)) + (covers_trans (step_covers update hmono options hcover) (compression_covers _)) + +omit [DecidableEq Key] in +/-- A queried interval/class of keys includes every actual hit in that class. -/ +theorem query_bound (concrete abstract : Finset (Cell Key n)) (hcover : Covers concrete abstract) + (accept : Key → Prop) [DecidablePred accept] + (objective : Features n → ℕ) (hmono : Monotone objective) + (cell : Cell Key n) (hc : cell ∈ concrete) (ha : accept cell.1) : + objective cell.2 ≤ (abstract.filter (fun c => accept c.1)).sup (fun c => objective c.2) := by + rcases hcover cell hc with ⟨upper, hu, hk, hf⟩ + exact (hmono hf).trans (Finset.le_sup + (s := abstract.filter (fun c => accept c.1)) (f := fun c : Cell Key n => objective c.2) + (Finset.mem_filter.mpr ⟨hu, by simpa only [← hk] using ha⟩)) + +omit [DecidableEq Key] in +theorem query_empty (concrete abstract : Finset (Cell Key n)) (hcover : Covers concrete abstract) + (accept : Key → Prop) [DecidablePred accept] + (hempty : abstract.filter (fun c => accept c.1) = ∅) : + ∀ cell ∈ concrete, ¬ accept cell.1 := by + intro cell hc ha + rcases hcover cell hc with ⟨upper, hu, hk, _⟩ + have hm : upper ∈ abstract.filter (fun c => accept c.1) := + Finset.mem_filter.mpr ⟨hu, by simpa only [← hk] using ha⟩ + rw [hempty] at hm + exact Finset.notMem_empty _ hm + +end Compression +end Allium.DP diff --git a/formal/lean/Allium/Enumeration.lean b/formal/lean/Allium/Enumeration.lean new file mode 100644 index 0000000..3c0558e --- /dev/null +++ b/formal/lean/Allium/Enumeration.lean @@ -0,0 +1,142 @@ +import Allium.DynamicProgramming +import Allium.Canonical + +/-! +# Ordered five-card decks and public slot roles + +The specification uses `List.Forall₂` (one membership proposition per slot), +while the enumerator uses the Cartesian skip/take implementation proved in +DynamicProgramming. Cultivation variants are NOT deduplicated before scoring. +Fixed characters begin AFTER fixed cards, matching context.rs. An ordinary +forced leader needs membership; a Final leader additionally occupies slot 0. + +Source: context.rs::{card_matches_slot,deck_matches_forced_leader}, placement.rs. +-/ +namespace Allium.Enumeration + +variable {Card : Type*} + +structure Roles where + fixedCards : List ℕ + fixedCharacters : List ℕ + forcedLeader : Option ℕ + finalChapter : Bool + /-- Invalid requests are rejected before forming a mathematical input. -/ + capacity : fixedCards.length + fixedCharacters.length ≤ 5 + +def matchesValue (wanted : Option ℕ) (actual : ℕ) : Prop := + match wanted with + | none => True + | some value => actual = value + +/-- Fixed characters are offset by the number of fixed CARD slots. -/ +def Roles.characterAt (roles : Roles) (slot : ℕ) : Option ℕ := + if roles.fixedCards.length ≤ slot then + roles.fixedCharacters[slot - roles.fixedCards.length]? + else none + +def slotAllowed (publicId character : Card → ℕ) (roles : Roles) + (slot : ℕ) (card : Card) : Prop := + matchesValue roles.fixedCards[slot]? (publicId card) ∧ + matchesValue (roles.characterAt slot) (character card) ∧ + (roles.finalChapter = true ∧ slot = 0 → matchesValue roles.forcedLeader (character card)) + +noncomputable def slotPool (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) (slot : ℕ) : Finset Card := by + classical + exact pool.filter (slotAllowed publicId character roles slot) + +noncomputable def choices (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) : List (Finset Card) := + (List.range 5).map (slotPool pool publicId character roles) + +@[simp] theorem choices_length (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) : (choices pool publicId character roles).length = 5 := by simp [choices] + +/-- Legality is independent of the enumerator's recursion. -/ +def ValidDeck (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) (uniqueCharacters : Bool) (deck : List Card) : Prop := + List.Forall₂ (fun options card => card ∈ options) + (choices pool publicId character roles) deck ∧ + (deck.map publicId).Nodup ∧ + (uniqueCharacters = true → (deck.map character).Nodup) ∧ + (∀ leader, roles.forcedLeader = some leader → ∃ card ∈ deck, character card = leader) + +noncomputable def allValidDecks (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) (uniqueCharacters : Bool) : Finset (List Card) := by + classical + exact (DP.assignments (choices pool publicId character roles)).filter (fun deck => + (deck.map publicId).Nodup ∧ + (uniqueCharacters = true → (deck.map character).Nodup) ∧ + (∀ leader, roles.forcedLeader = some leader → ∃ card ∈ deck, character card = leader)) + +/-- The actual finite enumerator contains every and only legal ordered deck. -/ +@[simp] theorem exhaustive_complete (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) (uniqueCharacters : Bool) (deck : List Card) : + deck ∈ allValidDecks pool publicId character roles uniqueCharacters ↔ + ValidDeck pool publicId character roles uniqueCharacters deck := by + classical + simp only [allValidDecks, Finset.mem_filter, DP.mem_assignments, ValidDeck] + +/-- Five positions are enforced even when every slot is unconstrained. -/ +theorem valid_length (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) (uniqueCharacters : Bool) (deck : List Card) + (h : ValidDeck pool publicId character roles uniqueCharacters deck) : deck.length = 5 := by + have hl := h.1.length_eq + simpa using hl.symm + +/-- Forall₂ cannot introduce a card that belongs to none of the slot pools. -/ +theorem member_from_choices (groups : List (Finset Card)) (deck : List Card) + (h : List.Forall₂ (fun options card => card ∈ options) groups deck) + (card : Card) (hc : card ∈ deck) : ∃ options ∈ groups, card ∈ options := by + induction h with + | nil => simp at hc + | @cons options member groups deck hm hrest ih => + rcases List.mem_cons.mp hc with heq | ht + · subst card + exact ⟨options, List.mem_cons_self, hm⟩ + · rcases ih ht with ⟨group, hg, hcard⟩ + exact ⟨group, List.mem_cons_of_mem _ hg, hcard⟩ + +theorem valid_card_in_pool (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) (uniqueCharacters : Bool) (deck : List Card) + (h : ValidDeck pool publicId character roles uniqueCharacters deck) + (card : Card) (hc : card ∈ deck) : card ∈ pool := by + classical + rcases member_from_choices _ _ h.1 card hc with ⟨options, ho, hm⟩ + rcases List.mem_map.mp ho with ⟨slot, _, heq⟩ + subst options + exact (Finset.mem_filter.mp hm).1 + +/-- Fixing a public ID keeps ALL of its variants that meet the same role. -/ +theorem same_public_role (pool : Finset Card) (publicId character : Card → ℕ) + (roles : Roles) (slot : ℕ) (a b : Card) (hpool : b ∈ pool) + (hid : publicId a = publicId b) (hchar : character a = character b) + (ha : a ∈ slotPool pool publicId character roles slot) : + b ∈ slotPool pool publicId character roles slot := by + classical + rcases Finset.mem_filter.mp ha with ⟨_, hrole⟩ + apply Finset.mem_filter.mpr + exact ⟨hpool, by simpa only [slotAllowed, hid, hchar] using hrole⟩ + +/-- Dense-variant identity is preserved through the full ordered enumeration; +only the final canonical collection identifies equal public card sets. -/ +noncomputable def exhaustiveKeys (pool : Finset Card) (publicId denseId character : Card → ℕ) + (roles : Roles) (uniqueCharacters : Bool) (score power : List Card → ℕ) : + Finset Canonical.Key := + (allValidDecks pool publicId character roles uniqueCharacters).image + (Canonical.ofDeck publicId denseId score power) + +@[simp] theorem exhaustive_keys_complete (pool : Finset Card) + (publicId denseId character : Card → ℕ) (roles : Roles) (uniqueCharacters : Bool) + (score power : List Card → ℕ) (key : Canonical.Key) : + key ∈ exhaustiveKeys pool publicId denseId character roles uniqueCharacters score power ↔ + ∃ deck, ValidDeck pool publicId character roles uniqueCharacters deck ∧ + Canonical.ofDeck publicId denseId score power deck = key := by + simp [exhaustiveKeys, Finset.mem_image] + +/-- Public IDs 0 and 65535 and character 0 have no sentinel meaning. -/ +theorem boundary_ids_are_values : + matchesValue (some 0) 0 ∧ matchesValue (some 65535) 65535 ∧ ¬ matchesValue (some 0) 1 := by simp [matchesValue] + +end Allium.Enumeration diff --git a/formal/lean/Allium/FiniteBounds.lean b/formal/lean/Allium/FiniteBounds.lean new file mode 100644 index 0000000..4362e0b --- /dev/null +++ b/formal/lean/Allium/FiniteBounds.lean @@ -0,0 +1,177 @@ +import Mathlib.Data.Finset.Powerset +import Mathlib.Data.Finset.Lattice.Fold +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Tactic + +/-! +# Finite relaxations + +The semantic value of a top-r sum is the maximum over subsets of size at most +r. Non-negative values permit zero padding. This module proves the actual +per-character relaxation, including character injectivity, rather than taking +`score <= bound` as an input assumption. + +Source: suffix.rs, solver/{numeric,power,challenge,final_chapter}.rs. +-/ +namespace Allium.FiniteBounds + +variable {Card Character : Type*} [DecidableEq Character] + +def selections (r : ℕ) (pool : Finset Card) : Finset (Finset Card) := + pool.powerset.filter (fun picks => picks.card ≤ r) + +@[simp] theorem mem_selections (r : ℕ) (pool picks : Finset Card) : + picks ∈ selections r pool ↔ picks ⊆ pool ∧ picks.card ≤ r := by + simp [selections] + +/-- A finite maximum, with no heuristically chosen prefix. -/ +def maxSum (r : ℕ) (pool : Finset Card) (weight : Card → ℕ) : ℕ := + (selections r pool).sup (fun picks => ∑ card ∈ picks, weight card) + +theorem sum_le_maxSum (r : ℕ) (pool picks : Finset Card) (weight : Card → ℕ) + (hsub : picks ⊆ pool) (hcard : picks.card ≤ r) : + (∑ card ∈ picks, weight card) ≤ maxSum r pool weight := by + exact Finset.le_sup (f := fun s : Finset Card => ∑ card ∈ s, weight card) + ((mem_selections r pool picks).mpr ⟨hsub, hcard⟩) + +theorem maxSum_mono_pool (r : ℕ) (weight : Card → ℕ) + {small large : Finset Card} (h : small ⊆ large) : + maxSum r small weight ≤ maxSum r large weight := by + apply Finset.sup_le + intro picks hp + rcases (mem_selections _ _ _).mp hp with ⟨hsub, hcard⟩ + exact sum_le_maxSum r large picks weight (hsub.trans h) hcard + +theorem maxSum_mono_count (pool : Finset Card) (weight : Card → ℕ) + {r s : ℕ} (h : r ≤ s) : maxSum r pool weight ≤ maxSum s pool weight := by + apply Finset.sup_le + intro picks hp + rcases (mem_selections _ _ _).mp hp with ⟨hsub, hcard⟩ + exact sum_le_maxSum s pool picks weight hsub (hcard.trans h) + +theorem maxSum_mono_weight (r : ℕ) (pool : Finset Card) (a b : Card → ℕ) + (h : ∀ card ∈ pool, a card ≤ b card) : maxSum r pool a ≤ maxSum r pool b := by + apply Finset.sup_le + intro picks hp + rcases (mem_selections _ _ _).mp hp with ⟨hsub, hcard⟩ + calc + (∑ card ∈ picks, a card) ≤ ∑ card ∈ picks, b card := + Finset.sum_le_sum (fun card hc => h card (hsub hc)) + _ ≤ maxSum r pool b := sum_le_maxSum r pool picks b hsub hcard + +theorem maxSum_global (r : ℕ) (pool : Finset Card) (weight : Card → ℕ) : + maxSum r pool weight ≤ r * pool.sup weight := by + apply Finset.sup_le + intro picks hp + rcases (mem_selections _ _ _).mp hp with ⟨hsub, hcard⟩ + calc + (∑ card ∈ picks, weight card) ≤ ∑ _card ∈ picks, pool.sup weight := + Finset.sum_le_sum (fun _ hc => Finset.le_sup (hsub hc)) + _ = picks.card * pool.sup weight := by simp + _ ≤ r * pool.sup weight := Nat.mul_le_mul_right _ hcard + +/-- The maximum of each component may come from a different card. -/ +theorem independent_components {n : ℕ} (r : ℕ) (pool picks : Finset Card) + (feature : Card → Fin n → ℕ) (objective : (Fin n → ℕ) → ℕ) + (hmono : Monotone objective) (hsub : picks ⊆ pool) (hcard : picks.card ≤ r) : + objective (fun i => ∑ card ∈ picks, feature card i) ≤ + objective (fun i => maxSum r pool (fun card => feature card i)) := by + apply hmono + intro i + exact sum_le_maxSum r pool picks (fun card => feature card i) hsub hcard + +/-- Exact maximum among the pool's variants of one character. -/ +def characterMax (pool : Finset Card) (character : Card → Character) + (weight : Card → ℕ) (c : Character) : ℕ := + (pool.filter (fun card => character card = c)).sup weight + +def characterBound (r : ℕ) (pool : Finset Card) (character : Card → Character) + (weight : Card → ℕ) : ℕ := + maxSum r (pool.image character) (characterMax pool character weight) + +theorem le_characterMax (pool : Finset Card) (character : Card → Character) + (weight : Card → ℕ) (card : Card) (h : card ∈ pool) : + weight card ≤ characterMax pool character weight (character card) := by + exact Finset.le_sup (by simp [h]) + +/-- A legal unique-character completion contributes at most the top-r sum of +per-character maxima. Reuse of a character is NOT silently permitted here. -/ +theorem character_bound_sound (r : ℕ) (pool picks : Finset Card) + (character : Card → Character) (weight : Card → ℕ) + (hsub : picks ⊆ pool) (hcard : picks.card ≤ r) + (hunique : Set.InjOn character picks) : + (∑ card ∈ picks, weight card) ≤ characterBound r pool character weight := by + unfold characterBound + calc + (∑ card ∈ picks, weight card) ≤ + ∑ card ∈ picks, characterMax pool character weight (character card) := + Finset.sum_le_sum (fun card hc => le_characterMax pool character weight card (hsub hc)) + _ = ∑ c ∈ picks.image character, characterMax pool character weight c := by + rw [Finset.sum_image] + exact hunique + _ ≤ maxSum r (pool.image character) (characterMax pool character weight) := + sum_le_maxSum r _ _ _ (Finset.image_subset_image hsub) + ((Finset.card_image_le).trans hcard) + +/-- Too few unused characters is a genuine feasibility contradiction. -/ +theorem insufficient_characters (pool picks : Finset Card) + (character : Card → Character) (hsub : picks ⊆ pool) + (hunique : Set.InjOn character picks) : picks.card ≤ (pool.image character).card := by + calc + picks.card = (picks.image character).card := + (Finset.card_image_of_injOn hunique).symm + _ ≤ (pool.image character).card := + Finset.card_le_card (Finset.image_subset_image hsub) + +/-- Removing possible cards cannot increase a character-aware suffix bound. -/ +theorem character_bound_mono (r : ℕ) (character : Card → Character) + (weight : Card → ℕ) {small large : Finset Card} (h : small ⊆ large) : + characterBound r small character weight ≤ characterBound r large character weight := by + unfold characterBound + apply le_trans (maxSum_mono_weight r _ _ _ ?_) + (maxSum_mono_pool r _ (Finset.image_subset_image h)) + intro c _ + apply Finset.sup_le + intro card hc + exact Finset.le_sup (by + rcases Finset.mem_filter.mp hc with ⟨hm, heq⟩ + exact Finset.mem_filter.mpr ⟨h hm, heq⟩) + +/-- A sorted candidate and its entire tail can be bounded by reusing the +current candidate's maximum; this deliberately relaxes uniqueness. -/ +theorem repeated_max_bound (picks : Finset Card) (weight : Card → ℕ) + (maximum r : ℕ) (hcard : picks.card ≤ r) + (hmax : ∀ card ∈ picks, weight card ≤ maximum) : + (∑ card ∈ picks, weight card) ≤ r * maximum := by + calc + (∑ card ∈ picks, weight card) ≤ ∑ _card ∈ picks, maximum := Finset.sum_le_sum hmax + _ = picks.card * maximum := by simp + _ ≤ r * maximum := Nat.mul_le_mul_right _ hcard + +/-- The dual lower bound used by minimizing Power; exactly r picks remain. -/ +theorem repeated_min_bound (picks : Finset Card) (weight : Card → ℕ) + (minimum r : ℕ) (hcard : picks.card = r) + (hmin : ∀ card ∈ picks, minimum ≤ weight card) : + r * minimum ≤ ∑ card ∈ picks, weight card := by + calc + r * minimum = ∑ _card ∈ picks, minimum := by simp [hcard] + _ ≤ ∑ card ∈ picks, weight card := Finset.sum_le_sum hmin + +/-- A bound over a nested tail justifies break, not merely continue. -/ +theorem monotone_break (bound : ℕ → ℕ) (hmono : Antitone bound) + (score i j threshold : ℕ) (hij : i ≤ j) + (hsound : score ≤ bound j) (hprune : bound i < threshold) : score < threshold := + lt_of_le_of_lt (hsound.trans (hmono hij)) hprune + +/-- Dominance of a BOUND state is safe for computing a ceiling. This theorem +makes no claim that an actual deck represented by that state can be deleted. -/ +theorem frontier_bound {State : Type*} [DecidableEq State] [Preorder State] + (old frontier : Finset State) (value : State → ℕ) (hmono : Monotone value) + (hcover : ∀ state ∈ old, ∃ better ∈ frontier, state ≤ better) : + old.sup value ≤ frontier.sup value := by + apply Finset.sup_le + intro state hs + rcases hcover state hs with ⟨better, hb, hle⟩ + exact (hmono hle).trans (Finset.le_sup hb) + +end Allium.FiniteBounds diff --git a/formal/lean/Allium/PowerModel.lean b/formal/lean/Allium/PowerModel.lean new file mode 100644 index 0000000..c31916f --- /dev/null +++ b/formal/lean/Allium/PowerModel.lean @@ -0,0 +1,190 @@ +import Allium.FiniteBounds + +/-! +# Concrete eight-entry power semantics + +The two unit profiles each have four member keys. The table is arbitrary: +shared-unit/attribute bonuses are NOT assumed to increase a table entry. +The six-unit scan, count-equals-five guards, and optional total-power cap are +modeled explicitly. The packed u18 representation is not identified with Lean +machine integers; this is the mathematical model of the decoded entries. + +Sources: evaluate.rs::{member_key,resolve_card_power,resolve_power_target}, +context.rs::clamp_power_total, solver/numeric.rs::bound_can_prune. +-/ +namespace Allium.PowerModel + +abbrev UnitId := Fin 6 +abbrev Attribute := Fin 6 + +/-- Exactly the index `profile * 4 + sharedUnit * 2 + sharedAttr`. -/ +def tableIndex (profile sharedUnit sharedAttr : Bool) : Fin 8 := + ⟨profile.toNat * 4 + sharedUnit.toNat * 2 + sharedAttr.toNat, by + cases profile <;> cases sharedUnit <;> cases sharedAttr <;> decide⟩ + +theorem tableIndex_surjective : + ∀ i : Fin 8, ∃ p u a : Bool, tableIndex p u a = i := by decide + +structure CardData where + attr : Attribute + units : Finset UnitId + profile : UnitId → Bool + values : Fin 8 → ℕ + +variable {Card : Type*} + +def commonUnits (data : Card → CardData) : List Card → Finset UnitId + | [] => Finset.univ + | card :: rest => (data card).units ∩ commonUnits data rest + +@[simp] theorem mem_commonUnits (data : Card → CardData) (deck : List Card) + (unit : UnitId) : + unit ∈ commonUnits data deck ↔ ∀ card ∈ deck, unit ∈ (data card).units := by + induction deck with + | nil => simp [commonUnits] + | cons card rest ih => simp [commonUnits, ih] + +def UniformAt (data : Card → CardData) (deck : List Card) (a : Attribute) : Prop := + ∀ card ∈ deck, (data card).attr = a + +noncomputable def sharesAttribute (data : Card → CardData) (deck : List Card) : Bool := by + classical + exact decide (∃ a, UniformAt data deck a) + +@[simp] theorem sharesAttribute_eq_true (data : Card → CardData) (deck : List Card) : + sharesAttribute data deck = true ↔ ∃ a, UniformAt data deck a := by + classical + simp [sharesAttribute] + +/-- The evaluator's unit count test is exactly membership in the intersection. -/ +theorem count_five_iff_common (data : Card → CardData) (deck : List Card) + (hfive : deck.length = 5) (unit : UnitId) : + deck.countP (fun card => decide (unit ∈ (data card).units)) = 5 ↔ + unit ∈ commonUnits data deck := by + rw [← hfive, List.countP_eq_length, mem_commonUnits] + simp + +/-- At every actual member, count-equals-five has one deck-wide attribute flag. -/ +theorem attribute_count_five (data : Card → CardData) (deck : List Card) + (hfive : deck.length = 5) (card : Card) (hcard : card ∈ deck) : + deck.countP (fun other => decide ((data other).attr = (data card).attr)) = 5 ↔ + sharesAttribute data deck = true := by + classical + rw [← hfive, List.countP_eq_length, sharesAttribute_eq_true] + simp only [decide_eq_true_eq] + constructor + · exact fun h => ⟨(data card).attr, h⟩ + · rintro ⟨a, ha⟩ other ho + exact (ha other ho).trans (ha card hcard).symm + +/-- The profile is selected per carried unit, not chosen independently. -/ +def unitValue (card : CardData) (common : Finset UnitId) (attr : Bool) + (unit : UnitId) : ℕ := + card.values (tableIndex (card.profile unit) (decide (unit ∈ common)) attr) + +def resolved (card : CardData) (common : Finset UnitId) (attr : Bool) : ℕ := + card.units.sup (unitValue card common attr) + +def tableMax (card : CardData) : ℕ := Finset.univ.sup card.values + +def tableMin (card : CardData) : ℕ := + Finset.univ.inf' Finset.univ_nonempty card.values + +theorem tableMin_le (card : CardData) (i : Fin 8) : tableMin card ≤ card.values i := + Finset.inf'_le card.values (Finset.mem_univ i) + +theorem le_tableMax (card : CardData) (i : Fin 8) : card.values i ≤ tableMax card := + Finset.le_sup (Finset.mem_univ i) + +theorem resolved_upper (card : CardData) (common : Finset UnitId) (attr : Bool) : + resolved card common attr ≤ tableMax card := by + apply Finset.sup_le + intro unit _ + exact le_tableMax card _ + +/-- Nonempty carried units are essential for the lower bound: an empty scan +returns zero, even when all eight decoded entries are positive. -/ +theorem resolved_lower (card : CardData) (hunits : card.units.Nonempty) + (common : Finset UnitId) (attr : Bool) : + tableMin card ≤ resolved card common attr := by + rcases hunits with ⟨unit, hu⟩ + calc + tableMin card ≤ unitValue card common attr unit := tableMin_le card _ + _ ≤ resolved card common attr := Finset.le_sup (f := unitValue card common attr) hu + +noncomputable def cardPower (data : Card → CardData) (deck : List Card) (card : Card) : ℕ := + resolved (data card) (commonUnits data deck) (sharesAttribute data deck) + +noncomputable def total (data : Card → CardData) (deck : List Card) : ℕ := + (deck.map (cardPower data deck)).sum + +/-- The cap is applied AFTER adding the honor bonus. -/ +def clamp (cap : Option ℕ) (value : ℕ) : ℕ := + match cap with + | none => value + | some limit => min value limit + +theorem clamp_monotone (cap : Option ℕ) : Monotone (clamp cap) := by + intro a b h + cases cap with + | none => exact h + | some limit => exact min_le_min_right limit h + +noncomputable def objective (data : Card → CardData) (honor : ℕ) (cap : Option ℕ) + (deck : List Card) : ℕ := clamp cap (total data deck + honor) + +/-- No uniqueness assumption: fixed slots and repeated-character requests +remain valid for this independent numeric relaxation. -/ +theorem prefix_free_upper (data : Card → CardData) (selected free : List Card) + (maximum : ℕ) (hmax : ∀ card ∈ free, tableMax (data card) ≤ maximum) : + total data (selected ++ free) ≤ + (selected.map (fun card => tableMax (data card))).sum + free.length * maximum := by + let value := cardPower data (selected ++ free) + have hs : (selected.map value).sum ≤ + (selected.map (fun card => tableMax (data card))).sum := + List.sum_le_sum (fun card _ => resolved_upper (data card) _ _) + have hf : (free.map value).sum ≤ free.length * maximum := by + calc + (free.map value).sum ≤ (free.map (fun _ => maximum)).sum := + List.sum_le_sum (fun card hc => (resolved_upper (data card) _ _).trans (hmax card hc)) + _ = free.length * maximum := by simp + simpa only [total, List.map_append, List.sum_append] using Nat.add_le_add hs hf + +theorem prefix_free_lower (data : Card → CardData) (selected free : List Card) + (minimum : ℕ) + (hunits : ∀ card ∈ selected ++ free, (data card).units.Nonempty) + (hmin : ∀ card ∈ free, minimum ≤ tableMin (data card)) : + (selected.map (fun card => tableMin (data card))).sum + free.length * minimum ≤ + total data (selected ++ free) := by + let value := cardPower data (selected ++ free) + have hs : (selected.map (fun card => tableMin (data card))).sum ≤ (selected.map value).sum := + List.sum_le_sum (fun card hc => resolved_lower (data card) (hunits card (List.mem_append_left _ hc)) _ _) + have hf : free.length * minimum ≤ (free.map value).sum := by + calc + free.length * minimum = (free.map (fun _ => minimum)).sum := by simp + _ ≤ (free.map value).sum := List.sum_le_sum (fun card hc => + (hmin card hc).trans (resolved_lower (data card) (hunits card (List.mem_append_right _ hc)) _ _)) + simpa only [total, List.map_append, List.sum_append] using Nat.add_le_add hs hf + +/-- Actual maximizing numeric prune, including the optional cap and honor. -/ +theorem maximizing_prune (data : Card → CardData) (selected free : List Card) + (maximum honor threshold : ℕ) (cap : Option ℕ) + (hmax : ∀ card ∈ free, tableMax (data card) ≤ maximum) + (hcut : clamp cap ((selected.map (fun card => tableMax (data card))).sum + + free.length * maximum + honor) < threshold) : + objective data honor cap (selected ++ free) < threshold := by + apply lt_of_le_of_lt _ hcut + exact clamp_monotone cap (Nat.add_le_add_right (prefix_free_upper data selected free maximum hmax) honor) + +/-- The dual branch must compare a LOWER bound using strict `>` instead. -/ +theorem minimizing_prune (data : Card → CardData) (selected free : List Card) + (minimum honor threshold : ℕ) (cap : Option ℕ) + (hunits : ∀ card ∈ selected ++ free, (data card).units.Nonempty) + (hmin : ∀ card ∈ free, minimum ≤ tableMin (data card)) + (hcut : threshold < clamp cap ((selected.map (fun card => tableMin (data card))).sum + + free.length * minimum + honor)) : + threshold < objective data honor cap (selected ++ free) := by + apply lt_of_lt_of_le hcut + exact clamp_monotone cap (Nat.add_le_add_right (prefix_free_lower data selected free minimum hunits hmin) honor) + +end Allium.PowerModel diff --git a/formal/lean/Allium/Quadratic.lean b/formal/lean/Allium/Quadratic.lean new file mode 100644 index 0000000..0c265e6 --- /dev/null +++ b/formal/lean/Allium/Quadratic.lean @@ -0,0 +1,153 @@ +import Mathlib.Data.Real.Basic +import Mathlib.Tactic + +/-! +# Correlated and joint power/skill bounds + +All inequalities are proved over exact reals. Positivity guards are explicit; +conversion to integer/rational machine bounds uses Arithmetic.lean separately. +No optimization oracle or numerical solver is trusted. + +Source: correlated.rs; solver/bonus_tiers.rs JointCeiling::live. +-/ +namespace Allium.Quadratic + +/-- The product maximum under a non-negative sum constraint. -/ +theorem product_under_sum (u v c : ℝ) (hu : 0 ≤ u) (hv : 0 ≤ v) + (h : u + v ≤ c) : 4 * u * v ≤ c ^ 2 := by + have hc : 0 ≤ c := le_trans (add_nonneg hu hv) h + have hp := mul_nonneg (sub_nonneg.mpr h) (add_nonneg hc (add_nonneg hu hv)) + nlinarith [sq_nonneg (u - v)] + +/-- A clipped vertex: if U is before the parabola's peak, U is optimal. -/ +theorem product_left_cap (u v cap c : ℝ) (hu : 0 ≤ u) + (hcap : u ≤ cap) (hsum : u + v ≤ c) (hpeak : 2 * cap ≤ c) : + u * v ≤ cap * (c - cap) := by + have hp := mul_nonneg (sub_nonneg.mpr hcap) + (show 0 ≤ c - cap - u by linarith) + have hq := mul_nonneg hu (show 0 ≤ c - u - v by linarith) + nlinarith + +/-- The monotone boundary case used by the correlated live-score bound. -/ +theorem product_boundary (u v intercept total : ℝ) + (hu : 0 ≤ u) (hv : 0 ≤ v) (hsum : u + v ≤ total) + (hintercept : total ≤ intercept) : + u * (intercept + v) ≤ intercept * total := by + have huT : u ≤ total := by linarith + have huI : u ≤ intercept := huT.trans hintercept + have hp := mul_nonneg (sub_nonneg.mpr huI) (sub_nonneg.mpr huT) + have hq := mul_nonneg hu (show 0 ≤ total - u - v by linarith) + nlinarith + +/-- A correlated linear plane implies the full quadratic envelope. -/ +theorem correlated_vertex (power skill intercept weight rate scale total : ℝ) + (hp : 0 ≤ power) (hs : 0 ≤ skill) (hc : 0 ≤ intercept) + (hw : 0 < weight) (hr : 0 < rate) (hq : 0 < scale) + (hplane : weight * power + rate * skill ≤ total) : + 4 * power * (intercept + skill) / scale ≤ + (rate * intercept + total) ^ 2 / (rate * weight * scale) := by + have hsum : weight * power + rate * (intercept + skill) ≤ + rate * intercept + total := by nlinarith + have hproduct := product_under_sum (weight * power) (rate * (intercept + skill)) + (rate * intercept + total) (mul_nonneg hw.le hp) + (mul_nonneg hr.le (add_nonneg hc hs)) hsum + calc + 4 * power * (intercept + skill) / scale = + (4 * (weight * power) * (rate * (intercept + skill))) / + (rate * weight * scale) := by field_simp + _ ≤ (rate * intercept + total) ^ 2 / (rate * weight * scale) := + div_le_div_of_nonneg_right hproduct (by positivity) + +/-- The second branch of correlated.rs's quadratic envelope. -/ +theorem correlated_boundary (power skill intercept weight rate scale total : ℝ) + (hp : 0 ≤ power) (hs : 0 ≤ skill) + (hw : 0 < weight) (hr : 0 < rate) (hq : 0 < scale) + (hplane : weight * power + rate * skill ≤ total) + (hbranch : total ≤ rate * intercept) : + 4 * power * (intercept + skill) / scale ≤ + 4 * intercept * total / (weight * scale) := by + have hproduct := product_boundary (weight * power) (rate * skill) + (rate * intercept) total (mul_nonneg hw.le hp) (mul_nonneg hr.le hs) hplane hbranch + have hscaled : 4 * (weight * power) * (rate * intercept + rate * skill) ≤ + 4 * (rate * intercept) * total := by nlinarith + calc + 4 * power * (intercept + skill) / scale = + (4 * (weight * power) * (rate * intercept + rate * skill)) / + (rate * weight * scale) := by field_simp + _ ≤ (4 * (rate * intercept) * total) / (rate * weight * scale) := + div_le_div_of_nonneg_right hscaled (by positivity) + _ = 4 * intercept * total / (weight * scale) := by field_simp + +/-- The same branch selection as the correlated mathematical algorithm. +Its heuristic plane weights influence tightness, never validity. -/ +noncomputable def correlatedBound (intercept weight rate scale total : ℝ) : ℝ := + if rate * intercept + total < 2 * total then + (rate * intercept + total) ^ 2 / (rate * weight * scale) + else 4 * intercept * total / (weight * scale) + +theorem correlated_bound_sound (power skill intercept weight rate scale total : ℝ) + (hp : 0 ≤ power) (hs : 0 ≤ skill) (hc : 0 ≤ intercept) + (hw : 0 < weight) (hr : 0 < rate) (hq : 0 < scale) + (hplane : weight * power + rate * skill ≤ total) : + 4 * power * (intercept + skill) / scale ≤ + correlatedBound intercept weight rate scale total := by + unfold correlatedBound + split_ifs with h + · exact correlated_vertex power skill intercept weight rate scale total hp hs hc hw hr hq hplane + · exact correlated_boundary power skill intercept weight rate scale total hp hs hw hr hq hplane + (by linarith) + +/-- Product ceiling in a box intersected with a half-plane. -/ +noncomputable def jointPeak (upperPower upperRate alpha beta total : ℝ) : ℝ := + if alpha * upperPower + beta * upperRate ≤ total then upperPower * upperRate + else if 2 * alpha * upperPower ≤ total then + upperPower * (total - alpha * upperPower) / beta + else if 2 * beta * upperRate ≤ total then + upperRate * (total - beta * upperRate) / alpha + else total ^ 2 / (4 * alpha * beta) + +/-- All four branches of the joint ceiling dominate every feasible product. -/ +theorem joint_peak_sound (power rate upperPower upperRate alpha beta total : ℝ) + (hp : 0 ≤ power) (hr : 0 ≤ rate) + (hP : power ≤ upperPower) (hR : rate ≤ upperRate) + (ha : 0 < alpha) (hb : 0 < beta) + (hplane : alpha * power + beta * rate ≤ total) : + power * rate ≤ jointPeak upperPower upperRate alpha beta total := by + unfold jointPeak + split_ifs with hcorner hleft hright + · exact mul_le_mul hP hR hr (hp.trans hP) + · have hu : alpha * power ≤ alpha * upperPower := mul_le_mul_of_nonneg_left hP ha.le + have hprod := product_left_cap (alpha * power) (beta * rate) + (alpha * upperPower) total (mul_nonneg ha.le hp) hu hplane (by nlinarith) + calc + power * rate = (alpha * power * (beta * rate)) / (alpha * beta) := by field_simp + _ ≤ (alpha * upperPower * (total - alpha * upperPower)) / (alpha * beta) := + div_le_div_of_nonneg_right hprod (by positivity) + _ = upperPower * (total - alpha * upperPower) / beta := by field_simp + · have hv : beta * rate ≤ beta * upperRate := mul_le_mul_of_nonneg_left hR hb.le + have hprod := product_left_cap (beta * rate) (alpha * power) + (beta * upperRate) total (mul_nonneg hb.le hr) hv (by linarith) (by nlinarith) + calc + power * rate = (beta * rate * (alpha * power)) / (alpha * beta) := by field_simp + _ ≤ (beta * upperRate * (total - beta * upperRate)) / (alpha * beta) := + div_le_div_of_nonneg_right hprod (by positivity) + _ = upperRate * (total - beta * upperRate) / alpha := by field_simp + · have hprod := product_under_sum (alpha * power) (beta * rate) total + (mul_nonneg ha.le hp) (mul_nonneg hb.le hr) hplane + calc + power * rate = (4 * (alpha * power) * (beta * rate)) / (4 * alpha * beta) := by + field_simp + _ ≤ total ^ 2 / (4 * alpha * beta) := + div_le_div_of_nonneg_right hprod (by positivity) + +/-- From selected features and a joint suffix maximum to the plane used above. -/ +theorem joint_plane (prePower preRate power skill powerWeight skillWeight skillRate joint : ℝ) + (hw : 0 ≤ skillRate) + (hjoint : powerWeight * power + skillWeight * skill ≤ joint) : + (powerWeight * skillRate) * (prePower + power) + + skillWeight * (preRate + skillRate * skill) ≤ + skillRate * joint + (powerWeight * skillRate) * prePower + skillWeight * preRate := by + have h := mul_le_mul_of_nonneg_left hjoint hw + nlinarith + +end Allium.Quadratic diff --git a/formal/lean/Allium/ScenarioPower.lean b/formal/lean/Allium/ScenarioPower.lean new file mode 100644 index 0000000..d6ff638 --- /dev/null +++ b/formal/lean/Allium/ScenarioPower.lean @@ -0,0 +1,99 @@ +import Allium.Composition + +/-! +# The multi-unit Power scenario envelope + +This is solver/power.rs::scenario_power, not composition::power_over_keys. +For nonempty common units it maximizes the evaluator over singleton common-unit +hypotheses. The result can be strictly larger than the real power with several +shared units; this is why visited leaves must be evaluated in their true context. +No monotonicity of the eight decoded values is used. +-/ +namespace Allium.ScenarioPower +open PowerModel + +def bound (card : CardData) (common : Finset UnitId) (attr : Bool) : ℕ := + if common = ∅ then resolved card ∅ attr + else common.sup (fun unit => resolved card {unit} attr) + +theorem bound_sound (card : CardData) (common : Finset UnitId) (attr : Bool) : + resolved card common attr ≤ bound card common attr := by + classical + by_cases hempty : common = ∅ + · simp [bound, hempty] + · rw [bound, if_neg hempty] + apply Finset.sup_le + intro unit hunit + by_cases hshared : unit ∈ common + · have hsame : unitValue card common attr unit = unitValue card {unit} attr unit := by + simp [unitValue, hshared] + calc + unitValue card common attr unit = unitValue card {unit} attr unit := hsame + _ ≤ resolved card {unit} attr := Finset.le_sup (f := unitValue card {unit} attr) hunit + _ ≤ common.sup (fun shared => resolved card {shared} attr) := Finset.le_sup (f := fun shared => resolved card {shared} attr) hshared + · obtain ⟨shared, hchosen⟩ := Finset.nonempty_iff_ne_empty.mpr hempty + have hne : unit ≠ shared := by + intro heq + exact hshared (by simpa only [heq] using hchosen) + have hsame : unitValue card common attr unit = unitValue card {shared} attr unit := by + simp [unitValue, hshared, hne] + calc + unitValue card common attr unit = unitValue card {shared} attr unit := hsame + _ ≤ resolved card {shared} attr := Finset.le_sup (f := unitValue card {shared} attr) hunit + _ ≤ common.sup (fun shared => resolved card {shared} attr) := Finset.le_sup (f := fun shared => resolved card {shared} attr) hchosen + +@[simp] theorem empty_exact (card : CardData) (attr : Bool) : + bound card ∅ attr = resolved card ∅ attr := by simp [bound] + +@[simp] theorem singleton_exact (card : CardData) (unit : UnitId) (attr : Bool) : + bound card {unit} attr = resolved card {unit} attr := by simp [bound] + +theorem bound_le_tableMax (card : CardData) (common : Finset UnitId) (attr : Bool) : + bound card common attr ≤ tableMax card := by + unfold bound + split_ifs + · exact resolved_upper card ∅ attr + · exact Finset.sup_le (fun _ _ => resolved_upper card _ attr) + +/-- The exact required common-unit set always passes the scenario's mask +containment filter at every actual member of a deck. -/ +theorem actual_common_admitted {Card : Type*} (data : Card → CardData) + (deck : List Card) (card : Card) (hc : card ∈ deck) : + commonUnits data deck ⊆ (data card).units := by + intro unit hu + exact (mem_commonUnits data deck unit).mp hu card hc + +/-- Regression: several common units can make the singleton envelope loose. -/ +def nonmonotoneCard : CardData := + { attr := 0 + units := {0, 1} + profile := fun unit => decide (unit = 1) + values := fun i => if i = 4 then 100 else if i = 6 then 20 else 10 } + +theorem multi_unit_is_only_an_upper_bound : + resolved nonmonotoneCard {0, 1} false = 20 ∧ + bound nonmonotoneCard {0, 1} false = 100 := by decide + +/-- Regression: admission does not make an arbitrary regime bound valid. -/ +def sharedBonusCard : CardData := + { attr := 0 + units := {0} + profile := fun _ => false + values := fun i => if i = 3 then 100 else 1 } + +theorem admission_is_not_bound_soundness : + Composition.Admits sharedBonusCard (none, none) ∧ + Composition.powerBound sharedBonusCard (none, none) = 1 ∧ + resolved sharedBonusCard {0} true = 100 := by + constructor + · exact ⟨trivial, trivial⟩ + · decide + +/-- Regression: the lower-bound theorem must retain the nonempty-unit guard. -/ +def emptyUnitCard : CardData := + { attr := 0, units := ∅, profile := fun _ => false, values := fun _ => 1 } + +theorem empty_units_require_a_lower_bound_guard : + tableMin emptyUnitCard = 1 ∧ resolved emptyUnitCard ∅ false = 0 := by decide + +end Allium.ScenarioPower diff --git a/formal/lean/Allium/ScenarioSearch.lean b/formal/lean/Allium/ScenarioSearch.lean new file mode 100644 index 0000000..65718be --- /dev/null +++ b/formal/lean/Allium/ScenarioSearch.lean @@ -0,0 +1,162 @@ +import Allium.Search +import Allium.Collection + +/-! +# Search with overlapping required classes and incidental leaves + +A composition pool admits more decks than belong to its semantic regime. +Requiring its bound to dominate ALL admitted leaves would be false for an +arbitrary nonmonotone power table. Here bounds cover only required leaves; +all visited leaves must still be globally legal. A shared tracker retains +coverage witnesses across scenes. Required classes cover the global space. + +This proves the scenario coordinator without assuming local Top-K exactness +under an externally supplied threshold. In particular, seeds need not belong +to the current scene, witnesses are counted by public identity, and K=0 works. +-/ +namespace Allium.ScenarioSearch + +variable {Candidate Identity : Type*} [LinearOrder Candidate] [DecidableEq Identity] + +/-- A node owes its bound to required leaves, not incidental legal leaves. -/ +def RequiredSound (score : Candidate → ℕ) (required : Finset Candidate) : + SearchTree Candidate → Prop + | .empty => True + | .leaf _ => True + | .branch upper left right => + (∀ candidate ∈ left.leaves ∪ right.leaves, + candidate ∈ required → score candidate ≤ upper) ∧ + RequiredSound score required left ∧ RequiredSound score required right + +/-- The existing pruning algorithm remains unchanged. Only the soundness +contract is weakened to the semantic class which this scene must cover. -/ +theorem required_search_spec (identity : Candidate → Identity) (score : Candidate → ℕ) + (horder : ∀ a b, score b < score a → a < b) (k : ℕ) + (required : Finset Candidate) (tree : SearchTree Candidate) + (hsound : RequiredSound score required tree) (retained : Finset Candidate) : + retained ⊆ search identity score k retained tree ∧ + search identity score k retained tree ⊆ retained ∪ tree.leaves ∧ + ∀ candidate ∈ tree.leaves, candidate ∈ required → + Covered identity k (search identity score k retained tree) candidate := by + classical + induction tree generalizing retained with + | empty => + simp only [search, SearchTree.leaves, Finset.union_empty] + exact ⟨(fun _ h => h), (fun _ h => h), by simp⟩ + | leaf candidate => + simp only [search, SearchTree.leaves] + refine ⟨Finset.subset_insert _ _, ?_, ?_⟩ + · intro x hx + simpa only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton, or_comm] using hx + · intro x hx _ + have heq : x = candidate := Finset.mem_singleton.mp hx + subst x + exact covered_of_mem identity k (Finset.mem_insert_self _ _) + | branch upper left right ihLeft ihRight => + rcases hsound with ⟨hub, hl, hr⟩ + by_cases hprune : k ≤ (strictWitnesses identity score retained upper).card + · simp only [search, if_pos hprune, SearchTree.leaves] + refine ⟨(fun _ h => h), Finset.subset_union_left, ?_⟩ + intro candidate hc hrequired + exact strict_upper_prune identity score horder k retained candidate upper + (hub candidate hc hrequired) hprune + · simp only [search, if_neg hprune, SearchTree.leaves] + rcases ihLeft hl retained with ⟨hlgrow, hlvalid, hlcover⟩ + rcases ihRight hr (search identity score k retained left) with + ⟨hrgrow, hrvalid, hrcover⟩ + refine ⟨hlgrow.trans hrgrow, ?_, ?_⟩ + · intro candidate hc + rcases Finset.mem_union.mp (hrvalid hc) with hmid | hright + · rcases Finset.mem_union.mp (hlvalid hmid) with hseed | hleft + · exact Finset.mem_union_left _ hseed + · exact Finset.mem_union_right _ (Finset.mem_union_left _ hleft) + · exact Finset.mem_union_right _ (Finset.mem_union_right _ hright) + · intro candidate hc hrequired + rcases Finset.mem_union.mp hc with hleft | hright + · exact covered_mono identity k hrgrow (hlcover candidate hleft hrequired) + · exact hrcover candidate hright hrequired + +/-- A simple finite tree with a data-derived uniform scene bound. Building +this tree is not a claim about the production DFS's runtime complexity. -/ +def boundedLeaves (upper : ℕ) : List Candidate → SearchTree Candidate + | [] => .empty + | candidate :: rest => .branch upper (.leaf candidate) (boundedLeaves upper rest) + +@[simp] theorem boundedLeaves_leaves (upper : ℕ) (candidates : List Candidate) : + (boundedLeaves upper candidates).leaves = candidates.toFinset := by + induction candidates with + | nil => simp [boundedLeaves, SearchTree.leaves] + | cons candidate rest ih => simp [boundedLeaves, SearchTree.leaves, ih] + +theorem boundedLeaves_sound (score : Candidate → ℕ) (required : Finset Candidate) + (upper : ℕ) (candidates : List Candidate) + (hbound : ∀ candidate ∈ required, score candidate ≤ upper) : + RequiredSound score required (boundedLeaves upper candidates) := by + induction candidates with + | nil => trivial + | cons candidate rest ih => + exact ⟨(fun x _ hx => hbound x hx), trivial, ih⟩ + +structure Scene (Candidate : Type*) where + tree : SearchTree Candidate + required : Finset Candidate + +def Scene.Valid (score : Candidate → ℕ) (legal : Finset Candidate) + (scene : Scene Candidate) : Prop := + scene.required ⊆ scene.tree.leaves ∧ + scene.tree.leaves ⊆ legal ∧ RequiredSound score scene.required scene.tree + +def runScenes (identity : Candidate → Identity) (score : Candidate → ℕ) (k : ℕ) + (retained : Finset Candidate) : List (Scene Candidate) → Finset Candidate + | [] => retained + | scene :: rest => + runScenes identity score k (search identity score k retained scene.tree) rest + +/-- Coverage is transferred through the shared tracker, including witnesses +from earlier scenes which are not admitted by the currently searched scene. -/ +theorem runScenes_spec (identity : Candidate → Identity) (score : Candidate → ℕ) + (horder : ∀ a b, score b < score a → a < b) (k : ℕ) + (legal : Finset Candidate) (scenes : List (Scene Candidate)) + (hscenes : ∀ scene ∈ scenes, scene.Valid score legal) + (retained : Finset Candidate) (hretained : retained ⊆ legal) : + retained ⊆ runScenes identity score k retained scenes ∧ + runScenes identity score k retained scenes ⊆ legal ∧ + ∀ scene ∈ scenes, ∀ candidate ∈ scene.required, + Covered identity k (runScenes identity score k retained scenes) candidate := by + induction scenes generalizing retained with + | nil => exact ⟨(fun _ h => h), hretained, by simp⟩ + | cons scene rest ih => + have hv := hscenes scene List.mem_cons_self + rcases required_search_spec identity score horder k scene.required scene.tree hv.2.2 retained with + ⟨hgrow, hvalid, hcover⟩ + have hmid : search identity score k retained scene.tree ⊆ legal := by + intro candidate hc + rcases Finset.mem_union.mp (hvalid hc) with hs | hl + · exact hretained hs + · exact hv.2.1 hl + rcases ih (fun s hs => hscenes s (List.mem_cons_of_mem _ hs)) _ hmid with + ⟨hrgrow, hrvalid, hrcover⟩ + refine ⟨hgrow.trans hrgrow, hrvalid, ?_⟩ + intro s hs candidate hc + rcases List.mem_cons.mp hs with heq | hrest + · subst s + exact covered_mono identity k hrgrow (hcover candidate (hv.1 hc) hc) + · exact hrcover s hrest candidate hc + +/-- Exact global canonical Top-K from overlapping scenes, with no assertion +that an external threshold leaves a scene's LOCAL Top-K unchanged. -/ +theorem runScenes_exact (identity : Candidate → Identity) (score : Candidate → ℕ) + (horder : ∀ a b, score b < score a → a < b) (k : ℕ) + (legal : Finset Candidate) (scenes : List (Scene Candidate)) + (hscenes : ∀ scene ∈ scenes, scene.Valid score legal) + (hcover : ∀ candidate ∈ legal, ∃ scene ∈ scenes, candidate ∈ scene.required) + (seeds : Finset Candidate) (hseeds : seeds ⊆ legal) : + topK identity k (runScenes identity score k seeds scenes) = topK identity k legal := by + rcases runScenes_spec identity score horder k legal scenes hscenes seeds hseeds with + ⟨_, hvalid, hcovered⟩ + apply coverage_exactness identity k hvalid + intro candidate hc + obtain ⟨scene, hs, hm⟩ := hcover candidate hc + exact hcovered scene hs candidate hm + +end Allium.ScenarioSearch diff --git a/formal/lean/Allium/Search.lean b/formal/lean/Allium/Search.lean new file mode 100644 index 0000000..5ca2a5c --- /dev/null +++ b/formal/lean/Allium/Search.lean @@ -0,0 +1,108 @@ +import Allium.TopK + +/-! +# A branch-and-bound kernel + +This is a mathematical search implementation, not an extraction of Rust. +The tree contains concrete candidates. A branch's bound is required to be +proved by `SearchTree.Sound`, which is not an axiom. The kernel obtains +K-distinct-identity witnesses from already evaluated candidates before pruning. +-/ + +namespace Allium + +variable {Candidate Identity : Type*} [LinearOrder Candidate] [DecidableEq Identity] + +inductive SearchTree (Candidate : Type*) where + | empty + | leaf (candidate : Candidate) + | branch (upper : ℕ) (left right : SearchTree Candidate) + +def SearchTree.leaves : SearchTree Candidate → Finset Candidate + | .empty => ∅ + | .leaf candidate => {candidate} + | .branch _ left right => left.leaves ∪ right.leaves + +/-- An upper-bound obligation at every internal node. -/ +def SearchTree.Sound (score : Candidate → ℕ) : SearchTree Candidate → Prop + | .empty => True + | .leaf _ => True + | .branch upper left right => + (∀ candidate ∈ left.leaves ∪ right.leaves, score candidate ≤ upper) ∧ + left.Sound score ∧ right.Sound score + +/-- Exact branch-and-bound, with a mathematical set of evaluated candidates. -/ +def search (identity : Candidate → Identity) (score : Candidate → ℕ) (k : ℕ) + (retained : Finset Candidate) : SearchTree Candidate → Finset Candidate + | .empty => retained + | .leaf candidate => insert candidate retained + | .branch upper left right => + if k ≤ (strictWitnesses identity score retained upper).card then retained + else search identity score k (search identity score k retained left) right + +/-- Search neither fabricates a leaf nor removes a seed. Every unvisited +leaf has a coverage certificate in the final retained pool. -/ +theorem search_spec (identity : Candidate → Identity) (score : Candidate → ℕ) + (horder : ∀ a b, score b < score a → a < b) (k : ℕ) + (tree : SearchTree Candidate) (hsound : tree.Sound score) + (retained : Finset Candidate) : + retained ⊆ search identity score k retained tree ∧ + search identity score k retained tree ⊆ retained ∪ tree.leaves ∧ + ∀ candidate ∈ tree.leaves, + Covered identity k (search identity score k retained tree) candidate := by + classical + induction tree generalizing retained with + | empty => + simp only [search, SearchTree.leaves, Finset.union_empty] + exact ⟨(fun _ h => h), (fun _ h => h), by simp⟩ + | leaf candidate => + simp only [search, SearchTree.leaves] + refine ⟨Finset.subset_insert _ _, ?_, ?_⟩ + · intro x hx + simpa only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton, + or_comm] using hx + · intro x hx + have heq : x = candidate := Finset.mem_singleton.mp hx + subst x + exact covered_of_mem identity k (Finset.mem_insert_self _ _) + | branch upper left right ihLeft ihRight => + rcases hsound with ⟨hub, hl, hr⟩ + by_cases hprune : k ≤ (strictWitnesses identity score retained upper).card + · simp only [search, if_pos hprune, SearchTree.leaves] + refine ⟨(fun _ h => h), Finset.subset_union_left, ?_⟩ + intro candidate hc + exact strict_upper_prune identity score horder k retained candidate upper + (hub candidate hc) hprune + · simp only [search, if_neg hprune, SearchTree.leaves] + rcases ihLeft hl retained with ⟨hlgrow, hlvalid, hlcover⟩ + rcases ihRight hr (search identity score k retained left) with + ⟨hrgrow, hrvalid, hrcover⟩ + refine ⟨hlgrow.trans hrgrow, ?_, ?_⟩ + · intro candidate hc + rcases Finset.mem_union.mp (hrvalid hc) with hmid | hright + · rcases Finset.mem_union.mp (hlvalid hmid) with hseed | hleft + · exact Finset.mem_union_left _ hseed + · exact Finset.mem_union_right _ (Finset.mem_union_left _ hleft) + · exact Finset.mem_union_right _ (Finset.mem_union_right _ hright) + · intro candidate hc + rcases Finset.mem_union.mp hc with hleft | hright + · exact covered_mono identity k hrgrow (hlcover candidate hleft) + · exact hrcover candidate hright + +/-- Exactness of the mathematical search kernel for every K, including zero. +An Allium mode still has to discharge leaf enumeration and concrete bounds. -/ +theorem search_exact (identity : Candidate → Identity) (score : Candidate → ℕ) + (horder : ∀ a b, score b < score a → a < b) (k : ℕ) + (tree : SearchTree Candidate) (hsound : tree.Sound score) + (seeds : Finset Candidate) (hseeds : seeds ⊆ tree.leaves) : + topK identity k (search identity score k seeds tree) = + topK identity k tree.leaves := by + rcases search_spec identity score horder k tree hsound seeds with + ⟨_, hvalid, hcover⟩ + apply coverage_exactness identity k _ hcover + intro candidate hc + rcases Finset.mem_union.mp (hvalid hc) with hseed | hleaf + · exact hseeds hseed + · exact hleaf + +end Allium diff --git a/formal/lean/Allium/Skill.lean b/formal/lean/Allium/Skill.lean new file mode 100644 index 0000000..56d269c --- /dev/null +++ b/formal/lean/Allium/Skill.lean @@ -0,0 +1,199 @@ +import Allium.Arithmetic +import Allium.FiniteBounds + +/-! +# Composition-sensitive skill ceilings + +Unit-count tables are deliberately NOT assumed monotone. Reference shares are +modelled in exact hundredths, with the floating-point bridge kept separate. +The four reference positions are the other four deck members, not the holder. + +Source: skill_ceiling.rs; evaluate.rs; pruning-proof §20. +-/ +namespace Allium.Skill + +/-- Encoded Skill objective, before the evaluator's floating-point bridge. -/ +def key (sum leader : ℕ) : ℕ := 2 * sum + 8 * leader + +theorem key_mono {s s' l l' : ℕ} (hs : s ≤ s') (hl : l ≤ l') : + key s l ≤ key s' l' := by unfold key; omega + +theorem effective_skill_identity (sum leader : ℝ) : + 10 * (leader + (sum - leader) / 5) = 2 * sum + 8 * leader := by ring + +/-- Global remaining-member ceiling, including the leader's extra weight. -/ +theorem global_bound (sum leader extraSum extraLeader free maximum : ℕ) + (hs : extraSum ≤ free * maximum) (hl : extraLeader ≤ maximum) : + key (sum + extraSum) (max leader extraLeader) ≤ + key (sum + free * maximum) (max leader maximum) := by + exact key_mono (Nat.add_le_add_left hs sum) (max_le_max_left leader hl) + +/-- Prefix maxima, not the last element of a potentially nonmonotone table. -/ +def unitCeiling (table : ℕ → ℕ) (staticMax possibleCount : ℕ) : ℕ := + min staticMax ((Finset.range (min 5 (max 1 possibleCount))).sup table) + +theorem unit_count_sound (table : ℕ → ℕ) (staticMax actualCount possibleCount : ℕ) + (hdeck : actualCount ≤ 5) (hcount : actualCount ≤ possibleCount) + (hstatic : table (actualCount - 1) ≤ staticMax) : + table (actualCount - 1) ≤ unitCeiling table staticMax possibleCount := by + apply le_min hstatic + apply Finset.le_sup (f := table) + simp only [Finset.mem_range] + omega + +/-- Each additional card increases a selected unit's population by at most one. -/ +theorem counted_union_bound {Card : Type*} [DecidableEq Card] + (selected remaining : Finset Card) (p : Card → Prop) [DecidablePred p] : + ((selected ∪ remaining).filter p).card ≤ + (selected.filter p).card + remaining.card := by + rw [Finset.filter_union] + exact (Finset.card_union_le _ _).trans + (Nat.add_le_add_left (Finset.card_filter_le _ _) _) + +/-- Empty and own units are removed before measuring different units. -/ +def otherUnits {Card Unit : Type*} [DecidableEq Unit] + (cards : Finset Card) (memberUnit : Card → Option Unit) (own : Option Unit) : + Finset (Option Unit) := + (cards.image memberUnit).filter (fun unit => unit ≠ none ∧ unit ≠ own) + +theorem other_units_union_bound {Card Unit : Type*} [DecidableEq Card] [DecidableEq Unit] + (selected remaining : Finset Card) (memberUnit : Card → Option Unit) (own : Option Unit) : + (otherUnits (selected ∪ remaining) memberUnit own).card ≤ + (otherUnits selected memberUnit own).card + remaining.card := by + unfold otherUnits + rw [Finset.image_union, Finset.filter_union] + exact (Finset.card_union_le _ _).trans + (Nat.add_le_add_left ((Finset.card_filter_le _ _).trans Finset.card_image_le) _) + +def differentUnitValue (base increment staticMax counted : ℕ) : ℕ := + min staticMax (base + increment * min 2 counted) + +theorem different_unit_mono (base increment staticMax : ℕ) : + Monotone (differentUnitValue base increment staticMax) := by + intro a b h + apply min_le_min_left + apply Nat.add_le_add_left + exact Nat.mul_le_mul_left increment (min_le_min_left 2 h) + +theorem different_unit_sound {Card Unit : Type*} [DecidableEq Card] [DecidableEq Unit] + (selected remaining : Finset Card) (memberUnit : Card → Option Unit) + (own : Option Unit) (base increment staticMax free : ℕ) (hfree : remaining.card ≤ free) : + differentUnitValue base increment staticMax + (otherUnits (selected ∪ remaining) memberUnit own).card ≤ + differentUnitValue base increment staticMax + ((otherUnits selected memberUnit own).card + free) := by + apply different_unit_mono + exact (other_units_union_bound selected remaining memberUnit own).trans + (Nat.add_le_add_left hfree _) + +/-- Share in hundredths of one percent; inputs are integer static references. -/ +def referenceShare (reference rate cap : ℕ) : ℕ := min (reference * rate) (100 * cap) + +theorem reference_share_cap (reference rate cap : ℕ) : + referenceShare reference rate cap ≤ 100 * cap := min_le_right _ _ + +theorem reference_share_mono {reference reference' rate rate' cap cap' : ℕ} + (hr : reference ≤ reference') (hw : rate ≤ rate') (hc : cap ≤ cap') : + referenceShare reference rate cap ≤ referenceShare reference' rate' cap' := by + exact min_le_min (Nat.mul_le_mul hr hw) (Nat.mul_le_mul_left 100 hc) + +def max4 (values : Fin 4 → ℕ) : ℕ := max (values 0) (max (values 1) (max (values 2) (values 3))) +def min4 (values : Fin 4 → ℕ) : ℕ := min (values 0) (min (values 1) (min (values 2) (values 3))) +def sum4 (values : Fin 4 → ℕ) : ℕ := values 0 + values 1 + values 2 + values 3 + +theorem max4_mono {a b : Fin 4 → ℕ} (h : ∀ i, a i ≤ b i) : max4 a ≤ max4 b := + max_le_max (h 0) (max_le_max (h 1) (max_le_max (h 2) (h 3))) + +theorem min4_mono {a b : Fin 4 → ℕ} (h : ∀ i, a i ≤ b i) : min4 a ≤ min4 b := + min_le_min (h 0) (min_le_min (h 1) (min_le_min (h 2) (h 3))) + +theorem sum4_mono {a b : Fin 4 → ℕ} (h : ∀ i, a i ≤ b i) : sum4 a ≤ sum4 b := by + unfold sum4 + exact Nat.add_le_add (Nat.add_le_add (Nat.add_le_add (h 0) (h 1)) (h 2)) (h 3) + +inductive ReferenceStrategy where + | maximum | minimum | average + +def referenceUpper (strategy : ReferenceStrategy) (shares : Fin 4 → ℕ) : ℕ := + match strategy with + | .maximum => Arithmetic.ceilDiv (max4 shares) 100 + | .minimum => Arithmetic.ceilDiv (min4 shares) 100 + | .average => sum4 shares / 400 + 1 + +noncomputable def referenceExact (strategy : ReferenceStrategy) (shares : Fin 4 → ℕ) : ℝ := + match strategy with + | .maximum => (max4 shares : ℝ) / 100 + | .minimum => (min4 shares : ℝ) / 100 + | .average => (sum4 shares : ℝ) / 400 + +theorem reference_upper_mono (strategy : ReferenceStrategy) {a b : Fin 4 → ℕ} + (h : ∀ i, a i ≤ b i) : referenceUpper strategy a ≤ referenceUpper strategy b := by + cases strategy with + | maximum => exact Arithmetic.ceilDiv_mono 100 (max4_mono h) + | minimum => exact Arithmetic.ceilDiv_mono 100 (min4_mono h) + | average => exact Nat.add_le_add_right (Nat.div_le_div_right (sum4_mono h)) 1 + +/-- Rational reference values are below the implemented integer ceiling. +The Average branch leaves at least 1/400 for its floating-point bridge. -/ +theorem reference_exact_bound (strategy : ReferenceStrategy) (shares : Fin 4 → ℕ) : + referenceExact strategy shares ≤ (referenceUpper strategy shares : ℝ) := by + cases strategy with + | maximum => + have h := Arithmetic.ceilDiv_upper (max4 shares) 100 (by decide) + change (max4 shares : ℝ) / 100 ≤ (Arithmetic.ceilDiv (max4 shares) 100 : ℝ) + rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 100)] + exact_mod_cast h + | minimum => + have h := Arithmetic.ceilDiv_upper (min4 shares) 100 (by decide) + change (min4 shares : ℝ) / 100 ≤ (Arithmetic.ceilDiv (min4 shares) 100 : ℝ) + rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 100)] + exact_mod_cast h + | average => + have hm := Nat.mod_lt (sum4 shares) (by decide : 0 < 400) + have hd := Nat.mod_add_div (sum4 shares) 400 + have h : sum4 shares ≤ (sum4 shares / 400 + 1) * 400 := by omega + change (sum4 shares : ℝ) / 400 ≤ ((sum4 shares / 400 + 1 : ℕ) : ℝ) + rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 400)] + exact_mod_cast h + +def relaxedShares (known : Finset (Fin 4)) (references : Fin 4 → ℕ) (rate cap : ℕ) : + Fin 4 → ℕ := fun i => + if i ∈ known then referenceShare (references i) rate cap else 100 * cap + +/-- Each unknown member can be safely replaced by the cap. -/ +theorem reference_relax_sound (strategy : ReferenceStrategy) (known : Finset (Fin 4)) + (references : Fin 4 → ℕ) (rate cap : ℕ) : + referenceUpper strategy (fun i => referenceShare (references i) rate cap) ≤ + referenceUpper strategy (relaxedShares known references rate cap) := by + apply reference_upper_mono + intro i + unfold relaxedShares + split_ifs + · exact le_rfl + · exact reference_share_cap _ _ _ + +/-- Merging candidate rules componentwise may lose correlation, but never +underestimates: candidate ceilings never read the holder's own reference. -/ +theorem merged_reference_rule_sound (strategy : ReferenceStrategy) (known : Finset (Fin 4)) + (references : Fin 4 → ℕ) (base base' rate rate' cap cap' : ℕ) + (hb : base ≤ base') (hr : rate ≤ rate') (hc : cap ≤ cap') : + base + referenceUpper strategy (relaxedShares known references rate cap) ≤ + base' + referenceUpper strategy (relaxedShares known references rate' cap') := by + apply Nat.add_le_add hb + apply reference_upper_mono + intro i + unfold relaxedShares + split_ifs + · exact reference_share_mono le_rfl hr hc + · exact Nat.mul_le_mul_left 100 hc + +/-- The encoded floating result is safe once its independently established +error, including the explicit offset, is strictly less than one integer unit. -/ +theorem encoded_key_upper (sum leader : ℕ) (encoded error : ℝ) + (hencoded : encoded ≤ (key sum leader : ℝ) + error) (herror : error < 1) : + Int.floor encoded ≤ (key sum leader : ℤ) := by + have h := Arithmetic.grid_floor_of_error (key sum leader : ℤ) 1 (by decide) + encoded error (by simpa using hencoded) (by simpa using herror) + simpa using h + +end Allium.Skill diff --git a/formal/lean/Allium/Support.lean b/formal/lean/Allium/Support.lean new file mode 100644 index 0000000..98757a3 --- /dev/null +++ b/formal/lean/Allium/Support.lean @@ -0,0 +1,178 @@ +import Allium.FiniteBounds +import Allium.Arithmetic +import Mathlib.Data.Finset.Max + +/-! +# Support-pool relaxation and cutoff algebra + +The support objective is the largest sum of at most W eligible public IDs. +Non-negative support weights make unused slots equivalent to zero padding. +This module proves prefix-exclusion monotonicity, a sorted-prefix optimality +certificate, and the compensated replacement inequality. The concrete +q+5-rank cutoff certificate and binary64 error budget remain separate duties. + +Source: evaluate.rs::calc_support_bonus, suffix.rs, dominance.rs, bonus_tiers.rs. +-/ +namespace Allium.Support + +variable {Id : Type*} + +/-- Partition a support sum without assuming rounded subtraction is exact. -/ +theorem sum_split [DecidableEq Id] (s t : Finset Id) (weight : Id → ℝ) : + (∑ id ∈ s \ t, weight id) + (∑ id ∈ s ∩ t, weight id) = ∑ id ∈ s, weight id := by + have hd : Disjoint (s \ t) (s ∩ t) := by + apply Finset.disjoint_left.mpr + intro id hs ht + exact (Finset.mem_sdiff.mp hs).2 (Finset.mem_inter.mp ht).2 + have hu : (s \ t) ∪ (s ∩ t) = s := by + ext id + simp only [Finset.mem_union, Finset.mem_sdiff, Finset.mem_inter] + tauto + calc + (∑ id ∈ s \ t, weight id) + (∑ id ∈ s ∩ t, weight id) = + ∑ id ∈ (s \ t) ∪ (s ∩ t), weight id := (Finset.sum_union hd).symm + _ = ∑ id ∈ s, weight id := by rw [hu] + +noncomputable def totals (slots : ℕ) (eligible : Finset Id) (weight : Id → ℝ) : Finset ℝ := + (FiniteBounds.selections slots eligible).image (fun picks => ∑ id ∈ picks, weight id) + +theorem totals_nonempty (slots : ℕ) (eligible : Finset Id) (weight : Id → ℝ) : + (totals slots eligible weight).Nonempty := by + refine ⟨0, Finset.mem_image.mpr ⟨∅, ?_, by simp⟩⟩ + exact (FiniteBounds.mem_selections _ _ _).mpr ⟨Finset.empty_subset _, by simp⟩ + +noncomputable def bestSum (slots : ℕ) (eligible : Finset Id) (weight : Id → ℝ) : ℝ := + (totals slots eligible weight).max' (totals_nonempty slots eligible weight) + +theorem sum_le_bestSum (slots : ℕ) (eligible picks : Finset Id) (weight : Id → ℝ) + (hsub : picks ⊆ eligible) (hsize : picks.card ≤ slots) : + (∑ id ∈ picks, weight id) ≤ bestSum slots eligible weight := by + apply Finset.le_max' + exact Finset.mem_image.mpr + ⟨picks, (FiniteBounds.mem_selections _ _ _).mpr ⟨hsub, hsize⟩, rfl⟩ + +theorem bestSum_attained (slots : ℕ) (eligible : Finset Id) (weight : Id → ℝ) : + ∃ picks ⊆ eligible, picks.card ≤ slots ∧ (∑ id ∈ picks, weight id) = bestSum slots eligible weight := by + have h := Finset.max'_mem (totals slots eligible weight) (totals_nonempty slots eligible weight) + rcases Finset.mem_image.mp h with ⟨picks, hp, heq⟩ + rcases (FiniteBounds.mem_selections _ _ _).mp hp with ⟨hsub, hsize⟩ + exact ⟨picks, hsub, hsize, heq⟩ + +theorem bestSum_nonneg (slots : ℕ) (eligible : Finset Id) (weight : Id → ℝ) : + 0 ≤ bestSum slots eligible weight := by + simpa using sum_le_bestSum slots eligible ∅ weight (Finset.empty_subset _) (by simp) + +theorem bestSum_mono_pool (slots : ℕ) (weight : Id → ℝ) + {small large : Finset Id} (h : small ⊆ large) : + bestSum slots small weight ≤ bestSum slots large weight := by + rcases bestSum_attained slots small weight with ⟨picks, hp, hs, heq⟩ + rw [← heq] + exact sum_le_bestSum slots large picks weight (hp.trans h) hs + +theorem bestSum_mono_weight (slots : ℕ) (eligible : Finset Id) (a b : Id → ℝ) + (h : ∀ id ∈ eligible, a id ≤ b id) : bestSum slots eligible a ≤ bestSum slots eligible b := by + rcases bestSum_attained slots eligible a with ⟨picks, hp, hs, heq⟩ + rw [← heq] + exact (Finset.sum_le_sum (fun id hi => h id (hp hi))).trans + (sum_le_bestSum slots eligible picks b hp hs) + +theorem bestSum_mono_slots (eligible : Finset Id) (weight : Id → ℝ) + {small large : ℕ} (h : small ≤ large) : + bestSum small eligible weight ≤ bestSum large eligible weight := by + rcases bestSum_attained small eligible weight with ⟨picks, hp, hs, heq⟩ + rw [← heq] + exact sum_le_bestSum large eligible picks weight hp (hs.trans h) + +/-- Excluding more main-deck public IDs never increases remaining support. -/ +theorem prefix_exclusion [DecidableEq Id] (pool : Finset Id) (weight : Id → ℝ) (slots : ℕ) + {selected complete : Finset Id} (h : selected ⊆ complete) : + bestSum slots (pool \ complete) weight ≤ bestSum slots (pool \ selected) weight := by + apply bestSum_mono_pool + intro id hi + rcases Finset.mem_sdiff.mp hi with ⟨hp, hn⟩ + exact Finset.mem_sdiff.mpr ⟨hp, fun hs => hn (h hs)⟩ + +/-- A per-ID maximum over leader profiles, with a maximum slot count, is an +upper bound even when the selected maxima come from incompatible profiles. -/ +theorem leader_profile_envelope (pool : Finset Id) (weight envelope : Id → ℝ) + (slots maxSlots : ℕ) (hs : slots ≤ maxSlots) (hw : ∀ id ∈ pool, weight id ≤ envelope id) : + bestSum slots pool weight ≤ bestSum maxSlots pool envelope := + (bestSum_mono_weight slots pool weight envelope hw).trans (bestSum_mono_slots pool envelope hs) + +/-- Threshold form of a top-r certificate. Both cardinality and the ordering +of UNCHOSEN entries matter; merely counting r chosen entries is not enough. -/ +theorem sorted_prefix_dominates [DecidableEq Id] (chosen picks : Finset Id) (weight : Id → ℝ) (cutoff : ℝ) + (hsize : picks.card ≤ chosen.card) (hc : 0 ≤ cutoff) + (hchosen : ∀ id ∈ chosen, cutoff ≤ weight id) + (houtside : ∀ id ∈ picks, id ∉ chosen → weight id ≤ cutoff) : + (∑ id ∈ picks, weight id) ≤ ∑ id ∈ chosen, weight id := by + classical + let common := picks ∩ chosen + have hsplitP : (∑ id ∈ picks \ chosen, weight id) + (∑ id ∈ common, weight id) = + ∑ id ∈ picks, weight id := by + exact sum_split picks chosen weight + have hsplitC : (∑ id ∈ chosen \ picks, weight id) + (∑ id ∈ common, weight id) = + ∑ id ∈ chosen, weight id := by + simpa [common, Finset.inter_comm] using sum_split chosen picks weight + have hcardP := Finset.card_sdiff_add_card_inter picks chosen + have hcardC := Finset.card_sdiff_add_card_inter chosen picks + have hcard : (picks \ chosen).card ≤ (chosen \ picks).card := by + rw [Finset.inter_comm chosen picks] at hcardC + omega + have hcardR : ((picks \ chosen).card : ℝ) ≤ (chosen \ picks).card := by exact_mod_cast hcard + have hupper : (∑ id ∈ picks \ chosen, weight id) ≤ (picks \ chosen).card * cutoff := by + calc + (∑ id ∈ picks \ chosen, weight id) ≤ ∑ _id ∈ picks \ chosen, cutoff := by + apply Finset.sum_le_sum + intro id hi + rcases Finset.mem_sdiff.mp hi with ⟨hp, hn⟩ + exact houtside id hp hn + _ = (picks \ chosen).card * cutoff := by simp + have hlower : (chosen \ picks).card * cutoff ≤ ∑ id ∈ chosen \ picks, weight id := by + calc + (chosen \ picks).card * cutoff = ∑ _id ∈ chosen \ picks, cutoff := by simp + _ ≤ ∑ id ∈ chosen \ picks, weight id := + Finset.sum_le_sum (fun id hi => hchosen id (Finset.mem_sdiff.mp hi).1) + have hmul := mul_le_mul_of_nonneg_right hcardR hc + linarith + +/-- Gain above the support cutoff. The algebra works with fractional values. -/ +noncomputable def gain (value cutoff : ℝ) : ℝ := max 0 (value - cutoff) + +theorem gain_gap (a b cutoff : ℝ) : gain a cutoff - gain b cutoff ≤ max 0 (a - b) := by + have h0 : 0 ≤ max 0 (b - cutoff) + max 0 (a - b) := + add_nonneg (le_max_left _ _) (le_max_left _ _) + have ha : a - cutoff ≤ max 0 (b - cutoff) + max 0 (a - b) := by + linarith [le_max_right 0 (b - cutoff), le_max_right 0 (a - b)] + have h := max_le h0 ha + unfold gain + linarith + +/-- The rank-derived floor f only strengthens the loss bound in the b round (sum + value)) oldStart ≤ + new.foldl (fun sum value => round (sum + value)) newStart := by + induction hvalues generalizing oldStart newStart with + | nil => exact hstart + | cons hvalue htail ih => + exact ih _ _ (hround (add_le_add hstart hvalue)) + +end Allium.Support diff --git a/formal/lean/Allium/TopK.lean b/formal/lean/Allium/TopK.lean new file mode 100644 index 0000000..2aafaf7 --- /dev/null +++ b/formal/lean/Allium/TopK.lean @@ -0,0 +1,175 @@ +import Mathlib.Data.Finset.Sort +import Mathlib.Data.Finset.Image +import Mathlib.Tactic + +/-! +# Canonical Top-K with public-set identity + +The order on `Candidate` is the complete better-first order, NOT just the +numeric objective. `identity` identifies the public card set; cultivation +variants and placements remain distinct candidates until collection. + +`topK` is specified by best representatives and a count of DISTINCT preceding +identities. The coverage theorem is the reusable exactness argument: a search +must either retain a no-worse representative of the same identity, or exhibit +K distinct retained identities strictly better than the discarded candidate. +No bound soundness or search exactness is assumed by this theorem. + +Source correspondence: search/tracker.rs; pruning-proof sections 1, 6, 13, 22. +-/ + +namespace Allium + +variable {Candidate Identity : Type*} [LinearOrder Candidate] [DecidableEq Identity] + +/-- Public identities with at least one strictly better concrete candidate. -/ +def earlierIds (identity : Candidate → Identity) (pool : Finset Candidate) + (candidate : Candidate) : Finset Identity := + (pool.filter (fun other => other < candidate)).image identity + +/-- The canonical representatives whose distinct-public-set rank is below K. -/ +noncomputable def topK (identity : Candidate → Identity) (k : ℕ) + (pool : Finset Candidate) : Finset Candidate := by + classical + exact pool.filter (fun candidate => + (∀ other ∈ pool, identity other = identity candidate → candidate ≤ other) ∧ + (earlierIds identity pool candidate).card < k) + +@[simp] theorem mem_topK (identity : Candidate → Identity) (k : ℕ) + (pool : Finset Candidate) (candidate : Candidate) : + candidate ∈ topK identity k pool ↔ + candidate ∈ pool ∧ + (∀ other ∈ pool, identity other = identity candidate → candidate ≤ other) ∧ + (earlierIds identity pool candidate).card < k := by + classical + simp [topK] + +@[simp] theorem mem_earlierIds (identity : Candidate → Identity) + (pool : Finset Candidate) (candidate : Candidate) (key : Identity) : + key ∈ earlierIds identity pool candidate ↔ + ∃ other ∈ pool, other < candidate ∧ identity other = key := by + simp only [earlierIds, Finset.mem_image, Finset.mem_filter] + aesop + +theorem earlierIds_mono_pool (identity : Candidate → Identity) + {small large : Finset Candidate} (h : small ⊆ large) (candidate : Candidate) : + earlierIds identity small candidate ⊆ earlierIds identity large candidate := by + intro key hk + rcases (mem_earlierIds _ _ _ _).mp hk with ⟨other, ho, hc, rfl⟩ + exact (mem_earlierIds _ _ _ _).mpr ⟨other, h ho, hc, rfl⟩ + +theorem earlierIds_mono_key (identity : Candidate → Identity) + (pool : Finset Candidate) {a b : Candidate} (h : a ≤ b) : + earlierIds identity pool a ⊆ earlierIds identity pool b := by + intro key hk + rcases (mem_earlierIds _ _ _ _).mp hk with ⟨other, ho, hc, rfl⟩ + exact (mem_earlierIds _ _ _ _).mpr ⟨other, ho, lt_of_lt_of_le hc h, rfl⟩ + +/-- A certificate for omitting one concrete candidate. -/ +def Covered (identity : Candidate → Identity) (k : ℕ) + (retained : Finset Candidate) (candidate : Candidate) : Prop := + (∃ other ∈ retained, identity other = identity candidate ∧ other ≤ candidate) ∨ + k ≤ (earlierIds identity retained candidate).card + +theorem covered_of_mem (identity : Candidate → Identity) (k : ℕ) + {retained : Finset Candidate} {candidate : Candidate} (h : candidate ∈ retained) : + Covered identity k retained candidate := + Or.inl ⟨candidate, h, rfl, le_rfl⟩ + +theorem covered_mono (identity : Candidate → Identity) (k : ℕ) + {small large : Finset Candidate} (h : small ⊆ large) {candidate : Candidate} + (hc : Covered identity k small candidate) : Covered identity k large candidate := by + rcases hc with ⟨other, ho, hi, hv⟩ | hr + · exact Or.inl ⟨other, h ho, hi, hv⟩ + · exact Or.inr (hr.trans (Finset.card_le_card (earlierIds_mono_pool identity h candidate))) + +/-- Replacing a pool by a valid coverage certificate preserves the full Top-K, +including placement/variant representatives and all equal-score ties. -/ +theorem coverage_exactness (identity : Candidate → Identity) (k : ℕ) + {full retained : Finset Candidate} (hsub : retained ⊆ full) + (hcover : ∀ candidate ∈ full, Covered identity k retained candidate) : + topK identity k retained = topK identity k full := by + classical + ext candidate + rw [mem_topK, mem_topK] + constructor + · rintro ⟨hmem, hbest, hrank⟩ + have lift (other : Candidate) (ho : other ∈ full) (hord : other ≤ candidate) : + ∃ replacement ∈ retained, + identity replacement = identity other ∧ replacement ≤ other := by + rcases hcover other ho with h | h + · exact h + · have hle := Finset.card_le_card (earlierIds_mono_key identity retained hord) + exact False.elim (Nat.not_le_of_lt hrank (h.trans hle)) + have hbestFull : ∀ other ∈ full, + identity other = identity candidate → candidate ≤ other := by + intro other ho hi + by_contra hnot + have hlt : other < candidate := lt_of_not_ge hnot + rcases lift other ho hlt.le with ⟨replacement, hm, hid, hv⟩ + have hc := hbest replacement hm (hid.trans hi) + exact (not_lt_of_ge (hc.trans hv)) hlt + have hbefore : earlierIds identity full candidate ⊆ + earlierIds identity retained candidate := by + intro key hk + rcases (mem_earlierIds _ _ _ _).mp hk with ⟨other, ho, hv, hid⟩ + rcases lift other ho hv.le with ⟨replacement, hm, hi, hr⟩ + exact (mem_earlierIds _ _ _ _).mpr + ⟨replacement, hm, lt_of_le_of_lt hr hv, hi.trans hid⟩ + exact ⟨hsub hmem, hbestFull, + lt_of_le_of_lt (Finset.card_le_card hbefore) hrank⟩ + · rintro ⟨hmem, hbest, hrank⟩ + have hretained : candidate ∈ retained := by + rcases hcover candidate hmem with ⟨other, ho, hi, hv⟩ | h + · have heq : other = candidate := le_antisymm hv (hbest other (hsub ho) hi) + simpa only [heq] using ho + · have hle := Finset.card_le_card (earlierIds_mono_pool identity hsub candidate) + exact False.elim (Nat.not_le_of_lt hrank (h.trans hle)) + exact ⟨hretained, fun other ho hi => hbest other (hsub ho) hi, + lt_of_le_of_lt + (Finset.card_le_card (earlierIds_mono_pool identity hsub candidate)) hrank⟩ + +theorem topK_subset (identity : Candidate → Identity) (k : ℕ) + (pool : Finset Candidate) : topK identity k pool ⊆ pool := by + intro candidate hc + exact ((mem_topK _ _ _ _).mp hc).1 + +/-- Deduplication is by identity, not by objective or concrete variant. -/ +theorem topK_identity_injective (identity : Candidate → Identity) (k : ℕ) + (pool : Finset Candidate) : Set.InjOn identity (topK identity k pool) := by + intro a ha b hb hab + rcases (mem_topK _ _ _ _).mp ha with ⟨ham, habest, _⟩ + rcases (mem_topK _ _ _ _).mp hb with ⟨hbm, hbbest, _⟩ + exact le_antisymm (habest b hbm hab.symm) (hbbest a ham hab) + +/-- Sorting the proven set gives exactly the same canonical result sequence. -/ +theorem coverage_canonical_sequence (identity : Candidate → Identity) (k : ℕ) + {full retained : Finset Candidate} (hsub : retained ⊆ full) + (hcover : ∀ candidate ∈ full, Covered identity k retained candidate) : + (topK identity k retained).sort (· ≤ ·) = + (topK identity k full).sort (· ≤ ·) := by + rw [coverage_exactness identity k hsub hcover] + +/-- Distinct already evaluated identities whose scores strictly exceed U. -/ +def strictWitnesses (identity : Candidate → Identity) (score : Candidate → ℕ) + (retained : Finset Candidate) (upper : ℕ) : Finset Identity := + (retained.filter (fun other => upper < score other)).image identity + +/-- The numeric prune uses STRICT comparison. The later key fields need no +assumption because a strict primary improvement decides the complete order. -/ +theorem strict_upper_prune (identity : Candidate → Identity) (score : Candidate → ℕ) + (horder : ∀ a b, score b < score a → a < b) (k : ℕ) + (retained : Finset Candidate) (candidate : Candidate) (upper : ℕ) + (hsound : score candidate ≤ upper) + (hwitness : k ≤ (strictWitnesses identity score retained upper).card) : + Covered identity k retained candidate := by + apply Or.inr + apply hwitness.trans + apply Finset.card_le_card + intro key hk + rcases Finset.mem_image.mp hk with ⟨other, ho, hi⟩ + rcases Finset.mem_filter.mp ho with ⟨hm, hv⟩ + exact (mem_earlierIds _ _ _ _).mpr + ⟨other, hm, horder other candidate (lt_of_le_of_lt hsound hv), hi⟩ + +end Allium diff --git a/formal/lean/Audit.lean b/formal/lean/Audit.lean new file mode 100644 index 0000000..a87f3bc --- /dev/null +++ b/formal/lean/Audit.lean @@ -0,0 +1,43 @@ +import Allium +import Lean.Util.CollectAxioms + +/-! +Audit the TRANSITIVE axiom dependencies of every declaration in the Allium +namespace, not merely a hand-picked list of headline theorems. This also checks +definitions, so hiding a new axiom in an opaque helper does not evade the gate. +The three permitted axioms are Lean's standard propositional extensionality, +classical choice, and quotient soundness. Model premises remain visible in +theorem types: passing this audit does NOT discharge an unproved premise. +-/ + +open Lean Elab Command in +run_cmd do + let env ← getEnv + let allowed : List Name := [`propext, `Classical.choice, `Quot.sound] + let mut declarations := 0 + let mut theorems := 0 + for (name, info) in env.constants.toList do + if (`Allium).isPrefixOf name then + declarations := declarations + 1 + match info with + | .thmInfo _ => theorems := theorems + 1 + | _ => pure () + let axioms ← collectAxioms name + for axiomName in axioms do + unless allowed.contains axiomName do + throwError "AXIOM AUDIT FAILED: {name} depends on forbidden axiom {axiomName}" + if declarations == 0 || theorems == 0 then + throwError "AXIOM AUDIT FAILED: no Allium declarations/theorems were imported" + logInfo m!"AXIOM AUDIT PASSED: {declarations} declarations; {theorems} theorems; allowlist={allowed}" + +#print axioms Allium.coverage_exactness +#print axioms Allium.topK_card +#print axioms Allium.collect_exact +#print axioms Allium.group_topK_merge +#print axioms Allium.search_exact +#print axioms Allium.complete_exact +#print axioms Allium.FiniteBounds.character_bound_sound +#print axioms Allium.DP.compressed_reachable_covers +#print axioms Allium.Skill.reference_relax_sound +#print axioms Allium.Quadratic.joint_peak_sound +#print axioms Allium.Arithmetic.grid_floor_of_error diff --git a/formal/lean/README.md b/formal/lean/README.md new file mode 100644 index 0000000..6bf39da --- /dev/null +++ b/formal/lean/README.md @@ -0,0 +1,82 @@ +# Allium 的 Lean 数学证明 + +**状态：第一档部分完成，尚未完成全量验证。** 这里没有对当前 Rust 引擎作出“已经形式化验证”的声明。 + +代码对照基线为 `5c6dff7387e57384b9b2c989ab4f535cdd74f098`，即合并 PR #43 后的 main。Lean 工程不修改 Rust 搜索、评分、超时、服务器或 WASM 实现，也不改变它们的运行时依赖。 + +## 已经证明什么 + +所有下列模块都由 `Allium.lean` 导入并实际编译。它们包含有证明项的定理，不是 `sorry` 占位文件。 + +| 模块 | 已证明的数学内容 | +| --- | --- | +| `TopK`、`Collection`、`Canonical` | 公共卡组身份与具体养成/摆位身份分离；五字段完整顺序；结果数量为 `min(K, 不同公共卡组数)`；逐次插入截断不依赖插入顺序；局部 Top-K 合并等于全局 Top-K。 | +| `Search`、`Budget` | 一个实际定义的分支限界数学算法；严格上界剪枝；合法种子保留；遗漏叶子的覆盖证书；完整搜索精确；超时只能返回已访问合法候选，超时标志不能被后续分支清除。 | +| `Enumeration` | 五个有序槽位的独立合法性规范与完整有限枚举等价；固定角色位于固定卡牌之后；Final 的固定队长占据第 0 槽；同一卡牌的全部合法养成变体仍在枚举中。 | +| `FiniteBounds` | 不同角色的 Top-r 最大值松弛；可用角色不足的不可行性；独立分量上界；后缀缩小时的单调性；最大化/最小化的重复极值界；压缩上界状态的安全性。 | +| `Arithmetic` | 打包整数的字典序条件；严格阈值的整数除法等价；向上除法；上下界取交；有范围前提的安全截断及可选上界回退；严格误差小于网格间隙时的取整桥梁。 | +| `Skill` | `2 * sum + 8 * leader` 技能键；非单调人数技能表的前缀最大值；异单位数量上界；最大值/最小值/平均值参考技能；未知成员用 cap 放宽；参考规则的逐分量合并。 | +| `Quadratic` | 相关评分包络的两个分支；联合 power/skill 半平面；矩形与半平面相交后乘积峰值的四个分支。 | +| `DynamicProgramming` | 有限组选择的完整可达性；必须组与可跳过组的区别；保持精确 key 的逐分量最大值压缩；每一轮压缩后的覆盖不变量；键区间查询与不可达排除。 | +| `Support` | 有限支援池的最大和；主队排除集合增大时支援不增加；不同队长 profile 的逐 ID 最大值包络；排序前缀的阈值证书；替换损失的截止值代数；单调舍入加法下的逐项支配。 | +| `PowerModel` | 2×4 八槽索引；六单位计数等于五人的语义；任意非单调查表的上下界；selected/free 松弛；先加称号再应用 cap 的双向严格剪枝。低界保留非空单位集合前提。 | +| `Composition` | 全部 49 个区域场景的覆盖；语义归属与卡池接纳的区别；每个真实 member key 都在场景 key 集内；非单调八槽 power 上界。 | +| `ScenarioSearch` | 场景允许额外合法叶子时的 required-class 证明；跨场景共享阈值；种子可不属于当前场景；不要求每个场景的局部 Top-K 在外部阈值下保持不变。 | +| `ConcretePower` | 首个具体 Power 数学实例：五槽合法性 → 49 场景 → per-character/per-card 上界 → honor/cap → 共享阈值搜索 → canonical 穷举 Top-K，无抽象上界可靠性或覆盖前提。 | +| `ScenarioPower` | 专用 Power 场景的多单位 singleton envelope；空/单单位精确性；实际单位交集的接纳性；三个内核检查的反例，保护非单调、接纳性和空单位边界。 | + +这些是数学机制的证明。表中出现一个辅助机制，不代表使用它的整个 Rust 函数、场景或所有前提已经证明。 + +## 主定理及其边界 + +`Allium.search_exact` 证明：对满足 `SearchTree.Sound score` 的有限搜索树，合法种子驱动的分支限界结果与全部叶子的 canonical Top-K 完全相同。这里的 `score` 必须和候选完整顺序的主目标一致。 + +`Allium.complete_exact` 将结论扩展到有中断检查的算法，但要求实际返回 `deadlineHit = false`。`TimedOut` 分支只有合法性结论，不能因此宣称精确 Top-K。 + +`SearchTree.Sound` **是待实例化的前提，不是已经验证所有生产上界的同义词**。当前尚未把各个 Allium 场景的完整评分、合法完成集合和每一个启用剪枝全部连接到该前提。这个连接仍属于第一档，而不是可以推迟到 Rust refinement 的工作。 + +第二轮新增 `Allium.ConcretePower.power_search_exact`：对 `Enumeration.Roles` 定义的五槽规范，使用实际八槽 power 数学公式构造 49 个场景并完成共享阈值搜索，其结果等于 `Enumeration.exhaustiveKeys` 的 canonical Top-K。它仅要求初始种子属于合法候选；上界、场景覆盖及叶子合法性全部在该实例内部证明，不再由调用者提供 `SearchTree.Sound`。 + +这里必须使用 `ScenarioSearch.RequiredSound`：卡牌通过某个场景的过滤，不代表完整卡组真的属于该场景。场景可以访问额外的合法叶子，但只对自己负责的候选承诺上界；各场景负责的候选并集覆盖全部合法答案。`ScenarioPower.admission_is_not_bound_soundness` 给出了不能混淆两者的机器检查反例。 + +**这个 Power 实例仍不是全部生产 DFS 的证明。** 它显式枚举合法的 admitted leaves，验证场景级剪枝，而非声称证明所有后缀/DP/支配/同分 fast path 或实现性能；完整业务受理域与其他评分目标仍在 S05 中。第二轮结果与剩余工作见 [`ROUND2.md`](ROUND2.md)。 + +同样，`Arithmetic.grid_floor_of_error` 的严格误差前提必须独立证明。当前并没有从 `pruning-proof.md` 第 29 节的全部 binary64 表达式推导出 N1–N7 误差预算；不能把实数或有理数定理当作这一缺口的替代品。 + +## 逐项覆盖与剩余义务 + +[`coverage.json`](coverage.json) 按 [`pruning-proof.md` 第 26 节](../../docs/pruning-proof.md#26-proof-to-code-inventory) 原顺序列出全部 **41 个剪枝机制**，另列 canonical collection、数学搜索、超时、槽位枚举、全场景实例化和 Rust refinement 边界。每项给出对照源文件、已存在定理以及仍未证明的内容。 + +状态含义如下：`proved` 指该条明确陈述的数学机制已经证明；`partial` 指仅完成部分引理；`open` 指尚未证明；`out_of_scope` 仅用于第一档之外的 Rust 实现/编译等价。**覆盖行数和 Lean 定理行数不是“验证百分比”。** 当前 `stage_one_complete` 为 `false`。 + +尚未闭合的主要内容包括完整支配守卫与 Top-K 逆恢复、49-regime 的其余评分目标连接与专用 Power unit-set 工作表/同分剪枝、精确 bonus-tier 的 first-N/key/slack/refill/certificate 构造、Final 与 WL 的完整场景连接、对数弦界及向外区间/atanh 余项证明、全部评分目标的浮点误差预算。清单中的每项都保留具体缺口，不用未经证明的假设冒充完成。 + +Rust 的内存安全、缓存一致性、数据读取、机器指令、编译器、WASM，以及 `RustSearch = LeanSpec` 的 refinement 不属于本轮第一档声明。 + +## 复现检查 + +需要 Elan/Lean 和 Python 3.11 或更新版本。工具链固定在 Lean `v4.24.0`；Mathlib 固定到 `f897ebcf72cd16f89ab4577d0c826cd14afaafc7`，其依赖由 `lake-manifest.json` 锁定。 + +```sh +cd formal/lean +lake exe cache get +python verify.py --self-test +``` + +验证脚本检查对照源文件的 SHA-256、全部模块导入、覆盖表引用的定理名、整库编译，以及所有 `Allium` 声明的传递公理依赖。Windows 的 CRLF 与 Linux 的 LF 仅作换行归一化，不忽略其他源码变化。 + +公理允许列表只有 `propext`、`Classical.choice`、`Quot.sound`。负向测试实际注入四类错误并要求检查失败：`sorry`、通过外部辅助声明引入的自定义公理、尚未使用的本地公理、`native_decide` 的求值公理。普通 `decide` 产生可由内核检查的证明，与 `native_decide` 的信任路径不同。 + +要检查是否达到第一档全量完成，执行： + +```sh +python verify.py --require-complete +``` + +**当前这条命令应当失败并列出未完成义务。** 普通 CI 通过只表示“声明范围内的证明与审计通过”，不表示全部生产搜索已验证。验证脚本还会拒绝从第 26 节清单中删去剪枝机制，或将第一档数学义务改成 `out_of_scope`；这两种情况也有负向测试。 + +## 修改与信任范围 + +源文件哈希变化会使验证脚本失败。应先审查差异，修改相关模型/证明并核对覆盖义务，再更新对照哈希。仅重算哈希不能证明新代码正确。 + +可信基础包括 Lean 内核、标准公理、固定依赖与实际运行的工具链。公理审计能检查证明依赖，不能替代对定理陈述是否对应游戏规则、前提是否充分、模型是否连接到实际场景的审查。本文和覆盖表刻意保留这些区别。 diff --git a/formal/lean/ROUND2.md b/formal/lean/ROUND2.md new file mode 100644 index 0000000..9dc3ca0 --- /dev/null +++ b/formal/lean/ROUND2.md @@ -0,0 +1,103 @@ +# 第二轮：具体 Power 场景与共享阈值证明 + +日期：2026-09-29。继续 Draft PR #44 的 `formal/lean-core-20260929` 分支；本轮起点是 `769f704deeb291ad1c124bc2dcd3c24afb9cf434`。对照 Rust 仍为 `5c6dff7387e57384b9b2c989ab4f535cdd74f098`，31 个对照文件的哈希未改动。 + +**结论：首个具体 Power 数学实例已经闭合；第一档全量证明仍未完成。** 没有修改 Rust 搜索或运行时依赖，没有合并 main，也没有把剩余第一档义务改名为 Rust refinement。 + +## 这次推进了什么 + +新增 5 个模块、41 条显式定理、784 行 `Allium/*.lean` 源码。现在共有 17 个证明模块、172 条显式定理、2,708 行模块源码。数量不代表完成百分比；自动生成的辅助定理另由公理审计计数。 + +### 具体 Power 主定理 + +[`ConcretePower.power_search_exact`](Allium/ConcretePower.lean) 证明：对 `Enumeration.Roles` 定义的五个有序槽位、公开卡牌去重、可选角色去重和队长条件，49 个场景的数学搜索输出与 `Enumeration.exhaustiveKeys` 的 canonical Top-K 完全相同。 + +这个实例的目标值实际定义为： + +```text +每张卡：扫描它携带的单位 + → 用单位 profile、是否全队同单位、是否全队同属性选择八槽表项 + → 取该卡扫描结果的最大值 +全队：五张卡求和 + honor + → 可选 total-power cap +``` + +八槽表允许任意非负数值，不假设“人数/属性加成越多，power 必然越高”。`PowerModel.count_five_iff_common` 和 `attribute_count_five` 把五人成员计数判断连接到单位交集及同属性条件。 + +主定理不接受 `SearchTree.Sound`、`score ≤ upper` 或“场景已经完整覆盖”作为外部前提。它在内部证明： + +- 所有合法卡组至少属于一个真实场景，且不会被该场景的接纳过滤排除。 +- 每个真实 member key 都被其场景的 key 集覆盖；由此直接推导 power 上界。 +- 角色去重开启时使用 per-character top-five 上界，关闭时使用 per-card top-five 上界；上界不是通过计算全部完整卡组的最高分取得的。 +- honor 与 cap 保持上界，共享 tracker 的严格阈值保留 canonical Top-K；K=0、同分、跨场景相同公共卡组和养成/摆位变体由同一框架处理。 + +初始种子的唯一额外要求是属于合法候选集合。空种子自动满足它。 + +**不能扩大这个结论：** `ConcretePower` 显式构造 admitted 合法叶子列表，证明的是带场景级剪枝的数学实现，不是所有生产 DFS 优化，也不提供性能结论。`Enumeration.Roles` 与全部受理域/特殊固定角色语义的连接，以及其他评分目标，仍在 S05 的分母内。 + +### 不把场景接纳与场景归属混为一谈 + +[`Composition`](Allium/Composition.lean) 定义了两个不同关系：`Admits` 是卡牌层面的宽松池过滤，`Matches` 是完整卡组的真实场景归属。 + +生产场景可能访问额外的合法卡组。对非单调查表，不能要求该场景的上界支配所有这些额外卡组，否则证明前提本身就不对。新增 [`ScenarioSearch.RequiredSound`](Allium/ScenarioSearch.lean) 只要求上界支配本场景负责的叶子，同时要求所有实际访问叶子全局合法。 + +`required_search_spec` 直接复用原有 `Allium.search`，证明它保留 required 候选的覆盖；`runScenes_exact` 再证明多个重叠场景共享 tracker 后的全局 Top-K 精确性。种子或阈值见证不需要属于当前场景，也不假定外部阈值下每个场景还会输出自己的局部 Top-K。 + +这不是报告一个已确认的 Rust 错误，而是补上此前通用搜索定理不足以直接描述的数学边界。 + +### Power 上下界与专用场景 envelope + +[`PowerModel`](Allium/PowerModel.lean) 证明八槽最大值上界、非空单位集合下的最小值下界、selected/free 组合，以及先加 honor 再应用 cap 的最大化 `< threshold` 和最小化 `> threshold` 剪枝。 + +[`ScenarioPower`](Allium/ScenarioPower.lean) 单独建模 `solver/power.rs::scenario_power`：空公共单位集合和单单位时精确；多个公共单位时，对单单位假设取最大值得到可靠上界。这个 envelope 与 `Composition.powerBound` 不是同一个公式。 + +三个静态反例均通过普通 `decide` 生成内核检查的证明，不使用 `native_decide`： + +1. 多单位真实值为 20，但 singleton envelope 为 100：它只能作上界，不能替代叶子回算。 +2. 卡牌被 Mixed 场景接纳，其 Mixed 上界为 1，但同单位同属性上下文的真实值为 100：接纳不是上界可靠性。 +3. 空单位扫描返回 0，而人为给定的八个表项都为 1：低界不能无条件删除非空单位前提。 + +第三项是解码后数学模型的边界反例，不足以单独断言这个表能由受理输入/压缩构造产生。该构造连接仍明确保留在 P36，未据此声称发现可触发的生产 bug。 + +## 实际验证 + +Windows 使用固定 Lean `v4.24.0`、固定 Mathlib 提交 `f897ebcf72cd16f89ab4577d0c826cd14afaafc7` 和 Python 3.14.7。 + +```sh +cd formal/lean +python verify.py --self-test +``` + +本轮实际返回 exit code 0： + +```text +SOURCE CHECK PASSED: 31 files; 17 imported proof modules +COVERAGE open: 13 +COVERAGE out_of_scope: 1 +COVERAGE partial: 27 +COVERAGE proved: 6 +STAGE ONE COMPLETE: False +Build completed successfully (3105 jobs). +AXIOM AUDIT PASSED: 591 declarations; 332 theorems +NEGATIVE AUDIT TEST PASSED: sorry +NEGATIVE AUDIT TEST PASSED: foreign-axiom +NEGATIVE AUDIT TEST PASSED: unused-local-axiom +NEGATIVE AUDIT TEST PASSED: native-decide +NEGATIVE COVERAGE TEST PASSED: omitted-pruning-mechanism +NEGATIVE COVERAGE TEST PASSED: excluded-mathematical-obligation +VERIFICATION PASSED FOR THE DECLARED SCOPE (see coverage.json) +``` + +公理允许列表仍只有 `propext`、`Classical.choice`、`Quot.sound`。检查器、允许列表、负向测试、对照哈希和 CI 判定逻辑均未放宽。`git diff --check` 通过。 + +`python verify.py --require-complete` 已实际运行并返回 exit code 1；构建和公理审计通过后，它明确列出 40 项 `partial/open` 义务并拒绝全量完成声明。远端 Linux 与 commitlint 的状态应按本轮提交的 GitHub Actions 结果检查，不能用上一轮的绿灯代替。 + +## 覆盖变化与尚未闭合的工作 + +`coverage.json` 保留全部 41 个原始剪枝机制与原顺序。P18、P38、S05 从 `open` 改为 `partial`，P36 的已证明内容和剩余条件细化；没有把任何整项提前标成 `proved`。 + +因此当前是 **6 proved / 27 partial / 13 open / 1 out_of_scope**。40 个第一档未闭合条目数量未变；它们粒度不同，本轮完成的是其中实质性的子义务，不能按行数换算完成率。 + +下一批数学连接已经具体到：专用 Power 的 unit-mask 交集工作表完整性、`best_completion` 扫描、least/cap 守卫下的同分公共集合剪枝；numeric 受理域和摘要/固定槽对应；普通/WL/Final 各目标的完整 RegimePlan 特征与评分表达式。支配逆恢复、bonus-tier/refill/certificate、Final/WL 其余剪枝、对数与区间余项、binary64 N1–N7 预算也都继续保留。 + +这份记录只证明上述已检查的声明，不宣称当前 Rust 二进制、WASM 或全部组卡模式已经形式化验证。 diff --git a/formal/lean/VALIDATION.md b/formal/lean/VALIDATION.md new file mode 100644 index 0000000..6fee18e --- /dev/null +++ b/formal/lean/VALIDATION.md @@ -0,0 +1,54 @@ +# 验证记录：2026-09-29 + +本记录对应本目录的数学证明，不是 Rust 全场景精确性或二进制 refinement 证书。对照源代码基线：`5c6dff7387e57384b9b2c989ab4f535cdd74f098`。 + +## 实际执行 + +执行环境为 Windows x86-64，Lean `4.24.0`（提交 `797c613eb9b6d4ec95db23e3e00af9ac6657f24b`）、Mathlib `f897ebcf72cd16f89ab4577d0c826cd14afaafc7`、Python `3.14.7`。依赖提交由 `lake-manifest.json` 固定。证明与依赖在独立工作目录中构建；没有修改 Rust 源码或 Cargo 依赖。 + +```text +python verify.py --self-test + +SOURCE CHECK PASSED: 31 files; 12 imported proof modules +COVERAGE open: 16 +COVERAGE out_of_scope: 1 +COVERAGE partial: 24 +COVERAGE proved: 6 +STAGE ONE COMPLETE: False +Build completed successfully (3100 jobs). +AXIOM AUDIT PASSED: 404 declarations; 254 theorems; + allowlist=[propext, Classical.choice, Quot.sound] +NEGATIVE AUDIT TEST PASSED: sorry +NEGATIVE AUDIT TEST PASSED: foreign-axiom +NEGATIVE AUDIT TEST PASSED: unused-local-axiom +NEGATIVE AUDIT TEST PASSED: native-decide +NEGATIVE COVERAGE TEST PASSED: omitted-pruning-mechanism +NEGATIVE COVERAGE TEST PASSED: excluded-mathematical-obligation +VERIFICATION PASSED FOR THE DECLARED SCOPE (see coverage.json) +``` + +上面的 `3100 jobs` 是包括依赖在内的 Lake 构建任务数，不是证明数量。公理审计的 `254 theorems` 包括 Lean 自动生成的辅助定理。`Allium/` 中实际有 **131 条显式 theorem 声明，12 个模块，共 1,924 行源码**；行数包含定义、证明和注释，不代表覆盖率。 + +负向测试不是简单搜索文本，而是把临时错误声明注入已导入的 Lean 环境，再要求传递公理审计实际拒绝它们。测试文件放在临时目录，未作为公理加入正式证明库。 + +`coverage.json` 中引用的每个定理名还通过 Lean 的 `#check` 验证存在。所有证明模块都必须在 `Allium.lean` 中导入，遗漏文件会在构建前失败。 + +## 未完成部分不会被绿灯隐藏 + +41 个原有剪枝机制对应 `P01` 至 `P41`，另外六项说明收集器、搜索、超时、枚举、全场景实例化和 Rust refinement 边界。当前有 24 项部分完成、16 项尚未证明。这些项目的规模并不相同，不能将这些数字换算为形式化验证百分比。 + +已实际运行 `python verify.py --require-complete`，在构建和公理审计通过后以退出码 1 拒绝全量完成声明，明确列出 40 项部分完成/未证明义务。尤其 `S05`——将各场景的评分、枚举和每一个剪枝连接到 `search_exact` 的前提——仍是第一档的未完成工作，不属于可排除的 Rust refinement。 + +## CI + +`.github/workflows/lean.yml` 在 Linux 上运行同一构建与 `--self-test` 检查。工作流的实际运行结果以对应 PR 的 GitHub Actions 日志为准；本记录不把本地成功写成未经执行的远端成功。 + +本轮本地未重新运行 Rust 单测、穷举矩阵或性能测试，不引用历史测试数量作为本轮结果。仓库原有的 Rust CI 保持不变。 + +## 第二轮追加记录（2026-09-29） + +此前内容保留为第一轮记录。当前第二轮的证明范围、命令输出、机器检查反例与明确剩余义务见 [ROUND2.md](ROUND2.md)。 + +第二轮新增 5 个模块、41 条显式定理；累计 17 个模块、172 条显式定理、2,708 行模块源码。`python verify.py --self-test` 实际通过：31 个对照源文件、全部 17 个模块、公理审计（591 declarations / 332 含自动生成项的 theorems）与六项负向测试全部通过。`python verify.py --require-complete` 实际返回 1，并在构建/审计通过后列出 40 项未完成义务。 + +本轮闭合的是 `ConcretePower.power_search_exact` 所陈述的具体五槽 Power 数学实例，不是全部生产 DFS、所有目标或 Rust refinement。覆盖状态为 6 proved / 27 partial / 13 open / 1 out_of_scope；`stage_one_complete` 仍为 false，PR 保持 Draft。 diff --git a/formal/lean/coverage.json b/formal/lean/coverage.json new file mode 100644 index 0000000..4204216 --- /dev/null +++ b/formal/lean/coverage.json @@ -0,0 +1,774 @@ +{ + "schema": 1, + "baseline_commit": "5c6dff7387e57384b9b2c989ab4f535cdd74f098", + "source_normalization": "UTF-8 source bytes with CRLF normalized to LF; SHA-256", + "inventory": "docs/pruning-proof.md section 26; P01..P41 preserve row order", + "stage_one_complete": false, + "status_meaning": { + "proved": "The stated mathematical mechanism is proved, not Rust refinement.", + "partial": "Some component lemmas are proved; explicit mathematical work remains.", + "open": "This mathematical obligation has not been proved.", + "out_of_scope": "Not part of first-tier mathematical verification." + }, + "sources": { + "docs/exactness-proof.md": "3d029cbd293d82a1ab473eca01891148d1a96a5ab6212d0d1516c0a414221337", + "docs/pruning-proof.md": "654daec45043d02f8e744718c33bda1387229092a87f2806ecc3218c5d24bd56", + "src/handler/build.rs": "7ff56fc78e299b2eb31dd69481db6b2938d2ab1da0bce612181f8170cea002c8", + "src/handler/capacity.rs": "44572e898ee231d261444ade8960ca35d3842411cea1a5baf2565ee4f8105709", + "src/handler/filter.rs": "38e84afa3a02dd263c18ddab26ae2d81fa6c038d1b4887c81993a8d7755e9370", + "src/handler/validate.rs": "f83d60a734b3aa9752a9f230ce0ce13643c85231ba683871216e06d009de15a3", + "src/pool/card_pool.rs": "d1f9509ae010f8b6c7944cf20de6ebd133fa7ff87d8a9e128870264a0358773a", + "src/search/alternatives.rs": "ae3b614dd7316a7170cc58bba65359d7de8dc59efb17747d9a470e13f3d90bd9", + "src/search/budget.rs": "e8dbe903ea2d4524616d9ca5dfc35c16f599365f62b4f410344ae4af02b26d10", + "src/search/composition.rs": "29c1bf14dc8afa5b0bc8f163e274fc691a00892acac8676eecbaba72812515a3", + "src/search/context.rs": "c7f0f698618d0d1f7aa71eb90a8feee396a0a291aa1b83f40951e3589a072687", + "src/search/correlated.rs": "37807a4f783b3365df7d2c00ba03ceaf3aa04d4b95a4c3fc7fe8caeff39d9abe", + "src/search/dfs.rs": "5c68865d3e723dcdc03c092a2496ec93a1a8f5b927e1f8e4c157ac6e82ac3e55", + "src/search/dominance.rs": "70986e344848efcc296950ae4d6e31e685c8dd4d7e3c4f24dd1486658a2e5a17", + "src/search/evaluate.rs": "397c1a90507b1ba0a2fab16d28053d22debe16e51ee801f106c3fd567cb8216b", + "src/search/log_linear.rs": "f3f99d9994c8a1731feeefa6b1d695d1afadad1e6bd447b923b22ee9e1bd37d8", + "src/search/log_linear/interval.rs": "3ad99ebc2649f71b99936ae276a372836407cf3d48530b6617d3f46fddae1b45", + "src/search/objective.rs": "25cca846cfc78fd3459806a32b6b7b9e32f5578ea0157f294c55f073668edc73", + "src/search/placement.rs": "b9ca952ef4d0d5ad72d1c2a3e3e9b2158e6524f10c81d2b2edb4f3a3296ad33b", + "src/search/problem.rs": "4f566d0c353d32e532bf37888eaab4118deaebb0c0a66862762fd91914ebb5f7", + "src/search/skill_ceiling.rs": "7754510f4e6d8a5d22ec617dff2309c36a49b81b60fe366b813d89d3ad793823", + "src/search/solver/bonus_tiers.rs": "83d637779f7c15515ff68281cbcb2282311c30658da45f20689cd117153a9574", + "src/search/solver/challenge.rs": "752b98922553ec498684c2ad948af34d3fe463703aa2a007f3f9a3624aea7ae9", + "src/search/solver/final_chapter.rs": "8a9c6b7e649bdef0cc073671b90380d47cdbf3de484ea977700e5ad0ec4b8450", + "src/search/solver/mod.rs": "d37f90c2a5f82791debd9e1c4e1b7260cba5e2a18701bb986e6a631a8eca7a4c", + "src/search/solver/numeric.rs": "dea69d0a3cac8821637588d453f93daa0f79f97fd10f81319c608cc1bfc09eae", + "src/search/solver/power.rs": "8eb79c577f05cff2786eb438a4679855b72c5847dc1bd96136d7e2c114b9a116", + "src/search/suffix.rs": "aac6deb47d759cae202502e36ec8526cbafe450c4fc48c020ff16172bfd916f5", + "src/search/tracker.rs": "3cbdd775eeda8b01e6b1b48dc2e56161605e4027ffa4e3631d019ef8a35d1a28", + "src/search/types.rs": "6dd1c41b4961dfb01df730cf23d310bf8953fa1bc880094cb975a416fa5d81e8", + "src/simd.rs": "948e4b7be60c519bdecaba84b8625de64d376b022a1a38071d213effc2c87687" + }, + "obligations": [ + { + "id": "P01", + "description": "Hard request filters", + "status": "partial", + "sources": [ + "src/handler/filter.rs", + "src/handler/build.rs" + ], + "theorems": [ + "Allium.Enumeration.exhaustive_complete", + "Allium.Enumeration.valid_card_in_pool" + ], + "remaining": [ + "槽位模型和合法枚举已证明；尚需逐项形式化 handler 的请求过滤、选项正规化与空结果/错误分支。" + ] + }, + { + "id": "P02", + "description": "Exact-tier over-target filter", + "status": "partial", + "sources": [ + "src/handler/build.rs" + ], + "theorems": [ + "Allium.Arithmetic.unavoidable_bonus_exclusion" + ], + "remaining": [ + "已证明非负不可避免加成的排除引理；尚需从普通/WL/Final 具体加成式导出对应不可避免量。" + ] + }, + { + "id": "P03", + "description": "Capacity handling", + "status": "open", + "sources": [ + "src/handler/capacity.rs" + ], + "theorems": [], + "remaining": [ + "尚未建立 validate/capacity 的接受域及每一种显式错误分支；未将固定容量视为可截断候选的理由。" + ] + }, + { + "id": "P04", + "description": "Numeric domain", + "status": "partial", + "sources": [ + "src/handler/capacity.rs", + "src/handler/validate.rs" + ], + "theorems": [ + "Allium.Arithmetic.grid_floor_of_error", + "Allium.Arithmetic.safe_clip", + "Allium.Arithmetic.optional_bound" + ], + "remaining": [ + "严格网格误差桥梁和安全饱和已证明；N1–N7 的逐表达式 binary64 误差预算、范围和构造器常数仍未证明。" + ] + }, + { + "id": "P05", + "description": "Same-character dominance", + "status": "partial", + "sources": [ + "src/search/dominance.rs" + ], + "theorems": [ + "Allium.Support.replacement_loss", + "Allium.Support.rounded_sum_mono", + "Allium.Arithmetic.support_compensation" + ], + "remaining": [ + "尚需证明完整支配守卫、q+5 截止名次、每个评分目标的替换单调性和两次舍入误差预算。" + ] + }, + { + "id": "P06", + "description": "Dominance Top-K recovery", + "status": "open", + "sources": [ + "src/search/alternatives.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明根映射、全部根养成实现的枚举及逆替换树覆盖；不能仅靠同分/同公共卡组替换引理宣称完成。" + ] + }, + { + "id": "P07", + "description": "Alternative-tree threshold", + "status": "open", + "sources": [ + "src/search/alternatives.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明每条逆替换边的完整比较键单调性和恢复树的子树阈值安全性。" + ] + }, + { + "id": "P08", + "description": "Character suffix bound", + "status": "partial", + "sources": [ + "src/search/suffix.rs" + ], + "theorems": [ + "Allium.FiniteBounds.character_bound_sound", + "Allium.FiniteBounds.insufficient_characters" + ], + "remaining": [ + "逐角色最大值再取 Top-r 的数学松弛已证明；各场景实际池、被排除角色和特征上界的实例化仍需连接。" + ] + }, + { + "id": "P09", + "description": "Exclusion delta", + "status": "open", + "sources": [ + "src/search/suffix.rs" + ], + "theorems": [], + "remaining": [ + "尚需形式化 Top-r 集合内移除/补入后的精确 delta 及预算使用方向。" + ] + }, + { + "id": "P10", + "description": "Dense suffix break", + "status": "partial", + "sources": [ + "src/search/dfs.rs", + "src/search/suffix.rs" + ], + "theorems": [ + "Allium.FiniteBounds.character_bound_mono", + "Allium.FiniteBounds.monotone_break" + ], + "remaining": [ + "嵌套池和单调 break 引理已证明；尚需连接 DFS 的 start/child/fixed-prefix 索引及具体组合上界。" + ] + }, + { + "id": "P11", + "description": "Candidate runs", + "status": "partial", + "sources": [ + "src/search/dfs.rs", + "src/search/suffix.rs" + ], + "theorems": [ + "Allium.FiniteBounds.monotone_break", + "Allium.FiniteBounds.independent_components" + ], + "remaining": [ + "尚需证明 run 划分保持相同 base/limited 项、尾部集合嵌套和 run-max 组合式。" + ] + }, + { + "id": "P12", + "description": "Sorted Power / Skill break", + "status": "partial", + "sources": [ + "src/search/dfs.rs" + ], + "theorems": [ + "Allium.FiniteBounds.repeated_max_bound", + "Allium.FiniteBounds.monotone_break" + ], + "remaining": [ + "重复最大值松弛已证明；尚需绑定排序分量、fixed-slot 例外和分支尾部。" + ] + }, + { + "id": "P13", + "description": "No-event numerator", + "status": "proved", + "sources": [ + "src/search/dfs.rs", + "src/search/suffix.rs" + ], + "theorems": [ + "Allium.Arithmetic.numerator_prune" + ], + "remaining": [] + }, + { + "id": "P14", + "description": "Event Score cutoff", + "status": "open", + "sources": [ + "src/search/objective.rs", + "src/search/dfs.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明活动点数的具体单调式、打包键阈值反解及 gallop/binary-search 不变量。" + ] + }, + { + "id": "P15", + "description": "Complete-deck skill ceilings", + "status": "partial", + "sources": [ + "src/search/dfs.rs", + "src/search/skill_ceiling.rs" + ], + "theorems": [ + "Allium.Skill.unit_count_sound", + "Allium.Skill.different_unit_sound", + "Allium.Skill.reference_exact_bound", + "Allium.Skill.reference_relax_sound" + ], + "remaining": [ + "技能类型的有限/有理数学上界已证明；尚需逐输入绑定 selected/candidate 构造、自动/固定队长和浮点桥梁。" + ] + }, + { + "id": "P16", + "description": "Correlated Score bound", + "status": "partial", + "sources": [ + "src/search/correlated.rs" + ], + "theorems": [ + "Allium.Quadratic.correlated_bound_sound" + ], + "remaining": [ + "二次包络的两个分支已证明；尚需证明 C/B/D 常数构造、线性平面来自合法技能槽及数值转换。" + ] + }, + { + "id": "P17", + "description": "Event independent bound", + "status": "partial", + "sources": [ + "src/search/suffix.rs" + ], + "theorems": [ + "Allium.FiniteBounds.independent_components", + "Allium.Arithmetic.upper_min", + "Allium.Arithmetic.clamp_mono" + ], + "remaining": [ + "尚需形式化六技能槽的排序/截断分配、具体活动公式及它们对 P/S/L/B 的单调性。" + ] + }, + { + "id": "P18", + "description": "Composition regimes", + "status": "partial", + "sources": [ + "src/search/composition.rs", + "src/pool/card_pool.rs", + "src/search/evaluate.rs", + "src/search/context.rs" + ], + "theorems": [ + "Allium.Composition.regime_count", + "Allium.Composition.regimes_cover", + "Allium.Composition.matches_admits", + "Allium.Composition.actual_unit_flag_mem", + "Allium.Composition.actual_attribute_flag", + "Allium.Composition.power_bound_sound", + "Allium.Composition.deck_classes_cover", + "Allium.ScenarioSearch.required_search_spec", + "Allium.ScenarioSearch.runScenes_exact", + "Allium.ConcretePower.planPower_sound", + "Allium.ConcretePower.power_search_exact" + ], + "remaining": [ + "49 场景覆盖、任意非单调八槽 power 上界、允许额外合法叶子的跨场景共享阈值，以及具体 Power 数学实例已证明；仍需把普通/WL/Final 的完整 RegimePlan 特征和其他目标评分上界逐项接入，并完成实际场景 DFS 的叶子与启用剪枝构造（与 P17/P35/S05 相交）。" + ] + }, + { + "id": "P19", + "description": "SIMD threshold mask", + "status": "open", + "sources": [ + "src/simd.rs" + ], + "theorems": [], + "remaining": [ + "尚需建立 lane/tail 位图的数学模型及 unsigned >= 阈值比较等价；不声称验证 Rust SIMD 指令。" + ] + }, + { + "id": "P20", + "description": "WL attribute matching", + "status": "open", + "sources": [ + "src/search/suffix.rs" + ], + "theorems": [], + "remaining": [ + "尚需构造新属性到未使用角色的注入匹配，证明可达属性计数界并覆盖非单调属性奖励表。" + ] + }, + { + "id": "P21", + "description": "WL support upper bound", + "status": "partial", + "sources": [ + "src/search/suffix.rs", + "src/search/solver/final_chapter.rs" + ], + "theorems": [ + "Allium.Support.prefix_exclusion", + "Allium.Support.leader_profile_envelope", + "Allium.Support.sorted_prefix_dominates" + ], + "remaining": [ + "有限支援池的排除单调性和逐 ID profile 包络已证明；尚需把有序支援扫描及其舍入连接到该模型。" + ] + }, + { + "id": "P22", + "description": "Exact bonus tiers", + "status": "partial", + "sources": [ + "src/search/solver/bonus_tiers.rs", + "src/search/skill_ceiling.rs" + ], + "theorems": [ + "Allium.Arithmetic.tier_suffix_interval", + "Allium.DP.compressed_reachable_covers", + "Allium.DP.query_bound", + "Allium.DP.query_empty" + ], + "remaining": [ + "键/特征 DP 的压缩和区间查询已证明；尚需具体 first-N 状态、GCD/offset、每卡 key/slack/excess 构造和每场景合法完成映射。" + ] + }, + { + "id": "P23", + "description": "Root sums", + "status": "partial", + "sources": [ + "src/search/solver/bonus_tiers.rs" + ], + "theorems": [ + "Allium.DP.mem_reachable", + "Allium.DP.unreachable_excludes_paths" + ], + "remaining": [ + "有限选择的可达性已证明；尚需绑定位行 root 表、各计数维度和 regime 总根排除。" + ] + }, + { + "id": "P24", + "description": "Selected-card refill", + "status": "open", + "sources": [ + "src/search/solver/bonus_tiers.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明 whole-tick profile 下选中卡 refill 的序单调性、完整卡组时的等式和截断松弛方向。" + ] + }, + { + "id": "P25", + "description": "Joint power-skill ceiling", + "status": "partial", + "sources": [ + "src/search/solver/bonus_tiers.rs", + "src/search/objective.rs" + ], + "theorems": [ + "Allium.Quadratic.joint_plane", + "Allium.Quadratic.joint_peak_sound", + "Allium.Arithmetic.optional_bound" + ], + "remaining": [ + "四分支 box/half-plane 乘积峰值已证明；尚需绑定 LiveProduct 构造、整数缩放、溢出守卫及向上/向下取整。" + ] + }, + { + "id": "P26", + "description": "Tier certificate", + "status": "open", + "sources": [ + "src/search/solver/bonus_tiers.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明 holding-position 子集枚举、排除/补位状态、whole-tick 近似与原浮点加成命中判据。" + ] + }, + { + "id": "P27", + "description": "Final member dominance", + "status": "open", + "sources": [ + "src/search/dominance.rs", + "src/search/alternatives.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明仅成员角色替换及所有合法队长旋转的覆盖，不能将成员支配应用于队长。" + ] + }, + { + "id": "P28", + "description": "Final leader/job bound", + "status": "partial", + "sources": [ + "src/search/solver/final_chapter.rs" + ], + "theorems": [ + "Allium.FiniteBounds.character_bound_sound" + ], + "remaining": [ + "尚需实例化每个 leader/job 的候选角色、合法槽位、支援 profile 和 leader 附加量。" + ] + }, + { + "id": "P29", + "description": "Final attribute DP", + "status": "partial", + "sources": [ + "src/search/solver/final_chapter.rs" + ], + "theorems": [ + "Allium.DP.mem_reachable", + "Allium.DP.compressed_reachable_covers" + ], + "remaining": [ + "通用组选择 DP 已证明；尚需实例化 OR-union/角色组/属性奖励表及队长初态。" + ] + }, + { + "id": "P30", + "description": "Final character-loop break", + "status": "partial", + "sources": [ + "src/search/solver/final_chapter.rs" + ], + "theorems": [ + "Allium.FiniteBounds.character_bound_mono", + "Allium.FiniteBounds.monotone_break" + ], + "remaining": [ + "尚需证明实际角色组迭代的嵌套后缀和其 ceiling 构造。" + ] + }, + { + "id": "P31", + "description": "Final last group", + "status": "open", + "sources": [ + "src/search/solver/final_chapter.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明最后一组自身项与 plan ceiling 相等，以及持有属性 rest maxima 的组可界定后续组。" + ] + }, + { + "id": "P32", + "description": "Final card-group bound", + "status": "partial", + "sources": [ + "src/search/solver/final_chapter.rs" + ], + "theorems": [ + "Allium.FiniteBounds.independent_components", + "Allium.Support.leader_profile_envelope" + ], + "remaining": [ + "尚需连接 per-group maxima、limited top-cap、Final 附加量和当前 profile 支援上界。" + ] + }, + { + "id": "P33", + "description": "Final group rest maxima", + "status": "partial", + "sources": [ + "src/search/solver/final_chapter.rs" + ], + "theorems": [ + "Allium.FiniteBounds.monotone_break" + ], + "remaining": [ + "尚需连接同属性 rest maxima 及候选 ceiling 的单调式。" + ] + }, + { + "id": "P34", + "description": "Final ranked-buffer break", + "status": "open", + "sources": [ + "src/search/solver/final_chapter.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明按有效 UB 排序、缓冲区满时所有溢出候选仍遍历、break 仅覆盖已排序部分。" + ] + }, + { + "id": "P35", + "description": "Final log-linear bound", + "status": "open", + "sources": [ + "src/search/log_linear.rs", + "src/search/solver/final_chapter.rs" + ], + "theorems": [], + "remaining": [ + "尚需证明 log-sum-exp 弦界、对数切线、分段凹技能式超梯度、逐组权重、区间算术和 32 项 atanh 余项证书。" + ] + }, + { + "id": "P36", + "description": "Numeric Power max/min", + "status": "partial", + "sources": [ + "src/search/solver/numeric.rs", + "src/search/evaluate.rs", + "src/search/context.rs", + "src/handler/capacity.rs" + ], + "theorems": [ + "Allium.FiniteBounds.repeated_max_bound", + "Allium.FiniteBounds.repeated_min_bound", + "Allium.Arithmetic.clamp_mono", + "Allium.PowerModel.tableIndex_surjective", + "Allium.PowerModel.count_five_iff_common", + "Allium.PowerModel.attribute_count_five", + "Allium.PowerModel.resolved_upper", + "Allium.PowerModel.resolved_lower", + "Allium.PowerModel.prefix_free_upper", + "Allium.PowerModel.prefix_free_lower", + "Allium.PowerModel.maximizing_prune", + "Allium.PowerModel.minimizing_prune", + "Allium.ScenarioPower.empty_units_require_a_lower_bound_guard" + ], + "remaining": [ + "已证明 decoded 八槽查表、五人成员计数、selected/free 组合及加称号后应用 cap 的双向严格剪枝；lower theorem 显式要求非空 unit 集合。尚需连接受理域（含空 unit 掩码与其压缩表构造）、具体 global/suffix 摘要和固定槽扫描状态，不能把这些连接归为 Rust refinement。" + ] + }, + { + "id": "P37", + "description": "Numeric Skill", + "status": "partial", + "sources": [ + "src/search/solver/numeric.rs", + "src/search/skill_ceiling.rs" + ], + "theorems": [ + "Allium.Skill.global_bound", + "Allium.Skill.unit_count_sound", + "Allium.Skill.different_unit_sound", + "Allium.Skill.merged_reference_rule_sound", + "Allium.Skill.encoded_key_upper" + ], + "remaining": [ + "技能数学引理已证明；尚需绑定 frontier 扫描终止、角色排除、full-key 同分规则及浮点编码误差。" + ] + }, + { + "id": "P38", + "description": "Power scenarios", + "status": "partial", + "sources": [ + "src/search/solver/power.rs", + "src/search/evaluate.rs" + ], + "theorems": [ + "Allium.ScenarioPower.bound_sound", + "Allium.ScenarioPower.empty_exact", + "Allium.ScenarioPower.singleton_exact", + "Allium.ScenarioPower.bound_le_tableMax", + "Allium.ScenarioPower.actual_common_admitted", + "Allium.ScenarioPower.multi_unit_is_only_an_upper_bound", + "Allium.ScenarioPower.admission_is_not_bound_soundness" + ], + "remaining": [ + "已证明实际 scenario_power 的非单调多单位 envelope、空/单单位精确性和真实公共 unit 集合的接纳性；并证明多单位只能作上界的反例。尚需证明生产 unit-mask 交集工作表的完整性、best_completion 扫描、实际叶子回算与带 least/cap 守卫的同分 public-set 剪枝。ConcretePower 的 49-regime 数学搜索不等于已证明此专用 fast path。" + ] + }, + { + "id": "P39", + "description": "Challenge bound frontier", + "status": "partial", + "sources": [ + "src/search/solver/challenge.rs" + ], + "theorems": [ + "Allium.DP.mem_reachable", + "Allium.DP.compressed_reachable_covers", + "Allium.FiniteBounds.frontier_bound" + ], + "remaining": [ + "跳过/选入与特征压缩的数学模型已证明；尚需实例化一角色五个不同 public ID、排序技能松弛及禁用不安全上下文的守卫。" + ] + }, + { + "id": "P40", + "description": "Challenge-all Top-K merge", + "status": "proved", + "sources": [ + "src/search/solver/challenge.rs" + ], + "theorems": [ + "Allium.group_topK_merge" + ], + "remaining": [] + }, + { + "id": "P41", + "description": "Feasibility pruning", + "status": "partial", + "sources": [ + "src/search/dfs.rs", + "src/search/solver/numeric.rs", + "src/search/solver/challenge.rs", + "src/search/placement.rs" + ], + "theorems": [ + "Allium.Enumeration.exhaustive_complete", + "Allium.Enumeration.valid_length", + "Allium.Enumeration.valid_card_in_pool", + "Allium.FiniteBounds.insufficient_characters" + ], + "remaining": [ + "槽位角色与合法枚举已证明；尚需覆盖全部 handler 参数正规化、搜索模式及实际 DFS feasibility 守卫。" + ] + }, + { + "id": "S01", + "description": "Canonical five-field Top-K, public-set deduplication, cardinality and bounded insertion", + "status": "proved", + "sources": [ + "src/search/tracker.rs" + ], + "theorems": [ + "Allium.coverage_exactness", + "Allium.topK_card", + "Allium.collect_exact", + "Allium.collect_order_independent", + "Allium.Canonical.key_lt_iff", + "Allium.Canonical.deck_key_injective" + ], + "remaining": [] + }, + { + "id": "S02", + "description": "Mathematical branch-and-bound kernel with explicitly sound node bounds", + "status": "proved", + "sources": [ + "src/search/dfs.rs" + ], + "theorems": [ + "Allium.strict_upper_prune", + "Allium.search_spec", + "Allium.search_exact" + ], + "remaining": [] + }, + { + "id": "S03", + "description": "Interruptible mathematical search: legal partial results, sticky expiry and Complete exactness", + "status": "proved", + "sources": [ + "src/search/budget.rs", + "src/search/types.rs" + ], + "theorems": [ + "Allium.interruptible_valid", + "Allium.complete_agrees_search", + "Allium.complete_exact", + "Allium.timed_out_results_legal" + ], + "remaining": [] + }, + { + "id": "S04", + "description": "Public-slot mathematical specification and complete ordered cultivation enumeration", + "status": "proved", + "sources": [ + "src/search/context.rs", + "src/search/placement.rs" + ], + "theorems": [ + "Allium.Enumeration.exhaustive_complete", + "Allium.Enumeration.exhaustive_keys_complete", + "Allium.Enumeration.same_public_role" + ], + "remaining": [] + }, + { + "id": "S05", + "description": "All-scene end-to-end instantiation of SearchTree.Sound and exhaustiveKeys", + "status": "partial", + "sources": [ + "src/search/solver/mod.rs", + "src/search/problem.rs", + "src/search/evaluate.rs", + "src/search/composition.rs", + "src/search/context.rs" + ], + "theorems": [ + "Allium.ConcretePower.member_admitted", + "Allium.ConcretePower.planPower_sound", + "Allium.ConcretePower.ceiling_sound", + "Allium.ConcretePower.scene_valid", + "Allium.ConcretePower.scenes_cover", + "Allium.ConcretePower.power_search_exact" + ], + "remaining": [ + "首个具体 Power 数学实例已贯通公开五槽规格、49-regime、八槽查表、per-character/per-card top-five、honor/cap、共享阈值与 exhaustiveKeys，主定理不再接受抽象上界或场景覆盖前提。但该树显式枚举已接纳的合法卡组，不是全部生产 DFS 优化；其他目标、实际 solver 场景、受理域/固定角色语义及每条启用剪枝的数学构造仍需逐项接入，全部仍属第一档。" + ] + }, + { + "id": "R01", + "description": "Rust memory safety, machine arithmetic refinement, extraction, compilation and executable equivalence", + "status": "out_of_scope", + "sources": [ + "src/search/dfs.rs" + ], + "theorems": [], + "remaining": [ + "属于第二/三档：本工程不声称证明 Rust 二进制与 Lean 模型等价。" + ] + } + ] +} diff --git a/formal/lean/lake-manifest.json b/formal/lean/lake-manifest.json new file mode 100644 index 0000000..f6e679a --- /dev/null +++ b/formal/lean/lake-manifest.json @@ -0,0 +1,95 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "f897ebcf72cd16f89ab4577d0c826cd14afaafc7", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "d768126816be17600904726ca7976b185786e6b9", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "556caed0eadb7901e068131d1be208dd907d07a2", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.74", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "dea6a3361fa36d5a13f87333dc506ada582e025c", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "alliumFormal", + "lakeDir": ".lake"} diff --git a/formal/lean/lakefile.toml b/formal/lean/lakefile.toml new file mode 100644 index 0000000..cc0d4b1 --- /dev/null +++ b/formal/lean/lakefile.toml @@ -0,0 +1,15 @@ +name = "alliumFormal" +version = "0.1.0" +defaultTargets = ["Allium"] + +[leanOptions] +autoImplicit = false +warningAsError = true + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "f897ebcf72cd16f89ab4577d0c826cd14afaafc7" + +[[lean_lib]] +name = "Allium" diff --git a/formal/lean/lean-toolchain b/formal/lean/lean-toolchain new file mode 100644 index 0000000..c00a535 --- /dev/null +++ b/formal/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.24.0 diff --git a/formal/lean/verify.py b/formal/lean/verify.py new file mode 100644 index 0000000..20abc68 --- /dev/null +++ b/formal/lean/verify.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Build every proof, audit transitive axioms, and check source/coverage drift. + +No dependencies other than Python 3.11+ and the pinned Lean/Lake toolchain. +A successful run checks the declared scope; it does not change open obligations +into proofs. Use --require-complete when evaluating stage-one completion. +""" +from __future__ import annotations + +import argparse +import hashlib +import json +from pathlib import Path +import re +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +NAME = re.compile(r"Allium(?:\.[A-Za-z_][A-Za-z_0-9']*)+") +STATUSES = {"proved", "partial", "open", "out_of_scope"} + + +def digest(path: Path) -> str: + """Ignore checkout CRLF conversion, not any other source change.""" + return hashlib.sha256(path.read_bytes().replace(b"\r\n", b"\n")).hexdigest() + + +def run(args: list[str], *, expect_failure: bool = False) -> str: + result = subprocess.run(args, cwd=HERE, text=True, encoding="utf-8", + errors="replace", stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, timeout=1800, check=False) + if expect_failure: + if result.returncode == 0 or "AXIOM AUDIT FAILED:" not in result.stdout: + raise RuntimeError(f"Negative audit fixture did not fail as intended:\n{result.stdout}") + elif result.returncode != 0: + raise RuntimeError(f"Command failed ({result.returncode}): {args}\n{result.stdout}") + return result.stdout + + +def check_inventory(obligations: list[dict]) -> None: + """The complete manual inventory must remain visible in the proof scope.""" + document = (ROOT / "docs/pruning-proof.md").read_text(encoding="utf-8") + section = document.split("## 26. Proof-to-code inventory", 1)[1].split("## 27.", 1)[0] + rows = [line.strip("|").split("|")[0].strip() + for line in section.splitlines() if line.startswith("| ")][2:] + if not rows: + raise ValueError("No pruning mechanisms found in the source inventory") + expected = {f"P{i:02}": description for i, description in enumerate(rows, 1)} + actual = {o["id"]: o["description"] for o in obligations if o["id"].startswith("P")} + if actual != expected: + raise ValueError("Pruning inventory mismatch: do not remove, rename or omit a mechanism") + required = set(expected) | {"S01", "S02", "S03", "S04", "S05", "R01"} + if {o["id"] for o in obligations} != required: + raise ValueError("Core/search/scene/refinement coverage inventory mismatch") + for obligation in obligations: + if obligation["status"] == "out_of_scope" and obligation["id"] != "R01": + raise ValueError(f"First-tier mathematical obligation cannot be excluded: {obligation['id']}") + + +def inventory_self_test(obligations: list[dict]) -> None: + """Reject omitting hard work or relabelling it as Rust refinement.""" + missing = [dict(o) for o in obligations if o["id"] != "P01"] + excluded = [dict(o, status="out_of_scope") if o["id"] == "S05" else dict(o) + for o in obligations] + for label, fixture in [("omitted-pruning-mechanism", missing), + ("excluded-mathematical-obligation", excluded)]: + try: + check_inventory(fixture) + except ValueError: + print(f"NEGATIVE COVERAGE TEST PASSED: {label}") + else: + raise RuntimeError(f"Coverage fixture was incorrectly accepted: {label}") + + +def metadata() -> tuple[dict, list[str]]: + manifest = json.loads((HERE / "coverage.json").read_text(encoding="utf-8")) + if manifest.get("schema") != 1 or not manifest.get("sources") or not manifest.get("obligations"): + raise ValueError("Missing or unsupported source/coverage manifest") + for relative, expected in manifest["sources"].items(): + path = (ROOT / relative).resolve() + if not path.is_relative_to(ROOT) or not path.is_file(): + raise ValueError(f"Invalid source path: {relative}") + actual = digest(path) + if actual != expected: + raise ValueError(f"Source drift: {relative}\nexpected {expected}\nactual {actual}\n" + "Reconcile the model and proofs before updating the snapshot.") + modules = {".".join(p.relative_to(HERE).with_suffix("").parts) + for p in (HERE / "Allium").rglob("*.lean")} + imported = set(re.findall(r"^import\s+(Allium(?:\.[A-Za-z_0-9]+)+)\s*$", + (HERE / "Allium.lean").read_text(encoding="utf-8"), re.M)) + if modules != imported: + raise ValueError(f"Umbrella import mismatch: missing={modules-imported}; stale={imported-modules}") + if not modules: + raise ValueError("No proof modules found") + ids: set[str] = set() + theorem_names: set[str] = set() + for obligation in manifest["obligations"]: + oid = obligation["id"] + if oid in ids or obligation["status"] not in STATUSES: + raise ValueError(f"Invalid/duplicate obligation: {oid}") + ids.add(oid) + if not obligation.get("description") or not obligation.get("sources"): + raise ValueError(f"Missing scope/source information: {oid}") + if not set(obligation["sources"]).issubset(manifest["sources"]): + raise ValueError(f"Unpinned source in obligation {oid}") + if obligation["status"] == "proved" and (obligation.get("remaining") or not obligation.get("theorems")): + raise ValueError(f"A proved obligation needs theorem references and no remaining work: {oid}") + if obligation["status"] in {"partial", "open"} and not obligation.get("remaining"): + raise ValueError(f"An incomplete obligation must disclose remaining work: {oid}") + for theorem in obligation.get("theorems", []): + if not NAME.fullmatch(theorem): + raise ValueError(f"Invalid theorem name: {theorem}") + theorem_names.add(theorem) + check_inventory(manifest['obligations']) + complete = all(o["status"] in {"proved", "out_of_scope"} for o in manifest["obligations"]) + if manifest.get("stage_one_complete") != complete: + raise ValueError("stage_one_complete contradicts the obligation table") + print(f"SOURCE CHECK PASSED: {len(manifest['sources'])} files; {len(modules)} imported proof modules") + for status in sorted(STATUSES): + count = sum(o["status"] == status for o in manifest["obligations"]) + print(f"COVERAGE {status}: {count}") + print(f"STAGE ONE COMPLETE: {complete}") + return manifest, sorted(theorem_names) + + +def audit(theorems: list[str], self_test: bool) -> None: + script = (HERE / "Audit.lean").read_text(encoding="utf-8") + imports, body = script.split("/-!", 1) + # Preserve the checker verbatim; inject fixtures before its run_cmd block. + body = "/-!" + body + with tempfile.TemporaryDirectory(prefix="allium-lean-audit-") as tmp: + root = Path(tmp) + checked = root / "Check.lean" + checked.write_text(script + "\n" + "\n".join(f"#check {name}" for name in theorems) + "\n", + encoding="utf-8") + output = run(["lake", "env", "lean", "-DwarningAsError=true", str(checked)]) + for line in output.splitlines(): + if "AXIOM AUDIT PASSED:" in line or "depends on axioms:" in line: + print(line) + if "AXIOM AUDIT PASSED:" not in output: + raise RuntimeError("Audit completed without its success marker") + if self_test: + fixtures = { + "sorry": "theorem Allium.negativeSorry : False := by sorry\n", + "foreign-axiom": "axiom ForeignUntrusted : False\n" + "theorem Allium.negativeForeign : False := ForeignUntrusted\n", + "unused-local-axiom": "axiom Allium.negativeUnused : False\n", + "native-decide": "theorem Allium.negativeNative : (2 + 2 : Nat) = 4 := by native_decide\n", + } + for label, fixture in fixtures.items(): + path = root / f"Reject-{label}.lean" + path.write_text(imports + "\n" + fixture + "\n" + body, encoding="utf-8") + run(["lake", "env", "lean", "-DwarningAsError=true", str(path)], expect_failure=True) + print(f"NEGATIVE AUDIT TEST PASSED: {label}") + + +def main() -> int: + for stream in (sys.stdout, sys.stderr): + if hasattr(stream, 'reconfigure'): + stream.reconfigure(encoding='utf-8', errors='backslashreplace') + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--self-test", action="store_true", help="verify rejection of four axiom escape routes") + parser.add_argument("--require-complete", action="store_true", help="fail while any stage-one obligation is incomplete") + args = parser.parse_args() + manifest, theorems = metadata() + print(run(["lake", "build"]).strip()) + audit(theorems, args.self_test) + if args.self_test: + inventory_self_test(manifest['obligations']) + if args.require_complete and not manifest["stage_one_complete"]: + pending = [o["id"] for o in manifest["obligations"] if o["status"] in {"partial", "open"}] + raise RuntimeError("Stage-one verification is incomplete: " + ", ".join(pending)) + print("VERIFICATION PASSED FOR THE DECLARED SCOPE (see coverage.json)") + return 0 + + +if __name__ == "__main__": + try: + sys.exit(main()) + except (OSError, ValueError, RuntimeError, subprocess.TimeoutExpired) as exc: + print(f"VERIFICATION FAILED: {exc}", file=sys.stderr) + sys.exit(1)