ProtectedLinearCertificates.lean

1 import Mathlib.LinearAlgebra.Dual.Lemmas
2 import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
3 import Mathlib.LinearAlgebra.Matrix.ToLin
4 import Mathlib.LinearAlgebra.Matrix.Rank
5 import Mathlib.Tactic.LinearCombination
6 import Mathlib.Tactic.Abel
7 
8 set_option autoImplicit false
9 
10 /-!
11 # KS57: exact protected answers or normalized algebraic obstruction certificates
12 
13 The alternative is proved for linear maps over an arbitrary field. A finite
14 matrix specialization retains actual row-vector equations. The proof does
15 not assume an elimination algorithm is correct, and does not certify the
16 separate Python implementation for arbitrary inputs.
17 -/
18 universe u v w z
19 noncomputable section
20 namespace KomorebiSpace.ProtectedLinearCertificates
21 open Module
22 variable {K : Type u} [Field K]
23 variable {E : Type v} {R : Type w} {S : Type z}
24 variable [AddCommGroup E] [Module K E]
25 variable [AddCommGroup R] [Module K R]
26 variable [AddCommGroup S] [Module K S]
27 variable (D : E →ₗ[K] R) (p : E →ₗ[K] S)
28 
29 def Answer (x y : E) : Prop := D y = 0 ∧ p y = p x
30 
31 def Certificate (x : E) : Prop :=
32   ∃ (lam : R →ₗ[K] K) (mu : S →ₗ[K] K),
33     lam.comp D = mu.comp p ∧ lam (D x) = 1
34 
35 /-- A certificate directly contradicts the equations of a protected answer. -/
36 theorem certificate_excludes_answer (x : E) (hc : Certificate D p x) :
37     ¬ ∃ y, Answer D p x y := by
38   rintro ⟨y, hy⟩
39   obtain ⟨lam, mu, hrel, hn⟩ := hc
40   have hzero : (1 : K) = 0 := calc
41     1 = lam (D x) := hn.symm
42     _ = mu (p x) := LinearMap.congr_fun hrel x
43     _ = mu (p y) := congrArg mu hy.2.symm
44     _ = lam (D y) := (LinearMap.congr_fun hrel y).symm
45     _ = 0 := by rw [hy.1, map_zero]
46   exact one_ne_zero hzero
47 
48 /-- Feasibility is membership in the range of the actual stacked operator. -/
49 theorem answer_iff_stacked_range (x : E) :
50     (∃ y, Answer D p x y) ↔ (0, p x) ∈ LinearMap.range (D.prod p) := by
51   constructor
52   · rintro ⟨y, hd, hp⟩
53     exact ⟨y, Prod.ext hd hp⟩
54   · rintro ⟨y, hy⟩
55     exact ⟨y, congrArg Prod.fst hy, congrArg Prod.snd hy⟩
56 
57 /-- Algebraic dual separation supplies a normalized witness when the stacked system fails. -/
58 theorem certificate_of_no_answer (x : E) (hn : ¬ ∃ y, Answer D p x y) :
59     Certificate D p x := by
60   have hb : (0, p x) ∉ LinearMap.range (D.prod p) := by
61     intro h
62     exact hn ((answer_iff_stacked_range D p x).mpr h)
63   obtain ⟨f, hf, hmap⟩ := Submodule.exists_dual_map_eq_bot_of_notMem hb inferInstance
64   let w : (R × S) →ₗ[K] K := (f (0, p x))⁻¹ • f
65   have hw (y : E) : w (D y, p y) = 0 := by
66     have hz : f (D y, p y) ∈ (LinearMap.range (D.prod p)).map f :=
67       ⟨(D y, p y), ⟨y, rfl⟩, rfl⟩
68     rw [hmap] at hz
69     change f (D y, p y) = 0 at hz
70     change (f (0, p x))⁻¹ * f (D y, p y) = 0
71     rw [hz, mul_zero]
72   have hwb : w (0, p x) = 1 := inv_mul_cancel₀ hf
73   let lam : R →ₗ[K] K := -(w.comp (LinearMap.inl K R S))
74   let mu : S →ₗ[K] K := w.comp (LinearMap.inr K R S)
75   have hsum (y : E) : w (D y, 0) + w (0, p y) = 0 := by
76     rw [← map_add]
77     simpa only [Prod.mk_add_mk, add_zero, zero_add] using hw y
78   refine ⟨lam, mu, ?_, ?_⟩
79   · ext y
80     change -w (D y, 0) = w (0, p y)
81     linear_combination -hsum y
82   · change -w (D x, 0) = 1
83     have hs := hsum x
84     rw [hwb] at hs
85     linear_combination -hs
86 
87 theorem certificate_iff_no_answer (x : E) :
88     Certificate D p x ↔ ¬ ∃ y, Answer D p x y :=
89   ⟨certificate_excludes_answer D p x, certificate_of_no_answer D p x⟩
90 
91 theorem answer_or_certificate (x : E) :
92     (∃ y, Answer D p x y) ∨ Certificate D p x := by
93   classical
94   by_cases h : ∃ y, Answer D p x y
95   · exact Or.inl h
96   · exact Or.inr (certificate_of_no_answer D p x h)
97 
98 /-- Exactly one alternative holds. -/
99 theorem exclusive_alternative (x : E) :
100     ((∃ y, Answer D p x y) ∨ Certificate D p x) ∧
101     ¬ ((∃ y, Answer D p x y) ∧ Certificate D p x) :=
102   ⟨answer_or_certificate D p x, fun h => certificate_excludes_answer D p x h.2 h.1⟩
103 
104 def ambiguity : Submodule K E := D.ker ⊓ p.ker
105 
106 theorem answer_iff_difference (x y₀ y : E) (hy₀ : Answer D p x y₀) :
107     Answer D p x y ↔ y-y₀ ∈ ambiguity D p := by
108   change (D y = 0 ∧ p y = p x) ↔ (D (y-y₀)=0 ∧ p (y-y₀)=0)
109   rw [map_sub, map_sub, hy₀.1, hy₀.2, sub_zero, sub_eq_zero]
110 
111 /-- Once an answer is chosen, the whole fiber is its affine translate by the ambiguity space. -/
112 def answerEquivAmbiguity (x y₀ : E) (hy₀ : Answer D p x y₀) :
113     {y : E // Answer D p x y} ≃ ambiguity D p where
114   toFun y := ⟨y.val-y₀, (answer_iff_difference D p x y₀ y.val hy₀).mp y.property⟩
115   invFun h := ⟨y₀+h.val, (answer_iff_difference D p x y₀ _ hy₀).mpr (by
116     simpa only [add_sub_cancel_left] using h.property)⟩
117   left_inv y := by apply Subtype.ext; change y₀+(y.val-y₀)=y.val; abel
118   right_inv h := by apply Subtype.ext; change (y₀+h.val)-y₀=h.val; abel
119 
120 theorem stacked_kernel : (D.prod p).ker = ambiguity D p := by
121   ext y
122   change ((D y, p y) = (0,0)) ↔ (D y=0 ∧ p y=0)
123   simp only [Prod.mk.injEq]
124 
125 /-- Rank-nullity includes zero-dimensional sources and targets. -/
126 theorem ambiguity_finrank [FiniteDimensional K E] :
127     Module.finrank K (ambiguity D p) =
128       Module.finrank K E - Module.finrank K (LinearMap.range (D.prod p)) := by
129   have h := LinearMap.finrank_range_add_finrank_ker (D.prod p)
130   rw [stacked_kernel] at h
131   omega
132 
133 end KomorebiSpace.ProtectedLinearCertificates
134 
135 namespace KomorebiSpace.ProtectedLinearCertificates
136 open Matrix Module
137 variable {K : Type u} [Field K]
138 variable {m n s : Type*} [Fintype m] [Fintype n] [Fintype s]
139 
140 /-- Coordinate row of an algebraic functional in the standard finite basis. -/
141 def rowCoefficients {ι : Type*} [Fintype ι] (f : (ι → K) →ₗ[K] K) : ι → K := by
142   classical
143   exact fun i => f (fun j => if i=j then 1 else 0)
144 
145 theorem linear_form_apply {ι : Type*} [Fintype ι]
146     (f : (ι → K) →ₗ[K] K) (x : ι → K) :
147     f x = rowCoefficients f ⬝ᵥ x := by
148   classical
149   rw [LinearMap.pi_apply_eq_sum_univ]
150   apply Finset.sum_congr rfl
151   intro i hi
152   exact mul_comm _ _
153 
154 /-- Literal matrix row certificates, rather than an unspecified dual obstruction. -/
155 theorem matrix_certificate_iff (A : Matrix m n K) (P : Matrix s n K) (x : n → K) :
156     (¬ ∃ y : n → K, A *ᵥ y = 0 ∧ P *ᵥ y = P *ᵥ x) ↔
157       ∃ (lam : m → K) (mu : s → K), lam ᵥ* A = mu ᵥ* P ∧ lam ⬝ᵥ (A *ᵥ x) = 1 := by
158   constructor
159   · intro h
160     obtain ⟨lam, mu, hrel, hn⟩ := certificate_of_no_answer A.mulVecLin P.mulVecLin x h
161     refine ⟨rowCoefficients lam, rowCoefficients mu, ?_, ?_⟩
162     · classical
163       funext j
164       have he := LinearMap.congr_fun hrel (Pi.single j 1)
165       change lam (A *ᵥ Pi.single j 1) = mu (P *ᵥ Pi.single j 1) at he
166       rw [linear_form_apply, linear_form_apply] at he
167       simpa only [Matrix.mulVec_single_one, Matrix.vecMul, dotProduct, Matrix.col_apply] using he
168     · rw [← linear_form_apply]
169       exact hn
170   · rintro ⟨lam, mu, hrel, hn⟩
171     apply certificate_excludes_answer A.mulVecLin P.mulVecLin x
172     refine ⟨dotProductBilin K K lam, dotProductBilin K K mu, ?_, hn⟩
173     ext y
174     change lam ⬝ᵥ (A *ᵥ y) = mu ⬝ᵥ (P *ᵥ y)
175     rw [Matrix.dotProduct_mulVec, Matrix.dotProduct_mulVec, hrel]
176 
177 theorem matrix_exclusive_alternative (A : Matrix m n K) (P : Matrix s n K) (x : n → K) :
178     ((∃ y : n → K, A *ᵥ y = 0 ∧ P *ᵥ y = P *ᵥ x) ∨
179       ∃ (lam : m → K) (mu : s → K), lam ᵥ* A = mu ᵥ* P ∧ lam ⬝ᵥ (A *ᵥ x) = 1) ∧
180     ¬ ((∃ y : n → K, A *ᵥ y = 0 ∧ P *ᵥ y = P *ᵥ x) ∧
181       ∃ (lam : m → K) (mu : s → K), lam ᵥ* A = mu ᵥ* P ∧ lam ⬝ᵥ (A *ᵥ x) = 1) := by
182   rw [← matrix_certificate_iff]
183   exact ⟨Classical.em _, fun h => h.2 h.1⟩
184 
185 /-- The literal vertical block matrix, with rows indexed by the disjoint union. -/
186 def stackedMatrix (A : Matrix m n K) (P : Matrix s n K) : Matrix (Sum m s) n K :=
187   fun i => Sum.elim (fun j => A j) (fun j => P j) i
188 
189 omit [Fintype m] [Fintype s] in
190 theorem stacked_matrix_kernel (A : Matrix m n K) (P : Matrix s n K) :
191     (stackedMatrix A P).mulVecLin.ker = ambiguity A.mulVecLin P.mulVecLin := by
192   ext y
193   change ((stackedMatrix A P) *ᵥ y = 0) ↔ (A *ᵥ y = 0 ∧ P *ᵥ y = 0)
194   constructor
195   · intro h
196     exact ⟨funext (fun i => congrFun h (Sum.inl i)), funext (fun i => congrFun h (Sum.inr i))⟩
197   · rintro ⟨hA, hP⟩
198     funext i
199     cases i with
200     | inl j => exact congrFun hA j
201     | inr j => exact congrFun hP j
202 
203 omit [Fintype m] [Fintype s] in
204 theorem matrix_ambiguity_dimension (A : Matrix m n K) (P : Matrix s n K) :
205     Module.finrank K (ambiguity A.mulVecLin P.mulVecLin) =
206       Fintype.card n - (stackedMatrix A P).rank := by
207   have h := LinearMap.finrank_range_add_finrank_ker (stackedMatrix A P).mulVecLin
208   rw [stacked_matrix_kernel, Module.finrank_fintype_fun_eq_card] at h
209   change (stackedMatrix A P).rank +
210     Module.finrank K (ambiguity A.mulVecLin P.mulVecLin) = Fintype.card n at h
211   omega
212 
213 end KomorebiSpace.ProtectedLinearCertificates
214 end

Back to source controls