DiscrepancyClosure.lean

1 import MachineTheory.CommonQuotientInterface
2 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
3 
4 /-!
5 # Finite construction of the propagated discrepancy space
6 
7 Start from the sum of difference ranges, then add the images under each
8 reference action. The sequence is increasing, stays inside E, and has no plateau
9 before E. Finite dimension gives stabilization by dim(V) rounds. The code is an
10 algebraic construction, not a claim about efficient numerical subspace discovery.
11 -/
12 namespace Komorebi.MachineTheory.CommonQuotient
13 
14 noncomputable section
15 
16 variable {K V Y A Θ : Type*}
17 variable [Field K] [AddCommGroup V] [Module K V] [AddCommGroup Y] [Module K Y]
18 
19 /-- Initial sum of all one-step difference ranges. -/
20 def seed (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) : Submodule K V :=
21   ⨆ θ, ⨆ a, LinearMap.range (T θ a - T θ₀ a)
22 
23 /-- One invariant-closure step. -/
24 def closureStep (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (N : Submodule K V) : Submodule K V :=
25   N ⊔ ⨆ a, N.map (T θ₀ a)
26 
27 /-- The actual increasing construction, starting at the source's difference ranges. -/
28 def stage (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) : ℕ → Submodule K V
29   | 0 => seed T θ₀
30   | n + 1 => closureStep T θ₀ (stage T θ₀ n)
31 
32 @[simp] theorem stage_zero (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) :
33     stage T θ₀ 0 = seed T θ₀ := rfl
34 
35 @[simp] theorem stage_succ (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (n : ℕ) :
36     stage T θ₀ (n + 1) = closureStep T θ₀ (stage T θ₀ n) := rfl
37 
38 /-- Every input difference is already present at stage zero. -/
39 theorem difference_mem_seed (T : Θ → A → V →ₗ[K] V) (θ₀ θ : Θ) (a : A) (v : V) :
40     (T θ a - T θ₀ a) v ∈ seed T θ₀ := by
41   have h : LinearMap.range (T θ a - T θ₀ a) ≤ seed T θ₀ :=
42     le_iSup_of_le θ (le_iSup_of_le a le_rfl)
43   exact h ⟨v, rfl⟩
44 
45 /-- The initial seed is contained in the propagated span. -/
46 theorem seed_le_discrepancy (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) :
47     seed T θ₀ ≤ discrepancy T θ₀ := by
48   apply iSup_le
49   intro θ
50   apply iSup_le
51   intro a x hx
52   obtain ⟨v, rfl⟩ := hx
53   exact difference_mem T θ₀ a θ v
54 
55 /-- Enlarging a submodule cannot shrink its closure step. -/
56 theorem closureStep_mono (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) :
57     Monotone (closureStep T θ₀) := by
58   intro N P h
59   exact sup_le_sup h (iSup_mono fun a => Submodule.map_mono h)
60 
61 /-- Each step contains the preceding stage. -/
62 theorem stage_le_succ (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (n : ℕ) :
63     stage T θ₀ n ≤ stage T θ₀ (n + 1) := le_sup_left
64 
65 /-- The sequence is increasing over arbitrary stage indices. -/
66 theorem stage_mono (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) : Monotone (stage T θ₀) :=
67   monotone_nat_of_le_succ (stage_le_succ T θ₀)
68 
69 /-- No iteration introduces a vector outside the defined discrepancy span. -/
70 theorem stage_le_discrepancy (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (n : ℕ) :
71     stage T θ₀ n ≤ discrepancy T θ₀ := by
72   induction n with
73   | zero => exact seed_le_discrepancy T θ₀
74   | succ n ih =>
75     apply sup_le ih
76     apply iSup_le
77     intro a x hx
78     obtain ⟨v, hv, rfl⟩ := hx
79     exact reference_invariant T θ₀ a (ih hv)
80 
81 /-- At a plateau every reference-action image remains in the same stage. -/
82 theorem plateau_invariant (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (n : ℕ)
83     (h : stage T θ₀ (n + 1) = stage T θ₀ n)
84     (a : A) (x : V) (hx : x ∈ stage T θ₀ n) : T θ₀ a x ∈ stage T θ₀ n := by
85   have hmap : (stage T θ₀ n).map (T θ₀ a) ≤ stage T θ₀ (n + 1) :=
86     le_trans (le_iSup (fun b : A => (stage T θ₀ n).map (T θ₀ b)) a) le_sup_right
87   have hx' := hmap ⟨x, hx, rfl⟩
88   simpa only [h] using hx'
89 
90 /-- The first plateau already equals E, without any finite-dimensional premise. -/
91 theorem plateau_eq_discrepancy (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (n : ℕ)
92     (h : stage T θ₀ (n + 1) = stage T θ₀ n) : stage T θ₀ n = discrepancy T θ₀ := by
93   apply le_antisymm (stage_le_discrepancy T θ₀ n)
94   apply discrepancy_le T θ₀
95   · intro θ a v
96     exact stage_mono T θ₀ (Nat.zero_le n) (difference_mem_seed T θ₀ θ a v)
97   · exact plateau_invariant T θ₀ n h
98 
99 /-- In finite dimension, a plateau occurs no later than the ambient dimension. -/
100 theorem bounded_plateau [FiniteDimensional K V] (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) :
101     ∃ n ≤ Module.finrank K V, stage T θ₀ (n + 1) = stage T θ₀ n := by
102   by_contra h
103   push Not at h
104   have hstrict : ∀ n, n ≤ Module.finrank K V → stage T θ₀ n < stage T θ₀ (n + 1) := by
105     intro n hn
106     exact lt_of_le_of_ne (stage_le_succ T θ₀ n) (Ne.symm (h n hn))
107   have hgrowth : ∀ n, n ≤ Module.finrank K V + 1 → n ≤ Module.finrank K (stage T θ₀ n) := by
108     intro n
109     induction n with
110     | zero => intro _; exact Nat.zero_le _
111     | succ n ih =>
112       intro hn
113       have hn' : n ≤ Module.finrank K V := Nat.le_of_succ_le_succ hn
114       have hp := ih (Nat.le_trans hn' (Nat.le_succ _))
115       have hi := Submodule.finrank_lt_finrank_of_lt (hstrict n hn')
116       omega
117   have hbig := hgrowth (Module.finrank K V + 1) le_rfl
118   have hupper := (stage T θ₀ (Module.finrank K V + 1)).finrank_le
119   omega
120 
121 /-- The source construction is complete by dim(V), not just at an unspecified limit. -/
122 theorem stage_finrank_eq [FiniteDimensional K V] (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) :
123     stage T θ₀ (Module.finrank K V) = discrepancy T θ₀ := by
124   obtain ⟨n, hn, heq⟩ := bounded_plateau T θ₀
125   apply le_antisymm (stage_le_discrepancy T θ₀ _)
126   rw [← plateau_eq_discrepancy T θ₀ n heq]
127   exact stage_mono T θ₀ hn
128 
129 /-- Every later stage remains the same constructed discrepancy space. -/
130 theorem stage_eq_of_finrank_le [FiniteDimensional K V] (T : Θ → A → V →ₗ[K] V)
131     (θ₀ : Θ) (n : ℕ) (hn : Module.finrank K V ≤ n) : stage T θ₀ n = discrepancy T θ₀ := by
132   apply le_antisymm (stage_le_discrepancy T θ₀ n)
133   rw [← stage_finrank_eq T θ₀]
134   exact stage_mono T θ₀ hn
135 
136 /-- Core 2.4 with the finite-dimensional, finite-catalogue source assumptions.
137 The three equivalent conditions, canonical quotient, arbitrary switching and
138 finite discrepancy construction are tied to the same T, reference and readout. -/
139 theorem source_core24 [Fintype A] [Fintype Θ] [FiniteDimensional K V]
140     (T : Θ → A → V →ₗ[K] V) (θ₀ : Θ) (Q : V →ₗ[K] Y) :
141     (ObservableAgreement T θ₀ Q ↔ discrepancy T θ₀ ≤ LinearMap.ker Q) ∧
142     (discrepancy T θ₀ ≤ LinearMap.ker Q ↔ Nonempty (CommonModel T Q)) ∧
143     stage T θ₀ (Module.finrank K V) = discrepancy T θ₀ ∧
144     (ObservableAgreement T θ₀ Q → ∀ (w : List (Θ × A)) (v : V),
145       Q (switchedMap T w v) = Q (wordMap (T θ₀) (w.map Prod.snd) v)) :=
146   ⟨agreement_iff_invisible T θ₀ Q, (commonModel_iff_invisible T θ₀ Q).symm,
147     stage_finrank_eq T θ₀, switching_output T θ₀ Q⟩
148 
149 /-- The source-facing raw reference operator family is tied to an actual candidate. -/
150 theorem source_core24_reference [Fintype A] [Fintype Θ] [FiniteDimensional K V]
151     (T : Θ → A → V →ₗ[K] V) (R : A → V →ₗ[K] V) (θ₀ : Θ)
152     (hR : T θ₀ = R) (Q : V →ₗ[K] Y) :
153     ((∀ θ w, Q.comp (wordMap (T θ) w) = Q.comp (wordMap R w)) ↔
154       Nonempty (CommonModel T Q)) ∧
155     ((∀ θ w, Q.comp (wordMap (T θ) w) = Q.comp (wordMap R w)) →
156       ∀ (w : List (Θ × A)) (v : V), Q (switchedMap T w v) = Q (wordMap R (w.map Prod.snd) v)) := by
157   subst R
158   exact ⟨agreement_iff_commonModel T θ₀ Q, switching_output T θ₀ Q⟩
159 
160 end
161 end Komorebi.MachineTheory.CommonQuotient

Back to source controls