PlanningTransport.lean

1 import MachineTheory.Planning
2 
3 /-!
4 Core 5.4, exact transport of planning through a joint-instrument quotient.
5 The proof first establishes a general information-state simulation, then constructs
6 that simulation from actual fine/coarse probability beliefs and the checked instrument.
7 -/
8 namespace Komorebi.MachineTheory
9 namespace Planning
10 open scoped BigOperators
11 noncomputable section
12 
13 variable {S T A O D : Type*} [Fintype O]
14 
15 /-- Every operational input to planning must factor through the retained state. -/
16 structure ExactMap (M : Model S A O D) (N : Model T A O D) (f : S → T) : Prop where
17   actions : ∀ s, M.actions s = N.actions (f s)
18   decisions : ∀ s, M.decisions s = N.decisions (f s)
19   cost : ∀ s a, M.cost s a = N.cost (f s) a
20   loss : ∀ s d, M.loss s d = N.loss (f s) d
21   prob : ∀ s a o, M.prob s a o = N.prob (f s) a o
22   next : ∀ s a o (ho : 0 < M.prob s a o),
23     f (M.next s a o ho) = N.next (f s) a o (by rw [← prob s a o]; exact ho)
24 
25 variable {M : Model S A O D} {N : Model T A O D} {f : S → T}
26 
27 /-- Report-dependent continuation payoffs are preserved on exactly the positive branches. -/
28 theorem ExactMap.sum_eq (H : ExactMap M N f) (V : O → S → ℝ) (W : O → T → ℝ)
29     (hVW : ∀ o s, V o s = W o (f s)) (s : S) (a : A) :
30     (∑ o, if ho : 0 < M.prob s a o then M.prob s a o * V o (M.next s a o ho) else 0) =
31     ∑ o, if ho : 0 < N.prob (f s) a o then
32       N.prob (f s) a o * W o (N.next (f s) a o ho) else 0 := by
33   classical
34   apply Finset.sum_congr rfl
35   intro o _
36   by_cases ho : 0 < M.prob s a o
37   · have ho' : 0 < N.prob (f s) a o := by rw [← H.prob s a o]; exact ho
38     rw [dite_eq_left ho, dite_eq_left ho', hVW, H.next]
39     exact congrArg₂ (· * ·) (H.prob s a o) rfl
40   · have ho' : ¬ 0 < N.prob (f s) a o := by rw [← H.prob s a o]; exact ho
41     rw [dite_eq_right ho, dite_eq_right ho']
42 
43 theorem ExactMap.backup_eq (H : ExactMap M N f) (V : S → ℝ) (W : T → ℝ)
44     (hVW : ∀ s, V s = W (f s)) (s : S) (a : A) :
45     backup M V s a = backup N W (f s) a := by
46   unfold backup
47   rw [H.cost]
48   congr 1
49   exact H.sum_eq (fun _ => V) (fun _ => W) (fun _ => hVW) s a
50 
51 theorem ExactMap.menu_eq (H : ExactMap M N f) (s : S) : menu M s = menu N (f s) := by
52   classical
53   simp only [menu, H.actions, H.decisions]
54 
55 /-- Equality of Bellman values at every horizon, proved from the local operational map. -/
56 theorem ExactMap.value_eq (H : ExactMap M N f) (h : Nat) (s : S) :
57     value M h s = value N h (f s) := by
58   induction h generalizing s with
59   | zero =>
60       apply finiteMin_congr _ _ _ _ _ _ (H.decisions s)
61       intro d _
62       exact H.loss s d
63   | succ h ih =>
64       apply finiteMin_congr _ _ _ _ _ _ (H.menu_eq s)
65       intro c _
66       cases c with
67       | inl d => exact H.loss s d
68       | inr a => exact H.backup_eq (value M h) (value N h) ih s a
69 
70 /-- This compares each first experiment with itself, including all of its continuation branches. -/
71 theorem ExactMap.firstValue_eq (H : ExactMap M N f) (h : Nat) (s : S) (c : D ⊕ A) :
72     firstValue M h s c = firstValue N h (f s) c := by
73   cases c with
74   | inl d => exact H.loss s d
75   | inr a => exact H.backup_eq _ _ (H.value_eq h) s a
76 
77 /-- The complete minimizing first-choice set is preserved, not only one minimum number. -/
78 theorem ExactMap.optimalFirst_iff (H : ExactMap M N f) (h : Nat) (s : S) (c : D ⊕ A) :
79     OptimalFirst M h s c ↔ OptimalFirst N h (f s) c := by
80   simp only [OptimalFirst, H.menu_eq, H.firstValue_eq, H.value_eq]
81 
82 /-- In particular, the allowed optimal stopping decisions agree at horizon zero. -/
83 theorem ExactMap.optimalStop_iff (H : ExactMap M N f) (h : Nat) (s : S) (d : D) :
84     OptimalStop M h s d ↔ OptimalStop N h (f s) d := by
85   simp only [OptimalStop, H.decisions, H.loss, H.value_eq]
86 
87 /-- A fixed tree has the same expected loss on the fine and coarse realization. -/
88 theorem ExactMap.evaluate_eq (H : ExactMap M N f) (P : Tree A O D) (s : S) :
89     evaluate M P s = evaluate N P (f s) := by
90   induction P generalizing s with
91   | stop d => exact H.loss s d
92   | experiment a k ih =>
93       simp only [evaluate, H.cost]
94       congr 1
95       exact H.sum_eq (fun o => evaluate M (k o)) (fun o => evaluate N (k o)) ih s a
96 
97 /-- Fine legality and coarse legality agree at every positive-probability continuation. -/
98 theorem ExactMap.feasible_iff (H : ExactMap M N f) (h : Nat) (s : S) (P : Tree A O D) :
99     Feasible M h s P ↔ Feasible N h (f s) P := by
100   induction h generalizing s P with
101   | zero =>
102       cases P with
103       | stop d => simp only [Feasible, H.decisions]
104       | experiment a k => rfl
105   | succ h ih =>
106       cases P with
107       | stop d => simp only [Feasible, H.decisions]
108       | experiment a k =>
109           simp only [Feasible, H.actions]
110           apply and_congr_right
111           intro _
112           constructor
113           · intro hk o ho'
114             have ho : 0 < M.prob s a o := by rw [H.prob]; exact ho'
115             have hh := (ih (M.next s a o ho) (k o)).mp (hk o ho)
116             rw [H.next] at hh
117             exact hh
118           · intro hk o ho
119             have ho' : 0 < N.prob (f s) a o := by rw [← H.prob]; exact ho
120             apply (ih (M.next s a o ho) (k o)).mpr
121             rw [H.next]
122             exact hk o ho'
123 
124 /-- One coarse tree, constructed from q alone, works for every fine belief mapping to q. -/
125 theorem ExactMap.common_minimizing_tree (H : ExactMap M N f) (h : Nat) (q : T) :
126     ∃ P : Tree A O D, P.Bounded h ∧ Feasible N h q P ∧ evaluate N P q = value N h q ∧
127       ∀ s, f s = q → Feasible M h s P ∧ evaluate M P s = value M h s := by
128   obtain ⟨P, hb, hp, he⟩ := minimizing_tree_exists N h q
129   refine ⟨P, hb, hp, he, ?_⟩
130   intro s hs
131   constructor
132   · exact (H.feasible_iff h s P).mpr (hs.symm ▸ hp)
133   · rw [H.evaluate_eq, H.value_eq, hs, he]
134 
135 end
136 end Planning
137 
138 namespace BeliefPlanning
139 open Instrument Planning
140 open scoped BigOperators
141 noncomputable section
142 
143 /-- A belief carries its positivity and normalization proof. -/
144 abbrev Belief (X : Type*) [Fintype X] := {p : X → ℝ // IsDist p}
145 
146 variable {X Z A O D : Type*} [Fintype X] [Fintype Z] [Fintype O] [DecidableEq Z]
147 
148 def aggregate (π : X → Z) (p : Belief X) : Belief Z := ⟨push π p.val, push_dist π p.val p.property⟩
149 
150 /-- Catalogues and charges are functions of the observable coarse belief. Terminal loss is statewise. -/
151 structure Contract (Z A D : Type*) [Fintype Z] where
152   actions : Belief Z → Finset A
153   decisions : Belief Z → Finset D
154   decisions_nonempty : ∀ q, (decisions q).Nonempty
155   charge : Belief Z → A → ℝ
156   charge_nonnegative : ∀ q a, 0 ≤ charge q a
157   terminalLoss : D → Z → ℝ
158 
159 /-- Fine-model planning has access only to catalogues and charges inherited from C p. -/
160 def fineModel (K : Law X A O) (π : X → Z) (C : Contract Z A D) :
161     Model (Belief X) A O D where
162   actions p := C.actions (aggregate π p)
163   decisions p := C.decisions (aggregate π p)
164   decisions_nonempty p := C.decisions_nonempty (aggregate π p)
165   cost p a := C.charge (aggregate π p) a
166   cost_nonnegative p a := C.charge_nonnegative (aggregate π p) a
167   loss p d := ∑ x, p.val x * C.terminalLoss d (π x)
168   prob p a o := mass (applyKernel (K.kernel a o) p.val)
169   nonnegative p a o := Finset.sum_nonneg (fun x _ =>
170     apply_nonnegative _ (K.nonnegative a o) p.val p.property.1 x)
171   normalized p a := (report_mass_total K a p.val).trans p.property.2
172   next p a o ho := ⟨normalize (applyKernel (K.kernel a o) p.val),
173     normalize_dist _ (apply_nonnegative _ (K.nonnegative a o) p.val p.property.1) ho⟩
174 
175 /-- The coarse planner uses the actual normalized coarse instrument. -/
176 def coarseModel (L : Law Z A O) (C : Contract Z A D) : Model (Belief Z) A O D where
177   actions := C.actions
178   decisions := C.decisions
179   decisions_nonempty := C.decisions_nonempty
180   cost := C.charge
181   cost_nonnegative := C.charge_nonnegative
182   loss q d := ∑ z, q.val z * C.terminalLoss d z
183   prob q a o := mass (applyKernel (L.kernel a o) q.val)
184   nonnegative q a o := Finset.sum_nonneg (fun z _ =>
185     apply_nonnegative _ (L.nonnegative a o) q.val q.property.1 z)
186   normalized q a := (report_mass_total L a q.val).trans q.property.2
187   next q a o ho := ⟨normalize (applyKernel (L.kernel a o) q.val),
188     normalize_dist _ (apply_nonnegative _ (L.nonnegative a o) q.val q.property.1) ho⟩
189 
190 /-- Aggregation preserves every terminal risk whose loss factors through the retained state. -/
191 theorem terminal_risk_eq (π : X → Z) (p : X → ℝ) (l : Z → ℝ) :
192     (∑ x, p x * l (π x)) = ∑ z, push π p z * l z := by
193   classical
194   simp only [push, Finset.sum_mul, ite_mul, zero_mul]
195   rw [Finset.sum_comm]
196   apply Finset.sum_congr rfl
197   intro x _
198   simp
199 
200 /-- The operational planning map is derived from, not substituted for, the joint-law theorem. -/
201 theorem instrumentMap (K : Law X A O) (L : Law Z A O) (π : X → Z)
202     (H : ∀ a o, Intertwines π (K.kernel a o) (L.kernel a o)) (C : Contract Z A D) :
203     ExactMap (fineModel K π C) (coarseModel L C) (aggregate π) where
204   actions _ := rfl
205   decisions _ := rfl
206   cost _ _ := rfl
207   loss p d := terminal_risk_eq π p.val (C.terminalLoss d)
208   prob p a o := report_mass_eq π (H a o) p.val
209   next p a o _ := by
210     apply Subtype.ext
211     change push π (normalize (applyKernel (K.kernel a o) p.val)) =
212       normalize (applyKernel (L.kernel a o) (push π p.val))
213     rw [push_normalize, H a o p.val]
214 
215 /-- Core 5.4: equal finite-horizon values, all first-choice values, and all optimal first-choice sets. -/
216 theorem compressed_belief_planning (K : Law X A O) (L : Law Z A O) (π : X → Z)
217     (H : ∀ a o, Intertwines π (K.kernel a o) (L.kernel a o)) (C : Contract Z A D)
218     (h : Nat) (p : Belief X) :
219     value (fineModel K π C) h p = value (coarseModel L C) h (aggregate π p) ∧
220     (∀ c, firstValue (fineModel K π C) h p c =
221       firstValue (coarseModel L C) h (aggregate π p) c) ∧
222     (∀ c, OptimalFirst (fineModel K π C) h p c ↔
223       OptimalFirst (coarseModel L C) h (aggregate π p) c) :=
224   ⟨(instrumentMap K L π H C).value_eq h p,
225     (instrumentMap K L π H C).firstValue_eq h p,
226     (instrumentMap K L π H C).optimalFirst_iff h p⟩
227 
228 /-- A finite optimal policy tree can be chosen from the coarse belief, uniformly over its entire fibre. -/
229 theorem common_optimal_inquiry (K : Law X A O) (L : Law Z A O) (π : X → Z)
230     (H : ∀ a o, Intertwines π (K.kernel a o) (L.kernel a o)) (C : Contract Z A D)
231     (h : Nat) (q : Belief Z) :
232     ∃ P : Tree A O D, P.Bounded h ∧ Feasible (coarseModel L C) h q P ∧
233       evaluate (coarseModel L C) P q = value (coarseModel L C) h q ∧
234       ∀ p : Belief X, aggregate π p = q → Feasible (fineModel K π C) h p P ∧
235         evaluate (fineModel K π C) P p = value (fineModel K π C) h p :=
236   (instrumentMap K L π H C).common_minimizing_tree h q
237 
238 /-- Even the coarse instrument is an output of the checked fibre criterion, not an assumed oracle. -/
239 theorem constructed_quotient_planning (K : Law X A O) (π : X → Z)
240     (hπ : Function.Surjective π) (hc : FiberCriterion π K.kernel)
241     (C : Contract Z A D) (h : Nat) (p : Belief X) :
242     value (fineModel K π C) h p = value (coarseModel (coarseLaw π hπ K) C) h (aggregate π p) :=
243   (instrumentMap K (coarseLaw π hπ K) π (coarseLaw_intertwines π hπ K hc) C).value_eq h p
244 
245 end
246 end BeliefPlanning
247 end Komorebi.MachineTheory

Back to source controls