TransferSupport.lean

1 module
2 public import PacketIR
3 import all PacketIR
4 import all QuantumPacketCore
5 public import Lean.Elab.Tactic.Omega
6 
7 /-!
8 Author: Komorebi P.
9 Paper VIII items 6.1, 6.2, 6.3. Paths retain their length and direction.
10 Zero-length paths are included explicitly, so the constant polynomial term
11 and diagonal reachability are not silently dropped.
12 -/
13 
14 public section
15 set_option autoImplicit false
16 namespace KomorebiPaperVIII
17 open scoped BigOperators
18 open KomorebiPaperVII
19 
20 variable {R I : Type*} [Ring R] [Fintype I] [DecidableEq I]
21 variable (P : PacketFamily R I)
22 
23 /-- A path of n exact nonzero transfer blocks, source a and target b. -/
24 def TransferPath (A : R) : ℕ → I → I → Prop
25   | 0, b, a => b = a
26   | n + 1, b, a => ∃ c, P.block A b c ≠ 0 ∧ TransferPath A n c a
27 
28 /-- Finite active-path evaluation. Zero edges are explicitly excluded. -/
29 noncomputable def activePathSum (A : R) : ℕ → I → I → R
30   | 0, b, a => if b = a then P.proj a else 0
31   | n + 1, b, a => by
32       classical
33       exact ∑ c, if P.block A b c ≠ 0 then
34         P.block A b c * activePathSum A n c a else 0
35 
36 /-- Theorem 6.1: the nested active-path sum equals the actual power block. -/
37 theorem power_path_expansion (A : R) (n : ℕ) (b a : I) :
38     P.block (A ^ n) b a = activePathSum P A n b a := by
39   classical
40   induction n generalizing b a with
41   | zero =>
42       by_cases h : b = a
43       · subst b
44         simp [activePathSum, PacketFamily.block, P.mul_proj]
45       · simp [activePathSum, PacketFamily.block, P.mul_proj, h]
46   | succ n ih =>
47       rw [pow_succ', P.compose_blocks]
48       simp only [activePathSum]
49       apply Finset.sum_congr rfl
50       intro c _
51       rw [ih]
52       by_cases h : P.block A b c = 0 <;> simp [h]
53 
54 /-- A recursive path sum vanishes when no contributing path exists. -/
55 theorem active_path_sum_zero (A : R) (n : ℕ) (b a : I)
56     (h : ¬ TransferPath P A n b a) : activePathSum P A n b a = 0 := by
57   classical
58   induction n generalizing b a with
59   | zero =>
60       change ¬ b = a at h
61       simp [activePathSum, h]
62   | succ n ih =>
63       simp only [activePathSum]
64       apply Finset.sum_eq_zero
65       intro c _
66       by_cases hc : P.block A b c = 0
67       · simp [hc]
68       · have hn : ¬ TransferPath P A n c a := by
69           intro hp
70           exact h ⟨c, hc, hp⟩
71         simp [hc, ih c a hn]
72 
73 /-- Theorem 6.1: no directed path of the required length implies a zero block. -/
74 theorem power_block_zero_of_no_path (A : R) (n : ℕ) (b a : I)
75     (h : ¬ TransferPath P A n b a) : P.block (A ^ n) b a = 0 := by
76   rw [power_path_expansion P]
77   exact active_path_sum_zero P A n b a h
78 
79 theorem power_support_inclusion (A : R) (n : ℕ) (b a : I)
80     (h : P.block (A ^ n) b a ≠ 0) : TransferPath P A n b a := by
81   classical
82   by_contra hn
83   exact h (power_block_zero_of_no_path P A n b a hn)
84 
85 /-- Corollary 6.3: a bound on path length gives nilpotence of the actual operator. -/
86 theorem nilpotent_of_path_bound (A : R) (h : ℕ)
87     (hpaths : ∀ b a, ¬ TransferPath P A (h + 1) b a) : A ^ (h + 1) = 0 := by
88   apply all_blocks_zero P
89   intro b a
90   exact power_block_zero_of_no_path P A (h + 1) b a (hpaths b a)
91 
92 /-- A topological-level certificate yields an explicit path-length bound. -/
93 theorem path_level_bound (A : R) (level : I → ℕ)
94     (hlevel : ∀ b a, P.block A b a ≠ 0 → level a < level b)
95     (n : ℕ) (b a : I) (hp : TransferPath P A n b a) :
96     level a + n ≤ level b := by
97   induction n generalizing b a with
98   | zero =>
99       have he : b = a := hp
100       subst b
101       omega
102   | succ n ih =>
103       obtain ⟨c, hc, hp⟩ := hp
104       have h1 := ih c a hp
105       have h2 := hlevel b c hc
106       omega
107 
108 /-- Constructive acyclicity certificate: levels 0,...,h force A^(h+1)=0. -/
109 theorem nilpotent_of_topological_levels (A : R) (h : ℕ) (level : I → Fin (h + 1))
110     (hlevel : ∀ b a, P.block A b a ≠ 0 → (level a).val < (level b).val) :
111     A ^ (h + 1) = 0 := by
112   apply nilpotent_of_path_bound P A h
113   intro b a hp
114   have hb := path_level_bound P A (fun i => (level i).val) hlevel (h + 1) b a hp
115   have hbound := (level b).isLt
116   omega
117 
118 section Polynomial
119 variable {K : Type*} [CommSemiring K] [Algebra K R]
120 
121 theorem block_smul (c : K) (A : R) (b a : I) :
122     P.block (c • A) b a = c • P.block A b a := by
123   simp only [PacketFamily.block, mul_smul_comm, smul_mul_assoc]
124 
125 /-- Corollary 6.2: the support of an actual finite polynomial is contained in
126     the union of power supports. Coefficients may be zero; degree zero is included. -/
127 theorem polynomial_support_inclusion (d : ℕ) (c : Fin (d + 1) → K) (A : R) (b a : I)
128     (h : P.block (∑ j, c j • A ^ (j : ℕ)) b a ≠ 0) :
129     ∃ j : Fin (d + 1), P.block (A ^ (j : ℕ)) b a ≠ 0 := by
130   classical
131   by_contra hn
132   apply h
133   rw [block_sum]
134   apply Finset.sum_eq_zero
135   intro j _
136   have hj : P.block (A ^ (j : ℕ)) b a = 0 := by
137     by_contra hj
138     exact hn ⟨j, hj⟩
139   rw [block_smul, hj, smul_zero]
140 
141 /-- A useful compiler certificate obtained by composing polynomial and path support. -/
142 theorem polynomial_zero_of_no_paths (d : ℕ) (c : Fin (d + 1) → K) (A : R) (b a : I)
143     (h : ∀ j : Fin (d + 1), ¬ TransferPath P A (j : ℕ) b a) :
144     P.block (∑ j, c j • A ^ (j : ℕ)) b a = 0 := by
145   classical
146   by_contra hn
147   obtain ⟨j, hj⟩ := polynomial_support_inclusion P d c A b a hn
148   exact h j (power_support_inclusion P A (j : ℕ) b a hj)
149 end Polynomial
150 
151 end KomorebiPaperVIII
152 
153 #print axioms KomorebiPaperVIII.power_path_expansion
154 #print axioms KomorebiPaperVIII.active_path_sum_zero
155 #print axioms KomorebiPaperVIII.power_block_zero_of_no_path
156 #print axioms KomorebiPaperVIII.power_support_inclusion
157 #print axioms KomorebiPaperVIII.nilpotent_of_path_bound
158 #print axioms KomorebiPaperVIII.path_level_bound
159 #print axioms KomorebiPaperVIII.nilpotent_of_topological_levels
160 #print axioms KomorebiPaperVIII.block_smul
161 #print axioms KomorebiPaperVIII.polynomial_support_inclusion
162 #print axioms KomorebiPaperVIII.polynomial_zero_of_no_paths

Back to source controls