SchurSupport.lean

1 module
2 public import InverseSupport
3 import all InverseSupport
4 import all PacketIR
5 import all QuantumPacketCore
6 public import Mathlib.Tactic
7 
8 /-!
9 Author: Komorebi P. Paper VIII item 6.8.
10 Actual rectangular coupling matrices and arbitrary packet projectors on both
11 retained and hidden spaces. The hidden inverse is Mathlib's matrix inverse.
12 A length-zero hidden path is allowed (enter and exit through the same packet).
13 -/
14 public section
15 set_option autoImplicit false
16 namespace KomorebiPaperVIII
17 open scoped BigOperators Classical
18 open KomorebiPaperVII
19 variable {K X Y I J : Type*} [Field K]
20 variable [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
21 variable [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J]
22 variable (P : PacketFamily (Matrix X X K) I) (Q : PacketFamily (Matrix Y Y K) J)
23 
24 /-- The correction is expanded through all actual hidden packet inverse blocks. -/
25 theorem schur_correction_expansion (B : Matrix X Y K) (Hinv : Matrix Y Y K)
26     (C : Matrix Y X K) (b a : I) :
27     P.block (B*Hinv*C) b a =
28       ∑ j, ∑ k, (P.proj b*B) * Q.block Hinv j k * (C*P.proj a) := by
29   conv_lhs => rw [←Q.reconstruct Hinv]
30   simp only [PacketFamily.block,Matrix.mul_sum,Matrix.sum_mul,Matrix.mul_assoc]
31 
32 /-- A nonzero correction has an actual nonzero entrance, inverse block, and exit. -/
33 theorem schur_correction_support (B : Matrix X Y K) (H : Matrix Y Y K)
34     (C : Matrix Y X K) (hH : IsUnit H.det) (b a : I)
35     (h : P.block (B*H⁻¹*C) b a ≠ 0) :
36     ∃ j k, P.proj b*B*Q.proj j ≠ 0 ∧ Reachable Q H j k ∧
37       Q.proj k*C*P.proj a ≠ 0 := by
38   rw [schur_correction_expansion P Q] at h
39   obtain ⟨j,_,hj⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
40   obtain ⟨k,_,hk⟩ := Finset.exists_ne_zero_of_sum_ne_zero hj
41   have hinv : Q.block H⁻¹ j k ≠ 0 := by
42     intro hz
43     apply hk
44     rw [hz,Matrix.mul_zero,Matrix.zero_mul]
45   have he : (P.proj b*B)*Q.block H⁻¹ j k*(C*P.proj a) =
46       (P.proj b*B*Q.proj j)*H⁻¹*(Q.proj k*C*P.proj a) := by
47     simp only [PacketFamily.block,Matrix.mul_assoc]
48   refine ⟨j,k,?_,matrix_inverse_support Q H hH j k hinv,?_⟩
49   · intro hz
50     apply hk
51     rw [he,hz,Matrix.zero_mul,Matrix.zero_mul]
52   · intro hz
53     apply hk
54     rw [he,hz,Matrix.mul_zero]
55 
56 /-- Item 6.8: the actual Schur support lies in direct edges or hidden walks. -/
57 theorem schur_support_inclusion (A : Matrix X X K) (B : Matrix X Y K)
58     (H : Matrix Y Y K) (C : Matrix Y X K) (hH : IsUnit H.det) (b a : I)
59     (h : P.block (A-B*H⁻¹*C) b a ≠ 0) :
60     P.block A b a ≠ 0 ∨
61       ∃ j k, P.proj b*B*Q.proj j ≠ 0 ∧ Reachable Q H j k ∧
62         Q.proj k*C*P.proj a ≠ 0 := by
63   by_cases ha : P.block A b a ≠ 0
64   · exact Or.inl ha
65   · right
66     apply schur_correction_support P Q B H C hH b a
67     intro hc
68     apply h
69     have hz : P.block A b a = 0 := not_ne_iff.mp ha
70     change P.proj b*(A-B*H⁻¹*C)*P.proj a = 0
71     rw [Matrix.mul_sub,Matrix.sub_mul]
72     change P.block A b a - P.block (B*H⁻¹*C) b a = 0
73     rw [hz,hc,sub_self]
74 
75 /-- No permitted route certifies a zero retained Schur block. -/
76 theorem schur_zero_of_no_route (A : Matrix X X K) (B : Matrix X Y K)
77     (H : Matrix Y Y K) (C : Matrix Y X K) (hH : IsUnit H.det) (b a : I)
78     (ha : P.block A b a = 0)
79     (hr : ∀ j k, P.proj b*B*Q.proj j ≠ 0 → Q.proj k*C*P.proj a ≠ 0 →
80       ¬ Reachable Q H j k) : P.block (A-B*H⁻¹*C) b a = 0 := by
81   by_contra hn
82   obtain h | ⟨j,k,hj,hp,hk⟩ := schur_support_inclusion P Q A B H C hH b a hn
83   · exact h ha
84   · exact hr j k hj hk hp
85 
86 end KomorebiPaperVIII
87 
88 -- FIFTH BLOCK AXIOM AUDIT
89 #print axioms KomorebiPaperVIII.schur_correction_expansion
90 #print axioms KomorebiPaperVIII.schur_correction_support
91 #print axioms KomorebiPaperVIII.schur_support_inclusion
92 #print axioms KomorebiPaperVIII.schur_zero_of_no_route

Back to source controls