Block2Examples.lean

1 import KomorebiLSM.TreeEnergy
2 import KomorebiLSM.PredictiveCompletion
3 import Mathlib.Tactic.NormNum
4 import Mathlib.Tactic.FinCases
5 
6 /-! Exact finite-tree selections and a proper predictive completion.
7 The three-coordinate example keeps the dynamically relevant first two
8 coordinates and genuinely omits the third. -/
9 set_option autoImplicit false
10 open scoped BigOperators
11 namespace Komorebi.LSM.Block2Examples
12 open Module PacketTree
13 
14 /-- Four leaves, with two internal children. -/
15 abbrev balancedTree : PacketTree := .branch 1 (fun _ => .branch 1 (fun _ => .leaf))
16 
17 /-- Select the left internal node and both right leaves. -/
18 def mixedCut : Node balancedTree → Bool
19   | .inl _ => false
20   | .inr ⟨i, .inl _⟩ => decide (i = 0)
21   | .inr ⟨i, .inr _⟩ => decide (i = 1)
22 
23 theorem mixed_depth_cut_complete : IsCompleteCut balancedTree mixedCut := by
24   rintro ⟨i, j, u⟩
25   cases u
26   fin_cases i <;> fin_cases j <;> rfl
27 
28 /-- On the all-one selection each path contains three selected nodes. -/
29 theorem selecting_ancestors_and_descendants_is_not_a_cut :
30     ¬ IsCompleteCut balancedTree (fun _ => true) := by
31   intro h
32   have hh := h ⟨0, 0, ()⟩
33   norm_num [pathCount, balancedTree] at hh
34 
35 /-- Deleting the only terminal node leaves an uncovered path. -/
36 theorem deleting_a_branch_is_not_a_cut :
37     ¬ IsCompleteCut (.branch 1 (fun _ => .leaf))
38       (fun v => match v with | .inl _ => false | .inr p => decide (p.1 = 0)) := by
39   intro h
40   have hh := h ⟨1, ()⟩
41   norm_num [pathCount] at hh
42 
43 /-- The mixed cut has three selected nodes, not four leaves. -/
44 theorem mixed_depth_selected_count :
45     selectedSum balancedTree mixedCut (fun _ => (1 : ℕ)) = 3 := by
46   norm_num [selectedSum, nodeSum, balancedTree, mixedCut, Fin.sum_univ_succ]
47 
48 /-- A conservative mass label reconstructs across mixed depths. -/
49 def treeMass : Node balancedTree → ℕ
50   | .inl _ => 10
51   | .inr ⟨i, .inl _⟩ => if i = 0 then 3 else 7
52   | .inr ⟨i, .inr ⟨j, _⟩⟩ => if i = 0 then (if j = 0 then 1 else 2)
53       else (if j = 0 then 3 else 4)
54 
55 theorem treeMass_conservative : Conservative balancedTree treeMass := by
56   constructor
57   · norm_num [treeMass, root, Fin.sum_univ_succ]
58   · intro i
59     fin_cases i <;> constructor
60     all_goals simp [Conservative, treeMass, Fin.sum_univ_succ]
61 
62 theorem mixed_depth_mass_reconstruction : selectedSum balancedTree mixedCut treeMass = 10 :=
63   selectedSum_eq_root balancedTree mixedCut treeMass mixed_depth_cut_complete treeMass_conservative
64 
65 /-- Additive conservation alone does not imply energy conservation. -/
66 theorem nonorthogonal_split_breaks_energy :
67     ((1/2 : ℝ) + 1/2 = 1) ∧ ‖(1/2 : ℝ)‖^2 + ‖(1/2 : ℝ)‖^2 ≠ ‖(1 : ℝ)‖^2 := by
68   norm_num
69 
70 abbrev Signal := ℚ × ℚ × ℚ
71 
72 def signalTransition : Signal →ₗ[ℚ] Signal where
73   toFun x := (x.1/2 + x.2.1, x.1/4 + x.2.1/3, (5/6)*x.2.2)
74   map_add' := by intro x y; ext <;> simp <;> ring
75   map_smul' := by intro a x; ext <;> simp <;> ring
76 
77 def firstRow : Dual ℚ Signal := LinearMap.fst ℚ ℚ (ℚ × ℚ)
78 def secondRow : Dual ℚ Signal := (LinearMap.fst ℚ ℚ ℚ).comp (LinearMap.snd ℚ ℚ (ℚ × ℚ))
79 def thirdRow : Dual ℚ Signal := (LinearMap.snd ℚ ℚ ℚ).comp (LinearMap.snd ℚ ℚ (ℚ × ℚ))
80 
81 def initialRows : Submodule ℚ (Dual ℚ Signal) := Submodule.span ℚ {firstRow}
82 def relevantRows : Submodule ℚ (Dual ℚ Signal) := LinearMap.ker (Dual.eval ℚ Signal (0,0,1))
83 noncomputable def completedRows : Submodule ℚ (Dual ℚ Signal) :=
84   predictiveCompletion (fun _ : Unit => signalTransition) initialRows
85 
86 theorem first_row_initial : firstRow ∈ initialRows := Submodule.subset_span (by simp)
87 
88 theorem initial_rows_relevant : initialRows ≤ relevantRows := by
89   apply Submodule.span_le.mpr
90   intro f hf
91   have he : f = firstRow := by simpa using hf
92   subst f
93   rfl
94 
95 theorem relevant_rows_invariant :
96     CommonInvariant (fun _ : Unit => signalTransition.dualMap) relevantRows := by
97   intro i w hw
98   obtain ⟨f, hf, rfl⟩ := Submodule.mem_map.mp hw
99   change f (signalTransition (0,0,1)) = 0
100   have hv : f (0,0,1) = 0 := hf
101   have he : signalTransition (0,0,1) = (5/6 : ℚ) • (0,0,1) := by
102     norm_num [signalTransition]
103   rw [he, map_smul, hv, smul_zero]
104 
105 theorem completion_omits_irrelevant_direction : completedRows ≤ relevantRows :=
106   invariantCompletion_minimal _ _ _ initial_rows_relevant relevant_rows_invariant
107 
108 theorem first_row_completed : firstRow ∈ completedRows :=
109   initial_le_invariantCompletion _ _ first_row_initial
110 
111 theorem pullback_creates_second_row :
112     signalTransition.dualMap firstRow - (1/2 : ℚ) • firstRow = secondRow := by
113   apply LinearMap.ext
114   intro x
115   simp [signalTransition, firstRow, secondRow]
116   ring
117 
118 theorem second_row_completed : secondRow ∈ completedRows := by
119   have hinv : CommonInvariant (fun _ : Unit => signalTransition.dualMap) completedRows :=
120     invariantCompletion_invariant _ _
121   have hp : signalTransition.dualMap firstRow ∈ completedRows :=
122     hinv () (Submodule.mem_map.mpr ⟨firstRow, first_row_completed, rfl⟩)
123   rw [← pullback_creates_second_row]
124   exact completedRows.sub_mem hp (completedRows.smul_mem _ first_row_completed)
125 
126 theorem relevant_row_decomposition (f : Dual ℚ Signal) (hf : f ∈ relevantRows) :
127     f = f (1,0,0) • firstRow + f (0,1,0) • secondRow := by
128   have hz : f (0,0,1) = 0 := hf
129   apply LinearMap.ext
130   intro x
131   have hx : x = x.1 • (1,0,0) + x.2.1 • (0,1,0) + x.2.2 • (0,0,1) := by
132     ext <;> simp
133   have hfx := congrArg f hx
134   simp only [map_add, map_smul, hz, smul_eq_mul, mul_zero, add_zero] at hfx
135   change f x = f (1,0,0) * x.1 + f (0,1,0) * x.2.1
136   rw [hfx]
137   ring
138 
139 theorem completion_is_exactly_two_coordinate_rows : completedRows = relevantRows := by
140   apply le_antisymm completion_omits_irrelevant_direction
141   intro f hf
142   rw [relevant_row_decomposition f hf]
143   exact completedRows.add_mem (completedRows.smul_mem _ first_row_completed)
144     (completedRows.smul_mem _ second_row_completed)
145 
146 theorem third_row_not_completed : thirdRow ∉ completedRows := by
147   intro h
148   have hr := completion_omits_irrelevant_direction h
149   change thirdRow (0,0,1) = 0 at hr
150   norm_num [thirdRow] at hr
151 
152 theorem completion_is_proper : completedRows ≠ ⊤ := by
153   intro h
154   exact third_row_not_completed (h ▸ Submodule.mem_top)
155 
156 theorem first_coordinate_not_closed :
157     ¬ ∃ F : ℚ → ℚ, ∀ x : Signal, F (firstRow x) = firstRow (signalTransition x) := by
158   rintro ⟨F, h⟩
159   have h0 := h (0,0,0)
160   have h1 := h (0,1,0)
161   norm_num [firstRow, signalTransition] at h0 h1
162   exact (by norm_num : (0 : ℚ) ≠ 1) (h0.symm.trans h1)
163 
164 /-- With no declared operations, no observable enrichment is needed. -/
165 theorem empty_family_completion (V : Type*) [AddCommGroup V] [Module ℚ V]
166     (W : Submodule ℚ V) : invariantCompletion (fun i : Empty => i.elim) W = W := by
167   apply le_antisymm
168   · exact invariantCompletion_minimal _ _ W le_rfl (fun i => i.elim)
169   · exact initial_le_invariantCompletion _ _
170 
171 end Komorebi.LSM.Block2Examples

Back to source controls