source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIII.EdgeOperators
7 
8 /-!
9 # Finite endpoint and heterogeneous path expansions
10 
11 This module strengthens the finite scalar edge model with the endpoint block
12 carried by a composable word, its coefficient-level walk expansion, and the
13 corresponding reachability obstructions.  It also gives a finite heterogeneous
14 matrix-factor expansion: the factors may vary from step to step, while their
15 packet index type remains fixed.
16 -/
17 
18 set_option autoImplicit false
19 
20 namespace Komorebi.PaperIII.EdgeOperators
21 
22 open scoped BigOperators Matrix
23 
24 universe u v w
25 
26 namespace PacketGraph
27 
28 variable {V : Type u} {E : Type v} {R : Type w}
29 
30 /-- Two scalar packet blocks with a matched intermediate packet collapse. -/
31 theorem packetMatrix_mul_packetMatrix
32     [Fintype V] [DecidableEq V] [Semiring R]
33     (source middle target : V) (leftCoefficient rightCoefficient : R) :
34     packetMatrix middle target leftCoefficient *
35         packetMatrix source middle rightCoefficient =
36       packetMatrix source target (leftCoefficient * rightCoefficient) := by
37   ext row column
38   by_cases hrow : row = target
39   · by_cases hcolumn : column = source
40     · simp [packetMatrix, Matrix.mul_apply, hrow, hcolumn]
41     · simp [packetMatrix, Matrix.mul_apply, hrow, hcolumn]
42   · simp [packetMatrix, Matrix.mul_apply, hrow]
43 
44 namespace EdgeSystem
45 
46 variable (G : PacketGraph V E) (S : EdgeSystem G R)
47 
48 /-- Coefficients multiplied in operator order, hence reverse execution order. -/
49 def reverseCoefficient [One R] [Mul R] : List E → R
50   | [] => 1
51   | e :: rest => reverseCoefficient rest * S.coefficient e
52 
53 /-- The target of the final edge in the nonempty word `first :: rest`. -/
54 def terminalTarget (first : E) : List E → V
55   | [] => G.target first
56   | next :: rest => terminalTarget next rest
57 
58 /-- A word, including the empty word, connects the specified endpoints. -/
59 def Connects (source target : V) : List E → Prop
60   | [] => source = target
61   | first :: rest =>
62       source = G.source first ∧
63         target = terminalTarget G first rest ∧
64           Composable G (first :: rest)
65 
66 /-- Endpoint connectivity is used only to filter finite sums in this module. -/
67 noncomputable instance instDecidableConnects
68     (source target : V) (word : List E) : Decidable (Connects G source target word) :=
69   Classical.propDecidable _
70 
71 /--
72 A nonempty composable word is one endpoint-supported packet block.  Its scalar
73 is the reverse-order product dictated by right-to-left operator composition.
74 -/
75 theorem wordOp_eq_packetMatrix_of_composable
76     [Fintype V] [DecidableEq V] [Semiring R]
77     (first : E) (rest : List E) (h : Composable G (first :: rest)) :
78     wordOp G S (first :: rest) =
79       packetMatrix (G.source first) (terminalTarget G first rest)
80         (reverseCoefficient G S (first :: rest)) := by
81   induction rest generalizing first with
82   | nil =>
83       simp [wordOp, edgeOp, terminalTarget, reverseCoefficient]
84   | cons next tail ih =>
85       change G.target first = G.source next ∧
86         Composable G (next :: tail) at h
87       rcases h with ⟨hmatch, htail⟩
88       change wordOp G S (next :: tail) * edgeOp G S first = _
89       rw [ih next htail]
90       simp only [terminalTarget, reverseCoefficient]
91       unfold edgeOp
92       rw [← hmatch]
93       exact packetMatrix_mul_packetMatrix
94         (G.source first) (G.target first) (terminalTarget G next tail)
95         (reverseCoefficient G S (next :: tail)) (S.coefficient first)
96 
97 /-- The endpoint entry of one word is its coefficient exactly when it connects. -/
98 theorem wordOp_apply_eq_if_connects
99     [Fintype V] [DecidableEq V] [Semiring R]
100     (word : List E) (source target : V) :
101     wordOp G S word target source =
102       if Connects G source target word then reverseCoefficient G S word else 0 := by
103   cases word with
104   | nil =>
105       by_cases h : source = target
106       · subst target
107         simp [wordOp, Connects, reverseCoefficient]
108       · have hreverse : target ≠ source := fun h' => h h'.symm
109         simp [wordOp, Connects, h, hreverse]
110   | cons first rest =>
111       by_cases hwalk : Composable G (first :: rest)
112       · rw [wordOp_eq_packetMatrix_of_composable G S first rest hwalk]
113         simp [packetMatrix, Connects, hwalk, and_comm]
114       · rw [wordOp_eq_zero_of_not_composable G S (first :: rest) hwalk]
115         simp [Connects, hwalk]
116 
117 /-- The finite scalar sum over length-`n` walks with fixed endpoints. -/
118 noncomputable def endpointWalkCoefficientSum
119     [Fintype E] [Semiring R]
120     (n : ℕ) (source target : V) : R := by
121   classical
122   exact ∑ word : Fin n → E,
123     if Connects G source target (List.ofFn word) then
124       reverseCoefficient G S (List.ofFn word)
125     else 0
126 
127 /-- Every transfer-power entry is the coefficient sum over its endpoint walks. -/
128 theorem transferOp_pow_apply_eq_sum_walks
129     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
130     (n : ℕ) (source target : V) :
131     (transferOp G S ^ n) target source =
132       endpointWalkCoefficientSum G S n source target := by
133   classical
134   rw [transferOp_pow_eq_explicitWordExpansion G S n]
135   unfold explicitWordExpansion endpointWalkCoefficientSum tupleWordOp
136   rw [Matrix.sum_apply]
137   apply Finset.sum_congr rfl
138   intro word _
139   exact wordOp_apply_eq_if_connects G S (List.ofFn word) source target
140 
141 /-- Absence of a fixed-length endpoint walk forces the corresponding entry to vanish. -/
142 theorem transferOp_pow_apply_eq_zero_of_no_walk
143     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
144     (n : ℕ) (source target : V)
145     (h : ∀ word : Fin n → E,
146       ¬ Connects G source target (List.ofFn word)) :
147     (transferOp G S ^ n) target source = 0 := by
148   rw [transferOp_pow_apply_eq_sum_walks G S n source target]
149   classical
150   simp [endpointWalkCoefficientSum, h]
151 
152 /-- Directed reachability, with the empty path witnessing reflexivity. -/
153 def Reachable (source target : V) : Prop :=
154   ∃ word : List E, Connects G source target word
155 
156 /-- An unreachable endpoint has zero coefficient in every finite transfer power. -/
157 theorem transferOp_pow_apply_eq_zero_of_not_reachable
158     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
159     (n : ℕ) (source target : V) (h : ¬ Reachable G source target) :
160     (transferOp G S ^ n) target source = 0 := by
161   apply transferOp_pow_apply_eq_zero_of_no_walk G S n source target
162   intro word hword
163   exact h ⟨List.ofFn word, hword⟩
164 
165 /--
166 If a seed is supported on vertices from which `target` is unreachable, every
167 finite transfer-power orbit vector has zero `target` coordinate.
168 -/
169 theorem transferOp_pow_mulVec_apply_eq_zero_of_unreachable_support
170     [Fintype E] [Fintype V] [DecidableEq V] [Semiring R]
171     (n : ℕ) (x : V → R) (support : Set V) (target : V)
172     (hx : ∀ source, source ∉ support → x source = 0)
173     (hunreachable : ∀ source, source ∈ support → ¬ Reachable G source target) :
174     ((transferOp G S ^ n) *ᵥ x) target = 0 := by
175   rw [Matrix.mulVec_apply_eq_sum]
176   apply Finset.sum_eq_zero
177   intro source _
178   by_cases hsource : source ∈ support
179   · rw [transferOp_pow_apply_eq_zero_of_not_reachable G S n source target
180       (hunreachable source hsource)]
181     simp
182   · rw [hx source hsource]
183     simp
184 
185 end EdgeSystem
186 end PacketGraph
187 
188 section Heterogeneous
189 
190 variable {V : Type u} {R : Type w}
191 
192 universe u0 u1 u2 u3
193 
194 /-- The fully typed two-step expansion, allowing three different packet types. -/
195 theorem heterogeneousPacketPathExpansion_two
196     {I0 : Type u0} {I1 : Type u1} {I2 : Type u2}
197     [Fintype I1] [NonUnitalNonAssocSemiring R]
198     (first : Matrix I1 I0 R) (second : Matrix I2 I1 R)
199     (source : I0) (target : I2) :
200     (second * first) target source =
201       ∑ middle : I1, second target middle * first middle source := by
202   rw [Matrix.mul_apply]
203 
204 /-- The fully typed three-step expansion, allowing four different packet types. -/
205 theorem heterogeneousPacketPathExpansion_three
206     {I0 : Type u0} {I1 : Type u1} {I2 : Type u2} {I3 : Type u3}
207     [Fintype I1] [Fintype I2] [Semiring R]
208     (first : Matrix I1 I0 R) (second : Matrix I2 I1 R)
209     (third : Matrix I3 I2 R) (source : I0) (target : I3) :
210     ((third * second) * first) target source =
211       ∑ middle2 : I2, ∑ middle1 : I1,
212         (third target middle2 * second middle2 middle1) * first middle1 source := by
213   rw [Matrix.mul_apply]
214   simp_rw [Matrix.mul_apply, Finset.sum_mul]
215   rw [Finset.sum_comm]
216 
217 /--
218 Compose a finite sequence of possibly different packet matrices in execution
219 order.  The head acts first and therefore appears on the right.
220 -/
221 def heterogeneousProduct
222     [Fintype V] [DecidableEq V] [Semiring R] :
223     List (Matrix V V R) → Matrix V V R
224   | [] => 1
225   | step :: rest => heterogeneousProduct rest * step
226 
227 /--
228 The scalar path sum for a heterogeneous sequence of packet matrices.  Each
229 successive intermediate packet is summed independently.
230 -/
231 def heterogeneousPathSum
232     [Fintype V] [DecidableEq V] [Semiring R] :
233     List (Matrix V V R) → V → V → R
234   | [], source, target => if target = source then 1 else 0
235   | step :: rest, source, target =>
236       ∑ middle : V, heterogeneousPathSum rest middle target * step middle source
237 
238 /--
239 Finite heterogeneous packet-path expansion for a common finite packet index
240 type.  Unlike a matrix power, the factor at every step may be different.
241 -/
242 theorem heterogeneousPacketPathExpansion
243     [Fintype V] [DecidableEq V] [Semiring R]
244     (steps : List (Matrix V V R)) (source target : V) :
245     heterogeneousProduct steps target source =
246       heterogeneousPathSum steps source target := by
247   induction steps generalizing source target with
248   | nil =>
249       by_cases h : source = target
250       · subst target
251         simp [heterogeneousProduct, heterogeneousPathSum]
252       · have hreverse : target ≠ source := fun h' => h h'.symm
253         simp [heterogeneousProduct, heterogeneousPathSum, hreverse]
254   | cons step rest ih =>
255       simp [heterogeneousProduct, heterogeneousPathSum, Matrix.mul_apply, ih]
256 
257 /-- A matrix step together with its declared directed packet support. -/
258 structure SupportedStep
259     [Zero R] where
260   operator : Matrix V V R
261   relation : V → V → Prop
262   supported : ∀ source target, ¬ relation source target → operator target source = 0
263 
264 /-- A path compatible with each declared support relation, including the empty path. -/
265 def SupportedPath
266     [Zero R] :
267     List (SupportedStep (V := V) (R := R)) → V → V → Prop
268   | [], source, target => source = target
269   | step :: rest, source, target =>
270       ∃ middle, step.relation source middle ∧ SupportedPath rest middle target
271 
272 /-- With no compatible declared packet path, the heterogeneous path sum is zero. -/
273 theorem heterogeneousPathSum_eq_zero_of_no_supportedPath
274     [Fintype V] [DecidableEq V] [Semiring R]
275     (steps : List (SupportedStep (V := V) (R := R))) (source target : V)
276     (h : ¬ SupportedPath steps source target) :
277     heterogeneousPathSum (steps.map SupportedStep.operator) source target = 0 := by
278   induction steps generalizing source target with
279   | nil =>
280       have hreverse : target ≠ source := fun h' => h h'.symm
281       simp [heterogeneousPathSum, hreverse]
282   | cons step rest ih =>
283       simp only [List.map_cons, heterogeneousPathSum]
284       apply Finset.sum_eq_zero
285       intro middle _
286       by_cases hedge : step.relation source middle
287       · have hrest : ¬ SupportedPath rest middle target := by
288           intro hpath
289           exact h ⟨middle, hedge, hpath⟩
290         rw [ih middle target hrest]
291         simp
292       · rw [step.supported source middle hedge]
293         simp
294 
295 /-- The supported specialization of the heterogeneous packet-path expansion. -/
296 theorem supportedHeterogeneousPacketPathExpansion
297     [Fintype V] [DecidableEq V] [Semiring R]
298     (steps : List (SupportedStep (V := V) (R := R))) (source target : V) :
299     heterogeneousProduct (steps.map SupportedStep.operator) target source =
300       heterogeneousPathSum (steps.map SupportedStep.operator) source target :=
301   heterogeneousPacketPathExpansion _ source target
302 
303 /-- A heterogeneous supported product has zero endpoint entry without a compatible path. -/
304 theorem heterogeneousProduct_apply_eq_zero_of_no_supportedPath
305     [Fintype V] [DecidableEq V] [Semiring R]
306     (steps : List (SupportedStep (V := V) (R := R))) (source target : V)
307     (h : ¬ SupportedPath steps source target) :
308     heterogeneousProduct (steps.map SupportedStep.operator) target source = 0 := by
309   rw [supportedHeterogeneousPacketPathExpansion steps source target]
310   exact heterogeneousPathSum_eq_zero_of_no_supportedPath steps source target h
311 
312 end Heterogeneous
313 
314 end Komorebi.PaperIII.EdgeOperators

Back to source controls