QuantizedTreeCompiler.lean

1 module
2 public import ExactTreeCompiler
3 import all ExactTreeCompiler
4 public import BudgetConvolution
5 import all BudgetConvolution
6 
7 /-!
8 Author: Komorebi P.
9 Paper VIII 9.8: exact quantized-budget compilation on the actual candidate tree
10 and independently defined legal cuts from the preceding block.
11 Every finite table result is attained; infeasibility is represented explicitly.
12 -/
13 public section
14 set_option autoImplicit false
15 set_option maxRecDepth 2048
16 namespace KomorebiPaperVIII
17 namespace CandidateTree
18 open scoped BigOperators
19 variable {α R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
20 
21 /-- Integer errors of a legal cut. Splitting itself introduces no error. -/
22 def cutWeight (w : α → ℕ) : {t : CandidateTree α} → Cut t → ℕ
23   | t, .keep _ => w t.root
24   | .node _ _ _, .split cs => ∑ i, cutWeight w (cs i)
25 
26 /-- Exact-weight min-plus recurrence. Unreachable states are `none`. -/
27 def budgetTable (κ : α → R) (w : α → ℕ) (σ : α → R) :
28     CandidateTree α → ℕ → Option R
29   | .leaf a, b => BudgetDP.singletonTable (w a) (κ a) b
30   | .node a _ ts, b =>
31     BudgetDP.choose (BudgetDP.singletonTable (w a) (κ a) b)
32       (BudgetDP.add (some (σ a))
33         (BudgetDP.combine (fun i => budgetTable κ w σ (ts i)) b))
34 
35 /-- Theorem 9.8 at every exact weight: lower bound, attainment, and infeasibility. -/
36 theorem budgetTable_correct (κ : α → R) (w : α → ℕ) (σ : α → R)
37     (t : CandidateTree α) (b : ℕ) :
38     BudgetDP.IsMinimum (budgetTable κ w σ t b)
39       (fun z => ∃ c : Cut t, cutWeight w c = b ∧ cutValue κ σ c = z) := by
40   induction t generalizing b with
41   | leaf a =>
42     apply BudgetDP.minimum_congr (BudgetDP.singletonTable_correct (w a) (κ a) b)
43     intro z
44     constructor
45     · rintro ⟨hb, hz⟩
46       exact ⟨.keep (.leaf a), hb.symm, hz.symm⟩
47     · rintro ⟨c, hb, hz⟩
48       cases c
49       exact ⟨hb.symm, hz.symm⟩
50   | node a n ts ih =>
51     let S := fun i b z => ∃ c : Cut (ts i), cutWeight w c = b ∧ cutValue κ σ c = z
52     have hchildren := BudgetDP.combine_correct (fun i => budgetTable κ w σ (ts i)) S ih b
53     have hshift := BudgetDP.add_correct (some (σ a))
54       (BudgetDP.combine (fun i => budgetTable κ w σ (ts i)) b)
55       (fun z => z = σ a)
56       (fun z => ∃ ws : Fin (n + 1) → ℕ, ∃ cs : Fin (n + 1) → R,
57         (∀ i, S i (ws i) (cs i)) ∧ (∑ i, ws i) = b ∧ (∑ i, cs i) = z)
58       ⟨rfl, fun z hz => by rw [hz]⟩ hchildren
59     have h := BudgetDP.choose_correct
60       (BudgetDP.singletonTable (w a) (κ a) b)
61       (BudgetDP.add (some (σ a))
62         (BudgetDP.combine (fun i => budgetTable κ w σ (ts i)) b))
63       _ _ (BudgetDP.singletonTable_correct (w a) (κ a) b) hshift
64     apply BudgetDP.minimum_congr h
65     intro z
66     constructor
67     · intro hz
68       rcases hz with ⟨hb, hz⟩ | hz
69       · exact ⟨.keep (.node a n ts), hb.symm, hz.symm⟩
70       · rcases hz with ⟨u, v, hu, ⟨ws, cs, hc, hw, hv⟩, hz⟩
71         choose cuts hweights hcosts using hc
72         refine ⟨.split cuts, ?_, ?_⟩
73         · change (∑ i, cutWeight w (cuts i)) = b
74           simpa only [hweights] using hw
75         · change σ a + (∑ i, cutValue κ σ (cuts i)) = z
76           simpa only [hcosts, hv, hu] using hz.symm
77     · rintro ⟨c, hw, hc⟩
78       cases c with
79       | keep => exact Or.inl ⟨hw.symm, hc.symm⟩
80       | split cuts =>
81         refine Or.inr ⟨σ a, ∑ i, cutValue κ σ (cuts i), rfl, ?_, hc.symm⟩
82         exact ⟨fun i => cutWeight w (cuts i), fun i => cutValue κ σ (cuts i),
83           fun i => ⟨cuts i, rfl, rfl⟩, hw, rfl⟩
84 
85 /-- The actual budget-constrained compiler scans only weights 0,...,B. -/
86 def compileBudget (κ : α → R) (w : α → ℕ) (σ : α → R)
87     (t : CandidateTree α) (B : ℕ) : Option R :=
88   BudgetDP.withinBudget (budgetTable κ w σ t) B
89 
90 /-- Exact constrained optimum over independent legal cuts of the original tree. -/
91 theorem quantized_budget_compiler (κ : α → R) (w : α → ℕ) (σ : α → R)
92     (t : CandidateTree α) (B : ℕ) :
93     BudgetDP.IsMinimum (compileBudget κ w σ t B)
94       (fun z => ∃ c : Cut t, cutWeight w c ≤ B ∧ cutValue κ σ c = z) := by
95   apply BudgetDP.minimum_congr
96     (BudgetDP.withinBudget_correct (budgetTable κ w σ t)
97       (fun b z => ∃ c : Cut t, cutWeight w c = b ∧ cutValue κ σ c = z)
98       (budgetTable_correct κ w σ t) B)
99   intro z
100   constructor
101   · rintro ⟨b, hb, c, hw, hc⟩
102     exact ⟨c, hw ▸ hb, hc⟩
103   · rintro ⟨c, hc, hz⟩
104     exact ⟨cutWeight w c, hc, c, rfl, hz⟩
105 
106 /-- Every finite answer is attained by a legal budget-feasible cut and beats all others. -/
107 theorem compileBudget_some_iff (κ : α → R) (w : α → ℕ) (σ : α → R)
108     (t : CandidateTree α) (B : ℕ) (v : R) :
109     compileBudget κ w σ t B = some v ↔
110       (∃ c : Cut t, cutWeight w c ≤ B ∧ cutValue κ σ c = v) ∧
111       ∀ c : Cut t, cutWeight w c ≤ B → v ≤ cutValue κ σ c := by
112   rw [BudgetDP.minimum_some_iff _ _ (quantized_budget_compiler κ w σ t B)]
113   constructor
114   · intro h
115     exact ⟨h.1, fun c hc => h.2 _ ⟨c, hc, rfl⟩⟩
116   · intro h
117     refine ⟨h.1, ?_⟩
118     rintro z ⟨c, hc, rfl⟩
119     exact h.2 c hc
120 
121 /-- No large finite penalty or zero-cost placeholder can masquerade as infeasibility. -/
122 theorem compileBudget_none_iff (κ : α → R) (w : α → ℕ) (σ : α → R)
123     (t : CandidateTree α) (B : ℕ) :
124     compileBudget κ w σ t B = none ↔ ¬ ∃ c : Cut t, cutWeight w c ≤ B := by
125   rw [BudgetDP.minimum_none_iff _ _ (quantized_budget_compiler κ w σ t B)]
126   simp
127 
128 /-- Increasing the budget cannot worsen a finite optimum. -/
129 theorem compileBudget_monotone (κ : α → R) (w : α → ℕ) (σ : α → R)
130     (t : CandidateTree α) (B C : ℕ) (hBC : B ≤ C) (u v : R)
131     (hu : compileBudget κ w σ t B = some u)
132     (hv : compileBudget κ w σ t C = some v) : v ≤ u := by
133   obtain ⟨⟨c, hc, hcost⟩, _⟩ := (compileBudget_some_iff κ w σ t B u).mp hu
134   have h := ((compileBudget_some_iff κ w σ t C v).mp hv).2 c (hc.trans hBC)
135   simpa only [hcost] using h
136 end CandidateTree
137 end KomorebiPaperVIII
138 
139 #print axioms KomorebiPaperVIII.CandidateTree.budgetTable_correct
140 #print axioms KomorebiPaperVIII.CandidateTree.quantized_budget_compiler
141 #print axioms KomorebiPaperVIII.CandidateTree.compileBudget_some_iff
142 #print axioms KomorebiPaperVIII.CandidateTree.compileBudget_none_iff
143 #print axioms KomorebiPaperVIII.CandidateTree.compileBudget_monotone
144 #print axioms KomorebiPaperVIII.CandidateTree.budgetTable
145 #print axioms KomorebiPaperVIII.CandidateTree.compileBudget

Back to source controls