CommonQuotient.lean

1 import MachineTheory.Transfer
2 import Mathlib.LinearAlgebra.Quotient.Basic
3 import Mathlib.LinearAlgebra.FiniteDimensional.Basic
4 
5 /-!
6 # A common observable quotient
7 
8 Core 2.4. The reference is one distinguished complete candidate. Agreement is
9 required as an operator identity on every initial vector and every finite word.
10 The discrepancy submodule is constructed from reference-propagated differences.
11 No finite testing horizon or learned identification is substituted for that premise.
12 -/
13 namespace Komorebi.MachineTheory.CommonQuotient
14 
15 noncomputable section
16 
17 universe uK uV uY uA uT uZ
18 variable {K : Type uK} {V : Type uV} {Y : Type uY} {A : Type uA} {Θ : Type uT}
19 variable [Field K] [AddCommGroup V] [Module K V] [AddCommGroup Y] [Module K Y]
20 
21 /-- Linear execution in the source's left-to-right convention. -/
22 def wordMap (F : A → V →ₗ[K] V) : List A → V →ₗ[K] V
23   | [] => LinearMap.id
24   | a :: w => (wordMap F w).comp (F a)
25 
26 @[simp] theorem wordMap_nil (F : A → V →ₗ[K] V) : wordMap F [] = LinearMap.id := rfl
27 
28 @[simp] theorem wordMap_cons (F : A → V →ₗ[K] V) (a : A) (w : List A) :
29     wordMap F (a :: w) = (wordMap F w).comp (F a) := rfl
30 
31 /-- The linear word is the existing deterministic execution, not a new order convention. -/
32 theorem wordMap_eq_run (F : A → V →ₗ[K] V) (w : List A) (v : V) :
33     wordMap F w v = Komorebi.MachineTheory.run (fun a => F a) w v := by
34   induction w generalizing v with
35   | nil => rfl
36   | cons a w ih => exact ih (F a v)
37 
38 /-- Appending a word executes it after the first word. -/
39 theorem wordMap_append (F : A → V →ₗ[K] V) (w t : List A) :
40     wordMap F (w ++ t) = (wordMap F t).comp (wordMap F w) := by
41   induction w with
42   | nil => rfl
43   | cons a w ih =>
44     ext v
45     simpa only [List.cons_append, wordMap_cons, LinearMap.comp_apply] using
46       LinearMap.congr_fun ih (F a v)
47 
48 @[simp] theorem wordMap_snoc (F : A → V →ₗ[K] V) (w : List A) (a : A) (v : V) :
49     wordMap F (w ++ [a]) v = F a (wordMap F w v) := by
50   rw [wordMap_append]
51   rfl
52 
53 /-- Every propagated one-step candidate discrepancy, over all initial vectors. -/
54 def generators (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) : Set V :=
55   {x | ∃ (w : List A) (a : A) (θ : Θ) (v : V),
56     wordMap (T θ₀) w ((T θ a - T θ₀ a) v) = x}
57 
58 /-- The actual propagated discrepancy space in the manuscript. -/
59 def discrepancy (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) : Submodule K V :=
60   Submodule.span K (generators T θ₀)
61 
62 /-- The premise compares fixed candidates on all words and all initial vectors. -/
63 def ObservableAgreement (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (Q : V →ₗ[K] Y) : Prop :=
64   ∀ θ w, Q.comp (wordMap (T θ) w) = Q.comp (wordMap (T θ₀) w)
65 
66 /-- Every named generator lies in the constructed submodule. -/
67 theorem generator_mem (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
68     (w : List A) (a : A) (θ : Θ) (v : V) :
69     wordMap (T θ₀) w ((T θ a - T θ₀ a) v) ∈ discrepancy T θ₀ :=
70   Submodule.subset_span ⟨w, a, θ, v, rfl⟩
71 
72 /-- One-step difference ranges are contained, without any observability assumption. -/
73 theorem difference_mem (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
74     (a : A) (θ : Θ) (v : V) : (T θ a - T θ₀ a) v ∈ discrepancy T θ₀ :=
75   generator_mem T θ₀ [] a θ v
76 
77 /-- Propagated discrepancies are invariant under each reference action. -/
78 theorem reference_invariant (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
79     (a : A) {x : V} (hx : x ∈ discrepancy T θ₀) :
80     T θ₀ a x ∈ discrepancy T θ₀ := by
81   refine Submodule.span_induction ?_ ?_ ?_ ?_ hx
82   · rintro x ⟨w, b, θ, v, rfl⟩
83     simpa only [wordMap_snoc] using generator_mem T θ₀ (w ++ [a]) b θ v
84   · rw [map_zero]
85     exact (discrepancy T θ₀).zero_mem
86   · intro x y _ _ hx hy
87     simpa only [map_add] using (discrepancy T θ₀).add_mem hx hy
88   · intro c x _ hx
89     simpa only [map_smul] using (discrepancy T θ₀).smul_mem c hx
90 
91 /-- Every candidate preserves the same discrepancy space. -/
92 theorem candidate_invariant (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
93     (θ : Θ) (a : A) {x : V} (hx : x ∈ discrepancy T θ₀) :
94     T θ a x ∈ discrepancy T θ₀ := by
95   have hd := difference_mem T θ₀ a θ x
96   have ha := reference_invariant T θ₀ a hx
97   have hs := (discrepancy T θ₀).add_mem hd ha
98   simpa only [LinearMap.sub_apply, sub_add_cancel] using hs
99 
100 /-- Any invariant submodule containing all differences contains every generator. -/
101 theorem discrepancy_le (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (N : Submodule K V)
102     (hd : ∀ θ a v, (T θ a - T θ₀ a) v ∈ N)
103     (hA : ∀ a x, x ∈ N → T θ₀ a x ∈ N) : discrepancy T θ₀ ≤ N := by
104   apply Submodule.span_le.mpr
105   rintro x ⟨w, a, θ, v, rfl⟩
106   have hw : ∀ (t : List A) (y : V), y ∈ N → wordMap (T θ₀) t y ∈ N := by
107     intro t
108     induction t with
109     | nil => intro y hy; exact hy
110     | cons b t ih => intro y hy; exact ih _ (hA b y hy)
111   exact hw w _ (hd θ a v)
112 
113 /-- Fixed-model agreement annihilates even reference-propagated discrepancies. -/
114 theorem discrepancy_invisible_of_agreement (T : Θ → A → V →ₗ[K] V)
115     (θ₀ : Θ) (Q : V →ₗ[K] Y) (h : ObservableAgreement T θ₀ Q) :
116     discrepancy T θ₀ ≤ LinearMap.ker Q := by
117   apply Submodule.span_le.mpr
118   rintro x ⟨w, a, θ, v, rfl⟩
119   change Q (wordMap (T θ₀) w ((T θ a - T θ₀ a) v)) = 0
120   have hw := LinearMap.congr_fun (h θ w) (T θ a v)
121   change Q (wordMap (T θ) w (T θ a v)) = Q (wordMap (T θ₀) w (T θ a v)) at hw
122   have haw := LinearMap.congr_fun (h θ (a :: w)) v
123   change Q (wordMap (T θ) w (T θ a v)) = Q (wordMap (T θ₀) w (T θ₀ a v)) at haw
124   simp only [LinearMap.sub_apply, map_sub]
125   rw [← hw, haw, sub_self]
126 
127 /-- The canonical update is an actual induced linear map on the quotient. -/
128 def quotientUpdate (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (a : A) :
129     (V ⧸ discrepancy T θ₀) →ₗ[K] (V ⧸ discrepancy T θ₀) :=
130   (discrepancy T θ₀).mapQ (discrepancy T θ₀) (T θ₀ a)
131     (fun _ hx => reference_invariant T θ₀ a hx)
132 
133 /-- The canonical update agrees with the reference on every quotient representative. -/
134 @[simp] theorem quotientUpdate_mk (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (a : A) (v : V) :
135     quotientUpdate T θ₀ a ((discrepancy T θ₀).mkQ v) =
136       (discrepancy T θ₀).mkQ (T θ₀ a v) :=
137   Submodule.mapQ_apply _ _ _ _
138 
139 /-- All candidate actions induce that same update, not merely matching readouts. -/
140 theorem quotientUpdate_candidate (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
141     (θ : Θ) (a : A) (v : V) :
142     (discrepancy T θ₀).mkQ (T θ a v) =
143       quotientUpdate T θ₀ a ((discrepancy T θ₀).mkQ v) := by
144   rw [quotientUpdate_mk]
145   apply sub_eq_zero.mp
146   rw [← map_sub]
147   change T θ a v - T θ₀ a v ∈ LinearMap.ker (discrepancy T θ₀).mkQ
148   rw [Submodule.ker_mkQ]
149   exact difference_mem T θ₀ a θ v
150 
151 /-- An invisible discrepancy space admits the protected quotient readout. -/
152 def quotientReadout (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (Q : V →ₗ[K] Y)
153     (h : discrepancy T θ₀ ≤ LinearMap.ker Q) : (V ⧸ discrepancy T θ₀) →ₗ[K] Y :=
154   (discrepancy T θ₀).liftQ Q h
155 
156 @[simp] theorem quotientReadout_mk (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
157     (Q : V →ₗ[K] Y) (h : discrepancy T θ₀ ≤ LinearMap.ker Q) (v : V) :
158     quotientReadout T θ₀ Q h ((discrepancy T θ₀).mkQ v) = Q v := rfl
159 
160 /-- A sequence of action/candidate pairs permits the candidate to change at every step. -/
161 def switchedMap (T : Θ → A → V →ₗ[K] V) : List (Θ × A) → V →ₗ[K] V :=
162   wordMap (fun p => T p.1 p.2)
163 
164 /-- The quotient evolution is independent of the successive candidate choices. -/
165 theorem switched_quotient (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
166     (w : List (Θ × A)) (v : V) :
167     (discrepancy T θ₀).mkQ (switchedMap T w v) =
168       wordMap (quotientUpdate T θ₀) (w.map Prod.snd) ((discrepancy T θ₀).mkQ v) := by
169   induction w generalizing v with
170   | nil => rfl
171   | cons p w ih =>
172     change (discrepancy T θ₀).mkQ (switchedMap T w (T p.1 p.2 v)) =
173       wordMap (quotientUpdate T θ₀) (w.map Prod.snd)
174         (quotientUpdate T θ₀ p.2 ((discrepancy T θ₀).mkQ v))
175     rw [ih, quotientUpdate_candidate]
176 
177 /-- Each fixed-candidate word also intertwines with the canonical quotient. -/
178 theorem word_quotient (T : Θ → A → V →ₗ[K] V) (θ₀ θ : Θ)
179     (w : List A) (v : V) :
180     (discrepancy T θ₀).mkQ (wordMap (T θ) w v) =
181       wordMap (quotientUpdate T θ₀) w ((discrepancy T θ₀).mkQ v) := by
182   induction w generalizing v with
183   | nil => rfl
184   | cons a w ih =>
185     change (discrepancy T θ₀).mkQ (wordMap (T θ) w (T θ a v)) =
186       wordMap (quotientUpdate T θ₀) w (quotientUpdate T θ₀ a ((discrepancy T θ₀).mkQ v))
187     rw [ih, quotientUpdate_candidate]
188 
189 /-- Invisibility implies observable agreement on arbitrary fixed-candidate words. -/
190 theorem agreement_of_discrepancy_invisible (T : Θ → A → V →ₗ[K] V)
191     (θ₀ : Θ) (Q : V →ₗ[K] Y) (h : discrepancy T θ₀ ≤ LinearMap.ker Q) :
192     ObservableAgreement T θ₀ Q := by
193   intro θ w
194   ext v
195   change Q (wordMap (T θ) w v) = Q (wordMap (T θ₀) w v)
196   rw [← quotientReadout_mk T θ₀ Q h (wordMap (T θ) w v),
197     ← quotientReadout_mk T θ₀ Q h (wordMap (T θ₀) w v),
198     word_quotient, word_quotient]
199 
200 /-- The exact equivalence of the first two source conditions. -/
201 theorem agreement_iff_invisible (T : Θ → A → V →ₗ[K] V)
202     (θ₀ : Θ) (Q : V →ₗ[K] Y) :
203     ObservableAgreement T θ₀ Q ↔ discrepancy T θ₀ ≤ LinearMap.ker Q :=
204   ⟨discrepancy_invisible_of_agreement T θ₀ Q, agreement_of_discrepancy_invisible T θ₀ Q⟩
205 
206 /-- The all-initial-vector fixed-candidate premise also controls arbitrary switching. -/
207 theorem switching_output (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ)
208     (Q : V →ₗ[K] Y) (h : ObservableAgreement T θ₀ Q)
209     (w : List (Θ × A)) (v : V) :
210     Q (switchedMap T w v) = Q (wordMap (T θ₀) (w.map Prod.snd) v) := by
211   have hE := discrepancy_invisible_of_agreement T θ₀ Q h
212   rw [← quotientReadout_mk T θ₀ Q hE (switchedMap T w v),
213     ← quotientReadout_mk T θ₀ Q hE (wordMap (T θ₀) (w.map Prod.snd) v),
214     switched_quotient, word_quotient]
215 
216 end
217 end Komorebi.MachineTheory.CommonQuotient

Back to source controls