PlanningControls.lean

1 import MachineTheory.PlanningSensor
2 
3 /-! Kernel-checked boundaries of the planning result. Models here are explicitly separate
4 from the manuscript sensor when their menus, losses, or charges differ. -/
5 namespace Komorebi.MachineTheory.PlanningControls
6 open Instrument Planning BeliefPlanning PlanningSensor
7 open scoped BigOperators
8 noncomputable section
9 
10 /-- Only the permitted terminal decision costs two; a forbidden zero-loss decision is not an option. -/
11 def noExperiments : Model Unit Unit Bool Bool where
12   actions _ := ∅
13   decisions _ := {false}
14   decisions_nonempty _ := by simp
15   cost _ _ := 0
16   cost_nonnegative _ _ := le_rfl
17   loss _ d := if d then 0 else 2
18   prob _ _ o := if o then 0 else 1
19   nonnegative _ _ o := by cases o <;> norm_num
20   normalized _ _ := by norm_num
21   next _ _ _ _ := ()
22 
23 theorem empty_experiment_menu_value (h : Nat) : value noExperiments h () = 2 := by
24   cases h <;> simp [value, finiteMin, menu, noExperiments]
25 
26 theorem forbidden_terminal_not_optimized : ¬ Feasible noExperiments 0 () (.stop true) := by
27   simp [Feasible, noExperiments]
28 
29 /-- A permissible experiment has one possible report. -/
30 def oneReport : Model Unit Unit Bool Bool :=
31   { noExperiments with
32     actions := fun _ => {()}
33     cost := fun _ _ => 1/2
34     cost_nonnegative := by intros; norm_num }
35 
36 def dormantBranch : Tree Unit Bool Bool :=
37   .experiment () (fun o => if o then .stop true else .stop false)
38 
39 /-- The dormant branch has a syntactic placeholder, but no posterior or permission claim is made there. -/
40 theorem impossible_branch_ignored : Feasible oneReport 1 () dormantBranch := by
41   simp [Feasible, oneReport, noExperiments, dormantBranch]
42 
43 theorem impossible_branch_cost_zero : evaluate oneReport dormantBranch () = 5/2 := by
44   norm_num [evaluate, oneReport, noExperiments, dormantBranch]
45 
46 theorem zero_horizon_forbids_experiment : ¬ Feasible oneReport 0 () dormantBranch := by
47   simp [Feasible, dormantBranch]
48 
49 /-- Current information states have the same observation law but different legal terminal choices. -/
50 def permissions : Model Bool Unit Unit Bool where
51   actions _ := ∅
52   decisions b := {b}
53   decisions_nonempty _ := by simp
54   cost _ _ := 0
55   cost_nonnegative _ _ := le_rfl
56   loss _ _ := 0
57   prob _ _ _ := 1
58   nonnegative _ _ _ := by norm_num
59   normalized _ _ := by simp
60   next b _ _ _ := b
61 
62 theorem same_reports_different_permissions :
63     permissions.prob false () () = permissions.prob true () () ∧
64     Feasible permissions 0 false (.stop false) ∧ ¬ Feasible permissions 0 true (.stop false) := by
65   simp [permissions, Feasible]
66 
67 /-- No one-state planner can preserve both of these terminal catalogues. -/
68 theorem no_common_permission_quotient (N : Model Unit Unit Unit Bool) :
69     ¬ ExactMap permissions N (fun _ => ()) := by
70   intro H
71   have he := (H.decisions false).trans (H.decisions true).symm
72   have hm : false ∈ permissions.decisions true := he ▸ (by simp [permissions])
73   simp [permissions] at hm
74 
75 /-- Even equality of optimal numbers does not imply equality of minimizing choices. -/
76 def differentTargets : Model Bool Unit Unit Bool :=
77   { permissions with
78     decisions := fun _ => Finset.univ
79     decisions_nonempty := fun _ => Finset.univ_nonempty
80     loss := fun b d => if b = d then 0 else 1 }
81 
82 theorem equal_values_different_choices :
83     value differentTargets 1 false = value differentTargets 1 true ∧
84     OptimalFirst differentTargets 0 false (.inl false) ∧
85     ¬ OptimalFirst differentTargets 0 true (.inl false) := by
86   norm_num [value, finiteMin, menu, differentTargets, permissions, OptimalFirst, firstValue]
87 
88 /-- Raising a measurement fee leaves all sensor probabilities and posterior updates unchanged. -/
89 def expensiveSensor : Model Counts Unit Bool Bool :=
90   { countModel with
91     cost := fun _ _ => 1
92     cost_nonnegative := by intros; norm_num }
93 
94 theorem expense_preserves_reports (n : Counts) (o : Bool) :
95     expensiveSensor.prob n () o = countModel.prob n () o := rfl
96 
97 theorem expense_preserves_update (n : Counts) (o : Bool)
98     (ho : 0 < expensiveSensor.prob n () o) :
99     expensiveSensor.next n () o ho = countModel.next n () o ho := rfl
100 
101 theorem expensive_zero (n : Counts) : value expensiveSensor 0 n = scalarValue 0 n :=
102   count_value_eq_scalar 0 n
103 
104 theorem expensive_first_query : backup expensiveSensor (value expensiveSensor 0) (0,0) () = 5/4 := by
105   change (1 : ℝ) + (∑ o, if _ : 0 < report (0,0) o then
106     report (0,0) o * value expensiveSensor 0 (advance (0,0) o) else 0) = _
107   simp only [Fintype.sum_bool, report_pos, dite_true, expensive_zero]
108   norm_num [scalarValue, stopRisk, report, advance, total, wTrue, wFalse]
109 
110 theorem expensive_value : value expensiveSensor 1 (0,0) = 1/2 := by
111   apply le_antisymm
112   · have h := value_le_stop expensiveSensor 1 (0,0) false (by simp [expensiveSensor, countModel])
113     change value expensiveSensor 1 (0,0) ≤ stopRisk (0,0) false at h
114     norm_num [stopRisk, total, wTrue, wFalse] at h
115     exact h
116   · apply le_finiteMin
117     intro c _
118     cases c with
119     | inl d => cases d <;> norm_num [expensiveSensor, countModel, stopRisk, total, wTrue, wFalse]
120     | inr a => cases a; change (1/2 : ℝ) ≤ backup expensiveSensor (value expensiveSensor 0) (0,0) ()
121                rw [expensive_first_query]; norm_num
122 
123 theorem unchanged_filter_different_value :
124     value countModel 1 (0,0) ≠ value expensiveSensor 1 (0,0) := by
125   rw [sensor_value_table.2.1, expensive_value]
126   norm_num
127 
128 theorem expensive_experiment_not_optimal : ¬ OptimalFirst expensiveSensor 0 (0,0) (.inr ()) := by
129   intro h
130   have he := h.2
131   change backup expensiveSensor (value expensiveSensor 0) (0,0) () = value expensiveSensor 1 (0,0) at he
132   rw [expensive_first_query, expensive_value] at he
133   norm_num at he
134 
135 end
136 end Komorebi.MachineTheory.PlanningControls

Back to source controls