PlanningSensor.lean

1 import MachineTheory.PlanningTransport
2 import Mathlib.Data.Fintype.BigOperators
3 import Mathlib.Tactic.FinCases
4 import Mathlib.Tactic.NormNum
5 import Mathlib.Tactic.Ring
6 import Mathlib.Tactic.FieldSimp
7 
8 /-! Exact source sensor, Core 5.4 worked example. No sampled outcomes or extracted numerical oracle. -/
9 namespace Komorebi.MachineTheory.PlanningSensor
10 open Instrument Planning BeliefPlanning
11 open scoped BigOperators
12 noncomputable section
13 
14 abbrev Pair := Bool × Bool
15 abbrev World := Bool × Bool × Bool
16 
17 def project (x : World) : Pair := (x.1, x.2.1)
18 
19 def accuracy (s o : Bool) : ℝ := if o = s then 3/4 else 1/4
20 
21 theorem accuracy_pos (s o : Bool) : 0 < accuracy s o := by
22   unfold accuracy; split_ifs <;> norm_num
23 
24 theorem accuracy_total (s : Bool) : (∑ o, accuracy s o) = 1 := by
25   cases s <;> norm_num [accuracy]
26 
27 def sensorLaw : Law Pair Unit Bool where
28   kernel _ o y x := if y = x then accuracy x.2 o else 0
29   nonnegative _ o y x := by split_ifs; exact le_of_lt (accuracy_pos _ _); exact le_rfl
30   normalized _ x := by simpa using accuracy_total x.2
31 
32 def fineLaw : Law World Unit Bool where
33   kernel _ o y x := if y = x then accuracy x.2.1 o else 0
34   nonnegative _ o y x := by split_ifs; exact le_of_lt (accuracy_pos _ _); exact le_rfl
35   normalized _ x := by simpa using accuracy_total x.2.1
36 
37 def contract : Contract Pair Unit Bool where
38   actions _ := {()}
39   decisions _ := Finset.univ
40   decisions_nonempty _ := Finset.univ_nonempty
41   charge _ _ := 1/20
42   charge_nonnegative _ _ := by norm_num
43   terminalLoss d z := if d = z.1 then 0 else 1
44 
45 theorem sensor_joint_quotient (a : Unit) (o : Bool) :
46     Intertwines project (fineLaw.kernel a o) (sensorLaw.kernel a o) := by
47   apply (intertwines_iff_rows _ _ _).mpr
48   intro z x
49   classical
50   simp only [fineLaw, sensorLaw]
51   rw [Finset.sum_eq_single x]
52   · by_cases hz : project x = z
53     · subst z; simp [project]
54     · have hz' : z ≠ project x := Ne.symm hz
55       simp [hz, hz']
56   · intro y _ hy
57     simp [hy]
58   · simp
59 
60 /-- The full eight-world theorem holds for every initial nuisance distribution and every horizon. -/
61 theorem sensor_all_prior_values (h : Nat) (p : Belief World) :
62     value (fineModel fineLaw project contract) h p =
63       value (coarseModel sensorLaw contract) h (aggregate project p) :=
64   (instrumentMap fineLaw sensorLaw project sensor_joint_quotient contract).value_eq h p
65 
66 abbrev Counts := Nat × Nat
67 
68 def wTrue (n : Counts) : ℝ := 3 ^ n.1
69 def wFalse (n : Counts) : ℝ := 3 ^ n.2
70 def total (n : Counts) : ℝ := wTrue n + wFalse n
71 
72 theorem wTrue_pos (n : Counts) : 0 < wTrue n := pow_pos (by norm_num) _
73 theorem wFalse_pos (n : Counts) : 0 < wFalse n := pow_pos (by norm_num) _
74 theorem total_pos (n : Counts) : 0 < total n := add_pos (wTrue_pos n) (wFalse_pos n)
75 
76 /-- Initial display zero fixes b=s. Counted reports then alter only the two diagonal masses. -/
77 def countBelief (n : Counts) : Belief Pair :=
78   ⟨fun z => if z.1 = z.2 then (if z.1 then wTrue n else wFalse n) / total n else 0, by
79     constructor
80     · intro z
81       have ha := wTrue_pos n
82       have hb := wFalse_pos n
83       have ht := total_pos n
84       rcases z with ⟨b,s⟩
85       cases b <;> cases s <;> dsimp <;> positivity
86     · norm_num [mass, Fintype.sum_prod_type]
87       rw [← add_div]
88       exact div_self (ne_of_gt (total_pos n))⟩
89 
90 def advance (n : Counts) (o : Bool) : Counts := if o then (n.1+1,n.2) else (n.1,n.2+1)
91 
92 def report (n : Counts) (o : Bool) : ℝ :=
93   if o then (3*wTrue n+wFalse n)/(4*total n)
94   else (wTrue n+3*wFalse n)/(4*total n)
95 
96 def stopRisk (n : Counts) (d : Bool) : ℝ :=
97   if d then wFalse n / total n else wTrue n / total n
98 
99 theorem report_pos (n : Counts) (o : Bool) : 0 < report n o := by
100   have ha := wTrue_pos n; have hb := wFalse_pos n; have ht := total_pos n
101   cases o <;> dsimp [report] <;> positivity
102 
103 theorem report_total (n : Counts) : (∑ o, report n o) = 1 := by
104   simp only [Fintype.sum_bool, report, Bool.false_eq_true, ite_false, ite_true]
105   have ht := ne_of_gt (total_pos n)
106   dsimp [total] at *
107   field_simp
108   ring
109 
110 def countModel : Model Counts Unit Bool Bool where
111   actions _ := {()}
112   decisions _ := Finset.univ
113   decisions_nonempty _ := Finset.univ_nonempty
114   cost _ _ := 1/20
115   cost_nonnegative _ _ := by norm_num
116   loss := stopRisk
117   prob n _ o := report n o
118   nonnegative n _ o := le_of_lt (report_pos n o)
119   normalized n _ := report_total n
120   next n _ o _ := advance n o
121 
122 theorem count_report_eq (n : Counts) (o : Bool) :
123     report n o = (coarseModel sensorLaw contract).prob (countBelief n) () o := by
124   have ht := ne_of_gt (total_pos n)
125   cases o <;>
126     simp [report, coarseModel, sensorLaw, countBelief, applyKernel, mass, accuracy,
127       Fintype.sum_prod_type, total] <;> field_simp
128 
129 theorem count_loss_eq (n : Counts) (d : Bool) :
130     stopRisk n d = (coarseModel sensorLaw contract).loss (countBelief n) d := by
131   cases d <;> simp [stopRisk, coarseModel, sensorLaw, contract, countBelief, Fintype.sum_prod_type]
132 
133 theorem count_update_eq (n : Counts) (o : Bool) (ho : 0 < report n o) :
134     countBelief (advance n o) = (coarseModel sensorLaw contract).next (countBelief n) () o
135       (by rw [← count_report_eq]; exact ho) := by
136   apply Subtype.ext
137   funext z
138   rcases z with ⟨b,s⟩
139   have ha := wTrue_pos n; have hb := wFalse_pos n
140   have ht := ne_of_gt (total_pos n)
141   have hu : 3*wTrue n+wFalse n ≠ 0 := ne_of_gt (by positivity)
142   have hv : wTrue n+3*wFalse n ≠ 0 := ne_of_gt (by positivity)
143   cases o <;> cases b <;> cases s <;>
144     simp [advance, countBelief, coarseModel, sensorLaw, normalize, mass, applyKernel,
145       Fintype.sum_prod_type, accuracy, total, wTrue, wFalse, pow_succ] at * <;>
146     field_simp
147 
148 /-- The count interface is proved to be the actual Bayesian sensor, not an independently asserted model. -/
149 theorem countMap : ExactMap countModel (coarseModel sensorLaw contract) countBelief where
150   actions _ := rfl
151   decisions _ := rfl
152   cost _ _ := rfl
153   loss := count_loss_eq
154   prob n a o := by cases a; exact count_report_eq n o
155   next n a o ho := by cases a; exact count_update_eq n o ho
156 
157 /-- A reduced arithmetic recursion, derived below from the finite-choice Bellman equation. -/
158 def scalarValue : Nat → Counts → ℝ
159   | 0,n => min (stopRisk n false) (stopRisk n true)
160   | h+1,n => min (min (stopRisk n false) (stopRisk n true))
161       (1/20 + report n false * scalarValue h (advance n false) +
162         report n true * scalarValue h (advance n true))
163 
164 theorem count_zero (n : Counts) : value countModel 0 n =
165     min (stopRisk n false) (stopRisk n true) := by
166   apply le_antisymm
167   · exact le_min (value_le_stop countModel 0 n false (by simp [countModel]))
168       (value_le_stop countModel 0 n true (by simp [countModel]))
169   · apply le_finiteMin
170     intro d _
171     cases d
172     · exact min_le_left _ _
173     · exact min_le_right _ _
174 
175 theorem count_succ (h : Nat) (n : Counts) : value countModel (h+1) n =
176     min (min (stopRisk n false) (stopRisk n true)) (backup countModel (value countModel h) n ()) := by
177   apply le_antisymm
178   · exact le_min (le_min (value_le_stop countModel _ n false (by simp [countModel]))
179         (value_le_stop countModel _ n true (by simp [countModel])))
180       (value_le_experiment countModel h n () (by simp [countModel]))
181   · apply le_finiteMin
182     intro c _
183     cases c with
184     | inl d =>
185         cases d
186         · exact le_trans (min_le_left _ _) (min_le_left _ _)
187         · exact le_trans (min_le_left _ _) (min_le_right _ _)
188     | inr a => cases a; exact min_le_right _ _
189 
190 theorem count_value_eq_scalar (h : Nat) (n : Counts) : value countModel h n = scalarValue h n := by
191   induction h generalizing n with
192   | zero => exact count_zero n
193   | succ h ih =>
194       rw [count_succ]
195       simp only [scalarValue]
196       congr 1
197       change (1/20 : ℝ) + (∑ o, if _ : 0 < report n o then
198         report n o * value countModel h (advance n o) else 0) = _
199       simp only [Fintype.sum_bool, report_pos, dite_true, ih]
200       ring
201 
202 /-- Exact values from the manuscript; Lean computes the finite recursion in rational real arithmetic. -/
203 theorem sensor_value_table :
204     value countModel 0 (0,0) = 1/2 ∧ value countModel 1 (0,0) = 3/10 ∧
205     value countModel 2 (0,0) = 3/10 ∧ value countModel 3 (0,0) = 11/40 := by
206   simp only [count_value_eq_scalar]
207   norm_num [scalarValue, stopRisk, report, advance, total, wTrue, wFalse]
208 
209 /-- The same exact numbers are the values of the genuine coarse instrument, not just the count code. -/
210 theorem coarse_sensor_value_three :
211     value (coarseModel sensorLaw contract) 3 (countBelief (0,0)) = 11/40 := by
212   rw [← countMap.value_eq]
213   exact sensor_value_table.2.2.2
214 
215 /-- The source adaptive policy: inspect twice; use a third report only on disagreement. -/
216 def adaptiveThree : Tree Unit Bool Bool :=
217   .experiment () (fun first => .experiment () (fun second =>
218     if first = second then .stop first else .experiment () (fun third => .stop third)))
219 
220 theorem adaptiveThree_bounded : adaptiveThree.Bounded 3 := by
221   simp [adaptiveThree, Tree.Bounded]
222 
223 theorem adaptiveThree_not_bounded_two : ¬ adaptiveThree.Bounded 2 := by
224   simp [adaptiveThree, Tree.Bounded]
225 
226 theorem adaptiveThree_feasible (n : Counts) : Feasible countModel 3 n adaptiveThree := by
227   simp [adaptiveThree, Feasible, countModel]
228 
229 theorem adaptiveThree_value : evaluate countModel adaptiveThree (0,0) = 11/40 := by
230   norm_num [adaptiveThree, evaluate, countModel, report, advance, stopRisk, total, wTrue, wFalse]
231 
232 theorem adaptiveThree_optimal :
233     Feasible countModel 3 (0,0) adaptiveThree ∧
234     (∀ P, Feasible countModel 3 (0,0) P →
235       evaluate countModel adaptiveThree (0,0) ≤ evaluate countModel P (0,0)) := by
236   refine ⟨adaptiveThree_feasible (0,0), ?_⟩
237   intro P hp
238   rw [adaptiveThree_value, ← sensor_value_table.2.2.2]
239   exact value_le_tree countModel 3 (0,0) P hp
240 
241 /-- The third report is genuinely reachable, with exact probability 3/8. -/
242 theorem adaptive_third_report_probability :
243     report (0,0) false * report (advance (0,0) false) true +
244       report (0,0) true * report (advance (0,0) true) false = 3/8 := by
245   norm_num [report, advance, total, wTrue, wFalse]
246 
247 /-- This auxiliary evaluator counts reports on exactly the same branches. -/
248 def reportCounter : Model Counts Unit Bool Bool :=
249   { countModel with
250     cost := fun _ _ => 1
251     cost_nonnegative := by intros; norm_num
252     loss := fun _ _ => 0 }
253 
254 /-- This auxiliary evaluator charges only the terminal classification error. -/
255 def errorCounter : Model Counts Unit Bool Bool :=
256   { countModel with
257     cost := fun _ _ => 0
258     cost_nonnegative := by intros; norm_num }
259 
260 theorem adaptiveThree_reports : evaluate reportCounter adaptiveThree (0,0) = 19/8 := by
261   norm_num [reportCounter, adaptiveThree, evaluate, countModel, report, advance, stopRisk, total, wTrue, wFalse]
262 
263 theorem adaptiveThree_error : evaluate errorCounter adaptiveThree (0,0) = 5/32 := by
264   norm_num [errorCounter, adaptiveThree, evaluate, countModel, report, advance, stopRisk, total, wTrue, wFalse]
265 
266 theorem cost_and_error_are_same_tree :
267     evaluate countModel adaptiveThree (0,0) =
268       (1/20) * evaluate reportCounter adaptiveThree (0,0) + evaluate errorCounter adaptiveThree (0,0) := by
269   rw [adaptiveThree_value, adaptiveThree_reports, adaptiveThree_error]
270   norm_num
271 
272 /-- The actual finite sensor tree is optimal for every eight-world prior with this same coarse belief. -/
273 theorem eight_world_adaptive_optimal (p : Belief World)
274     (hp : aggregate project p = countBelief (0,0)) :
275     Feasible (fineModel fineLaw project contract) 3 p adaptiveThree ∧
276     evaluate (fineModel fineLaw project contract) adaptiveThree p = 11/40 ∧
277     ∀ P, Feasible (fineModel fineLaw project contract) 3 p P →
278       (11/40 : ℝ) ≤ evaluate (fineModel fineLaw project contract) P p := by
279   have H := instrumentMap fineLaw sensorLaw project sensor_joint_quotient contract
280   have hc := countMap.feasible_iff 3 (0,0) adaptiveThree
281   have hv := countMap.evaluate_eq adaptiveThree (0,0)
282   refine ⟨?_, ?_, ?_⟩
283   · apply (H.feasible_iff 3 p adaptiveThree).mpr
284     rw [hp]
285     exact hc.mp (adaptiveThree_feasible (0,0))
286   · rw [H.evaluate_eq, hp, ← hv, adaptiveThree_value]
287   · intro P hP
288     have he : value (fineModel fineLaw project contract) 3 p = 11/40 := by
289       rw [H.value_eq, hp, coarse_sensor_value_three]
290     rw [← he]
291     exact value_le_tree _ 3 p P hP
292 
293 /-- Realization of an initial fine prior, not just an assumption that the fibre is inhabited. -/
294 def initialFine : Belief World :=
295   ⟨fun x => if x.1 = x.2.1 then 1/4 else 0, by
296     constructor
297     · intro x; dsimp; split_ifs <;> norm_num
298     · norm_num [mass, Fintype.sum_prod_type]⟩
299 
300 theorem initialFine_aggregates : aggregate project initialFine = countBelief (0,0) := by
301   apply Subtype.ext
302   funext z
303   rcases z with ⟨b,s⟩
304   cases b <;> cases s <;>
305     norm_num [aggregate, push, project, initialFine, countBelief, total, wTrue, wFalse,
306       Fintype.sum_prod_type]
307 
308 theorem source_sensor_optimum :
309     value (fineModel fineLaw project contract) 3 initialFine = 11/40 := by
310   rw [sensor_all_prior_values, initialFine_aggregates, coarse_sensor_value_three]
311 
312 end
313 end Komorebi.MachineTheory.PlanningSensor

Back to source controls