TransferZeta.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Algebra.Polynomial.Basic
7 import Mathlib.Algebra.Polynomial.Coeff
8 import Mathlib.Data.Finset.NatAntidiagonal
9 import Mathlib.Data.Fintype.Card
10 import Mathlib.Data.List.OfFn
11 import Mathlib.Data.Matrix.Basic
12 import Mathlib.LinearAlgebra.Matrix.Adjugate
13 import Mathlib.RingTheory.PowerSeries.Basic
14 import Mathlib.RingTheory.PowerSeries.Inverse
15 
16 /-!
17 # Finite weighted transfer walks and certificate-checked zeta series
18 
19 This file formalizes the finite combinatorial part of the transfer-zeta
20 construction.  A finite edge type represents a directed multigraph: distinct
21 edges may have the same source and target, so parallel edges are counted with
22 their full multiplicity.  Every edge has strictly positive natural weight.
23 
24 The coefficient algorithm is genuinely finite.  At weight `n` it enumerates
25 tuples of at most `n` edges, filters by endpoints and exact total weight, and
26 counts the survivors.  Positivity proves that this bound loses no walk.
27 
28 The finite transfer matrix also gives a certificate-free rational series.
29 Writing `T = I - A`, Lean constructs `Q = det T` and `H = adjugate T`, proves
30 `T H = Q I`, proves `Q(0) = 1`, and therefore constructs the inverse of `Q` in
31 the formal power-series ring.  The older coefficient-level certificate API is
32 retained below for compatibility with the enumerated `pathZeta` series.
33 -/
34 
35 set_option autoImplicit false
36 
37 namespace Komorebi.PaperII.TransferZeta
38 
39 open scoped BigOperators
40 
41 universe u v
42 
43 /--
44 A finite directed multigraph with positive integral edge weights.
45 
46 Parallel edges are represented by distinct elements of `E`; consequently all
47 enumerations below retain their multiplicities without a separate multiplicity
48 field.
49 -/
50 structure PositiveWeightedMultigraph (V : Type u) (E : Type v) where
51   source : E → V
52   target : E → V
53   weight : E → ℕ
54   weight_pos : ∀ e, 0 < weight e
55 
56 namespace PositiveWeightedMultigraph
57 
58 variable {V : Type u} {E : Type v}
59 
60 /-- The recursive endpoint condition for an ordered list of edges. -/
61 def IsWalk (G : PositiveWeightedMultigraph V E) (s t : V) : List E → Prop
62   | [] => s = t
63   | e :: es => G.source e = s ∧ G.IsWalk (G.target e) t es
64 
65 /-- Endpoint validity is decidable on every finite edge tuple. -/
66 instance instDecidableIsWalk [DecidableEq V]
67     (G : PositiveWeightedMultigraph V E) (s t : V) (es : List E) :
68     Decidable (G.IsWalk s t es) := by
69   induction es generalizing s with
70   | nil =>
71       change Decidable (s = t)
72       infer_instance
73   | cons e es ih =>
74       change Decidable (G.source e = s ∧ G.IsWalk (G.target e) t es)
75       exact instDecidableAnd
76 
77 /-- Total weight of an ordered edge list. -/
78 def pathWeight (G : PositiveWeightedMultigraph V E) (es : List E) : ℕ :=
79   (es.map G.weight).sum
80 
81 @[simp] theorem pathWeight_nil (G : PositiveWeightedMultigraph V E) :
82     G.pathWeight [] = 0 :=
83   rfl
84 
85 @[simp] theorem pathWeight_cons (G : PositiveWeightedMultigraph V E)
86     (e : E) (es : List E) :
87     G.pathWeight (e :: es) = G.weight e + G.pathWeight es :=
88   rfl
89 
90 /-- Positive edge weights bound the number of edges by cumulative weight. -/
91 theorem length_le_pathWeight (G : PositiveWeightedMultigraph V E) (es : List E) :
92     es.length ≤ G.pathWeight es := by
93   induction es with
94   | nil => simp
95   | cons e es ih =>
96       calc
97         (e :: es).length = 1 + es.length := by simp [Nat.add_comm]
98         _ ≤ G.weight e + G.pathWeight es :=
99           Nat.add_le_add (G.weight_pos e) ih
100         _ = G.pathWeight (e :: es) := by simp
101 
102 /-- A tuple carrying its length, with no a priori length bound. -/
103 abbrev EdgeTuple (E : Type v) := Σ r : ℕ, Fin r → E
104 
105 /-- A tuple whose length is at most `n`. -/
106 abbrev BoundedEdgeTuple (E : Type v) (n : ℕ) :=
107   Σ r : Fin (n + 1), Fin r.val → E
108 
109 /-- Convert a bounded tuple to its ordered edge list. -/
110 def tupleEdges {n : ℕ} (x : BoundedEdgeTuple E n) : List E :=
111   List.ofFn x.2
112 
113 /--
114 The exact finite enumeration used for the coefficient of weight `n`.
115 -/
116 def walkTuplesAtWeight [Fintype E] [DecidableEq E] [DecidableEq V]
117     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :
118     Finset (BoundedEdgeTuple E n) :=
119   Finset.univ.filter fun x ↦
120     G.IsWalk s t (tupleEdges x) ∧ G.pathWeight (tupleEdges x) = n
121 
122 /-- Membership in the finite enumerator has exactly the advertised meaning. -/
123 theorem mem_walkTuplesAtWeight_iff [Fintype E] [DecidableEq E] [DecidableEq V]
124     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ)
125     (x : BoundedEdgeTuple E n) :
126     x ∈ G.walkTuplesAtWeight s t n ↔
127       G.IsWalk s t (tupleEdges x) ∧ G.pathWeight (tupleEdges x) = n := by
128   simp [walkTuplesAtWeight]
129 
130 /-- The finite type whose elements are precisely the exact-weight walk tuples. -/
131 abbrev ExactWalkTuple [Fintype E] [DecidableEq V]
132     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :=
133   {x : BoundedEdgeTuple E n //
134     G.IsWalk s t (tupleEdges x) ∧ G.pathWeight (tupleEdges x) = n}
135 
136 /--
137 Independent semantic presentation: an exact walk is simply a finite edge list
138 with the required endpoints and total weight.  It carries no enumeration bound
139 in its definition.
140 -/
141 abbrev ExactWalk (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :=
142   {es : List E // G.IsWalk s t es ∧ G.pathWeight es = n}
143 
144 /-- Executable coefficient algorithm: enumerate, filter, and count. -/
145 def coefficientAlgorithm [Fintype E] [DecidableEq E] [DecidableEq V]
146     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) : ℕ :=
147   (G.walkTuplesAtWeight s t n).card
148 
149 /-- The enumerator's cardinality is the cardinality of the exact semantic type. -/
150 theorem coefficientAlgorithm_correct [Fintype E] [DecidableEq E] [DecidableEq V]
151     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :
152     G.coefficientAlgorithm s t n = Fintype.card (G.ExactWalkTuple s t n) := by
153   rw [coefficientAlgorithm, walkTuplesAtWeight, Fintype.card_subtype]
154 
155 /--
156 Exact capture theorem for unrestricted finite tuples.  The forward direction
157 says every enumerated tuple is a walk of weight `n`; the reverse direction is
158 where positivity supplies the finite length bound.
159 -/
160 theorem tuple_captured_iff [Fintype E] [DecidableEq E] [DecidableEq V]
161     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ)
162     (x : EdgeTuple E) :
163     (∃ y : BoundedEdgeTuple E n,
164         y ∈ G.walkTuplesAtWeight s t n ∧ tupleEdges y = List.ofFn x.2) ↔
165       G.IsWalk s t (List.ofFn x.2) ∧ G.pathWeight (List.ofFn x.2) = n := by
166   constructor
167   · rintro ⟨y, hy, hedge⟩
168     have hp := (G.mem_walkTuplesAtWeight_iff s t n y).mp hy
169     simpa [hedge] using hp
170   · intro hx
171     have hlength : x.1 ≤ n := by
172       calc
173         x.1 = (List.ofFn x.2).length := by simp
174         _ ≤ G.pathWeight (List.ofFn x.2) := G.length_le_pathWeight _
175         _ = n := hx.2
176     let y : BoundedEdgeTuple E n :=
177       ⟨⟨x.1, Nat.lt_succ_iff.mpr hlength⟩, x.2⟩
178     refine ⟨y, ?_, rfl⟩
179     exact (G.mem_walkTuplesAtWeight_iff s t n y).mpr (by simpa [y, tupleEdges] using hx)
180 
181 /-- Forget the bounded-tuple representation and recover its semantic edge list. -/
182 def exactWalkTupleToList [Fintype E] [DecidableEq V]
183     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ)
184     (x : G.ExactWalkTuple s t n) : G.ExactWalk s t n :=
185   ⟨tupleEdges x.1, x.2⟩
186 
187 /--
188 Positive weights turn a semantic exact walk back into a bounded tuple.  This is
189 the constructive content behind finiteness of the unrestricted list model.
190 -/
191 def exactWalkListToTuple [Fintype E] [DecidableEq V]
192     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ)
193     (x : G.ExactWalk s t n) : G.ExactWalkTuple s t n := by
194   have hlength : x.1.length ≤ n := by
195     calc
196       x.1.length ≤ G.pathWeight x.1 := G.length_le_pathWeight x.1
197       _ = n := x.2.2
198   let y : BoundedEdgeTuple E n :=
199     ⟨⟨x.1.length, Nat.lt_succ_iff.mpr hlength⟩, x.1.get⟩
200   refine ⟨y, ?_⟩
201   simpa [y, tupleEdges, List.ofFn_get] using x.2
202 
203 /-- Semantic lists survive the encode/decode round trip. -/
204 theorem exactWalkTupleToList_listToTuple [Fintype E] [DecidableEq V]
205     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ)
206     (x : G.ExactWalk s t n) :
207     G.exactWalkTupleToList s t n (G.exactWalkListToTuple s t n x) = x := by
208   apply Subtype.ext
209   simp [exactWalkTupleToList, exactWalkListToTuple, tupleEdges, List.ofFn_get]
210 
211 /-- Exact list-walks and exact bounded tuples are equivalent. -/
212 noncomputable def exactWalkEquiv [Fintype E] [DecidableEq V]
213     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :
214     G.ExactWalk s t n ≃ G.ExactWalkTuple s t n :=
215   (Equiv.ofBijective (G.exactWalkTupleToList s t n) ⟨by
216     intro x y hxy
217     apply Subtype.ext
218     rcases x with ⟨⟨⟨r, hr⟩, f⟩, hx⟩
219     rcases y with ⟨⟨⟨q, hq⟩, g⟩, hy⟩
220     have hlists : List.ofFn f = List.ofFn g := congrArg Subtype.val hxy
221     have htuples : (⟨r, f⟩ : EdgeTuple E) = ⟨q, g⟩ :=
222       List.equivSigmaTuple.symm.injective hlists
223     cases htuples
224     rfl, by
225     intro x
226     exact ⟨G.exactWalkListToTuple s t n x,
227       G.exactWalkTupleToList_listToTuple s t n x⟩⟩).symm
228 
229 /-- Positivity and the tuple equivalence make the unrestricted list model finite. -/
230 noncomputable instance instFintypeExactWalk [Fintype E] [DecidableEq V]
231     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :
232     Fintype (G.ExactWalk s t n) :=
233   Fintype.ofEquiv (G.ExactWalkTuple s t n) (G.exactWalkEquiv s t n).symm
234 
235 /-- The executable coefficient is the cardinality of the semantic list-walk type. -/
236 theorem coefficientAlgorithm_eq_card_exactWalk [Fintype E] [DecidableEq E] [DecidableEq V]
237     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :
238     G.coefficientAlgorithm s t n = Fintype.card (G.ExactWalk s t n) := by
239   rw [G.coefficientAlgorithm_correct s t n]
240   exact Fintype.card_congr (G.exactWalkEquiv s t n).symm
241 
242 /-- Data of the unique possible empty exact walk. -/
243 abbrev EmptyExactWalk (s t : V) (n : ℕ) :=
244   {_u : Unit // s = t ∧ n = 0}
245 
246 /--
247 Data obtained by removing the first edge of a nonempty exact walk.  The tail is
248 again an unrestricted list; the endpoint and weight equations are explicit.
249 -/
250 abbrev FirstEdgeExactWalk (G : PositiveWeightedMultigraph V E)
251     (s t : V) (n : ℕ) :=
252   {p : E × List E //
253     G.source p.1 = s ∧ G.IsWalk (G.target p.1) t p.2 ∧
254       G.weight p.1 + G.pathWeight p.2 = n}
255 
256 /--
257 Exact first-edge decomposition of semantic walks.  This is the combinatorial
258 source of the transfer recurrence: every walk is either the empty diagonal
259 walk, or a first edge followed by an exact tail, with no overlap.
260 -/
261 def exactWalkFirstEdgeEquiv (G : PositiveWeightedMultigraph V E)
262     (s t : V) (n : ℕ) :
263     G.ExactWalk s t n ≃ EmptyExactWalk s t n ⊕ G.FirstEdgeExactWalk s t n where
264   toFun x := by
265     rcases x with ⟨es, hes⟩
266     cases es with
267     | nil =>
268         exact Sum.inl ⟨(), hes.1, hes.2.symm⟩
269     | cons e es =>
270         exact Sum.inr ⟨(e, es), hes.1.1, hes.1.2, hes.2⟩
271   invFun x := by
272     rcases x with h | h
273     · exact ⟨[], ⟨h.2.1, h.2.2.symm⟩⟩
274     · exact ⟨h.1.1 :: h.1.2, ⟨⟨h.2.1, h.2.2.1⟩, h.2.2.2⟩⟩
275   left_inv x := by
276     rcases x with ⟨es, hes⟩
277     cases es <;> rfl
278   right_inv x := by
279     rcases x with h | h <;> rfl
280 
281 /-- First-edge data reindexed by the remaining weight. -/
282 abbrev FirstEdgeTail (G : PositiveWeightedMultigraph V E)
283     (s t : V) (n : ℕ) :=
284   Σ e : E, {_x : G.ExactWalk (G.target e) t (n - G.weight e) //
285     G.source e = s ∧ G.weight e ≤ n}
286 
287 /-- Reindex first-edge data by the exact remaining weight `n - weight e`. -/
288 def firstEdgeTailEquiv (G : PositiveWeightedMultigraph V E)
289     (s t : V) (n : ℕ) :
290     G.FirstEdgeExactWalk s t n ≃ G.FirstEdgeTail s t n where
291   toFun x := by
292     rcases x with ⟨⟨e, es⟩, hsource, hwalk, hweight⟩
293     have hle : G.weight e ≤ n := by
294       exact Nat.le.intro hweight
295     have hremaining : G.pathWeight es = n - G.weight e :=
296       Nat.eq_sub_of_add_eq (by simpa [Nat.add_comm] using hweight)
297     exact ⟨e, ⟨⟨es, hwalk, hremaining⟩, hsource, hle⟩⟩
298   invFun x := by
299     rcases x with ⟨e, ⟨⟨es, hwalk, hremaining⟩, hsource, hle⟩⟩
300     exact ⟨(e, es), hsource, hwalk, by
301       rw [hremaining]
302       exact Nat.add_sub_of_le hle⟩
303   left_inv x := by
304     rcases x with ⟨⟨e, es⟩, hsource, hwalk, hweight⟩
305     apply Subtype.ext
306     rfl
307   right_inv x := by
308     rcases x with ⟨e, ⟨⟨es, hwalk, hweight⟩, hsource, hle⟩⟩
309     apply Sigma.ext rfl
310     apply heq_of_eq
311     apply Subtype.ext
312     apply Subtype.ext
313     rfl
314 
315 /-- First-edge data is finite because the edge set and every exact tail are finite. -/
316 noncomputable instance instFintypeFirstEdgeExactWalk
317     [Fintype E] [DecidableEq V] (G : PositiveWeightedMultigraph V E)
318     (s t : V) (n : ℕ) : Fintype (G.FirstEdgeExactWalk s t n) :=
319   Fintype.ofEquiv (G.FirstEdgeTail s t n) (G.firstEdgeTailEquiv s t n).symm
320 
321 /-- Cardinality of the possible empty-walk contribution. -/
322 theorem card_emptyExactWalk [DecidableEq V] (s t : V) (n : ℕ) :
323     Fintype.card (EmptyExactWalk s t n) =
324       if s = t ∧ n = 0 then 1 else 0 := by
325   by_cases h : s = t ∧ n = 0 <;> simp [EmptyExactWalk, h]
326 
327 /-- Cardinality of first-edge data as a finite sum over edges. -/
328 theorem card_firstEdgeExactWalk [Fintype E] [DecidableEq V]
329     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :
330     Fintype.card (G.FirstEdgeExactWalk s t n) =
331       ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
332         Fintype.card (G.ExactWalk (G.target e) t (n - G.weight e)) else 0 := by
333   rw [Fintype.card_congr (G.firstEdgeTailEquiv s t n), Fintype.card_sigma]
334   apply Finset.sum_congr rfl
335   intro e _
336   by_cases h : G.source e = s ∧ G.weight e ≤ n <;> simp [h]
337 
338 /--
339 First-edge recurrence for the executable coefficients.  Unlike the old
340 rationality certificate, this is derived from the walk semantics and finite
341 edge data rather than assumed coefficientwise.
342 -/
343 theorem coefficientAlgorithm_firstEdge [Fintype E] [DecidableEq E] [DecidableEq V]
344     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :
345     G.coefficientAlgorithm s t n =
346       (if s = t ∧ n = 0 then 1 else 0) +
347         ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
348           G.coefficientAlgorithm (G.target e) t (n - G.weight e) else 0 := by
349   rw [G.coefficientAlgorithm_eq_card_exactWalk s t n,
350     Fintype.card_congr (G.exactWalkFirstEdgeEquiv s t n), Fintype.card_sum,
351     card_emptyExactWalk, G.card_firstEdgeExactWalk]
352   congr 1
353   apply Finset.sum_congr rfl
354   intro e _
355   by_cases h : G.source e = s ∧ G.weight e ≤ n
356   · simp only [h]
357     exact (G.coefficientAlgorithm_eq_card_exactWalk
358       (G.target e) t (n - G.weight e)).symm
359   · simp [h]
360 
361 /-- Number of edges from `i` to `j` having exact weight `n`. -/
362 def edgeCoefficient [Fintype E] [DecidableEq E] [DecidableEq V]
363     (G : PositiveWeightedMultigraph V E) (i j : V) (n : ℕ) : ℕ :=
364   (Finset.univ.filter fun e ↦
365     G.source e = i ∧ G.target e = j ∧ G.weight e = n).card
366 
367 /-- Polynomial weighted adjacency matrix. -/
368 noncomputable def weightedAdjacency [Fintype E] [DecidableEq V]
369     (G : PositiveWeightedMultigraph V E) : Matrix V V (Polynomial ℤ) :=
370   fun i j ↦ ∑ e : E,
371     if G.source e = i ∧ G.target e = j then
372       Polynomial.monomial (G.weight e) 1
373     else 0
374 
375 /--
376 Coefficient correctness for the polynomial adjacency matrix.  Because edges
377 are elements of a multigraph edge type, the cardinality counts parallel edges.
378 -/
379 theorem weightedAdjacency_coeff [Fintype E] [DecidableEq E] [DecidableEq V]
380     (G : PositiveWeightedMultigraph V E) (i j : V) (n : ℕ) :
381     (G.weightedAdjacency i j).coeff n = (G.edgeCoefficient i j n : ℤ) := by
382   classical
383   rw [weightedAdjacency, ← Polynomial.lcoeff_apply]
384   rw [map_sum]
385   simp only [Polynomial.lcoeff_apply]
386   calc
387     (∑ e : E, (if G.source e = i ∧ G.target e = j then
388         Polynomial.monomial (G.weight e) 1 else 0 : Polynomial ℤ).coeff n) =
389         ∑ e : E, if G.source e = i ∧ G.target e = j ∧ G.weight e = n
390           then (1 : ℤ) else 0 := by
391       apply Fintype.sum_congr
392       intro e
393       by_cases he : G.source e = i ∧ G.target e = j
394       · simp [he, Polynomial.coeff_monomial]
395       · have hfull : ¬(G.source e = i ∧ G.target e = j ∧ G.weight e = n) :=
396           fun h ↦ he ⟨h.1, h.2.1⟩
397         simp [he, hfull]
398     _ = (G.edgeCoefficient i j n : ℤ) := by
399       simp [edgeCoefficient]
400 
401 /-- Positive weights make every adjacency entry have zero constant term. -/
402 theorem weightedAdjacency_coeff_zero [Fintype E] [DecidableEq E] [DecidableEq V]
403     (G : PositiveWeightedMultigraph V E) (i j : V) :
404     (G.weightedAdjacency i j).coeff 0 = 0 := by
405   rw [G.weightedAdjacency_coeff i j 0]
406   simp only [edgeCoefficient, Int.ofNat_eq_zero, Finset.card_eq_zero,
407     Finset.filter_eq_empty_iff]
408   intro e _ hs
409   rcases hs with ⟨_, _, hw⟩
410   exact (Nat.ne_of_gt (G.weight_pos e)) hw
411 
412 /-- Formal `pathZeta` series whose coefficients are the certified unrestricted walk counts. -/
413 def pathZeta [Fintype E] [DecidableEq E] [DecidableEq V]
414     (G : PositiveWeightedMultigraph V E) (s t : V) : PowerSeries ℤ :=
415   PowerSeries.mk fun n ↦ (G.coefficientAlgorithm s t n : ℤ)
416 
417 /-- Coefficients of the formal zeta series are exactly the finite algorithm. -/
418 @[simp] theorem coeff_pathZeta [Fintype E] [DecidableEq E] [DecidableEq V]
419     (G : PositiveWeightedMultigraph V E) (s t : V) (n : ℕ) :
420     PowerSeries.coeff n (G.pathZeta s t) = (G.coefficientAlgorithm s t n : ℤ) := by
421   simp [pathZeta]
422 
423 section FiniteTransferRationality
424 
425 variable [Fintype E] [DecidableEq E] [Fintype V] [DecidableEq V]
426   (G : PositiveWeightedMultigraph V E)
427 
428 /-- Polynomial weighted adjacency included entrywise into `ℤ⟦X⟧`. -/
429 noncomputable def weightedAdjacencySeries : Matrix V V (PowerSeries ℤ) :=
430   Polynomial.coeToPowerSeries.ringHom.mapMatrix G.weightedAdjacency
431 
432 /-- The independently enumerated walk series assembled into a matrix. -/
433 def enumeratedPathZetaMatrix : Matrix V V (PowerSeries ℤ) :=
434   fun s t ↦ G.pathZeta s t
435 
436 /-- Multiplication by adjacency is an explicit finite sum over first edges. -/
437 theorem weightedAdjacencySeries_mul_enumeratedPathZetaMatrix_apply
438     (s t : V) :
439     (G.weightedAdjacencySeries * G.enumeratedPathZetaMatrix) s t =
440       ∑ e : E, if G.source e = s then
441         PowerSeries.X ^ G.weight e * G.pathZeta (G.target e) t else 0 := by
442   classical
443   have hadjacency (i k : V) :
444       G.weightedAdjacencySeries i k =
445         ∑ e : E, if G.source e = i ∧ G.target e = k then
446           (PowerSeries.X : PowerSeries ℤ) ^ G.weight e else 0 := by
447     rw [weightedAdjacencySeries, RingHom.mapMatrix_apply, Matrix.map_apply,
448       weightedAdjacency, map_sum]
449     apply Finset.sum_congr rfl
450     intro e _
451     by_cases h : G.source e = i ∧ G.target e = k <;>
452       simp [h, ← PowerSeries.X_pow_eq]
453   rw [Matrix.mul_apply]
454   simp_rw [hadjacency, Finset.sum_mul]
455   rw [Finset.sum_comm]
456   apply Finset.sum_congr rfl
457   intro e _
458   by_cases hs : G.source e = s
459   · simp [hs, enumeratedPathZetaMatrix]
460   · simp [hs]
461 
462 /--
463 Coefficient of `A(X) Z(X)` as the finite first-edge tail sum.  The proof
464 expands the finite edge adjacency definition and uses monomial coefficient
465 extraction; it assumes no rationality identity.
466 -/
467 theorem coeff_weightedAdjacencySeries_mul_enumeratedPathZetaMatrix
468     (s t : V) (n : ℕ) :
469     PowerSeries.coeff n
470         ((G.weightedAdjacencySeries * G.enumeratedPathZetaMatrix) s t) =
471       ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
472         (G.coefficientAlgorithm (G.target e) t (n - G.weight e) : ℤ) else 0 := by
473   classical
474   rw [G.weightedAdjacencySeries_mul_enumeratedPathZetaMatrix_apply s t, map_sum]
475   apply Finset.sum_congr rfl
476   intro e _
477   by_cases hs : G.source e = s
478   · simp [hs, PowerSeries.coeff_X_pow_mul']
479   · simp [hs]
480 
481 /--
482 Series form of the semantic first-edge recurrence:
483 `Z_enum = I + A(X) Z_enum`.
484 -/
485 theorem enumeratedPathZetaMatrix_eq_one_add_adjacency_mul :
486     G.enumeratedPathZetaMatrix =
487       1 + G.weightedAdjacencySeries * G.enumeratedPathZetaMatrix := by
488   ext s t n
489   change PowerSeries.coeff n (G.pathZeta s t) =
490     PowerSeries.coeff n
491       ((1 : Matrix V V (PowerSeries ℤ)) s t +
492         (G.weightedAdjacencySeries * G.enumeratedPathZetaMatrix) s t)
493   rw [G.coeff_pathZeta, map_add,
494     G.coeff_weightedAdjacencySeries_mul_enumeratedPathZetaMatrix s t n]
495   have hrec := congrArg Int.ofNat (G.coefficientAlgorithm_firstEdge s t n)
496   by_cases hst : s = t
497   · subst t
498     by_cases hn : n = 0 <;>
499       simpa [Matrix.one_apply, PowerSeries.coeff_one, hn] using hrec
500   · simpa [Matrix.one_apply, PowerSeries.coeff_one, hst] using hrec
501 
502 /-- The polynomial transfer matrix `I - A(X)` attached to the finite graph. -/
503 noncomputable def transferMatrix : Matrix V V (Polynomial ℤ) :=
504   1 - G.weightedAdjacency
505 
506 /-- The canonical denominator obtained from the finite transfer matrix. -/
507 noncomputable def transferDenominator : Polynomial ℤ :=
508   Matrix.det G.transferMatrix
509 
510 /-- The canonical numerator matrix obtained by taking the adjugate. -/
511 noncomputable def transferNumeratorMatrix : Matrix V V (Polynomial ℤ) :=
512   Matrix.adjugate G.transferMatrix
513 
514 /-- Entrywise canonical numerator for a source and target. -/
515 noncomputable def transferNumerator (s t : V) : Polynomial ℤ :=
516   G.transferNumeratorMatrix s t
517 
518 omit [DecidableEq E] in
519 /--
520 The adjugate identity is a finite, automatically generated rationality
521 certificate.  It has no coefficientwise walk-series hypothesis.
522 -/
523 theorem transferMatrix_mul_numerator :
524     G.transferMatrix * G.transferNumeratorMatrix =
525       G.transferDenominator • (1 : Matrix V V (Polynomial ℤ)) := by
526   exact Matrix.mul_adjugate G.transferMatrix
527 
528 omit [DecidableEq E] in
529 /-- The companion adjugate identity, with the factors reversed. -/
530 theorem transferNumerator_mul_transferMatrix :
531     G.transferNumeratorMatrix * G.transferMatrix =
532       G.transferDenominator • (1 : Matrix V V (Polynomial ℤ)) := by
533   exact Matrix.adjugate_mul G.transferMatrix
534 
535 /-- Evaluation at zero sends the weighted adjacency matrix to zero. -/
536 theorem constantCoeff_weightedAdjacency :
537     Polynomial.constantCoeff.mapMatrix G.weightedAdjacency = 0 := by
538   ext i j
539   simp [RingHom.mapMatrix_apply, Matrix.map_apply,
540     Polynomial.constantCoeff_apply, G.weightedAdjacency_coeff_zero]
541 
542 /-- Consequently, evaluation at zero sends the transfer matrix to `I`. -/
543 theorem constantCoeff_transferMatrix :
544     Polynomial.constantCoeff.mapMatrix G.transferMatrix =
545       (1 : Matrix V V ℤ) := by
546   ext i j
547   by_cases hij : i = j <;>
548     simp [transferMatrix, RingHom.mapMatrix_apply, Matrix.map_apply,
549     Polynomial.constantCoeff_apply, G.weightedAdjacency_coeff_zero,
550     Matrix.one_apply, hij]
551 
552 /-- The determinant denominator is canonically normalized by `Q(0) = 1`. -/
553 theorem transferDenominator_coeff_zero :
554     G.transferDenominator.coeff 0 = 1 := by
555   change Polynomial.constantCoeff G.transferDenominator = 1
556   rw [transferDenominator, RingHom.map_det, G.constantCoeff_transferMatrix,
557     Matrix.det_one]
558 
559 /-- In particular, the automatically generated polynomial denominator is nonzero. -/
560 theorem transferDenominator_ne_zero : G.transferDenominator ≠ 0 := by
561   intro hzero
562   have h : (0 : ℤ) = 1 := by
563     simpa [hzero] using G.transferDenominator_coeff_zero
564   exact Int.zero_ne_one h
565 
566 /-- The canonical denominator becomes a unit in the formal power-series ring. -/
567 theorem transferDenominator_isUnit :
568     IsUnit (G.transferDenominator : PowerSeries ℤ) := by
569   rw [PowerSeries.isUnit_iff_constantCoeff, Polynomial.constantCoeff_coe,
570     G.transferDenominator_coeff_zero]
571   exact isUnit_one
572 
573 /-- Explicit inverse of the normalized determinant in `ℤ〖X〗`. -/
574 noncomputable def transferDenominatorInverse : PowerSeries ℤ :=
575   PowerSeries.invOfUnit (G.transferDenominator : PowerSeries ℤ) (1 : ℤˣ)
576 
577 /-- The constructed series is a right inverse of the determinant denominator. -/
578 theorem transferDenominator_mul_inverse :
579     (G.transferDenominator : PowerSeries ℤ) *
580         G.transferDenominatorInverse = 1 := by
581   apply PowerSeries.mul_invOfUnit
582   simpa [Polynomial.constantCoeff_coe] using G.transferDenominator_coeff_zero
583 
584 /-- The constructed series is also a left inverse. -/
585 theorem transferDenominator_inverse_mul :
586     G.transferDenominatorInverse *
587         (G.transferDenominator : PowerSeries ℤ) = 1 := by
588   apply PowerSeries.invOfUnit_mul
589   simpa [Polynomial.constantCoeff_coe] using G.transferDenominator_coeff_zero
590 
591 /--
592 The canonical rational transfer series for an entry: `Q⁻¹ Hₛₜ`.  Both
593 `Q` and `H` are computed from the finite polynomial adjacency matrix.
594 -/
595 noncomputable def matrixPathZeta (s t : V) : PowerSeries ℤ :=
596   G.transferDenominatorInverse * (G.transferNumerator s t : PowerSeries ℤ)
597 
598 /-- Transfer matrix after entrywise inclusion into formal power series. -/
599 noncomputable def transferSeriesMatrix : Matrix V V (PowerSeries ℤ) :=
600   Polynomial.coeToPowerSeries.ringHom.mapMatrix G.transferMatrix
601 
602 omit [DecidableEq E] in
603 /-- The series transfer matrix is literally `I - A(X)`. -/
604 theorem transferSeriesMatrix_eq_one_sub_adjacency :
605     G.transferSeriesMatrix = 1 - G.weightedAdjacencySeries := by
606   rw [transferSeriesMatrix, transferMatrix, weightedAdjacencySeries, map_sub, map_one]
607 
608 /-- The enumerated walk series solves `(I - A(X)) Z_enum = I`. -/
609 theorem transferSeriesMatrix_mul_enumeratedPathZetaMatrix :
610     G.transferSeriesMatrix * G.enumeratedPathZetaMatrix = 1 := by
611   rw [G.transferSeriesMatrix_eq_one_sub_adjacency, sub_mul, one_mul]
612   exact sub_eq_iff_eq_add.mpr G.enumeratedPathZetaMatrix_eq_one_add_adjacency_mul
613 
614 /-- All canonical rational entries assembled into one matrix. -/
615 noncomputable def matrixPathZetaMatrix : Matrix V V (PowerSeries ℤ) :=
616   fun s t ↦ G.matrixPathZeta s t
617 
618 omit [DecidableEq E] in
619 /-- The polynomial adjugate identity survives entrywise inclusion into `ℤ⟦X⟧`. -/
620 theorem transferSeriesMatrix_mul_adjugate :
621     G.transferSeriesMatrix *
622         Polynomial.coeToPowerSeries.ringHom.mapMatrix G.transferNumeratorMatrix =
623       (G.transferDenominator : PowerSeries ℤ) •
624         (1 : Matrix V V (PowerSeries ℤ)) := by
625   calc
626     _ = Polynomial.coeToPowerSeries.ringHom.mapMatrix
627         (G.transferDenominator • (1 : Matrix V V (Polynomial ℤ))) := by
628       simpa [transferSeriesMatrix] using congrArg
629         (Polynomial.coeToPowerSeries.ringHom.mapMatrix)
630         G.transferMatrix_mul_numerator
631     _ = _ := by
632       ext i j
633       by_cases hij : i = j <;>
634         simp [RingHom.mapMatrix_apply, Matrix.map_apply, hij]
635 
636 omit [DecidableEq E] in
637 /-- The reversed adjugate identity after inclusion into `ℤ⟦X⟧`. -/
638 theorem adjugate_mul_transferSeriesMatrix :
639     Polynomial.coeToPowerSeries.ringHom.mapMatrix G.transferNumeratorMatrix *
640         G.transferSeriesMatrix =
641       (G.transferDenominator : PowerSeries ℤ) •
642         (1 : Matrix V V (PowerSeries ℤ)) := by
643   calc
644     _ = Polynomial.coeToPowerSeries.ringHom.mapMatrix
645         (G.transferDenominator • (1 : Matrix V V (Polynomial ℤ))) := by
646       simpa [transferSeriesMatrix] using congrArg
647         (Polynomial.coeToPowerSeries.ringHom.mapMatrix)
648         G.transferNumerator_mul_transferMatrix
649     _ = _ := by
650       ext i j
651       by_cases hij : i = j <;>
652         simp [RingHom.mapMatrix_apply, Matrix.map_apply, hij]
653 
654 omit [DecidableEq E] in
655 /-- The canonical rational matrix is the scaled adjugate. -/
656 theorem matrixPathZetaMatrix_eq_scaled_adjugate :
657     G.matrixPathZetaMatrix =
658       G.transferDenominatorInverse •
659         Polynomial.coeToPowerSeries.ringHom.mapMatrix G.transferNumeratorMatrix := by
660   ext s t
661   rfl
662 
663 /--
664 The automatic series solves the finite first-step transfer equation
665 `(I - A(X)) Z(X) = I`.  This is the matrix form of the first-edge recurrence.
666 -/
667 theorem transferSeriesMatrix_mul_matrixPathZetaMatrix :
668     G.transferSeriesMatrix * G.matrixPathZetaMatrix = 1 := by
669   rw [G.matrixPathZetaMatrix_eq_scaled_adjugate, Matrix.mul_smul,
670     G.transferSeriesMatrix_mul_adjugate]
671   ext i j
672   by_cases hij : i = j <;>
673     simp [Matrix.one_apply, hij, G.transferDenominator_inverse_mul]
674 
675 /-- The canonical rational matrix is also a left inverse of the transfer matrix. -/
676 theorem matrixPathZetaMatrix_mul_transferSeriesMatrix :
677     G.matrixPathZetaMatrix * G.transferSeriesMatrix = 1 := by
678   rw [G.matrixPathZetaMatrix_eq_scaled_adjugate, Matrix.smul_mul,
679     G.adjugate_mul_transferSeriesMatrix]
680   ext i j
681   by_cases hij : i = j <;>
682     simp [Matrix.one_apply, hij, G.transferDenominator_inverse_mul]
683 
684 /--
685 Uniqueness of the transfer inverse identifies the independently enumerated
686 walk series with the determinant/adjugate construction.
687 -/
688 theorem enumeratedPathZetaMatrix_eq_matrixPathZetaMatrix :
689     G.enumeratedPathZetaMatrix = G.matrixPathZetaMatrix := by
690   calc
691     G.enumeratedPathZetaMatrix = 1 * G.enumeratedPathZetaMatrix :=
692       (Matrix.one_mul _).symm
693     _ = (G.matrixPathZetaMatrix * G.transferSeriesMatrix) *
694         G.enumeratedPathZetaMatrix := by
695       rw [G.matrixPathZetaMatrix_mul_transferSeriesMatrix]
696     _ = G.matrixPathZetaMatrix *
697         (G.transferSeriesMatrix * G.enumeratedPathZetaMatrix) :=
698       Matrix.mul_assoc _ _ _
699     _ = G.matrixPathZetaMatrix * 1 := by
700       rw [G.transferSeriesMatrix_mul_enumeratedPathZetaMatrix]
701     _ = G.matrixPathZetaMatrix := Matrix.mul_one _
702 
703 /-- Every enumerated `pathZeta` entry is the canonical finite-matrix entry. -/
704 theorem pathZeta_eq_matrixPathZeta (s t : V) :
705     G.pathZeta s t = G.matrixPathZeta s t := by
706   exact congrFun (congrFun G.enumeratedPathZetaMatrix_eq_matrixPathZetaMatrix s) t
707 
708 /-- Explicit formula `Zₛₜ = det(I-A)⁻¹ adj(I-A)ₛₜ` in `ℤ⟦X⟧`. -/
709 theorem pathZeta_eq_inverse_mul_transferNumerator (s t : V) :
710     G.pathZeta s t = G.transferDenominatorInverse *
711       (G.transferNumerator s t : PowerSeries ℤ) := by
712   rw [G.pathZeta_eq_matrixPathZeta s t]
713   rfl
714 
715 /-- Automatic rationality, now derived from finite graph data alone. -/
716 theorem transferDenominator_mul_matrixPathZeta (s t : V) :
717     (G.transferDenominator : PowerSeries ℤ) * G.matrixPathZeta s t =
718       (G.transferNumerator s t : PowerSeries ℤ) := by
719   rw [matrixPathZeta, ← mul_assoc, G.transferDenominator_mul_inverse, one_mul]
720 
721 /-- Canonical determinant/adjugate identity for the enumerated walk series `pathZeta`. -/
722 theorem transferDenominator_mul_pathZeta (s t : V) :
723     (G.transferDenominator : PowerSeries ℤ) * G.pathZeta s t =
724       (G.transferNumerator s t : PowerSeries ℤ) := by
725   rw [G.pathZeta_eq_matrixPathZeta s t]
726   exact G.transferDenominator_mul_matrixPathZeta s t
727 
728 /--
729 The automatically generated determinant gives an eventual constant-coefficient
730 recurrence for the enumerated walk counts.
731 -/
732 theorem finite_graph_constant_coefficient_recurrence (s t : V)
733     {n : ℕ} (hn : (G.transferNumerator s t).natDegree < n) :
734     ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n,
735         G.transferDenominator.coeff p.1 *
736           (G.coefficientAlgorithm s t p.2 : ℤ) = 0 := by
737   have hcoeff := congrArg (PowerSeries.coeff n)
738     (G.transferDenominator_mul_pathZeta s t)
739   rw [PowerSeries.coeff_mul] at hcoeff
740   simpa [Polynomial.coeff_eq_zero_of_natDegree_lt hn] using hcoeff
741 
742 /--
743 Packaged certificate-free rationality theorem for the canonical matrix entry.
744 Unlike `certificate_explicit_rationality`, its only input is the finite graph.
745 -/
746 theorem finite_graph_matrix_rationality (s t : V) :
747     ∃ P Q : Polynomial ℤ,
748       Q.coeff 0 = 1 ∧ Q ≠ 0 ∧
749         (Q : PowerSeries ℤ) * G.matrixPathZeta s t = (P : PowerSeries ℤ) := by
750   exact ⟨G.transferNumerator s t, G.transferDenominator,
751     G.transferDenominator_coeff_zero, G.transferDenominator_ne_zero,
752     G.transferDenominator_mul_matrixPathZeta s t⟩
753 
754 /--
755 Automatic rationality of the original enumerated `pathZeta`.  The numerator
756 and denominator are computed from the finite graph as an adjugate entry and
757 the determinant of `I - A(X)`; no coefficientwise rationality premise occurs.
758 -/
759 theorem finite_graph_pathZeta_rationality (s t : V) :
760     ∃ P Q : Polynomial ℤ,
761       Q.coeff 0 = 1 ∧ Q ≠ 0 ∧
762         (Q : PowerSeries ℤ) * G.pathZeta s t = (P : PowerSeries ℤ) := by
763   refine ⟨G.transferNumerator s t, G.transferDenominator,
764     G.transferDenominator_coeff_zero, G.transferDenominator_ne_zero, ?_⟩
765   exact G.transferDenominator_mul_pathZeta s t
766 
767 /--
768 Direct traceability wrapper for the composite finite-graph transfer-zeta
769 theorem in Paper II: the finite coefficient algorithm counts semantic walks,
770 the coefficients satisfy the first-edge recurrence, and the canonical
771 determinant/adjugate data give the normalized rational identity.
772 -/
773 theorem finite_graph_transferZeta_trace (s t : V) :
774     (∀ n : ℕ,
775       G.coefficientAlgorithm s t n = Fintype.card (G.ExactWalk s t n)) ∧
776     (∀ n : ℕ,
777       G.coefficientAlgorithm s t n =
778         (if s = t ∧ n = 0 then 1 else 0) +
779           ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
780             G.coefficientAlgorithm (G.target e) t (n - G.weight e) else 0) ∧
781     G.transferDenominator.coeff 0 = 1 ∧
782     G.transferDenominator ≠ 0 ∧
783     (G.transferDenominator : PowerSeries ℤ) * G.pathZeta s t =
784       (G.transferNumerator s t : PowerSeries ℤ) := by
785   exact ⟨G.coefficientAlgorithm_eq_card_exactWalk s t,
786     G.coefficientAlgorithm_firstEdge s t,
787     G.transferDenominator_coeff_zero,
788     G.transferDenominator_ne_zero,
789     G.transferDenominator_mul_pathZeta s t⟩
790 
791 omit [Fintype V] in
792 /--
793 Direct traceability wrapper for the path-zeta algorithm row.  For each target
794 weight it records both semantic correctness of the returned cardinality and
795 the first-edge recurrence used by the subsequent matrix construction.
796 -/
797 theorem pathZetaAlgorithm_trace (s t : V) (n : ℕ) :
798     G.coefficientAlgorithm s t n = Fintype.card (G.ExactWalk s t n) ∧
799     G.coefficientAlgorithm s t n =
800       (if s = t ∧ n = 0 then 1 else 0) +
801         ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
802           G.coefficientAlgorithm (G.target e) t (n - G.weight e) else 0 := by
803   exact ⟨G.coefficientAlgorithm_eq_card_exactWalk s t n,
804     G.coefficientAlgorithm_firstEdge s t n⟩
805 
806 end FiniteTransferRationality
807 
808 /--
809 An explicit rationality certificate.  Its final field is a coefficient-level
810 identity, so checking the certificate never invokes a symbolic matrix inverse.
811 -/
812 structure RationalCertificate [Fintype E] [DecidableEq E] [DecidableEq V]
813     (G : PositiveWeightedMultigraph V E) (s t : V) where
814   numerator : Polynomial ℤ
815   denominator : Polynomial ℤ
816   denominator_constant : denominator.coeff 0 = 1
817   coefficient_identity : ∀ n : ℕ,
818     ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n,
819         denominator.coeff p.1 * (G.coefficientAlgorithm s t p.2 : ℤ) =
820       numerator.coeff n
821 
822 namespace RationalCertificate
823 
824 variable [Fintype E] [DecidableEq E] [DecidableEq V]
825   {G : PositiveWeightedMultigraph V E} {s t : V}
826 
827 /-- Normalization at zero forces the certified denominator to be nonzero. -/
828 theorem denominator_ne_zero (c : RationalCertificate G s t) :
829     c.denominator ≠ 0 := by
830   intro hzero
831   have h : (0 : ℤ) = 1 := by
832     simpa [hzero] using c.denominator_constant
833   exact Int.zero_ne_one h
834 
835 /-- The coefficient certificate checks the formal identity `Q Z = P`. -/
836 theorem mul_pathZeta_eq (c : RationalCertificate G s t) :
837     (c.denominator : PowerSeries ℤ) * G.pathZeta s t =
838       (c.numerator : PowerSeries ℤ) := by
839   ext n
840   rw [PowerSeries.coeff_mul]
841   simpa using c.coefficient_identity n
842 
843 /--
844 Certificate-explicit rationality: a supplied certificate yields normalized,
845 nonzero `Q` and the exact formal identity `Q Z = P`.
846 -/
847 theorem certificate_explicit_rationality (c : RationalCertificate G s t) :
848     ∃ P Q : Polynomial ℤ,
849       Q.coeff 0 = 1 ∧ Q ≠ 0 ∧
850         (Q : PowerSeries ℤ) * G.pathZeta s t = (P : PowerSeries ℤ) := by
851   exact ⟨c.numerator, c.denominator, c.denominator_constant,
852     c.denominator_ne_zero, c.mul_pathZeta_eq⟩
853 
854 /--
855 After the numerator's finite initial range, the walk counts obey the constant-
856 coefficient recurrence encoded by the certified denominator.
857 -/
858 theorem constant_coefficient_recurrence (c : RationalCertificate G s t)
859     {n : ℕ} (hn : c.numerator.natDegree < n) :
860     ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n,
861         c.denominator.coeff p.1 * (G.coefficientAlgorithm s t p.2 : ℤ) = 0 := by
862   rw [c.coefficient_identity n]
863   exact Polynomial.coeff_eq_zero_of_natDegree_lt hn
864 
865 end RationalCertificate
866 
867 end PositiveWeightedMultigraph
868 
869 end Komorebi.PaperII.TransferZeta

Back to source controls