DiscretePrecision.lean

1 module
2 public import BudgetConvolution
3 import all BudgetConvolution
4 
5 /-!
6 Author: Komorebi P.
7 Paper VIII 8.7: exact discrete precision assignment with an explicit guarded
8 residual budget. Costs are exact field values, not floating-point sentinels.
9 One option is independently selected for every edge, including zero-error options.
10 An empty option list correctly makes the whole assignment infeasible.
11 -/
12 public section
13 set_option autoImplicit false
14 namespace KomorebiPaperVIII
15 namespace BudgetDP
16 variable {R : Type*} [Field R] [LinearOrder R] [IsStrictOrderedRing R]
17 
18 /-- Independently defined legal assignments, with one listed option per edge. -/
19 inductive Assignment : List (List (ℕ × R)) → Type _ where
20   | nil : Assignment []
21   | cons {opts : List (ℕ × R)} {edges : List (List (ℕ × R))}
22       (choice : ℕ × R) (allowed : choice ∈ opts) (rest : Assignment edges) :
23       Assignment (opts :: edges)
24 
25 namespace Assignment
26 
27 def weight : {edges : List (List (ℕ × R))} → Assignment edges → ℕ
28   | _, .nil => 0
29   | _, .cons o _ rest => weight rest + o.1
30 
31 def cost : {edges : List (List (ℕ × R))} → Assignment edges → R
32   | _, .nil => 0
33   | _, .cons o _ rest => cost rest + o.2
34 end Assignment
35 
36 /-- The recurrence iterates over the current edge's options, not all assignments.
37 The guard is necessary because natural subtraction otherwise truncates at zero. -/
38 def discreteTable : List (List (ℕ × R)) → ℕ → Option R
39   | [], b => singletonTable 0 0 b
40   | opts :: edges, b =>
41     bestOver (fun o => if o.1 ≤ b then
42       add (discreteTable edges (b - o.1)) (some o.2) else none) opts
43 
44 /-- Exact-weight semantics of the dynamic program. -/
45 theorem discreteTable_correct (edges : List (List (ℕ × R))) (b : ℕ) :
46     IsMinimum (discreteTable edges b)
47       (fun z => ∃ a : Assignment edges, a.weight = b ∧ a.cost = z) := by
48   induction edges generalizing b with
49   | nil =>
50     apply minimum_congr (singletonTable_correct 0 (0 : R) b)
51     intro z
52     constructor
53     · rintro ⟨hb, hz⟩
54       exact ⟨.nil, hb.symm, hz.symm⟩
55     · rintro ⟨a, hb, hz⟩
56       cases a
57       exact ⟨hb.symm, hz.symm⟩
58   | cons opts edges ih =>
59     let S := fun (o : ℕ × R) z =>
60       ∃ a : Assignment edges, a.weight + o.1 = b ∧ a.cost + o.2 = z
61     have h : ∀ o ∈ opts, IsMinimum
62         (if o.1 ≤ b then add (discreteTable edges (b - o.1)) (some o.2) else none) (S o) := by
63       intro o _
64       by_cases hob : o.1 ≤ b
65       · simp only [hob, ↓reduceIte]
66         apply minimum_congr
67           (add_correct (discreteTable edges (b - o.1)) (some o.2)
68             (fun z => ∃ a : Assignment edges, a.weight = b - o.1 ∧ a.cost = z)
69             (fun z => z = o.2) (ih _) ⟨rfl, fun z hz => by rw [hz]⟩)
70         intro z
71         constructor
72         · rintro ⟨u, v, ⟨a, hw, hc⟩, hv, hz⟩
73           refine ⟨a, ?_, ?_⟩
74           · omega
75           · rw [hc, ← hv]
76             exact hz.symm
77         · rintro ⟨a, hw, hc⟩
78           exact ⟨a.cost, o.2, ⟨a, by omega, rfl⟩, rfl, hc.symm⟩
79       · simp only [hob, ↓reduceIte, IsMinimum]
80         rintro z ⟨a, hw, hc⟩
81         omega
82     apply minimum_congr (bestOver_correct opts _ S h)
83     intro z
84     constructor
85     · rintro ⟨o, ho, a, hw, hc⟩
86       exact ⟨.cons o ho a, hw, hc⟩
87     · rintro ⟨a, hw, hc⟩
88       cases a with
89       | cons o ho a => exact ⟨o, ho, a, hw, hc⟩
90 
91 /-- The finite discrete precision optimizer. -/
92 def discreteBudget (edges : List (List (ℕ × R))) (B : ℕ) : Option R :=
93   withinBudget (discreteTable edges) B
94 
95 /-- Theorem 8.7: an attained global minimum under the declared quantized budget. -/
96 theorem discrete_precision_program (edges : List (List (ℕ × R))) (B : ℕ) :
97     IsMinimum (discreteBudget edges B)
98       (fun z => ∃ a : Assignment edges, a.weight ≤ B ∧ a.cost = z) := by
99   apply minimum_congr (withinBudget_correct (discreteTable edges)
100     (fun b z => ∃ a : Assignment edges, a.weight = b ∧ a.cost = z)
101     (discreteTable_correct edges) B)
102   intro z
103   constructor
104   · rintro ⟨b, hb, a, hw, hc⟩
105     exact ⟨a, hw ▸ hb, hc⟩
106   · rintro ⟨a, ha, hz⟩
107     exact ⟨a.weight, ha, a, rfl, hz⟩
108 
109 /-- A finite answer is a feasible assignment cost, not merely a relaxation. -/
110 theorem discreteBudget_some_iff (edges : List (List (ℕ × R))) (B : ℕ) (v : R) :
111     discreteBudget edges B = some v ↔
112       (∃ a : Assignment edges, a.weight ≤ B ∧ a.cost = v) ∧
113         ∀ a : Assignment edges, a.weight ≤ B → v ≤ a.cost := by
114   rw [minimum_some_iff _ _ (discrete_precision_program edges B)]
115   constructor
116   · intro h
117     exact ⟨h.1, fun a ha => h.2 _ ⟨a, ha, rfl⟩⟩
118   · intro h
119     refine ⟨h.1, ?_⟩
120     rintro z ⟨a, ha, rfl⟩
121     exact h.2 a ha
122 
123 /-- Infeasibility is exactly the absence of a complete legal assignment. -/
124 theorem discreteBudget_none_iff (edges : List (List (ℕ × R))) (B : ℕ) :
125     discreteBudget edges B = none ↔ ¬ ∃ a : Assignment edges, a.weight ≤ B := by
126   rw [minimum_none_iff _ _ (discrete_precision_program edges B)]
127   simp
128 
129 /-- Regression: an over-budget option is not accepted through truncated subtraction. -/
130 theorem over_budget_option_rejected :
131     discreteBudget ([[(1, (0 : ℚ))]]) 0 = none := by decide
132 
133 /-- Regression: a zero-weight option remains admissible at a zero budget. -/
134 theorem zero_budget_option_accepted :
135     discreteBudget ([[(0, (3 : ℚ)), (1, (0 : ℚ))]]) 0 = some 3 := by
136   norm_num [discreteBudget, withinBudget, bestOver, discreteTable, singletonTable, choose, add]
137 
138 /-- Regression: no available type on an edge is infeasible, not free. -/
139 theorem empty_precision_options_rejected :
140     discreteBudget ([[]] : List (List (ℕ × ℚ))) 3 = none := by decide
141 
142 /-- Regression: the empty problem has cost zero and consumes no error budget. -/
143 theorem empty_precision_problem :
144     discreteBudget ([] : List (List (ℕ × ℚ))) 0 = some 0 := by decide
145 end BudgetDP
146 end KomorebiPaperVIII
147 
148 #print axioms KomorebiPaperVIII.BudgetDP.discreteTable_correct
149 #print axioms KomorebiPaperVIII.BudgetDP.discrete_precision_program
150 #print axioms KomorebiPaperVIII.BudgetDP.discreteBudget_some_iff
151 #print axioms KomorebiPaperVIII.BudgetDP.discreteBudget_none_iff
152 #print axioms KomorebiPaperVIII.BudgetDP.over_budget_option_rejected
153 #print axioms KomorebiPaperVIII.BudgetDP.zero_budget_option_accepted
154 #print axioms KomorebiPaperVIII.BudgetDP.empty_precision_options_rejected
155 #print axioms KomorebiPaperVIII.BudgetDP.empty_precision_problem
156 #print axioms KomorebiPaperVIII.BudgetDP.discreteTable
157 #print axioms KomorebiPaperVIII.BudgetDP.discreteBudget

Back to source controls