HardInquiry.lean

1 import MachineTheory.HardPareto
2 import Mathlib.Data.Fintype.Option
3 import Mathlib.Data.Fintype.Sum
4 import Mathlib.Data.Fintype.Prod
5 import Mathlib.Data.Finset.Union
6 
7 /-!
8 # Hard-budget finite inquiry
9 
10 Core 5.1. A literal tree uses `none` for an impossible report and an actual child
11 for every possible report. The validity predicate rejects both missing reachable
12 children and invented unreachable children. It evaluates the actual post-action
13 support. Costs have named natural-number coordinates; storage counts ALL nodes.
14 -/
15 namespace Komorebi.MachineTheory.HardInquiry
16 
17 open Finset
18 
19 variable {X E O C R : Type}
20 
21 /-- Boolean guards specify finite decision tables, not an unverified host checker. -/
22 structure Model (X E O C R : Type) where
23   permitted : E → X → Bool
24   next : E → X → X
25   observe : E → X → O
26   accept : X → C → Bool
27   stepCost : E → R → ℕ
28   terminalCost : C → Finset X → R → ℕ
29 
30 /-- A profile pairs online costs in every named coordinate with complete storage. -/
31 abbrev Profile (R : Type) := (R → ℕ) × ℕ
32 
33 /-- An option contains a real subtree or no stored subtree at all. -/
34 def Tree (E O C : Type) : ℕ → Type
35   | 0 => C
36   | h + 1 => C ⊕ (E × (O → Option (Tree E O C h)))
37 
38 variable [DecidableEq X] [Fintype E]
39   [Fintype O] [DecidableEq O] [Fintype C]
40   [Fintype R]
41 
42 namespace Model
43 
44 /-- Images, not pre-action supports, define the next information state. -/
45 def update (M : Model X E O C R) (V : Finset X) (e : E) (o : O) : Finset X :=
46   (V.filter (fun x => M.observe e x = o)).image (M.next e)
47 
48 omit [Fintype E] [Fintype O] [Fintype C] [Fintype R] in
49 theorem mem_update (M : Model X E O C R) (V : Finset X) (e : E) (o : O) (y : X) :
50     y ∈ M.update V e o ↔ ∃ x ∈ V, M.observe e x = o ∧ M.next e x = y := by
51   simp only [update, mem_image, mem_filter]
52   constructor
53   · rintro ⟨x, ⟨hx, ho⟩, hy⟩; exact ⟨x, hx, ho, hy⟩
54   · rintro ⟨x, hx, ho, hy⟩; exact ⟨x, ⟨hx, ho⟩, hy⟩
55 
56 omit [Fintype E] [Fintype O] [Fintype C] [Fintype R] in
57 theorem actual_next_mem (M : Model X E O C R) {V : Finset X} {x : X}
58     (hx : x ∈ V) (e : E) : M.next e x ∈ M.update V e (M.observe e x) :=
59   (M.mem_update _ _ _ _).mpr ⟨x, hx, rfl, rfl⟩
60 
61 def Allowed (M : Model X E O C R) (V : Finset X) (e : E) : Prop :=
62   V.Nonempty ∧ ∀ x ∈ V, M.permitted e x = true
63 
64 def Terminal (M : Model X E O C R) (V : Finset X) (c : C) : Prop :=
65   V.Nonempty ∧ ∀ x ∈ V, M.accept x c = true
66 
67 instance allowedDecidable (M : Model X E O C R) (V : Finset X) (e : E) :
68     Decidable (M.Allowed V e) := inferInstanceAs (Decidable (_ ∧ _))
69 instance terminalDecidable (M : Model X E O C R) (V : Finset X) (c : C) :
70     Decidable (M.Terminal V c) := inferInstanceAs (Decidable (_ ∧ _))
71 
72 /-- Validity uses only a common experiment/terminal label, never a hidden-state selector. -/
73 def Valid (M : Model X E O C R) : (h : ℕ) → Finset X → Tree E O C h → Prop
74   | 0, V, c => M.Terminal V c
75   | _ + 1, V, .inl c => M.Terminal V c
76   | h + 1, V, .inr (e, k) => M.Allowed V e ∧ ∀ o,
77       match k o with
78       | none => M.update V e o = ∅
79       | some t => M.Valid h (M.update V e o) t
80 
81 /-- Total finite validation of an explicit stored tree. -/
82 instance validDecidable (M : Model X E O C R) :
83     (h : ℕ) → (V : Finset X) → (t : Tree E O C h) → Decidable (M.Valid h V t)
84   | 0, V, c => M.terminalDecidable V c
85   | _+1, V, .inl c => M.terminalDecidable V c
86   | h+1, V, .inr (e,k) => by
87       letI : ∀ o, Decidable (match k o with
88           | none => M.update V e o = ∅
89           | some t => M.Valid h (M.update V e o) t) := fun o =>
90         match k o with
91         | none => inferInstance
92         | some t => M.validDecidable h (M.update V e o) t
93       exact inferInstanceAs (Decidable (M.Allowed V e ∧ ∀ o,
94         match k o with
95         | none => M.update V e o = ∅
96         | some t => M.Valid h (M.update V e o) t))
97 
98 omit [Fintype E] [Fintype O] [Fintype C] [Fintype R] in
99 theorem valid_nonempty (M : Model X E O C R) {h : ℕ} {V : Finset X} {t : Tree E O C h}
100     (hv : M.Valid h V t) : V.Nonempty := by
101   cases h with
102   | zero => exact hv.1
103   | succ h => cases t with
104     | inl c => exact hv.1
105     | inr ek => exact hv.1.1
106 
107 /-- Nonexistent children contribute zero storage and zero cost, not a free success. -/
108 def optional (p : Option (Profile R)) : Profile R := p.getD (0, 0)
109 
110 def nodeProfile (M : Model X E O C R) (e : E) (k : O → Option (Profile R)) : Profile R :=
111   (fun r => M.stepCost e r + univ.sup (fun o => (optional (k o)).1 r),
112     1 + ∑ o, (optional (k o)).2)
113 
114 def profile (M : Model X E O C R) : (h : ℕ) → Finset X → Tree E O C h → Profile R
115   | 0, V, c => (M.terminalCost c V, 1)
116   | _ + 1, V, .inl c => (M.terminalCost c V, 1)
117   | h + 1, V, .inr (e, k) => M.nodeProfile e
118       (fun o => (k o).map (M.profile h (M.update V e o)))
119 
120 omit [Fintype E] [Fintype C] [Fintype R] in
121 theorem records_positive (M : Model X E O C R) (h : ℕ) (V : Finset X) (t : Tree E O C h) :
122     1 ≤ (M.profile h V t).2 := by
123   cases h with
124   | zero => exact le_rfl
125   | succ h => cases t with
126     | inl c => exact le_rfl
127     | inr ek => exact Nat.le_add_right _ _
128 
129 omit [DecidableEq X] [Fintype E] [DecidableEq O] [Fintype C] [Fintype R] in
130 theorem nodeProfile_mono (M : Model X E O C R) (e : E)
131     (k l : O → Option (Profile R)) (hle : ∀ o, optional (k o) ≤ optional (l o)) :
132     M.nodeProfile e k ≤ M.nodeProfile e l := by
133   constructor
134   · intro r
135     apply Nat.add_le_add_left
136     apply Finset.sup_le
137     intro o _
138     exact ((hle o).1 r).trans (Finset.le_sup (f := fun o => (optional (l o)).1 r) (mem_univ o))
139   · exact Nat.add_le_add_left (Finset.sum_le_sum (fun o _ => (hle o).2)) 1
140 
141 /-- All acceptable terminal profiles at this support. -/
142 def stops (M : Model X E O C R) (V : Finset X) : Finset (Profile R) :=
143   (univ.filter (M.Terminal V)).image (fun c => (M.terminalCost c V, 1))
144 
145 omit [DecidableEq X] [Fintype E] [Fintype O] [DecidableEq O] in
146 @[simp] theorem mem_stops (M : Model X E O C R) (V : Finset X) (p : Profile R) :
147     p ∈ M.stops V ↔ ∃ c, M.Terminal V c ∧ (M.terminalCost c V, 1) = p := by
148   simp [stops]
149 
150 /-- Each report independently chooses one achievable child, unless it is impossible. -/
151 def options (M : Model X E O C R) (F : Finset X → Finset (Profile R))
152     (V : Finset X) (e : E) (o : O) : Finset (Option (Profile R)) :=
153   if (M.update V e o).Nonempty then (F (M.update V e o)).image some else {none}
154 
155 /-- One unpruned backup; the input family may already have been Pareto reduced. -/
156 def backup (M : Model X E O C R) (F : Finset X → Finset (Profile R))
157     (V : Finset X) : Finset (Profile R) :=
158   M.stops V ∪ univ.biUnion (fun e => if M.Allowed V e then
159     (Fintype.piFinset (M.options F V e)).image (M.nodeProfile e) else ∅)
160 
161 @[simp] theorem mem_backup (M : Model X E O C R) (F : Finset X → Finset (Profile R))
162     (V : Finset X) (p : Profile R) :
163     p ∈ M.backup F V ↔ p ∈ M.stops V ∨ ∃ e, M.Allowed V e ∧
164       ∃ k : O → Option (Profile R), (∀ o, k o ∈ M.options F V e o) ∧ M.nodeProfile e k = p := by
165   simp only [backup, mem_union, mem_biUnion, mem_univ, true_and]
166   constructor
167   · rintro (hs | ⟨e, he⟩)
168     · exact Or.inl hs
169     · by_cases ha : M.Allowed V e
170       · simp only [ha, ite_true, mem_image, Fintype.mem_piFinset] at he
171         exact Or.inr ⟨e, ha, he⟩
172       · simp [ha] at he
173   · rintro (hs | ⟨e, ha, k, hk, hp⟩)
174     · exact Or.inl hs
175     · exact Or.inr ⟨e, by simp only [ha, ite_true, mem_image, Fintype.mem_piFinset]; exact ⟨k, hk, hp⟩⟩
176 
177 noncomputable def solve (M : Model X E O C R) : ℕ → Finset X → Finset (Profile R)
178   | 0, V => HardPareto.frontier (M.stops V)
179   | h + 1, V => HardPareto.frontier (M.backup (M.solve h) V)
180 
181 /-- Soundness of one backup includes a complete concrete observation tree. -/
182 theorem backup_witness (M : Model X E O C R) (h : ℕ)
183     (F : Finset X → Finset (Profile R))
184     (sound : ∀ V p, p ∈ F V → ∃ t : Tree E O C h, M.Valid h V t ∧ M.profile h V t = p)
185     (V : Finset X) (p : Profile R) (hp : p ∈ M.backup F V) :
186     ∃ t : Tree E O C (h+1), M.Valid (h+1) V t ∧ M.profile (h+1) V t = p := by
187   classical
188   rcases (M.mem_backup F V p).mp hp with hs | ⟨e, ha, k, hk, he⟩
189   · obtain ⟨c, hc, he⟩ := (M.mem_stops V p).mp hs
190     exact ⟨.inl c, hc, he⟩
191   · have hw : ∀ o, ∃ t : Option (Tree E O C h),
192         (match t with | none => M.update V e o = ∅ | some t => M.Valid h (M.update V e o) t) ∧
193         t.map (M.profile h (M.update V e o)) = k o := by
194       intro o
195       by_cases hn : (M.update V e o).Nonempty
196       · have hm := hk o
197         simp only [options, hn, ite_true, mem_image] at hm
198         obtain ⟨q, hq, hko⟩ := hm
199         obtain ⟨t, hv, ht⟩ := sound _ q hq
200         exact ⟨some t, hv, by simpa only [Option.map_some, ht] using hko⟩
201       · have hm : k o = none := by simpa [options, hn] using hk o
202         exact ⟨none, Finset.not_nonempty_iff_eq_empty.mp hn, by simp [hm]⟩
203     let t : O → Option (Tree E O C h) := fun o => (hw o).choose
204     have hv : ∀ o, (match t o with | none => M.update V e o = ∅ | some t => M.Valid h (M.update V e o) t) :=
205       fun o => (hw o).choose_spec.1
206     have ht : (fun o => (t o).map (M.profile h (M.update V e o))) = k :=
207       funext (fun o => (hw o).choose_spec.2)
208     refine ⟨.inr (e,t), ⟨ha,hv⟩, ?_⟩
209     change M.nodeProfile e _ = p
210     rw [ht, he]
211 
212 /-- A dominating child replacement can be chosen at every actual branch simultaneously. -/
213 theorem backup_dominates (M : Model X E O C R) (h : ℕ)
214     (F : Finset X → Finset (Profile R))
215     (complete : ∀ V (t : Tree E O C h), M.Valid h V t → ∃ p ∈ F V, p ≤ M.profile h V t)
216     (V : Finset X) (t : Tree E O C (h+1)) (hv : M.Valid (h+1) V t) :
217     ∃ p ∈ M.backup F V, p ≤ M.profile (h+1) V t := by
218   classical
219   cases t with
220   | inl c => exact ⟨_, (M.mem_backup F V _).mpr (Or.inl ((M.mem_stops V _).mpr ⟨c,hv,rfl⟩)), le_rfl⟩
221   | inr ek =>
222     obtain ⟨e,k⟩ := ek
223     obtain ⟨ha,hk⟩ := hv
224     have hw : ∀ o, ∃ p ∈ M.options F V e o,
225         optional p ≤ optional ((k o).map (M.profile h (M.update V e o))) := by
226       intro o
227       cases heq : k o with
228       | none =>
229         have hz : M.update V e o = ∅ := by simpa only [heq] using hk o
230         exact ⟨none, by simp [options,hz], by simp⟩
231       | some t =>
232         have ht : M.Valid h (M.update V e o) t := by simpa only [heq] using hk o
233         have hn := M.valid_nonempty ht
234         obtain ⟨p,hp,hle⟩ := complete _ t ht
235         exact ⟨some p, by simp only [options,hn,ite_true,mem_image]; exact ⟨p,hp,rfl⟩,
236           by simpa [heq,optional] using hle⟩
237     let p : O → Option (Profile R) := fun o => (hw o).choose
238     refine ⟨M.nodeProfile e p, (M.mem_backup F V _).mpr (Or.inr ⟨e,ha,p,?_,rfl⟩), ?_⟩
239     · exact fun o => (hw o).choose_spec.1
240     · exact M.nodeProfile_mono e p _ (fun o => (hw o).choose_spec.2)
241 
242 /-- The dynamic program is sound and lower-cofinal in ALL valid tree profiles. -/
243 theorem solve_correct (M : Model X E O C R) (h : ℕ) :
244     (∀ V p, p ∈ M.solve h V → ∃ t : Tree E O C h, M.Valid h V t ∧ M.profile h V t = p) ∧
245     (∀ V (t : Tree E O C h), M.Valid h V t → ∃ p ∈ M.solve h V, p ≤ M.profile h V t) := by
246   induction h with
247   | zero =>
248     constructor
249     · intro V p hp
250       obtain ⟨c,hc,he⟩ := (M.mem_stops V p).mp (HardPareto.frontier_subset _ hp)
251       exact ⟨c,hc,he⟩
252     · intro V c hc
253       exact HardPareto.exists_frontier_le _ ((M.mem_stops V _).mpr ⟨c,hc,rfl⟩)
254   | succ h ih =>
255     constructor
256     · intro V p hp
257       exact M.backup_witness h (M.solve h) ih.1 V p (HardPareto.frontier_subset _ hp)
258     · intro V t ht
259       obtain ⟨p,hp,hle⟩ := M.backup_dominates h (M.solve h) ih.2 V t ht
260       obtain ⟨q,hq,hqp⟩ := HardPareto.exists_frontier_le _ hp
261       exact ⟨q,hq,hqp.trans hle⟩
262 
263 theorem solve_witness (M : Model X E O C R) (h : ℕ) (V : Finset X) (p : Profile R)
264     (hp : p ∈ M.solve h V) : ∃ t : Tree E O C h, M.Valid h V t ∧ M.profile h V t = p :=
265   (M.solve_correct h).1 V p hp
266 
267 theorem solve_dominates (M : Model X E O C R) (h : ℕ) (V : Finset X) (t : Tree E O C h)
268     (ht : M.Valid h V t) : ∃ p ∈ M.solve h V, p ≤ M.profile h V t :=
269   (M.solve_correct h).2 V t ht
270 
271 theorem solve_antichain (M : Model X E O C R) (h : ℕ) (V : Finset X)
272     {p q : Profile R} (hp : p ∈ M.solve h V) (hq : q ∈ M.solve h V) (hqp : q ≤ p) : p ≤ q := by
273   cases h with
274   | zero => exact ((HardPareto.mem_frontier _ _).mp hp).2 q (HardPareto.frontier_subset _ hq) hqp
275   | succ h => exact ((HardPareto.mem_frontier _ _).mp hp).2 q (HardPareto.frontier_subset _ hq) hqp
276 
277 /-- Core 5.1: EXACT nondominated profiles, not an upper approximation or separate optima. -/
278 theorem exact_frontier (M : Model X E O C R) (h : ℕ) (V : Finset X) (p : Profile R) :
279     p ∈ M.solve h V ↔
280       (∃ t : Tree E O C h, M.Valid h V t ∧ M.profile h V t = p) ∧
281       ∀ t : Tree E O C h, M.Valid h V t → M.profile h V t ≤ p → p ≤ M.profile h V t := by
282   constructor
283   · intro hp
284     refine ⟨M.solve_witness h V p hp, ?_⟩
285     intro t ht htp
286     obtain ⟨q,hq,hqt⟩ := M.solve_dominates h V t ht
287     exact (M.solve_antichain h V hp hq (hqt.trans htp)).trans hqt
288   · rintro ⟨⟨t,ht,he⟩,hmin⟩
289     obtain ⟨q,hq,hqt⟩ := M.solve_dominates h V t ht
290     rw [he] at hqt
291     obtain ⟨s,hs,hse⟩ := M.solve_witness h V q hq
292     have hpq : p ≤ q := by simpa only [hse] using hmin s hs (by simpa only [hse] using hqt)
293     exact (le_antisymm hpq hqt) ▸ hq
294 
295 /-- One online vector and one storage bound must be met by the SAME tree. -/
296 theorem joint_budget_iff (M : Model X E O C R) (h : ℕ) (V : Finset X) (b : Profile R) :
297     (∃ t : Tree E O C h, M.Valid h V t ∧ M.profile h V t ≤ b) ↔
298       ∃ p ∈ M.solve h V, p ≤ b := by
299   constructor
300   · rintro ⟨t,ht,hb⟩
301     obtain ⟨p,hp,hpt⟩ := M.solve_dominates h V t ht
302     exact ⟨p,hp,hpt.trans hb⟩
303   · rintro ⟨p,hp,hb⟩
304     obtain ⟨t,ht,he⟩ := M.solve_witness h V p hp
305     exact ⟨t,ht,by simpa only [he] using hb⟩
306 
307 /-- Exhaustion is complete only within the actual finite model and horizon. -/
308 theorem no_tree_iff_empty (M : Model X E O C R) (h : ℕ) (V : Finset X) :
309     (¬ ∃ t : Tree E O C h, M.Valid h V t) ↔ M.solve h V = ∅ := by
310   constructor
311   · intro ht
312     apply Finset.eq_empty_iff_forall_notMem.mpr
313     intro p hp
314     obtain ⟨t,hv,_⟩ := M.solve_witness h V p hp
315     exact ht ⟨t,hv⟩
316   · intro he ⟨t,ht⟩
317     obtain ⟨p,hp,_⟩ := M.solve_dominates h V t ht
318     simp only [he, Finset.notMem_empty] at hp
319 
320 end Model
321 end Komorebi.MachineTheory.HardInquiry

Back to source controls