JointReconstruction.lean

1 import Mathlib.LinearAlgebra.Basis.VectorSpace
2 import Mathlib.LinearAlgebra.Isomorphisms
3 import Mathlib.LinearAlgebra.Pi
4 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
5 
6 /-! # Target-relative joint reconstruction
7 
8 Core 8.1. Records and protected targets are actual field-linear maps. The decoder
9 constructed below has the entire record space as its domain. First it descends
10 through the kernel quotient to the attainable image, then Mathlib's basis
11 extension theorem extends it to the full space. This is an algebraic existence
12 result using classical choice, not an executable decoder or a communication law.
13 
14 The general theorem does not need finite dimension. `finite_joint_reconstruction`
15 retains the manuscript's finite-dimensional state space and finite record family.
16 -/
17 namespace Komorebi.MachineTheory.JointReconstruction
18 
19 noncomputable section
20 
21 variable {K V W T : Type*} [Field K]
22 variable [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
23 variable [AddCommGroup T] [Module K T]
24 
25 /-- Every linear decoder annihilates all ambiguities left by its input record. -/
26 theorem ker_le_of_decoder (A : V →ₗ[K] W) (Q : V →ₗ[K] T) (D : W →ₗ[K] T)
27     (h : Q = D.comp A) : LinearMap.ker A ≤ LinearMap.ker Q := by
28   rw [h]
29   exact A.ker_le_ker_comp D
30 
31 /-- Kernel containment says that indistinguishable records have the same target. -/
32 theorem target_eq_of_record_eq (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
33     (h : LinearMap.ker A ≤ LinearMap.ker Q) {v w : V} (hvw : A v = A w) :
34     Q v = Q w := by
35   have hzero : A (v - w) = 0 := by rw [map_sub, hvw, sub_self]
36   have hq : Q (v - w) = 0 := h hzero
37   exact sub_eq_zero.mp (by simpa only [map_sub] using hq)
38 
39 /-- Conversely, target constancy on record fibers implies the kernel condition. -/
40 theorem ker_le_of_target_constant (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
41     (h : ∀ v w, A v = A w → Q v = Q w) : LinearMap.ker A ≤ LinearMap.ker Q := by
42   intro v hv
43   change Q v = 0
44   have hvw : A v = A 0 := by simpa using hv
45   simpa using h v 0 hvw
46 
47 /-- Exact ambiguity criterion, expressed without a chosen decoder. -/
48 theorem ker_le_iff_target_constant (A : V →ₗ[K] W) (Q : V →ₗ[K] T) :
49     LinearMap.ker A ≤ LinearMap.ker Q ↔ ∀ v w, A v = A w → Q v = Q w :=
50   ⟨fun h _ _ hvw => target_eq_of_record_eq A Q h hvw, ker_le_of_target_constant A Q⟩
51 
52 /-- The quotient construction defines a linear decoder on exactly the attainable image. -/
53 def imageDecoder (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
54     (h : LinearMap.ker A ≤ LinearMap.ker Q) : LinearMap.range A →ₗ[K] T :=
55   ((LinearMap.ker A).liftQ Q h).comp A.quotKerEquivRange.symm.toLinearMap
56 
57 /-- On an actually observed record, the image decoder returns the original target. -/
58 @[simp] theorem imageDecoder_apply (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
59     (h : LinearMap.ker A ≤ LinearMap.ker Q) (v : V) :
60     imageDecoder A Q h (A.rangeRestrict v) = Q v := by
61   change (A.ker.liftQ Q h) (A.quotKerEquivRange.symm ⟨A v, _⟩) = Q v
62   rw [LinearMap.quotKerEquivRange_symm_apply_image]
63   exact Submodule.liftQ_apply A.ker Q v
64 
65 /-- The image-level reconstruction identity is proved before extension. -/
66 theorem imageDecoder_comp_rangeRestrict (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
67     (h : LinearMap.ker A ≤ LinearMap.ker Q) :
68     (imageDecoder A Q h).comp A.rangeRestrict = Q := by
69   ext v
70   exact imageDecoder_apply A Q h v
71 
72 /-- Extending a basis produces a decoder on the whole record space, with image agreement. -/
73 theorem exists_decoder_extending_imageDecoder (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
74     (h : LinearMap.ker A ≤ LinearMap.ker Q) :
75     ∃ D : W →ₗ[K] T, D.comp (LinearMap.range A).subtype = imageDecoder A Q h :=
76   (imageDecoder A Q h).exists_extend
77 
78 /-- The extension, rather than just the image decoder, factors the protected target. -/
79 theorem exists_decoder_of_ker_le (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
80     (h : LinearMap.ker A ≤ LinearMap.ker Q) :
81     ∃ D : W →ₗ[K] T, Q = D.comp A := by
82   obtain ⟨D,hD⟩ := exists_decoder_extending_imageDecoder A Q h
83   refine ⟨D, ?_⟩
84   ext v
85   have he := LinearMap.congr_fun hD (A.rangeRestrict v)
86   change D (A v) = imageDecoder A Q h (A.rangeRestrict v) at he
87   exact (he.trans (imageDecoder_apply A Q h v)).symm
88 
89 /-- Core 8.1: a full-domain linear decoder exists exactly under kernel containment. -/
90 theorem exists_decoder_iff_ker_le (A : V →ₗ[K] W) (Q : V →ₗ[K] T) :
91     (∃ D : W →ₗ[K] T, Q = D.comp A) ↔ LinearMap.ker A ≤ LinearMap.ker Q :=
92   ⟨fun ⟨D,hD⟩ => ker_le_of_decoder A Q D hD, exists_decoder_of_ker_le A Q⟩
93 
94 /-- The same existence criterion in terms of equal record values. -/
95 theorem exists_decoder_iff_target_constant (A : V →ₗ[K] W) (Q : V →ₗ[K] T) :
96     (∃ D : W →ₗ[K] T, Q = D.comp A) ↔ ∀ v w, A v = A w → Q v = Q w := by
97   rw [exists_decoder_iff_ker_le, ker_le_iff_target_constant]
98 
99 /-- Extensions agree on attainable records, without asserting uniqueness off the image. -/
100 theorem decoders_agree_on_range (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
101     (D E : W →ₗ[K] T) (hD : Q = D.comp A) (hE : Q = E.comp A)
102     (r : W) (hr : r ∈ LinearMap.range A) : D r = E r := by
103   obtain ⟨v,rfl⟩ := hr
104   exact (LinearMap.congr_fun hD v).symm.trans (LinearMap.congr_fun hE v)
105 
106 /-- A surviving ambiguity with nonzero target forbids every full-domain linear decoder. -/
107 theorem no_decoder_of_ambiguity (A : V →ₗ[K] W) (Q : V →ₗ[K] T)
108     (v : V) (hA : A v = 0) (hQ : Q v ≠ 0) :
109     ¬ ∃ D : W →ₗ[K] T, Q = D.comp A := by
110   intro hD
111   exact hQ ((exists_decoder_iff_ker_le A Q).mp hD hA)
112 
113 /-- Failure of reconstruction has an actual algebraic ambiguity witness. -/
114 theorem no_decoder_iff_ambiguity (A : V →ₗ[K] W) (Q : V →ₗ[K] T) :
115     (¬ ∃ D : W →ₗ[K] T, Q = D.comp A) ↔ ∃ v : V, A v = 0 ∧ Q v ≠ 0 := by
116   rw [exists_decoder_iff_ker_le]
117   change (¬ ∀ v, A v = 0 → Q v = 0) ↔ _
118   simp only [not_forall, exists_prop]
119 
120 /-- Full-state recovery is the identity-target specialization, exactly injectivity. -/
121 theorem full_state_iff_injective (A : V →ₗ[K] W) :
122     (∃ D : W →ₗ[K] V, LinearMap.id = D.comp A) ↔ Function.Injective A := by
123   rw [exists_decoder_iff_ker_le, LinearMap.ker_id, le_bot_iff, LinearMap.ker_eq_bot]
124 
125 section Records
126 variable {ι : Type*} {R : ι → Type*}
127 variable [∀ i, AddCommGroup (R i)] [∀ i, Module K (R i)]
128 
129 /-- The accessible joint record is the actual product-valued linear map. -/
130 def stackRecords (A : (i : ι) → V →ₗ[K] R i) : V →ₗ[K] ((i : ι) → R i) :=
131   LinearMap.pi A
132 
133 /-- Each coordinate of the stacked record is the original participant's record. -/
134 @[simp] theorem stackRecords_apply (A : (i : ι) → V →ₗ[K] R i) (v : V) (i : ι) :
135     stackRecords A v i = A i v := rfl
136 
137 /-- Sharing removes exactly the directions not common to every record kernel. -/
138 theorem ker_stackRecords (A : (i : ι) → V →ₗ[K] R i) :
139     LinearMap.ker (stackRecords A) = ⨅ i, LinearMap.ker (A i) :=
140   LinearMap.ker_pi A
141 
142 /-- Explicit pointwise form of the common-ambiguity identity. -/
143 theorem mem_ker_stackRecords (A : (i : ι) → V →ₗ[K] R i) (v : V) :
144     v ∈ LinearMap.ker (stackRecords A) ↔ ∀ i, A i v = 0 := by
145   rw [ker_stackRecords, Submodule.mem_iInf]
146   rfl
147 
148 /-- Target-relative criterion for the complete accessible family. -/
149 theorem stacked_decoder_iff (A : (i : ι) → V →ₗ[K] R i) (Q : V →ₗ[K] T) :
150     (∃ D : ((i : ι) → R i) →ₗ[K] T, Q = D.comp (stackRecords A)) ↔
151       (⨅ i, LinearMap.ker (A i)) ≤ LinearMap.ker Q := by
152   rw [exists_decoder_iff_ker_le, ker_stackRecords]
153 
154 /-- Full-state joint recovery requires the common ambiguity subspace to vanish. -/
155 theorem stacked_full_state_iff (A : (i : ι) → V →ₗ[K] R i) :
156     (∃ D : ((i : ι) → R i) →ₗ[K] V, LinearMap.id = D.comp (stackRecords A)) ↔
157       (⨅ i, LinearMap.ker (A i)) = ⊥ := by
158   rw [stacked_decoder_iff, LinearMap.ker_id, le_bot_iff]
159 
160 /-- Source-facing Core 8.1 with finite-dimensional states and finitely many records. -/
161 theorem finite_joint_reconstruction [Fintype ι] [FiniteDimensional K V]
162     (A : (i : ι) → V →ₗ[K] R i) (Q : V →ₗ[K] T) :
163     ((∃ D : ((i : ι) → R i) →ₗ[K] T, Q = D.comp (stackRecords A)) ↔
164       LinearMap.ker (stackRecords A) ≤ LinearMap.ker Q) ∧
165     ((∃ D : ((i : ι) → R i) →ₗ[K] V, LinearMap.id = D.comp (stackRecords A)) ↔
166       Function.Injective (stackRecords A)) ∧
167     LinearMap.ker (stackRecords A) = ⨅ i, LinearMap.ker (A i) :=
168   ⟨exists_decoder_iff_ker_le (stackRecords A) Q,
169     full_state_iff_injective (stackRecords A), ker_stackRecords A⟩
170 
171 end Records
172 end
173 end Komorebi.MachineTheory.JointReconstruction

Back to source controls