test(formal): add checked Lean core and pruning lemmas

.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.'

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 出：

formal/lean/.gitignore

@@ -0,0 +1,5 @@
+.lake/
+*.olean
+*.ilean
+*.trace
+__pycache__/

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

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

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