Block6Examples.lean

1 import KomorebiLSM.CanonicalCone
2 import KomorebiLSM.FiniteTestRows
3 import KomorebiLSM.FacetRobustness
4 import KomorebiLSM.CertifiedCorrection
5 import KomorebiLSM.Block5Examples
6 
7 /-! Exact applications and rejection boundaries for canonical and finite domains.
8 Finite sampled checks are kept separate from the all-word invariant arguments. -/
9 set_option autoImplicit false
10 namespace Komorebi.LSM.Block6Examples
11 open scoped BigOperators
12 open FiniteInstruments FiniteBayes Behavior TestDomains PositiveLift RobustDomains
13 
14 /-- P29 applies to the actual rank-two future-behavior space of the preceding example. -/
15 theorem canonical_example_compact : IsCompact (probabilityBase Block5Examples.process) :=
16   probabilityBase_compact Block5Examples.process_causal
17 
18 theorem canonical_example_spans :
19     Submodule.span ℝ (probabilityCone Block5Examples.process) = ⊤ :=
20   probabilityCone_spans Block5Examples.process_causal
21 
22 theorem canonical_example_initial : history Block5Examples.process [] ∈
23     probabilityBase Block5Examples.process := initial_mem_probabilityBase Block5Examples.process_causal
24 
25 theorem canonical_example_bounds (v : space Block5Examples.process)
26     (hv : v ∈ probabilityBase Block5Examples.process) :
27     evaluate Block5Examples.process Block5Examples.selected v 0 = 1 ∧
28     ∀ i : Fin 2, evaluate Block5Examples.process Block5Examples.selected v i ∈ Set.Icc (0 : ℝ) 1 :=
29   probabilityBase_core_bounds Block5Examples.process_causal Block5Examples.selected 0
30     Block5Examples.first_test_empty hv
31 
32 /-- A mass-normalized family can pass every one-step check and fail at length two. -/
33 noncomputable def delayedMatrix (o : Bool) : Matrix (Fin 2) (Fin 2) ℝ :=
34   if o then !![1/2,-1;0,0] else !![1/2,1;0,2]
35 
36 noncomputable def delayedBranch (s : Unit × Bool) : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) :=
37   (delayedMatrix s.2).mulVecLin
38 
39 noncomputable def delayedState : Fin 2 → ℝ := ![1,1/4]
40 
41 def firstMass : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
42 
43 theorem delayed_mass_conserved (a : Unit) (x : Fin 2 → ℝ) :
44     ∑ o, firstMass (delayedBranch (a,o) x) = firstMass x := by
45   simp [firstMass,delayedBranch,delayedMatrix,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
46   ring
47 
48 theorem delayed_first_probabilities :
49     firstMass (delayedBranch ((),false) delayedState) = 3/4 ∧
50     firstMass (delayedBranch ((),true) delayedState) = 1/4 := by
51   norm_num [firstMass,delayedBranch,delayedMatrix,delayedState,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
52 
53 theorem delayed_passes_one : delayedState ∈ testLevel delayedBranch firstMass 1 := by
54   intro w hw
55   cases w with
56   | nil => norm_num [observe_apply,wordAction,firstMass,delayedState]
57   | cons s w =>
58     have hw0 : w = [] := List.length_eq_zero_iff.mp (by simpa using hw)
59     subst w
60     rcases s with ⟨a,o⟩
61     cases a
62     cases o <;> norm_num [observe_apply,wordAction,firstMass,delayedBranch,delayedMatrix,
63       delayedState,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
64 
65 theorem delayed_negative_two :
66     firstMass (wordAction delayedBranch [((),false),((),true)] delayedState) = -1/8 := by
67   norm_num [wordAction,firstMass,delayedBranch,delayedMatrix,delayedState,Matrix.mulVec,dotProduct,
68     Fin.sum_univ_succ]
69 
70 theorem delayed_not_all_tests : delayedState ∉ allTests delayedBranch firstMass := by
71   intro h
72   have he := h [((),false),((),true)]
73   change 0 ≤ firstMass (wordAction delayedBranch [((),false),((),true)] delayedState) at he
74   rw [delayed_negative_two] at he
75   norm_num at he
76 
77 theorem delayed_level_one_not_stable :
78     testLevel delayedBranch firstMass 2 ≠ testLevel delayedBranch firstMass 1 := by
79   intro he
80   have hh := testLevel_stopping delayedBranch firstMass 1 he
81   exact delayed_not_all_tests (hh ▸ delayed_passes_one)
82 
83 /-- Missing observability leaves nonzero mass-zero states in the all-test cone. -/
84 def hiddenIdentity (_ : Unit × Unit) : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) := LinearMap.id
85 
86 theorem identity_words (w : List (Unit × Unit)) (x : Fin 2 → ℝ) :
87     wordAction hiddenIdentity w x = x := by
88   induction w generalizing x with
89   | nil => rfl
90   | cons s w ih => exact ih x
91 
92 theorem unobserved_ray_in_cone :
93     ![(0 : ℝ),1] ∈ allTests hiddenIdentity firstMass ∧
94     -(![(0 : ℝ),1]) ∈ allTests hiddenIdentity firstMass := by
95   constructor <;> intro w <;> simp [observe_apply,identity_words,firstMass]
96 
97 theorem unobserved_ray_nonzero : ![(0 : ℝ),1] ≠ 0 := by
98   intro h
99   have hh := congrFun h 1
100   norm_num at hh
101 
102 theorem unobserved_cone_mass_zero : firstMass ![(0 : ℝ),1] = 0 := rfl
103 
104 /-- A redundant synthesis has a closed, generating and strict-mass cone. -/
105 theorem redundant_summary_domain :
106     IsClosed (hull Block4Examples.summary) ∧
107     Submodule.span ℝ (hull Block4Examples.summary) = ⊤ ∧
108     PositivePackets.StrictMass (hull Block4Examples.summary) Block4Examples.summaryMass :=
109   ⟨hull_closed _ _ Block4Examples.summary_preserves_mass,
110    hull_spans _ Block4Examples.summary_surjective,
111    hull_strict_mass _ _ Block4Examples.summary_preserves_mass⟩
112 
113 theorem redundant_summary_base_compact :
114     IsCompact (normalizedHull Block4Examples.summary Block4Examples.summaryMass) :=
115   normalizedHull_compact _ _ Block4Examples.summary_preserves_mass
116 
117 theorem redundant_summary_lift (s : Unit × Bool) :
118     ∀ x ∈ hull Block4Examples.summary, Block4Examples.reducedBranch s x ∈ hull Block4Examples.summary :=
119   (positive_lift_iff _ _).mpr ⟨Block4Examples.hiddenMatrix s.2,
120     Block4Examples.tinyInstrument.nonneg s.1 s.2,Block4Examples.reduced_intertwining s⟩
121 
122 theorem redundant_summary_generators_repeat :
123     generator Block4Examples.summary (0 : Fin 3) = generator Block4Examples.summary 1 :=
124   Block4Examples.same_summary
125 
126 noncomputable def swapLift : Matrix (Fin 2) (Fin 2) ℝ := !![0,1;1,0]
127 
128 theorem swap_lift_nonnegative : ∀ i j, 0 ≤ swapLift i j := by
129   intro i j
130   fin_cases i <;> fin_cases j <;> norm_num [swapLift]
131 
132 theorem swap_preserves_total :
133     (FiniteInstruments.mass : (Fin 2 → ℝ) →ₗ[ℝ] ℝ).comp swapLift.mulVecLin = FiniteInstruments.mass := by
134   apply LinearMap.ext
135   intro x
136   simp [FiniteInstruments.mass_apply,swapLift,dotProduct,Fin.sum_univ_succ,add_comm]
137 
138 theorem distinct_positive_lifts :
139     (1 : Matrix (Fin 2) (Fin 2) ℝ) ≠ swapLift ∧
140     (FiniteInstruments.mass : (Fin 2 → ℝ) →ₗ[ℝ] ℝ).comp (1 : Matrix (Fin 2) (Fin 2) ℝ).mulVecLin = FiniteInstruments.mass ∧
141     (FiniteInstruments.mass : (Fin 2 → ℝ) →ₗ[ℝ] ℝ).comp swapLift.mulVecLin = FiniteInstruments.mass := by
142   refine ⟨?_,?_,swap_preserves_total⟩
143   · intro h
144     have he := congrArg (fun M : Matrix (Fin 2) (Fin 2) ℝ => M 0 0) h
145     norm_num [swapLift] at he
146   · apply LinearMap.ext
147     intro x
148     simp
149 
150 /-- A complete family of scalar Bernoulli branches. -/
151 noncomputable def coinFamily (θ : ℝ) (s : Unit × Bool) : ℝ →ₗ[ℝ] ℝ :=
152   (if s.2 then θ else 1-θ) • LinearMap.id
153 
154 theorem coin_mass (θ : ℝ) (a : Unit) (x : ℝ) :
155     ∑ o, (LinearMap.id : ℝ →ₗ[ℝ] ℝ) (coinFamily θ (a,o) x) = x := by
156   simp [coinFamily]
157   ring
158 
159 theorem coin_valid (θ : ℝ) (h₀ : 0 ≤ θ) (h₁ : θ ≤ 1) :
160     ValidFamily (Set.Ici (0 : ℝ)) (LinearMap.id : ℝ →ₗ[ℝ] ℝ) (coinFamily θ) := by
161   constructor
162   · rintro ⟨a,o⟩ x hx
163     change 0 ≤ x at hx
164     cases o
165     · exact mul_nonneg (sub_nonneg.mpr h₁) hx
166     · exact mul_nonneg h₀ hx
167   · exact coin_mass θ
168 
169 noncomputable def coinVertices (b : Bool) : Unit × Bool → ℝ →ₗ[ℝ] ℝ :=
170   coinFamily (if b then 3/4 else 1/4)
171 
172 theorem coin_vertices_valid : ∀ b, ValidFamily (Set.Ici (0 : ℝ)) LinearMap.id (coinVertices b) := by
173   intro b
174   cases b <;> apply coin_valid <;> norm_num
175 
176 theorem every_convex_coin_family_valid :
177     ∀ B ∈ convexHull ℝ (Set.range coinVertices), ValidFamily (Set.Ici (0 : ℝ)) LinearMap.id B :=
178   robust_convex_hull _ (convex_Ici _) _ coinVertices coin_vertices_valid
179 
180 noncomputable def switchingCoins (h : List (Unit × Bool)) : Unit × Bool → ℝ →ₗ[ℝ] ℝ :=
181   coinVertices (h.length % 2 == 0)
182 
183 theorem switched_tree_normalized (n : ℕ) :
184     adaptiveTreeMass switchingCoins LinearMap.id (fun _ => ()) n [] 1 = 1 :=
185   adaptiveTreeMass_eq (Set.Ici (0 : ℝ)) LinearMap.id switchingCoins
186     (fun _ => coin_vertices_valid _) (fun _ => ()) n [] 1
187 
188 theorem switched_every_word_valid (w : List (Unit × Bool)) :
189     0 ≤ adaptiveWord switchingCoins [] w 1 ∧ adaptiveWord switchingCoins [] w 1 ≤ 1 :=
190   ⟨adaptiveWord_nonnegative (Set.Ici (0 : ℝ)) LinearMap.id (fun _ hx => hx)
191       switchingCoins (fun _ => coin_vertices_valid _) [] w (by norm_num),
192    adaptiveWord_mass_le (Set.Ici (0 : ℝ)) LinearMap.id (fun _ hx => hx)
193       switchingCoins (fun _ => coin_vertices_valid _) [] w (by norm_num)⟩
194 
195 /-- Choosing the larger probability independently from each family breaks normalization. -/
196 noncomputable def crossedBranches (s : Unit × Bool) : ℝ →ₗ[ℝ] ℝ :=
197   if s.2 then coinVertices true s else coinVertices false s
198 
199 theorem independent_branch_mixing_breaks_mass :
200     (∑ o, crossedBranches ((),o) 1) = (3/2 : ℝ) := by
201   norm_num [crossedBranches,coinVertices,coinFamily]
202 
203 theorem bad_coin_has_negative_branch : coinFamily (3/2) ((),false) 1 = (-1/2 : ℝ) := by
204   norm_num [coinFamily]
205 
206 theorem feasible_member_is_not_whole_set_valid :
207     ValidFamily (Set.Ici (0 : ℝ)) LinearMap.id (coinFamily (1/2)) ∧
208     ¬ ValidFamily (Set.Ici (0 : ℝ)) LinearMap.id (coinFamily (3/2)) := by
209   refine ⟨coin_valid _ (by norm_num) (by norm_num), ?_⟩
210   intro h
211   have hp := h.1 ((),false) 1 (by norm_num)
212   change 0 ≤ coinFamily (3/2) ((),false) 1 at hp
213   rw [bad_coin_has_negative_branch] at hp
214   norm_num at hp
215 
216 theorem double_radius_can_be_tight :
217     ‖(-1 : ℝ)-0‖ = 1 ∧ ‖(1 : ℝ)-0‖ = 1 ∧ ‖(1 : ℝ)-(-1)‖ = 2 := by norm_num
218 
219 noncomputable def tableBranch (s : Unit × Bool) : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) :=
220   (reconstructed Block5Examples.process Block5Examples.selected Block5Examples.selected s).mulVecLin
221 
222 theorem table_false_coordinates (x : Fin 2 → ℝ) :
223     tableBranch ((),false) x = ![x 0-x 1,(x 0-x 1)/2] := by
224   change (reconstructed _ _ _ _).mulVec x = _
225   rw [Block5Examples.learned_false]
226   ext i
227   fin_cases i <;> norm_num [Matrix.mulVec,dotProduct,Fin.sum_univ_succ] <;> ring
228 
229 theorem table_true_coordinates (x : Fin 2 → ℝ) :
230     tableBranch ((),true) x = ![x 1,3/4*x 1] := by
231   change (reconstructed _ _ _ _).mulVec x = _
232   rw [Block5Examples.learned_true]
233   ext i
234   fin_cases i <;> norm_num [Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
235 
236 noncomputable def outerDomain : Set (Fin 2 → ℝ) := {x | 0 ≤ x 1 ∧ x 1 ≤ x 0}
237 
238 theorem table_preserves_outer (s : Unit × Bool) (x : Fin 2 → ℝ) (hx : x ∈ outerDomain) :
239     tableBranch s x ∈ outerDomain := by
240   rcases s with ⟨a,o⟩
241   cases a
242   change 0 ≤ x 1 ∧ x 1 ≤ x 0 at hx
243   cases o
244   · rw [table_false_coordinates]
245     change 0 ≤ (x 0-x 1)/2 ∧ (x 0-x 1)/2 ≤ x 0-x 1
246     constructor <;> linarith [hx.2]
247   · rw [table_true_coordinates]
248     change 0 ≤ 3/4*x 1 ∧ 3/4*x 1 ≤ x 1
249     constructor <;> linarith [hx.1]
250 
251 theorem table_mass_conserved (a : Unit) (x : Fin 2 → ℝ) :
252     ∑ o, firstMass (tableBranch (a,o) x) = firstMass x := by
253   cases a
254   simp only [Fintype.sum_bool,table_false_coordinates,table_true_coordinates,firstMass,LinearMap.proj_apply]
255   simp
256 
257 theorem table_allTests_outer : allTests tableBranch firstMass = outerDomain := by
258   apply Set.Subset.antisymm
259   · intro x hx
260     have h₁ := hx [((),true)]
261     have h₀ := hx [((),false)]
262     simp only [observe_apply,wordAction,LinearMap.comp_apply,LinearMap.id_apply,
263       table_false_coordinates,table_true_coordinates,firstMass,LinearMap.proj_apply] at h₀ h₁
264     exact ⟨h₁,by change 0 ≤ x 0-x 1 at h₀; linarith⟩
265   · apply allTests_greatest tableBranch firstMass outerDomain
266     · intro x hx; exact hx.1.trans hx.2
267     · exact table_preserves_outer
268 
269 theorem table_level_one_outer : testLevel tableBranch firstMass 1 = outerDomain := by
270   apply Set.Subset.antisymm
271   · intro x hx
272     have h₁ := hx [((),true)] (by simp)
273     have h₀ := hx [((),false)] (by simp)
274     simp only [observe_apply,wordAction,LinearMap.comp_apply,LinearMap.id_apply,
275       table_false_coordinates,table_true_coordinates,firstMass,LinearMap.proj_apply] at h₀ h₁
276     exact ⟨h₁,by change 0 ≤ x 0-x 1 at h₀; linarith⟩
277   · intro x hx w _
278     exact (table_allTests_outer.symm ▸ hx) w
279 
280 theorem table_finite_stopping : testLevel tableBranch firstMass 2 = testLevel tableBranch firstMass 1 := by
281   apply Set.Subset.antisymm (testLevel_antitone tableBranch firstMass (by decide))
282   intro x hx w _
283   have ho : x ∈ outerDomain := table_level_one_outer ▸ hx
284   exact (table_allTests_outer.symm ▸ ho) w
285 
286 noncomputable def intervalSynthesis : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) :=
287   (!![(1 : ℝ),1;1/2,3/4]).mulVecLin
288 
289 noncomputable def intervalLift (s : Unit × Bool) : Matrix (Fin 2) (Fin 2) ℝ :=
290   if s.2 then !![0,0;1/2,3/4] else !![1/2,1/4;0,0]
291 
292 theorem interval_normalized : firstMass.comp intervalSynthesis = FiniteInstruments.mass := by
293   apply LinearMap.ext
294   intro a
295   simp [firstMass,intervalSynthesis,FiniteInstruments.mass_apply,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
296 
297 theorem interval_surjective : Function.Surjective intervalSynthesis := by
298   intro x
299   refine ⟨![3*x 0-4*x 1,4*x 1-2*x 0],?_⟩
300   ext i
301   fin_cases i <;> norm_num [intervalSynthesis,Matrix.mulVec,dotProduct,Fin.sum_univ_succ] <;> ring
302 
303 theorem interval_lift_nonnegative : ∀ s i j, 0 ≤ intervalLift s i j := by
304   rintro ⟨a,o⟩ i j
305   cases o <;> fin_cases i <;> fin_cases j <;> norm_num [intervalLift]
306 
307 theorem interval_intertwines (s : Unit × Bool) :
308     (tableBranch s).comp intervalSynthesis = intervalSynthesis.comp (intervalLift s).mulVecLin := by
309   apply LinearMap.ext
310   intro x
311   rcases s with ⟨a,o⟩
312   cases a
313   cases o
314   · rw [LinearMap.comp_apply,table_false_coordinates,LinearMap.comp_apply]
315     ext i
316     fin_cases i <;> norm_num [intervalSynthesis,intervalLift,Matrix.mulVec,dotProduct,Fin.sum_univ_succ] <;> ring
317   · rw [LinearMap.comp_apply,table_true_coordinates,LinearMap.comp_apply]
318     ext i
319     fin_cases i <;> norm_num [intervalSynthesis,intervalLift,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
320 
321 theorem interval_initial : intervalSynthesis ![(1/2 : ℝ),1/2] = ![(1 : ℝ),5/8] := by
322   ext i
323   fin_cases i <;> norm_num [intervalSynthesis,Matrix.mulVec,dotProduct,Fin.sum_univ_succ]
324 
325 theorem interval_prior : IsPrior ![(1/2 : ℝ),1/2] := by
326   constructor
327   · intro i; fin_cases i <;> norm_num
328   · norm_num [Fin.sum_univ_succ]
329 
330 /-- The witness gives every finite word, not an extrapolation of a word table. -/
331 theorem interval_certificate_all_words (w : List (Unit × Bool)) :
332     0 ≤ firstMass (wordAction tableBranch w ![(1 : ℝ),5/8]) ∧
333     firstMass (wordAction tableBranch w ![(1 : ℝ),5/8]) ≤ 1 := by
334   rw [← interval_initial]
335   exact (finite_positive_lift_certificate tableBranch intervalSynthesis firstMass
336     interval_normalized table_mass_conserved intervalLift interval_intertwines
337     interval_lift_nonnegative _ interval_prior).2.2 w
338 
339 /-- The sufficient interval certificate need not equal the canonical all-test domain. -/
340 theorem certified_subcone_can_be_strict :
341     ![(1 : ℝ),0] ∈ allTests tableBranch firstMass ∧ ![(1 : ℝ),0] ∉ hull intervalSynthesis := by
342   constructor
343   · rw [table_allTests_outer]; constructor <;> norm_num
344   · rintro ⟨a,ha,he⟩
345     have h₀ := congrFun he 0
346     have h₁ := congrFun he 1
347     norm_num [intervalSynthesis,Matrix.mulVec,dotProduct,Fin.sum_univ_succ] at h₀ h₁
348     linarith [ha 0,ha 1]
349 
350 end Komorebi.LSM.Block6Examples

Back to source controls