source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Data.Matrix.Basic
7 
8 /-!
9 # Typed packet-supported edge operators
10 
11 An edge `e : E` is oriented from `source e` to `target e`.  Its elementary
12 packet operator has its only potentially nonzero matrix coefficient in row
13 `target e`, column `source e`.  Consequently matrix multiplication follows
14 execution order from right to left: `edgeOp f * edgeOp e` means first traverse
15 `e`, then traverse `f`.
16 -/
17 
18 set_option autoImplicit false
19 
20 namespace Komorebi.PaperIII.EdgeOperators
21 
22 open scoped BigOperators
23 
24 universe u v w
25 
26 /-- A finite directed multigraph; distinct edge values may have equal endpoints. -/
27 structure PacketGraph (V : Type u) (E : Type v) where
28   source : E → V
29   target : E → V
30 
31 namespace PacketGraph
32 
33 variable {V : Type u} {E : Type v} {R : Type w}
34 
35 /-- The matrix unit supported from packet `source` to packet `target`. -/
36 def packetMatrix [Zero R] [DecidableEq V]
37     (source target : V) (coefficient : R) : Matrix V V R :=
38   fun row column ↦ if row = target ∧ column = source then coefficient else 0
39 
40 @[simp] theorem packetMatrix_apply [Zero R] [DecidableEq V]
41     (source target row column : V) (coefficient : R) :
42     packetMatrix source target coefficient row column =
43       if row = target ∧ column = source then coefficient else 0 :=
44   rfl
45 
46 /-- An edge coefficient system on a packet graph. -/
47 structure EdgeSystem (G : PacketGraph V E) (R : Type w) where
48   coefficient : E → R
49 
50 namespace EdgeSystem
51 
52 variable (G : PacketGraph V E) (S : EdgeSystem G R)
53 
54 /-- The elementary operator carried by one directed edge. -/
55 def edgeOp [Zero R] [DecidableEq V] (e : E) : Matrix V V R :=
56   packetMatrix (G.source e) (G.target e) (S.coefficient e)
57 
58 @[simp] theorem edgeOp_apply [Zero R] [DecidableEq V]
59     (e : E) (row column : V) :
60     edgeOp G S e row column =
61       if row = G.target e ∧ column = G.source e then S.coefficient e else 0 :=
62   rfl
63 
64 /-- Edge operators are supported only on their declared target-source block. -/
65 theorem edgeOp_eq_zero_off_support [Zero R] [DecidableEq V]
66     (e : E) (row column : V)
67     (h : ¬ (row = G.target e ∧ column = G.source e)) :
68     edgeOp G S e row column = 0 := by
69   simp [edgeOp, packetMatrix, h]
70 
71 /--
72 Noncomposable edge products vanish.  In `edgeOp f * edgeOp e`, `e` acts first;
73 the product is zero when the target of `e` is not the source of `f`.
74 -/
75 theorem edgeOp_mul_edgeOp_eq_zero
76     [Fintype V] [DecidableEq V] [Semiring R]
77     (e f : E) (h : G.target e ≠ G.source f) :
78     edgeOp G S f * edgeOp G S e = 0 := by
79   ext row column
80   rw [Matrix.mul_apply]
81   apply Finset.sum_eq_zero
82   intro middle _
83   by_cases htarget : middle = G.target e
84   · subst middle
85     simp [edgeOp, packetMatrix, h]
86   · simp [edgeOp, packetMatrix, htarget]
87 
88 /--
89 A composable two-edge word collapses to the endpoint block, with coefficients
90 multiplied in operator order.
91 -/
92 theorem edgeOp_mul_edgeOp_of_composable
93     [Fintype V] [DecidableEq V] [Semiring R]
94     (e f : E) (h : G.target e = G.source f) :
95     edgeOp G S f * edgeOp G S e =
96       packetMatrix (G.source e) (G.target f)
97         (S.coefficient f * S.coefficient e) := by
98   ext row column
99   by_cases hrow : row = G.target f
100   · by_cases hcolumn : column = G.source e
101     · simp [edgeOp, packetMatrix, Matrix.mul_apply, h, hrow, hcolumn]
102     · simp [edgeOp, packetMatrix, Matrix.mul_apply, h, hcolumn]
103   · simp [edgeOp, packetMatrix, Matrix.mul_apply, hrow]
104 
105 /-- A list is composable in its written, left-to-right execution order. -/
106 def Composable (G : PacketGraph V E) : List E → Prop
107   | [] => True
108   | [_] => True
109   | e :: f :: rest => G.target e = G.source f ∧ Composable G (f :: rest)
110 
111 /-- Evaluate a word in execution order; the first listed edge acts first. -/
112 def wordOp [Fintype V] [DecidableEq V] [Semiring R]
113     (G : PacketGraph V E) (S : EdgeSystem G R) : List E → Matrix V V R
114   | [] => 1
115   | e :: rest => wordOp G S rest * edgeOp G S e
116 
117 @[simp] theorem wordOp_nil [Fintype V] [DecidableEq V] [Semiring R] :
118     wordOp G S [] = 1 :=
119   rfl
120 
121 @[simp] theorem wordOp_singleton [Fintype V] [DecidableEq V] [Semiring R]
122     (e : E) : wordOp G S [e] = edgeOp G S e := by
123   simp [wordOp]
124 
125 /-- Concatenating execution words reverses at the level of operator products. -/
126 theorem wordOp_append [Fintype V] [DecidableEq V] [Semiring R]
127     (first second : List E) :
128     wordOp G S (first ++ second) = wordOp G S second * wordOp G S first := by
129   induction first with
130   | nil => simp
131   | cons e rest ih =>
132       simp [wordOp, ih, Matrix.mul_assoc]
133 
134 /-- Prefixing a noncomposable edge pair makes the entire word operator zero. -/
135 theorem wordOp_eq_zero_of_first_break
136     [Fintype V] [DecidableEq V] [Semiring R]
137     (e f : E) (rest : List E) (h : G.target e ≠ G.source f) :
138     wordOp G S (e :: f :: rest) = 0 := by
139   change (wordOp G S rest * edgeOp G S f) * edgeOp G S e = 0
140   rw [Matrix.mul_assoc, edgeOp_mul_edgeOp_eq_zero G S e f h]
141   simp
142 
143 /-- Every noncomposable edge word evaluates to the zero packet operator. -/
144 theorem wordOp_eq_zero_of_not_composable
145     [Fintype V] [DecidableEq V] [Semiring R]
146     (word : List E) (h : ¬ Composable G word) :
147     wordOp G S word = 0 := by
148   induction word with
149   | nil => simp [Composable] at h
150   | cons e rest ih =>
151       cases rest with
152       | nil => simp [Composable] at h
153       | cons f tail =>
154           simp only [Composable, not_and_or] at h
155           rcases h with hbreak | htail
156           · exact wordOp_eq_zero_of_first_break G S e f tail hbreak
157           · change wordOp G S (f :: tail) * edgeOp G S e = 0
158             rw [ih htail]
159             simp
160 
161 /-- The transfer operator is the finite sum of all elementary edge operators. -/
162 def transferOp [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
163     (G : PacketGraph V E) (S : EdgeSystem G R) : Matrix V V R :=
164   ∑ e : E, edgeOp G S e
165 
166 /--
167 Recursive finite expansion of length-`n` edge words.  Each successor step
168 chooses the next (left-multiplying) edge after the already executed word.
169 -/
170 def wordExpansion [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
171     (G : PacketGraph V E) (S : EdgeSystem G R) :
172     ℕ → Matrix V V R
173   | 0 => 1
174   | n + 1 => transferOp G S * wordExpansion G S n
175 
176 /-- Evaluate a finite edge tuple as its left-to-right execution word. -/
177 def tupleWordOp [Fintype V] [DecidableEq V] [Semiring R]
178     (n : ℕ) (word : Fin n → E) : Matrix V V R :=
179   wordOp G S (List.ofFn word)
180 
181 /-- An actual finite sum over every edge word of length `n`. -/
182 def explicitWordExpansion [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
183     (n : ℕ) : Matrix V V R :=
184   ∑ word : Fin n → E, tupleWordOp G S n word
185 
186 /--
187 The finite word sum with every non-walk term removed.  `Composable` is exactly
188 the adjacent endpoint condition, so these are the typed graph walks.
189 -/
190 noncomputable def walkExpansion
191     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
192     (G : PacketGraph V E) (S : EdgeSystem G R) (n : ℕ) : Matrix V V R := by
193   classical
194   exact ∑ word : Fin n → E,
195     if Composable G (List.ofFn word) then tupleWordOp G S n word else 0
196 
197 /-- Appending one final edge left-multiplies the operator of the prefix. -/
198 theorem tupleWordOp_snoc
199     [Fintype V] [DecidableEq V] [Semiring R]
200     (n : ℕ) (final : E) (prior : Fin n → E) :
201     tupleWordOp G S (n + 1) (Fin.snoc prior final) =
202       edgeOp G S final * tupleWordOp G S n prior := by
203   unfold tupleWordOp
204   rw [List.ofFn_succ']
205   simp only [Fin.snoc_castSucc, Fin.snoc_last]
206   rw [List.concat_eq_append, wordOp_append]
207   simp
208 
209 /-- The explicit tuple sum grows by appending one final edge. -/
210 theorem explicitWordExpansion_succ
211     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
212     (n : ℕ) :
213     explicitWordExpansion G S (n + 1) =
214       transferOp G S * explicitWordExpansion G S n := by
215   unfold explicitWordExpansion
216   rw [← (Fin.snocEquiv (fun _ : Fin (n + 1) ↦ E)).sum_comp]
217   rw [Fintype.sum_prod_type]
218   change (∑ final : E, ∑ prior : Fin n → E,
219     tupleWordOp G S (n + 1) (Fin.snoc prior final)) = _
220   simp only [tupleWordOp_snoc]
221   unfold transferOp
222   rw [Finset.sum_mul]
223   simp_rw [Finset.mul_sum]
224 
225 /-- The recursive word expansion is exactly the explicit finite tuple sum. -/
226 theorem wordExpansion_eq_explicitWordExpansion
227     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
228     (n : ℕ) :
229     wordExpansion G S n = explicitWordExpansion G S n := by
230   induction n with
231   | zero =>
232       simp [wordExpansion, explicitWordExpansion, tupleWordOp]
233   | succ n ih =>
234       rw [wordExpansion, ih, explicitWordExpansion_succ G S n]
235 
236 /-- Removing noncomposable words does not change the finite operator sum. -/
237 theorem explicitWordExpansion_eq_walkExpansion
238     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
239     (n : ℕ) :
240     explicitWordExpansion G S n = walkExpansion G S n := by
241   classical
242   unfold explicitWordExpansion walkExpansion
243   apply Finset.sum_congr rfl
244   intro word _
245   by_cases hwalk : Composable G (List.ofFn word)
246   · simp [hwalk]
247   · have hzero : tupleWordOp G S n word = 0 :=
248       wordOp_eq_zero_of_not_composable G S (List.ofFn word) hwalk
249     simp [hwalk, hzero]
250 
251 /-- Every finite transfer power equals the recursively enumerated word expansion. -/
252 theorem transferOp_pow_eq_wordExpansion
253     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
254     (n : ℕ) :
255     transferOp G S ^ n = wordExpansion G S n := by
256   induction n with
257   | zero => rfl
258   | succ n ih =>
259       rw [pow_succ', ih]
260       rfl
261 
262 /-- Finite walk expansion: a transfer power is the sum of all length-`n` words. -/
263 theorem transferOp_pow_eq_explicitWordExpansion
264     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
265     (n : ℕ) :
266     transferOp G S ^ n = explicitWordExpansion G S n := by
267   rw [transferOp_pow_eq_wordExpansion G S n,
268     wordExpansion_eq_explicitWordExpansion G S n]
269 
270 /--
271 Finite walk expansion: `T^n` is exactly the sum over composable typed edge
272 words of length `n`; every non-walk word has vanished by packet support.
273 -/
274 theorem transferOp_pow_eq_walkExpansion
275     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
276     (n : ℕ) :
277     transferOp G S ^ n = walkExpansion G S n := by
278   rw [transferOp_pow_eq_explicitWordExpansion G S n,
279     explicitWordExpansion_eq_walkExpansion G S n]
280 
281 end EdgeSystem
282 end PacketGraph
283 end Komorebi.PaperIII.EdgeOperators

Back to source controls