PriceExamples.lean

1 import MachineTheory.WorkloadPricing
2 import MachineTheory.PrefixExamples
3 
4 /-! # Price-sensitive value of the actual ordered compiler
5 
6 False names a report-table read and true names a capacity test. The two event
7 counters below are projections of Block 10's actual search results. No setup,
8 allocation, semantic check, peak-memory, or host-time cost is inferred from them.
9 -/
10 namespace Komorebi.MachineTheory.PriceExamples
11 open ResourcePrices Finset
12 open scoped BigOperators
13 noncomputable section
14 
15 def fullCounts (event : Bool) : ℕ :=
16   if event then PrefixExamples.fullEight.checks else PrefixExamples.fullEight.reads
17 
18 def streamCounts (event : Bool) : ℕ :=
19   if event then PrefixExamples.streamEight.checks else PrefixExamples.streamEight.reads
20 
21 def perUse (event : Bool) : ℝ := (fullCounts event : ℝ) - streamCounts event
22 
23 def prices (readPrice testPrice : ℝ) : Bool → ℝ := fun b => if b then testPrice else readPrice
24 
25 /-- Literal projections of the inherited full/streaming search counter theorem. -/
26 theorem counter_binding :
27     fullCounts false=184 ∧ fullCounts true=45 ∧ streamCounts false=153 ∧ streamCounts true=198 := by
28   have h := PrefixExamples.eight_measured_reads
29   exact ⟨congrArg (fun x => x.1) h,congrArg (fun x => x.2.1) h,
30     congrArg (fun x => x.2.2.1) h,congrArg (fun x => x.2.2.2) h⟩
31 
32 theorem actual_delta : perUse = prices 31 (-153) := by
33   funext b
34   rcases counter_binding with ⟨h0,h1,h2,h3⟩
35   cases b <;> norm_num [perUse,prices,h0,h1,h2,h3]
36 
37 /-- The comparison is derived from the actual signed difference, not inserted as data. -/
38 theorem priced_scan (r t : ℝ) : saving perUse (prices r t) = 31*r-153*t := by
39   rw [actual_delta]
40   simp [saving,prices]
41   ring
42 
43 theorem same_valid_controller :
44     PrefixExamples.streamEight.answer=PrefixExamples.fullEight.answer ∧
45     ∀ t, PrefixExamples.streamEight.answer=some t → BinaryExamples.eight.Valid 3 univ t :=
46   ⟨PrefixExamples.eight_same_literal_answer,PrefixExamples.eight_returned_valid⟩
47 
48 theorem source_price_reversal : saving perUse (prices 5 1)=2 ∧ saving perUse (prices 1 1)= -122 := by
49   constructor <;> rw [priced_scan] <;> norm_num
50 
51 theorem not_universally_beneficial :
52     ¬ ∀ w : Bool → ℝ, (∀ i,0 ≤ w i) → 0 ≤ saving perUse w := by
53   rw [all_nonnegative_prices_iff,actual_delta]
54   intro h
55   have ht := h true
56   norm_num [prices] at ht
57 
58 /-- Natural subtraction destroys the negative coordinate before pricing. -/
59 theorem natural_subtraction_loses_cost :
60     fullCounts true-streamCounts true=0 ∧ (fullCounts true : ℝ)-streamCounts true= -153 := by
61   rcases counter_binding with ⟨_,h1,_,h3⟩
62   rw [h1,h3]
63   norm_num
64 
65 def expensivePrices : Finset (Bool → ℝ) := by
66   classical
67   exact {prices 5 1,prices 8 1}
68 
69 theorem expensive_nonempty : expensivePrices.Nonempty := by
70   classical
71   simp [expensivePrices]
72 
73 theorem listed_minimum : Planning.finiteMin expensivePrices expensive_nonempty (saving perUse)=2 := by
74   classical
75   apply le_antisymm
76   · have h := Planning.finiteMin_le expensivePrices expensive_nonempty (saving perUse)
77       (prices 5 1) (by simp [expensivePrices])
78     rw [priced_scan] at h
79     norm_num at h
80     exact h
81   · apply Planning.le_finiteMin
82     intro w hw
83     simp only [expensivePrices,mem_insert,mem_singleton] at hw
84     rcases hw with rfl | rfl <;> rw [priced_scan] <;> norm_num
85 
86 /-- Every convex-mixture price in this declared family saves at least two units. -/
87 theorem expensive_hull_minimum :
88     IsLeast ((saving perUse) '' convexHull ℝ (expensivePrices : Set (Bool → ℝ))) 2 := by
89   obtain ⟨_,_,_,h⟩ := finite_price_minimum perUse expensivePrices expensive_nonempty
90   rwa [listed_minimum] at h
91 
92 /-- Positivity on one price family says nothing about a price outside it. -/
93 theorem equal_price_outside_family :
94     prices 1 1 ∉ convexHull ℝ (expensivePrices : Set (Bool → ℝ)) := by
95   intro h
96   have hh := expensive_hull_minimum.2 ⟨prices 1 1,h,rfl⟩
97   rw [priced_scan] at hh
98   norm_num at hh
99 
100 /-- A hypothetical extra preparation account: 200 capacity-test units and no reads. -/
101 def extraPreparation : Bool → ℝ := prices 0 200
102 
103 def paid (N : ℕ) : Bool → ℝ := repeated extraPreparation perUse N
104 
105 theorem preparation_price (r t : ℝ) : saving extraPreparation (prices r t)=200*t := by
106   simp [saving,extraPreparation,prices]
107   ring
108 
109 /-- Natural event totals of the same repeated compiler comparison, with paid setup. -/
110 def actualWorkload (N : ℕ) : Ledger Unit Bool where
111   setup := fun i => if i then 200 else 0
112   uses := fun _ => N
113   old := fun _ => fullCounts
114   revised := fun _ => streamCounts
115 
116 theorem actual_workload_delta (N : ℕ) : (actualWorkload N).delta=paid N := by
117   funext i
118   simp [Ledger.delta,net,actualWorkload,paid,repeated,extraPreparation,prices,perUse]
119 
120 theorem actual_workload_totals (N : ℕ) :
121     (actualWorkload N).oldTotal false=N*184 ∧
122     (actualWorkload N).newTotal false=N*153 ∧
123     (actualWorkload N).oldTotal true=N*45 ∧
124     (actualWorkload N).newTotal true=200+N*198 := by
125   rcases counter_binding with ⟨h0,h1,h2,h3⟩
126   simp [Ledger.oldTotal,Ledger.newTotal,actualWorkload,h0,h1,h2,h3]
127 
128 /-- Price variation between uses cannot be collapsed into one unpriced cancellation. -/
129 theorem time_varying_prices_boundary :
130     (1 : ℝ)+(-1)=0 ∧ (1 : ℝ)*1+2*(-1) < 0 := by norm_num
131 
132 theorem paid_value (N : ℕ) (r t : ℝ) :
133     saving (paid N) (prices r t) = (N : ℝ)*(31*r-153*t)-200*t := by
134   exact (saving_repeated extraPreparation perUse (prices r t) N).trans
135     (by rw [priced_scan,preparation_price])
136 
137 theorem paid_at_five (N : ℕ) : saving (paid N) (prices 5 1)=2*(N : ℝ)-200 := by
138   rw [paid_value]
139   ring
140 
141 theorem paid_strict_threshold (N : ℕ) : 0 < saving (paid N) (prices 5 1) ↔ 100 < N := by
142   rw [paid_at_five]
143   constructor
144   · intro h
145     have h' : (100 : ℝ) < N := by linarith
146     exact_mod_cast h'
147   · intro h
148     have h' : (100 : ℝ) < N := by exact_mod_cast h
149     linarith
150 
151 /-- The full declared convex family, not only its endpoints, has this attained minimum. -/
152 theorem paid_hull_minimum (N : ℕ) :
153     IsLeast ((saving (paid N)) '' convexHull ℝ (expensivePrices : Set (Bool → ℝ)))
154       (2*(N : ℝ)-200) := by
155   classical
156   constructor
157   · refine ⟨prices 5 1,subset_convexHull ℝ (expensivePrices : Set (Bool → ℝ)) ?_,paid_at_five N⟩
158     simp [expensivePrices]
159   · rintro x ⟨w,hw,rfl⟩
160     apply (hull_lower_bound_iff (paid N) (expensivePrices : Set (Bool → ℝ)) _).mpr ?_ w hw
161     intro z hz
162     simp only [Finset.mem_coe,expensivePrices,mem_insert,mem_singleton] at hz
163     rcases hz with rfl | rfl
164     · rw [paid_at_five]
165     · rw [paid_value]
166       have hn : (0 : ℝ) ≤ N := Nat.cast_nonneg N
167       nlinarith
168 
169 /-- The uniform strict threshold follows because the lower price is actually attained. -/
170 theorem robust_reuse_threshold (N : ℕ) :
171     (∀ w ∈ convexHull ℝ (expensivePrices : Set (Bool → ℝ)),0 < saving (paid N) w) ↔ 100 < N := by
172   classical
173   constructor
174   · intro h
175     apply (paid_strict_threshold N).mp
176     exact h (prices 5 1) (subset_convexHull ℝ _ (by simp [expensivePrices]))
177   · intro h w hw
178     have hp : 0 < 2*(N : ℝ)-200 := by
179       rw [← paid_at_five]
180       exact (paid_strict_threshold N).mpr h
181     exact lt_of_lt_of_le hp ((paid_hull_minimum N).2 ⟨w,hw,rfl⟩)
182 
183 theorem setup_and_boundary_values :
184     saving (paid 1) (prices 5 1)= -198 ∧ saving (paid 100) (prices 5 1)=0 ∧
185     saving (paid 101) (prices 5 1)=2 := by
186   constructor
187   · rw [paid_at_five]; norm_num
188   · constructor <;> rw [paid_at_five] <;> norm_num
189 
190 /-- At equal prices every repeat loses work, and preparation makes the result worse. -/
191 theorem equal_price_never_pays (N : ℕ) : saving (paid N) (prices 1 1) < 0 := by
192   rw [paid_value]
193   have hn : (0 : ℝ) ≤ N := Nat.cast_nonneg N
194   nlinarith
195 
196 /-- Changing the workload changes the sign even with the price fixed. -/
197 theorem workload_change_boundary :
198     saving (net (fun _ : Unit => 0) (fun _ : Bool => 1)
199       (fun (j : Bool) (_ : Unit) => if j then (-2 : ℝ) else 1)) (fun _ => 1)= -1 := by
200   norm_num [saving,net]
201 
202 /-- A negative conversion price can reverse a componentwise positive event difference. -/
203 theorem negative_price_boundary : saving (fun _ : Unit => (1 : ℝ)) (fun _ => -1) < 0 := by
204   norm_num [saving]
205 
206 /-- An unnormalized or signed combination is not a convex-price certificate. -/
207 theorem extrapolation_boundary :
208     (1 : ℝ) ≤ 1 ∧ (1 : ℝ) ≤ 2 ∧ 2*(1 : ℝ)+(-1)*2 < 1 := by
209   norm_num
210 
211 /-- Re-expressing one event as ten subunits without adjusting its price changes the value. -/
212 theorem unmatched_units_boundary :
213     saving (fun _ : Unit => (10 : ℝ)) (fun _ => 1) ≠
214       saving (fun _ : Unit => (1 : ℝ)) (fun _ => 1) := by
215   norm_num [saving]
216 
217 /-- The source book's supplied weighted-search ledger, not a new execution of that study. -/
218 def sourceWeighted : Fin 3 → ℝ := fun i => if i.val=0 then 1552 else if i.val=1 then 1552 else -1868
219 
220 theorem source_ledger_arithmetic :
221     saving sourceWeighted (fun _ => 1)=1236 ∧
222     saving sourceWeighted (fun i => if i.val=1 then 0 else 1)= -316 := by
223   constructor <;> norm_num [saving,sourceWeighted,Fin.sum_univ_succ]
224 
225 end
226 end Komorebi.MachineTheory.PriceExamples

Back to source controls