CompanionBridge.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.EntireBridge
6 import KomorebiPaperIV.FiniteModels
7 
8 /-!
9 # Matrix exponential and entire signed sections
10 
11 These results identify the first column and the diagonal of the matrix
12 exponential by convergent sums. They do not assume ODE uniqueness, a
13 characteristic polynomial, or a determinant-of-exponential formula.
14 -/
15 
16 namespace Komorebi.PaperIV
17 open scoped PowerSeries
18 noncomputable section
19 
20 /-- The scalar series for any entry of the actual matrix exponential. -/
21 theorem hasSum_signedFundamentalMatrix_entry (N : ℕ) (z : ℂ) (p q : Fin N) :
22     HasSum (fun m => (m.factorial : ℂ)⁻¹ * z ^ m *
23         (signedShiftMatrix (R := ℂ) N ^ m) p q)
24       (signedFundamentalMatrix N z p q) := by
25   let h := by
26     open scoped Matrix.Norms.Operator in
27     exact NormedSpace.exp_series_hasSum_exp' (𝕂 := ℂ) (z • signedShiftMatrix (R := ℂ) N)
28   have he := Pi.hasSum.mp (Pi.hasSum.mp h p) q
29   simp only [smul_pow, Matrix.smul_apply, smul_eq_mul] at he
30   convert he using 1 <;> try rfl
31   funext m
32   ring
33 
34 /-- The first column is exactly the analytic signed-section vector. -/
35 theorem signedFundamentalMatrix_first_column {N : ℕ} (hN : 0 < N)
36     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
37     (z : ℂ) (p : Fin N) :
38     signedFundamentalMatrix N z p ⟨0, hN⟩ = entireSigned N p.val omega rho z := by
39   have h := hasSum_signedFundamentalMatrix_entry N z p ⟨0, hN⟩
40   apply h.unique
41   convert hasSum_entireSigned hN p.isLt homega hrho z using 1
42   funext m
43   rw [signedShiftMatrix_pow_apply N m hN, coeff_signedSection]
44   simp only [Nat.zero_add, signedSectionCoeff]
45   by_cases he : p.val = m % N
46   · simp [he, mul_comm, mul_assoc]
47   · simp [he, Ne.symm he]
48 
49 private theorem signedShift_diagonal_power (N m : ℕ) (hN : 0 < N) (p : Fin N) :
50     (signedShiftMatrix (R := ℂ) N ^ m) p p =
51       if m % N = 0 then (-1 : ℂ) ^ (m / N) else 0 := by
52   rw [signedShiftMatrix_pow_apply N m hN]
53   have hp := p.isLt
54   have he : p.val = (p.val + m) % N ↔ m % N = 0 := by
55     have hm := Nat.mod_lt m hN
56     rw [Nat.add_mod, Nat.mod_eq_of_lt hp]
57     by_cases hs : p.val + m % N < N
58     · rw [Nat.mod_eq_of_lt hs]
59       omega
60     · rw [Nat.mod_eq_sub_mod (by omega), Nat.mod_eq_of_lt (by omega)]
61       omega
62   by_cases hm : m % N = 0
63   · have hd : (p.val + m) / N = m / N := by
64       have hm' : m = N * (m / N) := by
65         simpa [hm] using (Nat.div_add_mod m N).symm
66       conv_lhs => rw [hm']
67       rw [Nat.add_mul_div_left p.val (m / N) hN, Nat.div_eq_of_lt hp, zero_add]
68     simp only [ite_eq_left (he.mpr hm), ite_eq_left hm, hd]
69   · simp only [ite_eq_right hm, ite_eq_right (he.not.mpr hm)]
70 
71 /-- Every diagonal entry is the distinguished signed denominator. -/
72 theorem signedFundamentalMatrix_diagonal {N : ℕ} (hN : 0 < N)
73     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
74     (z : ℂ) (p : Fin N) :
75     signedFundamentalMatrix N z p p = entireSigned N 0 omega rho z := by
76   have h := hasSum_signedFundamentalMatrix_entry N z p p
77   apply h.unique
78   convert hasSum_entireSigned hN hN homega hrho z using 1
79   funext m
80   rw [signedShift_diagonal_power N m hN, coeff_signedSection]
81   simp only [signedSectionCoeff]
82   split_ifs <;> simp [mul_comm, mul_assoc]
83 
84 /-- The trace formula in Theorem 6.4, with no spectral certificate premise. -/
85 theorem signedFundamentalMatrix_trace {N : ℕ} (hN : 0 < N)
86     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
87     (z : ℂ) :
88     Matrix.trace (signedFundamentalMatrix N z) =
89       (N : ℂ) * entireSigned N 0 omega rho z := by
90   classical
91   simp [Matrix.trace, Matrix.diag, signedFundamentalMatrix_diagonal hN homega hrho]
92 
93 end
94 end Komorebi.PaperIV

Back to source controls