HardExecution.lean

1 import MachineTheory.HardInquiry
2 import MachineTheory.RecipientExecution
3 
4 /-!
5 # Execution and fixed-recipient specialization
6 
7 The interpreter receives an actual state only as the environment simulation.
8 A controller chooses its root experiment in advance, then branches solely on its
9 report. The stored plan has no hidden-state selector. These exact semantics do
10 not verify arbitrary host code or assert physical fidelity of a supplied table.
11 -/
12 namespace Komorebi.MachineTheory.HardInquiry
13 open Finset
14 variable {X E O C R : Type}
15 
16 structure Receipt (X E O C R : Type) where
17   finalState : X
18   artifact : C
19   cost : R → ℕ
20   history : List (E × O)
21 
22 namespace Model
23 
24 /-- A primitive execution receipt is extended by the experiment just performed. -/
25 def prepend (M : Model X E O C R) (e : E) (o : O) (r : Receipt X E O C R) : Receipt X E O C R :=
26   { r with cost := fun j => M.stepCost e j + r.cost j, history := (e,o) :: r.history }
27 
28 /-- This interpreter has no support argument and never selects using a hidden case label. -/
29 def execute (M : Model X E O C R) (charge : C → X → R → ℕ) :
30     (h : ℕ) → Tree E O C h → X → Option (Receipt X E O C R)
31   | 0, c, x => some ⟨x,c,charge c x,[]⟩
32   | _+1, .inl c, x => some ⟨x,c,charge c x,[]⟩
33   | h+1, .inr (e,k), x => if M.permitted e x then
34       (k (M.observe e x)).bind (fun t =>
35         (M.execute charge h t (M.next e x)).map (M.prepend e (M.observe e x)))
36     else none
37 
38 variable [DecidableEq X] [Fintype O] [DecidableEq O]
39 
40 /-- Actual terminal work is maximized over the SAME possible post-action states. -/
41 def ChargesBounded (M : Model X E O C R) (charge : C → X → R → ℕ) : Prop :=
42   ∀ c V x, x ∈ V → ∀ r, charge c x r ≤ M.terminalCost c V r
43 
44 /-- Online bounds cover every actual execution, including the terminal recipient work. -/
45 theorem execution_sound (M : Model X E O C R) (charge : C → X → R → ℕ)
46     (hc : M.ChargesBounded charge) (h : ℕ) (V : Finset X) (t : Tree E O C h)
47     (hv : M.Valid h V t) (x : X) (hx : x ∈ V) :
48     ∃ r, M.execute charge h t x = some r ∧ M.accept r.finalState r.artifact = true ∧
49       r.cost ≤ (M.profile h V t).1 ∧ r.history.length ≤ h := by
50   induction h generalizing V x with
51   | zero =>
52     exact ⟨⟨x,t,charge t x,[]⟩,rfl,hv.2 x hx,hc t V x hx,le_rfl⟩
53   | succ h ih =>
54     cases t with
55     | inl c => exact ⟨⟨x,c,charge c x,[]⟩,rfl,hv.2 x hx,hc c V x hx,Nat.zero_le _⟩
56     | inr ek =>
57       obtain ⟨e,k⟩ := ek
58       have hp := hv.1.2 x hx
59       have hn := M.actual_next_mem hx e
60       cases he : k (M.observe e x) with
61       | none =>
62         have hz : M.update V e (M.observe e x) = ∅ := by simpa only [he] using hv.2 (M.observe e x)
63         rw [hz] at hn
64         exact False.elim (Finset.notMem_empty _ hn)
65       | some child =>
66         have hh : M.Valid h (M.update V e (M.observe e x)) child := by simpa only [he] using hv.2 (M.observe e x)
67         obtain ⟨r,hr,ha,hcost,hhist⟩ := ih _ child hh _ hn
68         refine ⟨M.prepend e (M.observe e x) r, ?_, ha, ?_, Nat.succ_le_succ hhist⟩
69         · simp only [execute,hp,ite_true,he,Option.bind_some,hr,Option.map_some]
70         · intro j
71           change M.stepCost e j + r.cost j ≤ M.stepCost e j + _
72           apply Nat.add_le_add_left
73           apply (hcost j).trans
74           have hl := Finset.le_sup (s := (univ : Finset O))
75             (f := fun o => (optional ((k o).map (M.profile h (M.update V e o)))).1 j)
76             (mem_univ (M.observe e x))
77           simpa only [he,Option.map_some,optional,Option.getD_some] using hl
78 
79 /-- Literal node count, separate from execution and from the number of visited nodes. -/
80 def records : (h : ℕ) → Tree E O C h → ℕ
81   | 0, _ => 1
82   | _+1, .inl _ => 1
83   | h+1, .inr (_,k) => 1 + ∑ o, ((k o).map (records h)).getD 0
84 
85 omit [DecidableEq X] [DecidableEq O] in
86  theorem records_pos (h : ℕ) (t : Tree E O C h) : 1 ≤ records h t := by
87   cases h with
88   | zero => exact le_rfl
89   | succ h => cases t with
90     | inl _ => exact le_rfl
91     | inr _ => exact Nat.le_add_right _ _
92 
93 theorem profile_records (M : Model X E O C R) (h : ℕ) (V : Finset X) (t : Tree E O C h) :
94     (M.profile h V t).2 = records h t := by
95   induction h generalizing V with
96   | zero => rfl
97   | succ h ih =>
98     cases t with
99     | inl _ => rfl
100     | inr ek =>
101       obtain ⟨e,k⟩ := ek
102       change 1 + _ = 1 + _
103       congr 1
104       apply Finset.sum_congr rfl
105       intro o _
106       cases he : k o with
107       | none => simp [he,optional]
108       | some child => simpa only [he,Option.map_some,optional,Option.getD_some] using ih (M.update V e o) child
109 
110 /-- A concrete model using per-case terminal costs satisfies the required bound. -/
111 def withTerminalCharges (M : Model X E O C R) (charge : C → X → R → ℕ) : Model X E O C R :=
112   { M with terminalCost := fun c V r => V.sup (fun x => charge c x r) }
113 
114 omit [DecidableEq X] [Fintype O] [DecidableEq O] in
115  theorem withTerminalCharges_bound (M : Model X E O C R) (charge : C → X → R → ℕ) :
116     (M.withTerminalCharges charge).ChargesBounded charge := by
117   intro c V x hx r
118   exact Finset.le_sup (f := fun x => charge c x r) hx
119 
120 variable [Fintype E] [Fintype C] [Fintype R]
121 
122 instance profileLE : DecidableRel ((· ≤ ·) : Profile R → Profile R → Prop) :=
123   fun p q => inferInstanceAs (Decidable ((∀ r, p.1 r ≤ q.1 r) ∧ p.2 ≤ q.2))
124 
125 /-- A computable finite reducer with the same mathematical Pareto definition. -/
126 def prune (s : Finset (Profile R)) : Finset (Profile R) :=
127   s.filter (fun p => ∀ q ∈ s, q ≤ p → p ≤ q)
128 
129 omit [DecidableEq X] [Fintype E] [Fintype O] [DecidableEq O] [Fintype C] in
130  theorem prune_eq_frontier (s : Finset (Profile R)) : prune s = HardPareto.frontier s := by
131   ext p
132   simp only [prune,mem_filter,HardPareto.mem_frontier]
133 
134 /-- Executable finite profile recurrence, with no heuristic deletion. -/
135 def compute (M : Model X E O C R) : ℕ → Finset X → Finset (Profile R)
136   | 0, V => prune (M.stops V)
137   | h+1, V => prune (M.backup (M.compute h) V)
138 
139 theorem compute_eq_solve (M : Model X E O C R) (h : ℕ) : M.compute h = M.solve h := by
140   induction h with
141   | zero => funext V; exact prune_eq_frontier _
142   | succ h ih => funext V; simp only [compute,solve,ih,prune_eq_frontier]
143 
144 theorem computed_budget_iff (M : Model X E O C R) (h : ℕ) (V : Finset X) (b : Profile R) :
145     (∃ t : Tree E O C h, M.Valid h V t ∧ M.profile h V t ≤ b) ↔
146       ∃ p ∈ M.compute h V, p ≤ b := by
147   rw [M.compute_eq_solve]
148   exact M.joint_budget_iff h V b
149 
150 /-- A witness for hard budgets also certifies all recipient outputs on actual executions. -/
151 theorem budget_execution (M : Model X E O C R) (charge : C → X → R → ℕ)
152     (hc : M.ChargesBounded charge) (h : ℕ) (V : Finset X) (b : Profile R)
153     (hb : ∃ p ∈ M.compute h V, p ≤ b) :
154     ∃ t : Tree E O C h, M.Valid h V t ∧ records h t ≤ b.2 ∧
155       ∀ x ∈ V, ∃ r, M.execute charge h t x = some r ∧
156         M.accept r.finalState r.artifact = true ∧ r.cost ≤ b.1 ∧ r.history.length ≤ h := by
157   obtain ⟨t,ht,hp⟩ := (M.computed_budget_iff h V b).mpr hb
158   refine ⟨t,ht,?_,?_⟩
159   · rw [← M.profile_records h V t]
160     exact hp.2
161   · intro x hx
162     obtain ⟨r,hr,ha,hc,hh⟩ := M.execution_sound charge hc h V t ht x hx
163     exact ⟨r,hr,ha,hc.trans hp.1,hh⟩
164 
165 end Model
166 
167 namespace AudienceBridge
168 variable {I : Type} {B Y : I → Type}
169 variable [DecidableEq X] [Fintype E] [Fintype O] [DecidableEq O]
170   [Fintype C] [Fintype R]
171 
172 /-- The fixed installed audience, not a newly designed decoder, defines terminal success. -/
173 noncomputable def attach (M : Model X E O C R)
174     (A : RecipientExecution.Audience X C I B Y) : Model X E O C R := by
175   classical
176   exact { M with accept := fun x c => decide (A.Accepts x c) }
177 
178 omit [DecidableEq X] [Fintype E] [Fintype O] [DecidableEq O] [Fintype C] [Fintype R] in
179  theorem attached_accept (M : Model X E O C R)
180     (A : RecipientExecution.Audience X C I B Y) (x : X) (c : C) :
181     (attach M A).accept x c = true ↔ A.Accepts x c := by
182   classical
183   simp [attach]
184 
185 omit [DecidableEq X] [Fintype E] [Fintype O] [DecidableEq O] [Fintype C] [Fintype R] in
186 /-- A single attained record over a current support requires a common artifact. -/
187 theorem terminal_common (M : Model X E O C R) (A : RecipientExecution.Audience X C I B Y)
188     (V : Finset X) (c : C) :
189     (attach M A).Terminal V c ↔ V.Nonempty ∧ ∀ x ∈ V, A.Accepts x c := by
190   simp only [Model.Terminal,attached_accept]
191 
192 /-- Core 5.1 instantiated with Block06's unchanged fixed-recipient acceptance. -/
193 theorem recipient_inquiry (M : Model X E O C R)
194     (A : RecipientExecution.Audience X C I B Y) (h : ℕ) (V : Finset X) (b : Profile R) :
195     (∃ t : Tree E O C h, (attach M A).Valid h V t ∧ (attach M A).profile h V t ≤ b) ↔
196       ∃ p ∈ (attach M A).solve h V, p ≤ b :=
197   (attach M A).joint_budget_iff h V b
198 
199 end AudienceBridge
200 end Komorebi.MachineTheory.HardInquiry

Back to source controls