RotationRank.lean

1 import KomorebiLSM.RotationModel
2 import KomorebiLSM.BehaviorMinimality
3 
4 /-! Reachability and observability of the actual rational rotation process.
5 The dimension conclusion concerns the full behavior space, rather than only
6 the rank of a finite sampled table. -/
7 set_option autoImplicit false
8 namespace Komorebi.LSM.RotationModel
9 open FiniteInstruments
10 
11 /-- Three actual reachable columns span every state. -/
12 theorem reachable_column_decomposition (z : State) :
13     z = ((5/4:ℝ)*z 0-(1/4:ℝ)*z 1-(11/8:ℝ)*z 2) • initial +
14       (-(3/2:ℝ)*z 0+(3/2:ℝ)*z 1+2*z 2) • rotate initial +
15       ((5/4:ℝ)*z 0-(5/4:ℝ)*z 1-(5/8:ℝ)*z 2) • rotate (rotate initial) := by
16   ext i
17   fin_cases i <;> simp [initial] <;> ring
18 
19 /-- Every state lies in the span of actual chronological history columns. -/
20 theorem realization_reachable : realization.IsReachable := by
21   change realization.reachable = ⊤
22   apply top_unique
23   intro z _
24   have h0 : initial ∈ realization.reachable :=
25     Submodule.subset_span ⟨[], rfl⟩
26   have h1 : rotate initial ∈ realization.reachable :=
27     Submodule.subset_span ⟨[(false,false)], rfl⟩
28   have h2 : rotate (rotate initial) ∈ realization.reachable :=
29     Submodule.subset_span ⟨[(false,false),(false,false)], rfl⟩
30   rw [reachable_column_decomposition z]
31   exact Submodule.add_mem _
32     (Submodule.add_mem _ (Submodule.smul_mem _ _ h0) (Submodule.smul_mem _ _ h1))
33     (Submodule.smul_mem _ _ h2)
34 
35 /-- Empty, probe, and rotate-then-probe tests distinguish every state. -/
36 theorem realization_observable : realization.IsObservable := by
37   intro z w h
38   have h0 : z 0 = w 0 := by
39     simpa only [Behavior.Realization.observe_apply, realization, wordAction_nil,
40       LinearMap.id_apply, mass_apply] using congrFun h []
41   have hp : (z 0+z 1)/2 = (w 0+w 1)/2 := by
42     simpa only [Behavior.Realization.observe_apply, realization, wordAction_cons,
43       wordAction_nil, LinearMap.id_comp, operator_probe0, probe0_apply,
44       map_smul, initial_mass, smul_eq_mul, mul_one] using congrFun h [(true,false)]
45   have hr :
46       (z 0+((3/5:ℝ)*z 1-(4/5:ℝ)*z 2))/2 =
47       (w 0+((3/5:ℝ)*w 1-(4/5:ℝ)*w 2))/2 := by
48     simpa only [Behavior.Realization.observe_apply, realization, wordAction_cons,
49       wordAction_nil, LinearMap.id_comp, LinearMap.comp_apply, operator_rotate0,
50       operator_probe0, probe0_apply, map_smul, initial_mass, smul_eq_mul, mul_one,
51       rotate_apply, Matrix.cons_val_zero, Matrix.cons_val_one] using
52       congrFun h [(false,false),(true,false)]
53   have h1 : z 1 = w 1 := by linarith
54   have h2 : z 2 = w 2 := by linarith
55   funext i
56   fin_cases i
57   · exact h0
58   · exact h1
59   · exact h2
60 
61 /-- The complete predictive behavior has dimension three. -/
62 theorem behavior_dimension_three : Module.finrank ℝ (Behavior.space process) = 3 := by
63   rw [← realization.minimal_dimension realization_reachable realization_observable]
64   simp [State]
65 
66 /-- Every finite realization of this complete word law has dimension at least three. -/
67 theorem any_realization_dimension_ge_three {E : Type*} [AddCommGroup E]
68     [Module ℝ E] [FiniteDimensional ℝ E] (r : Behavior.Realization process E) :
69     3 ≤ Module.finrank ℝ E := by
70   rw [← behavior_dimension_three]
71   exact r.behavior_dimension_le
72 
73 end Komorebi.LSM.RotationModel

Back to source controls